]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/lt_arith.ma
Towards chebyshev.
[helm.git] / helm / software / matita / library / nat / lt_arith.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/nat/lt_arith".
16
17 include "nat/div_and_mod.ma".
18
19 (* plus *)
20 theorem monotonic_lt_plus_r: 
21 \forall n:nat.monotonic nat lt (\lambda m.n+m).
22 simplify.intros.
23 elim n.simplify.assumption.
24 simplify.unfold lt.
25 apply le_S_S.assumption.
26 qed.
27
28 variant lt_plus_r: \forall n,p,q:nat. p < q \to n + p < n + q \def
29 monotonic_lt_plus_r.
30
31 theorem monotonic_lt_plus_l: 
32 \forall n:nat.monotonic nat lt (\lambda m.m+n).
33 simplify.
34 intros.
35 rewrite < sym_plus. rewrite < (sym_plus n).
36 apply lt_plus_r.assumption.
37 qed.
38
39 variant lt_plus_l: \forall n,p,q:nat. p < q \to p + n < q + n \def
40 monotonic_lt_plus_l.
41
42 theorem lt_plus: \forall n,m,p,q:nat. n < m \to p < q \to n + p < m + q.
43 intros.
44 apply (trans_lt ? (n + q)).
45 apply lt_plus_r.assumption.
46 apply lt_plus_l.assumption.
47 qed.
48
49 theorem lt_plus_to_lt_l :\forall n,p,q:nat. p+n < q+n \to p<q.
50 intro.elim n.
51 rewrite > plus_n_O.
52 rewrite > (plus_n_O q).assumption.
53 apply H.
54 unfold lt.apply le_S_S_to_le.
55 rewrite > plus_n_Sm.
56 rewrite > (plus_n_Sm q).
57 exact H1.
58 qed.
59
60 theorem lt_plus_to_lt_r :\forall n,p,q:nat. n+p < n+q \to p<q.
61 intros.apply (lt_plus_to_lt_l n). 
62 rewrite > sym_plus.
63 rewrite > (sym_plus q).assumption.
64 qed.
65
66 theorem le_to_lt_to_plus_lt: \forall a,b,c,d:nat.
67 a \le c \to b \lt d \to (a + b) \lt (c+d).
68 intros.
69 cut (a \lt c \lor a = c)
70 [ elim Hcut
71   [ apply (lt_plus );
72       assumption
73   | rewrite > H2.
74     apply (lt_plus_r c b d).
75     assumption
76   ]
77 | apply le_to_or_lt_eq.
78   assumption
79 ]
80 qed.
81
82
83 (* times and zero *)
84 theorem lt_O_times_S_S: \forall n,m:nat.O < (S n)*(S m).
85 intros.simplify.unfold lt.apply le_S_S.apply le_O_n.
86 qed.
87
88 theorem lt_times_eq_O: \forall a,b:nat.
89 O \lt a \to (a * b) = O \to b = O.
90 intros.
91 apply (nat_case1 b)
92 [ intros.
93   reflexivity
94 | intros.
95   rewrite > H2 in H1.
96   rewrite > (S_pred a) in H1
97   [ apply False_ind.
98     apply (eq_to_not_lt O ((S (pred a))*(S m)))
99     [ apply sym_eq.
100       assumption
101     | apply lt_O_times_S_S
102     ]
103   | assumption
104   ]
105 ]
106 qed.
107
108 theorem O_lt_times_to_O_lt: \forall a,c:nat.
109 O \lt (a * c) \to O \lt a.
110 intros.
111 apply (nat_case1 a)
112 [ intros.
113   rewrite > H1 in H.
114   simplify in H.
115   assumption
116 | intros.
117   apply lt_O_S
118 ]
119 qed.
120
121 (* times *)
122 theorem monotonic_lt_times_r: 
123 \forall n:nat.monotonic nat lt (\lambda m.(S n)*m).
124 simplify.
125 intros.elim n.
126 simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption.
127 apply lt_plus.assumption.assumption.
128 qed.
129
130 (* a simple variant of the previus monotionic_lt_times *)
131 theorem monotonic_lt_times_variant: \forall c:nat.
132 O \lt c \to monotonic nat lt (\lambda t.(t*c)).
133 intros.
134 apply (increasing_to_monotonic).
135 unfold increasing.
136 intros.
137 simplify.
138 rewrite > sym_plus.
139 rewrite > plus_n_O in \vdash (? % ?).
140 apply lt_plus_r.
141 assumption.
142 qed.
143
144 theorem lt_times_r: \forall n,p,q:nat. p < q \to (S n) * p < (S n) * q
145 \def monotonic_lt_times_r.
146
147 theorem monotonic_lt_times_l: 
148 \forall m:nat.monotonic nat lt (\lambda n.n * (S m)).
149 simplify.
150 intros.
151 rewrite < sym_times.rewrite < (sym_times (S m)).
152 apply lt_times_r.assumption.
153 qed.
154
155 variant lt_times_l: \forall n,p,q:nat. p<q \to p*(S n) < q*(S n)
156 \def monotonic_lt_times_l.
157
158 theorem lt_times:\forall n,m,p,q:nat. n<m \to p<q \to n*p < m*q.
159 intro.
160 elim n.
161 apply (lt_O_n_elim m H).
162 intro.
163 cut (lt O q).
164 apply (lt_O_n_elim q Hcut).
165 intro.change with (O < (S m1)*(S m2)).
166 apply lt_O_times_S_S.
167 apply (ltn_to_ltO p q H1).
168 apply (trans_lt ? ((S n1)*q)).
169 apply lt_times_r.assumption.
170 cut (lt O q).
171 apply (lt_O_n_elim q Hcut).
172 intro.
173 apply lt_times_l.
174 assumption.
175 apply (ltn_to_ltO p q H2).
176 qed.
177
178 theorem lt_times_r1: 
179 \forall n,m,p. O < n \to m < p \to n*m < n*p.
180 intros.
181 elim H;apply lt_times_r;assumption.
182 qed.
183
184 theorem lt_times_l1: 
185 \forall n,m,p. O < n \to m < p \to m*n < p*n.
186 intros.
187 elim H;apply lt_times_l;assumption.
188 qed.
189
190 theorem lt_to_le_to_lt_times : 
191 \forall n,n1,m,m1. n < n1 \to m \le m1 \to O < m1 \to n*m < n1*m1.
192 intros.
193 apply (le_to_lt_to_lt ? (n*m1))
194   [apply le_times_r.assumption
195   |apply lt_times_l1
196     [assumption|assumption]
197   ]
198 qed.
199
200 theorem lt_times_to_lt_l: 
201 \forall n,p,q:nat. p*(S n) < q*(S n) \to p < q.
202 intros.
203 cut (p < q \lor p \nlt q).
204 elim Hcut.
205 assumption.
206 absurd (p * (S n) < q * (S n)).
207 assumption.
208 apply le_to_not_lt.
209 apply le_times_l.
210 apply not_lt_to_le.
211 assumption.
212 exact (decidable_lt p q).
213 qed.
214
215 theorem lt_times_n_to_lt: 
216 \forall n,p,q:nat. O < n \to p*n < q*n \to p < q.
217 intro.
218 apply (nat_case n)
219   [intros.apply False_ind.apply (not_le_Sn_n ? H)
220   |intros 4.apply lt_times_to_lt_l
221   ]
222 qed.
223
224 theorem lt_times_to_lt_r: 
225 \forall n,p,q:nat. (S n)*p < (S n)*q \to lt p q.
226 intros.
227 apply (lt_times_to_lt_l n).
228 rewrite < sym_times.
229 rewrite < (sym_times (S n)).
230 assumption.
231 qed.
232
233 theorem lt_times_n_to_lt_r: 
234 \forall n,p,q:nat. O < n \to n*p < n*q \to lt p q.
235 intro.
236 apply (nat_case n)
237   [intros.apply False_ind.apply (not_le_Sn_n ? H)
238   |intros 4.apply lt_times_to_lt_r
239   ]
240 qed.
241
242 theorem le_times_to_le_div: \forall a,b,c:nat.
243 O \lt b \to (b*c) \le a \to c \le (a /b).
244 intros.
245 apply lt_S_to_le.
246 apply (lt_times_n_to_lt b)
247   [assumption
248   |rewrite > sym_times.
249    apply (le_to_lt_to_lt ? a)
250     [assumption
251     |simplify.
252      rewrite > sym_plus.
253      rewrite > (div_mod a b) in ⊢ (? % ?)
254       [apply lt_plus_r.
255        apply lt_mod_m_m.
256        assumption
257       |assumption
258       ]
259     ]
260   ]
261 qed.
262
263 theorem nat_compare_times_l : \forall n,p,q:nat. 
264 nat_compare p q = nat_compare ((S n) * p) ((S n) * q).
265 intros.apply nat_compare_elim.intro.
266 apply nat_compare_elim.
267 intro.reflexivity.
268 intro.absurd (p=q).
269 apply (inj_times_r n).assumption.
270 apply lt_to_not_eq. assumption.
271 intro.absurd (q<p).
272 apply (lt_times_to_lt_r n).assumption.
273 apply le_to_not_lt.apply lt_to_le.assumption.
274 intro.rewrite < H.rewrite > nat_compare_n_n.reflexivity.
275 intro.apply nat_compare_elim.intro.
276 absurd (p<q).
277 apply (lt_times_to_lt_r n).assumption.
278 apply le_to_not_lt.apply lt_to_le.assumption.
279 intro.absurd (q=p).
280 symmetry.
281 apply (inj_times_r n).assumption.
282 apply lt_to_not_eq.assumption.
283 intro.reflexivity.
284 qed.
285
286 (* times and plus *)
287 theorem lt_times_plus_times: \forall a,b,n,m:nat. 
288 a < n \to b < m \to a*m + b < n*m.
289 intros 3.
290 apply (nat_case n)
291   [intros.apply False_ind.apply (not_le_Sn_O ? H)
292   |intros.simplify.
293    rewrite < sym_plus.
294    unfold.
295    change with (S b+a*m1 \leq m1+m*m1).
296    apply le_plus
297     [assumption
298     |apply le_times
299       [apply le_S_S_to_le.assumption
300       |apply le_n
301       ]
302     ]
303   ]
304 qed.
305
306 (* div *) 
307
308 theorem eq_mod_O_to_lt_O_div: \forall n,m:nat. O < m \to O < n\to n \mod m = O \to O < n / m. 
309 intros 4.apply (lt_O_n_elim m H).intros.
310 apply (lt_times_to_lt_r m1).
311 rewrite < times_n_O.
312 rewrite > (plus_n_O ((S m1)*(n / (S m1)))).
313 rewrite < H2.
314 rewrite < sym_times.
315 rewrite < div_mod.
316 rewrite > H2.
317 assumption.
318 unfold lt.apply le_S_S.apply le_O_n.
319 qed.
320
321 theorem lt_div_n_m_n: \forall n,m:nat. (S O) < m \to O < n \to n / m \lt n.
322 intros.
323 apply (nat_case1 (n / m)).intro.
324 assumption.intros.rewrite < H2.
325 rewrite > (div_mod n m) in \vdash (? ? %).
326 apply (lt_to_le_to_lt ? ((n / m)*m)).
327 apply (lt_to_le_to_lt ? ((n / m)*(S (S O)))).
328 rewrite < sym_times.
329 rewrite > H2.
330 simplify.unfold lt.
331 rewrite < plus_n_O.
332 rewrite < plus_n_Sm.
333 apply le_S_S.
334 apply le_S_S.
335 apply le_plus_n.
336 apply le_times_r.
337 assumption.
338 rewrite < sym_plus.
339 apply le_plus_n.
340 apply (trans_lt ? (S O)).
341 unfold lt. apply le_n.assumption.
342 qed.
343
344 theorem eq_div_div_div_times: \forall n,m,q. O < n \to O < m \to
345 q/n/m = q/(n*m).
346 intros.
347 apply (div_mod_spec_to_eq q (n*m) ? (q\mod n+n*(q/n\mod m)) ? (mod q (n*m)))
348   [apply div_mod_spec_intro
349     [apply (lt_to_le_to_lt ? (n*(S (q/n\mod m))))
350       [rewrite < times_n_Sm.
351        apply lt_plus_l.
352        apply lt_mod_m_m.
353        assumption
354       |apply le_times_r.
355        apply lt_mod_m_m.
356        assumption
357       ]
358     |rewrite > sym_times in ⊢ (? ? ? (? (? ? %) ?)).
359      rewrite < assoc_times.
360      rewrite > (eq_times_div_minus_mod ? ? H1).
361      rewrite > sym_times.
362      rewrite > distributive_times_minus.
363      rewrite > sym_times.
364      rewrite > (eq_times_div_minus_mod ? ? H).
365      rewrite < sym_plus in ⊢ (? ? ? (? ? %)).
366      rewrite < assoc_plus.
367      rewrite < plus_minus_m_m
368       [rewrite < plus_minus_m_m
369         [reflexivity
370         |apply (eq_plus_to_le ? ? ((q/n)*n)).
371          rewrite < sym_plus.
372          apply div_mod.
373          assumption
374         ]
375       |apply (trans_le ? (n*(q/n)))
376         [apply le_times_r.
377          apply (eq_plus_to_le ? ? ((q/n)/m*m)).
378          rewrite < sym_plus.
379          apply div_mod.
380          assumption
381         |rewrite > sym_times.
382          rewrite > eq_times_div_minus_mod
383           [apply le_n
384           |assumption
385           ]
386         ]
387       ]
388     ]
389   |apply div_mod_spec_div_mod.
390    rewrite > (times_n_O O).
391    apply lt_times;assumption
392   ]
393 qed.
394
395 theorem eq_div_div_div_div: \forall n,m,q. O < n \to O < m \to
396 q/n/m = q/m/n.
397 intros.
398 apply (trans_eq ? ? (q/(n*m)))
399   [apply eq_div_div_div_times;assumption
400   |rewrite > sym_times.
401    apply sym_eq.
402    apply eq_div_div_div_times;assumption
403   ]
404 qed.
405
406 theorem SSO_mod: \forall n,m. O < m \to (S(S O))*n/m = (n/m)*(S(S O)) + mod ((S(S O))*n/m) (S(S O)).
407 intros.
408 rewrite < (lt_O_to_div_times n (S(S O))) in ⊢ (? ? ? (? (? (? % ?) ?) ?))
409   [rewrite > eq_div_div_div_div
410     [rewrite > sym_times in ⊢ (? ? ? (? (? (? (? % ?) ?) ?) ?)).
411      apply div_mod.
412      apply lt_O_S
413     |apply lt_O_S
414     |assumption
415     ]
416   |apply lt_O_S
417   ]
418 qed.
419 (* Forall a,b : N. 0 < b \to b * (a/b) <= a < b * (a/b +1) *)
420 (* The theorem is shown in two different parts: *)
421
422 theorem lt_to_div_to_and_le_times_lt_S: \forall a,b,c:nat.
423 O \lt b \to a/b = c \to (b*c \le a \land a \lt b*(S c)).
424 intros.
425 split
426 [ rewrite < H1.
427   rewrite > sym_times.
428   rewrite > eq_times_div_minus_mod
429   [ apply (le_minus_m a (a \mod b))
430   | assumption
431   ]
432 | rewrite < (times_n_Sm b c).
433   rewrite < H1.
434   rewrite > sym_times.
435   rewrite > (div_mod a b) in \vdash (? % ?)
436   [ rewrite > (sym_plus b ((a/b)*b)).
437     apply lt_plus_r.
438     apply lt_mod_m_m.
439     assumption
440   | assumption
441   ]
442 ]
443 qed.
444
445 theorem lt_to_le_times_to_lt_S_to_div: \forall a,c,b:nat.
446 O \lt b \to (b*c) \le a \to a \lt (b*(S c)) \to a/b = c.
447 intros.
448 apply (le_to_le_to_eq)
449 [ apply (leb_elim (a/b) c);intros
450   [ assumption
451   | cut (c \lt (a/b))
452     [ apply False_ind.
453       apply (lt_to_not_le (a \mod b) O)
454       [ apply (lt_plus_to_lt_l ((a/b)*b)).
455         simplify.
456         rewrite < sym_plus.
457         rewrite < div_mod
458         [ apply (lt_to_le_to_lt ? (b*(S c)) ?)
459           [ assumption
460           | rewrite > (sym_times (a/b) b).
461             apply le_times_r.
462             assumption
463           ]
464         | assumption
465         ]
466       | apply le_O_n
467       ]
468     | apply not_le_to_lt.
469       assumption
470     ]
471   ]
472 | apply (leb_elim c (a/b));intros
473   [ assumption
474   | cut((a/b) \lt c) 
475     [ apply False_ind.
476       apply (lt_to_not_le (a \mod b) b)
477       [ apply (lt_mod_m_m).
478         assumption
479       | apply (le_plus_to_le ((a/b)*b)).
480         rewrite < (div_mod a b)
481         [ apply (trans_le ? (b*c) ?)
482           [ rewrite > (sym_times (a/b) b).
483             rewrite > (times_n_SO b) in \vdash (? (? ? %) ?).
484             rewrite < distr_times_plus.
485             rewrite > sym_plus.
486             simplify in \vdash (? (? ? %) ?).
487             apply le_times_r.
488             assumption
489           | assumption
490           ]
491         | assumption
492         ]
493       ]
494     | apply not_le_to_lt. 
495       assumption
496     ]
497   ]
498 ]
499 qed.
500
501
502 theorem lt_to_lt_to_eq_div_div_times_times: \forall a,b,c:nat. 
503 O \lt c \to O \lt b \to (a/b) = (a*c)/(b*c).
504 intros.
505 apply sym_eq.
506 cut (b*(a/b) \le a \land a \lt b*(S (a/b)))
507 [ elim Hcut.
508   apply lt_to_le_times_to_lt_S_to_div
509   [ rewrite > (S_pred b)
510     [ rewrite > (S_pred c)
511       [ apply (lt_O_times_S_S)
512       | assumption
513       ]
514     | assumption
515     ]
516   | rewrite > assoc_times.
517     rewrite > (sym_times c (a/b)).
518     rewrite < assoc_times.
519     rewrite > (sym_times (b*(a/b)) c).
520     rewrite > (sym_times a c).
521     apply (le_times_r c (b*(a/b)) a).
522     assumption
523   | rewrite > (sym_times a c).
524     rewrite > (assoc_times ).
525     rewrite > (sym_times c (S (a/b))).
526     rewrite < (assoc_times).
527     rewrite > (sym_times (b*(S (a/b))) c).
528     apply (lt_times_r1 c a (b*(S (a/b))));
529       assumption    
530   ]
531 | apply (lt_to_div_to_and_le_times_lt_S)
532   [ assumption
533   | reflexivity
534   ]
535 ]
536 qed.
537
538 theorem times_mod: \forall a,b,c:nat.
539 O \lt c \to O \lt b \to ((a*c) \mod (b*c)) = c*(a\mod b).
540 intros.
541 apply (div_mod_spec_to_eq2 (a*c) (b*c) (a/b) ((a*c) \mod (b*c)) (a/b) (c*(a \mod b)))
542 [ rewrite > (lt_to_lt_to_eq_div_div_times_times a b c)
543   [ apply div_mod_spec_div_mod.
544     rewrite > (S_pred b)
545     [ rewrite > (S_pred c)
546       [ apply lt_O_times_S_S
547       | assumption
548       ]
549     | assumption
550     ]
551   | assumption
552   | assumption
553   ]
554 | apply div_mod_spec_intro
555   [ rewrite > (sym_times b c).
556     apply (lt_times_r1 c)
557     [ assumption
558     | apply (lt_mod_m_m).
559       assumption
560     ]
561   | rewrite < (assoc_times (a/b) b c).
562     rewrite > (sym_times a c).
563     rewrite > (sym_times ((a/b)*b) c).
564     rewrite < (distr_times_plus c ? ?).
565     apply eq_f.
566     apply (div_mod a b).
567     assumption
568   ]
569 ]
570 qed.
571
572
573
574
575 (* general properties of functions *)
576 theorem monotonic_to_injective: \forall f:nat\to nat.
577 monotonic nat lt f \to injective nat nat f.
578 unfold injective.intros.
579 apply (nat_compare_elim x y).
580 intro.apply False_ind.apply (not_le_Sn_n (f x)).
581 rewrite > H1 in \vdash (? ? %).
582 change with (f x < f y).
583 apply H.apply H2.
584 intros.assumption.
585 intro.apply False_ind.apply (not_le_Sn_n (f y)).
586 rewrite < H1 in \vdash (? ? %).
587 change with (f y < f x).
588 apply H.apply H2.
589 qed.
590
591 theorem increasing_to_injective: \forall f:nat\to nat.
592 increasing f \to injective nat nat f.
593 intros.apply monotonic_to_injective.
594 apply increasing_to_monotonic.assumption.
595 qed.
596