aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Natural/Abstract/NOrder.v
blob: 773f5d97eece7ea8ae4c8599993a499d5ec0c961 (plain)
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
Require Export NTimes.

Module NOrderPropFunct (Import NAxiomsMod : NAxiomsSig).
Module Export NTimesPropMod := NTimesPropFunct NAxiomsMod.
Open Local Scope NatScope.

(* The tactics le_less, le_equal and le_elim are inherited from NZOrder.v *)

(* Axioms *)

Theorem le_lt_or_eq : forall x y, x <= y <-> x < y \/ x == y.
Proof le_lt_or_eq.

Theorem nlt_0_r : forall x, ~ (x < 0).
Proof nlt_0_r.

Theorem lt_succ_le : forall x y, x < S y <-> x <= y.
Proof lt_succ_le.

(* Renaming theorems from NZOrder.v *)

Theorem lt_irrefl : forall n : N, ~ (n < n).
Proof NZOrdAxiomsMod.NZlt_irrefl.

Theorem lt_le_incl : forall n m : N, n < m -> n <= m.
Proof NZlt_le_incl.

Theorem lt_neq : forall n m : N, n < m -> n ~= m.
Proof NZlt_neq.

Theorem le_refl : forall n : N, n <= n.
Proof NZle_refl.

Theorem lt_succ_r : forall n : N, n < S n.
Proof NZlt_succ_r.

Theorem le_succ_r : forall n : N, n <= S n.
Proof NZle_succ_r.

Theorem lt_lt_succ : forall n m : N, n < m -> n < S m.
Proof NZlt_lt_succ.

Theorem le_le_succ : forall n m : N, n <= m -> n <= S m.
Proof NZle_le_succ.

Theorem le_succ_le_or_eq_succ : forall n m : N, n <= S m <-> n <= m \/ n == S m.
Proof NZle_succ_le_or_eq_succ.

Theorem neq_succ_l : forall n : N, S n ~= n.
Proof NZneq_succ_l.

Theorem nlt_succ_l : forall n : N, ~ S n < n.
Proof NZnlt_succ_l.

Theorem nle_succ_l : forall n : N, ~ S n <= n.
Proof NZnle_succ_l.

Theorem lt_le_succ : forall n m : N, n < m <-> S n <= m.
Proof NZlt_le_succ.

Theorem lt_succ_lt : forall n m : N, S n < m -> n < m.
Proof NZlt_succ_lt.

Theorem le_succ_le : forall n m : N, S n <= m -> n <= m.
Proof NZle_succ_le.

Theorem succ_lt_mono : forall n m : N, n < m <-> S n < S m.
Proof NZsucc_lt_mono.

Theorem succ_le_mono : forall n m : N, n <= m <-> S n <= S m.
Proof NZsucc_le_mono.

Theorem lt_lt_false : forall n m, n < m -> m < n -> False.
Proof NZlt_lt_false.

Theorem lt_asymm : forall n m, n < m -> ~ m < n.
Proof NZlt_asymm.

Theorem lt_trans : forall n m p : N, n < m -> m < p -> n < p.
Proof NZlt_trans.

Theorem le_trans : forall n m p : N, n <= m -> m <= p -> n <= p.
Proof NZle_trans.

Theorem le_lt_trans : forall n m p : N, n <= m -> m < p -> n < p.
Proof NZle_lt_trans.

Theorem lt_le_trans : forall n m p : N, n < m -> m <= p -> n < p.
Proof NZlt_le_trans.

Theorem le_antisymm : forall n m : N, n <= m -> m <= n -> n == m.
Proof NZle_antisymm.

(** Trichotomy, decidability, and double negation elimination *)

Theorem lt_trichotomy : forall n m : N,  n < m \/ n == m \/ m < n.
Proof NZlt_trichotomy.

Theorem le_lt_dec : forall n m : N, n <= m \/ m < n.
Proof NZle_lt_dec.

Theorem le_nlt : forall n m : N, n <= m <-> ~ m < n.
Proof NZle_nlt.

Theorem lt_dec : forall n m : N, n < m \/ ~ n < m.
Proof NZlt_dec.

Theorem lt_dne : forall n m, ~ ~ n < m <-> n < m.
Proof NZlt_dne.

Theorem nle_lt : forall n m : N, ~ n <= m <-> m < n.
Proof NZnle_lt.

Theorem le_dec : forall n m : N, n <= m \/ ~ n <= m.
Proof NZle_dec.

Theorem le_dne : forall n m : N, ~ ~ n <= m <-> n <= m.
Proof NZle_dne.

Theorem lt_nlt_succ : forall n m : N, n < m <-> ~ m < S n.
Proof NZlt_nlt_succ.

Theorem lt_exists_pred :
  forall z n : N, z < n -> exists k : N, n == S k /\ z <= k.
