← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to theories/Numbers/Integer/Abstract/ZLt.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
theories/Numbers/Integer/Abstract/ZLt.v
 
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
(************************************************************************)
 
10
 
 
11
(*i $Id: ZLt.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
 
12
 
 
13
Require Export ZMul.
 
14
 
 
15
Module ZOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
 
16
Module Export ZMulPropMod := ZMulPropFunct ZAxiomsMod.
 
17
Open Local Scope IntScope.
 
18
 
 
19
(* Axioms *)
 
20
 
 
21
Theorem Zlt_wd :
 
22
  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> (n1 < m1 <-> n2 < m2).
 
23
Proof NZlt_wd.
 
24
 
 
25
Theorem Zle_wd :
 
26
  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> (n1 <= m1 <-> n2 <= m2).
 
27
Proof NZle_wd.
 
28
 
 
29
Theorem Zmin_wd :
 
30
  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> Zmin n1 m1 == Zmin n2 m2.
 
31
Proof NZmin_wd.
 
32
 
 
33
Theorem Zmax_wd :
 
34
  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> Zmax n1 m1 == Zmax n2 m2.
 
35
Proof NZmax_wd.
 
36
 
 
37
Theorem Zlt_eq_cases : forall n m : Z, n <= m <-> n < m \/ n == m.
 
38
Proof NZlt_eq_cases.
 
39
 
 
40
Theorem Zlt_irrefl : forall n : Z, ~ n < n.
 
41
Proof NZlt_irrefl.
 
42
 
 
43
Theorem Zlt_succ_r : forall n m : Z, n < S m <-> n <= m.
 
44
Proof NZlt_succ_r.
 
45
 
 
46
Theorem Zmin_l : forall n m : Z, n <= m -> Zmin n m == n.
 
47
Proof NZmin_l.
 
48
 
 
49
Theorem Zmin_r : forall n m : Z, m <= n -> Zmin n m == m.
 
50
Proof NZmin_r.
 
51
 
 
52
Theorem Zmax_l : forall n m : Z, m <= n -> Zmax n m == n.
 
53
Proof NZmax_l.
 
54
 
 
55
Theorem Zmax_r : forall n m : Z, n <= m -> Zmax n m == m.
 
56
Proof NZmax_r.
 
57
 
 
58
(* Renaming theorems from NZOrder.v *)
 
59
 
 
60
Theorem Zlt_le_incl : forall n m : Z, n < m -> n <= m.
 
61
Proof NZlt_le_incl.
 
62
 
 
63
Theorem Zlt_neq : forall n m : Z, n < m -> n ~= m.
 
64
Proof NZlt_neq.
 
65
 
 
66
Theorem Zle_neq : forall n m : Z, n < m <-> n <= m /\ n ~= m.
 
67
Proof NZle_neq.
 
68
 
 
69
Theorem Zle_refl : forall n : Z, n <= n.
 
70
Proof NZle_refl.
 
71
 
 
72
Theorem Zlt_succ_diag_r : forall n : Z, n < S n.
 
73
Proof NZlt_succ_diag_r.
 
74
 
 
75
Theorem Zle_succ_diag_r : forall n : Z, n <= S n.
 
76
Proof NZle_succ_diag_r.
 
77
 
 
78
Theorem Zlt_0_1 : 0 < 1.
 
79
Proof NZlt_0_1.
 
80
 
 
81
Theorem Zle_0_1 : 0 <= 1.
 
82
Proof NZle_0_1.
 
83
 
 
84
Theorem Zlt_lt_succ_r : forall n m : Z, n < m -> n < S m.
 
85
Proof NZlt_lt_succ_r.
 
86
 
 
87
Theorem Zle_le_succ_r : forall n m : Z, n <= m -> n <= S m.
 
88
Proof NZle_le_succ_r.
 
89
 
 
90
Theorem Zle_succ_r : forall n m : Z, n <= S m <-> n <= m \/ n == S m.
 
91
Proof NZle_succ_r.
 
92
 
 
93
Theorem Zneq_succ_diag_l : forall n : Z, S n ~= n.
 
94
Proof NZneq_succ_diag_l.
 
95
 
 
96
Theorem Zneq_succ_diag_r : forall n : Z, n ~= S n.
 
97
Proof NZneq_succ_diag_r.
 
98
 
 
99
Theorem Znlt_succ_diag_l : forall n : Z, ~ S n < n.
 
100
Proof NZnlt_succ_diag_l.
 
101
 
 
102
Theorem Znle_succ_diag_l : forall n : Z, ~ S n <= n.
 
103
Proof NZnle_succ_diag_l.
 
104
 
 
105
Theorem Zle_succ_l : forall n m : Z, S n <= m <-> n < m.
 
106
Proof NZle_succ_l.
 
107
 
 
108
Theorem Zlt_succ_l : forall n m : Z, S n < m -> n < m.
 
109
Proof NZlt_succ_l.
 
110
 
 
111
Theorem Zsucc_lt_mono : forall n m : Z, n < m <-> S n < S m.
 
112
Proof NZsucc_lt_mono.
 
113
 
 
114
Theorem Zsucc_le_mono : forall n m : Z, n <= m <-> S n <= S m.
 
115
Proof NZsucc_le_mono.
 
116
 
 
117
Theorem Zlt_asymm : forall n m, n < m -> ~ m < n.
 
118
Proof NZlt_asymm.
 
119
 
 
120
Notation Zlt_ngt := Zlt_asymm (only parsing).
 
121
 
 
122
Theorem Zlt_trans : forall n m p : Z, n < m -> m < p -> n < p.
 
123
Proof NZlt_trans.
 
124
 
 
125
Theorem Zle_trans : forall n m p : Z, n <= m -> m <= p -> n <= p.
 
126
Proof NZle_trans.
 
127
 
 
128
Theorem Zle_lt_trans : forall n m p : Z, n <= m -> m < p -> n < p.
 
129
Proof NZle_lt_trans.
 
130
 
 
131
Theorem Zlt_le_trans : forall n m p : Z, n < m -> m <= p -> n < p.
 
132
Proof NZlt_le_trans.
 
133
 
 
134
Theorem Zle_antisymm : forall n m : Z, n <= m -> m <= n -> n == m.
 
135
Proof NZle_antisymm.
 
136
 
 
137
Theorem Zlt_1_l : forall n m : Z, 0 < n -> n < m -> 1 < m.
 
138
Proof NZlt_1_l.
 
139
 
 
140
(** Trichotomy, decidability, and double negation elimination *)
 
141
 
 
142
Theorem Zlt_trichotomy : forall n m : Z,  n < m \/ n == m \/ m < n.
 
143
Proof NZlt_trichotomy.
 
144
 
 
145
Notation Zlt_eq_gt_cases := Zlt_trichotomy (only parsing).
 
146
 
 
147
Theorem Zlt_gt_cases : forall n m : Z, n ~= m <-> n < m \/ n > m.
 
148
Proof NZlt_gt_cases.
 
149
 
 
150
Theorem Zle_gt_cases : forall n m : Z, n <= m \/ n > m.
 
151
Proof NZle_gt_cases.
 
152
 
 
153
Theorem Zlt_ge_cases : forall n m : Z, n < m \/ n >= m.
 
154
Proof NZlt_ge_cases.
 
155
 
 
156
Theorem Zle_ge_cases : forall n m : Z, n <= m \/ n >= m.
 
157
Proof NZle_ge_cases.
 
158
 
 
159
(** Instances of the previous theorems for m == 0 *)
 
160
 
 
161
Theorem Zneg_pos_cases : forall n : Z, n ~= 0 <-> n < 0 \/ n > 0.
 
162
Proof.
 
163
intro; apply Zlt_gt_cases.
 
164
Qed.
 
165
 
 
166
Theorem Znonpos_pos_cases : forall n : Z, n <= 0 \/ n > 0.
 
167
Proof.
 
168
intro; apply Zle_gt_cases.
 
169
Qed.
 
170
 
 
171
Theorem Zneg_nonneg_cases : forall n : Z, n < 0 \/ n >= 0.
 
172
Proof.
 
173
intro; apply Zlt_ge_cases.
 
174
Qed.
 
175
 
 
176
Theorem Znonpos_nonneg_cases : forall n : Z, n <= 0 \/ n >= 0.
 
177
Proof.
 
178
intro; apply Zle_ge_cases.
 
179
Qed.
 
180
 
 
181
Theorem Zle_ngt : forall n m : Z, n <= m <-> ~ n > m.
 
182
Proof NZle_ngt.
 
183
 
 
184
Theorem Znlt_ge : forall n m : Z, ~ n < m <-> n >= m.
 
185
Proof NZnlt_ge.
 
186
 
 
187
Theorem Zlt_dec : forall n m : Z, decidable (n < m).
 
188
Proof NZlt_dec.
 
189
 
 
190
Theorem Zlt_dne : forall n m, ~ ~ n < m <-> n < m.
 
191
Proof NZlt_dne.
 
192
 
 
193
Theorem Znle_gt : forall n m : Z, ~ n <= m <-> n > m.
 
194
Proof NZnle_gt.
 
195
 
 
196
Theorem Zlt_nge : forall n m : Z, n < m <-> ~ n >= m.
 
197
Proof NZlt_nge.
 
198
 
 
199
Theorem Zle_dec : forall n m : Z, decidable (n <= m).
 
200
Proof NZle_dec.
 
201
 
 
202
Theorem Zle_dne : forall n m : Z, ~ ~ n <= m <-> n <= m.
 
203
Proof NZle_dne.
 
204
 
 
205
Theorem Znlt_succ_r : forall n m : Z, ~ m < S n <-> n < m.
 
206
Proof NZnlt_succ_r.
 
207
 
 
208
Theorem Zlt_exists_pred :
 
209
  forall z n : Z, z < n -> exists k : Z, n == S k /\ z <= k.
 
210
Proof NZlt_exists_pred.
 
211
 
 
212
Theorem Zlt_succ_iter_r :
 
213
  forall (n : nat) (m : Z), m < NZsucc_iter (Datatypes.S n) m.
 
214
Proof NZlt_succ_iter_r.
 
215
 
 
216
Theorem Zneq_succ_iter_l :
 
217
  forall (n : nat) (m : Z), NZsucc_iter (Datatypes.S n) m ~= m.
 
218
Proof NZneq_succ_iter_l.
 
219
 
 
220
(** Stronger variant of induction with assumptions n >= 0 (n < 0)
 
221
in the induction step *)
 
222
 
 
223
Theorem Zright_induction :
 
224
  forall A : Z -> Prop, predicate_wd Zeq A ->
 
225
    forall z : Z, A z ->
 
226
      (forall n : Z, z <= n -> A n -> A (S n)) ->
 
227
        forall n : Z, z <= n -> A n.
 
228
Proof NZright_induction.
 
229
 
 
230
Theorem Zleft_induction :
 
231
  forall A : Z -> Prop, predicate_wd Zeq A ->
 
232
    forall z : Z, A z ->
 
233
      (forall n : Z, n < z -> A (S n) -> A n) ->
 
234
        forall n : Z, n <= z -> A n.
 
235
Proof NZleft_induction.
 
236
 
 
237
Theorem Zright_induction' :
 
238
  forall A : Z -> Prop, predicate_wd Zeq A ->
 
239
    forall z : Z,
 
240
      (forall n : Z, n <= z -> A n) ->
 
241
      (forall n : Z, z <= n -> A n -> A (S n)) ->
 
242
        forall n : Z, A n.
 
243
Proof NZright_induction'.
 
244
 
 
245
Theorem Zleft_induction' :
 
246
  forall A : Z -> Prop, predicate_wd Zeq A ->
 
247
    forall z : Z,
 
248
    (forall n : Z, z <= n -> A n) ->
 
249
    (forall n : Z, n < z -> A (S n) -> A n) ->
 
250
      forall n : Z, A n.
 
251
Proof NZleft_induction'.
 
252
 
 
253
Theorem Zstrong_right_induction :
 
254
  forall A : Z -> Prop, predicate_wd Zeq A ->
 
255
    forall z : Z,
 
256
    (forall n : Z, z <= n -> (forall m : Z, z <= m -> m < n -> A m) -> A n) ->
 
257
       forall n : Z, z <= n -> A n.
 
258
Proof NZstrong_right_induction.
 
259
 
 
260
Theorem Zstrong_left_induction :
 
261
  forall A : Z -> Prop, predicate_wd Zeq A ->
 
262
    forall z : Z,
 
263
      (forall n : Z, n <= z -> (forall m : Z, m <= z -> S n <= m -> A m) -> A n) ->
 
264
        forall n : Z, n <= z -> A n.
 
265
Proof NZstrong_left_induction.
 
266
 
 
267
Theorem Zstrong_right_induction' :
 
268
  forall A : Z -> Prop, predicate_wd Zeq A ->
 
269
    forall z : Z,
 
270
      (forall n : Z, n <= z -> A n) ->
 
271
      (forall n : Z, z <= n -> (forall m : Z, z <= m -> m < n -> A m) -> A n) ->
 
272
        forall n : Z, A n.
 
273
Proof NZstrong_right_induction'.
 
274
 
 
275
Theorem Zstrong_left_induction' :
 
276
  forall A : Z -> Prop, predicate_wd Zeq A ->
 
277
    forall z : Z,
 
278
    (forall n : Z, z <= n -> A n) ->
 
279
    (forall n : Z, n <= z -> (forall m : Z, m <= z -> S n <= m -> A m) -> A n) ->
 
280
      forall n : Z, A n.
 
281
Proof NZstrong_left_induction'.
 
282
 
 
283
Theorem Zorder_induction :
 
284
  forall A : Z -> Prop, predicate_wd Zeq A ->
 
285
    forall z : Z, A z ->
 
286
    (forall n : Z, z <= n -> A n -> A (S n)) ->
 
287
    (forall n : Z, n < z -> A (S n) -> A n) ->
 
288
      forall n : Z, A n.
 
289
Proof NZorder_induction.
 
290
 
 
291
Theorem Zorder_induction' :
 
292
  forall A : Z -> Prop, predicate_wd Zeq A ->
 
293
    forall z : Z, A z ->
 
294
    (forall n : Z, z <= n -> A n -> A (S n)) ->
 
295
    (forall n : Z, n <= z -> A n -> A (P n)) ->
 
296
      forall n : Z, A n.
 
297
Proof NZorder_induction'.
 
298
 
 
299
Theorem Zorder_induction_0 :
 
300
  forall A : Z -> Prop, predicate_wd Zeq A ->
 
301
    A 0 ->
 
302
    (forall n : Z, 0 <= n -> A n -> A (S n)) ->
 
303
    (forall n : Z, n < 0 -> A (S n) -> A n) ->
 
304
      forall n : Z, A n.
 
305
Proof NZorder_induction_0.
 
306
 
 
307
Theorem Zorder_induction'_0 :
 
308
  forall A : Z -> Prop, predicate_wd Zeq A ->
 
309
    A 0 ->
 
310
    (forall n : Z, 0 <= n -> A n -> A (S n)) ->
 
311
    (forall n : Z, n <= 0 -> A n -> A (P n)) ->
 
312
      forall n : Z, A n.
 
313
Proof NZorder_induction'_0.
 
314
 
 
315
Ltac Zinduct n := induction_maker n ltac:(apply Zorder_induction_0).
 
316
 
 
317
(** Elimintation principle for < *)
 
318
 
 
319
Theorem Zlt_ind :
 
320
  forall A : Z -> Prop, predicate_wd Zeq A ->
 
321
    forall n : Z, A (S n) ->
 
322
      (forall m : Z, n < m -> A m -> A (S m)) -> forall m : Z, n < m -> A m.
 
323
Proof NZlt_ind.
 
324
 
 
325
(** Elimintation principle for <= *)
 
326
 
 
327
Theorem Zle_ind :
 
328
  forall A : Z -> Prop, predicate_wd Zeq A ->
 
329
    forall n : Z, A n ->
 
330
      (forall m : Z, n <= m -> A m -> A (S m)) -> forall m : Z, n <= m -> A m.
 
331
Proof NZle_ind.
 
332
 
 
333
(** Well-founded relations *)
 
334
 
 
335
Theorem Zlt_wf : forall z : Z, well_founded (fun n m : Z => z <= n /\ n < m).
 
336
Proof NZlt_wf.
 
337
 
 
338
Theorem Zgt_wf : forall z : Z, well_founded (fun n m : Z => m < n /\ n <= z).
 
339
Proof NZgt_wf.
 
340
 
 
341
(* Theorems that are either not valid on N or have different proofs on N and Z *)
 
342
 
 
343
Theorem Zlt_pred_l : forall n : Z, P n < n.
 
344
Proof.
 
345
intro n; rewrite <- (Zsucc_pred n) at 2; apply Zlt_succ_diag_r.
 
346
Qed.
 
347
 
 
348
Theorem Zle_pred_l : forall n : Z, P n <= n.
 
349
Proof.
 
350
intro; apply Zlt_le_incl; apply Zlt_pred_l.
 
351
Qed.
 
352
 
 
353
Theorem Zlt_le_pred : forall n m : Z, n < m <-> n <= P m.
 
354
Proof.
 
355
intros n m; rewrite <- (Zsucc_pred m); rewrite Zpred_succ. apply Zlt_succ_r.
 
356
Qed.
 
357
 
 
358
Theorem Znle_pred_r : forall n : Z, ~ n <= P n.
 
359
Proof.
 
360
intro; rewrite <- Zlt_le_pred; apply Zlt_irrefl.
 
361
Qed.
 
362
 
 
363
Theorem Zlt_pred_le : forall n m : Z, P n < m <-> n <= m.
 
364
Proof.
 
365
intros n m; rewrite <- (Zsucc_pred n) at 2.
 
366
symmetry; apply Zle_succ_l.
 
367
Qed.
 
368
 
 
369
Theorem Zlt_lt_pred : forall n m : Z, n < m -> P n < m.
 
370
Proof.
 
371
intros; apply <- Zlt_pred_le; now apply Zlt_le_incl.
 
372
Qed.
 
373
 
 
374
Theorem Zle_le_pred : forall n m : Z, n <= m -> P n <= m.
 
375
Proof.
 
376
intros; apply Zlt_le_incl; now apply <- Zlt_pred_le.
 
377
Qed.
 
378
 
 
379
Theorem Zlt_pred_lt : forall n m : Z, n < P m -> n < m.
 
380
Proof.
 
381
intros n m H; apply Zlt_trans with (P m); [assumption | apply Zlt_pred_l].
 
382
Qed.
 
383
 
 
384
Theorem Zle_pred_lt : forall n m : Z, n <= P m -> n <= m.
 
385
Proof.
 
386
intros; apply Zlt_le_incl; now apply <- Zlt_le_pred.
 
387
Qed.
 
388
 
 
389
Theorem Zpred_lt_mono : forall n m : Z, n < m <-> P n < P m.
 
390
Proof.
 
391
intros; rewrite Zlt_le_pred; symmetry; apply Zlt_pred_le.
 
392
Qed.
 
393
 
 
394
Theorem Zpred_le_mono : forall n m : Z, n <= m <-> P n <= P m.
 
395
Proof.
 
396
intros; rewrite <- Zlt_pred_le; now rewrite Zlt_le_pred.
 
397
Qed.
 
398
 
 
399
Theorem Zlt_succ_lt_pred : forall n m : Z, S n < m <-> n < P m.
 
400
Proof.
 
401
intros n m; now rewrite (Zpred_lt_mono (S n) m), Zpred_succ.
 
402
Qed.
 
403
 
 
404
Theorem Zle_succ_le_pred : forall n m : Z, S n <= m <-> n <= P m.
 
405
Proof.
 
406
intros n m; now rewrite (Zpred_le_mono (S n) m), Zpred_succ.
 
407
Qed.
 
408
 
 
409
Theorem Zlt_pred_lt_succ : forall n m : Z, P n < m <-> n < S m.
 
410
Proof.
 
411
intros; rewrite Zlt_pred_le; symmetry; apply Zlt_succ_r.
 
412
Qed.
 
413
 
 
414
Theorem Zle_pred_lt_succ : forall n m : Z, P n <= m <-> n <= S m.
 
415
Proof.
 
416
intros n m; now rewrite (Zpred_le_mono n (S m)), Zpred_succ.
 
417
Qed.
 
418
 
 
419
Theorem Zneq_pred_l : forall n : Z, P n ~= n.
 
420
Proof.
 
421
intro; apply Zlt_neq; apply Zlt_pred_l.
 
422
Qed.
 
423
 
 
424
Theorem Zlt_n1_r : forall n m : Z, n < m -> m < 0 -> n < -1.
 
425
Proof.
 
426
intros n m H1 H2. apply -> Zlt_le_pred in H2.
 
427
setoid_replace (P 0) with (-1) in H2. now apply NZlt_le_trans with m.
 
428
apply <- Zeq_opp_r. now rewrite Zopp_pred, Zopp_0.
 
429
Qed.
 
430
 
 
431
End ZOrderPropFunct.
 
432