diff options
| -rw-r--r-- | transp-inf110-03-quantif.tex | 26 |
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} \] |