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