Finish proofreading exam questions.

1 files changed, 59 insertions, 52 deletions

diff --git a/controle-20260126.tex b/controle-20260126.tex
index 7ef04e2..7703669 100644
--- a/controle-20260126.tex
+++ b/controle-20260126.tex
@@ -74,31 +74,29 @@
 
 \noindent\textbf{Consignes.}
 
-\textcolor{red}{(À modifier.)}
-
-Les exercices et le problème sont totalement indépendants les uns des
-autres.  Ils pourront être traités dans un ordre quelconque, mais on
-demande de faire apparaître de façon très visible dans les copies où
-commence chaque exercice (tirez au moins un trait sur toute la largeur
-de la feuille entre deux exercices).
-
-Les questions du problème dépendent les unes des autres, mais ont été
-rédigées de manière à ce que chacune donne toutes les informations
-nécessaires pour passer à la suite.  Mais comme elles (les questions
-du problème) présentent une gradation approximative de difficulté, il
-est recommandé de les traiter dans l'ordre.
-
-La longueur du sujet ne doit pas effrayer : l'énoncé du problème est
-très long parce que des rappels et éclaircissements ont été faits et
-que les questions ont été rédigées de façon aussi précise que
-possible.  Par ailleurs, il ne sera pas nécessaire de tout traiter
-pour avoir le maximum des points.
+Les exercices 1 à 5 (qui portent sur la logique) et le problème final
+(qui porte sur la calculabilité) sont totalement indépendants les uns
+des autres.  Ils pourront être traités dans un ordre quelconque, mais
+on demande de faire apparaître de façon très visible dans les copies
+où commence chaque exercice (tirez au moins un trait sur toute la
+largeur de la feuille entre deux exercices).  \textbf{Le non-respect
+  de cette consigne pourra être pénalisé.}
 
 \medbreak
 
-Dans les exercices portant sur Coq (exercices 1 à 4), les erreurs de
-syntaxe Coq ne seront pas pénalisées tant qu'on comprend clairement
-l'intention.
+La longueur du sujet ne doit pas effrayer : les réponses attendues
+sont souvent plus courtes que les questions.  Notamment, l'énoncé du
+problème est long parce que des rappels et éclaircissements ont été
+faits et que les questions ont été rédigées de façon aussi précise que
+possible.
+
+\medbreak
+
+Dans les exercices portant sur Rocq (exercices 1 à 4), les erreurs de
+syntaxe Rocq ne seront pas pénalisées tant qu'on comprend clairement
+l'intention.  De même, quand on demande d'écrire un $\lambda$-terme,
+il n'est pas indispensable de suivre exactement les notations
+introduites en cours.
 
 \medbreak
 
@@ -112,12 +110,12 @@ L'usage des appareils électroniques est interdit.
 Durée : 3h
 
 Barème \emph{approximatif} et \emph{indicatif} (sur $20$) :
-\textcolor{red}{(à écrire)}.
+2+2+4+3+3+6
 
 \ifcorrige
-Ce corrigé comporte \textcolor{red}{(à remplir)} pages (page de garde incluse).
+Ce corrigé comporte 11 pages (page de garde incluse).
 \else
-Cet énoncé comporte \textcolor{red}{(à remplir)} pages (page de garde incluse).
+Cet énoncé comporte 7 pages (page de garde incluse).
 \fi
 
 \vfill
@@ -153,9 +151,10 @@ Dans cet exercice, on considère des paires d'états d'une preuve en Rocq avant
   A
 \end{verbatim}
 
-et on veut arriver à l'état suivant :
+\noindent et on veut arriver à l'état suivant :
 
 \begin{verbatim}  
+  A, B, C : Prop
   H1 : A /\ B
   H2 : C
   ============================
@@ -172,7 +171,7 @@ et on veut arriver à l'état suivant :
   (A \/ B) /\ C <-> (A /\ C) \/ (A /\ C)
 \end{verbatim}
 
-et on veut arriver à l'état suivant :
+\noindent et on veut arriver à l'état suivant :
 
 \begin{verbatim}
 First subgoal:
@@ -200,7 +199,7 @@ Second subgoal:
   A \/ B
 \end{verbatim}
 
-et on veut arriver à l'état suivant :
+\noindent et on veut arriver à l'état suivant :
 
 \begin{verbatim}
   No more goals.
