path: root/controle-20260126.tex

%% This is a LaTeX document.  Hey, Emacs, -*- latex -*- , get it?
\documentclass[12pt,a4paper]{article}
\usepackage[a4paper,hmargin=2cm,vmargin=3cm]{geometry}
\usepackage[french]{babel}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
%\usepackage{ucs}
\usepackage{lmodern}
\usepackage{newtxtext}
% A tribute to the worthy AMS:
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
%
\usepackage{mathrsfs}
\usepackage{wasysym}
\usepackage{url}
\usepackage{mathpartir}
\usepackage{flagderiv}
%
\usepackage{graphics}
\usepackage[usenames,dvipsnames]{xcolor}
\usepackage{tikz}
\usetikzlibrary{arrows}
\usepackage{hyperref}
%
\theoremstyle{definition}
\newtheorem{comcnt}{Tout}
\newcommand\thingy{%
\refstepcounter{comcnt}\medskip\noindent\textbf{\thecomcnt.} }
\newcommand\exercice[1][Exercice]{%
\refstepcounter{comcnt}\bigskip\noindent\textbf{#1~\thecomcnt.}\par\nobreak}
\renewcommand{\qedsymbol}{\smiley}
%
\newcommand{\dbllangle}{\mathopen{\langle\!\langle}}
\newcommand{\dblrangle}{\mathclose{\rangle\!\rangle}}
\newcommand{\dottedlimp}{\mathbin{\dot\Rightarrow}}
\newcommand{\dottedland}{\mathbin{\dot\land}}
\newcommand{\dottedlor}{\mathbin{\dot\lor}}
\newcommand{\dottedtop}{\mathord{\dot\top}}
\newcommand{\dottedbot}{\mathord{\dot\bot}}
\newcommand{\dottedneg}{\mathop{\dot\neg}}
\mathchardef\emdash="07C\relax
%
\DeclareUnicodeCharacter{00A0}{~}
%
%
\newcommand{\spaceout}{\hskip1emplus2emminus.5em}
\newif\ifcorrige
\corrigetrue
\newenvironment{corrige}%
{\ifcorrige\relax\else\setbox0=\vbox\bgroup\fi%
\smallbreak\noindent{\underbar{\textit{Corrigé.}}\quad}}
{{\hbox{}\nobreak\hfill\checkmark}%
\ifcorrige\par\smallbreak\else\egroup\par\fi}
%
%
%
\begin{document}
\ifcorrige
\title{INF110 / CSC-3TC34-TP\\Contrôle de connaissances — Corrigé\\{\normalsize Logique et Fondements de l'Informatique}}
\else
\title{INF110 / CSC-3TC34-TP\\Contrôle de connaissances\\{\normalsize Logique et Fondements de l'Informatique}}
\fi
\author{}
\date{26 janvier 2026}
\maketitle

\pretolerance=8000
\tolerance=50000

\vskip1truein\relax

\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.

\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.

\medbreak

L'usage de tous les documents écrits (notes de cours manuscrites ou
imprimées, feuilles d'exercices, livres) est autorisé.

L'usage des appareils électroniques est interdit.

\medbreak

Durée : 3h

Barème \emph{approximatif} et \emph{indicatif} (sur $20$) :
\textcolor{red}{(à écrire)}.

\ifcorrige
Ce corrigé comporte \textcolor{red}{(à remplir)} pages (page de garde incluse).
\else
Cet énoncé comporte \textcolor{red}{(à remplir)} pages (page de garde incluse).
\fi

\vfill

{\tiny\noindent
\immediate\write18{sh ./vc > vcline.tex}
Git: \input{vcline.tex}
\immediate\write18{echo ' (stale)' >> vcline.tex}
\par}

\pagebreak

\iftrue


%
%
%

\exercice

Dans cet exercice, on considère des paires d'états d'une preuve en Rocq 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
  H : (A /\ B) /\ C
  ============================
  A
\end{verbatim}

et on veut arriver à l'état suivant :

\begin{verbatim}  
  H1 : A /\ B
  H2 : C
  ============================
  A
\end{verbatim}

\smallskip

\textbf{(2)} On part de l'état suivant :

\begin{verbatim}
  A, B, C : Prop
  ============================
  (A \/ B) /\ C <-> (A /\ C) \/ (A /\ C)
\end{verbatim}

et on veut arriver à l'état suivant :

\begin{verbatim}
First subgoal:
  
  A, B, C : Prop
  ============================
  (A \/ B) /\ C -> (A /\ C) \/ (A /\ C)

Second subgoal:

  A, B, C : Prop
  ============================
  (A /\ C) \/ (A /\ C) -> (A \/ B) /\ C
\end{verbatim}

\smallskip

\textbf{(3)} On part de l'état suivant :

\begin{verbatim}
  A, B, C : Prop
  H1 : B
  H2 : C
  ============================
  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}
  H1 : A -> B
  H2 : ~ B
  ============================
  ~A
\end{verbatim}

et on veut arriver à l'état suivant :

\begin{verbatim}
  H1 : A -> B
  H2 : ~ B
  H3 : A
  ============================
  B
\end{verbatim}

\smallskip

\textbf{(5)} On part de l'état suivant :

\begin{verbatim}
  n, m : nat
  H : S n = S m
  ============================
  n = m
\end{verbatim}

et on veut arriver à l'état suivant :

\begin{verbatim}
  n, m : nat
  H : n = m
  ============================
  n = m
\end{verbatim}

\smallskip

\textbf{(6)} On part de l'état suivant :

\begin{verbatim}
  n : nat
  ============================
  n + 0 = n
\end{verbatim}

et on veut arriver à l'état suivant :

\begin{verbatim}
First subgoal:
  
  ============================
  0 + 0 = 0

Second subgoal:

  n : nat
  IHn : n + 0 = n
  ============================
  S n + 0 = S n
\end{verbatim}

\smallskip

\textbf{(7)} On part de l'état suivant :

\begin{verbatim}
  n : nat
  IHn : n + 0 = n
  ============================
  S n + 0 = S n
\end{verbatim}

et on veut arriver à l'état suivant :

\begin{verbatim}
  n : nat
  IHn : n + 0 = n
  ============================
  S (n + 0) = S n
\end{verbatim}

\smallskip

\textbf{(8)} On part de l'état suivant :

\begin{verbatim}
  n : nat
  IHn : n + 0 = n
  ============================
  S (n + 0) = S n
\end{verbatim}

et on veut arriver à l'état suivant :

\begin{verbatim}
  n : nat
  IHn : n + 0 = n
  ============================
  n + 0 = n
\end{verbatim}

\begin{corrige}
  \smallskip

  \textbf{(1)} \verb|destruct H as (H1, H2).|


  \textbf{(2)} \verb|split.|


  \textbf{(3)} \verb|right. assumption.|


  \textbf{(4)} \verb|intros H3. apply H2.|

  \textbf{(5)} \verb|injection H as H.|

  \textbf{(6)} \verb+induction n as [|n IHn].+ ou simplement \verb|induction n.|

  \textbf{(7)} \verb|simpl.|

  \textbf{(8)} \verb|f_equal.| (la tactique) ou \verb|apply f_equal.| (le lemme).

\end{corrige}

%
%
%

\exercice

Si l'on dispose du lemme suivant en Rocq :

\begin{verbatim}
  Lemma mul_0_r : forall n : nat, n * 0 = 0.
\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 + 0
\end{verbatim}

\smallskip

\textbf{(2)}

\begin{verbatim}
  n, m : nat
  ============================
  (n + m) * 0 = n * 0 + m * 0
\end{verbatim}

\smallskip

\textbf{(3)}

\begin{verbatim}
  n, m : nat
  ============================
  n + 0 = n
\end{verbatim}

\begin{corrige}
  \smallskip

  \textbf{(1)} On peut utiliser \texttt{rewrite -> mul\_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 mul\_0\_r.} car le but est convertible à \texttt{?n * 0 = 0} (car la partie droite de l'égalité se simplifie en \texttt{0}).

  \textbf{(2)} On peut utiliser \texttt{rewrite -> mul\_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 mul\_0\_r.} car le but n'est pas convertible à \texttt{?n * 0 = 0}.

  \textbf{(3)} On peut utiliser \texttt{rewrite <- mul\_0\_r.} car le but contient un sous-terme de la forme \texttt{0}. On ne peut pas utiliser \texttt{apply add\_0\_r.} car le but n'est pas convertible à \texttt{?n * 0 = 0}.
\end{corrige}

%
%
%

\exercice

\textbf{(A)} Pour chacun des termes de preuve Rocq suivants, retrouver le théorème du calcul propositionnel intuitionniste qu'il prouve.

\smallskip

\textbf{(1)} \verb|fun (H1 : A) (H2 : B) => H2|

\smallskip

\textbf{(2)} \verb|fun (H1 : A) (H2 : ~ A) => H2 H1|

\smallskip

\textbf{(3)} \verb|fun (H1 : A -> (B -> C)) (H2 : A) (H3 : B) => H1 H2 H3|

\smallskip

\textbf{(B)} Pour chaque formule logique suivante, en donner une démonstration en déduction naturelle (on donnera l'arbre de preuve ou la présentation
en style drapeau, comme on préfère).

\smallskip

\textbf{(1)} $A \Rightarrow A$.

\smallskip

\textbf{(2)} $(A \wedge B) \Rightarrow (B \wedge A)$.

\smallskip

\textbf{(3)} $(A \vee B) \Rightarrow (B \vee A)$.

\smallskip

\textbf{(4)} $\neg(A \vee B) \Rightarrow \neg A$.

\smallskip

\textbf{(5)} $(\forall x,\; P(x)) \vee (\forall x,\; Q(x)) \Rightarrow (\forall x,\; P(x) \vee Q(x))$.

\smallskip



\begin{corrige}

\smallskip

\textbf{(A)}

  \textbf{(1)} $A \Rightarrow B \Rightarrow B$.

  \textbf{(2)} $A \Rightarrow \neg \neg A$.

  \textbf{(3)} $(A \Rightarrow (B \Rightarrow C)) \Rightarrow A \Rightarrow B \Rightarrow C$.

\end{corrige}


%
%
%

\exercice

\textbf{(1)} Définir en Rocq un type inductif pour représenter les arbres binaires contenant des entiers.

\smallskip

\textbf{(2)} Définir une fonction \texttt{miroir} qui, étant donné un arbre binaire, renvoie son miroir (symétrie gauche-droite).

\smallskip

\textbf{(3)} Énoncer un lemme en Rocq affirmant que le miroir du miroir d'un arbre est l'arbre lui-même.

\smallskip

\textbf{(4)} Avec quelle(s) tactique(s) peut-on prouver ce lemme ? Expliquer brièvement.

\smallskip

\textbf{(5)} Définir une fonction \texttt{taille} qui calcule le nombre de noeuds d'un arbre binaire.

\smallskip

\textbf{(6)} Expliquer comment prouver en Rocq que la taille d'un arbre et la taille de son miroir sont égales.

\begin{corrige}
  \smallskip

  \textbf{(1)} On définit un type inductif pour les arbres binaires :

\begin{verbatim}
Inductive arbre : Type :=
| feuille : arbre
| noeud : nat -> arbre -> arbre -> arbre.
\end{verbatim}

  \textbf{(2)} On définit la fonction \texttt{miroir} par récursion structurelle :

\begin{verbatim}
Fixpoint miroir (a : arbre) : arbre :=
  match a with
  | feuille => feuille
  | noeud v g d => noeud v (miroir d) (miroir g)
  end.
\end{verbatim}

  \textbf{(3)} \verb|Lemma miroir_involutif : forall a : arbre, miroir (miroir a) = a.|

  \textbf{(4)} On peut prouver ce lemme par induction structurelle sur \texttt{a} (tactique \texttt{induction a.}). Après la simplification par \texttt{simpl.}, chaque cas se résout facilement avec \texttt{reflexivity.} ou les hypothèses d'induction.

  \textbf{(5)} On définit la fonction \texttt{taille} par récursion :

\begin{verbatim}
Fixpoint taille (a : arbre) : nat :=
  match a with
  | feuille => 0
  | noeud v g d => (taille g) + (taille d)
  end.
\end{verbatim}

  \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.

  Preuve complète :

\begin{verbatim}
Require Import Arith.

Lemma taille_miroir : forall a : arbre, taille a = taille (miroir a).
Proof.
  induction a; simpl.
  - reflexivity.
  - rewrite IHa1.
    rewrite IHa2.
    apply Nat.add_comm.
Qed.
\end{verbatim}
\vskip-4ex\leavevmode
\end{corrige}


\fi


%
%
%

\exercice

\textbf{Rappels de quelques définitions habituelles.}  On rappelle
qu'un \textbf{mot binaire [fini]} 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
binaires.  La \textbf{longueur} $|w|$ d'un mot binaire $w \in
\{0,1\}^*$ est le nombre total de bits qu'il contient (p.ex., $|00|=2$
et $|\varepsilon|=0$), et nous suivrons la convention de numéroter les
bits de la gauche vers la droite de $0$ à $|w|-1$ (par exemple, le bit
numéroté $0$ de $1010$ vaut $1$, tandis que son bit numéroté $3$
vaut $0$).  On dit qu'un mot binaire $u$ est un \textbf{préfixe} d'un
mot binaire $v$ lorsque $v$ commence par les bits de $u$, ou,
formellement : $|u|\leq|v|$ et pour chaque $0\leq j < |u|$, le bit
numéroté $j$ de $v$ est égal au bit numéroté $j$ de $u$.  (Par
exemple, $1010$ est un préfixe de $1010111$, tout mot binaire est un
préfixe de lui-même, et $\varepsilon$ est un préfixe de n'importe quel
mot binaire.)

\medskip

On pourra utiliser sans justification et sans commentaire le fait que
les mots binaires peuvent être manipulés algorithmiquement (via un
codage de Gödel qu'on ne demande pas de préciser) : notamment,
calculer la longueur d'un mot, ou renvoyer son bit numéroté $i$, sont
des opération calculables.

\medskip

On appelle \textbf{arbre de Kleene} l'ensemble $\mathscr{K} \subseteq
\{0,1\}^*$ de mots binaires défini de la manière suivante : un mot
binaire $w \in \{0,1\}^*$ de longueur $|w|$ appartient à $\mathscr{K}$
lorsque, pour chaque $0 \leq i < |w|$, le bit numéroté $i$ de $w$ vaut
\begin{itemize}
\item $0$ s'il existe un arbre de calcul (codé par un entier) $<|w|$
  attestant $\varphi_i(0) = 0$,
\item $1$ s'il existe un arbre de calcul (codé par un entier) $<|w|$
  attestant $\varphi_i(0) = v$, où $v\neq 0$,
\item et arbitraire sinon
\end{itemize}
où $\varphi_i$ désigne la $i$-ième fonction générale récursive.
\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$,
\item $1$ si la $i$-ième machine de Turing termine en $<|w|$
  étapes et renvoie une valeur $v \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$
de $w$ est contraint, si le programme $i$ termine, par le résultat de
celui-ci.

(On prendra note du fait que $\varepsilon \in \mathscr{K}$ car la
contrainte « pour chaque $0\leq i < |w|$ » est vide — donc
trivialement vérifiée — vu que $|\varepsilon|=0$.)

\bigskip

\textbf{(1)} Montrer que si $v \in \mathscr{K}$ et si $u$ est un
préfixe de $v$. alors on a aussi $u \in \mathscr{K}$.

\medskip

On dit que $\mathscr{K}$ est un \textbf{arbre} de mots
binaires\footnote{Si cette terminologie semble mystérieuse,
l'explication est que le graphe (infini d'après la question (3)) dont
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).

\medskip

\textbf{(2)} Montrer que $\mathscr{K}$ est une partie \emph{décidable}
(i.e., calculable) de $\{0,1\}^*$.

\medskip

\textbf{(3)} Montrer qu'il existe dans $\mathscr{K}$ des mots binaires
de longueur arbitrairement grande (formellement : $\forall n. \;
\exists w\in\mathscr{K}. \; (|w| \geq n)$).  On pourra même expliquer
comment en calculer algorithmiquement.

\medskip

On appelle \textbf{branche infinie} de $\mathscr{K}$ une suite infinie
$(b_i)_{i\in\mathbb{N}}$ de bits (i.e., un élément de
$\{0,1\}^{\mathbb{N}}$) dont tous les préfixes appartiennent
à $\mathscr{K}$, c'est-à-dire : $b_0\cdots b_{\ell-1} \in \mathscr{K}$
pour tout $\ell \in \mathbb{N}$.

\medskip

\textbf{(4)} \emph{Indépendamment de tout ce qui précède,} montrer
qu'il n'existe pas d'algorithme qui prend en entrée un $e \in
\mathbb{N}$, \emph{termine toujours en temps fini}, et renvoie
\begin{itemize}
\item $0$ si $\varphi_e(0) = 0$,
\item $1$ si $\varphi_e(0) = v$ où $v \neq 0$,
\item et une valeur arbitraire sinon.
\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
renvoie
\begin{itemize}
\item $0$ si la $e$-ième machine de Turing termine et qu'elle
  renvoie $0$,
\item $1$ si la $e$-ième machine de Turing termine et qu'elle renvoie
  une valeur $v \neq 0$,
\item et une valeur arbitraire sinon.
\end{itemize}

\emph{Indication :} utiliser l'astuce de Quine pour construire un
programme qui fait le contraire de ce qu'on lui prédit.

\emph{Attention !} On demande dans cette question une démonstration
précise : on ne se contentera pas d'un raisonnement informel du type
« on ne peut pas savoir si $\varphi_e(0)$ terminera un jour, donc on
ne peut pas calculer sa valeur ».

\medskip

\textbf{(5)} Déduire de (4) qu'il n'existe aucune branche infinie
calculable de $\mathscr{K}$.

\medskip

Le \textbf{lemme de Kőnig} est l'affirmation suivante : « tout arbre
de mots binaires contenant des mots binaires de longueur
arbitrairement grande a une branche infinie » (les termes « arbre »,
« contenant des mots binaires 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

\textbf{(6)} Que peut-on conclure du lemme de Kőnig concernant
l'arbre $\mathscr{K}$ ?

\medskip

\textbf{(7)} Expliquer pourquoi la question (5) \emph{suggère} que le
lemme de Kőnig n'est pas démontrable en mathématiques constructives.
(On ne demande pas ici un raisonnement formel précis, mais une idée.)



%
%
%
\end{document}