From f1df8ae273381697fd7b56ca68d1cfa7a48aafe4 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Sun, 3 Dec 2023 19:34:31 +0100
Subject: An example of Curry-Howard with implication.

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

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 95c0dae..a28dbce 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -944,6 +944,7 @@ partir des hypothèses portées \alert{au-dessus}.
 \end{frame}
 %
 \begin{frame}
+\label{example-typing-derivation}
 \frametitle{Exemple de dérivation}
 
 Montrons le jugement selon lequel
@@ -1928,6 +1929,36 @@ dérivation.
 arbres de preuve en déduction naturelle du calcul propositionnel
 intuitionniste restreint au seul connecteur $\Rightarrow$.
 
+\end{frame}
+%
+\begin{frame}
+\frametitle{Correspondance de Curry-Howard : exemple avec implication}
+
+\itempoint Transformons en démonstration le terme
+\[\lambda(f:\beta\to\alpha\to\gamma). \lambda(x:\alpha). \lambda(y:\beta). fyx\]
+qu'on a typé (transp. \ref{example-typing-derivation}) comme
+$(\beta\to\alpha\to\gamma) \to (\alpha\to\beta\to\gamma)$ :
+
+{\footnotesize
+\[
+\inferrule*[left=\llap{$\Rightarrow$Élim}]{
+\inferrule*[left=\llap{$\Rightarrow$Élim}]{
+\inferrule*[left=\llap{$\Rightarrow$Élim}]{
+\inferrule*[left=\llap{$\Rightarrow$Int}]{
+\inferrule*[left=\llap{$\Rightarrow$Int}]{
+\inferrule*[left=\llap{Ax}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle B \Rightarrow A \Rightarrow C ,\\ \scriptscriptstyle A ,B \\ \end{array}$} \vdash B \Rightarrow A \Rightarrow C }
+\\
+\inferrule*[right=\rlap{Ax}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle B \Rightarrow A \Rightarrow C ,\\ \scriptscriptstyle A ,B \\ \end{array}$} \vdash B }
+}{\mbox{$\begin{array}{cc}\scriptscriptstyle B \Rightarrow A \Rightarrow C ,\\ \scriptscriptstyle A ,B \\ \end{array}$} \vdash A \Rightarrow C }
+\\
+\inferrule*[right=\rlap{Ax}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle B \Rightarrow A \Rightarrow C ,\\ \scriptscriptstyle A ,B \\ \end{array}$} \vdash A }
+}{B \Rightarrow A \Rightarrow C , A , B  \vdash C }
+}{B \Rightarrow A \Rightarrow C , A  \vdash B \Rightarrow C }
+}{B \Rightarrow A \Rightarrow C  \vdash A \Rightarrow B \Rightarrow C }
+}{\vdash (B \Rightarrow A \Rightarrow C ) \Rightarrow  (A \Rightarrow B \Rightarrow C )}
+\]
+\par}
+
 \end{frame}
 %
 \begin{frame}
-- 
cgit v1.2.3