(** *** Projet Coq 2014 - L3 S1 - Lucca Hirschi *) (** Vous pouvez lire ce document dans sa version HTML mais l'idéal est de le compiler au fur et à mesure pour lire les messages renvoyés par Coq. Vous avez besoin de Coq et d'un front-end (par exemple CoqIDE par défaut dans Coq ou Proof General pour l'interface avec Emacs). Ce TP vous expliquera les notions essentielles de l'outil Coq. Il contient peu de questions mais beaucoup d'explications. Assurez-vous donc de bien comprendre au fur et à mesure. *) (** Lien vers la page du projet: <> *) (************************) (** * I : Introduction **) (************************) (** ** 1. Généralités **) (***********************) (** Une des contributions de l'informatique à la logique sont les outils construisant des preuves. Il existe deux catégories principales de ces outils: - les prouveurs automatiques tels que les SAT ou SMT solveurs ainsi que les model checkers, etc. Vous en avez donc déja utilisé un lors du premier mini projet; - les assisants de preuves tels que Coq, Abella, PVS ou Agda, etc. Ce sont des outils interactifs construisant des preuves en demandent une intervention humaine mais qui automatisent certaines tâches. Dans ce projet on utilisera Coq (dans la seconde catégorie). En quelques mots, Coq est composé: - d'un "proof-checker" qui vérifie que la preuve construite est bien une suite de règles logiques correctement utilisées. C'est le (petit) noyau dans lequel il faut avoir confiance, - d'un langage fonctionnel permettant de programmer et de formaliser des théories, calculs, etc., - et d'un langage de "tactiques" permettant d'automatiser certaines étapes de preuves. Le noyau de Coq repose sur de solides fondations: le calcul des constructions. *) (** ** 2. Démarrer Coq **) (************************) (** Je vous conseille d'utiliser l'une des deux solutions suivantes: - l'IDE fourni avec COQ. Vous le lancez en tapant 'coqide' dans un terminal ou - le mode Emacs Proof General que vous pouvez trouver ici: 'http://proofgeneral.inf.ed.ac.uk/'. Mais allez au plus simple pour pouvoir continuer à lire le sujet (dans Coq). *) (** ** 3. Les types de Coq **) (****************************) (** Dans le langage de Coq (aka Gallina) vous pouvez écrire des formules, vérifier qu'elles sont correctement formées et les prouver.*) (** En Coq, tous les objets sont des termes du langage et ont donc un type que vous pouvez afficher avec la commande [Check [terme].] (toute commande Coq doit se terminer par un ".").*) Check 3. Check nat. Check Set. Check Type. (** La notation [A:B] indique que le terme [A] a le type [B]. On verra que de façon équivalente, ça signifie également que [A] est une preuve de [B].*) Check 1=2. Check True. Check (forall x:nat, x=0 \/ x>0). Check Prop. (** Bien-sûr, certains termes sont mal formés comme [1+True] par exemple (essayez de compiler puis commentez la ligne suivante): *) Check (1 + True). (** Une bonne façon de s'y retrouver dans tous ces types est d'avoir en tête que: - les termes de type [Prop] correspondent aux propositions logiques (ex. [1=2] ou [True]), - les termes de type [Set] sont des types de données (ex. nat), - les termes de type [T] où [T] est un type de donnée (i.e., [T:Set]) sont des données (ex. 1), - et.... [Type] est tout en haut (on a [Prop:Type] et [Set:Type]). Avec un schéma ça donne (une arrête signifie 'est de type'): << Type / \ Set Prop / | / \ nat bool True ((1=0) \/ False) / | / \ 1 0 true false >> *) (** Dans la suite, on va rapidement voir la syntaxe de ce langage, à savoir comment écrire des fonctions et des propositions et comment les prouver. On commence dans la section suivante (II) avec les définitions de fonctions et de données (on restera dans le monde [Set]). Puis dans la section III sur les preuves, on plongera dans le monde [Prop].*) (******************************) (** * II : Programmer en Coq **) (******************************) (** ** 1. Fonctions, calcul, bool *) (** La commande [Require Import [module]] permet de charger les définitions, lemmes, théorèmes et leurs preuves d'un module. *) Require Import Bool. (** Je peux maintenant chercher toutes les définitons du module. *) Search bool. (** Je peux afficher la définition d'un terme avec [Print].*) Print bool. (** [bool] (qui est lui même de type [Set]) est un type de donnée contenant deux éléments [true] et [false]. On dit aussi que les habitants de [bool] sont [true] et [false]. Quelle est la différence avec [True:Prop]? *) Print ifb. (** On peut donc écrire une fonction avec le mot clé [fun] jouant le rôle d'un lambda: *) Check (fun (b:bool) (n:nat) => if b then n else 0). (** On note la distinction entre la flèche [=>] des fonctions et celle des types: [->]. Si on veut définir un terme ou une fonction (pour l'utiliser par la suite), on utilise le mot clé [Definition]. L'exemple suivant comprend pas mal de points de syntaxe:*) Definition ifb2 (b : bool) (n:nat) := let ntrue := n-1 in let nfalse := n in match b with | true => ntrue | false => nfalse end. (** On peut aussi écrire: *) Definition f := fun b:bool => b. (** qui est équivalent à: *) Definition f2 (b:bool) := b. Print f. Print f2. (** On essaye d'appeler notre fonction: *) Check (ifb2 true 1). (** Et oui, Coq ne réduit pas le terme qu'on lui donne, il vérifie juste son type. Si on veut réduire le terme, alors il faut invoquer [Eval compute in [terme]] et Coq va effectuer le calcul (purement symbolique!).*) Eval compute in (ifb2 true 1). (** En Coq, toute fonction est TOTALE. C'est-à-dire que les fonctions terminent TOUJOURS et renvoient un résultat du bon type. Il n'y a pas d'exceptions, d'erreurs à runtime ou d'Obj.magic.*) (** **** Question 1:*)(** Ecrivez une fonction qui renvoie le XOR de trois booléens et testez-la. *) (** ** 2. Définitions inductives, points fixes et nat **) (*******************************************************) Print nat. (** Les entiers sont représentés comme des entiers de Peano: c'est l'axiomatisation de Peano. Si vous voulez invoquer des propriétés sur les entiers qui ne sont pas des lemmes déjà écrits (dans le module [Arith] par exemple) alors il faut les prouver dans Coq.*) (** On note le mot clé [Inductive] qui permet de définir: - un type de données lui-même de type [Set] (ici c'est [nat]), - ainsi que les habitants de ce type (les termes qui ont ce type). Ici il n'y a que le terme 0 qui est un entier et le terme "S" (successeur) qui a le type [nat -> nat]. C'est l'équivalent d'une définition inductive par fermeture de règles (ou fonctions constructeurs) vue en logique. Dans le cas de [nat], on définit un ensemble inductif [nat] de termes par fermeture des fonctions constucteurs suivantes: << n : nat ----------------- [0] --------------- [Succ] 0 : nat S(n) : nat >> *) Search nat. Print pred. (** Ok, rien de nouveau. Maintenant, comment écrire [plus] ? Pensez-y avant d'avancer. *) Print plus. (** [fix] est un raccourci pour le mot clé [Fixpoint] qui permet de définir des fonctions récursives (un peu comme le "let rec" d'Ocaml).*) Fixpoint mon_mult (n m : nat) : nat := match n with | 0 => 0 | S p => m + mon_mult p m end. (** Notez bien le message renvoyé par Coq après la définition de fonction: [mon_mult is recursively defined (decreasing on 1st argument)]. Coq détecte que l'induction est bien fondée. C'est de cette façon qu'il s'assure que toutes les fonctions terminent. Le critère (syntaxique) de Coq est le suivant: un argument au moins DOIT être structurellement plus petit au moment de l'appel récursif qu'à l'entrée de la fonction. Regardez-les deux exemples suivants.*) Fixpoint fail1 (n m : nat) : nat := match n with | 0 => 0 | S p => m + fail1 (S p) m (* et oui ça boucle ici *) end. Fixpoint fail2 (n m : nat) : nat := match n with | 0 => 0 | S p => m + fail2 (p + 0) m (** et oui c'est plus petit mais pas structurellement plus petit *) end. (** **** Question 2:*)(** Ecrivez une fonction qui prend un entier et qui renvoie [true] s'il est pair et [false] sinon. Exécutez cette fonction sur plusieurs exemples. *) (** **** Question 3:*)(** Ecrivez un type de données [arbre] contenant une représentation de tous les arbres binaires étiquetés par des entiers. *) (** **** Question 4:*)(** Ecrivez une fonction qui renvoie la somme de toutes les étiquettes des noeuds d'un arbre. Testez. *) (** **** Question 5:*)(** Ecrivez une fonction qui prend deux entiers et qui renvoie [true] si le premier est plus petit que le second et [false] sinon. Testez. *) (** **** Question Bonus (bonus pris en compte pour le projet):*) (** Ecrivez une fonction qui calcule le pgcd de deux entiers. Testez. *) (** ** 3. Types polymorphes, listes et types dépendants **) (*********************************************************) Require Import List. Check list. Print list. (** Le type [list] est une fonction qui prend un type [A] et renvoie un type (le type des listes de type [A]).*) Check (list nat). Check 1 :: 2 :: 3 :: nil. (** Mais qu'est-ce que c'est que "::" ? (tout est un terme en Coq).*) Locate "::". (** [Locate] nous informe que "[::]" est juste un mot clé pour le terme [cons] (en notation infix).*) (** Petit coup d'oeil rapide aux fonctions de [list].*) Search list. Check map. Print map. Eval compute in map S (1::2::3::4::nil). Eval compute in map (fun x => x +2) (1::2::3::4::nil). Locate "++". Print app. (** Très bien mais il n'existe pas de fonction pour accéder au n-ieme élément d'une liste, pourquoi? *) (** Jusqu'ici on a vu: - des termes dépendant de termes (par exemple [S : nat -> nat]); - des types dépendant de types (par exemple [list : Type -> Type]). Il existe aussi des types dépendant de termes (aka types dépendants). Voici un exemple de type dépendant: un tableau de taille donnée:*) Inductive array (n : nat) : Type := tab : forall l : list nat, length l = n -> array n. (** [array] est de type [nat -> Type]. Par exemple, [array 10] est le type des tableaux de taille 10. *) Check array. Check (array 10 : Type). (** **** Question Bonus (bonus pris en compte pour le projet):*) (** Ecrire une fonction qui réalise le fold_left polymorphique d'OCaml sur les listes. *) (** **** Question Bonus (bonus pris en compte pour le projet):*) (** Ecrire une fonction de tri. *) (** ** 4. Résumé **) (******************) (** Voici quelques lignes de Coq que vous devez comprendre (ainsi que les messages renvoyés Coq).*) Check true. Check bool. Check Set. Print bool. Fixpoint mon_exp (n m : nat) : nat := match m with | 0 => 1 | S m' => n * mon_exp n m' end. Eval compute in (mon_exp 2 5). Inductive formula : Type := MonTrue : formula | MonFalse : formula | MonEt : formula -> formula -> formula | MonOu : formula -> formula -> formula | MonNon : formula -> formula. Fixpoint eval (F : formula) : bool := match F with | MonTrue => true | MonFalse => false | MonEt F1 F2 => if eval F1 then eval F2 else false | MonOu F1 F2 => if eval F1 then true else eval F2 | MonNon F' => negb (eval F') end. Eval compute in (eval (MonOu (MonEt MonTrue MonFalse) (MonTrue))). (****************************) (** * III : Prouver en Coq **) (****************************) (** Dans la première partie, on va découvrir ce qu'est une preuve en Coq. Ca risque d'être un peu cosmique. Pour bien comprendre, il vaut mieux avoir entendu parler de la correspondence de Curry-Howard (cf. les références données sur ma page et le cours de lambda-calcul). Mais pas de panique, dans la section suivante on va voir comment s'aider des tactiques les plus importantes. Dans la dernière section on verra l'induction.*) (** ** 1. Une preuve en Coq **) (*****************************) (** Le but ici est de comprendre l'objet preuve de Coq. On va prouver quelques lemmes complètement triviaux et ça vous paraîtra compliqué mais le but est de comprendre ce qu'il se passe quand plus tard vous prouverez des théorèmes plus compliqués en utilisant de grosses tactiques.*) (** En fait on a déjà écrit des preuves: [f:A] est une fonction de type A mais en Coq on peut aussi appeler ça une preuve de la formule logique A : c'est la correspondence de Curry-Howard. En résumé, une preuve Coq de la formule [A] c'est un terme de type [A]. *) Check True. (** [True] est un terme de type [Prop] c'est donc aussi une formule. A ne pas confondre avec le booléen [true]. *) (** On va prouver notre premier lemme: *) Lemma tauto1 : True. (** On veut prouver [True], ça va être facile. En déduction naturelle, il existe la règle Intro Top, en Coq on peut regarder ce que siginifie [True] et [False]:*) Print True. Print False. (** [True] est la formule qui n'a qu'un habitant [I] (traduction: le seul terme de type [True] est [I]). Prouver [True] revient à donner [I] qui a le bon type [I:True]. Bien sûr, [False] n'a pas d'habitant: on ne peut pas le prouver.*) apply I. (** La preuve est complète comme nous l'indique Coq.*) Qed. (** [Qed] demande à Coq de clore la preuve (une fois que tous les buts ont été prouvés). Coq construit alors le terme correspondant et lui donne le nom du lemme.*) Print tauto1. (** Résumé de cette magnifique preuve: tauto1 est une preuve de True (= tauto1 est la fonction I de type True). On a prouvé True car on a construit un terme habitant dans ce type. *) Lemma tauto2 (A B : Prop): A -> B -> A /\ B. (** Voici quelques règles générales sur la construction de preuves en Coq: - Coq nous indique le nombres d'objectifs (cad. de preuves à construire) avant de pouvoir clore la preuve (ici un objectif sur un total d'un), - Pour chaque objectif, on visualise le but (sous la ligne continue) et les hypothèses que l'on a à disposition. En déduction naturelle, on a [Gamma |- P] alors qu'en Coq, on a: << Gamma _______ (1/1) P >> - La construction de la preuve est dirigée par le but (ce qu'il faut montrer) un peu comme en déduction naturelle. On ne construit donc pas la preuve en partant des axiomes. Toutefois, on verra que l'on peut manipuler les axiomes plus facilement qu'en déduction natirelle, - On constuit la preuve en donnant à Coq une fonction à appliquer au but (qui va le remplacer par les sous-buts correspondants aux arguments de la fonction). On utilise le mot clé [apply [fonction]], - Comme ce n'est pas très pratique (on a vu ça avec [True]), on peut utiliser des tactiques pour s'aider. Il existe de nombreuses tactiques. Certaines vont essayer d'appliquer plusieurs fonctions selon la tête du séquent à prouver et permettent donc de gagner beaucoup de temps/lignes. On en verra une petite liste dans la section suivante. Retenez bien qu'une tactique ne fait généralement pas partie de la preuve. Elle permet de chercher un terme à appliquer en fonction de la tête du but et des hyptohèses.*) (** Ici, on va utiliser la tactique [intro]. Elle correspond à l'introduction de la flèche en déduction naturelle: << Gamma, P |- Q ----------------- Gamma |- P -> Q >> *) intro. intro. (** Ou plus simplement [intros]. C'est une bonne habitude de nommer les hyptohèses que l'on charge, ici j'aurais fait [intros HA HB] par ex. On doit désormais prouver une conjonction [/\]. On peut regarder ce que ça signifie. *) Locate "/\". Check and. Print and. (** [and] a le type [Prop] (c'est donc une formule) qui contient un seul habitant [conj] de type [A -> B -> and A B]. C'est comme cela qu'est encodée la conjonction en Coq. Et donc, pour construire un terme de type [and A B] il faut construire des termes de type [A] et [B] et appliquer cette fonction. *) Check conj. Print conj. apply conj. (** Cette fonction prenait deux arguments: il faut donc construire les termes (= preuves) pour ces deux arguments, d'où les deux sous-buts que Coq nous demande de prouver. *) (** On a le but en hypothèse. Il suffit donc d'appliquer la fonction H (de type A). *) apply H. (** On a prouvé le premier sous-but. Il reste le second sous-but. *) apply H0. Qed. (** On peut afficher le terme que l'on a construit (vous serez déçu ;) ): *) Print tauto2. (** Le terme que l'on a construit est simplement [conj]. On aurait pu pour prouver ce petit lemme directement en disant à Coq: "voici un terme habitant dans le type à prouver". On peut le faire en utilisant [exact]: *) Lemma tauto2bis: forall A B : Prop, A -> B -> A/\B. exact conj. Qed. (** Tout ça fait sens grace à la correspondance de Curry-Howard: << Le séquent [Gamma |- A] est prouvable en déduction naturelle intuitionniste si et seulement s'il existe un lambda-terme [t] tel que [Gamma |- t : A] (quitte à réindexer Gamma). >> Où [Gamma |- t : A] dénote que [t] a le type [A] dans le contexte de typage [Gamma]. *) (** On va maintenant prouver un lemme un poil plus compliqué. Mais cette fois, je vais utiliser des tactiques et on regardera le terme produit. *) Lemma tauto3 : forall A B : Prop, A/\B -> B/\A. intros A B H. (** On NOMME ces hypothèses *) destruct H. split. apply H0. apply H. Qed. Print tauto3. (** Ouf, comment on a fait ce pattern-matching? *) (** H est de type [and] qui ne contient que le constructeur conj, on peut donc réaliser un pattern-macthing sur le terme H. C'est ce que fait [destruct]: il n'y a qu'un pattern possible (car il n'y a qu'un seul habitant dans [and A B]) et on récupère les deux hypothèses [A] et [B] venant des arguments de conj. On remarque qu'ici, destruct fait la même chose que la règle de la conjonction gauche du calcul des séquents: << Gamma, A, B |- Q ------------------ Gamma, A/\B |- Q >>*) (** Ensuite [split] va appliquer la fonction constructeur associée au but (ici c'est la fonction conj) et donc générer les deux sous-buts correspondant à ses arguments. [split] correspond donc à la règle de l'introduction de la conjonction en déduction naturelle: << Gamma |- P Gamma |- Q -------------------------- Gamma |- P/\Q >> Et on conclut avec l'application des hypothèses.*) (** On peut aussi réutiliser un lemme déjà prouvé (ça revient à appliquer le terme construit lors de la preuve de ce lemme).*) Lemma tauto3' : forall A B : Prop, A/\B -> B/\A. intros A B AB. (** On NOMME ces hypothèses *) destruct AB. apply tauto2. apply H0. apply H. Qed. (** ** 2. Tactiques principales **) (*********************************) (** On peut s'amuser à construire le terme qui a exactement le bon type. Mais Coq nous permet de construire la preuve/fonction de façon interactive. Et c'est de cette façon qu'on écrira des preuves plus tard. On va se servir du "Coq cheat sheet" pour prouver quelques propriétés de logique propositionnelle. Prenez la page 2 de ce document. *) Lemma or_comm : forall A B, A\/B -> B\/A. Proof. intros A B AoB. destruct AoB. Print or. (** Et oui, si on fait [Print or] alors on se rend compte que le type [or] contient deux habitants (les deux projections): [or_introl : A -> A \/ B] et [or_intror : B -> A \/ B]. Donc [destruct] va faire le pattern-matching de ces deux cas ce qui aura pour effet de créer deux sous-buts suivant le pattern choisi. C'est exactement la règle de la disjonction gauche (\/ left) du calcul des séquents. *) right. auto. (** On a simplement choisi quelle côté de la disjonction on voulait prouver (comme le permet les deux règles de l'introduction de la disjonction (\/I1 et \/I2) de la déduction naturelle par exemple) et on a invoqué une hypothèse. [auto] est une tactique qui va chercher dans les hypothèses s'il n'y a pas directement le but. *) left. auto. Qed. Print or_comm. (** On va définir le prédicat "si et seulement si". On appelle "prédicat" un objet qui renvoie un [Prop] (une formule). *) Definition iff (P Q : Prop) := (P -> Q) /\ (Q -> P). (** On va maintenant prouver quelques lemmes sur ce prédicat. *) Lemma iff_implies : forall P Q, iff P Q -> (P -> Q). Proof. intros P Q H. (** Quand une hypothèse (ou la conclusion) contient une formule dont vous avez oublié la définition, vous pouvez l'unfolder de cette façon: *) unfold iff in H. destruct H as [HPQ HQP]. (** Le [as [nom1 nom2]] me permet de nommer les hypothèses générées par le [destruct]: c'est une bonne habitude de tout nommer. *) auto. Qed. Lemma iff_sym : forall P Q, (iff P Q) -> (iff Q P). Proof. intros P Q H. destruct H as [HPQ HQP]. split; auto. (** Dans la ligne précédente j'utilise le point virgule entre split et auto pour demander à Coq d'appliquer automatiquement [auto] à tous les sous-buts générés par [split]. Le point virgule est très utile pour automatiser certaines tâches redondantes.*) Qed. (** **** Question 6:*)(** Prouvez les lemmes suivants:*) (** On définit maintenant le prédicat sur les entiers "est un entier pair". Pour constuire un prédicat en Coq, il faut: - lui donner un nom et un type (ici [even : nat -> Prop], - définir les règles d'inférences (et leur donner des noms) qui permettent de définir ce prédicat. Dans notre cas, il y en a deux que l'on nommera even0 et evenS. La première dit simplement que 0 est pair (sans autre hypothèse). La seconde dit que sous l'hypothèse que [x] est pair alors [x+2] est pair.*) Inductive evenP : nat -> Prop := even0 : evenP 0 | evenS : forall x:nat, evenP x -> evenP (S (S x)). (** Cette définition est la traduction en Coq du prédicat [evenP] défini avec les règles d'inférences suivantes: << evenP x --------- even0 et ------------ evenS evenP 0 evenP (x+2) >> *) (** Attention: en écrivant ce type de données, on n'a pas prouvé que tout entier était pair. On a construit un terme qui prend un entier et qui renvoie la formule qui dit "l'entier est pair". Le lemme (faux) qui dit que tout entier est pair est [forall n, evenP n].*) (** **** Question 7:**) (** Prouvez maintenant que deux est pair: *) (** **** Question 8:**) (** Définissez le prédicat "plus petit que" de type [nat -> nat -> Prop]. Quelle est la différence avec ce que vous avez écrit pour la question 5 ? Prouvez que 3 et plus petit que 6.*) (** **** Question 9:**) (** Définissez le prédicat "estTrie" de type [list nat -> Prop]. Prouvez que [3 :: 6 :: nil] estTrie. *) (** ** 3. Preuves inductives et recherche de lemmes **) (*****************************************************) (** Si on veut montrer, par exemple, que [n+1] n'est pas pair si [n] est pair alors on va avoir besoin de raisonner par induction (vous en êtes convaincu?). Ca tombe bien parce que quand on définit un objet inductif, Coq nous fournit automatiquement un axiome d'induction structurelle. Pour les entiers c'est: *) Check nat_ind. (** C'est bien le schéma par induction habituel: on peut donc appliquer ce terme quand on veut faire une induction ou alors, de façon équivalente, appeler la tactique [induction]. On va s'en servir dans la preuve suivante. *) Require Import Arith. Lemma sum_even : forall n, evenP n -> ~ evenP (S n). Proof. intros n En. unfold not. intro ESn. (** On va faire une induction sur n: *) induction n. (** On doit traiter le cas n=0 (initialisation): *) (** Dans ce cas, on se rend compte que ESn n'est pas possible. On va utiliser la tactique [inversion] qui va traiter les différents cas possibles de evenP en éliminant ceux qui sont impossibles. *) inversion ESn. (** Cas inductif: on commence par utiliser l'hypothèse d'induction. *) apply IHn. (** On sait que n+2 est pair: on va donc inverser ESn et on aura que n est pair *) inversion ESn. auto. auto. Qed. (** [nat_ind] est en fait un lemme qui est automatiquement généré à partir de la définition inductive de [nat]. Et ça marche pour tous les prédicats inductifs. Par exemple: *) Check evenP_ind. (** On comprend qu'en fait ces lemmes sont des inductions strcuturelles (induction sur la dérivation qui permet de dériver le prédicat. Méditez là-dessus... *) (** Dans les preuves sur les entiers, on a souvent besoin d'utiliser des axiomes ou de petits lemmes triviaux pour réécrire des termes. Regardons cet exemple: *) Lemma pasSiFacile : forall n, n*2 + 0 = 1 - 1 + n + n. intro n. (** On a besoin d'expliquer à Coq que le [+ 0] ne sert à rien. Pour cela,on va chercher l'axiome qui dit que [n+0=n] (c'est vrai car 0 est le neutre de +, ça fait parti de l'axiomatisation des entiers dans Coq). On a différentes façons de chercher un lemme dans Coq: - [Search [objet]] cherche tous les lemmes prouvant une formule contenant [[objet]]; - [SearchAbout [formule]] cherche tous les lemmes contenant [[formule]]; - [SearchPattern [pattern]] cherche tous les lemmes prouvant une formule contenant [[pattern]]; - [SearchRewrite [pattern]] cherche tous les lemmes dont la conclusion est une égalité contenant [[pattern]].*) Search le. SearchAbout le. SearchRewrite (_ + 0). (** On va donc utiliser le lemme [plus_n_O] pour réécrire notre but. On utilise la tactique [rewrite] (avec une flèche [<-] si on veut réécrire dans le sens contraire). *) rewrite <- plus_n_O. (** (On peut aussi utiliser plus_0_r) *) SearchRewrite (_ - _). rewrite -> (minus_diag 1). (** **** Question 10:*)(** Terminez la preuve (sans autre tactique que [rewrite] et [reflexivity]). *) Qed. (** *) (** **** Question 11:*)(** Prouvez les lemmes suivants (réfléchissez à la preuve sur papier au préalable et sachez que vous pouvez faire des inductions sur les prédicats inductifs): *) Lemma even_double : forall n, evenP n -> exists (m m2 : nat), n = 2*m. Qed. Require Import Omega. (** La tactique [omega] résout tous les problèmes de systèmes d'inéquations et d'équations linéaires. *) Lemma double_even : forall n, evenP (2*n). Qed. Lemma sum_pair : forall n m, evenP n -> evenP m -> evenP (n+m). Qed. (** **** Question Bonus (bonus pris en compte pour le projet):*) (** Prouvez que la fonction de tri que vous avez écrite est correcte en utilisant le prédicat "estTrie" de la question 9. C'est tout pour la correction? *)