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
|
Require Export ZTimes.
Module ZOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
Module Export ZTimesPropMod := ZTimesPropFunct ZAxiomsMod.
Open Local Scope NatIntScope.
(* Axioms *)
Theorem Zle_lt_or_eq : forall n m : Z, n <= m <-> n < m \/ n == m.
Proof NZle_lt_or_eq.
Theorem Zlt_irrefl : forall n : Z, ~ n < n.
Proof NZlt_irrefl.
Theorem Zlt_succ_le : forall n m : Z, n < S m <-> n <= m.
Proof NZlt_succ_le.
(* 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_refl : forall n : Z, n <= n.
Proof NZle_refl.
Theorem Zlt_succ_r : forall n : Z, n < S n.
Proof NZlt_succ_r.
Theorem Zle_succ_r : forall n : Z, n <= S n.
Proof NZle_succ_r.
Theorem Zlt_lt_succ : forall n m : Z, n < m -> n < S m.
Proof NZlt_lt_succ.
Theorem Zle_le_succ : forall n m : Z, n <= m -> n <= S m.
Proof NZle_le_succ.
Theorem Zle_succ_le_or_eq_succ : forall n m : Z, n <= S m <-> n <= m \/ n == S m.
Proof NZle_succ_le_or_eq_succ.
Theorem Zneq_succ_l : forall n : Z, S n ~= n.
Proof NZneq_succ_l.
Theorem Znlt_succ_l : forall n : Z, ~ S n < n.
Proof NZnlt_succ_l.
Theorem Znle_succ_l : forall n : Z, ~ S n <= n.
Proof NZnle_succ_l.
Theorem Zlt_le_succ : forall n m : Z, n < m <-> S n <= m.
Proof NZlt_le_succ.
Theorem Zlt_succ_lt : forall n m : Z, S n < m -> n < m.
Proof NZlt_succ_lt.
Theorem Zle_succ_le : forall n m : Z, S n <= m -> n <= m.
Proof NZle_succ_le.
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.
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.
(** Trichotomy, decidability, and double negation elimination *)
Theorem Zlt_trichotomy : forall n m : Z, n < m \/ n == m \/ m < n.
Proof NZlt_trichotomy.
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_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_em : forall n m : Z, n < m \/ ~ n < m.
Proof NZlt_em.
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_em : forall n m : Z, n <= m \/ ~ n <= m.
Proof NZle_em.
Theorem Zle_dne : forall n m : Z, ~ ~ n <= m <-> n <= m.
Proof NZle_dne.
Theorem Zlt_nlt_succ : forall n m : Z, n < m <-> ~ m < S n.
Proof NZlt_nlt_succ.
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 E 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 E 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 Zorder_induction :
forall A : Z -> Prop, predicate_wd E 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 E 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.
intros A A_wd z Az AS AP n; apply Zorder_induction with (z := z); try assumption.
intros m H1 H2. apply AP in H2; [| now apply -> Zlt_le_succ].
unfold predicate_wd, fun_wd in A_wd; apply -> (A_wd (P (S m)) m);
[assumption | apply Zpred_succ].
Qed.
Theorem Zright_induction' :
forall A : Z -> Prop, predicate_wd E 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 Zstrong_right_induction' :
forall A : Z -> Prop, predicate_wd E 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'.
(** Elimintation principle for < *)
Theorem Zlt_ind :
forall A : Z -> Prop, predicate_wd E 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 E 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.
Ltac Zinduct n := induction_maker n ltac:(apply Zorder_induction with (z := 0)).
(** 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; pattern n at 2; qsetoid_rewrite <- (Zsucc_pred n); apply Zlt_succ_r.
Qed.
Theorem Zle_pred_l : forall n : Z, P n <= n.
Proof.
intro; le_less; 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_le.
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; pattern n at 2; qsetoid_rewrite <- (Zsucc_pred n).
apply Zlt_le_succ.
Qed.
Theorem Zlt_lt_pred : forall n m : Z, n < m -> P n < m.
Proof.
intros; apply <- Zlt_pred_le; le_less.
Qed.
Theorem Zle_le_pred : forall n m : Z, n <= m -> P n <= m.
Proof.
intros; le_less; 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; le_less; 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_le.
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.
End ZOrderPropFunct.
|
