From 3f5a0152427fd9a89e7239befd259d27b97aaef5 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 14 Feb 2008 15:41:46 +0000 Subject: [PATCH] Prima versione di bertrand. Tanti cambiamenti qua e la. --- helm/software/matita/library/nat/bertrand.ma | 518 ++++++++++++++++++ helm/software/matita/library/nat/binomial.ma | 13 +- helm/software/matita/library/nat/chebyshev.ma | 281 +++++++++- .../matita/library/nat/chebyshev_teta.ma | 102 +++- helm/software/matita/library/nat/exp.ma | 17 + .../software/matita/library/nat/factorial2.ma | 5 - helm/software/matita/library/nat/nat.ma | 5 + helm/software/matita/library/nat/pi_p.ma | 29 + helm/software/matita/library/nat/sqrt.ma | 15 + helm/software/matita/library/nat/times.ma | 22 +- 10 files changed, 981 insertions(+), 26 deletions(-) create mode 100644 helm/software/matita/library/nat/bertrand.ma diff --git a/helm/software/matita/library/nat/bertrand.ma b/helm/software/matita/library/nat/bertrand.ma new file mode 100644 index 000000000..f014b0ecc --- /dev/null +++ b/helm/software/matita/library/nat/bertrand.ma @@ -0,0 +1,518 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "nat/sqrt.ma". +include "nat/chebyshev_teta.ma". +include "nat/chebyshev.ma". + +definition not_bertrand \def \lambda n. +\forall p.n < p \to p \le 2*n \to \not (prime p). + +(* not used +theorem divides_pi_p_to_divides: \forall p,n,b,g.prime p \to +divides p (pi_p n b g) \to \exists i. (i < n \and (b i = true \and +divides p (g i))). +intros 2.elim n + [simplify in H1. + apply False_ind. + apply (le_to_not_lt p 1) + [apply divides_to_le + [apply le_n + |assumption + ] + |elim H.assumption + ] + |apply (bool_elim ? (b n1));intro + [rewrite > (true_to_pi_p_Sn ? ? ? H3) in H2. + elim (divides_times_to_divides ? ? ? H1 H2) + [apply (ex_intro ? ? n1). + split + [apply le_n + |split;assumption + ] + |elim (H ? ? H1 H4). + elim H5. + apply (ex_intro ? ? a). + split + [apply lt_to_le.apply le_S_S.assumption + |assumption + ] + ] + |rewrite > (false_to_pi_p_Sn ? ? ? H3) in H2. + elim (H ? ? H1 H2). + elim H4. + apply (ex_intro ? ? a). + split + [apply lt_to_le.apply le_S_S.assumption + |assumption + ] + ] + ] +qed. + +theorem divides_B: \forall n,p.prime p \to p \divides (B n) \to +p \le n \land \exists i.mod (n /(exp p (S i))) 2 \neq O. +intros. +unfold B in H1. +elim (divides_pi_p_to_divides ? ? ? ? H H1). +elim H2.clear H2. +elim H4.clear H4. +elim (divides_pi_p_to_divides ? ? ? ? H H5).clear H5. +elim H4.clear H4. +elim H6.clear H6. +cut (p = a) + [split + [rewrite > Hcut.apply le_S_S_to_le.assumption + |apply (ex_intro ? ? a1). + rewrite > Hcut. + intro. + change in H7:(? ? %) with (exp a ((n/(exp a (S a1))) \mod 2)). + rewrite > H6 in H7. + simplify in H7. + absurd (p \le 1) + [apply divides_to_le[apply lt_O_S|assumption] + |apply lt_to_not_le.elim H.assumption + ] + ] + |apply (divides_exp_to_eq ? ? ? H ? H7). + apply primeb_true_to_prime. + assumption + ] +qed. +*) + +definition k \def \lambda n,p. +sigma_p (log p n) (λi:nat.true) (λi:nat.((n/(exp p (S i))\mod 2))). + +theorem le_k: \forall n,p. k n p \le log p n. +intros.unfold k.elim (log p n) + [apply le_n + |rewrite > true_to_sigma_p_Sn + [rewrite > plus_n_SO. + rewrite > sym_plus in ⊢ (? ? %). + apply le_plus + [apply le_S_S_to_le. + apply lt_mod_m_m. + apply lt_O_S + |assumption + ] + |reflexivity + ] + ] +qed. + +definition B1 \def +\lambda n. pi_p (S n) primeb (\lambda p.(exp p (k n p))). + +theorem eq_B_B1: \forall n. B n = B1 n. +intros.unfold B.unfold B1. +apply eq_pi_p + [intros.reflexivity + |intros.unfold k. + apply exp_sigma_p1 + ] +qed. + +definition B_split1 \def \lambda n. +pi_p (S n) primeb (\lambda p.(exp p (bool_to_nat (leb (k n p) 1)* (k n p)))). + +definition B_split2 \def \lambda n. +pi_p (S n) primeb (\lambda p.(exp p (bool_to_nat (leb 2 (k n p))* (k n p)))). + +theorem eq_B1_times_B_split1_B_split2: \forall n. +B1 n = B_split1 n * B_split2 n. +intro.unfold B1.unfold B_split1.unfold B_split2. +rewrite < times_pi_p. +apply eq_pi_p + [intros.reflexivity + |intros.apply (bool_elim ? (leb (k n x) 1));intro + [rewrite > (lt_to_leb_false 2 (k n x)) + [simplify.rewrite < plus_n_O. + rewrite < times_n_SO.reflexivity + |apply le_S_S.apply leb_true_to_le.assumption + ] + |rewrite > (le_to_leb_true 2 (k n x)) + [simplify.rewrite < plus_n_O. + rewrite < plus_n_O.reflexivity + |apply not_le_to_lt.apply leb_false_to_not_le.assumption + ] + ] + ] +qed. + +lemma lt_div_to_times: \forall n,m,q. O < q \to n/q < m \to n < q*m. +intros. +cut (O < m) as H2 + [apply not_le_to_lt. + intro.apply (lt_to_not_le ? ? H1). + apply le_times_to_le_div;assumption + |apply (ltn_to_ltO ? ? H1) + ] +qed. + +lemma lt_to_div_O:\forall n,m. n < m \to n / m = O. +intros. +apply (div_mod_spec_to_eq n m (n/m) (n \mod m) O n) + [apply div_mod_spec_div_mod. + apply (ltn_to_ltO ? ? H) + |apply div_mod_spec_intro + [assumption + |reflexivity + ] + ] +qed. + +(* the value of n could be smaller *) +lemma k1: \forall n,p. 18 \le n \to p \le n \to 2*n/ 3 < p\to k (2*n) p = O. +intros.unfold k. +elim (log p (2*n)) + [reflexivity + |rewrite > true_to_sigma_p_Sn + [rewrite > H3. + rewrite < plus_n_O. + cases n1 + [rewrite < exp_n_SO. + cut (2*n/p = 2) as H4 + [rewrite > H4.reflexivity + |apply lt_to_le_times_to_lt_S_to_div + [apply (ltn_to_ltO ? ? H2) + |rewrite < sym_times. + apply le_times_r. + assumption + |rewrite > sym_times in ⊢ (? ? %). + apply lt_div_to_times + [apply lt_O_S + |assumption + ] + ] + ] + |cut (2*n/(p)\sup(S (S n2)) = O) as H4 + [rewrite > H4.reflexivity + |apply lt_to_div_O. + apply (le_to_lt_to_lt ? (exp ((2*n)/3) 2)) + [apply (le_times_to_le (exp 3 2)) + [apply leb_true_to_le.reflexivity + |rewrite > sym_times in ⊢ (? ? %). + rewrite > times_exp. + apply (trans_le ? (exp n 2)) + [rewrite < assoc_times. + rewrite > exp_SSO in ⊢ (? ? %). + apply le_times_l. + assumption + |apply monotonic_exp1. + apply (le_plus_to_le 3). + change in ⊢ (? ? %) with ((S(2*n/3))*3). + apply (trans_le ? (2*n)) + [simplify in ⊢ (? ? %). + rewrite < plus_n_O. + apply le_plus_l. + apply (trans_le ? 18 ? ? H). + apply leb_true_to_le.reflexivity + |apply lt_to_le. + apply lt_div_S. + apply lt_O_S + ] + ] + ] + |apply (lt_to_le_to_lt ? (exp p 2)) + [apply lt_exp1 + [apply lt_O_S + |assumption + ] + |apply le_exp + [apply (ltn_to_ltO ? ? H2) + |apply le_S_S.apply le_S_S.apply le_O_n + ] + ] + ] + ] + ] + |reflexivity + ] + ] +qed. + +theorem le_B_split1_teta:\forall n.18 \le n \to not_bertrand n \to +B_split1 (2*n) \le teta (2 * n / 3). +intros.unfold B_split1.unfold teta. +apply (trans_le ? (pi_p (S (2*n)) primeb (λp:nat.(p)\sup(bool_to_nat (eqb (k (2*n) p) 1))))) + [apply le_pi_p.intros. + apply le_exp + [apply prime_to_lt_O.apply primeb_true_to_prime.assumption + |apply (bool_elim ? (leb (k (2*n) i) 1));intro + [elim (le_to_or_lt_eq ? ? (leb_true_to_le ? ? H4)) + [lapply (le_S_S_to_le ? ? H5) as H6. + apply (le_n_O_elim ? H6). + rewrite < times_n_O. + apply le_n + |rewrite > (eq_to_eqb_true ? ? H5). + rewrite > H5.apply le_n + ] + |apply le_O_n + ] + ] + |apply (trans_le ? (pi_p (S (2*n/3)) primeb (λp:nat.(p)\sup(bool_to_nat (eqb (k (2*n) p) 1))))) + [apply (eq_ind ? ? ? (le_n ?)). + apply or_false_eq_SO_to_eq_pi_p + [apply le_S_S. + apply le_times_to_le_div2 + [apply lt_O_S + |rewrite > sym_times in ⊢ (? ? %). + apply le_times_n. + apply leb_true_to_le.reflexivity + ] + |intros. + unfold not_bertrand in H1. + elim (decidable_le (S n) i) + [left. + apply not_prime_to_primeb_false. + apply H1 + [assumption + |apply le_S_S_to_le.assumption + ] + |right. + rewrite > k1 + [reflexivity + |assumption + |apply le_S_S_to_le. + apply not_le_to_lt.assumption + |assumption + ] + ] + ] + |apply le_pi_p.intros. + elim (eqb (k (2*n) i) 1) + [rewrite < exp_n_SO.apply le_n + |simplify.apply prime_to_lt_O. + apply primeb_true_to_prime. + assumption + ] + ] + ] +qed. + +theorem le_B_split2_exp: \forall n. exp 2 7 \le n \to +B_split2 (2*n) \le exp (2*n) (pred(sqrt(2*n)/2)). +intros.unfold B_split2. +cut (O < n) + [apply (trans_le ? (pi_p (S (sqrt (2*n))) primeb + (λp:nat.(p)\sup(bool_to_nat (leb 2 (k (2*n) p))*k (2*n) p)))) + [apply (eq_ind ? ? ? (le_n ?)). + apply or_false_eq_SO_to_eq_pi_p + [apply le_S_S. + apply le_sqrt_n_n + |intros. + apply (bool_elim ? (leb 2 (k (2*n) i)));intro + [apply False_ind. + apply (lt_to_not_le ? ? H1).unfold sqrt. + apply f_m_to_le_max + [apply le_S_S_to_le.assumption + |apply le_to_leb_true. + rewrite < exp_SSO. + apply not_lt_to_le.intro. + apply (le_to_not_lt 2 (log i (2*n))) + [apply (trans_le ? (k (2*n) i)) + [apply leb_true_to_le.assumption + |apply le_k + ] + |apply le_S_S.unfold log.apply f_false_to_le_max + [apply (ex_intro ? ? O).split + [apply le_O_n + |apply le_to_leb_true.simplify. + apply (trans_le ? n) + [assumption. + |apply le_plus_n_r + ] + ] + |intros.apply lt_to_leb_false. + apply (lt_to_le_to_lt ? (exp i 2)) + [assumption + |apply le_exp + [apply (ltn_to_ltO ? ? H1) + |assumption + ] + ] + ] + ] + ] + |right.reflexivity + ] + ] + |apply (trans_le ? (pi_p (S (sqrt (2*n))) primeb (λp:nat.2*n))) + [apply le_pi_p.intros. + apply (trans_le ? (exp i (log i (2*n)))) + [apply le_exp + [apply prime_to_lt_O. + apply primeb_true_to_prime. + assumption + |apply (bool_elim ? (leb 2 (k (2*n) i)));intro + [simplify in ⊢ (? (? % ?) ?). + rewrite > sym_times. + rewrite < times_n_SO. + apply le_k + |apply le_O_n + ] + ] + |apply le_exp_log. + rewrite > (times_n_O O) in ⊢ (? % ?). + apply lt_times + [apply lt_O_S + |assumption + ] + ] + |apply (trans_le ? (exp (2*n) (prim(sqrt (2*n))))) + [unfold prim. + apply (eq_ind ? ? ? (le_n ?)). + apply exp_sigma_p + |apply le_exp + [rewrite > (times_n_O O) in ⊢ (? % ?). + apply lt_times + [apply lt_O_S + |assumption + ] + |apply le_prim_n3. + unfold sqrt. + apply f_m_to_le_max + [apply (trans_le ? (2*(exp 2 7))) + [apply leb_true_to_le.reflexivity + |apply le_times_r.assumption + ] + |apply le_to_leb_true. + apply (trans_le ? (2*(exp 2 7))) + [apply leb_true_to_le.reflexivity + |apply le_times_r.assumption + ] + ] + ] + ] + ] + ] + |apply (lt_to_le_to_lt ? ? ? ? H). + apply leb_true_to_le.reflexivity + ] +qed. + +theorem not_bertrand_to_le_B: +\forall n.exp 2 7 \le n \to not_bertrand n \to +B (2*n) \le (exp 2 (2*(2 * n / 3)))*(exp (2*n) (pred(sqrt(2*n)/2))). +intros. +rewrite > eq_B_B1. +rewrite > eq_B1_times_B_split1_B_split2. +apply le_times + [apply (trans_le ? (teta ((2*n)/3))) + [apply le_B_split1_teta + [apply (trans_le ? ? ? ? H). + apply leb_true_to_le.reflexivity + |assumption + ] + |apply le_teta + ] + |apply le_B_split2_exp. + assumption + ] +qed. + +(* +theorem not_bertrand_to_le1: +\forall n.18 \le n \to not_bertrand n \to +exp 2 (2*n) \le (exp 2 (2*(2 * n / 3)))*(exp (2*n) (S(sqrt(2*n)))). +*) + +theorem le_times_div_m_m: \forall n,m. O < m \to n/m*m \le n. +intros. +rewrite > (div_mod n m) in ⊢ (? ? %) + [apply le_plus_n_r + |assumption + ] +qed. + +theorem not_bertrand_to_le1: +\forall n.exp 2 7 \le n \to not_bertrand n \to +(exp 2 (2*n / 3)) \le (exp (2*n) (sqrt(2*n)/2)). +intros. +apply (le_times_to_le (exp 2 (2*(2 * n / 3)))) + [apply lt_O_exp.apply lt_O_S + |rewrite < exp_plus_times. + apply (trans_le ? (exp 2 (2*n))) + [apply le_exp + [apply lt_O_S + |rewrite < sym_plus. + change in ⊢ (? % ?) with (3*(2*n/3)). + rewrite > sym_times. + apply le_times_div_m_m. + apply lt_O_S + ] +(* weaker form + rewrite < distr_times_plus. + apply le_times_r. + apply (trans_le ? ((2*n + n)/3)) + [apply le_plus_div.apply lt_O_S + |rewrite < sym_plus. + change in ⊢ (? (? % ?) ?) with (3*n). + rewrite < sym_times. + rewrite > lt_O_to_div_times + [apply le_n + |apply lt_O_S + ] + ] + ] *) + |apply (trans_le ? (2*n*B(2*n))) + [apply le_exp_B. + apply (trans_le ? ? ? ? H). + apply leb_true_to_le.reflexivity + |rewrite > S_pred in ⊢ (? ? (? ? (? ? %))) + [rewrite > exp_S. + rewrite < assoc_times. + rewrite < sym_times in ⊢ (? ? (? % ?)). + rewrite > assoc_times in ⊢ (? ? %). + apply le_times_r. + apply not_bertrand_to_le_B;assumption + |apply le_times_to_le_div + [apply lt_O_S + |apply (trans_le ? (sqrt (exp 2 8))) + [apply leb_true_to_le.reflexivity + |apply monotonic_sqrt. + change in ⊢ (? % ?) with (2*(exp 2 7)). + apply le_times_r. + assumption + ] + ] + ] + ] + ] + ] +qed. + +theorem not_bertrand_to_le2: +\forall n.exp 2 7 \le n \to not_bertrand n \to +2*n / 3 \le (sqrt(2*n)/2)*S(log 2 (2*n)). +intros. +rewrite < (eq_log_exp 2) + [apply (trans_le ? (log 2 ((exp (2*n) (sqrt(2*n)/2))))) + [apply le_log + [apply le_n + |apply not_bertrand_to_le1;assumption + ] + |apply log_exp1. + apply le_n + ] + |apply le_n + ] +qed. + +(* +theorem tech: \forall n. 2*(3*(S(log 2 (2*n)))/4) < sqrt (2*n) \to +(sqrt(2*n)/2)*S(log 2 (2*n)) < 2*n / 3. +intros. + *) diff --git a/helm/software/matita/library/nat/binomial.ma b/helm/software/matita/library/nat/binomial.ma index 1a3410320..e7d58039a 100644 --- a/helm/software/matita/library/nat/binomial.ma +++ b/helm/software/matita/library/nat/binomial.ma @@ -248,4 +248,15 @@ apply eq_sigma_p;intros rewrite < times_n_SO. reflexivity ] -qed. \ No newline at end of file +qed. + +theorem exp_Sn_SSO: \forall n. exp (S n) 2 = S((exp n 2) + 2*n). +intros.simplify. +rewrite < times_n_SO. +rewrite < plus_n_O. +rewrite < sym_times.simplify. +rewrite < assoc_plus. +rewrite < sym_plus. +reflexivity. +qed. + diff --git a/helm/software/matita/library/nat/chebyshev.ma b/helm/software/matita/library/nat/chebyshev.ma index 317a82d15..ff7db61cc 100644 --- a/helm/software/matita/library/nat/chebyshev.ma +++ b/helm/software/matita/library/nat/chebyshev.ma @@ -20,6 +20,203 @@ include "nat/factorial2.ma". definition prim: nat \to nat \def \lambda n. sigma_p (S n) primeb (\lambda p.(S O)). +theorem le_prim_n: \forall n. prim n \le n. +intros.unfold prim. elim n + [apply le_n + |apply (bool_elim ? (primeb (S n1)));intro + [rewrite > true_to_sigma_p_Sn + [rewrite > sym_plus. + rewrite < plus_n_Sm. + rewrite < plus_n_O. + apply le_S_S.assumption + |assumption + ] + |rewrite > false_to_sigma_p_Sn + [apply le_S.assumption + |assumption + ] + ] + ] +qed. + +theorem not_prime_times_SSO: \forall n. 1 < n \to \lnot prime (2*n). +intros.intro.elim H1. +absurd (2 = 2*n) + [apply H3 + [apply (witness ? ? n).reflexivity + |apply le_n + ] + |apply lt_to_not_eq. + rewrite > times_n_SO in ⊢ (? % ?). + apply lt_times_r. + assumption + ] +qed. + +theorem eq_prim_prim_pred: \forall n. 1 < n \to +(prim (2*n)) = (prim (pred (2*n))). +intros.unfold prim. +rewrite < S_pred + [rewrite > false_to_sigma_p_Sn + [reflexivity + |apply not_prime_to_primeb_false. + apply not_prime_times_SSO. + assumption + ] + |apply (trans_lt ? (2*1)) + [simplify.apply lt_O_S + |apply lt_times_r. + assumption + ] + ] +qed. + +theorem le_prim_n1: \forall n. 4 \le n \to prim (S(2*n)) \le n. +intros.unfold prim. elim H + [simplify.apply le_n + |cut (sigma_p (2*S n1) primeb (λp:nat.1) = sigma_p (S (2*S n1)) primeb (λp:nat.1)) + [apply (bool_elim ? (primeb (S(2*(S n1)))));intro + [rewrite > true_to_sigma_p_Sn + [rewrite > sym_plus. + rewrite < plus_n_Sm. + rewrite < plus_n_O. + apply le_S_S. + rewrite < Hcut. + rewrite > times_SSO. + assumption + |assumption + ] + |rewrite > false_to_sigma_p_Sn + [apply le_S. + rewrite < Hcut. + rewrite > times_SSO. + assumption + |assumption + ] + ] + |apply sym_eq.apply (eq_prim_prim_pred (S n1)). + apply le_S_S.apply (trans_le ? 4) + [apply leb_true_to_le.reflexivity + |assumption + ] + ] + ] +qed. + +(* usefull to kill a successor in bertrand *) +theorem le_prim_n2: \forall n. 7 \le n \to prim (S(2*n)) \le pred n. +intros.unfold prim. elim H + [apply leb_true_to_le.reflexivity. + |cut (sigma_p (2*S n1) primeb (λp:nat.1) = sigma_p (S (2*S n1)) primeb (λp:nat.1)) + [apply (bool_elim ? (primeb (S(2*(S n1)))));intro + [rewrite > true_to_sigma_p_Sn + [rewrite > sym_plus. + rewrite < plus_n_Sm. + rewrite < plus_n_O. + simplify in ⊢ (? ? %). + rewrite > S_pred in ⊢ (? ? %) + [apply le_S_S. + rewrite < Hcut. + rewrite > times_SSO. + assumption + |apply (ltn_to_ltO ? ? H1) + ] + |assumption + ] + |rewrite > false_to_sigma_p_Sn + [simplify in ⊢ (? ? %). + apply (trans_le ? ? ? ? (le_pred_n n1)). + rewrite < Hcut. + rewrite > times_SSO. + assumption + |assumption + ] + ] + |apply sym_eq.apply (eq_prim_prim_pred (S n1)). + apply le_S_S.apply (trans_le ? 4) + [apply leb_true_to_le.reflexivity + |apply (trans_le ? ? ? ? H1). + apply leb_true_to_le.reflexivity + ] + ] + ] +qed. + +(* da spostare *) +theorem le_pred: \forall n,m. n \le m \to pred n \le pred m. +apply nat_elim2;intros + [apply le_O_n + |apply False_ind.apply (le_to_not_lt ? ? H). + apply lt_O_S + |simplify.apply le_S_S_to_le.assumption + ] +qed. + +(* si dovrebbe poter migliorare *) +theorem le_prim_n3: \forall n. 15 \le n \to +prim n \le pred (n/2). +intros. +elim (or_eq_eq_S (pred n)). +elim H1 + [cut (n = S (2*a)) + [rewrite > Hcut. + apply (trans_le ? (pred a)) + [apply le_prim_n2. + apply (le_times_to_le 2) + [apply le_n_Sn + |apply le_S_S_to_le. + rewrite < Hcut. + assumption + ] + |apply le_pred. + apply le_times_to_le_div + [apply lt_O_S + |apply le_n_Sn + ] + ] + |rewrite < H2. + apply S_pred. + apply (ltn_to_ltO ? ? H) + ] + |cut (n=2*(S a)) + [rewrite > Hcut. + rewrite > eq_prim_prim_pred + [rewrite > times_SSO in ⊢ (? % ?). + change in ⊢ (? (? %) ?) with (S (2*a)). + rewrite > sym_times in ⊢ (? ? (? (? % ?))). + rewrite > lt_O_to_div_times + [apply (trans_le ? (pred a)) + [apply le_prim_n2. + apply le_S_S_to_le. + apply (lt_times_to_lt 2) + [apply le_n_Sn + |apply le_S_S_to_le. + rewrite < Hcut. + apply le_S_S. + assumption + ] + |apply le_pred. + apply le_n_Sn + ] + |apply lt_O_S + ] + |apply le_S_S. + apply not_lt_to_le.intro. + apply (le_to_not_lt ? ? H). + rewrite > Hcut. + lapply (le_S_S_to_le ? ? H3) as H4. + apply (le_n_O_elim ? H4). + apply leb_true_to_le.reflexivity + ] + |rewrite > times_SSO. + rewrite > S_pred + [apply eq_f.assumption + |apply (ltn_to_ltO ? ? H) + ] + ] + ] +qed. + (* This is chebishev psi function *) definition A: nat \to nat \def \lambda n. pi_p (S n) primeb (\lambda p.exp p (log p n)). @@ -1511,23 +1708,6 @@ theorem A_SSSSO: A (S(S(S(S O)))) = S(S(S(S(S(S(S(S(S(S(S(S O))))))))))). reflexivity. qed. -(* da spostare *) -theorem or_eq_eq_S: \forall n.\exists m. -n = (S(S O))*m \lor n = S ((S(S O))*m). -intro.elim n - [apply (ex_intro ? ? O). - left.reflexivity - |elim H.elim H1 - [apply (ex_intro ? ? a). - right.apply eq_f.assumption - |apply (ex_intro ? ? (S a)). - left.rewrite > H2. - apply sym_eq. - apply times_SSO - ] - ] -qed. - (* (* a better result *) theorem le_A_exp3: \forall n. S O < n \to @@ -1987,7 +2167,7 @@ apply (trans_le ? (2*(4*n*(B (4*n))))) qed. theorem le_priml: \forall n. O < n \to -(S(S O))*n \le (S (log (S(S O)) ((S(S O))*n)))*S(prim ((S(S O))*n)). +2*n \le (S (log 2 (2*n)))*S(prim (2*n)). intros. rewrite < (eq_log_exp (S(S O))) in ⊢ (? % ?) [apply (trans_le ? ((log (S(S O)) (exp ((S(S O))*n) (S(prim ((S(S O))*n))))))) @@ -2017,3 +2197,68 @@ apply (trans_le ? (exp (A n) 2)) ] qed. +(* bounds *) +theorem le_primr: \forall n. 1 < n \to prim n \le 2*(2*n-3)/log 2 n. +intros. +apply le_times_to_le_div + [apply lt_O_log + [apply lt_to_le.assumption + |assumption + ] + |apply (trans_le ? (log 2 (exp n (prim n)))) + [rewrite > sym_times. + apply log_exp2 + [apply le_n + |apply lt_to_le.assumption + ] + |rewrite < (eq_log_exp 2) in ⊢ (? ? %) + [apply le_log + [apply le_n + |apply le_exp_primr + ] + |apply le_n + ] + ] + ] +qed. + +theorem le_priml1: \forall n. O < n \to +2*n/((log 2 n)+2) - 1 \le prim (2*n). +intros. +apply le_plus_to_minus. +apply le_times_to_le_div2 + [rewrite > sym_plus. + simplify.apply lt_O_S + |rewrite > sym_times in ⊢ (? ? %). + rewrite < plus_n_Sm. + rewrite < plus_n_Sm in ⊢ (? ? (? ? %)). + rewrite < plus_n_O. + rewrite < sym_plus. + rewrite < log_exp + [simplify in ⊢ (? ? (? (? (? ? (? % ?))) ?)). + apply le_priml. + assumption + |apply le_n + |assumption + ] + ] +qed. + +(* +theorem prim_SSSSSSO: \forall n.30\le n \to O < prim (8*n) - prim n. +intros. +apply lt_to_lt_O_minus. +change in ⊢ (? ? (? (? % ?))) with (2*4). +rewrite > assoc_times. +apply (le_to_lt_to_lt ? (2*(2*n-3)/log 2 n)) + [apply le_primr.apply (trans_lt ? ? ? ? H). + apply leb_true_to_le.reflexivity + |apply (lt_to_le_to_lt ? (2*(4*n)/((log 2 (4*n))+2) - 1)) + [elim H + [ +normalize in ⊢ (%);simplify. + |apply le_priml1. +*) + + + diff --git a/helm/software/matita/library/nat/chebyshev_teta.ma b/helm/software/matita/library/nat/chebyshev_teta.ma index bdec36391..4c839892a 100644 --- a/helm/software/matita/library/nat/chebyshev_teta.ma +++ b/helm/software/matita/library/nat/chebyshev_teta.ma @@ -385,7 +385,7 @@ apply divides_to_le ] qed. -theorem lt_O_to_le_teta_M_teta: \forall m. O < m\to +theorem lt_O_to_le_teta_exp_teta: \forall m. O < m\to teta (S(2*m)) < exp 2 (2*m)*teta (S m). intros. apply (le_to_lt_to_lt ? (M m*teta (S m))) @@ -398,5 +398,105 @@ apply (le_to_lt_to_lt ? (M m*teta (S m))) ] qed. +theorem teta_pred: \forall n. S O < n \to teta (2*n) = teta (pred (2*n)). +intros.unfold teta. +rewrite > false_to_pi_p_Sn + [rewrite < S_pred + [reflexivity + |rewrite > (times_n_O 2) in ⊢ (? % ?). + apply lt_times_r. + apply lt_to_le.assumption + ] + |apply not_prime_to_primeb_false. + intro. + elim H1. + apply (lt_to_not_eq ? ? H). + apply (injective_times_r 1). + rewrite < times_n_SO. + apply H3 + [apply (witness ? ? n).reflexivity + |apply le_n + ] + ] +qed. +theorem le_teta: \forall m.teta m \le exp 2 (2*m). +intro.apply (nat_elim1 m).intros. +elim (or_eq_eq_S m1). +elim H1 + [rewrite > H2. + generalize in match H2. + cases a + [intro.apply le_n + |cases n;intros + [apply leb_true_to_le.reflexivity + |rewrite > teta_pred + [rewrite > times_SSO. + change in ⊢ (? (? %) ?) with (S (2*S n1)). + apply (trans_le ? (exp 2 (2*(S n1))*teta (S (S n1)))) + [apply lt_to_le. + apply lt_O_to_le_teta_exp_teta. + apply lt_O_S + |rewrite < times_SSO. + change in ⊢ (? ? (? ? %)) with ((2*S (S n1))+((2*S (S n1)) + O)). + rewrite < plus_n_O. + rewrite > exp_plus_times. + apply le_times + [apply le_exp + [apply lt_O_S + |apply le_times_r. + apply le_n_Sn + ] + |apply H. + rewrite > H3. + apply lt_m_nm + [apply lt_O_S + |apply le_n + ] + ] + ] + |apply le_S_S.apply lt_O_S + ] + ] + ] + |rewrite > H2. + generalize in match H2. + cases a;intro + [apply leb_true_to_le.reflexivity + |apply (trans_le ? (exp 2 (2*(S n))*teta (S (S n)))) + [apply lt_to_le. + apply lt_O_to_le_teta_exp_teta. + apply lt_O_S + |change in ⊢ (? ? (? ? %)) with (S (2*S n) + (S (2*S n) +O)). + rewrite < plus_n_O. + rewrite < plus_n_Sm. + rewrite < sym_plus. + rewrite > plus_n_Sm. + rewrite > exp_plus_times. + apply le_times_r. + rewrite < times_SSO. + apply H. + rewrite > H3. + apply le_S_S. + apply lt_m_nm + [apply lt_O_S + |apply le_n + ] + ] + ] + ] +qed. + +(* +alias id "sqrt" = "cic:/matita/nat/sqrt/sqrt.con". +alias id "not" = "cic:/matita/logic/connectives/Not.con". +theorem absurd_bound: \forall n. exp 2 7 \le n \to +(\forall p. n < p \to p < 2*n \to not (prime p)) \to +bc (2*n) n < exp (2*n) (div (sqrt (2*n)) 2 - 1)*exp 4 (div (2*n) 3). +intros. +cut (O < n) + [cut (sqrt (2*n) < div (2*n) 3) + [ + | +*) diff --git a/helm/software/matita/library/nat/exp.ma b/helm/software/matita/library/nat/exp.ma index 25c81c069..52793cb5a 100644 --- a/helm/software/matita/library/nat/exp.ma +++ b/helm/software/matita/library/nat/exp.ma @@ -207,6 +207,23 @@ elim (le_to_or_lt_eq n m) ] ] qed. + +theorem lt_exp_to_lt1: +\forall a,n,m. O < a \to exp n a < exp m a \to n < m. +intros. +elim (le_to_or_lt_eq n m) + [assumption + |apply False_ind. + apply (lt_to_not_eq ? ? H1). + rewrite < H2. + reflexivity + |apply (le_exp_to_le1 ? ? a) + [assumption + |apply lt_to_le. + assumption + ] + ] +qed. theorem times_exp: \forall n,m,p. exp n p * exp m p = exp (n*m) p. diff --git a/helm/software/matita/library/nat/factorial2.ma b/helm/software/matita/library/nat/factorial2.ma index 594feb51f..6215d6657 100644 --- a/helm/software/matita/library/nat/factorial2.ma +++ b/helm/software/matita/library/nat/factorial2.ma @@ -25,11 +25,6 @@ theorem exp_S: \forall n,m. exp m (S n) = m*exp m n. intros.reflexivity. qed. -alias num (instance 0) = "natural number". -lemma times_SSO: \forall n.2*(S n) = S(S(2*n)). -intro.simplify.rewrite < plus_n_Sm.reflexivity. -qed. - theorem lt_O_to_fact1: \forall n.O true_to_pi_p_Sn + [rewrite > true_to_sigma_p_Sn + [simplify. + rewrite > H. + rewrite > exp_plus_times. + reflexivity. + |assumption + ] + |assumption + ] + |intro. + rewrite > false_to_pi_p_Sn + [rewrite > false_to_sigma_p_Sn + [simplify.assumption + |assumption + ] + |assumption + ] + ] + ] +qed. + theorem times_pi_p: \forall n,p,f,g. pi_p n p (\lambda x.f x*g x) = pi_p n p f * pi_p n p g. intros. diff --git a/helm/software/matita/library/nat/sqrt.ma b/helm/software/matita/library/nat/sqrt.ma index 733afe641..f738e1cf2 100644 --- a/helm/software/matita/library/nat/sqrt.ma +++ b/helm/software/matita/library/nat/sqrt.ma @@ -204,3 +204,18 @@ apply f_m_to_le_max |simplify;apply le_exp_log;assumption] |rewrite < H1;simplify;apply le_n]] qed. + +(* monotonicity *) +theorem monotonic_sqrt: monotonic nat le sqrt. +unfold.intros. +unfold sqrt in ⊢ (? ? (% ?)). +apply f_m_to_le_max + [apply (trans_le ? ? ? ? H). + apply le_sqrt_n_n + |apply le_to_leb_true. + apply (trans_le ? ? ? ? H). + apply leq_sqrt_n + ] +qed. + + diff --git a/helm/software/matita/library/nat/times.ma b/helm/software/matita/library/nat/times.ma index 24a2846d7..ec0f86199 100644 --- a/helm/software/matita/library/nat/times.ma +++ b/helm/software/matita/library/nat/times.ma @@ -21,7 +21,6 @@ let rec times n m \def [ O \Rightarrow O | (S p) \Rightarrow m+(times p m) ]. -(*CSC: the URI must disappear: there is a bug now *) interpretation "natural times" 'times x y = (cic:/matita/nat/times/times.con x y). theorem times_n_O: \forall n:nat. O = n*O. @@ -68,6 +67,27 @@ rewrite < plus_n_O. reflexivity. qed. +alias num (instance 0) = "natural number". +lemma times_SSO: \forall n.2*(S n) = S(S(2*n)). +intro.simplify.rewrite < plus_n_Sm.reflexivity. +qed. + +theorem or_eq_eq_S: \forall n.\exists m. +n = (S(S O))*m \lor n = S ((S(S O))*m). +intro.elim n + [apply (ex_intro ? ? O). + left.reflexivity + |elim H.elim H1 + [apply (ex_intro ? ? a). + right.apply eq_f.assumption + |apply (ex_intro ? ? (S a)). + left.rewrite > H2. + apply sym_eq. + apply times_SSO + ] + ] +qed. + theorem symmetric_times : symmetric nat times. unfold symmetric. intros.elim x. -- 2.39.2