1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/nat/lt_arith".
17 include "nat/div_and_mod.ma".
20 theorem monotonic_lt_plus_r:
21 \forall n:nat.monotonic nat lt (\lambda m.n+m).
23 elim n.simplify.assumption.
25 apply le_S_S.assumption.
28 variant lt_plus_r: \forall n,p,q:nat. p < q \to n + p < n + q \def
31 theorem monotonic_lt_plus_l:
32 \forall n:nat.monotonic nat lt (\lambda m.m+n).
35 rewrite < sym_plus. rewrite < (sym_plus n).
36 apply lt_plus_r.assumption.
39 variant lt_plus_l: \forall n,p,q:nat. p < q \to p + n < q + n \def
42 theorem lt_plus: \forall n,m,p,q:nat. n < m \to p < q \to n + p < m + q.
44 apply (trans_lt ? (n + q)).
45 apply lt_plus_r.assumption.
46 apply lt_plus_l.assumption.
49 theorem lt_plus_to_lt_l :\forall n,p,q:nat. p+n < q+n \to p<q.
52 rewrite > (plus_n_O q).assumption.
54 unfold lt.apply le_S_S_to_le.
56 rewrite > (plus_n_Sm q).
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).
63 rewrite > (sym_plus q).assumption.
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).
69 cut (a \lt c \lor a = c)
74 apply (lt_plus_r c b d).
77 | apply le_to_or_lt_eq.
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.
88 theorem lt_times_eq_O: \forall a,b:nat.
89 O \lt a \to (a * b) = O \to b = O.
96 rewrite > (S_pred a) in H1
98 apply (eq_to_not_lt O ((S (pred a))*(S m)))
101 | apply lt_O_times_S_S
108 theorem O_lt_times_to_O_lt: \forall a,c:nat.
109 O \lt (a * c) \to O \lt a.
121 lemma lt_times_to_lt_O: \forall i,n,m:nat. i < n*m \to O < m.
123 elim (le_to_or_lt_eq O ? (le_O_n m))
127 rewrite < times_n_O in H.
128 apply (not_le_Sn_O ? H)
133 theorem monotonic_lt_times_r:
134 \forall n:nat.monotonic nat lt (\lambda m.(S n)*m).
137 simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption.
138 apply lt_plus.assumption.assumption.
141 (* a simple variant of the previus monotionic_lt_times *)
142 theorem monotonic_lt_times_variant: \forall c:nat.
143 O \lt c \to monotonic nat lt (\lambda t.(t*c)).
145 apply (increasing_to_monotonic).
150 rewrite > plus_n_O in \vdash (? % ?).
155 theorem lt_times_r: \forall n,p,q:nat. p < q \to (S n) * p < (S n) * q
156 \def monotonic_lt_times_r.
158 theorem monotonic_lt_times_l:
159 \forall m:nat.monotonic nat lt (\lambda n.n * (S m)).
162 rewrite < sym_times.rewrite < (sym_times (S m)).
163 apply lt_times_r.assumption.
166 variant lt_times_l: \forall n,p,q:nat. p<q \to p*(S n) < q*(S n)
167 \def monotonic_lt_times_l.
169 theorem lt_times:\forall n,m,p,q:nat. n<m \to p<q \to n*p < m*q.
172 apply (lt_O_n_elim m H).
175 apply (lt_O_n_elim q Hcut).
176 intro.change with (O < (S m1)*(S m2)).
177 apply lt_O_times_S_S.
178 apply (ltn_to_ltO p q H1).
179 apply (trans_lt ? ((S n1)*q)).
180 apply lt_times_r.assumption.
182 apply (lt_O_n_elim q Hcut).
186 apply (ltn_to_ltO p q H2).
190 \forall n,m,p. O < n \to m < p \to n*m < n*p.
192 elim H;apply lt_times_r;assumption.
196 \forall n,m,p. O < n \to m < p \to m*n < p*n.
198 elim H;apply lt_times_l;assumption.
201 theorem lt_to_le_to_lt_times :
202 \forall n,n1,m,m1. n < n1 \to m \le m1 \to O < m1 \to n*m < n1*m1.
204 apply (le_to_lt_to_lt ? (n*m1))
205 [apply le_times_r.assumption
207 [assumption|assumption]
211 theorem lt_times_to_lt_l:
212 \forall n,p,q:nat. p*(S n) < q*(S n) \to p < q.
214 cut (p < q \lor p \nlt q).
217 absurd (p * (S n) < q * (S n)).
223 exact (decidable_lt p q).
226 theorem lt_times_n_to_lt:
227 \forall n,p,q:nat. O < n \to p*n < q*n \to p < q.
230 [intros.apply False_ind.apply (not_le_Sn_n ? H)
231 |intros 4.apply lt_times_to_lt_l
235 theorem lt_times_to_lt_r:
236 \forall n,p,q:nat. (S n)*p < (S n)*q \to lt p q.
238 apply (lt_times_to_lt_l n).
240 rewrite < (sym_times (S n)).
244 theorem lt_times_n_to_lt_r:
245 \forall n,p,q:nat. O < n \to n*p < n*q \to lt p q.
248 [intros.apply False_ind.apply (not_le_Sn_n ? H)
249 |intros 4.apply lt_times_to_lt_r
255 theorem nat_compare_times_l : \forall n,p,q:nat.
256 nat_compare p q = nat_compare ((S n) * p) ((S n) * q).
257 intros.apply nat_compare_elim.intro.
258 apply nat_compare_elim.
261 apply (inj_times_r n).assumption.
262 apply lt_to_not_eq. assumption.
264 apply (lt_times_to_lt_r n).assumption.
265 apply le_to_not_lt.apply lt_to_le.assumption.
266 intro.rewrite < H.rewrite > nat_compare_n_n.reflexivity.
267 intro.apply nat_compare_elim.intro.
269 apply (lt_times_to_lt_r n).assumption.
270 apply le_to_not_lt.apply lt_to_le.assumption.
273 apply (inj_times_r n).assumption.
274 apply lt_to_not_eq.assumption.
279 theorem lt_times_plus_times: \forall a,b,n,m:nat.
280 a < n \to b < m \to a*m + b < n*m.
283 [intros.apply False_ind.apply (not_le_Sn_O ? H)
287 change with (S b+a*m1 \leq m1+m*m1).
291 [apply le_S_S_to_le.assumption
300 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.
301 intros 4.apply (lt_O_n_elim m H).intros.
302 apply (lt_times_to_lt_r m1).
304 rewrite > (plus_n_O ((S m1)*(n / (S m1)))).
310 unfold lt.apply le_S_S.apply le_O_n.
313 theorem lt_div_n_m_n: \forall n,m:nat. (S O) < m \to O < n \to n / m \lt n.
315 apply (nat_case1 (n / m)).intro.
316 assumption.intros.rewrite < H2.
317 rewrite > (div_mod n m) in \vdash (? ? %).
318 apply (lt_to_le_to_lt ? ((n / m)*m)).
319 apply (lt_to_le_to_lt ? ((n / m)*(S (S O)))).
332 apply (trans_lt ? (S O)).
333 unfold lt. apply le_n.assumption.
336 theorem eq_div_div_div_times: \forall n,m,q. O < n \to O < m \to
339 apply (div_mod_spec_to_eq q (n*m) ? (q\mod n+n*(q/n\mod m)) ? (mod q (n*m)))
340 [apply div_mod_spec_intro
341 [apply (lt_to_le_to_lt ? (n*(S (q/n\mod m))))
342 [rewrite < times_n_Sm.
350 |rewrite > sym_times in ⊢ (? ? ? (? (? ? %) ?)).
351 rewrite < assoc_times.
352 rewrite > (eq_times_div_minus_mod ? ? H1).
354 rewrite > distributive_times_minus.
356 rewrite > (eq_times_div_minus_mod ? ? H).
357 rewrite < sym_plus in ⊢ (? ? ? (? ? %)).
358 rewrite < assoc_plus.
359 rewrite < plus_minus_m_m
360 [rewrite < plus_minus_m_m
362 |apply (eq_plus_to_le ? ? ((q/n)*n)).
367 |apply (trans_le ? (n*(q/n)))
369 apply (eq_plus_to_le ? ? ((q/n)/m*m)).
373 |rewrite > sym_times.
374 rewrite > eq_times_div_minus_mod
381 |apply div_mod_spec_div_mod.
382 rewrite > (times_n_O O).
383 apply lt_times;assumption
387 theorem eq_div_div_div_div: \forall n,m,q. O < n \to O < m \to
390 apply (trans_eq ? ? (q/(n*m)))
391 [apply eq_div_div_div_times;assumption
392 |rewrite > sym_times.
394 apply eq_div_div_div_times;assumption
398 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)).
400 rewrite < (lt_O_to_div_times n (S(S O))) in ⊢ (? ? ? (? (? (? % ?) ?) ?))
401 [rewrite > eq_div_div_div_div
402 [rewrite > sym_times in ⊢ (? ? ? (? (? (? (? % ?) ?) ?) ?)).
411 (* Forall a,b : N. 0 < b \to b * (a/b) <= a < b * (a/b +1) *)
412 (* The theorem is shown in two different parts: *)
414 theorem lt_to_div_to_and_le_times_lt_S: \forall a,b,c:nat.
415 O \lt b \to a/b = c \to (b*c \le a \land a \lt b*(S c)).
420 rewrite > eq_times_div_minus_mod
421 [ apply (le_minus_m a (a \mod b))
424 | rewrite < (times_n_Sm b c).
427 rewrite > (div_mod a b) in \vdash (? % ?)
428 [ rewrite > (sym_plus b ((a/b)*b)).
437 theorem lt_to_le_times_to_lt_S_to_div: \forall a,c,b:nat.
438 O \lt b \to (b*c) \le a \to a \lt (b*(S c)) \to a/b = c.
440 apply (le_to_le_to_eq)
441 [ apply (leb_elim (a/b) c);intros
445 apply (lt_to_not_le (a \mod b) O)
446 [ apply (lt_plus_to_lt_l ((a/b)*b)).
450 [ apply (lt_to_le_to_lt ? (b*(S c)) ?)
452 | rewrite > (sym_times (a/b) b).
460 | apply not_le_to_lt.
464 | apply (leb_elim c (a/b));intros
468 apply (lt_to_not_le (a \mod b) b)
469 [ apply (lt_mod_m_m).
471 | apply (le_plus_to_le ((a/b)*b)).
472 rewrite < (div_mod a b)
473 [ apply (trans_le ? (b*c) ?)
474 [ rewrite > (sym_times (a/b) b).
475 rewrite > (times_n_SO b) in \vdash (? (? ? %) ?).
476 rewrite < distr_times_plus.
478 simplify in \vdash (? (? ? %) ?).
486 | apply not_le_to_lt.
494 theorem lt_to_lt_to_eq_div_div_times_times: \forall a,b,c:nat.
495 O \lt c \to O \lt b \to (a/b) = (a*c)/(b*c).
498 cut (b*(a/b) \le a \land a \lt b*(S (a/b)))
500 apply lt_to_le_times_to_lt_S_to_div
501 [ rewrite > (S_pred b)
502 [ rewrite > (S_pred c)
503 [ apply (lt_O_times_S_S)
508 | rewrite > assoc_times.
509 rewrite > (sym_times c (a/b)).
510 rewrite < assoc_times.
511 rewrite > (sym_times (b*(a/b)) c).
512 rewrite > (sym_times a c).
513 apply (le_times_r c (b*(a/b)) a).
515 | rewrite > (sym_times a c).
516 rewrite > (assoc_times ).
517 rewrite > (sym_times c (S (a/b))).
518 rewrite < (assoc_times).
519 rewrite > (sym_times (b*(S (a/b))) c).
520 apply (lt_times_r1 c a (b*(S (a/b))));
523 | apply (lt_to_div_to_and_le_times_lt_S)
530 theorem times_mod: \forall a,b,c:nat.
531 O \lt c \to O \lt b \to ((a*c) \mod (b*c)) = c*(a\mod b).
533 apply (div_mod_spec_to_eq2 (a*c) (b*c) (a/b) ((a*c) \mod (b*c)) (a/b) (c*(a \mod b)))
534 [ rewrite > (lt_to_lt_to_eq_div_div_times_times a b c)
535 [ apply div_mod_spec_div_mod.
537 [ rewrite > (S_pred c)
538 [ apply lt_O_times_S_S
546 | apply div_mod_spec_intro
547 [ rewrite > (sym_times b c).
548 apply (lt_times_r1 c)
550 | apply (lt_mod_m_m).
553 | rewrite < (assoc_times (a/b) b c).
554 rewrite > (sym_times a c).
555 rewrite > (sym_times ((a/b)*b) c).
556 rewrite < (distr_times_plus c ? ?).
567 (* general properties of functions *)
568 theorem monotonic_to_injective: \forall f:nat\to nat.
569 monotonic nat lt f \to injective nat nat f.
570 unfold injective.intros.
571 apply (nat_compare_elim x y).
572 intro.apply False_ind.apply (not_le_Sn_n (f x)).
573 rewrite > H1 in \vdash (? ? %).
574 change with (f x < f y).
577 intro.apply False_ind.apply (not_le_Sn_n (f y)).
578 rewrite < H1 in \vdash (? ? %).
579 change with (f y < f x).
583 theorem increasing_to_injective: \forall f:nat\to nat.
584 increasing f \to injective nat nat f.
585 intros.apply monotonic_to_injective.
586 apply increasing_to_monotonic.assumption.