1 files changed, 64 insertions, 2 deletions
diff --git a/controle-20250129.tex b/controle-20250129.tex
index 474e0c9..e5549be 100644
--- a/controle-20250129.tex
+++ b/controle-20250129.tex
@@ -379,7 +379,7 @@ Parmi les buts suivants, quand peut-on utiliser ce lemme avec la tactique \textt
 
 \exercice
 
-Dans cet exercice, on donne un terme de preuve Coq et on demande de retrouver le théorème du calcul propositionnel intuitionniste qu'il prouve.
+\textbf{(A)} Dans cet exercice, on donne un terme de preuve Coq et on demande de retrouver le théorème du calcul propositionnel intuitionniste qu'il prouve.
 
 \smallskip
 
@@ -393,14 +393,76 @@ Dans cet exercice, on donne un terme de preuve Coq et on demande de retrouver le
 
 \textbf{(3)} \verb|fun (H1 : A -> B) (H2 : ~ B) => (fun (H3 : A) => H2 (H1 H3))|
 
+\smallskip
+
+\textbf{(B)} Écrire la démonstration décrite par le terme (3) en
+déduction naturelle (on donnera l'arbre de preuve ou la présentation
+en style drapeau, comme on préfère).
+
 \begin{corrige}
   \smallskip
 
-  \textbf{(1)} $A \Rightarrow A$.
+\textbf{(A)} \textbf{(1)} $A \Rightarrow A$.
 
   \textbf{(2)} $(A \Rightarrow B) \Rightarrow (B \Rightarrow C) \Rightarrow A \Rightarrow C$.
 
   \textbf{(3)} $(A \Rightarrow B) \Rightarrow \neg B \Rightarrow \neg A$.
+
+\medskip
+
+\textbf{(B)} Voici la démonstration de (3) écrite en arbre de preuve :
+\begin{footnotesize}
+\[
+\inferrule*[left={$\Rightarrow$Int}]{
+\inferrule*[Left={$\Rightarrow$Int}]{
+\inferrule*[Left={$\Rightarrow$Int}]{
+\inferrule*[Left={$\Rightarrow$Élim}]{
+\inferrule*[Left={Ax}]{ }{(A \Rightarrow B), \neg B, A \vdash \neg B}\\
+\inferrule*[Right={$\Rightarrow$Élim}]{
+\inferrule*[Left={Ax}]{ }{(A \Rightarrow B), \neg B, A \vdash A\Rightarrow B}\\
+\inferrule*[Right={Ax}]{ }{(A \Rightarrow B), \neg B, A \vdash A}
+}{(A \Rightarrow B), \neg B, A \vdash B}
+}{(A \Rightarrow B), \neg B, A \vdash \bot}
+}{(A \Rightarrow B), \neg B \vdash A \Rightarrow \bot}
+}{A \Rightarrow B \vdash \neg B \Rightarrow \neg A}
+}{\vdash (A \Rightarrow B) \Rightarrow \neg B \Rightarrow \neg A}
+\]
+\end{footnotesize}
+ou avec uniquement les conclusions de chaque séquent, et en indiquant
+les noms comme dans le terme Coq :
+\begin{footnotesize}
+\[
+\inferrule*[left={$\Rightarrow$Int($H_1$)}]{
+\inferrule*[Left={$\Rightarrow$Int($H_2$)}]{
+\inferrule*[Left={$\Rightarrow$Int($H_3$)}]{
+\inferrule*[Left={$\Rightarrow$Élim}]{
+\inferrule*[Left={$H_2$}]{ }{\neg B}\\
+\inferrule*[Right={$\Rightarrow$Élim}]{
+\inferrule*[Left={$H_1$}]{ }{A\Rightarrow B}\\
+\inferrule*[Right={$H_3$}]{ }{A}
+}{B}
+}{\bot}
+}{A \Rightarrow \bot}
+}{\neg B \Rightarrow \neg A}
+}{(A \Rightarrow B) \Rightarrow \neg B \Rightarrow \neg A}
+\]
+\end{footnotesize}
+et la voici écrite dans le style « drapeau » :
+\bgroup\normalsize
+\begin{footnotesize}
+\begin{flagderiv}[exercice-3-proof]
+\assume{hyp1}{A\Rightarrow B}{}
+\assume{hyp2}{\neg B}{}
+\assume{hyp3}{A}{}
+\step{subconcb}{B}{$\Rightarrow$Élim sur \ref{hyp1} et \ref{hyp3}}
+\step{subconcbot}{\bot}{$\Rightarrow$Élim sur \ref{hyp2} et \ref{subconcb}}
+\conclude{subconcnega}{A \Rightarrow \bot}{$\Rightarrow$Int de \ref{hyp3} dans \ref{subconcbot}}
+\conclude{subconcimp}{\neg B \Rightarrow \neg A}{$\Rightarrow$Int de \ref{hyp2} dans \ref{subconcnega}}
+\conclude{subconcimp}{(A \Rightarrow B) \Rightarrow \neg B \Rightarrow \neg A}{$\Rightarrow$Int de \ref{hyp1} dans \ref{subconcimp}}
+\end{flagderiv}
+\end{footnotesize}
+\egroup
+\vskip-4ex\leavevmode
 \end{corrige}