Examples of sequent calculus proofs.

1 files changed, 74 insertions, 3 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index cae26b4..32ff068 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -1985,6 +1985,7 @@ intuitionniste restreint au seul connecteur $\Rightarrow$.
 \end{frame}
 %
 \begin{frame}
+\label{example-proposition-proof-with-implication}
 \frametitle{Correspondance de Curry-Howard : exemple avec implication}
 
 \itempoint Transformons en démonstration le terme
@@ -1994,11 +1995,11 @@ $(\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{$\Rightarrow$Int}]{
+\inferrule*[left=\llap{$\Rightarrow$Élim}]{
+\inferrule*[left=\llap{$\Rightarrow$Élim}]{
 \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 }
@@ -2719,6 +2720,76 @@ $\bot$
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Exemples de démonstrations en calcul des séquents}
+
+On reprend les mêmes exemples que dans le
+transp. \ref{example-propositional-proofs} :
+\vskip-5ex\leavevmode
+\begin{center}
+\begin{tabular}{c|c}
+%
+{\footnotesize
+$
+\inferrule*[left={$\Rightarrow$R},right=\hphantom{Int}]{
+\inferrule*[left=\llap{$\land$R}]{
+\inferrule*[left=\llap{$\land$L$_2$}]{
+\inferrule*[left=\llap{Ax}]{ }{B \vdash B}
+}{A\land B \vdash B}
+\\
+\inferrule*[right=\rlap{$\land$L$_1$}]{
+\inferrule*[right=\rlap{Ax}]{ }{A \vdash A}
+}{A\land B \vdash A}
+}{A\land B \vdash B\land A}
+}{\vdash A\land B \Rightarrow B\land A}
+$
+}
+&
+{\footnotesize
+$
+\inferrule*[left={$\Rightarrow$R},right=\hphantom{Int}]{
+\inferrule*[left=\llap{$\lor$L}]{
+\inferrule*[left=\llap{$\lor$R$_2$}]{
+\inferrule*[left=\llap{Ax}]{ }{A \vdash A}
+}{A \vdash B\lor A}
+\\
+\inferrule*[right=\rlap{$\lor$R$_1$}]{
+\inferrule*[right=\rlap{Ax}]{ }{B \vdash B}
+}{B \vdash B\lor A}
+}{A\lor B \vdash B\lor A}
+}{\vdash A\lor B \Rightarrow B\lor A}
+$
+}
+\end{tabular}
+\end{center}
+
+\medskip
+
+Et que dans le transp. \ref{example-proposition-proof-with-implication} :
+
+\vskip-2ex
+{\footnotesize
+\[
+\inferrule*[left=\llap{$\Rightarrow$R}]{
+\inferrule*[left=\llap{$\Rightarrow$R}]{
+\inferrule*[left=\llap{$\Rightarrow$R}]{
+\inferrule*[left=\llap{$\Rightarrow$L}]{
+\inferrule*[left=\llap{Ax}]{ }{A, B \vdash B }
+\\
+\inferrule*[right=\rlap{$\Rightarrow$L}]{
+\inferrule*[left=\llap{Ax}]{ }{A , B  \vdash A }
+\\
+\inferrule*[right=\rlap{Ax}]{ }{C , A , B  \vdash C  }
+}{A \Rightarrow C , A , B  \vdash C }
+}{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}
+%
 % TODO:
 % - présentation en calcul des séquents
 % - élimination des coupures