Proof NZlt_exists_pred.

Theorem lt_succ_iter_r :
  forall (n : nat) (m : N), m < NZsucc_iter (Datatypes.S n) m.
Proof NZlt_succ_iter_r.

Theorem neq_succ_iter_l :
  forall (n : nat) (m : N), 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 right_induction :
  forall A : N -> Prop, predicate_wd E A ->
    forall z : N, A z ->
      (forall n : N, z <= n -> A n -> A (S n)) ->
        forall n : N, z <= n -> A n.
Proof NZright_induction.

Theorem left_induction :
  forall A : N -> Prop, predicate_wd E A ->
    forall z : N, A z ->
      (forall n : N, n < z -> A (S n) -> A n) ->
        forall n : N, n <= z -> A n.
Proof NZleft_induction.

Theorem order_induction :
  forall A : N -> Prop, predicate_wd E A ->
    forall z : N, A z ->
      (forall n : N, z <= n -> A n -> A (S n)) ->
      (forall n : N, n < z  -> A (S n) -> A n) ->
        forall n : N, A n.
Proof NZorder_induction.

Theorem right_induction' :
  forall A : N -> Prop, predicate_wd E A ->
    forall z : N,
      (forall n : N, n <= z -> A n) ->
      (forall n : N, z <= n -> A n -> A (S n)) ->
        forall n : N, A n.
Proof NZright_induction'.

Theorem strong_right_induction' :
  forall A : N -> Prop, predicate_wd E A ->
    forall z : N,
      (forall n : N, n <= z -> A n) ->
      (forall n : N, z <= n -> (forall m : N, z <= m -> m < n -> A m) -> A n) ->
        forall n : N, A n.
Proof NZstrong_right_induction'.

(** Elimintation principle for < *)

Theorem lt_ind :
  forall A : N -> Prop, predicate_wd E A ->
    forall n : N,
      A (S n) ->
      (forall m : N, n < m -> A m -> A (S m)) ->
        forall m : N, n < m -> A m.
Proof NZlt_ind.

(** Elimintation principle for <= *)

Theorem le_ind :
  forall A : N -> Prop, predicate_wd E A ->
    forall n : N,
      A n ->
      (forall m : N, n <= m -> A m -> A (S m)) ->
        forall m : N, n <= m -> A m.
Proof NZle_ind.

(** Theorems that are true for natural numbers but not for integers *)

Theorem le_0_l : forall n : N, 0 <= n.
Proof.
induct n.
now le_equal.
intros; now apply le_le_succ.
Qed.

Theorem nle_succ_0 : forall n, ~ (S n <= 0).
Proof.
intros n H; apply <- lt_le_succ in H; false_hyp H nlt_0_r.
Qed.

Theorem le_0_eq_0 : forall n, n <= 0 <-> n == 0.
Proof.
intros n; split; intro H.
le_elim H; [false_hyp H nlt_0_r | assumption].
le_equal.
Qed.

Theorem lt_0_succ : forall n, 0 < S n.
Proof.
induct n; [apply lt_succ_r | intros n H; now apply lt_lt_succ].
Qed.

Theorem lt_lt_0 : forall n m, n < m -> 0 < m.
Proof.
intros n m; induct n.
trivial.
intros n IH H. apply IH; now apply lt_succ_lt.
Qed.

Theorem neq_0_lt_0 : forall n, n ~= 0 <-> 0 < n.
Proof.
nondep_induct n.
split; intro H; [now elim H | intro; now apply lt_irrefl with 0].
intro n; split; intro H; [apply lt_0_succ | apply neq_succ_0].
Qed.

Lemma Acc_nonneg_lt : forall n : N,
  Acc (fun n m => 0 <= n /\ n < m) n -> Acc lt n.
Proof.
intros n H; induction H as [n _ H2];
constructor; intros y H; apply H2; split; [apply le_0_l | assumption].
Qed.

Theorem lt_wf : well_founded lt.
Proof.
unfold well_founded; intro n; apply Acc_nonneg_lt. apply NZlt_wf.
Qed.

(** Elimination principlies for < and <= for relations *)

Section RelElim.

(* FIXME: Variable R : relation N. -- does not work *)

Variable R : N -> N -> Prop.
Hypothesis R_wd : rel_wd E E R.

Add Morphism R with signature E ==> E ==> iff as R_morph2.
Proof R_wd.

Theorem le_ind_rel :
   (forall m, R 0 m) ->
   (forall n m, n <= m -> R n m -> R (S n) (S m)) ->
     forall n m, n <= m -> R n m.
Proof.
intros Base Step; induct n.
intros; apply Base.
intros n IH m H. elim H using le_ind.
solve_predicate_wd.
apply Step; [| apply IH]; now le_equal.
intros k H1 H2. apply le_succ_le in H1. auto.
Qed.

