An example of Curry-Howard with disjunction.

1 files changed, 41 insertions, 0 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 05d3797..e2419ac 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -2103,6 +2103,47 @@ doute sur la correspondance elle-même.
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Correspondance de Curry-Howard : exemple avec conjonction}
+
+\itempoint Transformons en programme la démonstration qu'on a donnée
+de $A\lor B \Rightarrow B\lor A$
+(transp. \ref{example-propositional-proofs} et suivants) :
+
+{\footnotesize
+\[
+\inferrule*[left={Abs},right=\hphantom{Int}]{
+\inferrule*[left=\llap{Match}]{
+\inferrule*[left=\llap{Var}]{ }{u:\alpha+\beta \vdash u:\alpha+\beta}
+\\
+\inferrule*[right={Inj$_2$}]{
+\inferrule*[right=\rlap{Var}]{ }{\ldots,v:\alpha \vdash v:\alpha}
+}{{\scriptstyle\cdots} \vdash \iota_2^{(\beta,\alpha)} v : \beta+\alpha}
+\\
+\inferrule*[right=\rlap{Inj$_1$}]{
+\inferrule*[right=\rlap{Var}]{ }{\ldots,v':\beta \vdash v':\beta}
+}{{\scriptstyle\cdots} \vdash \iota_1^{(\beta,\alpha)} v' : \beta+\alpha}
+}{u:\alpha+\beta \vdash (\texttt{match~} u\texttt{~with~}\iota_1
+  v \mapsto \iota^{(\beta,\alpha)}_2 v,\; \iota_2 v' \mapsto \iota_1^{(\beta,\alpha)} v') : \beta+\alpha}
+}{\vdash \lambda (u:\alpha+\beta) .
+(\texttt{match~} u\texttt{~with~}\iota_1
+  v \mapsto \iota^{(\beta,\alpha)}_2 v,\; \iota_2 v' \mapsto \iota_1^{(\beta,\alpha)} v') : \alpha+\beta \to \beta+\alpha}
+\]
+\par}
+
+\bigskip
+
+\itempoint Il s'agit de la fonction
+\[
+\lambda (u:\alpha+\beta) .
+(\texttt{match~} u\texttt{~with~}\iota_1
+  v \mapsto \iota^{(\beta,\alpha)}_2 v,\; \iota_2 v' \mapsto \iota_1^{(\beta,\alpha)} v')
+\]
+(polymorphe de type $\alpha+\beta \to \beta+\alpha$) qui échange les
+deux cas d'une somme.
+
+\end{frame}
+%
 % TODO:
 % - substitution des variables propositionnelles par des formules
 % - substitution d'équivalences