Section nat_experiment Fixpoint plus nat nat nat match with plus end F

Section nat_experiment.

Fixpoint plus (n:nat)(m:nat) : nat :=
  match n with 
  | 0 => m
  | S(n') => S (plus n' m)
end.


Fixpoint mult (n:nat)(m:nat) : nat :=
  match n with
  | 0 => 0
  | S(n') => plus m (mult n' m)
end.


Lemma plus_0_l: forall n:nat, plus 0 n = n.
Proof.
  simpl.
  reflexivity.
Qed.


Lemma plus_0_r: forall n:nat, plus n 0 = n.
Proof.
  intros.
  induction n.
  reflexivity.
  simpl.
  rewrite -> IHn.
  reflexivity.
Qed. 

Lemma plus_0_r_2: forall n:nat, plus n 0 = n.
Proof.
  intros.
  destruct n.
  reflexivity.
  auto.
Qed.

Lemma plus_0: forall n:nat, plus n 0 = plus 0 n.
Proof.
  intros.
  rewrite -> plus_0_l.
  rewrite -> plus_0_r_2.
  reflexivity.
Qed.

Notation "x + y" := (plus x y)
                       (at level 50, left associativity)
                       : nat_scope.
  
Lemma plus_s: forall n m, n+S(m) = S(n+m).
Proof.
  intros.
  destruct n.
  simpl.
  reflexivity.
  simpl.
  auto.
Qed.
  

  
Theorem plus_commutative: forall n m, (plus n m) = (plus m n).
Proof.
  intros n m.
  induction m. 
  rewrite -> plus_0.
  reflexivity.
  simpl.
  rewrite <- IHm.
  rewrite <- plus_s.
  reflexivity.
Qed.

Theorem plus_associative: forall n m p, (n+m)+p = n+(m+p).
Proof.
  intros n m p.
  induction n.
  trivial.
  simpl.
  rewrite <- plus_commutative.
  rewrite <- IHn.
  rewrite <- plus_commutative.
  reflexivity.
Qed.


Lemma plus_ass_com: forall n m p, n + (m+p) = n + (p+m).
Proof.
intros.
induction n. 
simpl.
rewrite -> plus_commutative.
reflexivity.
simpl.
rewrite -> IHn.
reflexivity.
Qed.


Lemma mult_0_r: forall n, mult n 0 = 0.
Proof.
  auto.
Qed.

Lemma mult_0_l: forall n, mult 0 n = 0.
Proof.
  auto.
Qed.

Lemma mult_s_l: forall n m, mult (S m) n = n + mult m n.
Proof.
trivial.
Qed.


Lemma mult_1_r: forall n, mult n 1 = n.
Proof.
induction n.
rewrite -> mult_0_l.
reflexivity.
simpl.
rewrite IHn.
reflexivity.
Qed.


Lemma mult_s_r: forall n m, mult n (S m) = n + mult n m.
Proof.
intros n m.
induction n.
rewrite -> mult_0_l.
rewrite -> mult_0_l.
simpl.
reflexivity.
simpl.
rewrite -> IHn.
rewrite -> plus_commutative.
rewrite -> plus_associative.
rewrite -> plus_ass_com.
reflexivity.
Qed.


Theorem mult_commutative: forall n m, (mult n m) = (mult m n).
Proof.
intros.
induction n.
rewrite -> mult_0_r.
rewrite -> mult_0_l.
reflexivity.
rewrite -> mult_s_l.
rewrite -> IHn.
rewrite -> mult_s_r.
reflexivity.
Qed.



End nat_experiment.