1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
8
(* Evgeny Makarov, INRIA, 2007 *)
9
(************************************************************************)
11
(*i $Id: ZAdd.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
15
Module ZAddPropFunct (Import ZAxiomsMod : ZAxiomsSig).
16
Module Export ZBasePropMod := ZBasePropFunct ZAxiomsMod.
17
Open Local Scope IntScope.
20
forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> n1 + m1 == n2 + m2.
23
Theorem Zadd_0_l : forall n : Z, 0 + n == n.
26
Theorem Zadd_succ_l : forall n m : Z, (S n) + m == S (n + m).
29
Theorem Zsub_0_r : forall n : Z, n - 0 == n.
32
Theorem Zsub_succ_r : forall n m : Z, n - (S m) == P (n - m).
35
Theorem Zopp_0 : - 0 == 0.
38
Theorem Zopp_succ : forall n : Z, - (S n) == P (- n).
41
(* Theorems that are valid for both natural numbers and integers *)
43
Theorem Zadd_0_r : forall n : Z, n + 0 == n.
46
Theorem Zadd_succ_r : forall n m : Z, n + S m == S (n + m).
49
Theorem Zadd_comm : forall n m : Z, n + m == m + n.
52
Theorem Zadd_assoc : forall n m p : Z, n + (m + p) == (n + m) + p.
55
Theorem Zadd_shuffle1 : forall n m p q : Z, (n + m) + (p + q) == (n + p) + (m + q).
58
Theorem Zadd_shuffle2 : forall n m p q : Z, (n + m) + (p + q) == (n + q) + (m + p).
61
Theorem Zadd_1_l : forall n : Z, 1 + n == S n.
64
Theorem Zadd_1_r : forall n : Z, n + 1 == S n.
67
Theorem Zadd_cancel_l : forall n m p : Z, p + n == p + m <-> n == m.
70
Theorem Zadd_cancel_r : forall n m p : Z, n + p == m + p <-> n == m.
73
(* Theorems that are either not valid on N or have different proofs on N and Z *)
75
Theorem Zadd_pred_l : forall n m : Z, P n + m == P (n + m).
78
rewrite <- (Zsucc_pred n) at 2.
79
rewrite Zadd_succ_l. now rewrite Zpred_succ.
82
Theorem Zadd_pred_r : forall n m : Z, n + P m == P (n + m).
84
intros n m; rewrite (Zadd_comm n (P m)), (Zadd_comm n m);
88
Theorem Zadd_opp_r : forall n m : Z, n + (- m) == n - m.
91
rewrite Zopp_0; rewrite Zsub_0_r; now rewrite Zadd_0_r.
92
intro m. rewrite Zopp_succ, Zsub_succ_r, Zadd_pred_r; now rewrite Zpred_inj_wd.
95
Theorem Zsub_0_l : forall n : Z, 0 - n == - n.
97
intro n; rewrite <- Zadd_opp_r; now rewrite Zadd_0_l.
100
Theorem Zsub_succ_l : forall n m : Z, S n - m == S (n - m).
102
intros n m; do 2 rewrite <- Zadd_opp_r; now rewrite Zadd_succ_l.
105
Theorem Zsub_pred_l : forall n m : Z, P n - m == P (n - m).
107
intros n m. rewrite <- (Zsucc_pred n) at 2.
108
rewrite Zsub_succ_l; now rewrite Zpred_succ.
111
Theorem Zsub_pred_r : forall n m : Z, n - (P m) == S (n - m).
113
intros n m. rewrite <- (Zsucc_pred m) at 2.
114
rewrite Zsub_succ_r; now rewrite Zsucc_pred.
117
Theorem Zopp_pred : forall n : Z, - (P n) == S (- n).
119
intro n. rewrite <- (Zsucc_pred n) at 2.
120
rewrite Zopp_succ. now rewrite Zsucc_pred.
123
Theorem Zsub_diag : forall n : Z, n - n == 0.
126
now rewrite Zsub_0_r.
127
intro n. rewrite Zsub_succ_r, Zsub_succ_l; now rewrite Zpred_succ.
130
Theorem Zadd_opp_diag_l : forall n : Z, - n + n == 0.
132
intro n; now rewrite Zadd_comm, Zadd_opp_r, Zsub_diag.
135
Theorem Zadd_opp_diag_r : forall n : Z, n + (- n) == 0.
137
intro n; rewrite Zadd_comm; apply Zadd_opp_diag_l.
140
Theorem Zadd_opp_l : forall n m : Z, - m + n == n - m.
142
intros n m; rewrite <- Zadd_opp_r; now rewrite Zadd_comm.
145
Theorem Zadd_sub_assoc : forall n m p : Z, n + (m - p) == (n + m) - p.
147
intros n m p; do 2 rewrite <- Zadd_opp_r; now rewrite Zadd_assoc.
150
Theorem Zopp_involutive : forall n : Z, - (- n) == n.
153
now do 2 rewrite Zopp_0.
154
intro n. rewrite Zopp_succ, Zopp_pred; now rewrite Zsucc_inj_wd.
157
Theorem Zopp_add_distr : forall n m : Z, - (n + m) == - n + (- m).
159
intros n m; NZinduct n.
160
rewrite Zopp_0; now do 2 rewrite Zadd_0_l.
161
intro n. rewrite Zadd_succ_l; do 2 rewrite Zopp_succ; rewrite Zadd_pred_l.
162
now rewrite Zpred_inj_wd.
165
Theorem Zopp_sub_distr : forall n m : Z, - (n - m) == - n + m.
167
intros n m; rewrite <- Zadd_opp_r, Zopp_add_distr.
168
now rewrite Zopp_involutive.
171
Theorem Zopp_inj : forall n m : Z, - n == - m -> n == m.
173
intros n m H. apply Zopp_wd in H. now do 2 rewrite Zopp_involutive in H.
176
Theorem Zopp_inj_wd : forall n m : Z, - n == - m <-> n == m.
178
intros n m; split; [apply Zopp_inj | apply Zopp_wd].
181
Theorem Zeq_opp_l : forall n m : Z, - n == m <-> n == - m.
183
intros n m. now rewrite <- (Zopp_inj_wd (- n) m), Zopp_involutive.
186
Theorem Zeq_opp_r : forall n m : Z, n == - m <-> - n == m.
188
symmetry; apply Zeq_opp_l.
191
Theorem Zsub_add_distr : forall n m p : Z, n - (m + p) == (n - m) - p.
193
intros n m p; rewrite <- Zadd_opp_r, Zopp_add_distr, Zadd_assoc.
194
now do 2 rewrite Zadd_opp_r.
197
Theorem Zsub_sub_distr : forall n m p : Z, n - (m - p) == (n - m) + p.
199
intros n m p; rewrite <- Zadd_opp_r, Zopp_sub_distr, Zadd_assoc.
200
now rewrite Zadd_opp_r.
203
Theorem sub_opp_l : forall n m : Z, - n - m == - m - n.
205
intros n m. do 2 rewrite <- Zadd_opp_r. now rewrite Zadd_comm.
208
Theorem Zsub_opp_r : forall n m : Z, n - (- m) == n + m.
210
intros n m; rewrite <- Zadd_opp_r; now rewrite Zopp_involutive.
213
Theorem Zadd_sub_swap : forall n m p : Z, n + m - p == n - p + m.
215
intros n m p. rewrite <- Zadd_sub_assoc, <- (Zadd_opp_r n p), <- Zadd_assoc.
216
now rewrite Zadd_opp_l.
219
Theorem Zsub_cancel_l : forall n m p : Z, n - m == n - p <-> m == p.
221
intros n m p. rewrite <- (Zadd_cancel_l (n - m) (n - p) (- n)).
222
do 2 rewrite Zadd_sub_assoc. rewrite Zadd_opp_diag_l; do 2 rewrite Zsub_0_l.
226
Theorem Zsub_cancel_r : forall n m p : Z, n - p == m - p <-> n == m.
229
stepl (n - p + p == m - p + p) by apply Zadd_cancel_r.
230
now do 2 rewrite <- Zsub_sub_distr, Zsub_diag, Zsub_0_r.
233
(* The next several theorems are devoted to moving terms from one side of
234
an equation to the other. The name contains the operation in the original
235
equation (add or sub) and the indication whether the left or right term
238
Theorem Zadd_move_l : forall n m p : Z, n + m == p <-> m == p - n.
241
stepl (n + m - n == p - n) by apply Zsub_cancel_r.
242
now rewrite Zadd_comm, <- Zadd_sub_assoc, Zsub_diag, Zadd_0_r.
245
Theorem Zadd_move_r : forall n m p : Z, n + m == p <-> n == p - m.
247
intros n m p; rewrite Zadd_comm; now apply Zadd_move_l.
250
(* The two theorems above do not allow rewriting subformulas of the form
251
n - m == p to n == p + m since subtraction is in the right-hand side of
252
the equation. Hence the following two theorems. *)
254
Theorem Zsub_move_l : forall n m p : Z, n - m == p <-> - m == p - n.
256
intros n m p; rewrite <- (Zadd_opp_r n m); apply Zadd_move_l.
259
Theorem Zsub_move_r : forall n m p : Z, n - m == p <-> n == p + m.
261
intros n m p; rewrite <- (Zadd_opp_r n m). now rewrite Zadd_move_r, Zsub_opp_r.
264
Theorem Zadd_move_0_l : forall n m : Z, n + m == 0 <-> m == - n.
266
intros n m; now rewrite Zadd_move_l, Zsub_0_l.
269
Theorem Zadd_move_0_r : forall n m : Z, n + m == 0 <-> n == - m.
271
intros n m; now rewrite Zadd_move_r, Zsub_0_l.
274
Theorem Zsub_move_0_l : forall n m : Z, n - m == 0 <-> - m == - n.
276
intros n m. now rewrite Zsub_move_l, Zsub_0_l.
279
Theorem Zsub_move_0_r : forall n m : Z, n - m == 0 <-> n == m.
281
intros n m. now rewrite Zsub_move_r, Zadd_0_l.
284
(* The following section is devoted to cancellation of like terms. The name
285
includes the first operator and the position of the term being canceled. *)
287
Theorem Zadd_simpl_l : forall n m : Z, n + m - n == m.
289
intros; now rewrite Zadd_sub_swap, Zsub_diag, Zadd_0_l.
292
Theorem Zadd_simpl_r : forall n m : Z, n + m - m == n.
294
intros; now rewrite <- Zadd_sub_assoc, Zsub_diag, Zadd_0_r.
297
Theorem Zsub_simpl_l : forall n m : Z, - n - m + n == - m.
299
intros; now rewrite <- Zadd_sub_swap, Zadd_opp_diag_l, Zsub_0_l.
302
Theorem Zsub_simpl_r : forall n m : Z, n - m + m == n.
304
intros; now rewrite <- Zsub_sub_distr, Zsub_diag, Zsub_0_r.
307
(* Now we have two sums or differences; the name includes the two operators
308
and the position of the terms being canceled *)
310
Theorem Zadd_add_simpl_l_l : forall n m p : Z, (n + m) - (n + p) == m - p.
312
intros n m p. now rewrite (Zadd_comm n m), <- Zadd_sub_assoc,
313
Zsub_add_distr, Zsub_diag, Zsub_0_l, Zadd_opp_r.
316
Theorem Zadd_add_simpl_l_r : forall n m p : Z, (n + m) - (p + n) == m - p.
318
intros n m p. rewrite (Zadd_comm p n); apply Zadd_add_simpl_l_l.
321
Theorem Zadd_add_simpl_r_l : forall n m p : Z, (n + m) - (m + p) == n - p.
323
intros n m p. rewrite (Zadd_comm n m); apply Zadd_add_simpl_l_l.
326
Theorem Zadd_add_simpl_r_r : forall n m p : Z, (n + m) - (p + m) == n - p.
328
intros n m p. rewrite (Zadd_comm p m); apply Zadd_add_simpl_r_l.
331
Theorem Zsub_add_simpl_r_l : forall n m p : Z, (n - m) + (m + p) == n + p.
333
intros n m p. now rewrite <- Zsub_sub_distr, Zsub_add_distr, Zsub_diag,
334
Zsub_0_l, Zsub_opp_r.
337
Theorem Zsub_add_simpl_r_r : forall n m p : Z, (n - m) + (p + m) == n + p.
339
intros n m p. rewrite (Zadd_comm p m); apply Zsub_add_simpl_r_l.
342
(* Of course, there are many other variants *)
added
removed
theories/Numbers/Integer/Abstract/ZAdd.v
