From: Andrea Asperti Date: Wed, 19 Dec 2012 17:05:03 +0000 (+0000) Subject: bertrand! X-Git-Tag: make_still_working~1381 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9e078dc1cbf90124fecf391e4c3b717fd1143afb;p=helm.git bertrand! -tThis line, and those below, will be ignored-- A chebyshev/bertrand256.ma A chebyshev/bertrand.ma --- diff --git a/matita/matita/lib/arithmetics/chebyshev/bertrand.ma b/matita/matita/lib/arithmetics/chebyshev/bertrand.ma new file mode 100644 index 000000000..572c512ae --- /dev/null +++ b/matita/matita/lib/arithmetics/chebyshev/bertrand.ma @@ -0,0 +1,461 @@ +(* + ||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/sqrt.ma". +include "arithmetics/chebyshev/chebyshev_B.ma". +include "arithmetics/chebyshev/chebyshev_teta.ma". + +definition bertrand ≝ λn. ∃p.n < p ∧ p \le 2*n ∧ (prime p). + +definition not_bertrand ≝ λn.∀p.n < p → p ≤ 2*n → \not (prime p). + +lemma min_prim : ∀n.∃p. n < p ∧ prime p ∧ + ∀q.prime q → q < p → q ≤ n. +#n cases (le_to_or_lt_eq ?? (le_O_n n)) #Hn + [%{(min (S (n!)) (S n) primeb)} % + [%[@le_min_l + |@primeb_true_to_prime @(f_min_true primeb) + cases (ex_prime n Hn) #p * * #ltnp #lep #primep + %{p} % + [% [@ltnp | whd >(plus_n_O p) >plus_n_Sm @le_plus //] + |@prime_to_primeb_true // + ] + ] + |#p #primep #ltp @not_lt_to_le % #ltnp + lapply (lt_min_to_false … ltnp ltp) + >(prime_to_primeb_true ? primep) #H destruct (H) + ] + |%{2} % + [%[k_def elim (log p n) + [@le_n + |#n1 #Hind >bigop_Strue + [>(plus_n_O n1) in ⊢ (??%); >plus_n_Sm >commutative_plus + @le_plus + [@Hind + |@le_S_S_to_le @lt_mod_m_m @lt_O_S + ] + |// + ] + ] +qed. + +definition B1 ≝ λn. + ∏_{p < S n | primeb p}(exp p (k n p)). + +lemma B1_def : ∀n. B1 n = ∏_{p < S n | primeb p}(exp p (k n p)). +// qed. + +definition Dexp ≝ mk_Dop nat 1 timesAC (λa,b.exp b a) ??. + [// | normalize //] +qed. + +theorem eq_B_B1: ∀n. B n = B1 n. +#n >Bdef >B1_def @same_bigop + [// |#i #ltiS #_ >k_def @exp_sigma_l] +qed. + +definition B_split1 ≝ λn. + ∏_{p < S n | primeb p}(exp p (bool_to_nat (leb (k n p) 1)* (k n p))). + +lemma B_split1_def : ∀n. + B_split1 n = ∏_{p < S n | primeb p}(exp p (bool_to_nat (leb (k n p) 1)* (k n p))). +// qed. + +definition B_split2 ≝ λn. + ∏_{p < S n | primeb p}(exp p (bool_to_nat (leb 2 (k n p))* (k n p))). + +lemma B_split2_def : ∀n. + B_split2 n = ∏_{p < S n | primeb p}(exp p (bool_to_nat (leb 2 (k n p))* (k n p))). +// qed. + +theorem eq_B1_times_B_split1_B_split2: ∀n. + B1 n = B_split1 n * B_split2 n. +#n >B1_def >B_split1_def >B_split2_def Hc + [>(lt_to_leb_false 2 (k n p)) + [commutative_times (le_to_leb_true 2 (k n p)) + [>commutative_times commutative_times k_def +elim (log p (2*n)) + [// + |#i #Hind >bigop_Strue + [>Hind Hcut //] + @lt_to_le_times_to_lt_S_to_div + [@(ltn_to_ltO ?? ltp) + |commutative_times in ⊢ (??%); @lt_div_to_times // + ] + |#n2 cut (2*n/(p)\sup(S (S n2)) = O) [2:#Hcut >Hcut //] + @lt_to_div_O @(le_to_lt_to_lt ? (exp ((2*n)/3) 2)) + [@(le_times_to_le (exp 3 2)) + [@leb_true_to_le // + |>commutative_times in ⊢ (??%); > times_exp + @(transitive_le ? (exp n 2)) + [exp_2 in ⊢ (??%); @le_times // + |@(le_exp1 … (lt_O_S ?)) + @(le_plus_to_le 3) + cut (3+2*n/3*3 = S(2*n/3)*3) [//] #eq1 >eq1 + @(transitive_le ? (2*n)) + [normalize in ⊢(??%); B_split1_def >teta_def +@(transitive_le ? (∏_{p < S (2*n) | primeb p} (p\sup(bool_to_nat (eqb (k (2*n) p) 1))))) + [@le_pi #p #ltp #primebp @le_exp + [@prime_to_lt_O @primeb_true_to_prime // + |cases (true_or_false (leb (k (2*n) p) 1)) #Hc + [cases (le_to_or_lt_eq ? ? (leb_true_to_le ?? Hc)) -Hc #Hc + [lapply (le_S_S_to_le ?? Hc) -Hc #Hc + @(le_n_O_elim ? Hc) (eq_to_eqb_true ?? Hc) >Hc @le_n + ] + |>Hc @le_O_n + ] + ] + |@(transitive_le ? (∏_{p < S (2*n/3) | primeb p} (p\sup(bool_to_nat (eqb (k (2*n) p) 1))))) + [>(pad_bigop_nil (S(2*n)) (S (2*n/3)) primeb ? 1 timesA) [//] + [#i #lei #lti whd in not_Bn; + cases (decidable_le (S n) i) #Hc + [%1 @not_prime_to_primeb_false @not_Bn [//|@le_S_S_to_le //] + |%2 >k1 // @not_lt_to_le @Hc + ] + |@le_S_S @le_times_to_le_div2 + [@lt_O_S + |>commutative_times in ⊢ (??%); @le_times // + ] + ] + |@le_pi #i #lti #primei cases (eqb (k (2*n) i) 1) + [B_split2_def +cut (O < n) [@(lt_to_le_to_lt … len) @leb_true_to_le //] #posn +@(transitive_le ? + (∏_{p < S (sqrt (2*n)) | primeb p} + (p\sup(bool_to_nat (leb 2 (k (2*n) p))*k (2*n) p)))) + [>(pad_bigop_nil (S (2*n)) (S(sqrt(2*n))) primeb ? 1 timesA) + [//|3: @le_S_S @le_sqrt_n] + #p #lep #ltp cases (true_or_false (leb 2 (k (2*n) p))) #Hc + [@False_ind @(absurd ?? (lt_to_not_le ?? lep)) + @(true_to_le_max … ltp) @le_to_leb_true (times_n_1 0) in ⊢ (?%?); >commutative_times in ⊢ (?%?); + @lt_times // + |@le_to_leb_true @(transitive_le ? n) // + ] + |#m #lt1m @lt_to_leb_false @(lt_to_le_to_lt … H2n) + @le_exp [@(ltn_to_ltO ?? lep) |//] + ] + |@(transitive_le ? (k (2*n) p)) [@leb_true_to_le //|@le_k] + ] + |%2 >Hc % + ] + |@(transitive_le ? (∏_{p < S (sqrt (2*n)) | primeb p} (2*n))) + [@le_pi #p #ltp #primep @(transitive_le ? (exp p (log p (2*n)))) + [@le_exp + [@prime_to_lt_O @primeb_true_to_prime // + |cases (true_or_false (leb 2 (k (2*n) p))) #Hc >Hc + [>commutative_times (times_n_O O) in ⊢ (?%?); @lt_times // + ] + |@(transitive_le ? (exp (2*n) (prim(sqrt (2*n))))) + [>exp_sigma // + |@le_exp + [>(times_n_O O) in ⊢ (?%?); @lt_times // + |@le_prim_n3 @true_to_le_max + [@(transitive_le ? (2*(exp 2 7))) + [@leb_true_to_le // |@le_S @monotonic_le_times_r //] + |@le_to_leb_true @(transitive_le ? (2*(exp 2 7))) + [@leb_true_to_le % | @monotonic_le_times_r //] + ] + ] + ] + ] + ] +qed. + +theorem not_bertrand_to_le_B: + ∀n.exp 2 7 ≤ n → not_bertrand n → + B (2*n) ≤ (exp 2 (2*(2 * n / 3)))*(exp (2*n) (pred(sqrt(2*n)/2))). +#n #len #notB >eq_B_B1 >eq_B1_times_B_split1_B_split2 @le_times + [@(transitive_le ? (teta ((2*n)/3))) + [@le_B_split1_teta [@(transitive_le … len) @leb_true_to_le //|//] + |@le_teta + ] + |@le_B_split2_exp // + ] +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)))). +*) + +lemma le_times_div_m_m: ∀n,m. O < m → n/m*m ≤ n. +#n #m #posm >(div_mod n m) in ⊢ (??%); // +qed. + +theorem not_bertrand_to_le1: + ∀n.exp 2 7 ≤ n → not_bertrand n → + exp 2 (2*n / 3) ≤ exp (2*n) (sqrt(2*n)/2). +#n #len #notB @(le_times_to_le (exp 2 (2*(2 * n / 3)))) + [@lt_O_exp @lt_O_S + |Heq + >commutative_times @le_times_div_m_m @lt_O_S + |@(transitive_le ? (2*n*B(2*n))) + [@le_exp_B @(transitive_le …len) @leb_true_to_le // + |<(S_pred (sqrt (2*n)/2)) + [whd in ⊢ (??(??%)); commutative_times @le_times // + ] + ] + ] + ] + ] +qed. + +theorem not_bertrand_to_le2: + ∀n.exp 2 7 ≤ n → not_bertrand n → + 2*n / 3 ≤ (sqrt(2*n)/2)*S(log 2 (2*n)). +#n #len #notB <(eq_log_exp 2 (2*n/3) (le_n ?)) +@(transitive_le ? (log 2 ((exp (2*n) (sqrt(2*n)/2))))) + [@le_log [@le_n|@not_bertrand_to_le1 //] |@log_exp1 @le_n] +qed. + +lemma lt_div_S_div: ∀n,m. O < m → exp m 2 ≤ n → + n/(S m) < n/m. +#n #m #posm #len @lt_times_to_lt_div @(lt_to_le_to_lt ? (S(n/m)*m)) + [@lt_div_S // + |commutative_times commutative_times @le_plus [2://] + @le_times_to_le_div // + ] +qed. + +lemma times_div_le: ∀a,b,c,d.O < b → O < d → + (a/b)*(c/d) ≤ (a*c)/(b*d). +#a #b #c #d #posa #posb @le_times_to_le_div + [>(times_n_O O) @lt_times // + |cut (∀n,m,p,q.n*m*(p*q) = p*n*(q*m)) [//] #Heq >Heq + @le_times // + ] +qed. + +lemma tech: ∀n. 2*(S(log 2 (2*n))) ≤ sqrt (2*n) → + (sqrt(2*n)/2)*S(log 2 (2*n)) ≤ 2*n / 4. +#n #H +cut (4 = 2*2) [//] #H4 +cut (4*(S(log 2 (2*n))) ≤ 2* sqrt(2*n)) + [>H4 >associative_times @monotonic_le_times_r @H] #H1 +>commutative_times @(le_times_to_le_div … (lt_O_S ?)) +associative_times >commutative_times >(div_times … (lt_O_S …)) @leq_sqrt_n + ] + ] +qed. + +(* we need a "good" lower bound for sqrt (2*n) *) +lemma exp_to_log_r : ∀b,n,m. 1 < b → n < m → exp b n ≤ m → n ≤ log b m. +#b #n #m #lt1b #ltnm #Hexp @true_to_le_max [@ltnm |@le_to_leb_true //] +qed. + +lemma square_double :∀n. 2 < n → (S n)*(S n) ≤ 2*n*n. +#n #posn normalize (plus_n_O (n+(n+n*n))) +cut (S(n+(n+n*n)+0)=n*n+(n+(S n))) [//] #Hcut >Hcut >distributive_times_plus_r +@monotonic_le_plus_r Hcut1 +@monotonic_lt_times_l [@(ltn_to_ltO … posn) |@posn] +qed. + +(* axiom daemon : ∀P:Prop.P. *) + +lemma sqrt_bound: ∀n. exp 2 8 ≤ n → 2*(S(log 2 (2*n))) ≤ sqrt (2*n). +#n #len +cut (8 ≤ log 2 n) [<(eq_log_exp 2 8) [@le_log [@le_n|@len]|@le_n]] #Hlog +cut (0(exp_n_1 2) in ⊢ (? (? ? (? (? ? (? % ?)))) ?); +>(log_exp … (le_n ?) posn) >commutative_plus >plus_n_Sm @true_to_le_max + [@le_S_S @monotonic_le_times_r + cut (2(plus_n_O m) in ⊢ (?%?); >plus_n_Sm @monotonic_le_plus_r // + |>(exp_n_1 2) in ⊢ (?(?(??%)?)?);>(log_exp … (le_n ?) posm) @le_S_S @Hind + ] + |@le_to_leb_true >associative_times @monotonic_le_times_r + >commutative_plus + lapply len @(nat_elim1 n) #m #Hind #lem + cut (8(eq_log_exp … (le_n ?)) @le_n + |cases (le_to_or_lt_eq … lem) -lem #Hcasem + [lapply (Hind (2^((log 2 m)-1)) ??) + [@le_exp [@lt_O_S] @le_plus_to_minus_r + @(lt_exp_to_lt 2 8) [@lt_O_S | >Hclog @Hcasem] + |(plus_n_O (log 2 m -1)) + >plus_n_Sm (eq_log_exp … (le_n ?)) >(eq_log_exp … (le_n ?)) + >plus_minus_commutative [2:@lt_O_log //] + cut (2+3 ≤ 2+log 2 m) + [@monotonic_le_plus_r @(le_exp_to_le 2) [@le_n|>Hclog @lt_to_le @lt8m]] + generalize in match (2+log 2 m); #a #Hle >(commutative_times 2 a) + (commutative_times ? 2) lapply Hle cases a + [//| #a0 -Hle #Hle whd in match (S a0 -1); <(minus_n_O a0) + @square_double @le_S_S_to_le @lt_to_le @Hle] + ] + |(eq_log_exp … (le_n ?)) @leb_true_to_le % + ] + ] + ] +qed. + +theorem le_to_bertrand2: + ∀n. 2^8 ≤ n → bertrand n. +#n #len @not_not_bertrand_to_bertrand % #notBn +@(absurd (2*n / 3 \le (sqrt(2*n)/2)*S(log 2 (2*n)))) + [@not_bertrand_to_le2 + [@(transitive_le ???? len) @le_exp [@lt_O_S|@le_n_Sn]|//] + |@lt_to_not_le + @(le_to_lt_to_lt ???? (lt_div_S_div ????)) + [@tech @sqrt_bound // + |@(transitive_le ? (2*exp 2 8)) + [@leb_true_to_le // |@monotonic_le_times_r //] + |@lt_O_S + ] + ] +qed. + +(* +theorem bertrand_n : +\forall n. O < n \to bertrand n. +intros;elim (decidable_le n 256) + [apply le_to_bertrand;assumption + |apply le_to_bertrand2;apply lt_to_le;apply not_le_to_lt;apply H1] +qed. *) + +(* test +theorem mod_exp: eqb (mod (exp 2 8) 13) O = false. +reflexivity. +*) diff --git a/matita/matita/lib/arithmetics/chebyshev/bertrand256.ma b/matita/matita/lib/arithmetics/chebyshev/bertrand256.ma new file mode 100644 index 000000000..074434722 --- /dev/null +++ b/matita/matita/lib/arithmetics/chebyshev/bertrand256.ma @@ -0,0 +1,889 @@ +(* + ||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/chebyshev/chebyshev_teta.ma". + +(* include "nat/sqrt.ma". +include "nat/chebyshev_teta.ma". +include "nat/chebyshev.ma". +include "list/in.ma". +include "list/sort.ma". +include "nat/o.ma". +include "nat/sieve.ma". *) + +(* +let rec list_divides l n \def + match l with + [ nil ⇒ false + | cons (m:nat) (tl:list nat) ⇒ orb (divides_b m n) (list_divides tl n) ]. + +definition lprim : nat \to list nat \def + \lambda n.let rec aux m acc \def + match m with + [ O => acc + | S m1 => match (list_divides acc (n-m1)) with + [ true => aux m1 acc + | false => aux m1 (n-m1::acc)]] + in aux (pred n) []. + +let rec checker l \def + match l with + [ nil => true + | cons h1 t1 => match t1 with + [ nil => true + | cons h2 t2 => (andb (checker t1) (leb h1 (2*h2))) ]]. + +lemma checker_cons : \forall t,l.checker (t::l) = true \to checker l = true. +intros 2;simplify;intro;elim l in H ⊢ % + [reflexivity + |change in H1 with (andb (checker (a::l1)) (leb t (a+(a+O))) = true); + apply (andb_true_true ? ? H1)] +qed. + +theorem checker_sound : \forall l1,l2,l,x,y.l = l1@(x::y::l2) \to + checker l = true \to x \leq 2*y. +intro;elim l1 0 + [simplify;intros 5;rewrite > H;simplify;intro; + apply leb_true_to_le;apply (andb_true_true_r ? ? H1); + |simplify;intros;rewrite > H1 in H2;lapply (checker_cons ? ? H2); + apply (H l2 ? ? ? ? Hletin);reflexivity] +qed. +*) + +definition bertrand ≝ λn. ∃p.n < p ∧ p \le 2*n ∧ (prime p). + +definition not_bertrand ≝ λn.∀p.n < p → p ≤ 2*n → \not (prime p). + +lemma min_prim : ∀n.∃p. n < p ∧ prime p ∧ + ∀q.prime q → q < p → q ≤ n. +#n cases (le_to_or_lt_eq ?? (le_O_n n)) #Hn + [%{(min (S (n!)) (S n) primeb)} % + [%[@le_min_l + |@primeb_true_to_prime @(f_min_true primeb) + cases (ex_prime n Hn) #p * * #ltnp #lep #primep + %{p} % + [% [@ltnp | whd >(plus_n_O p) >plus_n_Sm @le_plus //] + |@prime_to_primeb_true // + ] + ] + |#p #primep #ltp @not_lt_to_le % #ltnp + lapply (lt_min_to_false … ltnp ltp) + >(prime_to_primeb_true ? primep) #H destruct (H) + ] + |%{2} % + [%[ H4.apply H1 + |elim (check_list1 ? ? ? H1).clear H1. + elim H4.clear H4. + elim H1.clear H1. + elim (in_list_cons_case ? ? ? ? H2) + [apply (ex_intro ? ? n). + split + [split + [apply in_list_cons.apply in_list_head + |rewrite > H1.assumption + ] + |rewrite > H1.assumption + ] + |elim (H H6 p H1 H3).clear H. + apply (ex_intro ? ? a1). + elim H8.clear H8. + elim H.clear H. + split + [split + [apply in_list_cons.assumption + |assumption + ] + |assumption + ] + ] + ] + ] +qed. + +(* qualcosa che non va con gli S *) +lemma le_to_bertrand : \forall n.O < n \to n \leq exp 2 8 \to bertrand n. +intros. +apply (list_of_primes_to_bertrand ? (S(exp 2 8)) (sieve (S(exp 2 8)))) + [assumption + |apply primeb_true_to_prime.reflexivity + |apply (le_to_lt_to_lt ? ? ? H1). + apply le_n + |lapply (sieve_sound1 (S(exp 2 8))) as H + [elim H.assumption + |apply leb_true_to_le.reflexivity + ] + |intros.apply (sieve_sound2 ? ? H3 H2) + |apply check_list2. + reflexivity + ] +qed. + +lemma not_not_bertrand_to_bertrand1: \forall n. +\lnot (not_bertrand n) \to \forall x. n \le x \to x \le 2*n \to +(\forall p.x < p \to p \le 2*n \to \not (prime p)) +\to \exists p.n < p \land p \le x \land (prime p). +intros 4.elim H1 + [apply False_ind.apply H.assumption + |apply (bool_elim ? (primeb (S n1)));intro + [apply (ex_intro ? ? (S n1)). + split + [split + [apply le_S_S.assumption + |apply le_n + ] + |apply primeb_true_to_prime.assumption + ] + |elim H3 + [elim H7.clear H7. + elim H8.clear H8. + apply (ex_intro ? ? a). + split + [split + [assumption + |apply le_S.assumption + ] + |assumption + ] + |apply lt_to_le.assumption + |elim (le_to_or_lt_eq ? ? H7) + [apply H5;assumption + |rewrite < H9. + apply primeb_false_to_not_prime. + assumption + ] + ] + ] + ] +qed. + +theorem not_not_bertrand_to_bertrand: \forall n. +\lnot (not_bertrand n) \to bertrand n. +unfold bertrand.intros. +apply (not_not_bertrand_to_bertrand1 ? ? (2*n)) + [assumption + |apply le_times_n.apply le_n_Sn + |apply le_n + |intros.apply False_ind. + apply (lt_to_not_le ? ? H1 H2) + ] +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 + ] + |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 tech1: \forall a,b,c,d.O < b \to O < d \to +(a/b)*(c/d) \le (a*c)/(b*d). +intros. +apply le_times_to_le_div + [rewrite > (times_n_O O). + apply lt_times;assumption + |rewrite > assoc_times. + rewrite < assoc_times in ⊢ (? (? ? %) ?). + rewrite < sym_times in ⊢ (? (? ? (? % ?)) ?). + rewrite > assoc_times. + rewrite < assoc_times. + apply le_times; + rewrite > sym_times;apply le_times_div_m_m;assumption + ] +qed. + +theorem tech: \forall n. 2*(S(log 2 (2*n))) \le sqrt (2*n) \to +(sqrt(2*n)/2)*S(log 2 (2*n)) \le 2*n / 4. +intros. +cut (4*(S(log 2 (2*n))) \le 2* sqrt(2*n)) + [rewrite > sym_times. + apply le_times_to_le_div + [apply lt_O_S + |rewrite < assoc_times. + apply (trans_le ? (2*sqrt(2*n)*(sqrt (2*n)/2))) + [apply le_times_l.assumption + |apply (trans_le ? ((2*sqrt(2*n)*(sqrt(2*n))/2))) + [apply le_times_div_div_times. + apply lt_O_S + |rewrite > assoc_times. + rewrite > sym_times. + rewrite > lt_O_to_div_times. + apply leq_sqrt_n. + apply lt_O_S + ] + ] + ] + |change in ⊢ (? (? % ?) ?) with (2*2). + rewrite > assoc_times. + apply le_times_r. + assumption + ] +qed. + +theorem lt_div_S_div: \forall n,m. O < m \to exp m 2 \le n \to +n/(S m) < n/m. +intros. +apply lt_times_to_lt_div. +apply (lt_to_le_to_lt ? (S(n/m)*m)) + [apply lt_div_S.assumption + |rewrite > sym_times in ⊢ (? ? %). simplify. + rewrite > sym_times in ⊢ (? ? (? ? %)). + apply le_plus_l. + apply le_times_to_le_div + [assumption + |rewrite < exp_SSO. + assumption + ] + ] +qed. + +theorem exp_plus_SSO: \forall a,b. exp (a+b) 2 = (exp a 2) + 2*a*b + (exp b 2). +intros. +rewrite > exp_SSO. +rewrite > distr_times_plus. +rewrite > times_plus_l. +rewrite < exp_SSO. +rewrite > assoc_plus. +rewrite > assoc_plus. +apply eq_f. +rewrite > times_plus_l. +rewrite < exp_SSO. +rewrite < assoc_plus. +rewrite < sym_times. +rewrite > plus_n_O in ⊢ (? ? (? (? ? %) ?) ?). +rewrite > assoc_times. +apply eq_f2;reflexivity. +qed. + +theorem tech3: \forall n. (exp 2 8) \le n \to 2*(S(log 2 (2*n))) \le sqrt (2*n). +intros. +lapply (le_log 2 ? ? (le_n ?) H) as H1. +rewrite > exp_n_SO in ⊢ (? (? ? (? (? ? (? % ?)))) ?). +rewrite > log_exp + [rewrite > sym_plus. + rewrite > plus_n_Sm. + unfold sqrt. + apply f_m_to_le_max + [apply le_times_r. + apply (trans_le ? (2*log 2 n)) + [rewrite < times_SSO_n. + apply le_plus_r. + apply (trans_le ? 8) + [apply leb_true_to_le.reflexivity + |rewrite < (eq_log_exp 2) + [assumption + |apply le_n + ] + ] + |apply (trans_le ? ? ? ? (le_exp_log 2 ? ? )). + apply le_times_SSO_n_exp_SSO_n. + apply (lt_to_le_to_lt ? ? ? ? H). + apply leb_true_to_le.reflexivity + ] + |apply le_to_leb_true. + rewrite > assoc_times. + apply le_times_r. + rewrite > sym_times. + rewrite > assoc_times. + rewrite < exp_SSO. + rewrite > exp_plus_SSO. + rewrite > distr_times_plus. + rewrite > distr_times_plus. + rewrite > assoc_plus. + apply (trans_le ? (4*exp (log 2 n) 2)) + [change in ⊢ (? ? (? % ?)) with (2*2). + rewrite > assoc_times in ⊢ (? ? %). + rewrite < times_SSO_n in ⊢ (? ? %). + apply le_plus_r. + rewrite < times_SSO_n in ⊢ (? ? %). + apply le_plus + [rewrite > sym_times in ⊢ (? (? ? %) ?). + rewrite < assoc_times. + rewrite < assoc_times. + change in ⊢ (? (? % ?) ?) with 8. + rewrite > exp_SSO. + apply le_times_l. + (* strange things here *) + rewrite < (eq_log_exp 2) + [assumption + |apply le_n + ] + |apply (trans_le ? (log 2 n)) + [change in ⊢ (? % ?) with 8. + rewrite < (eq_log_exp 2) + [assumption + |apply le_n + ] + |rewrite > exp_n_SO in ⊢ (? % ?). + apply le_exp + [apply lt_O_log + [apply (lt_to_le_to_lt ? ? ? ? H). + apply leb_true_to_le.reflexivity + |apply (lt_to_le_to_lt ? ? ? ? H). + apply leb_true_to_le.reflexivity + ] + |apply le_n_Sn + ] + ] + ] + |change in ⊢ (? (? % ?) ?) with (exp 2 2). + apply (trans_le ? ? ? ? (le_exp_log 2 ? ?)) + [apply le_times_exp_n_SSO_exp_SSO_n + [apply le_n + |change in ⊢ (? % ?) with 8. + rewrite < (eq_log_exp 2) + [assumption + |apply le_n + ] + ] + |apply (lt_to_le_to_lt ? ? ? ? H). + apply leb_true_to_le.reflexivity + ] + ] + ] + |apply le_n + |apply (lt_to_le_to_lt ? ? ? ? H). + apply leb_true_to_le.reflexivity + ] +qed. + +theorem le_to_bertrand2: +\forall n. (exp 2 8) \le n \to bertrand n. +intros. +apply not_not_bertrand_to_bertrand.unfold.intro. +absurd (2*n / 3 \le (sqrt(2*n)/2)*S(log 2 (2*n))) + [apply not_bertrand_to_le2 + [apply (trans_le ? ? ? ? H). + apply le_exp + [apply lt_O_S + |apply le_n_Sn + ] + |assumption + ] + |apply lt_to_not_le. + apply (le_to_lt_to_lt ? ? ? ? (lt_div_S_div ? ? ? ?)) + [apply tech.apply tech3.assumption + |apply lt_O_S + |apply (trans_le ? (2*exp 2 8)) + [apply leb_true_to_le.reflexivity + |apply le_times_r.assumption + ] + ] + ] +qed. + +theorem bertrand_n : +\forall n. O < n \to bertrand n. +intros;elim (decidable_le n 256) + [apply le_to_bertrand;assumption + |apply le_to_bertrand2;apply lt_to_le;apply not_le_to_lt;apply H1] +qed. + +(* test +theorem mod_exp: eqb (mod (exp 2 8) 13) O = false. +reflexivity. +*)