diff options
Diffstat (limited to 'transp-inf110-03-quantif.tex')
| -rw-r--r-- | transp-inf110-03-quantif.tex | 20 |
1 files changed, 19 insertions, 1 deletions
diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex index 867d04d..0e1891f 100644 --- a/transp-inf110-03-quantif.tex +++ b/transp-inf110-03-quantif.tex @@ -528,6 +528,20 @@ Doit-on croire à ceci (pour $U$ et $V$ deux types) ? \Rightarrow (\exists(f:U\Rightarrow V).\,\forall(x:U).\,P(x,f(x))) \] +{\footnotesize +\[ +\begin{aligned} +\text{« preuve(?) » :~} +\lambda(h:\cdots).\, +\langle +&\lambda(x:U).\, +(\texttt{match~}hx\texttt{~with~}\langle v,z\rangle \mapsto v),\\ +&\lambda(x:U).\, +(\texttt{match~}hx\texttt{~with~}\langle v,z\rangle \mapsto z) +\rangle +\end{aligned} +\] +\par} \medskip @@ -553,11 +567,15 @@ fonction. \medskip +{\footnotesize + \itempoint C'est ici la différence principale entre des systèmes comme Coq (où l'énoncé ci-dessus ne sera pas prouvable pour $P : U\times V \to \mathit{Prop}$) et les systèmes à la Martin-Löf comme Agda (où Curry-Howard est suivi « jusqu'au bout » : il n'y a pas de $\exists$ -uniquement logique, et cet énoncé est prouvable). +uniquement logique, et cet énoncé est prouvable comme indiqué). + +\par} \end{frame} % |