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 (* \ / Matita is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/nat/log".
17 include "datatypes/constructors.ma".
18 include "nat/minimization.ma".
19 include "nat/relevant_equations.ma".
20 include "nat/primes.ma".
22 definition log \def \lambda p,n.
23 max n (\lambda x.leb (exp p x) n).
25 theorem le_exp_log: \forall p,n. O < n \to
26 exp p (log p n) \le n.
30 apply (f_max_true (\lambda x.leb (exp p x) n)).
31 apply (ex_intro ? ? O).
34 |apply le_to_leb_true.simplify.assumption
38 theorem log_SO: \forall n. S O < n \to log n (S O) = O.
40 apply sym_eq.apply le_n_O_to_eq.
41 apply (le_exp_to_le n)
43 |simplify in ⊢ (? ? %).
49 theorem lt_log_n_n: \forall p, n. S O < p \to O < n \to log p n < n.
52 [elim (le_to_or_lt_eq ? ? Hcut)
54 |absurd (exp p n \le n)
55 [rewrite < H2 in ⊢ (? (? ? %) ?).
63 |unfold log.apply le_max_n
67 theorem lt_O_log: \forall p,n. O < n \to p \le n \to O < log p n.
72 apply (leb_false_to_not_le ? ? ? H1).
73 rewrite > (exp_n_SO p).
74 apply (lt_max_to_false ? ? ? H2).
78 theorem le_log_n_n: \forall p,n. S O < p \to log p n \le n.
84 [assumption|apply lt_O_S]
88 theorem lt_exp_log: \forall p,n. S O < p \to n < exp p (S (log p n)).
90 [simplify.rewrite < times_n_SO.apply lt_to_le.assumption
92 apply leb_false_to_not_le.
93 apply (lt_max_to_false ? (S n1) (S (log p (S n1))))
94 [apply le_S_S.apply le_n
96 [assumption|apply lt_O_S]
101 theorem log_times1: \forall p,n,m. S O < p \to O < n \to O < m \to
102 log p (n*m) \le S(log p n+log p m).
104 unfold in ⊢ (? (% ? ?) ?).
105 apply f_false_to_le_max
106 [apply (ex_intro ? ? O).
109 |apply le_to_leb_true.
111 rewrite > times_n_SO.
112 apply le_times;assumption
115 apply lt_to_leb_false.
116 apply (lt_to_le_to_lt ? ((exp p (S(log p n)))*(exp p (S(log p m)))))
117 [apply lt_times;apply lt_exp_log;assumption
118 |rewrite < exp_plus_times.
120 [apply lt_to_le.assumption
129 theorem log_times: \forall p,n,m.S O < p \to log p (n*m) \le S(log p n+log p m).
134 [rewrite < times_n_O.
145 theorem log_exp: \forall p,n,m.S O < p \to O < m \to
146 log p ((exp p n)*m)=n+log p m.
148 unfold log in ⊢ (? ? (% ? ?) ?).
149 apply max_spec_to_max.
159 rewrite > assoc_times.
160 apply (trans_le ? ((S(S O))*(p\sup n1*m)))
161 [apply le_S_times_SSO
162 [rewrite > (times_n_O O) in ⊢ (? % ?).
178 apply le_to_leb_true.
179 rewrite > exp_plus_times.
186 apply lt_to_leb_false.
187 apply (lt_to_le_to_lt ? ((exp p n)*(exp p (S(log p m)))))
189 [apply lt_O_exp.apply lt_to_le.assumption
190 |apply lt_exp_log.assumption
192 |rewrite < exp_plus_times.
194 [apply lt_to_le.assumption
195 |rewrite < plus_n_Sm.
202 theorem le_log: \forall p,n,m. S O < p \to O < n \to n \le m \to
206 apply (lt_exp_to_lt p)
208 |apply (le_to_lt_to_lt ? n)
211 |apply (le_to_lt_to_lt ? m)
220 theorem log_n_n: \forall n. S O < n \to log n n = S O.
222 rewrite > exp_n_SO in ⊢ (? ? (? ? %) ?).
223 rewrite > times_n_SO in ⊢ (? ? (? ? %) ?).
234 theorem log_i_SSOn: \forall n,i. S O < n \to n < i \to i \le ((S(S O))*n) \to
235 log i ((S(S O))*n) = S O.
237 apply antisymmetric_le
238 [apply not_lt_to_le.intro.
239 apply (lt_to_not_le ((S(S O)) * n) (exp i (S(S O))))
242 [apply (le_to_lt_to_lt ? n);assumption
245 |apply (trans_le ? (exp i (log i ((S(S O))*n))))
247 [apply (ltn_to_ltO ? ? H1)
251 rewrite > (times_n_O O) in ⊢ (? % ?).
254 |apply lt_to_le.assumption
258 |apply (trans_le ? (log i i))
259 [rewrite < (log_n_n i) in ⊢ (? % ?)
261 [apply (trans_lt ? n);assumption
262 |apply (ltn_to_ltO ? ? H1)
265 |apply (trans_lt ? n);assumption
268 [apply (trans_lt ? n);assumption
269 |apply (ltn_to_ltO ? ? H1)