@@ -211,15 +210,17 @@ et on veut arriver à l'état suivant :
 \textbf{(4)} On part de l'état suivant :
 
 \begin{verbatim}
+  A, B : Prop
   H1 : A -> B
   H2 : ~ B
   ============================
   ~A
 \end{verbatim}
 
-et on veut arriver à l'état suivant :
+\noindent et on veut arriver à l'état suivant :
 
 \begin{verbatim}
+  A, B : Prop
   H1 : A -> B
   H2 : ~ B
   H3 : A
@@ -238,7 +239,7 @@ et on veut arriver à l'état suivant :
   n = m
 \end{verbatim}
 
-et on veut arriver à l'état suivant :
+\noindent et on veut arriver à l'état suivant :
 
 \begin{verbatim}
   n, m : nat
@@ -257,7 +258,7 @@ et on veut arriver à l'état suivant :
   n + 0 = n
 \end{verbatim}
 
-et on veut arriver à l'état suivant :
+\noindent et on veut arriver à l'état suivant :
 
 \begin{verbatim}
 First subgoal:
@@ -284,7 +285,7 @@ Second subgoal:
   S n + 0 = S n
 \end{verbatim}
 
-et on veut arriver à l'état suivant :
+\noindent et on veut arriver à l'état suivant :
 
 \begin{verbatim}
   n : nat
@@ -304,7 +305,7 @@ et on veut arriver à l'état suivant :
   S (n + 0) = S n
 \end{verbatim}
 
-et on veut arriver à l'état suivant :
+\noindent et on veut arriver à l'état suivant :
 
 \begin{verbatim}
   n : nat
@@ -334,7 +335,6 @@ et on veut arriver à l'état suivant :
   \textbf{(7)} \verb|simpl.|
 
   \textbf{(8)} \verb|f_equal.| (la tactique) ou \verb|apply f_equal.| (le lemme).
-
 \end{corrige}
 
 %
@@ -516,7 +516,7 @@ forme drapeau), qui vaudra au moins une partie des points.
 
 \smallskip
 
-\textbf{(6)} Expliquer comment prouver en Rocq que la taille d'un arbre et la taille de son miroir sont égales.
+\textbf{(6)} Expliquer succinctement comment prouver en Rocq que la taille d'un arbre et la taille de son miroir sont égales.
 
 \begin{corrige}
   \smallskip
@@ -553,7 +553,9 @@ Fixpoint taille (a : arbre) : nat :=
   end.
 \end{verbatim}
 
-  \textbf{(6)} On énoncerait le lemme \verb|Lemma taille_miroir : forall a : arbre, taille a = taille (miroir a).|
+  \textbf{(6)} On énoncerait le lemme :
+
+\verb|Lemma taille_miroir : forall a : arbre, taille a = taille (miroir a).|
   
   Pour le prouver, on utilise l'induction structurelle (\texttt{induction a.}). Le cas de base (feuille) se résout par \texttt{reflexivity.} Dans le cas récursif, la simplification calcule la taille du miroir. Les hypothèses d'induction permettent de réécrire les tailles du miroir des sous-arbres. On conclut en utilisant la commutativité de l'addition.
 
@@ -662,10 +664,10 @@ peut pas être démontrable en calcul propositionnel intuitionniste.
 %
 %
 
-\exercice
+\exercice[Problème]
 
-\textbf{Rappels de quelques définitions habituelles.}  On rappelle
-qu'un \textbf{mot binaire [fini]} est une suite finie (éventuellement
+\textbf{Rappels de quelques définitions et notations habituelles.}  On rappelle
+qu'un \textbf{mot binaire} est une suite finie (éventuellement
 vide, c'est-à-dire de longueur nulle) de $0$ et de $1$.  On notera
 $\{0,1\}^* = \{\varepsilon, 0, 1, 00, 01, 10, 11, 000, \ldots\}$ (ici,
 $\varepsilon$ désigne le mot vide) l'ensemble de tous les mots
@@ -701,21 +703,24 @@ lorsque, pour chaque $0 \leq i < |w|$, le bit numéroté $i$ de $w$ vaut
   attestant $\varphi_i(0) = 0$,
 \item $1$ s'il existe un arbre de calcul (codé par un entier) $<|w|$
   attestant $\varphi_i(0) = r$, où $r\neq 0$,
-\item et arbitraire sinon
+\item et arbitraire sinon,
 \end{itemize}
