summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--transp-inf110-03-quantif.tex26
1 files changed, 17 insertions, 9 deletions
diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex
index 78b6e27..beaac0b 100644
--- a/transp-inf110-03-quantif.tex
+++ b/transp-inf110-03-quantif.tex
@@ -162,7 +162,7 @@ $\forall v. P(v)$ {\footnotesize (« une façon de transformer $v$ en un
témoignage de $P(v)$ »)}, qui est une sorte de \emph{conjonction en
famille} $\bigwedge_v P(v)$, correspondra au \alert{type produit en
famille} $\prod_v \sigma(v)$ {\footnotesize (« fonction renvoyant
- une valeur de $\sigma(v)$ pour chaque $v$ »)}.
+ pour chaque $v$ une valeur de $\sigma(v)$ »)}.
\medskip
@@ -232,7 +232,7 @@ $t_0$ correspondant dans autre chose qu'une preuve. {\footnotesize
\frametitle{Règles d'introduction et d'élimination de $\forall$}
{\footnotesize\textcolor{orange}{Les règles ci-dessous (et
- transp. suivant) sont \alert{incomplètes} : il manque des
+ transp. suivants) sont \alert{incomplètes} : il manque des
explications sur le type $I$ sur lequel on quantifie et comment on
peut en former des « termes ».}\par}
@@ -383,6 +383,8 @@ ces notations pour $\forall, \exists$ :
si $s$ désigne une preuve de $Q$ faisant intervenir $v$ variable libre
de type $I$, on notera $\lambda(v:I).\,s$ la preuve de
$\forall(v:I).\,Q$ obtenue par introduction du $\forall$.
+{\footnotesize (\textbf{N.B.} $v$ peut apparaître dans $Q$ mais pas
+ dans $\Gamma$.)}
\[
\inferrule{\Gamma, v:I\vdash s:Q}{\Gamma\vdash \lambda(v:I).\,s\;:\;\forall (v:I).\, Q}
\]
@@ -394,6 +396,9 @@ $f$ désigne une preuve de $\forall(v:I).\,Q$ et $t$ un terme de
type $I$, on notera $ft$ la preuve de $Q[v\backslash t]$ {\footnotesize
(c'est-à-dire $Q$ avec $v$ remplacé par $t$)} obtenue par
élimination du $\forall$ sur ce terme.
+
+{\footnotesize (\textbf{N.B.} on n'explique pas comment le « terme »
+ $t$ est formé.)}
\[
\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash f \;:\; \forall (v:I).\, Q}{\Gamma\vdash ft \;:\; Q[v\backslash t]}
\]
@@ -401,8 +406,8 @@ type $I$, on notera $ft$ la preuve de $Q[v\backslash t]$ {\footnotesize
\medskip
\itempoint Ceci est conforme à l'idée de BHK : une preuve de
-$\forall(v:I).\, Q(v)$ prend un $t$ de type $I$ et renvoie une preuve
-de $Q(t)$.
+$\forall(v:I).\, Q(v)$ prend un $x$ de type $I$ et renvoie une preuve
+de $Q(x)$.
\end{frame}
%
@@ -421,11 +426,14 @@ du $\exists$.
\medskip
\itempoint \textcolor{blue}{\underline{Élimination du $\exists$ :}} si
-$z$ désigne une preuve de $\exists(v:I).\,P$ et $s$ une preuve de $Q$
-faisant intervenir $v$ variable libre de type $I$ et $h$ hypothèse
-supposant $P$ (pour ce $v$-là, donc), on notera
-$(\texttt{match~}z\texttt{~with~}\langle v,h\rangle \mapsto s)$ la
-preuve de $Q$ obtenue par élimination du $\exists$.
+$z$ désigne une preuve de $\exists(v:I).\,P$ et $s$ une preuve,
+faisant intervenir $v$ variable libre de type $I$, de $Q$ qui ne fait
+pas intervenir $v$, et $h$ hypothèse supposant $P$ (pour ce $v$-là,
+donc), on notera $(\texttt{match~}z\texttt{~with~}\langle v,h\rangle
+\mapsto s)$ la preuve de $Q$ obtenue par élimination du $\exists$.
+
+{\footnotesize (\textbf{N.B.} $v$ peut apparaître dans $s$ mais pas
+ dans $\Gamma$ ni $Q$.)}
\[
\inferrule{\Gamma\vdash z \;:\; \exists (v:I).\, P\\\Gamma,\, v:I,\, h:P\vdash Q}{\Gamma\vdash (\texttt{match~}z\texttt{~with~}\langle v,h\rangle \mapsto s) \;:\; Q}
\]