]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library_auto/auto/nat/orders.ma
added library_auto/ to tests.
[helm.git] / helm / software / matita / library_auto / auto / 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 set "baseuri" "cic:/matita/library_auto/nat/orders".
16
17 include "auto/nat/nat.ma".
18 include "higher_order_defs/ordering.ma".
19
20 (* definitions *)
21 inductive le (n:nat) : nat \to Prop \def
22   | le_n : le n n
23   | le_S : \forall m:nat. le n m \to le n (S m).
24
25 (*CSC: the URI must disappear: there is a bug now *)
26 interpretation "natural 'less or equal to'" 'leq x y = (cic:/matita/library_auto/nat/orders/le.ind#xpointer(1/1) x y).
27 (*CSC: the URI must disappear: there is a bug now *)
28 interpretation "natural 'neither less nor equal to'" 'nleq x y =
29   (cic:/matita/logic/connectives/Not.con
30     (cic:/matita/library_auto/nat/orders/le.ind#xpointer(1/1) x y)).
31
32 definition lt: nat \to nat \to Prop \def
33 \lambda n,m:nat.(S n) \leq m.
34
35 (*CSC: the URI must disappear: there is a bug now *)
36 interpretation "natural 'less than'" 'lt x y = (cic:/matita/library_auto/nat/orders/lt.con x y).
37 (*CSC: the URI must disappear: there is a bug now *)
38 interpretation "natural 'not less than'" 'nless x y =
39   (cic:/matita/logic/connectives/Not.con (cic:/matita/library_auto/nat/orders/lt.con x y)).
40
41 definition ge: nat \to nat \to Prop \def
42 \lambda n,m:nat.m \leq n.
43
44 (*CSC: the URI must disappear: there is a bug now *)
45 interpretation "natural 'greater or equal to'" 'geq x y = (cic:/matita/library_auto/nat/orders/ge.con x y).
46
47 definition gt: nat \to nat \to Prop \def
48 \lambda n,m:nat.m<n.
49
50 (*CSC: the URI must disappear: there is a bug now *)
51 interpretation "natural 'greater than'" 'gt x y = (cic:/matita/library_auto/nat/orders/gt.con x y).
52 (*CSC: the URI must disappear: there is a bug now *)
53 interpretation "natural 'not greater than'" 'ngtr x y =
54   (cic:/matita/logic/connectives/Not.con (cic:/matita/library_auto/nat/orders/gt.con x y)).
55
56 theorem transitive_le : transitive nat le.
57 unfold transitive.
58 intros.
59 elim H1;auto.
60 (*[ assumption
61 | apply le_S.
62   assumption
63 ]*)
64 qed.
65
66 theorem trans_le: \forall n,m,p:nat. n \leq m \to m \leq p \to n \leq p
67 \def transitive_le.
68
69 theorem transitive_lt: transitive nat lt.
70 unfold transitive.
71 unfold lt.
72 intros.
73 elim H1;auto.
74   (*apply le_S;assumption.*)
75   
76 qed.
77
78 theorem trans_lt: \forall n,m,p:nat. lt n m \to lt m p \to lt n p
79 \def transitive_lt.
80
81 theorem le_S_S: \forall n,m:nat. n \leq m \to S n \leq S m.
82 intros.
83 elim H;auto.
84 (*[ apply le_n.
85 | apply le_S.
86   assumption
87 ]*)
88 qed.
89
90 theorem le_O_n : \forall n:nat. O \leq n.
91 intros.
92 elim n;auto.
93 (*[ apply le_n
94 | apply le_S. 
95   assumption
96 ]*)
97 qed.
98
99 theorem le_n_Sn : \forall n:nat. n \leq S n.
100 intros.auto.
101 (*apply le_S.
102 apply le_n.*)
103 qed.
104
105 theorem le_pred_n : \forall n:nat. pred n \leq n.
106 intros.
107 elim n;auto.
108 (*[ simplify.
109   apply le_n
110 | simplify.
111   apply le_n_Sn
112 ]*)
113 qed.
114
115 theorem le_S_S_to_le : \forall n,m:nat. S n \leq S m \to n \leq m.
116 intros.
117 change with (pred (S n) \leq pred (S m)).
118 elim H;auto.
119 (*[ apply le_n
120 | apply (trans_le ? (pred n1))
121   [ assumption
122   | apply le_pred_n
123   ]
124 ]*)
125 qed.
126
127 theorem leS_to_not_zero : \forall n,m:nat. S n \leq m \to not_zero m.
128 intros.
129 elim H
130 [ (*qui auto non chiude il goal*)
131   exact I
132 | (*qui auto non chiude il goal*)
133   exact I
134 ]
135 qed.
136
137 (* not le *)
138 theorem not_le_Sn_O: \forall n:nat. S n \nleq O.
139 intros.
140 unfold Not.
141 simplify.
142 intros.
143 (*qui auto NON chiude il goal*)
144 apply (leS_to_not_zero ? ? H).
145 qed.
146
147 theorem not_le_Sn_n: \forall n:nat. S n \nleq n.
148 intros.
149 elim n
150 [ apply not_le_Sn_O
151 | unfold Not.
152   simplify.
153   intros.auto
154   (*cut (S n1 \leq n1).
155   [ apply H.
156     assumption
157   | apply le_S_S_to_le.
158     assumption
159   ]*)
160 ]
161 qed.
162
163 (* le to lt or eq *)
164 theorem le_to_or_lt_eq : \forall n,m:nat. 
165 n \leq m \to n < m \lor n = m.
166 intros.
167 elim H
168 [ auto
169   (*right.
170   reflexivity*)
171 | left.
172   unfold lt.
173   auto
174   (*apply le_S_S.
175   assumption*)
176 ]
177 qed.
178
179 (* not eq *)
180 theorem lt_to_not_eq : \forall n,m:nat. n<m \to n \neq m.
181 unfold Not.
182 intros.
183 cut ((le (S n) m) \to False)
184 [ auto
185   (*apply Hcut.
186   assumption*)
187 | rewrite < H1.
188   apply not_le_Sn_n
189 ]
190 qed.
191
192 (* le vs. lt *)
193 theorem lt_to_le : \forall n,m:nat. n<m \to n \leq m.
194 simplify.
195 intros.
196 auto.
197 (*unfold lt in H.
198 elim H
199 [ apply le_S. 
200   apply le_n
201 | apply le_S. 
202   assumption
203 ]*)
204 qed.
205
206 theorem lt_S_to_le : \forall n,m:nat. n < S m \to n \leq m.
207 auto.
208 (*simplify.
209 intros.
210 apply le_S_S_to_le.
211 assumption.*)
212 qed.
213
214 theorem not_le_to_lt: \forall n,m:nat. n \nleq m \to m<n.
215 intros 2.
216 apply (nat_elim2 (\lambda n,m.n \nleq m \to m<n))
217 [ intros.
218   apply (absurd (O \leq n1));auto
219   (*[ apply le_O_n
220   | assumption
221   ]*)
222 | unfold Not.
223   unfold lt.
224   intros.auto
225   (*apply le_S_S.
226   apply le_O_n*)
227 | unfold Not.
228   unfold lt.
229   intros.
230   apply le_S_S.
231   apply H.
232   intros.
233   auto
234   (*apply H1.
235   apply le_S_S.
236   assumption*)
237 ]
238 qed.
239
240 theorem lt_to_not_le: \forall n,m:nat. n<m \to m \nleq n.
241 unfold Not.
242 unfold lt.
243 intros 3.
244 elim H;auto.
245 (*[ apply (not_le_Sn_n n H1)
246 | apply H2.
247   apply lt_to_le. 
248   apply H3
249 ]*)
250 qed.
251
252 theorem not_lt_to_le: \forall n,m:nat. Not (lt n m) \to le m n.
253 simplify.
254 intros.
255 apply lt_S_to_le.
256 apply not_le_to_lt.
257 (*qui auto non chiude il goal*)
258 exact H.
259 qed.
260
261 theorem le_to_not_lt: \forall n,m:nat. le n m \to Not (lt m n).
262 intros.
263 unfold Not.
264 unfold lt.
265 apply lt_to_not_le.
266 unfold lt.auto.
267 (*apply le_S_S.
268 assumption.*)
269 qed.
270
271 (* le elimination *)
272 theorem le_n_O_to_eq : \forall n:nat. n \leq O \to O=n.
273 intro.
274 elim n
275 [ reflexivity
276 | apply False_ind.auto
277   (*apply not_le_Sn_O.
278   goal 17. apply H1.*)
279 ]
280 qed.
281
282 theorem le_n_O_elim: \forall n:nat.n \leq O \to \forall P: nat \to Prop.
283 P O \to P n.
284 intro.
285 elim n
286 [ assumption
287 | apply False_ind.
288   apply  (not_le_Sn_O ? H1)
289 ]
290 qed.
291
292 theorem le_n_Sm_elim : \forall n,m:nat.n \leq S m \to 
293 \forall P:Prop. (S n \leq S m \to P) \to (n=S m \to P) \to P.
294 intros 4.
295 elim H;auto.
296 (*[ apply H2.
297   reflexivity
298 | apply H3. 
299   apply le_S_S. 
300   assumption
301 ]*)
302 qed.
303
304 (* le to eq *)
305 lemma le_to_le_to_eq: \forall n,m. n \le m \to m \le n \to n = m.
306 apply nat_elim2
307 [ intros.
308   auto
309   (*apply le_n_O_to_eq.
310   assumption*)
311 | intros.auto
312   (*apply sym_eq.
313   apply le_n_O_to_eq.
314   assumption*)
315 | intros.
316   apply eq_f.auto
317   (*apply H
318   [ apply le_S_S_to_le.assumption
319   | apply le_S_S_to_le.assumption
320   ]*)
321 ]
322 qed.
323
324 (* lt and le trans *)
325 theorem lt_O_S : \forall n:nat. O < S n.
326 intro.auto.
327 (*unfold.
328 apply le_S_S.
329 apply le_O_n.*)
330 qed.
331
332 theorem lt_to_le_to_lt: \forall n,m,p:nat. lt n m \to le m p \to lt n p.
333 intros.
334 elim H1;auto.
335 (*[ assumption
336 | unfold lt.
337   apply le_S.
338   assumption
339 ]*)
340 qed.
341
342 theorem le_to_lt_to_lt: \forall n,m,p:nat. le n m \to lt m p \to lt n p.
343 intros 4.
344 elim H
345 [ assumption
346 | apply H2.auto
347   (*unfold lt.
348   apply lt_to_le.
349   assumption*)
350 ]
351 qed.
352
353 theorem lt_S_to_lt: \forall n,m. S n < m \to n < m.
354 intros.auto.
355 (*apply (trans_lt ? (S n))
356 [ apply le_n
357 | assumption
358 ]*)
359 qed.
360
361 theorem ltn_to_ltO: \forall n,m:nat. lt n m \to lt O m.
362 intros.
363 apply (le_to_lt_to_lt O n)
364 [ apply le_O_n
365 | assumption
366 ]
367 qed.
368
369 theorem lt_O_n_elim: \forall n:nat. lt O n \to 
370 \forall P:nat\to Prop. (\forall m:nat.P (S m)) \to P n.
371 intro.
372 elim n
373 [ apply False_ind.
374   exact (not_le_Sn_O O H)
375 | apply H2
376 ]
377 qed.
378
379 (* other abstract properties *)
380 theorem antisymmetric_le : antisymmetric nat le.
381 unfold antisymmetric.
382 auto.
383 (*intros 2.
384 apply (nat_elim2 (\lambda n,m.(n \leq m \to m \leq n \to n=m)))
385 [ intros.
386   apply le_n_O_to_eq.
387   assumption
388 | intros.
389   apply False_ind.
390   apply (not_le_Sn_O ? H)
391 | intros.
392   apply eq_f.
393   apply H;
394     apply le_S_S_to_le;assumption
395 ]*)
396 qed.
397
398 (*NOTA:
399  * auto chiude il goal prima della tattica intros 2, tuttavia non chiude gli ultimi
400  * 2 rami aperti dalla tattica apply (nat_elim2 (\lambda n,m.(n \leq m \to m \leq n \to n=m))).
401  * evidentemente auto sfrutta una dimostrazione diversa rispetto a quella proposta
402  * nella libreria
403  *)
404
405 theorem antisym_le: \forall n,m:nat. n \leq m \to m \leq n \to n=m
406 \def antisymmetric_le.
407
408 theorem decidable_le: \forall n,m:nat. decidable (n \leq m).
409 intros.
410 apply (nat_elim2 (\lambda n,m.decidable (n \leq m)))
411 [ intros.
412   unfold decidable.auto
413   (*left.
414   apply le_O_n*)
415 | intros.
416   unfold decidable.
417   auto
418   (*right.
419   exact (not_le_Sn_O n1)*)
420 | intros 2.
421   unfold decidable.
422   intro.
423   elim H
424   [ auto
425     (*left.
426     apply le_S_S.
427     assumption*)
428   | right.
429     unfold Not.
430     auto
431     (*intro.
432     apply H1.
433     apply le_S_S_to_le.
434     assumption*)
435   ]
436 ]
437 qed.
438
439 theorem decidable_lt: \forall n,m:nat. decidable (n < m).
440 intros.
441 (*qui auto non chiude il goal*)
442 exact (decidable_le (S n) m).
443 qed.
444
445 (* well founded induction principles *)
446
447 theorem nat_elim1 : \forall n:nat.\forall P:nat \to Prop. 
448 (\forall m.(\forall p. (p \lt m) \to P p) \to P m) \to P n.
449 intros.
450 cut (\forall q:nat. q \le n \to P q)
451 [ auto
452   (*apply (Hcut n).
453   apply le_n*)
454 | elim n
455   [ apply (le_n_O_elim q H1).
456     apply H.
457     intros.
458     apply False_ind.
459     apply (not_le_Sn_O p H2)
460   | apply H.
461     intros.
462     apply H1.
463     auto
464     (*cut (p < S n1)
465     [ apply lt_S_to_le.
466       assumption
467     | apply (lt_to_le_to_lt p q (S n1) H3 H2).
468     ]*)
469   ]
470 ]
471 qed.
472
473 (* some properties of functions *)
474
475 definition increasing \def \lambda f:nat \to nat. 
476 \forall n:nat. f n < f (S n).
477
478 theorem increasing_to_monotonic: \forall f:nat \to nat.
479 increasing f \to monotonic nat lt f.
480 unfold monotonic.
481 unfold lt.
482 unfold increasing.
483 unfold lt.
484 intros.
485 elim H1;auto.
486 (*[ apply H
487 | apply (trans_le ? (f n1))
488   [ assumption
489   | apply (trans_le ? (S (f n1)))
490     [ apply le_n_Sn
491     | apply H
492     ]
493   ]
494 ]*)
495 qed.
496
497 theorem le_n_fn: \forall f:nat \to nat. (increasing f) 
498 \to \forall n:nat. n \le (f n).
499 intros.
500 elim n;auto.
501 (*[ apply le_O_n
502 | apply (trans_le ? (S (f n1)))
503   [ apply le_S_S.
504     apply H1
505   | simplify in H.
506     unfold increasing in H.
507     unfold lt in H.
508     apply H
509   ]
510 ]*)
511 qed.
512
513 theorem increasing_to_le: \forall f:nat \to nat. (increasing f) 
514 \to \forall m:nat. \exists i. m \le (f i).
515 intros.auto.
516 (*elim m
517 [ apply (ex_intro ? ? O).
518   apply le_O_n
519 | elim H1.
520   apply (ex_intro ? ? (S a)).
521   apply (trans_le ? (S (f a)))
522   [ apply le_S_S.
523     assumption
524   | simplify in H.
525     unfold increasing in H.
526     unfold lt in H.
527     apply H
528   ]
529 ]*)
530 qed.
531
532 theorem increasing_to_le2: \forall f:nat \to nat. (increasing f) 
533 \to \forall m:nat. (f O) \le m \to 
534 \exists i. (f i) \le m \land m <(f (S i)).
535 intros.
536 elim H1
537 [ auto.
538   (*apply (ex_intro ? ? O).
539   split
540   [ apply le_n
541   | apply H
542   ]*)
543 | elim H3.
544   elim H4.  
545   cut ((S n1) < (f (S a)) \lor (S n1) = (f (S a)))
546   [ elim Hcut
547     [ apply (ex_intro ? ? a).
548       auto
549       (*split
550       [ apply le_S.
551         assumption
552       | assumption
553       ]*)
554     | apply (ex_intro ? ? (S a)).
555       split
556       [ rewrite < H7.
557         apply le_n
558       | auto
559         (*rewrite > H7.
560         apply H*)
561       ]
562     ]
563   | auto
564     (*apply le_to_or_lt_eq.
565     apply H6*)
566   ]
567 ]
568 qed.