(* 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
Ainsi :
Heureusement Coq permet la notation usuelle (décimale) de ces
entiers, mais ce n'est qu'une notation pratique !
- O (la lettre O qui représente l'entier 0),
- soit l'image par la fonction S (pour "successeur") d'un entier naturel.
- 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
- ...
On dit que la constante O et la fonction S sont les
constructeurs du type nat. En Coq :
À 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.
- 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.
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.
Theorem neq_0_succ : ∀ n : nat, ¬ (0 = S n).
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Theorem exo_discriminate2 : ∀ n : nat, (S (S 0)) = (S 0) → n = S n.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Addition des entiers naturels
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.
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 :
Exercice qui a l'air bête mais est très important :
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.
Theorem add_0_l : ∀ n : nat, 0 + n = n.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Theorem add_1_l : ∀ n : nat, 1 + n = S n.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Theorem add_succ_l : ∀ n m : nat, S n + m = S (n + m).
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
(* 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
Premiers exemples de rewrite
Theorem exemple_rewrite_hyp : ∀ n : nat, n = 42 → n + 2 = 44.
Proof.
intros n H.
rewrite H.
simpl.
reflexivity.
Qed.
Theorem la_tete_a_toto : ∀ n : nat, n = 0 → n + n = n.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
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 : ∀ n : nat, 0 + (1 + (1 + n)) = S (S n).
Proof.
intros n.
Check (add_1_l (1 + n)).
rewrite (add_1_l (1 + n)).
Check (add_1_l n).
rewrite (add_1_l 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.
Theorem exo_rewrite_theorems : (1 + 1) + ((0 + (0 + 1)) + 1) = 4.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Unification, encore
Theorem exemple_rewrite_thm_unif : ∀ 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 :
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.
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.
- souvent il en fait trop
- pédagogiquement, cela ne correspond pas vraiment à quelque chose qu'on fait en mathématiques
Exercice : Prouver le théorème suivant sans simpl.
Theorem exo_rewrite_unif :
∀ n : nat, 0 + ((S 1) + S (1 + n))= S (S (S (S n))).
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
∀ 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)
- soit 0
- soit (S n') où n' est un autre entier.
Theorem double_eq_0_is_0 : ∀ 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'. *)
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 :
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.
- 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'.
Exercice : Prouver le théorème suivant avec une preuve par cas.
Theorem npm_eq_0 : ∀ (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.
Theorem exo_destruct2 : ∀ n : nat, S (S (S n)) = 4 → n = 1.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Preuve par induction (ou récurrence)
Theorem add_0_r : ∀ n : nat, n + 0 = n.
Proof.
intros n.
simpl. (* Aïe, simpl ne marche pas *)
(* On peut essayer une preuve par cas : *)
destruct n as [| n'].
- (* le cas n = 0 se passe bien *)
simpl. reflexivity.
- (* mais là on va être bloqué... *)
simpl.
(* Il nous faudrait une preuve que n' + 0 = 0...
On est bloqué. *)
Abort. (* La commande Abort abandonne une preuve. *)
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 »).
Theorem add_0_r : ∀ (n : nat), n + 0 = n.
Proof.
induction n as [|n' IH].
- (* On suppose que n = 0. *)
(* Par définition de +, 0 + 0 vaut 0. *)
rewrite add_0_l.
(* Les deux membres de l'égalité sont les mêmes, ce cas est terminé. *)
reflexivity.
- (* On suppose que n = S n' et que n' vérifie
(IH) : n' + 0 = n'. *)
(* Par définition de +, S n' + 0 = S (n' + 0). *)
rewrite add_succ_l.
(* On remplace, grâce à (IH), le terme (n' + 0) par n'. *)
rewrite IH.
(* Les deux membres de l'égalité sont les mêmes, c'est terminé. *)
reflexivity.
Qed.
Dans la tactique induction n as [|n' IH], il y a :
Avec les tactiques intros, apply, destruct, simpl, discriminate,
exfalso, reflexivity, induction et rewrite vous pouvez écrire
énormément de preuves
- 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.
Exercice : Prouver le théorème suivant.
Theorem add_1_r : ∀ n : nat, n + 1 = S n.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Exercice : Prouver le théorème suivant.
Theorem add_succ_r : ∀ n m, n + S m = S (n + m).
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
(* Indice : utiliser les théorèmes précédents avec la tactique
rewrite. Par exemple, si le but contient une expression du type
truc + S bidule, alors rewrite add_succ_r remplace cette expression
par S (truc + bidule). *)
Theorem add_comm : ∀ (n m : nat), n + m = m + n.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Theorem add_assoc : ∀ (n m p : nat), n + (m + p) = (n + m) + p.
Proof.
(* Remarquez que Coq affiche naturellement + comme étant
associatif à gauche *)
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Proof.
(* Remarquez que Coq affiche naturellement + comme étant
associatif à gauche *)
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
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.
Theorem add_succ_comm : ∀ n m, n + S m = S n + m.
Proof.
induction n as [| n' IH].
- intros m. rewrite add_0_l, add_1_l. reflexivity.
- intros m. rewrite (add_succ_l (S n')), add_succ_l.
rewrite (IH m). reflexivity.
Qed.
Avec des mots :
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).
- 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).
Exercice papier-crayon :
Theorem secret_of_the_universe : 6 × 7 = 42.
Proof.
simpl.
reflexivity.
Qed.
Theorem mul_0_l : ∀ n : nat, 0 × n = 0.
Proof.
intros n.
simpl.
reflexivity.
Qed.
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.
Theorem mul_succ_l : ∀ n m : nat, (S n) × m = n × m + m.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Theorem mul_1_l : ∀ n : nat, 1 × n = n.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
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).
Theorem mul_0_r : ∀ n : nat, n × 0 = 0.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Theorem mul_1_r : ∀ n : nat, n × 1 = n.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Theorem mul_eq_0_rl : ∀ n m : nat, (n = 0 ∨ m = 0) → n × m = 0.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
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.
Theorem exple_rewrite_rl : ∀ n, 6 = n → n × (S n) = 42.
Proof.
intros n H.
rewrite <-H.
simpl.
reflexivity.
Qed.
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.
Theorem exercise_rewrite_rl : ∀ n, 15 = 10 + n → 27 + n + 10 = 42.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Exercice : Prouver le théorème suivant par induction.
Theorem mul_succ_r : ∀ n m : nat, n × S m = n × m + n.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Theorem mul_comm : ∀ n m : nat, n × m = m × n.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Bilan
- 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
- 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