X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Farithmetics%2Flog.ma;h=6c7e159e416c0f4f1bc58bf9b5a3d501f479e7ac;hb=74223db3fc45caccb3cfac80971b29cb0613da28;hp=b48aea3f8e4b72b3b419339fe174ddbf1105f085;hpb=53452958508001e7af3090695b619fe92135fb9e;p=helm.git
diff --git a/matita/matita/lib/arithmetics/log.ma b/matita/matita/lib/arithmetics/log.ma
index b48aea3f8..6c7e159e4 100644
--- a/matita/matita/lib/arithmetics/log.ma
+++ b/matita/matita/lib/arithmetics/log.ma
@@ -1,474 +1,224 @@
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| A.Asperti, C.Sacerdoti Coen, *)
-(* ||A|| E.Tassi, S.Zacchiroli *)
-(* \ / *)
-(* \ / Matita is distributed under the terms of the *)
-(* v GNU Lesser General Public License Version 2.1 *)
-(* *)
-(**************************************************************************)
-
(*
-include "datatypes/constructors.ma".
-include "nat/minimization.ma".
-include "nat/relevant_equations.ma".
-include "nat/primes.ma".
-include "nat/iteration2.ma".
-include "nat/div_and_mod_diseq.ma".
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department of the University of Bologna, Italy.
+ ||I||
+ ||T||
+ ||A|| This file is distributed under the terms of the
+ \ / GNU General Public License Version 2
+ \ /
+ V_______________________________________________________________ *)
+
+include "arithmetics/exp.ma".
+include "arithmetics/div_and_mod.ma".
+include "arithmetics/minimization.ma".
-definition log \def \lambda p,n.
-max n (\lambda x.leb (exp p x) n).
+definition log â λp,n.
+ max n (λx.leb (exp p x) n).
-theorem le_exp_log: \forall p,n. O < n \to
-exp p (log p n) \le n.
-intros.
-apply leb_true_to_le.
-unfold log.
-apply (f_max_true (\lambda x.leb (exp p x) n)).
-apply (ex_intro ? ? O).
-split
- [apply le_O_n
- |apply le_to_leb_true.simplify.assumption
+lemma tech_log : âp,n. 1
Hleb %
]
+qed.
+
+theorem le_exp_log: âp,n. O < n â
+ exp p (log p n) ⤠n.
+#a #n #posn @leb_true_to_le
+(* whd in match (log ??); *)
+@(f_max_true (λx.leb (exp a x) n)) %{0} % //
+@le_to_leb_true //
qed.
-theorem log_SO: \forall n. S O < n \to log n (S O) = O.
-intros.
-apply sym_eq.apply le_n_O_to_eq.
-apply (le_exp_to_le n)
- [assumption
- |simplify in ⢠(? ? %).
- apply le_exp_log.
- apply le_n
- ]
+theorem log_SO: ân. 1 < n â log n 1 = O.
+#n #lt1n @sym_eq @le_n_O_to_eq @(le_exp_to_le n) //
qed.
-theorem lt_to_log_O: \forall n,m. O < m \to m < n \to log n m = O.
-intros.
-apply sym_eq.apply le_n_O_to_eq.
-apply le_S_S_to_le.
-apply (lt_exp_to_lt n)
- [apply (le_to_lt_to_lt ? m);assumption
- |simplify in ⢠(? ? %).
- rewrite < times_n_SO.
- apply (le_to_lt_to_lt ? m)
- [apply le_exp_log.assumption
- |assumption
- ]
+theorem lt_to_log_O: ân,m. O < m â m < n â log n m = O.
+#n #m #posm #ltnm @sym_eq @le_n_O_to_eq @le_S_S_to_le @(lt_exp_to_lt n)
+ [@(le_to_lt_to_lt ? m) //
+ |normalize in ⢠(??%); (exp_n_SO p).
-apply (lt_max_to_false ? ? ? H2).
-assumption.
+theorem lt_O_log: âp, n. 1 < n â p ⤠n â O < log p n.
+#p #n #lt1p #lepn whd in match (log ??);
+@not_lt_to_le % #H lapply (lt_max_to_false ??? lt1p H)
+(le_to_leb_true ⦠lepn) #H destruct
qed.
-theorem le_log_n_n: \forall p,n. S O < p \to log p n \le n.
-intros.
-cases n
- [apply le_n
- |apply lt_to_le.
- apply lt_log_n_n
- [assumption|apply lt_O_S]
- ]
+theorem le_log_n_n: âp,n. 1 < p â log p n ⤠n.
+#p #n #lt1p cases n [@le_n |#m @lt_to_le @lt_log_n_n //]
qed.
-theorem lt_exp_log: \forall p,n. S O < p \to n < exp p (S (log p n)).
-intros.cases n
- [simplify.rewrite < times_n_SO.apply lt_to_le.assumption
- |apply not_le_to_lt.
- apply leb_false_to_not_le.
- apply (lt_max_to_false ? (S n1) (S (log p (S n1))))
- [apply le_S_S.apply le_n
- |apply lt_log_n_n
- [assumption|apply lt_O_S]
- ]
- ]
-qed.
+theorem lt_exp_log: âp,n. 1 < p â n < exp p (S (log p n)).
+#p #n #lt1p cases n
+ [normalize times_n_SO.
- apply le_times;assumption
+theorem log_times1: âp,n,m. 1 < p â O < n â O < m â
+ log p (n*m) ⤠S(log p n+log p m).
+#p #n #m #lt1p #posn #posm
+whd in ⢠(?(%??)?); @f_false_to_le_max
+ [%{O} %
+ [>(times_n_O 0) in ⢠(?%%); @lt_times //
+ |@le_to_leb_true normalize >(times_n_O 0) in ⢠(?%%); @lt_times //
]
- |intros.
- apply lt_to_leb_false.
- apply (lt_to_le_to_lt ? ((exp p (S(log p n)))*(exp p (S(log p m)))))
- [apply lt_times;apply lt_exp_log;assumption
- |rewrite < exp_plus_times.
- apply le_exp
- [apply lt_to_le.assumption
- |simplify.
- rewrite < plus_n_Sm.
- assumption
- ]
+ |#i #Hm @lt_to_leb_false
+ @(lt_to_le_to_lt ? ((exp p (S(log p n)))*(exp p (S(log p m)))))
+ [@lt_times @lt_exp_log //
+ | log_SO
- [simplify.
- rewrite < plus_n_O.
- apply le_log_n_n.
- assumption
- |assumption
- ]
- |elim H1
- [rewrite > log_SO
- [rewrite < plus_n_O.
- rewrite < times_n_SO.
- apply le_log_n_n.
- assumption
- |assumption
- ]
- |apply (trans_le ? (S n1 + S n2))
- [apply le_plus;apply le_log_n_n;assumption
- |simplify.
- apply le_S_S.
- rewrite < plus_n_Sm.
- change in ⢠(? % ?) with ((S n1)+n2).
- rewrite > sym_plus.
- apply le_plus_r.
- change with (n1 < n1*S n2).
- rewrite > times_n_SO in ⢠(? % ?).
- apply lt_times_r1
- [assumption
- |apply le_S_S.assumption
- ]
+theorem log_times: âp,n,m. 1 < p â
+ log p (n*m) ⤠S(log p n+log p m).
+#p #n #m #lt1p cases n // -n #n cases m
+ [(log_SO ⦠lt1p) >commutative_times (log_SO ⦠lt1p) < plus_n_O commutative_plus normalize >plus_n_Sm
+ @monotonic_le_plus_r >(times_n_1 n) in ⢠(?%?);
+ @monotonic_lt_times_r // @le_S_S //
]
]
]
- |apply le_to_leb_true.
- rewrite > exp_plus_times.
- apply le_times;apply le_exp_log;assumption
+ |@le_to_leb_true >exp_plus_times @le_times @le_exp_log //
]
qed.
-theorem log_exp: \forall p,n,m.S O < p \to O < m \to
-log p ((exp p n)*m)=n+log p m.
-intros.
-unfold log in ⢠(? ? (% ? ?) ?).
-apply max_spec_to_max.
-unfold max_spec.
-split
- [split
- [elim n
- [simplify.
- rewrite < plus_n_O.
- apply le_log_n_n.
- assumption
- |simplify.
- rewrite > assoc_times.
- apply (trans_le ? ((S(S O))*(p\sup n1*m)))
- [apply le_S_times_SSO
- [rewrite > (times_n_O O) in ⢠(? % ?).
- apply lt_times
- [apply lt_O_exp.
- apply lt_to_le.
- assumption
- |assumption
- ]
- |assumption
- ]
- |apply le_times
- [assumption
- |apply le_n
- ]
- ]
- ]
- |simplify.
- apply le_to_leb_true.
- rewrite > exp_plus_times.
- apply le_times_r.
- apply le_exp_log.
- assumption
+theorem log_exp: âp,n,m. 1 < p â O < m â
+ log p ((exp p n)*m)=n+log p m.
+#p #n #m #lt1p #posm whd in ⢠(??(%??)?);
+@max_spec_to_max %
+ [elim n
+ [<(exp_n_O p) >commutative_times (commutative_times ? p)
+ >associative_times >(times_n_1 (p^a * m)) in ⢠(?%?);
+ >commutative_times in ⢠(?%?); @monotonic_lt_times_l //
+ >(times_n_O 0) @lt_times // @lt_O_exp @lt_to_le //
]
- |intros.
- simplify.
- apply lt_to_leb_false.
- apply (lt_to_le_to_lt ? ((exp p n)*(exp p (S(log p m)))))
- [apply lt_times_r1
- [apply lt_O_exp.apply lt_to_le.assumption
- |apply lt_exp_log.assumption
- ]
- |rewrite < exp_plus_times.
- apply le_exp
- [apply lt_to_le.assumption
- |rewrite < plus_n_Sm.
- assumption
- ]
+ |@le_to_leb_true >exp_plus_times
+ @monotonic_le_times_r @le_exp_log //
+ |#i #Hi #Hm @lt_to_leb_false
+ @(lt_to_le_to_lt ? ((exp p n)*(exp p (S(log p m)))))
+ [@monotonic_lt_times_r [@lt_O_exp @lt_to_le // |@lt_exp_log //]
+ | times_n_SO in ⢠(? ? (? ? %) ?).
-rewrite > log_exp
- [rewrite > log_SO
- [rewrite < plus_n_O.reflexivity
- |assumption
- ]
- |assumption
- |apply le_n
- ]
+theorem eq_log_exp: âp,n. 1< p â
+ log p (exp p n)=n.
+#p #n #lt1p >(times_n_1 (p^n)) in ⢠(??(??%)?); >log_exp // >log_SO //
qed.
-theorem log_exp1: \forall p,n,m.S O < p \to
-log p (exp n m) \le m*S(log p n).
-intros.elim m
- [simplify in ⢠(? (? ? %) ?).
- rewrite > log_SO
- [apply le_O_n
- |assumption
- ]
- |simplify.
- apply (trans_le ? (S (log p n+log p (n\sup n1))))
- [apply log_times.assumption
- |apply le_S_S.
- apply le_plus_r.
- assumption
- ]
+theorem log_exp1: âp,n,m. 1 < p â
+ log p (exp n m) ⤠m*S(log p n).
+#p #n #m #lt1p elim m // -m #m #Hind
+@(transitive_le ? (S (log p n+log p (n\sup m))))
+ [whd in match (exp ??); >commutative_times @log_times //
+ |@le_S_S @monotonic_le_plus_r //
]
qed.
-theorem log_exp2: \forall p,n,m.S O < p \to O < n \to
-m*(log p n) \le log p (exp n m).
-intros.
-apply le_S_S_to_le.
-apply (lt_exp_to_lt p)
- [assumption
- |rewrite > sym_times.
- rewrite < exp_exp_times.
- apply (le_to_lt_to_lt ? (exp n m))
- [elim m
- [simplify.apply le_n
- |simplify.apply le_times
- [apply le_exp_log.
- assumption
- |assumption
- ]
- ]
- |apply lt_exp_log.
- assumption
+theorem log_exp2: âp,n,m. 1 < p â 0 < n â
+ m*(log p n) ⤠log p (exp n m).
+#p #n #m #ltp1 #posn @le_S_S_to_le @(lt_exp_to_lt p)
+ [@lt_to_le //
+ |>commutative_times H1;simplify;apply (trans_le ? n)
- [apply le_log_n_n;assumption
- |apply le_n_Sn]
- |intro;unfold log;simplify;rewrite > H1;simplify;apply le_max_f_max_g;
- intros;apply le_to_leb_true;constructor 2;apply leb_true_to_le;assumption]
+lemma le_log_S: âp,n.1 < p â
+ log p n ⤠log p (S n).
+#p #n #lt1p normalize cases (leb (exp p n) (S n)) normalize //
+@le_max_f_max_g #i #ltin #H @le_to_leb_true @le_S @leb_true_to_le //
qed.
-theorem le_log: \forall p,n,m. S O < p \to n \le m \to
-log p n \le log p m.
-intros.elim H1
- [constructor 1
- |apply (trans_le ? ? ? H3);apply le_log_plus;assumption]
+theorem le_log: âp,n,m. 1 < p â n ⤠m â
+ log p n ⤠log p m.
+#p #n #m #lt1p #lenm elim lenm // -m #m #lenm #Hind
+@(transitive_le ⦠Hind) @le_log_S //
qed.
-theorem log_div: \forall p,n,m. S O < p \to O < m \to m \le n \to
-log p (n/m) \le log p n -log p m.
-intros.
-apply le_plus_to_minus_r.
-apply (trans_le ? (log p ((n/m)*m)))
- [apply log_times_l
- [apply le_times_to_le_div
- [assumption
- |rewrite < times_n_SO.
- assumption
- ]
- |assumption
- |assumption
- ]
- |apply le_log
- [assumption
- |rewrite > (div_mod n m) in ⢠(? ? %)
- [apply le_plus_n_r
- |assumption
- ]
- ]
- ]
-qed.
-
-theorem log_n_n: \forall n. S O < n \to log n n = S O.
-intros.
-rewrite > exp_n_SO in ⢠(? ? (? ? %) ?).
-rewrite > times_n_SO in ⢠(? ? (? ? %) ?).
-rewrite > log_exp
- [rewrite > log_SO
- [reflexivity
- |assumption
- ]
- |assumption
- |apply le_n
- ]
-qed.
-
-theorem log_i_SSOn: \forall n,i. S O < n \to n < i \to i \le ((S(S O))*n) \to
-log i ((S(S O))*n) = S O.
-intros.
-apply antisymmetric_le
- [apply not_lt_to_le.intro.
- apply (lt_to_not_le ((S(S O)) * n) (exp i (S(S O))))
- [rewrite > exp_SSO.
- apply lt_times
- [apply (le_to_lt_to_lt ? n);assumption
- |assumption
- ]
- |apply (trans_le ? (exp i (log i ((S(S O))*n))))
- [apply le_exp
- [apply (ltn_to_ltO ? ? H1)
- |assumption
- ]
- |apply le_exp_log.
- rewrite > (times_n_O O) in ⢠(? % ?).
- apply lt_times
- [apply lt_O_S
- |apply lt_to_le.assumption
- ]
+theorem log_div: âp,n,m. 1 < p â O < m â m ⤠n â
+ log p (n/m) ⤠log p n -log p m.
+#p #n #m #lt1p #posn #lemn
+@le_plus_to_minus_r @(transitive_le ? (log p ((n/m)*m)))
+ [@log_times_l // @le_times_to_le_div //
+ |@le_log //
+ ]
+qed.
+
+theorem log_n_n: ân. 1 < n â log n n = 1.
+#n #lt1n >(exp_n_1 n) in ⢠(??(??%)?);
+>(times_n_1 (n^1)) in ⢠(??(??%)?); >log_exp //
+qed.
+
+theorem log_i_2n: ân,i. 1 < n â n < i â i ⤠2*n â
+ log i (2*n) = 1.
+#n #i #lt1n #ltni #lei
+cut (âa,b. aâ¤b â bâ¤a â a=b)
+ [#a #b #leab #leba cases (le_to_or_lt_eq ⦠leab)
+ [#ltab @False_ind @(absurd ? ltab) @le_to_not_lt // | //]] #Hcut
+@Hcut
+ [@not_lt_to_le % #H
+ @(absurd ?? (lt_to_not_le (2 * n) (exp i 2) ?))
+ [@(transitive_le ? (exp i (log i (2*n))))
+ [@le_exp // @(ltn_to_ltO ? ? ltni)
+ |@le_exp_log >(times_n_O O) in ⢠(?%?); @lt_times // @lt_to_le //
]
+ |>exp_2 @lt_times @(le_to_lt_to_lt ? n) //
]
- |apply (trans_le ? (log i i))
- [rewrite < (log_n_n i) in ⢠(? % ?)
- [apply le_log
- [apply (trans_lt ? n);assumption
- |apply le_n
- ]
- |apply (trans_lt ? n);assumption
- ]
- |apply le_log
- [apply (trans_lt ? n);assumption
- |assumption
- ]
+ |@(transitive_le ? (log i i))
+ [<(log_n_n i) in ⢠(?%?); // @(transitive_lt ⦠lt1n) //
+ |@le_log // @(transitive_lt ⦠lt1n) //
]
]
qed.
-theorem exp_n_O: \forall n. O < n \to exp O n = O.
-intros.apply (lt_O_n_elim ? H).intros.
-simplify.reflexivity.
+theorem exp_n_O: ân. O < n â exp O n = O.
+#n #posn @(lt_O_n_elim ? posn) normalize //
qed.
-(*
-theorem tech1: \forall n,i.O < n \to
-(exp (S n) (S(S i)))/(exp n (S i)) \le ((exp n i) + (exp (S n) (S i)))/(exp n i).
-intros.
-simplify in ⢠(? (? ? %) ?).
-rewrite < eq_div_div_div_times
- [apply monotonic_div
- [apply lt_O_exp.assumption
- |apply le_S_S_to_le.
- apply lt_times_to_lt_div.
- change in ⢠(? % ?) with ((exp (S n) (S i)) + n*(exp (S n) (S i))).
-
-
- |apply (trans_le ? ((n)\sup(i)*(S n)\sup(S i)/(n)\sup(S i)))
- [apply le_times_div_div_times.
- apply lt_O_exp.assumption
- |apply le_times_to_le_div2
- [apply lt_O_exp.assumption
- |simplify.
-
-theorem tech1: \forall a,b,n,m.O < m \to
-n/m \le b \to (a*n)/m \le a*b.
-intros.
-apply le_times_to_le_div2
- [assumption
- |
-
-theorem tech2: \forall n,m. O < n \to
-(exp (S n) m) / (exp n m) \le (n + m)/n.
-intros.
-elim m
- [rewrite < plus_n_O.simplify.
- rewrite > div_n_n.apply le_n
- |apply le_times_to_le_div
- [assumption
- |apply (trans_le ? (n*(S n)\sup(S n1)/(n)\sup(S n1)))
- [apply le_times_div_div_times.
- apply lt_O_exp
- |simplify in ⢠(? (? ? %) ?).
- rewrite > sym_times in ⢠(? (? ? %) ?).
- rewrite < eq_div_div_div_times
- [apply le_times_to_le_div2
- [assumption
- |
-
-
-theorem le_log_sigma_p:\forall n,m,p. O < m \to S O < p \to
-log p (exp n m) \le sigma_p n (\lambda i.true) (\lambda i. (m / i)).
-intros.
-elim n
- [rewrite > exp_n_O
- [simplify.apply le_n
- |assumption
- ]
- |rewrite > true_to_sigma_p_Sn
- [apply (trans_le ? (m/n1+(log p (exp n1 m))))
- [
-*)
-*)