Entiers naturels (2ème partie : induction)

Induction sur les entiers naturels

On rappelle que 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.

Les tactiques simpl, destruct, reflexivity et rewrite vues dans le sujet précédent 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 (lorsque le type est celui des entiers naturels) 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 nsous 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.

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.

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.

Indication : Vous aurez à utiliser une propriété de l'addition.

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 (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. Ce qui est embêtant est qu'il faut jouer avec l'associativité de l'addition, ce qu'à l'écrit on ne détaille jamais. La solution utilise les règles suivantes : mul_0_l, add_0_r, mul_succ_l, add_assoc, add_comm et add_succ_comm, parfois de droite à gauche, et certaines sont utilisées plusieurs fois... Il est conseillé d'écrire le but sur papier, avec les parenthèses apparentes et de travailler déjà sur papier à la façon d'obtenir le but. N'hésitez pas à demander de l'aide à un camarade ou à votre chargé⋅e de TP si vous n'y arrivez pas.

Exercice : Prouver le théorème suivant.

Bilan

Dans ce sujet, nous avons essentiellement travaillé 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 !)