diff options
Diffstat (limited to 'exercices-inf110.tex')
| -rw-r--r-- | exercices-inf110.tex | 29 |
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} |