(***  On peut voir le type nat chargé par Coq avec la commande:***)
Print nat.

(*** Au moment de la définition du type inductif nat, plusieurs principes
d'induction sont créés. Par exemple le principe de récurrence:***)
Check nat_ind.

(************************************)
(******* Autour de l'addition *******)
(************************************)


(***On peut voir l'implémentation de l'adition avec la commande suivante.
Noter l'usage de la notation + qui apparaît dans le
corps de la définition. ***)
Print plus.


(*** Deux égalités définitionnelles : ce sontdes identités qui s'obtient
uniquement en dépliant la définition du plus et en "calculant" (réduisant)
autant que possible ***)
Lemma plus0m : forall m, 0 + m = m.
Proof. intro m; reflexivity. Qed.

Lemma plusSn : forall n m, S n + m = S (n + m).
Proof. intros n m; reflexivity. Qed.

(*** Par contre les deux identités suivantes ne sont pas définitionnelles:
il faut une induction sur le premier argument du plus pour les prouver ***)
Lemma plusn0 : forall n, n + 0 = n.
Proof. 
intro n; elim n.
  reflexivity.
intros m Hrec.
simpl.
rewrite Hrec.
reflexivity.
Qed.

Lemma plusnS :
  forall n m, n + S m = S (n + m).
Proof.
intros; induction n. 
(* contrairement a la tactique elim, induction introduit et nomme
les hypothèses qu'elle engendre *)
  reflexivity.
simpl.
rewrite IHn.
reflexivity.
Qed. 

(*** Commutativité ***)

Lemma plusC : forall n m, n + m = m + n.
Proof.
intro n; elim n.
  intro m; elim m.
    reflexivity.
  intros k Hk.
  simpl.
  rewrite <- Hk.
  reflexivity.
intros m Hm k.
simpl.
rewrite Hm.
rewrite plusnS.
reflexivity.
Qed.


(*** Associativité ***)
Lemma plusA : forall n m p, (n + m) + p = n + (m + p).
Proof.
intro n; elim n.
  intros m p; simpl; reflexivity.
intros m Hm p q.
simpl; rewrite Hm.
reflexivity.
Qed.

(************************************)
(*** Autour de la multiplication ****)
(************************************)

Lemma mult0n : forall n, 0 * n = 0.
Proof. intro n; reflexivity. Qed.

Lemma multSn : forall n m, S n * m = m + n * m.
Proof. intros n m; reflexivity. Qed.

Lemma multC : forall n m, n * m = m * n.
Proof.
intro n; elim n.
  intro m; elim m; [reflexivity|intros p Hp].
  simpl.
  rewrite <- Hp.
  reflexivity.
intros m Hm p.
simpl.
rewrite Hm.
(*  on prouve ce résultat par induction sur p.
on aurait pu en faire un lemme multnS, à la manière de multSn *)
elim p.
  reflexivity.
intros q Hq.
simpl.
rewrite <- Hq.
rewrite <- plusA.
rewrite (plusC q m).
rewrite <- plusA.
reflexivity.
Qed.

(* Remarque sur le comportement de la tactique rewrite :

Si on ne fournit pas les arguments du lemme à réécrire, comme
ci dessus dans "rewrite <- plusA", c'est la première instanciation
possible des arguments qui décide de la valeurs des arguments.
Puis toutes les  occurrences du membre gauche de l'égalité complètement 
instanciée ainsi obtenue sont réécrites.

On peut aussi ne fournir à la tactique rewrite que le lemme 
partiellement appliqué.

Ces remarques évitent de fournir systématiquement les arguments 
qui peuvent être de "gros" termes.

Néanmoins il peut s'avérer impossible d'éviter de les fournir...
 *)


(*** Associativité de la multiplication ***)

(* En fait, on prouve d'abord la distributivité à droite *)
Lemma mult_plusDr :
  forall n m p, n * (m + p) = n * m + n * p.
Proof.
intros n m p; elim n; clear n. (* nettoyage de n qui n'est plus utilisé*)
  reflexivity.
intros n HIn.
simpl; rewrite HIn.
rewrite (plusA m p (n * m + n * p)).
rewrite <- (plusA p (n * m) (n * p)).
rewrite (plusC p (n * m)).
rewrite (plusA (n * m) p (n * p)).
(* plusA est partiellement appliqué mais suffisamment 
pour sélectionner la bonne occurrence*)
rewrite (plusA m). 
reflexivity.
Qed.

(* Pour le même prix on a la distributivité à gauche, grâce à la 
commutativité*)
Lemma mult_plusDl : forall n m p, (n + m) * p = n * p + m * p.
Proof.
intros n m p.
rewrite multC.
rewrite mult_plusDr.
rewrite (multC p).
rewrite (multC p m).
reflexivity.
Qed.

Lemma multA : forall n m p, (n * m) * p = n * (m * p).
Proof.
intro n; elim n.
intros; induction n.
    reflexivity.
  reflexivity.
intros m HIm p q. 
simpl. 
rewrite mult_plusDl.
rewrite HIm.
reflexivity.
Qed.

(*** Relation d'ordre ***)
Definition le (n m : nat) := exists p, n + p = m.


Lemma le_refl : forall n, le n n.
Proof.
intro n. 
exists 0. 
rewrite plusn0.
reflexivity.
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 <- plusA.
rewrite H1; exact H2.
Qed.


(* Un lemme de régularité à gauche *)
Lemma plus_reg_l : forall n p q, n + p = n + q -> p = q.
Proof.
intros; induction n.
 assumption.
 injection H; assumption.
Qed.

(* Une somme nulle est une somme de zéros *)
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_reg_l with n.
   rewrite <- plusA.
   rewrite H1; rewrite H2.
   rewrite plusn0; reflexivity.
 destruct H.
   rewrite H in H1.
   rewrite plusn0 in H1; assumption.
Qed.