diff options
| -rw-r--r-- | exercices-inf110.tex | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/exercices-inf110.tex b/exercices-inf110.tex index 43ca6c6..6b1f15b 100644 --- a/exercices-inf110.tex +++ b/exercices-inf110.tex @@ -1945,8 +1945,8 @@ 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. +Proof. intro H. destruct H. split. intro H1. apply H1. exact H. +intro H2. exact H. split. intro H1. exact H. intro H2. apply H2. exact H. Qed. \par} @@ -1960,13 +1960,13 @@ preuve en question : \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) +\lambda(h_2:B\Rightarrow A).\,h_2 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) + | or\_intror H0 => conj (fun H1 : A -> B => H0) (fun H2 : B -> A => H2 H0) end)}) \end{corrige} |