A simple exercise about Coq.

1 files changed, 62 insertions, 0 deletions

diff --git a/controle-20240126.tex b/controle-20240126.tex
index 42af5da..b55a66c 100644
--- a/controle-20240126.tex
+++ b/controle-20240126.tex
@@ -113,6 +113,68 @@ Git: \input{vcline.tex}
 
 \exercice
 
+On considère un extrait d'une démonstration interactive en Coq du
+théorème \texttt{forall (A:Prop) (B:Prop) (C:Prop),
+  (A->B)->(B->C)->(A->C)} où on a recopié ci-dessous seulement la
+sortie de Coq.  On demande de retrouver les deux commandes qui ont été
+utilisées, et de proposer l'étape suivante.
+
+\smallskip
+
+{\tt\par\noindent
+1 subgoal\\
+\ \ \\
+\ \ A, B, C : Prop\\
+\ \ ============================\\
+\ \ (A -> B) -> (B -> C) -> A -> C\\
+\\
+thm < \textrm{(commande à trouver)}\\
+1 subgoal\\
+\ \ \\
+\ \ A, B, C : Prop\\
+\ \ x : A -> B\\
+\ \ y : B -> C\\
+\ \ z : A\\
+\ \ ============================\\
+\ \ C\\
+\\
+thm < \textrm{(commande à trouver)}\\
+1 subgoal\\
+\ \ \\
+\ \ A, B, C : Prop\\
+\ \ x : A -> B\\
+\ \ y : B -> C\\
+\ \ z : A\\
+\ \ ============================\\
+\ \ B\\
+\\
+thm < \textrm{(commande à trouver)}
+}
+
+\smallskip
+
+(À défaut de connaître le nom précis de la tactique, on pourra
+expliquer ce qu'elle fait de façon générale, ou à quelle règle de
+logique elle correspond.)
+
+\begin{corrige}
+La première commande était \texttt{intros x y z.} et correspond à la
+règle d'introduction du $\Rightarrow$ appliquée trois fois.  La
+commande suivante était \texttt{apply y.} et correspond à la règle
+d'élimination du $\Rightarrow$ entre l'hypothèse (\texttt{y}) qu'on
+lui indique et la démonstration qu'onva produire du nouveau but.  Une
+commande naturelle ensuite serait \texttt{apply x.} (qui ramènerait le
+but à \texttt{A}, et qui pourrait être suivie de \texttt{exact z.}
+pour terminer la démonstration).
+\end{corrige}
+
+
+%
+%
+%
+
+\exercice
+
 (Dans cet exercice, on ne demande pas de justifier les réponses.)
 
 \textbf{(1)} En calcul propositionnel intuitionniste, quelle est la