-où $\varphi_i$ désigne la $i$-ième fonction générale récursive.
+où $\varphi_i$ désigne la $i$-ième fonction générale récursive
+(d'arité $1$).
+
 \emph{Si on préfère} parler en termes de machines de Turing, on pourra
 changer la définition en :
 \begin{itemize}
 \item $0$ si la $i$-ième machine de Turing
   termine\footnote{Sous-entendu : à partir d'une bande vierge (ou
   d'une bande représentant le nombre $0$, ou tout autre état initial
-  fixé, peu importe).} en $<|w|$ étapes et renvoie $0$,
+  fixé sans importance).} en $<|w|$ étapes et renvoie $0$,
 \item $1$ si la $i$-ième machine de Turing termine en $<|w|$
   étapes et renvoie une valeur $r \neq 0$,
 \item et arbitraire sinon
 \end{itemize}
 (cela ne changera rien de substantiel aux raisonnements).
+
 Informellement dit, l'appartenance d'un mot $w$ à $\mathscr{K}$ est
 déterminée par le résultat de l'exécution des $|w|$ premiers
 programmes, chacun jusqu'à la borne $|w|$, et le bit numéroté $i$
@@ -751,14 +756,15 @@ les sommets sont les éléments de $\mathscr{K}$, avec une arête de $u$
 à $v$ lorsque $u$ est un préfixe de $v$, est un arbre (infini) au sens
 de la théorie des graphes.  Cette remarque n'est pas utile pour le
 présent exercice.}  pour exprimer la propriété démontrée par cette
-question (1) (formellement, un arbre de mots binaires est une partie
+question (1). (Formellement, un arbre de mots binaires est une partie
 $\mathscr{T} \subseteq \{0,1\}^*$ telle que si $v\in\mathscr{T}$ et
-que $u$ est un préfixe de $v$, alors $u\in\mathscr{T}$).
+que $u$ est un préfixe de $v$, alors $u\in\mathscr{T}$.)
 
 \medskip
 
 \textbf{(2)} Montrer que $\mathscr{K}$ est une partie \emph{décidable}
-(i.e., calculable) de $\{0,1\}^*$.
+(i.e., calculable) de $\{0,1\}^*$.  Sa fonction indicatrice est-elle
+primitive récursive ?
 
 \begin{corrige}
 On veut montrer qu'il existe un algorithme qui, donné un $w \in
@@ -773,9 +779,9 @@ lance l'exécution de la $i$-ième machine pour au plus $|w|-1$ étapes
 et le reste est analogue.)  Si une des conditions échoue, le mot $w$
 n'est pas dans $\mathscr{K}$, tandis que si toutes réussissent, le mot
 est dans $\mathscr{K}$.  Il s'agit bien là d'un algorithme qui termine
-à coup sûr en temps fini (il est même primitif récursif puisqu'on a
+à coup sûr en temps fini.  Il est même primitif récursif puisqu'on a
 essentiellement deux boucles imbriquées, une sur $i$ et une sur $j$,
-bornées par $|w|$).
+bornées par $|w|$.
 \end{corrige}
 
 \medskip
@@ -822,6 +828,7 @@ qu'il n'existe pas d'algorithme qui prend en entrée un $e \in
 \item et une valeur arbitraire sinon (i.e., si $\varphi_e(0)$ n'est
   pas définie).
 \end{itemize}
+
 \emph{Si on préfère} parler en termes de machines de Turing, on pourra
 montrer qu'il n'existe pas d'algorithme qui prend en entrée le code
 $e$ d'une machine de Turing, \emph{termine toujours en temps fini}, et
@@ -896,11 +903,11 @@ n'a pas branche infinie calculable.
 
 Le \textbf{lemme de Kőnig} est l'affirmation suivante : « tout arbre
 de mots binaires contenant des mots de longueur arbitrairement grande
-a une branche infinie » (les termes « arbre », « contenant des mots de
-longueur arbitrairement grande » et « branche infinie » ont été
-définis précisément ci-dessus).  On ne demande pas de démontrer cette
-affirmation : néanmoins, c'est un théorème des mathématiques
-classiques usuelles.
+a une branche infinie » (les termes « arbre de mots binaires »,
+« contenant des mots de longueur arbitrairement grande » et « branche
+infinie » ont été définis précisément ci-dessus).  On ne demande pas
+de démontrer cette affirmation : néanmoins, c'est un théorème des
+mathématiques classiques usuelles.
 
 \medskip