Entiers naturels et induction

Définition inductive des entiers naturels

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 !

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.

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

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

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.

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 :

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.

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.

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

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

Exercice : Prouver le théorème suivant.

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

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.

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 :

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.

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.

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.

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.

Preuve par induction (ou récurrence)

Les tactiques simpl, destruct, reflexivity et rewrite ne suffisent pas toujours :

Nous avons besoin de prouver ce théorème par induction. Une preuve par induction, aussi appelée preuve par récurrence sur entier naturel n a deux parties

• on prouve la proposition dans le cas où n vaut 0,
• puis dans le cas où n s'écrit S n' pour un certain n', on prouve la propriété pour n sous l'hypothèse qu'elle est vraie pour n' (on appelle cette hypothèse « hypothèse d'induction »).

Dans la tactique induction n as [|n' IH], il y a :

• rien à gauche de la barre | car c'est le cas 0, sans argument
• à droite de la barre | il y a n' car c'est le cas n = (S n') et il faut bien donner un nom à cette nouvelle variable et aussi un nom (ici IH) pour l'hypothèse que n' vérifie la propriété qu'on cherche à prouver.

Avec les tactiques intros, apply, destruct, simpl, discriminate, exfalso, reflexivity, induction et rewrite vous pouvez écrire énormément de preuves

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

Remarque : le choix de la variable sur laquelle porte l'induction est important, il est guidé par la façon dont la fonction add a été écrite. Comme cette fonction sépare les cas suivant son premier argument, les preuves sur + se feront par induction sur l'opérande de gauche.

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

Pour finir cette partie sur l'addition, quelques remarques de qualité de vie sur rewrite. Si vous avez suivi notre conseil sur simpl (ne pas trop l'utiliser), vous avez dû écrire beaucoup de rewrite. En fait, on peut enchaîner les réécritures avec la syntaxe rewrite regle_1, regle_2, ..., regle_n. Voici un exemple (avec de plus, un théorème qui sert souvent). Remarquer également qu'on a donné explicitement certains arguments.

La multiplication

La multiplication est aussi définie récursivement :

Avec des mots :

• si n = 0, alors mul n m = 0.
• sinon, n = (S p) pour un certain p, et alors mul (S p) m = m + (mul p m).

Réécrite avec les notations usuelles, la dernière égalité est bien compréhensible : (p + 1) × m = p × m + 1 × m = p × m + m = m + p × m. Dans la bibliothèque de Coq, la notation (n × m) correspond à (mul n m).

Exercice papier-crayon :

Évaluer à la main (mul 2 3). Les évaluations de l'addition peuvent être faites directement. Comme pour l'addition précédente, la définition de la multiplication est constructive, c'est-à-dire permet effectivement de calculer. On peut donc aussi utiliser la tactique simpl pour demander à Coq de calculer avec mul. Voir les exemples suivants :

Comme la multiplication fait intervenir l'addition dans sa définition, vous aurez à utiliser les théorèmes déjà prouvés sur l'addition. Pour rappel, ceux-ci sont :

• add_0_l : ∀ n : nat, 0 + n = n
• add_0_r : ∀ n : nat, n + 0 = n
• add_1_l : ∀ n : nat, 1 + n = S n
• add_1_r : ∀ n : nat, n + 1 = S n
• add_succ_l : ∀ n m : nat, S n + m = S (n + m)
• add_succ_r : ∀ n m : nat, n + S m = S (n + m)
• add_comm : ∀ n m : nat, n + m = m + n
• add_assoc : ∀ n m p : nat, n + (m + p) = (n + m) + p

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant (sans induction).

Comme pour l'addition, nous avons maintenant avec mul_succ_l et mul_0_l tout ce qu'il faut pour calculer avec rewrite, il vaut mieux éviter simpl.

Exercice : Prouver le théorème suivant (avec induction).

Exercice : Prouver le théorème suivant (avec induction).

Exercice : Prouver le théorème suivant (sans induction).

En général, les théorèmes et hypothèses sont écrits de façon à ce que le sens « naturel » de réécriture soit de gauche à droite (dans un certain sens, le membre de droite de l'égalité est « plus simple » que le membre de gauche). Il arrive toutefois qu'on doive réécrire en utilisant l'égalité de droite à gauche. Ceci se fait avec la syntaxe rewrite <-regle, comme le montre l'exemple suivant.

Avant de passer à quelque chose de plus sérieux (et difficile) un petit exercice stupide pour s'exercer. Utiliser add_assoc et l'hypothèse de droite à gauche. N'utiliser simpl qu'à la toute fin, lorsqu'il n'y a que des nombres littéraux.

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant par induction.

Celui ci est un peu embêtant... mais est un passage obligé pour prouver que la multiplication est commutative. Si vraiment, vous n'y arrivez pas après avoir beaucoup essayé, passez à la suite et revenez plus tard.

Exercice : Prouver le théorème suivant.

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. Ensuite, nous avons vu l'induction sur les entiers (la récurrence), avec la tactique induction nom_var as [| autre_nom_var nom_hypothese]. 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_0_r : ∀ n : nat, n + 0 = n
• add_1_l : ∀ n : nat, 1 + n = S n
• add_1_r : ∀ n : nat, n + 1 = S n
• add_succ_l : ∀ n m : nat, S n + m = S (n + m)
• add_succ_r : ∀ n m : nat, n + S m = S (n + m)
• add_comm : ∀ n m : nat, n + m = m + n
• add_assoc : ∀ n m p : nat, n + (m + p) = (n + m) + p
• mul_0_l : ∀ n : nat, 0 × n = 0
• mul_0_r : ∀ n : nat, n × 0 = 0
• mul_1_l : ∀ n : nat, 1 × n = n
• mul_1_r : ∀ n : nat, n × 1 = n
• mul_succ_l : ∀ n m : nat, S n × m = n × m + m
• mul_succ_r : ∀ n m : nat, n × S m = n × m + n
• mul_comm : ∀ n m : nat, n × m = m × n

Les autres propriétés importante de la multiplication sont à prouver dans les exercices à faire à la maison. Ce sont :

• mul_add_distr_l : ∀ n m p : nat, n × (m + p) = n × m + n × p
• mul_add_distr_r : ∀ n m p : nat, (n + m) × p = n × p + m × p
• mul_assoc : ∀ n m p : nat, n × (m × p) = n × m × p
• mul_eq_0: ∀ n m : nat, n × m = 0 ↔ n = 0 ∨ m = 0

Si vous avez vraiment bien assimilé tout ce sujet, vous avez sûrement beaucoup progressé en mathématiques et en informatique théorique ! (Et on espère que c'était amusant !)