From 791c6b3ecaf43c0857367db4feb58901337ae166 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Sun, 3 Dec 2023 20:41:57 +0100
Subject: An example of Curry-Howard with disjunction.

---
 transp-inf110-02-typage.tex | 41 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 41 insertions(+)

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
@@ -2101,6 +2101,47 @@ $\pi_i,\ \langle,\rangle,\ \iota_i,\ \texttt{match}...\texttt{with}$
 n'est standardisée (bcp de variations existent), mais il n'y a aucun
 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:
-- 
cgit v1.2.3