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.