Incorporate Coq exercises provided by TZ.

1 files changed, 363 insertions, 1 deletions

diff --git a/controle-20250129.tex b/controle-20250129.tex
index e2a28c3..74b2d52 100644
--- a/controle-20250129.tex
+++ b/controle-20250129.tex
@@ -127,7 +127,369 @@ Git: \input{vcline.tex}
 %
 %
 
-\bigbreak
+\exercice
+
+Dans cet exercice, on considère des paires d'états d'une preuve en Coq avant et après l'application d'une tactique. On demande de retrouver quelle est la tactique ou la séquence de tactiques appliquée.
+
+\smallskip
+
+\textbf{(1)} On part de l'état suivant :
+
+\begin{verbatim}
+  A, B, C : Prop
+  ============================
+  (A /\ B) /\ C <-> A /\ B /\ C
+\end{verbatim}
+
+et on veut arriver à l'état suivant :
+
+\begin{verbatim}
+First subgoal:
+  
+  A, B, C : Prop
+  ============================
+  (A /\ B) /\ C -> A /\ B /\ C
+
+Second subgoal:
+
+  A, B, C : Prop
+  ============================
+  A /\ B /\ C -> (A /\ B) /\ C
+\end{verbatim}
+
+\smallskip
+
+
+\textbf{(2)} On part de l'état suivant :
+
+\begin{verbatim}
+  A, B, C : Prop
+  H : (A /\ B) /\ C
+  ============================
+  A
+\end{verbatim}
+
+et on veut arriver à l'état suivant :
+
+\begin{verbatim}  
+  H1 : A
+  H2 : B
+  H3 : C
+  ============================
+  A
+\end{verbatim}
+
+\smallskip
+
+\textbf{(3)} On part de l'état suivant :
+
+\begin{verbatim}
+  A, B, C : Prop
+  H : A
+  ============================
+  A \/ B
+\end{verbatim}
+
+et on veut arriver à l'état suivant :
+
+\begin{verbatim}
+  No more goals.
+\end{verbatim}
+
+\smallskip
+
+\textbf{(4)} On part de l'état suivant :
+
+\begin{verbatim}
+  ============================
+  (A -> B) -> ~ B -> ~ A
+\end{verbatim}
+
+et on veut arriver à l'état suivant :
+
+\begin{verbatim}
+  H1 : A -> B
+  H2 : ~ B
+  H3 : A
+  ============================
+  False
+\end{verbatim}
+
+\smallskip
+
+\textbf{(5)} On part de l'état suivant :
+
+\begin{verbatim}
+  n, m : nat
+  ============================
+  n + m = m + n
+\end{verbatim}
+
+et on veut arriver à l'état suivant :
+
+\begin{verbatim}
+First subgoal:
+  
+  m : nat
+  ============================
+  0 + m = m + 0
+
+Second subgoal:
+
+  n, m : nat
+  IHn : n + m = m + n
+  ============================
+  S n + m = m + S n
+\end{verbatim}
+
+\smallskip
+
+\textbf{(6)} On part de l'état suivant :
+
+\begin{verbatim}
+  n, m : nat
+  ============================
+  S (n + m) = S (m + n)
+\end{verbatim}
+
+et on veut arriver à l'état suivant :
+
+\begin{verbatim}
+  n, m : nat
+  ============================
+  n + m = m + n
+\end{verbatim}
+
+\smallskip
+
+\textbf{(7)} On part de l'état suivant :
+
+\begin{verbatim}
+  n, m : nat
+  H : S n = S m
+  ============================
+  n + 1 = m + 1
+\end{verbatim}
+
+et on veut arriver à l'état suivant :
+
+\begin{verbatim}
+  n, m : nat
+  H : n = m
+  ============================
+  n + 1 = m + 1
+\end{verbatim}
+
+\begin{corrige}
+  \smallskip
+
+  \textbf{(1)} \verb|split|.
+
+
+  \textbf{(2)} En deux étapes : \verb|destruct H as (H1, H3). destruct H1 as (H1, H2).| Possible également en une seule étape : \verb|destruct H as ((H1, H2), H3).|
+
+
+  \textbf{(3)} \verb|left. assumption.|
+
+
+  \textbf{(4)} \verb|intros H1 H2 H3.|
+
+
+  \textbf{(5)} \verb+induction n as [|n IHn].+ ou simplement \verb|induction n.|
+
+
+  \textbf{(6)} \verb|f_equal.| (la tactique) ou \verb|apply f_equal.| (le lemme).
+
+
+  \textbf{(7)} \verb|injection H as H.|
+\end{corrige}
+
+%
+%
+%
+
+\exercice
+
+Si l'on dispose du lemme suivant en Coq :
+
+\begin{verbatim}
+  Lemma add_0_r : forall n : nat, n + 0 = n.
+\end{verbatim}
+
+Parmi les buts suivants, quand peut-on utiliser ce lemme avec la tactique \texttt{rewrite} ? Quand peut-on utiliser ce lemme avec la tactique \texttt{apply} ? Justifier brièvement.
+
+\smallskip
+
+\textbf{(1)}
+
+\begin{verbatim}
+  n : nat
+  ============================
+  n + 0 = 0 + n
+\end{verbatim}
+
+\smallskip
+
+\textbf{(2)}
+
+\begin{verbatim}
+  n, m : nat
+  ============================
+  (n + m) + 0 = m + n
+\end{verbatim}
+
+\smallskip
+
+\textbf{(3)}
+
+\begin{verbatim}
+  n, m : nat
+  ============================
+  (m * n) + 0 = m * n
+\end{verbatim}
+
+\smallskip
+
+\textbf{(4)}
+
+\begin{verbatim}
+  n, m : nat
+  ============================
+  (n + 0) + m = n + m
+\end{verbatim}
+
+\begin{corrige}
+  \smallskip
+
+  \textbf{(1)} On peut utiliser \texttt{rewrite -> add\_0\_r.} car le but contient un sous-terme de la forme \texttt{?n + 0} (où \texttt{?n} est \texttt{n}). On peut également utiliser \texttt{apply add\_0\_r.} car le but est convertible à \texttt{?n + 0 = ?n} (car la partie droite de l'égalité se simplifie en \texttt{n}).
+
+  \textbf{(2)} On peut utiliser \texttt{rewrite -> add\_0\_r.} car le but contient un sous-terme de la forme \texttt{?n + 0} (où \texttt{?n} est \texttt{n + m}). On ne peut pas utiliser \texttt{apply add\_0\_r.} car le but n'est pas convertible à \texttt{?n + 0 = ?n} (sauf à réécrire au préalable le but avec la commutativité de l'addition).
+
+  \textbf{(3)} On peut utiliser \texttt{rewrite -> add\_0\_r.} car le but contient un sous-terme de la forme \texttt{?n + 0} (où \texttt{?n} est \texttt{m * n}). On peut également utiliser \texttt{apply add\_0\_r.} car le but est de la forme \texttt{?n + 0 = ?n} (où \texttt{?n} est \texttt{m * n}).
+
+  \textbf{(4)} On peut utiliser \texttt{rewrite -> add\_0\_r.} car le but contient un sous-terme de la forme \texttt{?n + 0} (où \texttt{?n} est \texttt{n}). On ne peut pas utiliser \texttt{apply add\_0\_r.} car le but n'est pas convertible à \texttt{?n + 0 = ?n} (sauf à se débarrasser au préalable du \texttt{+ m} grâce à la tactique \texttt{f\_equal}).
+\end{corrige}
+
+%
+%
+%
+
+\exercice
+
+Dans cet exercice, on donne un terme de preuve Coq et on demande de retrouver le théorème du calcul propositionnel intuitionniste qu'il prouve.
+
+\smallskip
+
+\textbf{(1)} \verb|fun H : A => H|
+
+\smallskip
+
+\textbf{(2)} \verb|fun (H1 : A -> B) (H2 : B -> C) (H3 : A) => H2 (H1 H3)|
+
+\smallskip
+
+\textbf{(3)} \verb|fun (H1 : A -> B) (H2 : ~ B) => (fun H3 : A => H2 (H1 H3))|
+
+\begin{corrige}
+  \smallskip
+
+  \textbf{(1)} $A \Rightarrow A$.
+
+  \textbf{(2)} $(A \Rightarrow B) \Rightarrow (B \Rightarrow C) \Rightarrow A \Rightarrow C$.
+
+  \textbf{(3)} $(A \Rightarrow B) \Rightarrow \neg B \Rightarrow \neg A$.
+\end{corrige}
+
+
+%
+%
+%
+
+\exercice
+
+\textbf{(1)} Définir en Coq un type pour représenter les jours de la semaine (7 valeurs possibles).
+
+\smallskip
+
+\textbf{(2)} Définir une fonction qui, étant donné un jour de la semaine, renvoie le jour suivant.
+
+\smallskip
+
+\textbf{(3)} Énoncer un lemme en Coq affirmant que le jour suivant du dimanche est le lundi.
+
+\smallskip
+
+\textbf{(4)} Avec quelle(s) tactique(s) peut-on prouver ce lemme ?
+
+\smallskip
+
+\textbf{(5)} Énoncer un lemme en Coq affirmant que le jour suivant du jour $j$ n'est pas $j$.
+
+\smallskip
+
+\textbf{(6)} Expliquer dans les grandes lignes comment on pourrait prouver ce lemme en Coq (notamment qu'elles seraient les principales tactiques utilisées).
+
+\begin{corrige}
+  \smallskip
+
+  \textbf{(1)} On définit un type inductif à 7 constructeurs :
+
+\begin{verbatim}
+Inductive jour : Type :=
+| lundi : jour
+| mardi : jour
+| mercredi : jour
+| jeudi : jour
+| vendredi : jour
+| samedi : jour
+| dimanche : jour.
+\end{verbatim}
+
+  \textbf{(2)} On définit une fonction (non récursive) par pattern matching :
+
+\begin{verbatim}
+Definition suivant (j : jour) : jour :=
+  match j with
+  | lundi => mardi
+  | mardi => mercredi
+  | mercredi => jeudi
+  | jeudi => vendredi
+  | vendredi => samedi
+  | samedi => dimanche
+  | dimanche => lundi
+  end.
+\end{verbatim}
+
+  \textbf{(3)} \verb|Lemma suivant_dimanche_lundi : suivant dimanche = lundi.|
+
+  \textbf{(4)} \verb|simpl.| (optionnel) suivi de \verb|reflexivity.|
+
+  \textbf{(5)} \verb|Lemma suivant_est_different : forall j : jour, suivant j <> j.| ou \verb|forall j : jour, ~ suivant j = j| (équivalents étant donné que \verb|<>| n'est qu'une notation en Coq).
+
+  \textbf{(6)} On peut prouver ce lemme par analyse de cas sur \texttt{j} (tactique \texttt{destruct j.}). Après un appel optionnel à \texttt{simpl.} ou \texttt{simpl in *.} pour calculer la valeur de \texttt{suivant j} dans chaque cas, on peut conclure par \texttt{discriminate.} pour montrer que les deux termes sont différents.
+
+  Preuve complète :
+
+\begin{verbatim}
+Lemma suivant_est_different : forall j : jour, suivant j <> j.
+Proof.
+  intros j H.
+  destruct j; simpl in *; discriminate.
+Qed.
+\end{verbatim}
+\vskip-4ex\leavevmode
+\end{corrige}
+
+
+%
+%
+%
+
+%% \bigbreak
+%% \hbox to\hsize{\hrulefill}
+%% \smallskip
+
+\pagebreak
 
 \exercice[Problème]