Start talking about cut elimination.

1 files changed, 79 insertions, 0 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index b31d1cb..6ce7248 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -1150,6 +1150,7 @@ chaque règle « variable ».
 \end{frame}
 %
 \begin{frame}
+\label{substitution-lemma}
 \frametitle{Lemme de substitution}
 
 \itempoint\textbf{Lemme :} Si $\Gamma, v:\sigma \vdash E : \tau$ et
@@ -2891,6 +2892,84 @@ $\inferrule*[left=$\Rightarrow$Élim]{
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Calcul des séquents : élimination des coupures}
+
+La règle de coupure exprime une forme de transitivité des démonstrations :
+\[
+\inferrule*[left=Cut]{\Gamma \vdash P\\\Gamma,P\vdash Q}{\Gamma\vdash Q}
+\]
+
+\medskip
+
+\itempoint \textbf{Théorème} (Gentzen) : la règle de « coupure » n'est
+pas nécessaire en calcul des séquents : tout séquent prouvable avec
+elle est encore prouvable sans elle.
+
+\smallskip
+
+La preuve est même constructive et se fait par des transformations
+« locales ».
+
+\medskip
+
+\itempoint En déduction naturelle, l'élimination des coupures est
+facile : pour éliminer une coupure il suffit de reprendre la
+démonstration de $\Gamma,P\vdash Q$ avec l'hypothèse $P$ en moins, et
+d'utiliser celle de $\Gamma\vdash P$ partout où $P$ est invoquée
+(cf. transp. \ref{substitution-lemma}).  {\footnotesize (La difficulté
+  est plutôt l'élimination de « détours » Intro+Élim $\approx$
+  normal\textsuperscript{ion}.)}
+
+\medskip
+
+\itempoint En calcul des séquents, la difficulté supplémentaire est
+que $P$ peut faire intervenir un connecteur introduit à droite dans
+$\Gamma\vdash P$ et à gauche dans $\Gamma,P\vdash Q$.
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Exemples d'étape d'élimination des coupures}
+
+\begin{center}
+\scalebox{0.8}{%
+$\inferrule*[left=Cut]{
+\inferrule*[left=\llap{$\land$R}]{\Gamma \vdash P_1\\\Gamma \vdash P_2}{\Gamma \vdash P_1\land P_2}
+\\
+\inferrule*[right=\rlap{$\land$L$_1$}]{\Gamma,P_1\vdash Q}{\Gamma,P_1\land P_2\vdash Q}
+}{\Gamma\vdash Q}$
+}
+~devient~
+\scalebox{0.8}{%
+$\inferrule*[left=Cut]{
+\Gamma \vdash P_1
+\\
+\Gamma,P_1\vdash Q
+}{\Gamma\vdash Q}$
+}
+\end{center}
+
+\begin{center}
+\scalebox{0.7}{%
+$\inferrule*[left=Cut]{
+\inferrule*[left=\llap{$\Rightarrow$R}]{\Gamma, M\vdash P}{\Gamma \vdash M\Rightarrow P}
+\\
+\inferrule*[right=\rlap{$\Rightarrow$L}]{\Gamma \vdash M\\\Gamma,P\vdash Q}{\Gamma,M\Rightarrow P\vdash Q}
+}{\Gamma\vdash Q}$
+}
+~devient~
+\scalebox{0.7}{%
+$\inferrule*[left=Cut]{
+\Gamma \vdash M
+\\
+\inferrule*[right=\rlap{Cut}]{\Gamma,M \vdash P\\\Gamma,P\vdash Q}{\Gamma,M\vdash Q}
+}{\Gamma\vdash Q}$
+}
+\end{center}
+
+\end{frame}
+%
 % TODO:
 % - présentation en calcul des séquents
 % - élimination des coupures