From 7b5f152d4abc26ebe068d4296bb3e9986079b488 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Sat, 16 Dec 2023 22:19:34 +0100
Subject: Give the proof in Coq as well.

---
 exercices-inf110.tex | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)

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}
 
 
-- 
cgit v1.2.3