]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/orders.ma
6dd8773f8820062586cacd3df6ebbea26afa8421
[helm.git] / helm / software / matita / library / nat / orders.ma
1 (**************************************************************************)
2 (*       ___                                                                *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "nat/nat.ma".
16 include "higher_order_defs/ordering.ma".
17
18 (* definitions *)
19 inductive le (n:nat) : nat \to Prop \def
20   | le_n : le n n
21   | le_S : \forall m:nat. le n m \to le n (S m).
22
23 interpretation "natural 'less or equal to'" 'leq x y = (cic:/matita/nat/orders/le.ind#xpointer(1/1) x y).
24
25 interpretation "natural 'neither less nor equal to'" 'nleq x y =
26   (cic:/matita/logic/connectives/Not.con
27     (cic:/matita/nat/orders/le.ind#xpointer(1/1) x y)).
28
29 definition lt: nat \to nat \to Prop \def
30 \lambda n,m:nat.(S n) \leq m.
31
32 interpretation "natural 'less than'" 'lt x y = (cic:/matita/nat/orders/lt.con x y).
33
34 interpretation "natural 'not less than'" 'nless x y =
35   (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/orders/lt.con x y)).
36
37 definition ge: nat \to nat \to Prop \def
38 \lambda n,m:nat.m \leq n.
39
40 interpretation "natural 'greater or equal to'" 'geq x y = (cic:/matita/nat/orders/ge.con x y).
41
42 definition gt: nat \to nat \to Prop \def
43 \lambda n,m:nat.m<n.
44
45 interpretation "natural 'greater than'" 'gt x y = (cic:/matita/nat/orders/gt.con x y).
46
47 interpretation "natural 'not greater than'" 'ngtr x y =
48   (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/orders/gt.con x y)).
49
50 theorem transitive_le : transitive nat le.
51 unfold transitive.intros.elim H1.
52 assumption.
53 apply le_S.assumption.
54 qed.
55
56 theorem trans_le: \forall n,m,p:nat. n \leq m \to m \leq p \to n \leq p
57 \def transitive_le.
58
59 theorem transitive_lt: transitive nat lt.
60 unfold transitive.unfold lt.intros.elim H1.
61 apply le_S. assumption.
62 apply le_S.assumption.
63 qed.
64
65 theorem trans_lt: \forall n,m,p:nat. lt n m \to lt m p \to lt n p
66 \def transitive_lt.
67
68 theorem le_S_S: \forall n,m:nat. n \leq m \to S n \leq S m.
69 intros.elim H.
70 apply le_n.
71 apply le_S.assumption.
72 qed.
73
74 theorem le_O_n : \forall n:nat. O \leq n.
75 intros.elim n.
76 apply le_n.apply 
77 le_S. assumption.
78 qed.
79
80 theorem le_n_Sn : \forall n:nat. n \leq S n.
81 intros. apply le_S.apply le_n.
82 qed.
83
84 theorem le_pred_n : \forall n:nat. pred n \leq n.
85 intros.elim n.
86 simplify.apply le_n.
87 simplify.apply le_n_Sn.
88 qed.
89
90 theorem le_S_S_to_le : \forall n,m:nat. S n \leq S m \to n \leq m.
91 intros.change with (pred (S n) \leq pred (S m)).
92 elim H.apply le_n.apply (trans_le ? (pred n1)).assumption.
93 apply le_pred_n.
94 qed.
95
96 theorem lt_S_S_to_lt: \forall n,m. 
97   S n < S m \to n < m.
98 intros. apply le_S_S_to_le. assumption.
99 qed.
100
101 theorem lt_to_lt_S_S: ∀n,m. n < m → S n < S m.
102 intros;
103 unfold lt in H;
104 apply (le_S_S ? ? H).
105 qed.
106
107 theorem leS_to_not_zero : \forall n,m:nat. S n \leq m \to not_zero m.
108 intros.elim H.exact I.exact I.
109 qed.
110
111 (* not le *)
112 theorem not_le_Sn_O: \forall n:nat. S n \nleq O.
113 intros.unfold Not.simplify.intros.apply (leS_to_not_zero ? ? H).
114 qed.
115
116 theorem not_le_Sn_n: \forall n:nat. S n \nleq n.
117 intros.elim n.apply not_le_Sn_O.unfold Not.simplify.intros.cut (S n1 \leq n1).
118 apply H.assumption.
119 apply le_S_S_to_le.assumption.
120 qed.
121
122 theorem lt_pred: \forall n,m. 
123   O < n \to n < m \to pred n < pred m. 
124 apply nat_elim2
125   [intros.apply False_ind.apply (not_le_Sn_O ? H)
126   |intros.apply False_ind.apply (not_le_Sn_O ? H1)
127   |intros.simplify.unfold.apply le_S_S_to_le.assumption
128   ]
129 qed.
130
131 theorem S_pred: \forall n:nat.lt O n \to eq nat n (S (pred n)).
132 intro.elim n.apply False_ind.exact (not_le_Sn_O O H).
133 apply eq_f.apply pred_Sn.
134 qed.
135
136 theorem le_pred_to_le:
137  ∀n,m. O < m → pred n ≤ pred m → n ≤ m.
138 intros 2;
139 elim n;
140 [ apply le_O_n
141 | simplify in H2;
142   rewrite > (S_pred m);
143   [ apply le_S_S;
144     assumption
145   | assumption
146   ]
147 ].
148 qed.
149
150 theorem le_to_le_pred:
151  ∀n,m. n ≤ m → pred n ≤ pred m.
152 intros 2;
153 elim n;
154 [ simplify;
155   apply le_O_n
156 | simplify;
157   elim m in H1 ⊢ %;
158   [ elim (not_le_Sn_O ? H1)
159   | simplify;
160     apply le_S_S_to_le;
161     assumption
162   ]
163 ].
164 qed.
165
166 (* le to lt or eq *)
167 theorem le_to_or_lt_eq : \forall n,m:nat. 
168 n \leq m \to n < m \lor n = m.
169 intros.elim H.
170 right.reflexivity.
171 left.unfold lt.apply le_S_S.assumption.
172 qed.
173
174 theorem Not_lt_n_n: ∀n. n ≮ n.
175 intro;
176 unfold Not;
177 intro;
178 unfold lt in H;
179 apply (not_le_Sn_n ? H).
180 qed.
181
182 (* not eq *)
183 theorem lt_to_not_eq : \forall n,m:nat. n<m \to n \neq m.
184 unfold Not.intros.cut ((le (S n) m) \to False).
185 apply Hcut.assumption.rewrite < H1.
186 apply not_le_Sn_n.
187 qed.
188
189 (*not lt*)
190 theorem eq_to_not_lt: \forall a,b:nat.
191 a = b \to a \nlt b.
192 intros.
193 unfold Not.
194 intros.
195 rewrite > H in H1.
196 apply (lt_to_not_eq b b)
197 [ assumption
198 | reflexivity
199 ]
200 qed.
201
202 theorem lt_n_m_to_not_lt_m_Sn: ∀n,m. n < m → m ≮ S n.
203 intros;
204 unfold Not;
205 intro;
206 unfold lt in H;
207 unfold lt in H1;
208 generalize in match (le_S_S ? ? H);
209 intro;
210 generalize in match (transitive_le ? ? ? H2 H1);
211 intro;
212 apply (not_le_Sn_n ? H3).
213 qed.
214
215 (* le vs. lt *)
216 theorem lt_to_le : \forall n,m:nat. n<m \to n \leq m.
217 simplify.intros.unfold lt in H.elim H.
218 apply le_S. apply le_n.
219 apply le_S. assumption.
220 qed.
221
222 theorem lt_S_to_le : \forall n,m:nat. n < S m \to n \leq m.
223 simplify.intros.
224 apply le_S_S_to_le.assumption.
225 qed.
226
227 theorem not_le_to_lt: \forall n,m:nat. n \nleq m \to m<n.
228 intros 2.
229 apply (nat_elim2 (\lambda n,m.n \nleq m \to m<n)).
230 intros.apply (absurd (O \leq n1)).apply le_O_n.assumption.
231 unfold Not.unfold lt.intros.apply le_S_S.apply le_O_n.
232 unfold Not.unfold lt.intros.apply le_S_S.apply H.intros.apply H1.apply le_S_S.
233 assumption.
234 qed.
235
236 theorem lt_to_not_le: \forall n,m:nat. n<m \to m \nleq n.
237 unfold Not.unfold lt.intros 3.elim H.
238 apply (not_le_Sn_n n H1).
239 apply H2.apply lt_to_le. apply H3.
240 qed.
241
242 theorem not_lt_to_le: \forall n,m:nat. Not (lt n m) \to le m n.
243 simplify.intros.
244 apply lt_S_to_le.
245 apply not_le_to_lt.exact H.
246 qed.
247
248 theorem le_to_not_lt: \forall n,m:nat. le n m \to Not (lt m n).
249 intros.unfold Not.unfold lt.
250 apply lt_to_not_le.unfold lt.
251 apply le_S_S.assumption.
252 qed.
253
254 theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
255 intros;
256 elim (le_to_or_lt_eq ? ? H1);
257 [ assumption
258 | elim (H H2)
259 ].
260 qed.
261
262 (* le elimination *)
263 theorem le_n_O_to_eq : \forall n:nat. n \leq O \to O=n.
264 intro.elim n.reflexivity.
265 apply False_ind.
266 apply not_le_Sn_O;
267 [2: apply H1 | skip].
268 qed.
269
270 theorem le_n_O_elim: \forall n:nat.n \leq O \to \forall P: nat \to Prop.
271 P O \to P n.
272 intro.elim n.
273 assumption.
274 apply False_ind.
275 apply  (not_le_Sn_O ? H1).
276 qed.
277
278 theorem le_n_Sm_elim : \forall n,m:nat.n \leq S m \to 
279 \forall P:Prop. (S n \leq S m \to P) \to (n=S m \to P) \to P.
280 intros 4.elim H.
281 apply H2.reflexivity.
282 apply H3. apply le_S_S. assumption.
283 qed.
284
285 (* le and eq *)
286 lemma le_to_le_to_eq: \forall n,m. n \le m \to m \le n \to n = m.
287 apply nat_elim2
288   [intros.apply le_n_O_to_eq.assumption
289   |intros.apply sym_eq.apply le_n_O_to_eq.assumption
290   |intros.apply eq_f.apply H
291     [apply le_S_S_to_le.assumption
292     |apply le_S_S_to_le.assumption
293     ]
294   ]
295 qed.
296
297 (* lt and le trans *)
298 theorem lt_O_S : \forall n:nat. O < S n.
299 intro. unfold. apply le_S_S. apply le_O_n.
300 qed.
301
302 theorem lt_to_le_to_lt: \forall n,m,p:nat. lt n m \to le m p \to lt n p.
303 intros.elim H1.
304 assumption.unfold lt.apply le_S.assumption.
305 qed.
306
307 theorem le_to_lt_to_lt: \forall n,m,p:nat. le n m \to lt m p \to lt n p.
308 intros 4.elim H.
309 assumption.apply H2.unfold lt.
310 apply lt_to_le.assumption.
311 qed.
312
313 theorem lt_S_to_lt: \forall n,m. S n < m \to n < m.
314 intros.
315 apply (trans_lt ? (S n))
316   [apply le_n|assumption]
317 qed.
318
319 theorem ltn_to_ltO: \forall n,m:nat. lt n m \to lt O m.
320 intros.apply (le_to_lt_to_lt O n).
321 apply le_O_n.assumption.
322 qed.
323
324 theorem lt_SO_n_to_lt_O_pred_n: \forall n:nat.
325 (S O) \lt n \to O \lt (pred n).
326 intros.
327 apply (ltn_to_ltO (pred (S O)) (pred n) ?).
328  apply (lt_pred (S O) n);
329  [ apply (lt_O_S O) 
330  | assumption
331  ]
332 qed.
333
334 theorem lt_O_n_elim: \forall n:nat. lt O n \to 
335 \forall P:nat\to Prop. (\forall m:nat.P (S m)) \to P n.
336 intro.elim n.apply False_ind.exact (not_le_Sn_O O H).
337 apply H2.
338 qed.
339
340 (* other abstract properties *)
341 theorem antisymmetric_le : antisymmetric nat le.
342 unfold antisymmetric.intros 2.
343 apply (nat_elim2 (\lambda n,m.(n \leq m \to m \leq n \to n=m))).
344 intros.apply le_n_O_to_eq.assumption.
345 intros.apply False_ind.apply (not_le_Sn_O ? H).
346 intros.apply eq_f.apply H.
347 apply le_S_S_to_le.assumption.
348 apply le_S_S_to_le.assumption.
349 qed.
350
351 theorem antisym_le: \forall n,m:nat. n \leq m \to m \leq n \to n=m
352 \def antisymmetric_le.
353
354 theorem le_n_m_to_lt_m_Sn_to_eq_n_m: ∀n,m. n ≤ m → m < S n → n=m.
355 intros;
356 unfold lt in H1;
357 generalize in match (le_S_S_to_le ? ? H1);
358 intro;
359 apply antisym_le;
360 assumption.
361 qed.
362
363 theorem decidable_le: \forall n,m:nat. decidable (n \leq m).
364 intros.
365 apply (nat_elim2 (\lambda n,m.decidable (n \leq m))).
366 intros.unfold decidable.left.apply le_O_n.
367 intros.unfold decidable.right.exact (not_le_Sn_O n1).
368 intros 2.unfold decidable.intro.elim H.
369 left.apply le_S_S.assumption.
370 right.unfold Not.intro.apply H1.apply le_S_S_to_le.assumption.
371 qed.
372
373 theorem decidable_lt: \forall n,m:nat. decidable (n < m).
374 intros.exact (decidable_le (S n) m).
375 qed.
376
377 (* well founded induction principles *)
378
379 theorem nat_elim1 : \forall n:nat.\forall P:nat \to Prop. 
380 (\forall m.(\forall p. (p \lt m) \to P p) \to P m) \to P n.
381 intros.cut (\forall q:nat. q \le n \to P q).
382 apply (Hcut n).apply le_n.
383 elim n.apply (le_n_O_elim q H1).
384 apply H.
385 intros.apply False_ind.apply (not_le_Sn_O p H2).
386 apply H.intros.apply H1.
387 cut (p < S n1).
388 apply lt_S_to_le.assumption.
389 apply (lt_to_le_to_lt p q (S n1) H3 H2).
390 qed.
391
392 (* some properties of functions *)
393
394 definition increasing \def \lambda f:nat \to nat. 
395 \forall n:nat. f n < f (S n).
396
397 theorem increasing_to_monotonic: \forall f:nat \to nat.
398 increasing f \to monotonic nat lt f.
399 unfold monotonic.unfold lt.unfold increasing.unfold lt.intros.elim H1.apply H.
400 apply (trans_le ? (f n1)).
401 assumption.apply (trans_le ? (S (f n1))).
402 apply le_n_Sn.
403 apply H.
404 qed.
405
406 theorem le_n_fn: \forall f:nat \to nat. (increasing f) 
407 \to \forall n:nat. n \le (f n).
408 intros.elim n.
409 apply le_O_n.
410 apply (trans_le ? (S (f n1))).
411 apply le_S_S.apply H1.
412 simplify in H. unfold increasing in H.unfold lt in H.apply H.
413 qed.
414
415 theorem increasing_to_le: \forall f:nat \to nat. (increasing f) 
416 \to \forall m:nat. \exists i. m \le (f i).
417 intros.elim m.
418 apply (ex_intro ? ? O).apply le_O_n.
419 elim H1.
420 apply (ex_intro ? ? (S a)).
421 apply (trans_le ? (S (f a))).
422 apply le_S_S.assumption.
423 simplify in H.unfold increasing in H.unfold lt in H.
424 apply H.
425 qed.
426
427 theorem increasing_to_le2: \forall f:nat \to nat. (increasing f) 
428 \to \forall m:nat. (f O) \le m \to 
429 \exists i. (f i) \le m \land m <(f (S i)).
430 intros.elim H1.
431 apply (ex_intro ? ? O).
432 split.apply le_n.apply H.
433 elim H3.elim H4.
434 cut ((S n1) < (f (S a)) \lor (S n1) = (f (S a))).
435 elim Hcut.
436 apply (ex_intro ? ? a).
437 split.apply le_S. assumption.assumption.
438 apply (ex_intro ? ? (S a)).
439 split.rewrite < H7.apply le_n.
440 rewrite > H7.
441 apply H.
442 apply le_to_or_lt_eq.apply H6.
443 qed.