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.
122 theorem monotonic_lt_times_r:
123 \forall n:nat.monotonic nat lt (\lambda m.(S n)*m).
126 simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption.
127 apply lt_plus.assumption.assumption.
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)).
134 apply (increasing_to_monotonic).
139 rewrite > plus_n_O in \vdash (? % ?).
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.
147 theorem monotonic_lt_times_l:
148 \forall m:nat.monotonic nat lt (\lambda n.n * (S m)).
151 rewrite < sym_times.rewrite < (sym_times (S m)).
152 apply lt_times_r.assumption.
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.
158 theorem lt_times:\forall n,m,p,q:nat. n<m \to p<q \to n*p < m*q.
161 apply (lt_O_n_elim m H).
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.
171 apply (lt_O_n_elim q Hcut).
175 apply (ltn_to_ltO p q H2).
179 \forall n,m,p. O < n \to m < p \to n*m < n*p.
181 elim H;apply lt_times_r;assumption.
185 \forall n,m,p. O < n \to m < p \to m*n < p*n.
187 elim H;apply lt_times_l;assumption.
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.
193 apply (le_to_lt_to_lt ? (n*m1))
194 [apply le_times_r.assumption
196 [assumption|assumption]
200 theorem lt_times_to_lt_l:
201 \forall n,p,q:nat. p*(S n) < q*(S n) \to p < q.
203 cut (p < q \lor p \nlt q).
206 absurd (p * (S n) < q * (S n)).
212 exact (decidable_lt p q).
215 theorem lt_times_n_to_lt:
216 \forall n,p,q:nat. O < n \to p*n < q*n \to p < q.
219 [intros.apply False_ind.apply (not_le_Sn_n ? H)
220 |intros 4.apply lt_times_to_lt_l
224 theorem lt_times_to_lt_r:
225 \forall n,p,q:nat. (S n)*p < (S n)*q \to lt p q.
227 apply (lt_times_to_lt_l n).
229 rewrite < (sym_times (S n)).
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.
237 [intros.apply False_ind.apply (not_le_Sn_n ? H)
238 |intros 4.apply lt_times_to_lt_r
244 theorem nat_compare_times_l : \forall n,p,q:nat.
245 nat_compare p q = nat_compare ((S n) * p) ((S n) * q).
246 intros.apply nat_compare_elim.intro.
247 apply nat_compare_elim.
250 apply (inj_times_r n).assumption.
251 apply lt_to_not_eq. assumption.
253 apply (lt_times_to_lt_r n).assumption.
254 apply le_to_not_lt.apply lt_to_le.assumption.
255 intro.rewrite < H.rewrite > nat_compare_n_n.reflexivity.
256 intro.apply nat_compare_elim.intro.
258 apply (lt_times_to_lt_r n).assumption.
259 apply le_to_not_lt.apply lt_to_le.assumption.
262 apply (inj_times_r n).assumption.
263 apply lt_to_not_eq.assumption.
268 theorem lt_times_plus_times: \forall a,b,n,m:nat.
269 a < n \to b < m \to a*m + b < n*m.
272 [intros.apply False_ind.apply (not_le_Sn_O ? H)
276 change with (S b+a*m1 \leq m1+m*m1).
280 [apply le_S_S_to_le.assumption
289 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.
290 intros 4.apply (lt_O_n_elim m H).intros.
291 apply (lt_times_to_lt_r m1).
293 rewrite > (plus_n_O ((S m1)*(n / (S m1)))).
299 unfold lt.apply le_S_S.apply le_O_n.
302 theorem lt_div_n_m_n: \forall n,m:nat. (S O) < m \to O < n \to n / m \lt n.
304 apply (nat_case1 (n / m)).intro.
305 assumption.intros.rewrite < H2.
306 rewrite > (div_mod n m) in \vdash (? ? %).
307 apply (lt_to_le_to_lt ? ((n / m)*m)).
308 apply (lt_to_le_to_lt ? ((n / m)*(S (S O)))).
321 apply (trans_lt ? (S O)).
322 unfold lt. apply le_n.assumption.
325 theorem eq_div_div_div_times: \forall n,m,q. O < n \to O < m \to
328 apply (div_mod_spec_to_eq q (n*m) ? (q\mod n+n*(q/n\mod m)) ? (mod q (n*m)))
329 [apply div_mod_spec_intro
330 [apply (lt_to_le_to_lt ? (n*(S (q/n\mod m))))
331 [rewrite < times_n_Sm.
339 |rewrite > sym_times in ⊢ (? ? ? (? (? ? %) ?)).
340 rewrite < assoc_times.
341 rewrite > (eq_times_div_minus_mod ? ? H1).
343 rewrite > distributive_times_minus.
345 rewrite > (eq_times_div_minus_mod ? ? H).
346 rewrite < sym_plus in ⊢ (? ? ? (? ? %)).
347 rewrite < assoc_plus.
348 rewrite < plus_minus_m_m
349 [rewrite < plus_minus_m_m
351 |apply (eq_plus_to_le ? ? ((q/n)*n)).
356 |apply (trans_le ? (n*(q/n)))
358 apply (eq_plus_to_le ? ? ((q/n)/m*m)).
362 |rewrite > sym_times.
363 rewrite > eq_times_div_minus_mod
370 |apply div_mod_spec_div_mod.
371 rewrite > (times_n_O O).
372 apply lt_times;assumption
376 theorem eq_div_div_div_div: \forall n,m,q. O < n \to O < m \to
379 apply (trans_eq ? ? (q/(n*m)))
380 [apply eq_div_div_div_times;assumption
381 |rewrite > sym_times.
383 apply eq_div_div_div_times;assumption
387 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)).
389 rewrite < (lt_O_to_div_times n (S(S O))) in ⊢ (? ? ? (? (? (? % ?) ?) ?))
390 [rewrite > eq_div_div_div_div
391 [rewrite > sym_times in ⊢ (? ? ? (? (? (? (? % ?) ?) ?) ?)).
400 (* Forall a,b : N. 0 < b \to b * (a/b) <= a < b * (a/b +1) *)
401 (* The theorem is shown in two different parts: *)
403 theorem lt_to_div_to_and_le_times_lt_S: \forall a,b,c:nat.
404 O \lt b \to a/b = c \to (b*c \le a \land a \lt b*(S c)).
409 rewrite > eq_times_div_minus_mod
410 [ apply (le_minus_m a (a \mod b))
413 | rewrite < (times_n_Sm b c).
416 rewrite > (div_mod a b) in \vdash (? % ?)
417 [ rewrite > (sym_plus b ((a/b)*b)).
426 theorem lt_to_le_times_to_lt_S_to_div: \forall a,c,b:nat.
427 O \lt b \to (b*c) \le a \to a \lt (b*(S c)) \to a/b = c.
429 apply (le_to_le_to_eq)
430 [ apply (leb_elim (a/b) c);intros
434 apply (lt_to_not_le (a \mod b) O)
435 [ apply (lt_plus_to_lt_l ((a/b)*b)).
439 [ apply (lt_to_le_to_lt ? (b*(S c)) ?)
441 | rewrite > (sym_times (a/b) b).
449 | apply not_le_to_lt.
453 | apply (leb_elim c (a/b));intros
457 apply (lt_to_not_le (a \mod b) b)
458 [ apply (lt_mod_m_m).
460 | apply (le_plus_to_le ((a/b)*b)).
461 rewrite < (div_mod a b)
462 [ apply (trans_le ? (b*c) ?)
463 [ rewrite > (sym_times (a/b) b).
464 rewrite > (times_n_SO b) in \vdash (? (? ? %) ?).
465 rewrite < distr_times_plus.
467 simplify in \vdash (? (? ? %) ?).
475 | apply not_le_to_lt.
483 theorem lt_to_lt_to_eq_div_div_times_times: \forall a,b,c:nat.
484 O \lt c \to O \lt b \to (a/b) = (a*c)/(b*c).
487 cut (b*(a/b) \le a \land a \lt b*(S (a/b)))
489 apply lt_to_le_times_to_lt_S_to_div
490 [ rewrite > (S_pred b)
491 [ rewrite > (S_pred c)
492 [ apply (lt_O_times_S_S)
497 | rewrite > assoc_times.
498 rewrite > (sym_times c (a/b)).
499 rewrite < assoc_times.
500 rewrite > (sym_times (b*(a/b)) c).
501 rewrite > (sym_times a c).
502 apply (le_times_r c (b*(a/b)) a).
504 | rewrite > (sym_times a c).
505 rewrite > (assoc_times ).
506 rewrite > (sym_times c (S (a/b))).
507 rewrite < (assoc_times).
508 rewrite > (sym_times (b*(S (a/b))) c).
509 apply (lt_times_r1 c a (b*(S (a/b))));
512 | apply (lt_to_div_to_and_le_times_lt_S)
519 theorem times_mod: \forall a,b,c:nat.
520 O \lt c \to O \lt b \to ((a*c) \mod (b*c)) = c*(a\mod b).
522 apply (div_mod_spec_to_eq2 (a*c) (b*c) (a/b) ((a*c) \mod (b*c)) (a/b) (c*(a \mod b)))
523 [ rewrite > (lt_to_lt_to_eq_div_div_times_times a b c)
524 [ apply div_mod_spec_div_mod.
526 [ rewrite > (S_pred c)
527 [ apply lt_O_times_S_S
535 | apply div_mod_spec_intro
536 [ rewrite > (sym_times b c).
537 apply (lt_times_r1 c)
539 | apply (lt_mod_m_m).
542 | rewrite < (assoc_times (a/b) b c).
543 rewrite > (sym_times a c).
544 rewrite > (sym_times ((a/b)*b) c).
545 rewrite < (distr_times_plus c ? ?).
556 (* general properties of functions *)
557 theorem monotonic_to_injective: \forall f:nat\to nat.
558 monotonic nat lt f \to injective nat nat f.
559 unfold injective.intros.
560 apply (nat_compare_elim x y).
561 intro.apply False_ind.apply (not_le_Sn_n (f x)).
562 rewrite > H1 in \vdash (? ? %).
563 change with (f x < f y).
566 intro.apply False_ind.apply (not_le_Sn_n (f y)).
567 rewrite < H1 in \vdash (? ? %).
568 change with (f y < f x).
572 theorem increasing_to_injective: \forall f:nat\to nat.
573 increasing f \to injective nat nat f.
574 intros.apply monotonic_to_injective.
575 apply increasing_to_monotonic.assumption.