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