(******************)
(*   EXERCICE 1   *)
(******************)

(* 1. Deux égalités définitionnelles: preuve par "reflexivity" *)

Lemma plus_0_m :
  forall m, 0 + m = m.

Proof.
reflexivity.
Qed.

Lemma plus_Sn_m :
  forall n m, S n + m = S (n + m).

Proof.
reflexivity.
Qed.

(* 2. Deux égalités non-définitionnelles: preuve par induction *)

Lemma plus_n_0 :
  forall n, n + 0 = n.

Proof.
intro; induction n.
 reflexivity.
 simpl in |- *; rewrite IHn; reflexivity.
Qed.

Lemma plus_n_Sm :
  forall n m, n + S m = S (n + m).

Proof.
intros; induction n.
 reflexivity.
 simpl in |- *; rewrite IHn; reflexivity.
Qed.

(* 3. Commutativité *)

Lemma plus_commut :
  forall n m, n + m = m + n.

Proof.
intros; induction n.
 rewrite plus_n_0; reflexivity.
 simpl in |- *; rewrite plus_n_Sm; rewrite IHn; reflexivity.
Qed.

(* 4. Associativité *)

Lemma plus_assoc :
  forall n m p, (n + m) + p = n + (m + p).

Proof.
intros; induction n.
 reflexivity.
 simpl in |- * ; rewrite IHn; reflexivity.
Qed.

(**********************)
(*   MULTIPLICATION   *)
(**********************)

(* 1. Deux égalités définitionnelles: preuve par "reflexivity" *)

Lemma mult_0_m :
  forall m, 0 * m = 0.

Proof.
reflexivity.
Qed.

Lemma mult_Sn_m :
  forall n m, S n * m = m + n * m.

Proof.
reflexivity.
Qed.

(* 2. Pour prouver la commutativité de la multiplication, il faut
   d'abord reprendre les égalités ci-dessus, dans "l'autre sens".
   Il ne s'agit alors plus d'égalités définitionnelles, mais
   d'égalités que l'on prouve par induction. *)

Lemma mult_n_0 :
  forall n, n * 0 = 0.

Proof.
intro; induction n.
 reflexivity.
 simpl in |- *; rewrite IHn; reflexivity.
Qed.

Lemma mult_n_Sm :
  forall n m, n * S m = n + n * m.

Proof.
intros; induction n.
 reflexivity.
 simpl in |- *; rewrite IHn.
   rewrite <- (plus_assoc m n (n * m)).
   rewrite (plus_commut m n).
   rewrite (plus_assoc n m (n * m)).
   reflexivity.
Qed.

Lemma mult_commut :
  forall n m, n * m = m * n.

Proof.
intros; induction n.
 rewrite mult_n_0; reflexivity.
 simpl in |- *; rewrite IHn; rewrite mult_n_Sm; reflexivity.
Qed.

(* Avant de pouvoir démontrer l'associativité, il faut déjà
   établir la distributivité à gauche! *)

Lemma mult_plus_distr_l :
  forall n m p, (n + m) * p = n * p + m * p.

Proof.
intros; induction n.
 reflexivity.
 simpl in |- *.
   rewrite IHn.
   symmetry  in |- *; apply plus_assoc.
Qed.

Lemma mult_assoc :
  forall n m p, (n * m) * p = n * (m * p).

Proof.
intros; induction n.
 reflexivity.
 simpl in |- *.
   rewrite mult_plus_distr_l.
   rewrite IHn; reflexivity.
Qed.

(* 3. La distributivité à gauche a déjà été prouvée plus haut.
   On donne en bonus la distributivité à droite *)

Lemma mult_plus_distr_r :
  forall n m p, n * (m + p) = n * m + n * p.

Proof.
intros; induction n.
 reflexivity.
 simpl in |- *; rewrite IHn.
   rewrite (plus_assoc m p (n * m + n * p)).
   rewrite <- (plus_assoc p (n * m) (n * p)).
   rewrite (plus_commut p (n * m)).
   rewrite (plus_assoc (n * m) p (n * p)).
   symmetry  in |- *; apply plus_assoc.
Qed.

(******************)
(*   EXERCICE 3   *)
(******************)

Definition le (n m : nat) := exists p, n + p = m.

Lemma le_refl :
  forall n, le n n.

Proof.
intro n; exists 0; apply plus_n_0.
Qed.

Lemma le_trans :
  forall n m p, le n m -> le m p -> le n p.

Proof.
intros n m p H1 H2.
destruct H1 as (k1, H1).
destruct H2 as (k2, H2).
exists (k1 + k2).
rewrite <- plus_assoc.
rewrite H1; exact H2.
Qed.

(* Pour montrer l'antisymétrie, on a d'abord besoin des deux
   lemmes suivants: *)

(* (a) - Simplification à gauche *)

Lemma plus_simpl_l :
  forall n p q, n + p = n + q -> p = q.

Proof.
intros; induction n.
 assumption.
 injection H; assumption.
Qed.

(* (b) - Lemme de la somme nulle *)

Lemma plus_is_0 :
  forall n m, n + m = 0 -> n = 0 /\ m = 0.

Proof.
intros n m.
case n; clear n.
 case m; clear m.
  intro; split; reflexivity.
  intros n H; discriminate H.
 intros n H; discriminate H.
Qed.

(* Antisymétrie: *)

Lemma le_asym :
  forall n m, le n m -> le m n -> n = m.

Proof.
intros n m H1 H2.
destruct H1 as (k1, H1).
destruct H2 as (k2, H2).
assert (k1 = 0 /\ k2 = 0).
 apply plus_is_0.
   apply plus_simpl_l with n.
   rewrite <- plus_assoc.
   rewrite H1; rewrite H2.
   rewrite plus_n_0; reflexivity.
 destruct H.
   rewrite H in H1.
   rewrite plus_n_0 in H1; assumption.
Qed.