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
|
Require Export Ring.
Require Export ZPlus.
Module ZTimesPropFunct (Import ZAxiomsMod : ZAxiomsSig).
Module Export ZPlusPropMod := ZPlusPropFunct ZAxiomsMod.
Open Local Scope IntScope.
Theorem Ztimes_0_r : forall n : Z, n * 0 == 0.
Proof NZtimes_0_r.
Theorem Ztimes_succ_r : forall n m : Z, n * (S m) == n * m + n.
Proof NZtimes_succ_r.
(** Theorems that are valid for both natural numbers and integers *)
Theorem Ztimes_0_l : forall n : Z, 0 * n == 0.
Proof NZtimes_0_l.
Theorem Ztimes_succ_l : forall n m : Z, (S n) * m == n * m + m.
Proof NZtimes_succ_l.
Theorem Ztimes_comm : forall n m : Z, n * m == m * n.
Proof NZtimes_comm.
Theorem Ztimes_plus_distr_r : forall n m p : Z, (n + m) * p == n * p + m * p.
Proof NZtimes_plus_distr_r.
Theorem Ztimes_plus_distr_l : forall n m p : Z, n * (m + p) == n * m + n * p.
Proof NZtimes_plus_distr_l.
Theorem Ztimes_assoc : forall n m p : Z, n * (m * p) == (n * m) * p.
Proof NZtimes_assoc.
Theorem Ztimes_1_l : forall n : Z, 1 * n == n.
Proof NZtimes_1_l.
Theorem Ztimes_1_r : forall n : Z, n * 1 == n.
Proof NZtimes_1_r.
(* The following two theorems are true in an ordered ring,
but since they don't mention order, we'll put them here *)
Theorem Ztimes_eq_0 : forall n m : Z, n * m == 0 -> n == 0 \/ m == 0.
Proof NZtimes_eq_0.
Theorem Ztimes_neq_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
Proof NZtimes_neq_0.
(** Z forms a ring *)
Lemma Zring : ring_theory 0 1 NZplus NZtimes NZminus Zopp NZeq.
Proof.
constructor.
exact Zplus_0_l.
exact Zplus_comm.
exact Zplus_assoc.
exact Ztimes_1_l.
exact Ztimes_comm.
exact Ztimes_assoc.
exact Ztimes_plus_distr_r.
intros; now rewrite Zplus_opp_minus.
exact Zplus_opp_r.
Qed.
Add Ring ZR : Zring.
(** Theorems that are either not valid on N or have different proofs on N and Z *)
Theorem Ztimes_pred_r : forall n m : Z, n * (P m) == n * m - n.
Proof.
intros n m.
pattern m at 2; qsetoid_rewrite <- (Zsucc_pred m).
now rewrite Ztimes_succ_r, <- Zplus_minus_assoc, Zminus_diag, Zplus_0_r.
Qed.
Theorem Ztimes_pred_l : forall n m : Z, (P n) * m == n * m - m.
Proof.
intros n m; rewrite (Ztimes_comm (P n) m), (Ztimes_comm n m). apply Ztimes_pred_r.
Qed.
Theorem Ztimes_opp_r : forall n m : Z, n * (- m) == - (n * m).
Proof.
intros; ring.
Qed.
Theorem Ztimes_opp_l : forall n m : Z, (- n) * m == - (n * m).
Proof.
intros; ring.
Qed.
Theorem Ztimes_opp_opp : forall n m : Z, (- n) * (- m) == n * m.
Proof.
intros; ring.
Qed.
Theorem Ztimes_minus_distr_r : forall n m p : Z, n * (m - p) == n * m - n * p.
Proof.
intros; ring.
Qed.
Theorem Ztimes_minus_distr_l : forall n m p : Z, (n - m) * p == n * p - m * p.
Proof.
intros; ring.
Qed.
End ZTimesPropFunct.
|
