diff options
| -rw-r--r-- | controle-20240126.tex | 62 |
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 |