Theorem lt_ind_rel :
   (forall m, R 0 (S m)) ->
   (forall n m, n < m -> R n m -> R (S n) (S m)) ->
   forall n m, n < m -> R n m.
Proof.
intros Base Step; induct n.
intros m H. apply lt_exists_pred in H; destruct H as [m' [H _]].
rewrite H; apply Base.
intros n IH m H. elim H using lt_ind.
solve_predicate_wd.
apply Step; [| apply IH]; now apply lt_succ_r.
intros k H1 H2. apply lt_succ_lt in H1. auto.
Qed.

End RelElim.

(** Predecessor and order *)

Theorem succ_pred_pos : forall n : N, 0 < n -> S (P n) == n.
Proof.
intros n H; apply succ_pred; intro H1; rewrite H1 in H.
false_hyp H lt_irrefl.
Qed.

Theorem le_pred_l : forall n : N, P n <= n.
Proof.
nondep_induct n.
rewrite pred_0; le_equal.
intros; rewrite pred_succ;  apply le_succ_r.
Qed.

Theorem lt_pred_l : forall n : N, n ~= 0 -> P n < n.
Proof.
nondep_induct n.
intro H; elimtype False; now apply H.
intros; rewrite pred_succ;  apply lt_succ_r.
Qed.

Theorem le_le_pred : forall n m : N, n <= m -> P n <= m.
Proof.
intros n m H; apply le_trans with n. apply le_pred_l. assumption.
Qed.

Theorem lt_lt_pred : forall n m : N, n < m -> P n < m.
Proof.
intros n m H; apply le_lt_trans with n. apply le_pred_l. assumption.
Qed.

Theorem lt_le_pred : forall n m : N, n < m -> n <= P m. (* Converse is false for n == m == 0 *)
Proof.
intro n; nondep_induct m.
intro H; false_hyp H nlt_0_r.
intros m IH. rewrite pred_succ; now apply -> lt_succ_le.
Qed.

Theorem lt_pred_le : forall n m : N, P n < m -> n <= m. (* Converse is false for n == m == 0 *)
Proof.
intros n m; nondep_induct n.
rewrite pred_0; intro H; le_less.
intros n IH. rewrite pred_succ in IH. now apply -> lt_le_succ.
Qed.

Theorem lt_pred_lt : forall n m : N, n < P m -> n < m.
Proof.
intros n m H; apply lt_le_trans with (P m); [assumption | apply le_pred_l].
Qed.

Theorem le_pred_le : forall n m : N, n <= P m -> n <= m.
Proof.
intros n m H; apply le_trans with (P m); [assumption | apply le_pred_l].
Qed.

Theorem pred_le_mono : forall n m : N, n <= m -> P n <= P m. (* Converse is false for n == 1, m == 0 *)
Proof.
intros n m H; elim H using le_ind_rel.
solve_rel_wd.
intro; rewrite pred_0; apply le_0_l.
intros p q H1 _; now do 2 rewrite pred_succ.
Qed.

Theorem pred_lt_mono : forall n m : N, n ~= 0 -> (n < m <-> P n < P m).
Proof.
intros n m H1; split; intro H2.
assert (m ~= 0). apply <- neq_0_lt_0. now apply lt_lt_0 with n.
now rewrite <- (succ_pred n) in H2; rewrite <- (succ_pred m) in H2;
[apply <- succ_lt_mono | | |].
assert (m ~= 0). apply <- neq_0_lt_0. apply lt_lt_0 with (P n).
apply lt_le_trans with (P m). assumption. apply le_pred_l.
apply -> succ_lt_mono in H2. now do 2 rewrite succ_pred in H2.
Qed.

Theorem lt_succ_lt_pred : forall n m : N, S n < m <-> n < P m.
Proof.
intros n m. rewrite pred_lt_mono. apply neq_succ_0. now rewrite pred_succ.
Qed.

Theorem le_succ_le_pred : forall n m : N, S n <= m -> n <= P m. (* Converse is false for n == m == 0 *)
Proof.
intros n m H. apply lt_le_pred. now apply <- lt_le_succ.
Qed.

Theorem lt_pred_lt_succ : forall n m : N, P n < m -> n < S m. (* Converse is false for n == m == 0 *)
Proof.
intros n m H. apply <- lt_succ_le. now apply lt_pred_le.
Qed.

Theorem le_pred_le_succ : forall n m : N, P n <= m <-> n <= S m.
Proof.
intros n m; nondep_induct n.
rewrite pred_0. split; intro H; apply le_0_l.
intro n. rewrite pred_succ. apply succ_le_mono.
Qed.

End NOrderPropFunct.


(*
 Local Variables:
 tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
 End:
*)