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
|
Require Export NBase.
Require Import NZOrder.
Module Type NOrderSig.
Declare Module Export NBaseMod : NBaseSig.
Open Local Scope NatScope.
Parameter Inline lt : N -> N -> Prop.
Parameter Inline le : N -> N -> Prop.
Notation "x < y" := (lt x y) : NatScope.
Notation "x <= y" := (le x y) : NatScope.
Notation "x > y" := (lt y x) (only parsing) : NatScope.
Notation "x >= y" := (le y x) (only parsing) : NatScope.
Add Morphism lt with signature E ==> E ==> iff as lt_wd.
Add Morphism le with signature E ==> E ==> iff as le_wd.
Axiom le_lt_or_eq : forall x y, x <= y <-> x < y \/ x == y.
Axiom nlt_0_r : forall x, ~ (x < 0).
Axiom lt_succ_le : forall x y, x < S y <-> x <= y.
End NOrderSig.
Module NOrderPropFunct (Import NOrderModule : NOrderSig).
Module Export NBasePropMod := NBasePropFunct NBaseMod.
Open Local Scope NatScope.
Ltac le_intro1 := rewrite le_lt_or_eq; left.
Ltac le_intro2 := rewrite le_lt_or_eq; right.
Ltac le_elim H := rewrite le_lt_or_eq in H; destruct H as [H | H].
Theorem lt_succ_lt : forall n m : N, S n < m -> n < m.
Proof.
intro n; induct m.
intro H; false_hyp H nlt_0_r.
intros m IH H. apply <- lt_succ_le. apply -> lt_succ_le in H. le_elim H.
le_intro1; now apply IH.
rewrite <- H; le_intro1. apply <- lt_succ_le; now le_intro2.
Qed.
Theorem lt_irrefl : forall n : N, ~ (n < n).
Proof.
induct n.
apply nlt_0_r.
intros n IH H. apply -> lt_succ_le in H; le_elim H.
apply lt_succ_lt in H; now apply IH.
assert (n < S n) by (apply <- lt_succ_le; now le_intro2).
rewrite H in *; now apply IH.
Qed.
Module NZOrderMod <: NZOrderSig.
Module NZBaseMod := NZBaseMod.
Definition NZlt := lt.
Definition NZle := le.
Add Morphism NZlt with signature E ==> E ==> iff as NZlt_wd.
Proof lt_wd.
Add Morphism NZle with signature E ==> E ==> iff as NZle_wd.
Proof le_wd.
Definition NZle_lt_or_eq := le_lt_or_eq.
Definition NZlt_succ_le := lt_succ_le.
Definition NZlt_succ_lt := lt_succ_lt.
Definition NZlt_irrefl := lt_irrefl.
End NZOrderMod.
Module Export NZOrderPropMod := NZOrderPropFunct NZOrderMod.
(* Renaming theorems from NZOrder.v *)
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 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 central_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 NZcentral_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_intro2.
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 H; le_elim H; [false_hyp H nlt_0_r | assumption].
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, 0 ~= n -> 0 < n.
Proof.
nondep_induct n. intro H; now elim H. intros; apply lt_0_succ.
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_intro2.
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.
End NOrderPropFunct.
(*
Local Variables:
tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
End:
*)
|
