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
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
|
Require Export ZBase.
Module ZPlusPropFunct (Import ZAxiomsMod : ZAxiomsSig).
Module Export ZBasePropMod := ZBasePropFunct ZAxiomsMod.
Open Local Scope NatIntScope.
Theorem Zplus_0_l : forall n : Z, 0 + n == n.
Proof NZplus_0_l.
Theorem Zplus_succ_l : forall n m : Z, (S n) + m == S (n + m).
Proof NZplus_succ_l.
Theorem Zminus_0_r : forall n : Z, n - 0 == n.
Proof NZminus_0_r.
Theorem Zminus_succ_r : forall n m : Z, n - (S m) == P (n - m).
Proof NZminus_succ_r.
Theorem Zopp_0 : - 0 == 0.
Proof Zopp_0.
Theorem Zopp_succ : forall n : Z, - (S n) == P (- n).
Proof Zopp_succ.
(** Theorems that are valid for both natural numbers and integers *)
Theorem Zplus_0_r : forall n : Z, n + 0 == n.
Proof NZplus_0_r.
Theorem Zplus_succ_r : forall n m : Z, n + S m == S (n + m).
Proof NZplus_succ_r.
Theorem Zplus_comm : forall n m : Z, n + m == m + n.
Proof NZplus_comm.
Theorem Zplus_assoc : forall n m p : Z, n + (m + p) == (n + m) + p.
Proof NZplus_assoc.
Theorem Zplus_shuffle1 : forall n m p q : Z, (n + m) + (p + q) == (n + p) + (m + q).
Proof NZplus_shuffle1.
Theorem Zplus_shuffle2 : forall n m p q : Z, (n + m) + (p + q) == (n + q) + (m + p).
Proof NZplus_shuffle2.
Theorem Zplus_1_l : forall n : Z, 1 + n == S n.
Proof NZplus_1_l.
Theorem Zplus_1_r : forall n : Z, n + 1 == S n.
Proof NZplus_1_r.
Theorem Zplus_cancel_l : forall n m p : Z, p + n == p + m <-> n == m.
Proof NZplus_cancel_l.
Theorem Zplus_cancel_r : forall n m p : Z, n + p == m + p <-> n == m.
Proof NZplus_cancel_r.
(** Theorems that are either not valid on N or have different proofs on N and Z *)
Theorem Zplus_pred_l : forall n m : Z, P n + m == P (n + m).
Proof.
intros n m.
pattern n at 2. qsetoid_rewrite <- (Zsucc_pred n).
rewrite Zplus_succ_l. now rewrite Zpred_succ.
Qed.
Theorem Zplus_pred_r : forall n m : Z, n + P m == P (n + m).
Proof.
intros n m; rewrite (Zplus_comm n (P m)), (Zplus_comm n m);
apply Zplus_pred_l.
Qed.
Theorem Zplus_opp_minus : forall n m : Z, n + (- m) == n - m.
Proof.
NZinduct m.
rewrite Zopp_0; rewrite Zminus_0_r; now rewrite Zplus_0_r.
intro m. rewrite Zopp_succ, Zminus_succ_r, Zplus_pred_r; now rewrite Zpred_inj_wd.
Qed.
Theorem Zminus_0_l : forall n : Z, 0 - n == - n.
Proof.
intro n; rewrite <- Zplus_opp_minus; now rewrite Zplus_0_l.
Qed.
Theorem Zminus_succ_l : forall n m : Z, S n - m == S (n - m).
Proof.
intros n m; do 2 rewrite <- Zplus_opp_minus; now rewrite Zplus_succ_l.
Qed.
Theorem Zminus_pred_l : forall n m : Z, P n - m == P (n - m).
Proof.
intros n m. pattern n at 2; qsetoid_rewrite <- (Zsucc_pred n).
rewrite Zminus_succ_l; now rewrite Zpred_succ.
Qed.
Theorem Zminus_pred_r : forall n m : Z, n - (P m) == S (n - m).
Proof.
intros n m. pattern m at 2; qsetoid_rewrite <- (Zsucc_pred m).
rewrite Zminus_succ_r; now rewrite Zsucc_pred.
Qed.
Theorem Zopp_pred : forall n : Z, - (P n) == S (- n).
Proof.
intro n. pattern n at 2; qsetoid_rewrite <- (Zsucc_pred n).
rewrite Zopp_succ. now rewrite Zsucc_pred.
Qed.
Theorem Zminus_diag : forall n : Z, n - n == 0.
Proof.
NZinduct n.
now rewrite Zminus_0_r.
intro n. rewrite Zminus_succ_r, Zminus_succ_l; now rewrite Zpred_succ.
Qed.
Theorem Zplus_opp_r : forall n : Z, n + (- n) == 0.
Proof.
intro n; rewrite Zplus_opp_minus; now rewrite Zminus_diag.
Qed.
Theorem Zplus_opp_l : forall n : Z, - n + n == 0.
Proof.
intro n; rewrite Zplus_comm; apply Zplus_opp_r.
Qed.
Theorem Zminus_swap : forall n m : Z, - m + n == n - m.
Proof.
intros n m; rewrite <- Zplus_opp_minus; now rewrite Zplus_comm.
Qed.
Theorem Zplus_minus_assoc : forall n m p : Z, n + (m - p) == (n + m) - p.
Proof.
intros n m p; do 2 rewrite <- Zplus_opp_minus; now rewrite Zplus_assoc.
Qed.
Theorem Zopp_involutive : forall n : Z, - (- n) == n.
Proof.
NZinduct n.
now do 2 rewrite Zopp_0.
intro n. rewrite Zopp_succ, Zopp_pred; now rewrite Zsucc_inj_wd.
Qed.
Theorem Zopp_plus_distr : forall n m : Z, - (n + m) == - n + (- m).
Proof.
intros n m; NZinduct n.
rewrite Zopp_0; now do 2 rewrite Zplus_0_l.
intro n. rewrite Zplus_succ_l; do 2 rewrite Zopp_succ; rewrite Zplus_pred_l.
now rewrite Zpred_inj_wd.
Qed.
Theorem Zopp_minus_distr : forall n m : Z, - (n - m) == - n + m.
Proof.
intros n m; rewrite <- Zplus_opp_minus, Zopp_plus_distr.
now rewrite Zopp_involutive.
Qed.
Theorem Zopp_inj : forall n m : Z, - n == - m -> n == m.
Proof.
intros n m H. apply Zopp_wd in H. now do 2 rewrite Zopp_involutive in H.
Qed.
Theorem Zopp_inj_wd : forall n m : Z, - n == - m <-> n == m.
Proof.
intros n m; split; [apply Zopp_inj | apply Zopp_wd].
Qed.
Theorem Zminus_plus_distr : forall n m p : Z, n - (m + p) == (n - m) - p.
Proof.
intros n m p; rewrite <- Zplus_opp_minus, Zopp_plus_distr, Zplus_assoc.
now do 2 rewrite Zplus_opp_minus.
Qed.
Theorem Zminus_minus_distr : forall n m p : Z, n - (m - p) == (n - m) + p.
Proof.
intros n m p; rewrite <- Zplus_opp_minus, Zopp_minus_distr, Zplus_assoc.
now rewrite Zplus_opp_minus.
Qed.
Theorem Zminus_opp : forall n m : Z, n - (- m) == n + m.
Proof.
intros n m; rewrite <- Zplus_opp_minus; now rewrite Zopp_involutive.
Qed.
Theorem Zplus_minus_swap : forall n m p : Z, n + m - p == n - p + m.
Proof.
intros n m p. rewrite <- Zplus_minus_assoc, <- (Zplus_opp_minus n p), <- Zplus_assoc.
now rewrite Zminus_swap.
Qed.
Theorem Zminus_plus_diag : forall n m : Z, n - m + m == n.
Proof.
intros; rewrite <- Zplus_minus_swap; rewrite <- Zplus_minus_assoc;
rewrite Zminus_diag; now rewrite Zplus_0_r.
Qed.
Theorem Zplus_minus_diag : forall n m : Z, n + m - m == n.
Proof.
intros; rewrite <- Zplus_minus_assoc; rewrite Zminus_diag; now rewrite Zplus_0_r.
Qed.
Theorem Zplus_minus_eq_l : forall n m p : Z, m + p == n <-> n - m == p.
Proof.
intros n m p.
stepl (-m + (m + p) == -m + n) by apply Zplus_cancel_l.
stepr (p == n - m) by now split.
rewrite Zplus_assoc, Zplus_opp_l, Zplus_0_l. now rewrite Zminus_swap.
Qed.
Theorem Zplus_minus_eq_r : forall n m p : Z, m + p == n <-> n - p == m.
Proof.
intros n m p; rewrite Zplus_comm; now apply Zplus_minus_eq_l.
Qed.
Theorem Zminus_eq : forall n m : Z, n - m == 0 <-> n == m.
Proof.
intros n m. rewrite <- Zplus_minus_eq_l, Zplus_0_r; now split.
Qed.
End ZPlusPropFunct.
|
