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/library_auto/nat/lt_arith".
17 include "auto/nat/div_and_mod.ma".
20 theorem monotonic_lt_plus_r:
21 \forall n:nat.monotonic nat lt (\lambda m.n+m).
32 variant lt_plus_r: \forall n,p,q:nat. p < q \to n + p < n + q \def
35 theorem monotonic_lt_plus_l:
36 \forall n:nat.monotonic nat lt (\lambda m.m+n).
40 rewrite < (sym_plus n).*)
41 applyS lt_plus_r.assumption.
43 (* IN ALTERNATIVA: mantengo le 2 rewrite, e concludo con auto. *)
45 variant lt_plus_l: \forall n,p,q:nat. p < q \to p + n < q + n \def
48 theorem lt_plus: \forall n,m,p,q:nat. n < m \to p < q \to n + p < m + q.
51 (*apply (trans_lt ? (n + q)).
52 apply lt_plus_r.assumption.
53 apply lt_plus_l.assumption.*)
56 theorem lt_plus_to_lt_l :\forall n,p,q:nat. p+n < q+n \to p<q.
59 rewrite > (plus_n_O q).
65 rewrite > (plus_n_Sm q).
70 theorem lt_plus_to_lt_r :\forall n,p,q:nat. n+p < n+q \to p<q.
72 apply (lt_plus_to_lt_l n).
74 rewrite > (sym_plus q).
79 theorem lt_O_times_S_S: \forall n,m:nat.O < (S n)*(S m).
89 theorem monotonic_lt_times_r:
90 \forall n:nat.monotonic nat lt (\lambda m.(S n)*m).
98 | apply lt_plus;assumption (* chiudo con assumption entrambi i sottogoal attivi*)
102 theorem lt_times_r: \forall n,p,q:nat. p < q \to (S n) * p < (S n) * q
103 \def monotonic_lt_times_r.
105 theorem monotonic_lt_times_l:
106 \forall m:nat.monotonic nat lt (\lambda n.n * (S m)).
109 (*rewrite < sym_times.
110 rewrite < (sym_times (S m)).*)
111 applyS lt_times_r.assumption.
114 (* IN ALTERNATIVA: mantengo le 2 rewrite, e concludo con auto. *)
117 variant lt_times_l: \forall n,p,q:nat. p<q \to p*(S n) < q*(S n)
118 \def monotonic_lt_times_l.
120 theorem lt_times:\forall n,m,p,q:nat. n<m \to p<q \to n*p < m*q.
123 [ apply (lt_O_n_elim m H).
126 [ apply (lt_O_n_elim q Hcut).
129 (*change with (O < (S m1)*(S m2)).
130 apply lt_O_times_S_S.*)
131 | apply (ltn_to_ltO p q H1). (*funziona anche auto*)
133 | apply (trans_lt ? ((S n1)*q))
138 [ apply (lt_O_n_elim q Hcut).
143 |apply (ltn_to_ltO p q H2). (*funziona anche auto*)
149 theorem lt_times_to_lt_l:
150 \forall n,p,q:nat. p*(S n) < q*(S n) \to p < q.
152 cut (p < q \lor p \nlt q)
155 | absurd (p * (S n) < q * (S n))
157 | apply le_to_not_lt.
164 |exact (decidable_lt p q).
168 theorem lt_times_to_lt_r:
169 \forall n,p,q:nat. (S n)*p < (S n)*q \to lt p q.
171 apply (lt_times_to_lt_l n).
173 rewrite < (sym_times (S n)).
177 theorem nat_compare_times_l : \forall n,p,q:nat.
178 nat_compare p q = nat_compare ((S n) * p) ((S n) * q).
180 apply nat_compare_elim
182 apply nat_compare_elim
188 (*apply (inj_times_r n).
191 (*apply lt_to_not_eq.
197 (*apply (lt_times_to_lt_r n).
200 (*apply le_to_not_lt.
208 rewrite > nat_compare_n_n.
211 apply nat_compare_elim
215 (*apply (lt_times_to_lt_r n).
218 (*apply le_to_not_lt.
226 apply (inj_times_r n).
229 (*apply lt_to_not_eq.
240 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.
242 apply (lt_O_n_elim m H).
244 apply (lt_times_to_lt_r m1).
246 rewrite > (plus_n_O ((S m1)*(n / (S m1)))).
259 theorem lt_div_n_m_n: \forall n,m:nat. (S O) < m \to O < n \to n / m \lt n.
261 apply (nat_case1 (n / m))
266 rewrite > (div_mod n m) in \vdash (? ? %)
267 [ apply (lt_to_le_to_lt ? ((n / m)*m))
268 [ apply (lt_to_le_to_lt ? ((n / m)*(S (S O))))
269 [ rewrite < sym_times.
274 (*rewrite < plus_n_O.
284 (*rewrite < sym_plus.
288 (*apply (trans_lt ? (S O)).
296 (* general properties of functions *)
297 theorem monotonic_to_injective: \forall f:nat\to nat.
298 monotonic nat lt f \to injective nat nat f.
299 unfold injective.intros.
300 apply (nat_compare_elim x y)
303 apply (not_le_Sn_n (f x)).
304 rewrite > H1 in \vdash (? ? %).
305 change with (f x < f y).
313 apply (not_le_Sn_n (f y)).
314 rewrite < H1 in \vdash (? ? %).
315 change with (f y < f x).
322 theorem increasing_to_injective: \forall f:nat\to nat.
323 increasing f \to injective nat nat f.
326 (*apply monotonic_to_injective.
327 apply increasing_to_monotonic.