An example of Curry-Howard with implication.

1 files changed, 31 insertions, 0 deletions

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
@@ -1931,6 +1932,36 @@ 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}
 \frametitle{Correspondance de Curry-Howard : conjonction}
 
 On veut \alert{étendre} le $\lambda$CST avec un \textbf{type produit}