Give the proof in Coq as well.

1 files changed, 29 insertions, 0 deletions

diff --git a/exercices-inf110.tex b/exercices-inf110.tex
index 70cce79..43ca6c6 100644
--- a/exercices-inf110.tex
+++ b/exercices-inf110.tex
@@ -1939,6 +1939,35 @@ finale).  Dans les deux cas de la disjonction on a montré
 $(A\Rightarrow B)\Rightarrow B$.  Donc finalement $A\lor B \Rightarrow
 ((A\Rightarrow B) \Rightarrow B) \land ((B\Rightarrow A) \Rightarrow
 A)$.
+
+En Coq, cette preuve s'écrit :
+
+{\tt
+Parameter A B C : Prop.\\
+Theorem thm : A\textbackslash /B -> ((A->B)->B) /\textbackslash\ ((B->A)->A).\\
+Proof.  intro H.  destruct H.  split.  intro H0.  apply H0.  exact H.
+intro H0.  exact H.  split.  intro H0. exact H.  intro H0. apply H0.
+exact H.  Qed.
+\par}
+
+On peut aussi directement donner un $\lambda$-terme correspondant à la
+preuve en question :
+\[
+\begin{aligned}
+\lambda(h:A\lor B).\,
+(\texttt{match~}h\texttt{~with~}&\iota_1 h_0
+\mapsto \langle \lambda(h_1:A\Rightarrow B).\,h_1 h_0,\;
+\lambda(h_2:B\Rightarrow A).\,h_0\rangle,\\
+&\iota_2 h_0
+\mapsto \langle \lambda(h_1:A\Rightarrow B).\,h_0,\;
+\lambda(h_2:B\Rightarrow A).\,h_1 h_0\rangle)
+\end{aligned}
+\]
+(ou en syntaxe Coq : \texttt{(fun H : A \textbackslash/ B =>
+ match H with
+   or\_introl H0 => conj (fun H1 : A -> B => H1 H0) (fun H2 : B -> A => H0)
+ | or\_intror H0 => conj (fun H2 : A -> B => H0) (fun H1 : B -> A => H1 H0)
+ end)})
 \end{corrige}