--- /dev/null
+(*
+ ||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} %
+ [%[<Hn @lt_O_S | @primeb_true_to_prime //]
+ |#p #primep #lt2 @False_ind @(absurd … lt2)
+ @le_to_not_lt @prime_to_lt_SO //
+ ]
+ ]
+qed.
+
+lemma not_not_bertrand_to_bertrand1: ∀n.
+¬(not_bertrand n) → ∀x. n ≤ x → x ≤ 2*n →
+ (∀p.x < p → p ≤ 2*n → ¬(prime p))
+ → ∃p.n < p ∧ p ≤ x ∧ (prime p).
+#n #not_not #x #lenx elim lenx
+ [#len #Bn @False_ind @(absurd ?? not_not) @Bn
+ |#n1 #lenn1 #Hind #ltn1 #HB cases (true_or_false (primeb (S n1))) #Hc
+ [%{(S n1)} % [% [@le_S_S // |//] |@primeb_true_to_prime // ]
+ |cases (Hind ??)
+ [#p * * #ltnp #lep #primep %{p} %[%[@ltnp|@le_S//]|//]
+ |@lt_to_le //
+ |#p #ltp #lep cases (le_to_or_lt_eq ?? ltp) #Hcase
+ [@HB // |<Hcase @primeb_false_to_not_prime //]
+ ]
+ ]
+ ]
+qed.
+
+theorem not_not_bertrand_to_bertrand: ∀n.
+ ¬(not_bertrand n) → bertrand n.
+#n #not_not @(not_not_bertrand_to_bertrand1 ?? (2*n)) //
+#p #le2n #lep @False_ind @(absurd ? le2n) @le_to_not_lt //
+qed.
+
+definition k ≝ λn,p.
+ ∑_{i < log p n}((n/(exp p (S i))\mod 2)).
+
+lemma k_def : ∀n,p. k n p = ∑_{i < log p n}((n/(exp p (S i))\mod 2)).
+// qed.
+
+theorem le_k: ∀n,p. k n p ≤ log p n.
+#n #p >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 <times_pi
+@same_bigop
+ [//
+ |#p #ltp #primebp cases (true_or_false (leb (k n p) 1)) #Hc >Hc
+ [>(lt_to_leb_false 2 (k n p))
+ [<times_n_1 >commutative_times <times_n_1 //
+ |@le_S_S @leb_true_to_le //
+ ]
+ |>(le_to_leb_true 2 (k n p))
+ [>commutative_times <times_n_1 >commutative_times <times_n_1 //
+ |@not_le_to_lt @leb_false_to_not_le //
+ ]
+ ]
+ ]
+qed.
+
+lemma lt_div_to_times: ∀n,m,q. O < q → n/q < m → n < q*m.
+#n #m #q #posq #ltm
+cut (O < m) [@(ltn_to_ltO … ltm)] #posm
+@not_le_to_lt % #len @(absurd …ltm) @le_to_not_lt @le_times_to_le_div //
+qed.
+
+(* integrare in div_and_mod *)
+lemma lt_to_div_O:∀n,m. n < m → n / m = O.
+#n #m #ltnm @(div_mod_spec_to_eq n m (n/m) (n \mod m) O n)
+ [@div_mod_spec_div_mod @(ltn_to_ltO ?? ltnm)
+ |@div_mod_spec_intro //
+ ]
+qed.
+
+(* the value of n could be smaller *)
+lemma k1: ∀n,p. 18 ≤ n → p ≤ n → 2*n/ 3 < p → k (2*n) p = O.
+#n #p #le18 #lep #ltp >k_def
+elim (log p (2*n))
+ [//
+ |#i #Hind >bigop_Strue
+ [>Hind <plus_n_O cases i
+ [<exp_n_1
+ cut (2*n/p = 2) [2:#Hcut >Hcut //]
+ @lt_to_le_times_to_lt_S_to_div
+ [@(ltn_to_ltO ?? ltp)
+ |<commutative_times @monotonic_le_times_r //
+ |>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))
+ [<associative_times >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 ⊢(??%); <plus_n_O
+ @monotonic_le_plus_l @(transitive_le ? 18 … le18)
+ @leb_true_to_le //
+ |@lt_to_le @lt_div_S @lt_O_S
+ ]
+ ]
+ ]
+ |@(lt_to_le_to_lt ? (exp p 2))
+ [@lt_exp1 [@lt_O_S|//]
+ |@le_exp [@(ltn_to_ltO ?? ltp) |@le_S_S @le_S_S @le_O_n]
+ ]
+ ]
+ ]
+ |//
+ ]
+ ]
+qed.
+
+theorem le_B_split1_teta:∀n.18 ≤ n → not_bertrand n →
+ B_split1 (2*n) ≤ teta (2 * n / 3).
+#n #le18 #not_Bn >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) <times_n_O @le_n
+ |>(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)
+ [<exp_n_1 @le_n
+ |normalize @prime_to_lt_O @primeb_true_to_prime //
+ ]
+ ]
+ ]
+qed.
+
+theorem le_B_split2_exp: ∀n. exp 2 7 ≤ n →
+ B_split2 (2*n) ≤ exp (2*n) (pred(sqrt(2*n)/2)).
+#n #len >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 <exp_2
+ @not_lt_to_le % #H2n
+ @(absurd ?? (le_to_not_lt 2 (log p (2*n)) ?))
+ [@le_S_S @f_false_to_le_max
+ [%{0} %
+ [>(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_1 @le_k|@le_O_n]
+ ]
+ |@le_exp_log >(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
+ |<exp_plus_times @(transitive_le ? (exp 2 (2*n)))
+ [@(le_exp … (lt_O_S ?))
+ cut (2*(2*n/3)+2*n/3 = 3*(2*n/3)) [//] #Heq >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 ⊢ (??(??%)); <associative_times
+ <commutative_times in ⊢ (??%); @monotonic_le_times_r
+ @not_bertrand_to_le_B //
+ |@(le_times_to_le_div … (lt_O_S ?))
+ @(transitive_le ? (sqrt (exp 2 8)))
+ [@leb_true_to_le %
+ |@monotonic_sqrt >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 //
+ |<times_n_Sm >commutative_times <times_n_Sm >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 @(transitive_le ? (2*sqrt(2*n)*(sqrt (2*n)/2)))
+ [@le_times [@H1|@le_n]
+ |@(transitive_le ? ((2*sqrt(2*n)*(sqrt(2*n))/2)))
+ [@le_times_div_div_times @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 <times_n_Sm <plus_n_O >(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 <plus_n_Sm cut (n+n = 2*n) [//] #Hcut1 >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<n) [@(lt_to_le_to_lt … len) @lt_O_S] #posn
+>(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<n) [@(lt_to_le_to_lt … len) @le_S_S @le_S_S @lt_O_S] #lt2n
+ elim lt2n [//] #m #lt2m #Hind
+ cut (0<m) [@(transitive_le … lt2m) @leb_true_to_le //] #posm
+ @(transitive_le ? (log 2 (2*m) +2))
+ [@le_plus [2://] @le_log [//] normalize <plus_n_O
+ >(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<m) [@(transitive_le … lem) @leb_true_to_le //] #lt8m
+ cut (1<m) [@(transitive_le … lt8m) @leb_true_to_le //] #lt1m
+ cut (0<m) [@(transitive_le … lt1m) @leb_true_to_le //] #posm
+ cases (le_to_or_lt_eq … (le_exp_log 2 m posm)) #Hclog
+ [@(transitive_le … (le_exp_log 2 m posm))
+ lapply (Hind … Hclog ?) [@le_exp [@lt_O_S|@exp_to_log_r [@le_n|@lt8m|@lem]]]
+ -Hind #Hind @(transitive_le … Hind) >(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]
+ |<Hclog in ⊢ (??%); @(lt_exp … (le_n…)) whd >(plus_n_O (log 2 m -1))
+ >plus_n_Sm <plus_minus_m_m [@le_n | @lt_O_log @lt1m]
+ |-Hind #Hind lapply (le_times … Hind (le_n 2))
+ cut (∀a,b. a^(b+1) = a^b*a) [#a #b <plus_n_Sm <plus_n_O //] #exp_S
+ <exp_S <plus_minus_m_m [2:@lt_O_log //]
+ -Hind #Hind <Hclog @(transitive_le … Hind)
+ >(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)
+ <associative_times @le_times [2://] <associative_times
+ >(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]
+ ]
+ |<Hcasem >(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.
+*)
--- /dev/null
+(*
+ ||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} %
+ [%[<Hn @lt_O_S | @primeb_true_to_prime //]
+ |#p #primep #lt2 @False_ind @(absurd … lt2)
+ @le_to_not_lt @prime_to_lt_SO //
+ ]
+ ]
+qed.
+
+theorem list_of_primes_to_bertrand: \forall n,pn,l.0 < n \to prime pn \to n <pn \to
+list_of_primes pn l \to
+(\forall p. prime p \to p \le pn \to in_list nat p l) \to
+(\forall p. in_list nat p l \to 2 < p \to
+\exists pp. in_list nat pp l \land pp < p \land p \le 2*pp) \to bertrand n.
+intros.
+elim (min_prim n).
+apply (ex_intro ? ? a).
+elim H6.clear H6.elim H7.clear H7.
+split
+ [split
+ [assumption
+ |elim (le_to_or_lt_eq ? ? (prime_to_lt_SO ? H9))
+ [elim (H5 a)
+ [elim H10.clear H10.elim H11.clear H11.
+ apply (trans_le ? ? ? H12).
+ apply le_times_r.
+ apply H8
+ [unfold in H3.
+ elim (H3 a1 H10).
+ assumption
+ |assumption
+ ]
+ |apply H4
+ [assumption
+ |apply not_lt_to_le.intro.
+ apply (lt_to_not_le ? ? H2).
+ apply H8;assumption
+ ]
+ |assumption
+ ]
+ |rewrite < H7.
+ apply O_lt_const_to_le_times_const.
+ assumption
+ ]
+ ]
+ |assumption
+ ]
+qed.
+
+let rec check_list l \def
+ match l with
+ [ nil \Rightarrow true
+ | cons (hd:nat) tl \Rightarrow
+ match tl with
+ [ nil \Rightarrow eqb hd 2
+ | cons hd1 tl1 \Rightarrow
+ (leb (S hd1) hd \land leb hd (2*hd1) \land check_list tl)
+ ]
+ ]
+.
+
+lemma check_list1: \forall n,m,l.(check_list (n::m::l)) = true \to
+m < n \land n \le 2*m \land (check_list (m::l)) = true \land ((check_list l) = true).
+intros 3.
+change in ⊢ (? ? % ?→?) with (leb (S m) n \land leb n (2*m) \land check_list (m::l)).
+intro.
+lapply (andb_true_true ? ? H) as H1.
+lapply (andb_true_true_r ? ? H) as H2.clear H.
+lapply (andb_true_true ? ? H1) as H3.
+lapply (andb_true_true_r ? ? H1) as H4.clear H1.
+split
+ [split
+ [split
+ [apply leb_true_to_le.assumption
+ |apply leb_true_to_le.assumption
+ ]
+ |assumption
+ ]
+ |generalize in match H2.
+ cases l
+ [intro.reflexivity
+ |change in ⊢ (? ? % ?→?) with (leb (S n1) m \land leb m (2*n1) \land check_list (n1::l1)).
+ intro.
+ lapply (andb_true_true_r ? ? H) as H2.
+ assumption
+ ]
+ ]
+qed.
+
+theorem check_list2: \forall l. check_list l = true \to
+\forall p. in_list nat p l \to 2 < p \to
+\exists pp. in_list nat pp l \land pp < p \land p \le 2*pp.
+intro.elim l 2
+ [intros.apply False_ind.apply (not_in_list_nil ? ? H1)
+ |cases l1;intros
+ [lapply (in_list_singleton_to_eq ? ? ? H2) as H4.
+ apply False_ind.
+ apply (lt_to_not_eq ? ? H3).
+ apply sym_eq.apply eqb_true_to_eq.
+ rewrite > 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.
+*)
projects / helm.git / commitdiff