Wrap up exercise 3 and answer key.

1 files changed, 47 insertions, 12 deletions

diff --git a/controle-20260126.tex b/controle-20260126.tex
index 3f5e45e..7ef04e2 100644
--- a/controle-20260126.tex
+++ b/controle-20260126.tex
@@ -397,7 +397,9 @@ Parmi les buts suivants, quand peut-on utiliser ce lemme avec la tactique \textt
 
 \exercice
 
-\textbf{(A)} Pour chacun des termes de preuve Rocq suivants, retrouver le théorème du calcul propositionnel intuitionniste qu'il prouve.
+\textbf{(A)} Pour chacun des termes de preuve Rocq suivants, retrouver
+le théorème du calcul propositionnel intuitionniste qu'il prouve.
+(Ici, \texttt{A}, \texttt{B}, \texttt{C} vivent dans \texttt{Prop}.)
 
 \smallskip
 
@@ -409,32 +411,38 @@ Parmi les buts suivants, quand peut-on utiliser ce lemme avec la tactique \textt
 
 \smallskip
 
-\textbf{(3)} \verb|fun (H1 : A -> (B -> C)) (H2 : A) (H3 : B) => H1 H2 H3|
+\textbf{(3)} \verb|fun (H1 : A -> (B -> C)) (H2 : B) (H3 : A) => H1 H3 H2|
 
 \smallskip
 
-\textbf{(B)} Pour chaque formule logique suivante, en donner une démonstration en déduction naturelle (on donnera l'arbre de preuve ou la présentation
-en style drapeau, comme on préfère).
+\textbf{(B)} Pour chaque formule logique suivante, en donner une
+preuve (en calcul propositionnel intuitionniste pour (1)–(4)).  La
+preuve sera exprimée de préférence sous forme d'un $\lambda$-terme,
+qui n'a pas à être justifié si on est sûr qu'il est correct et qu'on
+veut gagner du temps ; toutefois, si on ne sait pas écrire le
+$\lambda$-terme ou si on a un doute à son sujet, on pourra donner une
+preuve en déduction naturelle (présentée comme arbre de preuve ou sous
+forme drapeau), qui vaudra au moins une partie des points.
 
 \smallskip
 
-\textbf{(1)} $A \Rightarrow A$.
+\textbf{(1)} $A \Rightarrow A$
 
 \smallskip
 
-\textbf{(2)} $(A \wedge B) \Rightarrow (B \wedge A)$.
+\textbf{(2)} $A \Rightarrow (A \land A)$
 
 \smallskip
 
-\textbf{(3)} $(A \vee B) \Rightarrow (B \vee A)$.
+\textbf{(3)} $(A \lor A) \Rightarrow A$
 
 \smallskip
 
-\textbf{(4)} $\neg(A \vee B) \Rightarrow \neg A$.
+\textbf{(4)} $\neg(A \lor B) \Rightarrow \neg A$
 
 \smallskip
 
-\textbf{(5)} $(\forall x,\; P(x)) \vee (\forall x,\; Q(x)) \Rightarrow (\forall x,\; P(x) \vee Q(x))$.
+\textbf{(5)} $((\forall x.\; P(x)) \lor (\forall x.\; Q(x))) \Rightarrow (\forall x.\; (P(x) \lor Q(x)))$ (en logique du premier ordre intuitionniste)
 
 \smallskip
 
@@ -446,12 +454,39 @@ en style drapeau, comme on préfère).
 
 \textbf{(A)}
 
-  \textbf{(1)} $A \Rightarrow B \Rightarrow B$.
+  \textbf{(1)} $A \Rightarrow B \Rightarrow B$
 
-  \textbf{(2)} $A \Rightarrow \neg \neg A$.
+  \textbf{(2)} $A \Rightarrow \neg \neg A$
 
-  \textbf{(3)} $(A \Rightarrow (B \Rightarrow C)) \Rightarrow A \Rightarrow B \Rightarrow C$.
+  \textbf{(3)} $(A \Rightarrow B \Rightarrow C) \Rightarrow B \Rightarrow A \Rightarrow C$
 
+\smallskip
+
+\textbf{(B)}
+
+  \textbf{(1)} $\lambda(u:A).\; u$
+
+  \textbf{(2)} $\lambda(u:A).\; \langle u,u\rangle$
+
+  \textbf{(3)} $\lambda(u:A\lor A).\; (\texttt{match~}u\texttt{~with~}
+  \iota_1 v \mapsto v,\; \iota_2 v \mapsto v)$ (noter qu'on peut
+  préférer l'écrire avec des noms de variables liées différentes dans
+  l'alternative : $\lambda(u:A\lor A).\;
+  (\texttt{match~}u\texttt{~with~} \iota_1 v_1 \mapsto
+  v_1,\penalty-100\; \iota_2 v_2 \mapsto v_2)$, c'est exactement
+  équivalent)
+
+  \textbf{(4)} $\lambda(h:\neg(A \lor B)).\; \lambda(u:A).\; h(\iota_1^{(A,B)} u)$
+
+  \textbf{(5)} $\lambda(h:(\forall x.\; P(x)) \lor (\forall x.\;
+  Q(x))).\; (\texttt{match~}h\texttt{~with~} \iota_1 g \mapsto
+  \lambda(x:I).\; \iota_1^{(P(x),Q(x))}(g x),\penalty-500\; \iota_2 g
+  \mapsto \lambda(x:I).\penalty0\; \iota_2^{(P(x),Q(x))}(g x))$ ou, si
+  on préfère, $\lambda(h:(\forall x.\; P(x)) \lor (\forall x.\;
+  Q(x))).\; \lambda(x:I).\penalty-500\;
+  (\texttt{match~}h\texttt{~with~} \iota_1 g \mapsto
+  \iota_1^{(P(x),Q(x))}(g x),\penalty-500\; \iota_2 g \mapsto
+  \iota_2^{(P(x),Q(x))}(g x))$
 \end{corrige}