Projet Coq - TPs

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: 
http://www.lsv.ens-cachan.fr/~hirschi/enseignements/projet_coq/projet_coq.php

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:Set (T est de type 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 avec les définitions de fonctions et de données (on restera dans le monde Set). Puis dans la section suivante sur les preuves, on plongera dans le monde Prop.

II : Programmer en Coq

1. Fonctions, calcul, bool

Je vais ouvrir une section bool, tout ce que je vais importer le sera uniquement dans cette section.
Section SecBool.
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 objet avec Print.
  Print bool.
bool (qui est lui même de type Set) est un type 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:
  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 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 (b1 b2 b3 : bool) (n:nat) :=
    let n' := n + 1 in
    match b1 with
      | true => b2
      | false => b3
    end.
On peut aussi écrire:
  Definition f := fun b:bool => b.
On essaye d'appeler notre fonction:
  Check (ifb2 true true false 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 true false 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.
End SecBool.

Question 1:

Ecrivez une fonction qui renvoie le XOR de trois booléens et testez-la.
Definition xor (b1 b2 b3 : bool) : bool :=
  if b1
  then if b2 then false
       else if b3 then false else true
  else if b2
       then if b3 then false else true
       else b3.
Eval compute in (xor true false true).
Eval compute in (xor false true true).
Eval compute in (xor false false true).

2. Définitions inductives, points fixes et nat

Section SecNat.
  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.
  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.
End SecNat.

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.
Fixpoint evenb (n:nat) :=
  match n with
    | 0 => true
    | S p => negb (evenb p)
end.
Eval compute in (evenb 5).
Eval compute in (evenb 8).

Question 3:

Ecrivez un type de données arbre contenant une représentation de tous les arbres binaires étiquetés par des entiers.
Inductive arbreb : Set :=
  Feuille
| Noeud : nat -> arbreb -> arbreb -> arbreb.

Question 4:

Ecrivez une fonction qui renvoie la somme de toutes les étiquettes des noeuds d'un arbre. Testez.
Fixpoint sum_arbre (arbre:arbreb) :=
  match arbre with
    | Feuille => 0
    | Noeud n a1 a2 => n + (sum_arbre a1) + (sum_arbre a2)
end.
Eval compute in (sum_arbre (Noeud 5 (Noeud 1 Feuille Feuille) (Noeud 2 Feuille Feuille))).

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.
Fixpoint is_le (n m : nat) :=
  match n with
    | 0 => true
    | S n' => match m with
                 0 => false
               | S m' => is_le n' m'
              end
  end.
Eval compute in (is_le 3 4).
Eval compute in (is_le 1 7).
Eval compute in (is_le 23 21).

Question Bonus (bonus pris en compte pour le projet):

Ecrivez une fonction qui calcule le pgcd de deux entiers. Testez.
Fixpoint eq (n m : nat) : bool :=
  match n, m with
    | 0, 0 => true
    | S n', S m' => eq n' m'
    | _,_ => false
  end.
Si on écrit naivement l'algo d'euclide on aura pas la décroissance structurelle. On introduit un compteur d'appel récursif n qui décroît à chaque étape. A nous, dans la suite, de prouver (en Coq) que n=a+b suffit et que pgcd calcule bien le PGCD.
Fixpoint pgcdN (n a b : nat) : nat :=
  match n with
    | O => 1
    | S n' =>
      match a,b with
        | 1,_ => 1
        | _, 1 => 1
        | 0, _ => b
        | _, 0 => a
        | _, _ => match is_le a b with
                          | true => match eq a b with
                                      | true => a
                                      | false => pgcdN n' (b-a) a
                                    end
                          | false => pgcdN n' (a-b) b
                        end

      end
end.
Definition pgcd (a b : nat) : nat := pgcdN (a+b+1) a b.
Eval compute in (pgcd 4 12).
Eval compute in (pgcd 15 20).
Eval compute in (pgcd 36 45).

3. Types polymorphes, listes et types dépendants

Section SecList.
  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).
End SecList.

Question Bonus (bonus pris en compte pour le projet):

Ecrire une fonction qui réalise le fold_left d'OCaml sur les listes.
Fixpoint fold_left (A B:Type) (f : A->B->A) (a:A) (l : list B) : A :=
  match l with
    | nil => a
    | b :: l' => f (fold_left A B f a l') b
end.
Eval compute in (fold_left nat nat plus 0 (1::2::3::nil)).

Question Bonus (bonus pris en compte pour le projet):

Ecrire une fonction de tri. On encode le tri par insertion.
Fixpoint insert (l : list nat) (a : nat) : list nat :=
  match l with
      | nil => a :: nil
      | x :: l' => if is_le a x
                   then a :: l
                   else x:: (insert l' a)
end.
Fixpoint tri (l : list nat) : list nat :=
  match l with
      | nil => nil
      | hd :: tl => insert (tri tl) hd
end.
Eval compute in (tri (1::4::5::nil)).
Eval compute in (tri (10::2::0::22::nil)).
Eval compute in (tri (5::4::5::nil)).

4. Résumé

Voici quelques lignes de Coq que vous devez comprendre (ainsi que les messages de 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). 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.

Section Curry.
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.
  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 : forall 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). On ne construit donc pas la preuve en partant des axiomes,
  • 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. 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 a b A B 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 On a le but en hypothèse. Il suffit donc d'appliquer la fonction H (de type A).
    apply H.
    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 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 -> A/\B.
    intros A B H.
On NOMME ces hypothèses
    destruct H.
    split.
    apply H.
    apply H0.
  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.
End Curry.

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:
Lemma and_assoc : forall P Q R, P /\ (Q /\ R) -> (P /\ Q) /\ R.
  intros P Q R PQR.
  destruct PQR as [HP [HQ HR]].
  split;auto.
