123 lines
2.0 KiB
Coq
123 lines
2.0 KiB
Coq
Lemma add_n_0: forall n:nat, n+0 = n.
|
|
Proof.
|
|
intro n.
|
|
induction n.
|
|
- reflexivity.
|
|
- simpl.
|
|
rewrite IHn.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Lemma add_nSm: forall n m:nat,
|
|
n + S m = S (n + m).
|
|
Proof.
|
|
intros n m.
|
|
induction n.
|
|
- reflexivity.
|
|
- simpl.
|
|
rewrite <- IHn.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem plus_comm : forall a b:nat,
|
|
a + b = b + a.
|
|
Proof.
|
|
intros a b.
|
|
induction a.
|
|
- rewrite add_n_0.
|
|
reflexivity.
|
|
- simpl.
|
|
rewrite add_nSm.
|
|
rewrite <- IHa.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem plus_assoc : forall a b c:nat,
|
|
a + (b + c) = (a + b) + c.
|
|
Proof.
|
|
intros a b c.
|
|
induction a.
|
|
- reflexivity.
|
|
- simpl.
|
|
rewrite IHa.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Lemma mult_n_0: forall n:nat, n*0 = 0.
|
|
Proof.
|
|
intros n.
|
|
induction n.
|
|
- reflexivity.
|
|
- simpl.
|
|
rewrite IHn.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Lemma mult_nSm: forall n m:nat,
|
|
n * S m = n + (n * m).
|
|
Proof.
|
|
intros n m.
|
|
induction n.
|
|
- reflexivity.
|
|
- simpl.
|
|
rewrite IHn.
|
|
SearchRewrite ((_ + _) + _).
|
|
rewrite plus_assoc.
|
|
rewrite (plus_comm m n).
|
|
rewrite <- plus_assoc.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem mult_comm: forall a b:nat,
|
|
a * b = b * a.
|
|
Proof.
|
|
intros a b.
|
|
induction a.
|
|
- rewrite mult_n_0.
|
|
reflexivity.
|
|
- simpl.
|
|
rewrite mult_nSm.
|
|
rewrite <- IHa.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem mult_distr_l : forall a b c:nat,
|
|
a * (b + c) = (a * b) + (a * c).
|
|
Proof.
|
|
intros a b c.
|
|
induction a.
|
|
- reflexivity.
|
|
- simpl.
|
|
rewrite IHa.
|
|
rewrite plus_assoc.
|
|
rewrite plus_assoc.
|
|
rewrite <- (plus_assoc b c (a*b)).
|
|
rewrite (plus_comm c (a*b)).
|
|
rewrite plus_assoc.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem mult_distr_r : forall a b c:nat,
|
|
(a + b) * c = (a * c) + (b * c).
|
|
Proof.
|
|
intros a b c.
|
|
induction a.
|
|
- reflexivity.
|
|
- simpl.
|
|
rewrite <- (plus_assoc c (a*c) (b*c)).
|
|
rewrite <- IHa.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem mult_assoc : forall a b c:nat,
|
|
a * (b * c) = (a * b) * c.
|
|
Proof.
|
|
intros a b c.
|
|
induction a.
|
|
- reflexivity.
|
|
- simpl.
|
|
rewrite IHa.
|
|
rewrite mult_distr_r.
|
|
reflexivity.
|
|
Qed.
|