(* This file is part of the "Initiation aux preuves formelles" course in Villetaneuse, France. Copyright (C) Kerjean, Mayero, Rousselin This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version. This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details. *)Set Keyed Unification. (* rewrite plus prévisible *)

Entiers naturels (1ère partie)

Définition inductive des entiers naturels

(* Le type [nat] est un type inductif : il est fait de constantes et de constructeurs, qui peuvent être récursifs, c'est à dire faire référence au type lui-même. *) Print nat. Check O. Check S.

Pour Coq, un entier naturel est soit

• O (la lettre O qui représente l'entier 0),
• soit l'image par la fonction S (pour "successeur") d'un entier naturel.

Ainsi :

• O représente zéro
• S O est le successeur de zéro donc un
• S (S O) est le successeur de un donc deux
• ...

Heureusement Coq permet la notation usuelle (décimale) de ces entiers, mais ce n'est qu'une notation pratique !

Check O. Check S (S O). Check S (S (S (S (S O)))). Check 0. (* notation 0 pour zéro (O) *)

On dit que la constante O et la fonction S sont les constructeurs du type nat. En Coq :

• les résultats de constructeurs différents sont toujours différents,
• deux termes composés uniquement de constructeurs ne peuvent être égaux que s'ils s'écrivent de la même manière.

À partir de maintenant, on utilisera la notation 0 (le chiffre zéro) pour zéro au lieu de O (la lettre O). La tactique discriminate H demande à Coq de vérifier que la preuve H d'une égalité entre deux termes écrits uniquement avec des constructeurs est contradictoire, c'est-à-dire est une preuve de False.

Theorem deux_non_egal_a_trois : ~ (S (S 0) = S (S (S 0))). Proof. (* En guise d'exemple, on prouve que 2 n'est pas égal à 3 dans [nat]. Remarquer que Coq a écrit ≠ dans le but, en effet « différent de » est la même chose en Coq que _non égal_. *) unfold not. (* Supposons (hypothèse ([H])) que [2 = 3]. *) intros H. (* Comme [2 = S (S 0)] et [3 = S (S (S 0))], ils s'écrivent différemment donc [H] fournit une preuve de False. *) discriminate H. Qed.

Exercice : Prouver le théorème suivant.

Theorem neq_0_succ : forall n : nat, ~ (0 = S n). Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant.

N'oubliez pas que de False, on prouve n'importe quoi.

Theorem exo_discriminate2 : forall n : nat, (S (S 0)) = (S 0) -> n = S n. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Addition des entiers naturels

Définissons maintenant l'addition des entiers relatifs. Dans un premier temps, on note add n m la somme de n et m.

Fixpoint add (n m : nat) : nat := match n with (* "faire correspondre n avec" *) 0 => m (* Si n = 0, alors n + m = m. *) | S p => S (add p m) (* (S p) + m = S (p + m). *) end.

Explications : add n m regarde si n vaut 0, si oui il renvoie m, sinon c'est que n = S p pour un certain p. On calcule alors (add p m) et on prend le successeur de ce nombre là. Cette définition de l'addition est récursive (en Coq, "Fixpoint" pour une définition récursive) : la fonction add est elle-même utilisée dans sa définition. Pourtant il n'y a pas de raisonnement circulaire, cette définition permet bien de calculer (sinon, Coq ne nous aurait pas laissé faire de toute façon). Cette définition est un programme : on a non seulement déclaré une fonction qui prend deux entiers et en retourne un, mais en plus on a dit comment calculer le résultat. Ceci permet à Coq de faire les calculs lui-même :

Compute (add 2 2). Compute (add 12 30).

Exercice qui a l'air bête mais est très important :

Calculer à la main (papier et crayon), en utilisant la définition de add : add (S (S 0)) (S (S (S 0))).

En fait Coq dispose des notations usuelles pour l'addition (et la plupart des opérations usuelles.

Compute 2 + 5.

Nous allons maintenant devoir prouver des égalités.

• La tactique simpl demande à Coq de calculer dans le but en utilisant « bêtement » la définition (et seulement la définition) d'une (ou plusieurs) fonctions, autant que possible. Elle n'est pas bien nommée, et devrait plutôt s'appeler «  compute  » ou quelque chose comme ça.
• La tactique reflexivity demande à Coq de conclure la preuve en constatant que les membres de gauche et de droite d'une égalité sont les mêmes.

Theorem deux_et_deux_font_quatre : 2 + 2 = 4. Proof. simpl. (* 2 + 2 = S (1 + 2) = S (S (0 + 2)) = S (S 2) = 4. *) reflexivity. Qed.

Exercice : Prouver le théorème suivant.

Theorem add_0_l : forall n : nat, 0 + n = n. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant.

Theorem add_1_l : forall n : nat, 1 + n = S n. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant.

Theorem add_succ_l : forall n m : nat, S n + m = S (n + m). Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant.

(* N'oubliez pas [discriminate] pour réfuter une égalité. *) Theorem deux_et_deux_ne_font_pas_cinq : ~ (2 + 2 = 5). Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

La tactique rewrite

La tactique rewrite est une tactique très importante, probablement la plus utilisée de toutes ! Elle permet de réécrire à l'aide d'une égalité. Si vous avez une hypothèse H : a = b alors rewrite H va transformer chaque a du but par un b.

Premiers exemples de rewrite

Theorem exemple_rewrite_hyp : forall n : nat, n = 42 -> n + 2 = 44. Proof. intros n H. (* Soit n un entier naturel tel que (hyp. H) n = 42. *) rewrite H. (* D'après (H) on peut réécrire n en 42. *) simpl. (* Par calcul, 42 + 2 = 44. *) reflexivity. (* Ce qui achève la preuve. *) Qed.

Exercice : Prouver le théorème suivant.

Theorem la_tete_a_toto : forall n : nat, n = 0 -> n + n = n. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Comme avec exact (ou en fait avec toutes les autres tactiques), on peut utiliser des théorèmes déjà prouvés, dont la conclusion est une égalité, pour faire des réécritures avec rewrite. On peut préciser à quels termes on applique ces théorèmes. Dans l'exemple important ci-dessous, tous les arguments sont précisés, on a aussi inséré des commandes Check pour que vous voyiez les énoncés précis utilisés, avant la réécriture (bien sûr, dans une vraie preuve on n'écrit pas ces Check).

(* On va utiliser les théorèmes suivants : *) Check add_1_l. Check add_0_l. Theorem exemple_rewrite_thm : forall n : nat, 0 + (1 + (1 + n)) = S (S n). Proof. intros n. (* Regardons ce que donne add_1_l appliqué au terme (1 + n). *) Check (add_1_l (1 + n)). rewrite (add_1_l (1 + n)). (* Regardons ce que donne add_1_l appliqué au terme n. *) Check (add_1_l n). rewrite (add_1_l n). (* Regardons ce que donne add_0_l appliqué au terme (S (S n)). *) Check (add_0_l (S (S n))). rewrite (add_0_l (S (S n))). reflexivity. Qed.

Exercice : sans utiliser simpl, prouver le théorème suivant.

C'est juste pour s'entraîner à rewrite et bien voir comment ça transforme le but). Vous utiliserez les règles add_0_l et add_1_l, ainsi que le « théorème » deux_et_deux_font_quatre.

Theorem exo_rewrite_theorems : (1 + 1) + ((0 + (0 + 1)) + 1) = 4. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Unification, encore

En fait, il arrive souvent qu'il n'y ait pas tellement le choix pour les arguments des théorèmes utilisés dans rewrite, ou bien, s'il y a le choix, que Coq décide pour vous de façon assez raisonnable. Alors, on peut omettre les arguments des théorèmes. Si on reprend l'exemple précédent en laissant Coq unifier/décider tout seul, ça donne :

Theorem exemple_rewrite_thm_unif : forall n : nat, 0 + (1 + (1 + n)) = S (S n). Proof. intros n. rewrite add_1_l. rewrite add_1_l. rewrite add_0_l. reflexivity. Qed.

En fait, avec add_0_l et add_succ_l on a deux résultats qui suffisent, avec rewrite, à prouver tous les autres. On peut aussi utiliser simpl, mais en fait simpl a un certain nombre de défauts :

• souvent il en fait trop
• pédagogiquement, cela ne correspond pas vraiment à quelque chose qu'on fait en mathématiques

Donc à part dans le cas où de nouvelles opérations sont définies, il vaut mieux éviter de l'utiliser et faire des rewrite plus précis et prévisibles.

Exercice : Prouver le théorème suivant sans simpl.

Utiliser uniquement les tactiques intros, rewrite et reflexivity et les théorèmes add_0_l, add_succ_l et add_1_l. Dans un premier temps, vous donnerez dans les rewrite les arguments, dans un second temps, voir si vous pouvez les omettre et laisser Coq remplir tout seul les trous.

Theorem exo_rewrite_unif : forall n : nat, 0 + ((S 1) + S (1 + n))= S (S (S (S n))). Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Preuve par cas : destruct (encore)

La façon dont sont construits les naturels en Coq fait apparaître deux cas bien différents : un entier naturel, disons n vaut :

• soit 0
• soit (S n') où n' est un autre entier.

En Coq, la tactique destruct sur une variable de type entier (en général de n'importe quel type inductif) permet les preuves par cas.

Theorem double_eq_0_is_0 : forall n : nat, n + n = 0 -> n = 0. Proof. (* Soit [n] un entier naturel. *) intros n. (* On suppose (hyp. ([H])) que [n + n = 0]. *) intros H. (* Preuve par cas : [n] est soit nul soit successeur d'un entier [n']. Remarquer que dans le deuxième cas, on doit nommer l'entier (ici [n']) dont n est le successeur. *) destruct n as [| n']. - (* Premier cas : [n = 0]. *) reflexivity. - (* Deuxième cas : [n = S n'] pour un certain [n' : nat]. *) (* Nous allons montrer que ce cas est impossible. *) exfalso. (* En réécrivant avec [add_succ_l], l'hypothèse [H] devient [S (n' + S n') = 0]. *) rewrite add_succ_l in H. (* Noter la nouvelle syntaxe [rewrite règle in nom_hypothese]. *) (* Or, il est impossible que le successeur d'un naturel soit nul, par définition des entiers naturels. *) discriminate H. Qed.

Dans la tactique destruct n as [| n'] on retrouve la syntaxe quelque_chose | autre_chose, qu'on avait vue lorsqu'on détruit les \/. Ici :

• quelque_chose est vide car c'est le cas n = 0, donc avec le constructeur sans argument
• autre_chose est n' : on nomme l'entier n' tel que n = (S n'). Bien sûr on aurait pu choisir n'importe quel autre nom que n'.

Remarque : on vient de voir qu'on peut aussi utiliser rewrite dans une hypothèse à l'aide de la syntaxe rewrite règle in nom_hypothese.

Exercice : Prouver le théorème suivant avec une preuve par cas .

Theorem npm_eq_0 : forall (n m : nat), n + m = 0 -> n = 0. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant avec une preuve par cas .

Indice : il faut faire une deuxième preuve par cas dans un des cas.

Theorem exo_destruct2 : forall n : nat, S (S (S n)) = 4 -> n = 1. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Bilan

Nous avons d'abord vu que les entiers naturels sont définis en Coq par induction. Il y a 0, puis S 0, puis S (S 0), ... Par définition, deux entiers naturels écrits uniquement avec des constructeurs sont différents s'ils sont syntaxiquement différents. La tactique discriminate nom_d'hypothese permet de trouver une contradiction (donc de terminer la preuve) de ce type dans une égalité. Un aspect important de Coq est qu'il est capable de calculer . Nous avons vu qu'avec la tactique simpl, il calcule autant qu'il peut en utilisant les définitions données. La tactique reflexivity permet de terminer une preuve d'une égalité en demandant à Coq de constater que les membres gauche et droit d'une égalité sont les mêmes. La tactique rewrite preuve_egalite utilise la preuve d'une égalité disons a = b pour changer tous les a du but en b. Nous avons vu qu'avec un théorème du type égalité universellement quantifiée, on peut laisser Coq unifier (remplir les trous) ou bien au contraire les remplir nous-mêmes. La variante rewrite preuve_egalite in nom_d'hypothèse permet de réécrire dans une hypothèse plutôt que dans le but. Il est possible d'enchaîner les réécritures en séparant les règles par des virgules. Enfin, il est possible de réécrire avec une égalité vue de droite à gauche avec la syntaxe rewrite <-preuve_egalite. Enfin, nous avons prouvé de nombreuses propriétés très utiles de l'addition et de la multiplication (mais inutile de les apprendre par coeur) :

• add_0_l : ∀ n : nat, 0 + n = n
• add_1_l : ∀ n : nat, 1 + n = S n
• add_succ_l : ∀ n m : nat, S n + m = S (n + m)

La liste est très courte pour l'instant ! Pour prouver plus de lemmes, nous aurons besoin d'une nouvelle méthode de preuve : la preuve par induction (aussi appelée par récurrence sur les entiers naturels). Ceci sera fait dans le sujet de TP suivant.