Section nat_experiment Variable nat Definition two Definition plus_two

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
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.