Qed.

Lemma iff_trans : forall P Q R, (iff P Q) -> (iff Q R) -> (iff P R).
  intros P Q R PQ QR.
  destruct PQ.
  destruct QR.
  split; auto.
Qed.
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:
Lemma deux_pair : evenP 2.
  apply evenS.
  apply even0.
Qed.

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.
Inductive leP : nat -> nat -> Prop :=
  Ze : forall n, leP 0 n
| Su : forall n m, leP n m -> leP (S n) (S m).

Question 9:

Définissez le prédicat "estTrie" de type list nat -> Prop. Prouvez que 3 :: 6 :: nil estTrie.
Inductive estTrie : list nat -> Prop :=
  TNil : estTrie nil
| TOne : forall x:nat, estTrie (x::nil)
| TCons : forall x y:nat, forall tl:list nat, leP x y -> estTrie (y :: tl) -> estTrie (x::y::tl).
Lemma test : estTrie (3::6::nil).
  apply TCons.
  repeat (apply Su);apply Ze.
  apply TOne.
Qed.

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. 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_nat.
On comprend qu'en fait ces lemmes sont des inductions 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).
  SearchRewrite (_+_).
  SearchRewrite (_+_+_).
  rewrite plus_assoc_reverse.
  rewrite plus_comm.
  rewrite <- plus_n_O.
  SearchRewrite (_ * _).
  rewrite mult_succ_r.
  rewrite mult_1_r.
  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, n = 2*m.
  intros n En.
  induction En.
  exists 0; ring.
  destruct IHEn.
  exists (x0+1).
  rewrite H.
  replace (2*(x0+1)) with (2*x0 +2).
  ring.
  ring.
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).
  intros n.
  induction n.
  simpl.
  apply even0.
  assert (2*(S n) = S (S (2*n))).
  omega.
  rewrite H.
  apply evenS.
  auto.
Qed.

Lemma sum_pair : forall n m, evenP n -> evenP m -> evenP (n+m).
  intros n m En Em.
  destruct (even_double n);auto.
  destruct (even_double m);auto.
  rewrite H.
  rewrite H0.
  replace (2*x+2*x0) with (2* (x+x0)).
  apply double_even.
  ring.
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?
Lemma is_le_mono : forall x y, is_le x y = true -> is_le x (S y)=true.
  admit.
laissé en exo
Qed.
Lemma is_le_sym : forall x, is_le x x=true.
admit.
laissé en exo
Qed.
Lemma is_le_correct : forall x y, x<=y <-> is_le x y=true.
intros x y.
split.
intros xly.
induction y;auto.
inversion xly.
auto.
assert ((x<=y) \/ x=(S y)) by omega.
destruct H.
apply is_le_mono;auto.
rewrite H.
apply is_le_sym.

intro xLy.
induction x.
omega.
induction y.
inversion xLy.
simpl in xLy.
admit.
Qed.
Lemma leP_correct : forall x y, x<=y <-> leP x y.
 admit. Qed.
Lemma disj_is_le : forall x y, is_le x y = true \/ is_le x y = false.
intros.
destruct (is_le x y); tauto.
Qed.

Lemma insert_correct : forall l a, estTrie l -> estTrie (insert l a).
  intros l a ETl.
  elim ETl.
  Print estTrie.
  simpl. apply TOne.
  intro x.
  destruct (disj_is_le a x); simpl; rewrite H; simpl.
  apply TCons.
  apply leP_correct;auto.
  apply is_le_correct;auto.
  apply TOne.
  apply TCons.
  apply leP_correct; auto.
  assert (~ a<=x).
  intro.
  assert (is_le a x=true). apply is_le_correct; auto; auto.
  assert (true=false). rewrite <- H; auto.
  intuition. intuition.

  apply TOne.

  intros x y tl Lexy ET1 ET2.
  assert (ETxy : estTrie (x :: y :: tl)).
  apply TCons; auto.

  destruct (disj_is_le a x); simpl; rewrite H; simpl.
  apply TCons.
  apply leP_correct; auto.
  apply is_le_correct; auto.
  apply TCons; auto.

  destruct (disj_is_le a y); simpl. rewrite H0; simpl.
  apply TCons.
  apply leP_correct.
  assert (~ a<= x).
  intro.
  assert (is_le a x=true).
  apply is_le_correct; auto.
  assert (true=false).
  rewrite <-H2.
  rewrite <-H; auto.
  intuition.
  omega.
  unfold insert in ET2.
  rewrite H0 in ET2; auto.

  rewrite H0; simpl.
  apply TCons; auto.
  unfold insert in ET2.
  rewrite H0 in ET2; auto.
Qed.

Lemma tri_correct : forall l:list nat, estTrie (tri l).
  induction l.
  apply TNil.
  assert (estTrie (insert (tri l) a)).
  unfold insert.
  apply insert_correct;auto.
  auto.
Qed.
Ouf.. Bon on a prouvé que notre fonction de tri renvoie toujours des listes triées. Mais ça ne suffit pas! La fonction pourrait très bien toujours renvoyer une liste vide. Il faut aussi montrer que la liste renvoyée par tri est une permutation de la liste en entrée.
Inductive isIn : nat -> list nat -> Prop :=
  | IsHD : forall n l, isIn n (n::l)
  | IsTL : forall n hd l, isIn n l -> isIn n (hd::l).
Inductive permP : list nat -> list nat -> Prop :=
  | pNil : permP nil nil
  | pCons : forall l l' n, permP l l' -> isIn n l' -> permP (n::l) l'.
Lemma tri_correct_perm : forall l, permP l (tri l).
  admit.
si vous êtes motivés
Qed.
This page has been generated by coqdoc