Require Import Unicode.Utf8.
Set Keyed Unification. (* rewrite plus prévisible *)
Require PeanoNat.
Import PeanoNat.Nat.

Exercices supplémentaires sur les entiers naturels

Pour résoudre ces exercices, vous pouvez utiliser les théorèmes suivants (déjà prouvés dans Naturels) :
  • 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
ainsi, bien sûr, que les théorèmes prouvés précédemment dans ce sujet.
Pour vous souvenir de l'énoncé, vous pouvez utiliser la commande Check.
Check mul_comm.

Exercice : Prouver le théorème suivant.

Indice pour le sens direct : faire une preuve par cas sur la nullité ou non de n ou de m (utiliser la tactique destruct).
Theorem mul_eq_0 : ∀ (n m : nat), n × m = 0 ↔ n = 0 ∨ m = 0.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant.

Theorem mul_add_distr_r : ∀ n m p : nat, (n + m) × p = n × p + m × p.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

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

Utiliser rewrite et les théorèmes précédents.
Theorem mul_add_distr_l : ∀ n m p : nat, n × (m + p) = n × m + n × p.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant.

Theorem mul_assoc : ∀ n m p : nat, (n × m) × p = n × (m × p).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)