Section nat_experiment Variable nat Definition two Definition plus_two

Section nat_experiment.

Variable a:nat.

Definition two := S(S(0)).

Definition plus_two(n:nat):nat  := S(S(n)).

Definition plus_four(n:nat):nat  := S(S(S(S(n)))).

Lemma appl : plus_two(plus_two(a)) = plus_four(a).
Proof.
trivial.
Qed.


Lemma s_appl : S(plus_two(plus_two(a))) = S(plus_four(a)).
Proof.
trivial.
Qed.

Lemma dummy : plus_two(two) = plus_four(0).
Proof.
trivial.
Qed.

Lemma assoc : S(plus_two(a)) = plus_two(S(a)).
Proof.
trivial.
Qed.


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.
   

End nat_experiment.