From 4b8d70e5cbf2a3c2d381c05a946d30297364ba93 Mon Sep 17 00:00:00 2001 From: "David A. Madore" Date: Tue, 20 Jan 2026 12:26:17 +0100 Subject: Start writing 2026 test with questions provided by TZ. --- controle-20260126.tex | 545 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 545 insertions(+) create mode 100644 controle-20260126.tex (limited to 'controle-20260126.tex') diff --git a/controle-20260126.tex b/controle-20260126.tex new file mode 100644 index 0000000..1b22f2a --- /dev/null +++ b/controle-20260126.tex @@ -0,0 +1,545 @@ +%% 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 + + +% +% +% + +\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} + + + +% +% +% +\end{document} -- cgit v1.2.3