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
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
(*i $Id: ZLt.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
Require Export ZMul.
Module ZOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
Module Export ZMulPropMod := ZMulPropFunct ZAxiomsMod.
Open Local Scope IntScope.
(* Axioms *)
Theorem Zlt_wd :
forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> (n1 < m1 <-> n2 < m2).
Proof NZlt_wd.
Theorem Zle_wd :
forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> (n1 <= m1 <-> n2 <= m2).
Proof NZle_wd.
Theorem Zmin_wd :
forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> Zmin n1 m1 == Zmin n2 m2.
Proof NZmin_wd.
Theorem Zmax_wd :
forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> Zmax n1 m1 == Zmax n2 m2.
Proof NZmax_wd.
Theorem Zlt_eq_cases : forall n m : Z, n <= m <-> n < m \/ n == m.
Proof NZlt_eq_cases.
Theorem Zlt_irrefl : forall n : Z, ~ n < n.
Proof NZlt_irrefl.
Theorem Zlt_succ_r : forall n m : Z, n < S m <-> n <= m.
Proof NZlt_succ_r.
Theorem Zmin_l : forall n m : Z, n <= m -> Zmin n m == n.
Proof NZmin_l.
Theorem Zmin_r : forall n m : Z, m <= n -> Zmin n m == m.
Proof NZmin_r.
Theorem Zmax_l : forall n m : Z, m <= n -> Zmax n m == n.
Proof NZmax_l.
Theorem Zmax_r : forall n m : Z, n <= m -> Zmax n m == m.
Proof NZmax_r.
(* Renaming theorems from NZOrder.v *)
Theorem Zlt_le_incl : forall n m : Z, n < m -> n <= m.
Proof NZlt_le_incl.
Theorem Zlt_neq : forall n m : Z, n < m -> n ~= m.
Proof NZlt_neq.
Theorem Zle_neq : forall n m : Z, n < m <-> n <= m /\ n ~= m.
Proof NZle_neq.
Theorem Zle_refl : forall n : Z, n <= n.
Proof NZle_refl.
Theorem Zlt_succ_diag_r : forall n : Z, n < S n.
Proof NZlt_succ_diag_r.
Theorem Zle_succ_diag_r : forall n : Z, n <= S n.
Proof NZle_succ_diag_r.
Theorem Zlt_0_1 : 0 < 1.
Proof NZlt_0_1.
Theorem Zle_0_1 : 0 <= 1.
Proof NZle_0_1.
Theorem Zlt_lt_succ_r : forall n m : Z, n < m -> n < S m.
Proof NZlt_lt_succ_r.
Theorem Zle_le_succ_r : forall n m : Z, n <= m -> n <= S m.
Proof NZle_le_succ_r.
Theorem Zle_succ_r : forall n m : Z, n <= S m <-> n <= m \/ n == S m.
Proof NZle_succ_r.
Theorem Zneq_succ_diag_l : forall n : Z, S n ~= n.
Proof NZneq_succ_diag_l.
Theorem Zneq_succ_diag_r : forall n : Z, n ~= S n.
Proof NZneq_succ_diag_r.
Theorem Znlt_succ_diag_l : forall n : Z, ~ S n < n.
Proof NZnlt_succ_diag_l.
Theorem Znle_succ_diag_l : forall n : Z, ~ S n <= n.
Proof NZnle_succ_diag_l.
Theorem Zle_succ_l : forall n m : Z, S n <= m <-> n < m.
Proof NZle_succ_l.
Theorem Zlt_succ_l : forall n m : Z, S n < m -> n < m.
Proof NZlt_succ_l.
Theorem Zsucc_lt_mono : forall n m : Z, n < m <-> S n < S m.
Proof NZsucc_lt_mono.
Theorem Zsucc_le_mono : forall n m : Z, n <= m <-> S n <= S m.
Proof NZsucc_le_mono.
Theorem Zlt_asymm : forall n m, n < m -> ~ m < n.
Proof NZlt_asymm.
Notation Zlt_ngt := Zlt_asymm (only parsing).
Theorem Zlt_trans : forall n m p : Z, n < m -> m < p -> n < p.
Proof NZlt_trans.
Theorem Zle_trans : forall n m p : Z, n <= m -> m <= p -> n <= p.
Proof NZle_trans.
Theorem Zle_lt_trans : forall n m p : Z, n <= m -> m < p -> n < p.
Proof NZle_lt_trans.
Theorem Zlt_le_trans : forall n m p : Z, n < m -> m <= p -> n < p.
Proof NZlt_le_trans.
Theorem Zle_antisymm : forall n m : Z, n <= m -> m <= n -> n == m.
Proof NZle_antisymm.
Theorem Zlt_1_l : forall n m : Z, 0 < n -> n < m -> 1 < m.
Proof NZlt_1_l.
(** Trichotomy, decidability, and double negation elimination *)
Theorem Zlt_trichotomy : forall n m : Z, n < m \/ n == m \/ m < n.
Proof NZlt_trichotomy.
Notation Zlt_eq_gt_cases := Zlt_trichotomy (only parsing).
Theorem Zlt_gt_cases : forall n m : Z, n ~= m <-> n < m \/ n > m.
Proof NZlt_gt_cases.
Theorem Zle_gt_cases : forall n m : Z, n <= m \/ n > m.
Proof NZle_gt_cases.
Theorem Zlt_ge_cases : forall n m : Z, n < m \/ n >= m.
Proof NZlt_ge_cases.
Theorem Zle_ge_cases : forall n m : Z, n <= m \/ n >= m.
Proof NZle_ge_cases.
(** Instances of the previous theorems for m == 0 *)
Theorem Zneg_pos_cases : forall n : Z, n ~= 0 <-> n < 0 \/ n > 0.
Proof.
intro; apply Zlt_gt_cases.
Qed.
Theorem Znonpos_pos_cases : forall n : Z, n <= 0 \/ n > 0.
Proof.
intro; apply Zle_gt_cases.
Qed.
Theorem Zneg_nonneg_cases : forall n : Z, n < 0 \/ n >= 0.
Proof.
intro; apply Zlt_ge_cases.
Qed.
Theorem Znonpos_nonneg_cases : forall n : Z, n <= 0 \/ n >= 0.
Proof.
intro; apply Zle_ge_cases.
Qed.
Theorem Zle_ngt : forall n m : Z, n <= m <-> ~ n > m.
Proof NZle_ngt.
Theorem Znlt_ge : forall n m : Z, ~ n < m <-> n >= m.
Proof NZnlt_ge.
Theorem Zlt_dec : forall n m : Z, decidable (n < m).
Proof NZlt_dec.
Theorem Zlt_dne : forall n m, ~ ~ n < m <-> n < m.
Proof NZlt_dne.
Theorem Znle_gt : forall n m : Z, ~ n <= m <-> n > m.
Proof NZnle_gt.
Theorem Zlt_nge : forall n m : Z, n < m <-> ~ n >= m.
Proof NZlt_nge.
Theorem Zle_dec : forall n m : Z, decidable (n <= m).
Proof NZle_dec.
Theorem Zle_dne : forall n m : Z, ~ ~ n <= m <-> n <= m.
Proof NZle_dne.
Theorem Znlt_succ_r : forall n m : Z, ~ m < S n <-> n < m.
Proof NZnlt_succ_r.
Theorem Zlt_exists_pred :
forall z n : Z, z < n -> exists k : Z, n == S k /\ z <= k.
Proof NZlt_exists_pred.
Theorem Zlt_succ_iter_r :
forall (n : nat) (m : Z), m < NZsucc_iter (Datatypes.S n) m.
Proof NZlt_succ_iter_r.
Theorem Zneq_succ_iter_l :
forall (n : nat) (m : Z), NZsucc_iter (Datatypes.S n) m ~= m.
Proof NZneq_succ_iter_l.
(** Stronger variant of induction with assumptions n >= 0 (n < 0)
in the induction step *)
Theorem Zright_induction :
forall A : Z -> Prop, predicate_wd Zeq A ->
forall z : Z, A z ->
(forall n : Z, z <= n -> A n -> A (S n)) ->
forall n : Z, z <= n -> A n.
Proof NZright_induction.
Theorem Zleft_induction :
forall A : Z -> Prop, predicate_wd Zeq A ->
forall z : Z, A z ->
(forall n : Z, n < z -> A (S n) -> A n) ->
forall n : Z, n <= z -> A n.
Proof NZleft_induction.
Theorem Zright_induction' :
forall A : Z -> Prop, predicate_wd Zeq A ->
forall z : Z,
(forall n : Z, n <= z -> A n) ->
(forall n : Z, z <= n -> A n -> A (S n)) ->
forall n : Z, A n.
Proof NZright_induction'.
Theorem Zleft_induction' :
forall A : Z -> Prop, predicate_wd Zeq A ->
forall z : Z,
(forall n : Z, z <= n -> A n) ->
(forall n : Z, n < z -> A (S n) -> A n) ->
forall n : Z, A n.
Proof NZleft_induction'.
Theorem Zstrong_right_induction :
forall A : Z -> Prop, predicate_wd Zeq A ->
forall z : Z,
(forall n : Z, z <= n -> (forall m : Z, z <= m -> m < n -> A m) -> A n) ->
forall n : Z, z <= n -> A n.
Proof NZstrong_right_induction.
Theorem Zstrong_left_induction :
forall A : Z -> Prop, predicate_wd Zeq A ->
forall z : Z,
(forall n : Z, n <= z -> (forall m : Z, m <= z -> S n <= m -> A m) -> A n) ->
forall n : Z, n <= z -> A n.
Proof NZstrong_left_induction.
Theorem Zstrong_right_induction' :
forall A : Z -> Prop, predicate_wd Zeq A ->
forall z : Z,
(forall n : Z, n <= z -> A n) ->
(forall n : Z, z <= n -> (forall m : Z, z <= m -> m < n -> A m) -> A n) ->
forall n : Z, A n.
Proof NZstrong_right_induction'.
Theorem Zstrong_left_induction' :
forall A : Z -> Prop, predicate_wd Zeq A ->
forall z : Z,
(forall n : Z, z <= n -> A n) ->
(forall n : Z, n <= z -> (forall m : Z, m <= z -> S n <= m -> A m) -> A n) ->
forall n : Z, A n.
Proof NZstrong_left_induction'.
Theorem Zorder_induction :
forall A : Z -> Prop, predicate_wd Zeq A ->
forall z : Z, A z ->
(forall n : Z, z <= n -> A n -> A (S n)) ->
(forall n : Z, n < z -> A (S n) -> A n) ->
forall n : Z, A n.
Proof NZorder_induction.
Theorem Zorder_induction' :
forall A : Z -> Prop, predicate_wd Zeq A ->
forall z : Z, A z ->
(forall n : Z, z <= n -> A n -> A (S n)) ->
(forall n : Z, n <= z -> A n -> A (P n)) ->
forall n : Z, A n.
Proof NZorder_induction'.
Theorem Zorder_induction_0 :
forall A : Z -> Prop, predicate_wd Zeq A ->
A 0 ->
(forall n : Z, 0 <= n -> A n -> A (S n)) ->
(forall n : Z, n < 0 -> A (S n) -> A n) ->
forall n : Z, A n.
Proof NZorder_induction_0.
Theorem Zorder_induction'_0 :
forall A : Z -> Prop, predicate_wd Zeq A ->
A 0 ->
(forall n : Z, 0 <= n -> A n -> A (S n)) ->
(forall n : Z, n <= 0 -> A n -> A (P n)) ->
forall n : Z, A n.
Proof NZorder_induction'_0.
Ltac Zinduct n := induction_maker n ltac:(apply Zorder_induction_0).
(** Elimintation principle for < *)
Theorem Zlt_ind :
forall A : Z -> Prop, predicate_wd Zeq A ->
forall n : Z, A (S n) ->
(forall m : Z, n < m -> A m -> A (S m)) -> forall m : Z, n < m -> A m.
Proof NZlt_ind.
(** Elimintation principle for <= *)
Theorem Zle_ind :
forall A : Z -> Prop, predicate_wd Zeq A ->
forall n : Z, A n ->
(forall m : Z, n <= m -> A m -> A (S m)) -> forall m : Z, n <= m -> A m.
Proof NZle_ind.
(** Well-founded relations *)
Theorem Zlt_wf : forall z : Z, well_founded (fun n m : Z => z <= n /\ n < m).
Proof NZlt_wf.
Theorem Zgt_wf : forall z : Z, well_founded (fun n m : Z => m < n /\ n <= z).
Proof NZgt_wf.
(* Theorems that are either not valid on N or have different proofs on N and Z *)
Theorem Zlt_pred_l : forall n : Z, P n < n.
Proof.
intro n; rewrite <- (Zsucc_pred n) at 2; apply Zlt_succ_diag_r.
Qed.
Theorem Zle_pred_l : forall n : Z, P n <= n.
Proof.
intro; apply Zlt_le_incl; apply Zlt_pred_l.
Qed.
Theorem Zlt_le_pred : forall n m : Z, n < m <-> n <= P m.
Proof.
intros n m; rewrite <- (Zsucc_pred m); rewrite Zpred_succ. apply Zlt_succ_r.
Qed.
Theorem Znle_pred_r : forall n : Z, ~ n <= P n.
Proof.
intro; rewrite <- Zlt_le_pred; apply Zlt_irrefl.
Qed.
Theorem Zlt_pred_le : forall n m : Z, P n < m <-> n <= m.
Proof.
intros n m; rewrite <- (Zsucc_pred n) at 2.
symmetry; apply Zle_succ_l.
Qed.
Theorem Zlt_lt_pred : forall n m : Z, n < m -> P n < m.
Proof.
intros; apply <- Zlt_pred_le; now apply Zlt_le_incl.
Qed.
Theorem Zle_le_pred : forall n m : Z, n <= m -> P n <= m.
Proof.
intros; apply Zlt_le_incl; now apply <- Zlt_pred_le.
Qed.
Theorem Zlt_pred_lt : forall n m : Z, n < P m -> n < m.
Proof.
intros n m H; apply Zlt_trans with (P m); [assumption | apply Zlt_pred_l].
Qed.
Theorem Zle_pred_lt : forall n m : Z, n <= P m -> n <= m.
Proof.
intros; apply Zlt_le_incl; now apply <- Zlt_le_pred.
Qed.
Theorem Zpred_lt_mono : forall n m : Z, n < m <-> P n < P m.
Proof.
intros; rewrite Zlt_le_pred; symmetry; apply Zlt_pred_le.
Qed.
Theorem Zpred_le_mono : forall n m : Z, n <= m <-> P n <= P m.
Proof.
intros; rewrite <- Zlt_pred_le; now rewrite Zlt_le_pred.
Qed.
Theorem Zlt_succ_lt_pred : forall n m : Z, S n < m <-> n < P m.
Proof.
intros n m; now rewrite (Zpred_lt_mono (S n) m), Zpred_succ.
Qed.
Theorem Zle_succ_le_pred : forall n m : Z, S n <= m <-> n <= P m.
Proof.
intros n m; now rewrite (Zpred_le_mono (S n) m), Zpred_succ.
Qed.
Theorem Zlt_pred_lt_succ : forall n m : Z, P n < m <-> n < S m.
Proof.
intros; rewrite Zlt_pred_le; symmetry; apply Zlt_succ_r.
Qed.
Theorem Zle_pred_lt_succ : forall n m : Z, P n <= m <-> n <= S m.
Proof.
intros n m; now rewrite (Zpred_le_mono n (S m)), Zpred_succ.
Qed.
Theorem Zneq_pred_l : forall n : Z, P n ~= n.
Proof.
intro; apply Zlt_neq; apply Zlt_pred_l.
Qed.
Theorem Zlt_n1_r : forall n m : Z, n < m -> m < 0 -> n < -1.
Proof.
intros n m H1 H2. apply -> Zlt_le_pred in H2.
setoid_replace (P 0) with (-1) in H2. now apply NZlt_le_trans with m.
apply <- Zeq_opp_r. now rewrite Zopp_pred, Zopp_0.
Qed.
End ZOrderPropFunct.
|
