From f1e914a978ecd196768098acd101dabd5ab30b82 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Mon, 22 Jan 2024 19:08:16 +0100
Subject: A simple exercise about Coq.

---
 controle-20240126.tex | 62 +++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 62 insertions(+)

diff --git a/controle-20240126.tex b/controle-20240126.tex
index 42af5da..b55a66c 100644
--- a/controle-20240126.tex
+++ b/controle-20240126.tex
@@ -107,6 +107,68 @@ Git: \input{vcline.tex}
 \pagebreak
 
 
+%
+%
+%
+
+\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}
+
+
 %
 %
 %
-- 
cgit v1.2.3