From 947ee89dec9e60561dfac3ce7e1842f35f178cb8 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 7 Dec 2007 11:38:57 +0000 Subject: [PATCH] A few more theorems. --- .../matita/library/nat/div_and_mod_diseq.ma | 38 ++++++++ helm/software/matita/library/nat/log.ma | 90 +++++++++++++++++++ helm/software/matita/library/nat/primes.ma | 22 +++++ 3 files changed, 150 insertions(+) diff --git a/helm/software/matita/library/nat/div_and_mod_diseq.ma b/helm/software/matita/library/nat/div_and_mod_diseq.ma index 53c59de35..4977df660 100644 --- a/helm/software/matita/library/nat/div_and_mod_diseq.ma +++ b/helm/software/matita/library/nat/div_and_mod_diseq.ma @@ -306,3 +306,41 @@ apply (trans_le ? ((a*m/i)/m)) ] qed. +theorem le_div_times_Sm: \forall a,i,m. O < i \to O < m \to +a / i \le (a * S (m / i))/m. +intros. +apply (trans_le ? ((a * S (m / i))/((S (m/i))*i))) + [rewrite < (eq_div_div_div_times ? i) + [rewrite > lt_O_to_div_times + [apply le_n + |apply lt_O_S + ] + |apply lt_O_S + |assumption + ] + |apply le_times_to_le_div + [assumption + |apply (trans_le ? (m*(a*S (m/i))/(S (m/i)*i))) + [apply le_times_div_div_times. + rewrite > (times_n_O O). + apply lt_times + [apply lt_O_S + |assumption + ] + |rewrite > sym_times. + apply le_times_to_le_div2 + [rewrite > (times_n_O O). + apply lt_times + [apply lt_O_S + |assumption + ] + |apply le_times_r. + apply lt_to_le. + apply lt_div_S. + assumption + ] + ] + ] + ] +qed. + diff --git a/helm/software/matita/library/nat/log.ma b/helm/software/matita/library/nat/log.ma index d96fb28c2..d4e1b2bd9 100644 --- a/helm/software/matita/library/nat/log.ma +++ b/helm/software/matita/library/nat/log.ma @@ -18,6 +18,8 @@ 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". definition log \def \lambda p,n. max n (\lambda x.leb (exp p x) n). @@ -246,6 +248,29 @@ intros.elim m ] 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 + ] + ] +qed. + theorem le_log: \forall p,n,m. S O < p \to O < n \to n \le m \to log p n \le log p m. intros. @@ -319,3 +344,68 @@ apply antisymmetric_le ] ] qed. + +theorem exp_n_O: \forall n. O < n \to exp O n = O. +intros.apply (lt_O_n_elim ? H).intros. +simplify.reflexivity. +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 + [assumption + |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. +*) +(* falso +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)))) + [ diff --git a/helm/software/matita/library/nat/primes.ma b/helm/software/matita/library/nat/primes.ma index ec7118980..0186d4324 100644 --- a/helm/software/matita/library/nat/primes.ma +++ b/helm/software/matita/library/nat/primes.ma @@ -286,6 +286,28 @@ cut(O \lt c) ] qed. +theorem eq_div_plus: \forall n,m,d. O < d \to +divides d n \to divides d m \to +(n + m ) / d = n/d + m/d. +intros. +elim H1. +elim H2. +rewrite > H3.rewrite > H4. +rewrite < distr_times_plus. +rewrite > sym_times. +rewrite > sym_times in ⊢ (? ? ? (? (? % ?) ?)). +rewrite > sym_times in ⊢ (? ? ? (? ? (? % ?))). +rewrite > lt_O_to_div_times + [rewrite > lt_O_to_div_times + [rewrite > lt_O_to_div_times + [reflexivity + |assumption + ] + |assumption + ] + |assumption + ] +qed. (* boolean divides *) definition divides_b : nat \to nat \to bool \def -- 2.39.2