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_to_log_O: \forall n,m. O < m \to m < n \to log n m = O.
51 apply sym_eq.apply le_n_O_to_eq.
53 apply (lt_exp_to_lt n)
54 [apply (le_to_lt_to_lt ? m);assumption
55 |simplify in ⊢ (? ? %).
57 apply (le_to_lt_to_lt ? m)
58 [apply le_exp_log.assumption
64 theorem lt_log_n_n: \forall p, n. S O < p \to O < n \to log p n < n.
67 [elim (le_to_or_lt_eq ? ? Hcut)
69 |absurd (exp p n \le n)
70 [rewrite < H2 in ⊢ (? (? ? %) ?).
78 |unfold log.apply le_max_n
82 theorem lt_O_log: \forall p,n. O < n \to p \le n \to O < log p n.
87 apply (leb_false_to_not_le ? ? ? H1).
88 rewrite > (exp_n_SO p).
89 apply (lt_max_to_false ? ? ? H2).
93 theorem le_log_n_n: \forall p,n. S O < p \to log p n \le n.
99 [assumption|apply lt_O_S]
103 theorem lt_exp_log: \forall p,n. S O < p \to n < exp p (S (log p n)).
105 [simplify.rewrite < times_n_SO.apply lt_to_le.assumption
107 apply leb_false_to_not_le.
108 apply (lt_max_to_false ? (S n1) (S (log p (S n1))))
109 [apply le_S_S.apply le_n
111 [assumption|apply lt_O_S]
116 theorem log_times1: \forall p,n,m. S O < p \to O < n \to O < m \to
117 log p (n*m) \le S(log p n+log p m).
119 unfold in ⊢ (? (% ? ?) ?).
120 apply f_false_to_le_max
121 [apply (ex_intro ? ? O).
124 |apply le_to_leb_true.
126 rewrite > times_n_SO.
127 apply le_times;assumption
130 apply lt_to_leb_false.
131 apply (lt_to_le_to_lt ? ((exp p (S(log p n)))*(exp p (S(log p m)))))
132 [apply lt_times;apply lt_exp_log;assumption
133 |rewrite < exp_plus_times.
135 [apply lt_to_le.assumption
144 theorem log_times: \forall p,n,m.S O < p \to log p (n*m) \le S(log p n+log p m).
149 [rewrite < times_n_O.
160 theorem log_exp: \forall p,n,m.S O < p \to O < m \to
161 log p ((exp p n)*m)=n+log p m.
163 unfold log in ⊢ (? ? (% ? ?) ?).
164 apply max_spec_to_max.
174 rewrite > assoc_times.
175 apply (trans_le ? ((S(S O))*(p\sup n1*m)))
176 [apply le_S_times_SSO
177 [rewrite > (times_n_O O) in ⊢ (? % ?).
193 apply le_to_leb_true.
194 rewrite > exp_plus_times.
201 apply lt_to_leb_false.
202 apply (lt_to_le_to_lt ? ((exp p n)*(exp p (S(log p m)))))
204 [apply lt_O_exp.apply lt_to_le.assumption
205 |apply lt_exp_log.assumption
207 |rewrite < exp_plus_times.
209 [apply lt_to_le.assumption
210 |rewrite < plus_n_Sm.
217 theorem eq_log_exp: \forall p,n.S O < p \to
220 rewrite > times_n_SO in ⊢ (? ? (? ? %) ?).
223 [rewrite < plus_n_O.reflexivity
231 theorem log_exp1: \forall p,n,m.S O < p \to
232 log p (exp n m) \le m*S(log p n).
234 [simplify in ⊢ (? (? ? %) ?).
240 apply (trans_le ? (S (log p n+log p (n\sup n1))))
241 [apply log_times.assumption
249 theorem le_log: \forall p,n,m. S O < p \to O < n \to n \le m \to
253 apply (lt_exp_to_lt p)
255 |apply (le_to_lt_to_lt ? n)
258 |apply (le_to_lt_to_lt ? m)
267 theorem log_n_n: \forall n. S O < n \to log n n = S O.
269 rewrite > exp_n_SO in ⊢ (? ? (? ? %) ?).
270 rewrite > times_n_SO in ⊢ (? ? (? ? %) ?).
281 theorem log_i_SSOn: \forall n,i. S O < n \to n < i \to i \le ((S(S O))*n) \to
282 log i ((S(S O))*n) = S O.
284 apply antisymmetric_le
285 [apply not_lt_to_le.intro.
286 apply (lt_to_not_le ((S(S O)) * n) (exp i (S(S O))))
289 [apply (le_to_lt_to_lt ? n);assumption
292 |apply (trans_le ? (exp i (log i ((S(S O))*n))))
294 [apply (ltn_to_ltO ? ? H1)
298 rewrite > (times_n_O O) in ⊢ (? % ?).
301 |apply lt_to_le.assumption
305 |apply (trans_le ? (log i i))
306 [rewrite < (log_n_n i) in ⊢ (? % ?)
308 [apply (trans_lt ? n);assumption
309 |apply (ltn_to_ltO ? ? H1)
312 |apply (trans_lt ? n);assumption
315 [apply (trans_lt ? n);assumption
316 |apply (ltn_to_ltO ? ? H1)