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.