From: Andrea Asperti Date: Mon, 17 Dec 2012 09:00:18 +0000 (+0000) Subject: Still porting chebyshev X-Git-Tag: make_still_working~1393 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=29c979302cf398410bf6f10c11b146ebe42bd54a;p=helm.git Still porting chebyshev --- diff --git a/matita/matita/lib/arithmetics/big_pi.ma b/matita/matita/lib/arithmetics/big_pi.ma index 94068a088..0c818e6de 100644 --- a/matita/matita/lib/arithmetics/big_pi.ma +++ b/matita/matita/lib/arithmetics/big_pi.ma @@ -48,6 +48,20 @@ theorem times_pi: ∀n,p,f,g. ] qed. +theorem pi_1: ∀n,p. + ∏_{i < n | p i} 1 = 1. +#n #p elim n // #n1 #Hind cases (true_or_false (p n1)) #Hc + [>bigop_Strue >Hind // |>bigop_Sfalse // ] +qed. + +theorem exp_pi: ∀n,m,p,f. + ∏_{i < n | p i}(exp (f i) m) = exp (∏_{i < n | p i}(f i)) m. +#n #m #p #f elim m + [@pi_1 + |#m1 #Hind >times_pi >Hind % + ] +qed. + (* theorem true_to_pi_p_Sn: ∀n,p,g. p n = true \to pi_p (S n) p g = (g n)*(pi_p n p g). @@ -304,28 +318,6 @@ elim n ] qed. -theorem pi_p_SO: \forall n,p. -pi_p n p (\lambda i.S O) = S O. -intros.elim n - [reflexivity - |simplify.elim (p n1) - [simplify.rewrite < plus_n_O.assumption - |simplify.assumption - ] - ] -qed. - -theorem exp_pi_p: \forall n,m,p,f. -pi_p n p (\lambda x.exp (f x) m) = exp (pi_p n p f) m. -intros. -elim m - [simplify.apply pi_p_SO - |simplify. - rewrite > times_pi_p. - rewrite < H. - reflexivity - ] -qed. theorem exp_times_pi_p: \forall n,m,k,p,f. pi_p n p (\lambda x.exp k (m*(f x))) = diff --git a/matita/matita/lib/arithmetics/bigops.ma b/matita/matita/lib/arithmetics/bigops.ma index 247af0b92..88b7fdb7a 100644 --- a/matita/matita/lib/arithmetics/bigops.ma +++ b/matita/matita/lib/arithmetics/bigops.ma @@ -20,12 +20,12 @@ definition sameF_p: nat → (nat → bool) →∀A.relation(nat→A) ≝ lemma sameF_upto_le: ∀A,f,g,n,m. n ≤m → sameF_upto m A f g → sameF_upto n A f g. -#A #f #g #n #m #lenm #samef #i #ltin @samef /2/ +#A #f #g #n #m #lenm #samef #i #ltin @samef /2 by lt_to_le_to_lt/ qed. lemma sameF_p_le: ∀A,p,f,g,n,m. n ≤m → sameF_p m p A f g → sameF_p n p A f g. -#A #p #f #g #n #m #lenm #samef #i #ltin #pi @samef /2/ +#A #p #f #g #n #m #lenm #samef #i #ltin #pi @samef /2 by lt_to_le_to_lt/ qed. (* @@ -104,6 +104,25 @@ theorem pad_bigop: ∀k,n,p,B,nil,op.∀f:nat→B. n ≤ k → [@same_bigop #i #lti // >(not_le_to_leb_false …) /2/ |#j #leup #Hind >bigop_Sfalse >(le_to_leb_true … leup) // ] qed. + +theorem pad_bigop1: ∀k,n,p,B,nil,op.∀f:nat→B. n ≤ k → + (∀i. n ≤ i → i < k → p i = false) → + \big[op,nil]_{i < n | p i}(f i) + = \big[op,nil]_{i < k | p i}(f i). +#k #n #p #B #nil #op #f #lenk (elim lenk) + [#_ @same_bigop #i #lti // + |#j #leup #Hind #Hfalse >bigop_Sfalse + [@Hind #i #leni #ltij @Hfalse // @le_S // + |@Hfalse // + ] + ] +qed. + +theorem bigop_false: ∀n,B,nil,op.∀f:nat→B. + \big[op,nil]_{i < n | false }(f i) = nil. +#n #B #nil #op #f elim n // #n1 #Hind +>bigop_Sfalse // +qed. record Aop (A:Type[0]) (nil:A) : Type[0] ≝ {op :2> A → A → A; @@ -111,6 +130,24 @@ record Aop (A:Type[0]) (nil:A) : Type[0] ≝ nilr:∀a. op a nil = a; assoc: ∀a,b,c.op a (op b c) = op (op a b) c }. + +theorem pad_bigop_nil: ∀k,n,p,B,nil.∀op:Aop B nil.∀f:nat→B. n ≤ k → + (∀i. n ≤ i → i < k → p i = false ∨ f i = nil) → + \big[op,nil]_{i < n | p i}(f i) + = \big[op,nil]_{i < k | p i}(f i). +#k #n #p #B #nil #op #f #lenk (elim lenk) + [#_ @same_bigop #i #lti // + |#j #leup #Hind #Hfalse cases (true_or_false (p j)) #Hpj + [>bigop_Strue // + cut (f j = nil) + [cases (Hfalse j leup (le_n … )) // >Hpj #H destruct (H)] #Hfj + >Hfj >nill @Hind #i #leni #ltij + cases (Hfalse i leni (le_S … ltij)) /2/ + |>bigop_Sfalse // @Hind #i #leni #ltij + cases (Hfalse i leni (le_S … ltij)) /2/ + ] + ] +qed. theorem bigop_sum: ∀k1,k2,p1,p2,B.∀nil.∀op:Aop B nil.∀f,g:nat→B. op (\big[op,nil]_{ibigop_Strue // >Hind >bigop_sum @same_bigop - #i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2/ + #i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2 by plus_minus/ #eqi [|#H] >eqi in ⊢ (???%); - >div_plus_times /2/ >Hp1 >(mod_plus_times …) /2/ + >div_plus_times /2 by monotonic_lt_minus_l/ + >Hp1 >(mod_plus_times …) /2 by refl, monotonic_lt_minus_l, eq_f/ |>bigop_Sfalse // >Hind >(pad_bigop (S n*k2)) // @same_bigop #i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2/ #eqi >eqi in ⊢ (???%); >div_plus_times /2/ @@ -248,7 +286,7 @@ qed. lemma sub_lt: ∀A,e,p,n,m. n ≤ m → sub_hk (λx.x) (λx.x) A (mk_range A e n p) (mk_range A e m p). -#A #e #f #n #m #lenm #i #lti #fi % // % /2/ +#A #e #f #n #m #lenm #i #lti #fi % // % /2 by lt_to_le_to_lt/ qed. theorem transitive_sub: ∀h1,k1,h2,k2,A,I,J,K. @@ -293,6 +331,54 @@ theorem bigop_iso: ∀n1,n2,p1,p2,B.∀nil.∀op:ACop B nil.∀f1,f2. ] qed. +(* lemma div_mod_exchange: ∀i,n,m. i < n*m → i\n = i mod m. *) + +(* commutation *) +theorem bigop_commute: ∀n,m,p11,p12,p21,p22,B.∀nil.∀op:ACop B nil.∀f. +0 < n → 0 < m → +(∀i,j. i < n → j < m → (p11 i ∧ p12 i j) = (p21 j ∧ p22 i j)) → +\big[op,nil]_{ibigop_prod >bigop_prod @bigop_iso +%{(λi.(i\mod m)*n + i/m)} %{(λi.(i\mod n)*m + i/n)} % + [% + [#i #lti #Heq (* whd in ⊢ (???(?(?%?)?)); *) @eq_f2 + [@sym_eq @mod_plus_times /2 by lt_times_to_lt_div/ + |@sym_eq @div_plus_times /2 by lt_times_to_lt_div/ + ] + |#i #lti #Hi + cut ((i\mod m*n+i/m)\mod n=i/m) + [@mod_plus_times @lt_times_to_lt_div //] #H1 + cut ((i\mod m*n+i/m)/n=i \mod m) + [@div_plus_times @lt_times_to_lt_div //] #H2 + %[%[@(lt_to_le_to_lt ? (i\mod m*n+n)) + [whd >plus_n_Sm @monotonic_le_plus_r @lt_times_to_lt_div // + |>commutative_plus @(le_times (S(i \mod m)) m n n) // @lt_mod_m_m // + ] + |lapply (Heq (i/m) (i \mod m) ??) + [@lt_mod_m_m // |@lt_times_to_lt_div //|>Hi >H1 >H2 //] + ] + |>H1 >H2 // + ] + ] + |#i #lti #Hi + cut ((i\mod n*m+i/n)\mod m=i/n) + [@mod_plus_times @lt_times_to_lt_div //] #H1 + cut ((i\mod n*m+i/n)/m=i \mod n) + [@div_plus_times @lt_times_to_lt_div //] #H2 + %[%[@(lt_to_le_to_lt ? (i\mod n*m+m)) + [whd >plus_n_Sm @monotonic_le_plus_r @lt_times_to_lt_div // + |>commutative_plus @(le_times (S(i \mod n)) n m m) // @lt_mod_m_m // + ] + |lapply (Heq (i \mod n) (i/n) ??) + [@lt_times_to_lt_div // |@lt_mod_m_m // |>Hi >H1 >H2 //] + ] + |>H1 >H2 // + ] + ] +qed. + (* distributivity *) record Dop (A:Type[0]) (nil:A): Type[0] ≝ @@ -313,7 +399,7 @@ theorem bigop_distr: ∀n,p,B,nil.∀R:Dop B nil.∀f,a. |>bigop_Sfalse // >bigop_Sfalse // ] qed. - + (* Sigma e Pi *) notation "∑_{ ident i < n | p } f" diff --git a/matita/matita/lib/arithmetics/chebyshev/chebyshev.ma b/matita/matita/lib/arithmetics/chebyshev/chebyshev.ma new file mode 100644 index 000000000..c6be766b1 --- /dev/null +++ b/matita/matita/lib/arithmetics/chebyshev/chebyshev.ma @@ -0,0 +1,1466 @@ +(* + ||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/log.ma". +include "arithmetics/big_pi.ma". +include "arithmetics/ord.ma". + +(* include "nat/factorization.ma". +include "nat/factorial2.ma". +include "nat/o.ma". *) + +(* (prim n) counts the number of prime numbers up to n included *) +definition prim ≝ λn. ∑_{i < S n | primeb i} 1. + +lemma le_prim_n: ∀n. prim n ≤ n. +#n elim n // -n #n #H +whd in ⊢ (?%?); cases (primeb (S n)) whd in ⊢ (?%?); + [@le_S_S @H |@le_S @H] +qed. + +lemma not_prime_times_2: ∀n. 1 < n → ¬prime (2*n). +#n #ltn % * #H #H1 @(absurd (2 = 2*n)) + [@H1 // %{n} // + |@lt_to_not_eq >(times_n_1 2) in ⊢ (?%?); @monotonic_lt_times_r // + ] +qed. + +theorem eq_prim_prim_pred: ∀n. 1 < n → + prim (2*n) = prim (pred (2*n)). +#n #ltn +lapply (S_pred (2*n) ?) [>(times_n_1 0) in ⊢ (?%?); @lt_times //] #H2n +lapply (not_prime_times_2 n ltn) #notp2n +whd in ⊢ (??%?); >(not_prime_to_primeb_false … notp2n) whd in ⊢ (??%?); +Heq + Heq + Hn normalize // + ] +qed. + +(* axiom daemon : ∀P:Prop.P. *) + +(* la prova potrebbe essere migliorata *) +theorem le_prim_n3: ∀n. 15 ≤ n → + prim n ≤ pred (n/2). +#n #len cases (even_or_odd (pred n)) #a * #Hpredn + [cut (n = S (2*a)) [Hn @(transitive_le ? (pred a)) + [@le_prim_n2 @(le_times_to_le 2) [//|@le_S_S_to_le Hn @(transitive_le ? (pred a)) + [>eq_prim_prim_pred + [2:@(lt_times_n_to_lt_r 2) Hpredn @le_prim_n2 @le_S_S_to_le @(lt_times_n_to_lt_r 2) (plus_n_O (log i n)) in ⊢ (?%?); >plus_n_Sm + @monotonic_le_plus_r @lt_O_log // + @le_S_S_to_le // + ] + ] + |bigop_Strue in ⊢ (???%); // + cases (true_or_false (dividesb n1 m)) #Hdivides + [>bigop_Strue [@eq_f @Hind| @true_to_andb_true //] + |>bigop_Sfalse + [>not_divides_to_ord_O + [whd in ⊢ (???(?%?)); // + |@dividesb_false_to_not_divides // + |@primeb_true_to_prime // + ] + |>Hprime >Hdivides % + ] + ] +|>bigop_Sfalse [>bigop_Sfalse // |>Hprime %] +] +qed. + +(* integrations to minimization *) +theorem false_to_lt_max: ∀f,n,m.O < n → + f n = false → max m f ≤ n → max m f < n. +#f #n #m #posn #Hfn #Hmax cases (le_to_or_lt_eq ?? Hmax) -Hmax #Hmax + [// + |cases (exists_max_forall_false f m) + [* #_ #Hfmax @False_ind @(absurd ?? not_eq_true_false) // + |* // + ] + ] +qed. + +(* boh ... +theorem lt_max_to_false : ∀f,n,m. + max n f < m → m ≤ n → f m = false. +#f #n elim n + [#m #H1 #H2 @False_ind @(absurd ? H2) @lt_to_not_le // + |#n1 #Hind #m whd in ⊢ (?%?→?); #Hmax #ltm +elim (max_S_max f n1); in H1 ⊢ %. +elim H1. +absurd (m \le S n1).assumption. +apply lt_to_not_le.rewrite < H5.assumption. +elim H1. +apply (le_n_Sm_elim m n1 H2). +intro. +apply H.rewrite < H5.assumption. +apply le_S_S_to_le.assumption. +intro.rewrite > H6.assumption. +qed. *) + +(* integrations to minimization *) +lemma lt_1_max_prime: ∀n. 1 < n → + 1 < max (S n) (λi:nat.primeb i∧dividesb i n). +#n #lt1n +@(lt_to_le_to_lt ? (smallest_factor n)) + [@lt_SO_smallest_factor // + |@true_to_le_max + [@le_S_S @le_smallest_factor_n + |@true_to_andb_true + [@prime_to_primeb_true @prime_smallest_factor_n // + |@divides_to_dividesb_true + [@lt_O_smallest_factor @lt_to_le // + |@divides_smallest_factor_n @lt_to_le // + ] + ] + ] + ] +qed. + +theorem lt_max_to_pi_p_primeb: ∀q,m. Obigop_Strue + [>(exp_ord n m … posm) in ⊢ (??%?); + [@eq_f >(Hind (ord_rem m n)) + [@same_bigop + [#x #ltxn cases (true_or_false (primeb x)) #Hx >Hx + [cases (true_or_false (dividesb x (ord_rem m n))) #Hx1 >Hx1 + [@sym_eq @divides_to_dividesb_true + [@prime_to_lt_O @primeb_true_to_prime // + |@(transitive_divides ? (ord_rem m n)) + [@dividesb_true_to_divides // + |@(divides_ord_rem … posm) @(transitive_lt … ltxn) + @prime_to_lt_SO @primeb_true_to_prime // + ] + ] + |@sym_eq @not_divides_to_dividesb_false + [@prime_to_lt_O @primeb_true_to_prime // + |@(ord_O_to_not_divides … posm) + [@primeb_true_to_prime // + |<(ord_ord_rem n … posm … ltxn) + [@not_divides_to_ord_O + [@primeb_true_to_prime // + |@dividesb_false_to_not_divides // + ] + |@primeb_true_to_prime // + |@primeb_true_to_prime @(andb_true_l ?? Hcase) + ] + ] + ] + ] + |// + ] + |#x #ltxn #Hx @eq_f @ord_ord_rem // + [@primeb_true_to_prime @(andb_true_l ? ? Hcase) + |@primeb_true_to_prime @(andb_true_l ? ? Hx) + ] + ] + |@not_eq_to_le_to_lt + [elim (exists_max_forall_false (λi:nat.primeb i∧dividesb i (ord_rem m n)) (S(ord_rem m n))) + [* #Hex #Hord_rem cases Hex #x * #H6 #H7 % #H + >H in Hord_rem; #Hn @(absurd ?? (not_divides_ord_rem m n posm ?)) + [@dividesb_true_to_divides @(andb_true_r ?? Hn) + |@prime_to_lt_SO @primeb_true_to_prime @(andb_true_l ?? Hn) + ] + |* #Hall #Hmax >Hmax @lt_to_not_eq @prime_to_lt_O + @primeb_true_to_prime @(andb_true_l ?? Hcase) + ] + |@(transitive_le ? (max (S m) (λi:nat.primeb i∧dividesb i (ord_rem m n)))) + [@le_to_le_max @le_S_S @(divides_to_le … posm) @(divides_ord_rem … posm) + @prime_to_lt_SO @primeb_true_to_prime @(andb_true_l ?? Hcase) + |@(transitive_le ? (max (S m) (λi:nat.primeb i∧dividesb i m))) + [@le_max_f_max_g #i #ltim #Hi + cases (true_or_false (primeb i)) #Hprimei >Hprimei + [@divides_to_dividesb_true + [@prime_to_lt_O @primeb_true_to_prime // + |@(transitive_divides ? (ord_rem m n)) + [@dividesb_true_to_divides @(andb_true_r ?? Hi) + |@(divides_ord_rem … posm) + @prime_to_lt_SO @primeb_true_to_prime + @(andb_true_l ?? Hcase) + ] + ] + |>Hprimei in Hi; #Hi @Hi + ] + |@le_S_S_to_le // + ] + ] + ] + |@(lt_O_ord_rem … posm) @prime_to_lt_SO + @primeb_true_to_prime @(andb_true_l ?? Hcase) + ] + |@prime_to_lt_SO @primeb_true_to_prime @(andb_true_l ?? Hcase) + ] + |// + ] + |cases (le_to_or_lt_eq ?? posm) #Hm + [>bigop_Sfalse + [@(Hind … posm) @false_to_lt_max + [@(lt_to_le_to_lt ? (max (S m) (λi:nat.primeb i∧dividesb i m))) + [@lt_to_le @lt_1_max_prime // + |@le_S_S_to_le // + ] + |// + |@le_S_S_to_le // + ] + |@Hcase + ] + |primei // + @sym_eq @not_divides_to_dividesb_false + [@prime_to_lt_O @primeb_true_to_prime // + |% #divi @(absurd ?? (le_to_not_lt i 1 ?)) + [@prime_to_lt_SO @(primeb_true_to_prime ? primei) + |@divides_to_le // + ] + ] + |// + ] + ] + ] + ] +qed. + +(* factorization of n into primes *) +theorem pi_p_primeb_dividesb: ∀n. O < n → + n = ∏_{ p < S n | primeb p ∧ dividesb p n} (exp p (ord n p)). +#n #posn @lt_max_to_pi_p_primeb // @lt_max_n @le_S @posn +qed. + +theorem pi_p_primeb: ∀n. O < n → + n = ∏_{ p < (S n) | primeb p}(exp p (ord n p)). +#n #posn (exp_ord p ? lt1p posn) in ⊢ (??(??%)); +>log_exp // @lt_O_ord_rem // +qed. + +theorem sigma_p_dividesb: +∀m,n,p. O < n → prime p → p ∤ n → +m = ∑_{ i < m | dividesb (p\sup (S i)) ((exp p m)*n)} 1. +#m elim m // -m #m #Hind #n #p #posn #primep #ndivp +>bigop_Strue + [>commutative_plus (Hind n p posn primep ndivp) in ⊢ (? ? % ?); + @same_bigop + [#i #ltim cases (true_or_false (dividesb (p\sup(S i)) (p\sup m*n))) #Hc >Hc + [@sym_eq @divides_to_dividesb_true + [@lt_O_exp @prime_to_lt_O // + |%{((exp p (m - i))*n)} commutative_plus + @plus_minus_m_m @lt_to_le // + ] + |(* @sym_eq *) + @False_ind @(absurd ?? (dividesb_false_to_not_divides ? ? Hc)) + %{((exp p (m - S i))*n)} commutative_plus @plus_minus_m_m // + assumption + |% + ] + ] + |// + ] + |@divides_to_dividesb_true + [@lt_O_exp @prime_to_lt_O // | %{n} //] + ] +qed. + +theorem sigma_p_dividesb1: +∀m,n,p,k. O < n → prime p → p ∤ n → m ≤ k → + m = ∑_{i < k | dividesb (p\sup (S i)) ((exp p m)*n)} 1. +#m #n #p #k #posn #primep #ndivp #lemk +lapply (prime_to_lt_SO ? primep) #lt1p +lapply (prime_to_lt_O ? primep) #posp +>(sigma_p_dividesb m n p posn primep ndivp) in ⊢ (??%?); +>(pad_bigop k m) // @same_bigop + [#i #ltik cases (true_or_false (leb m i)) #Him > Him + [whd in ⊢(??%?); @sym_eq + @not_divides_to_dividesb_false + [@lt_O_exp // + |lapply (leb_true_to_le … Him) -Him #Him + % #Hdiv @(absurd ?? (le_to_not_lt ?? Him)) + (* <(ord_exp p m lt1p) *) >(plus_n_O m) + <(not_divides_to_ord_O ?? primep ndivp) + <(ord_exp p m lt1p) + (times_n_O O) @lt_times // @lt_O_exp // + ] + |@lt_O_exp // + ] + ] + |% + ] + |// + ] +qed. + +theorem eq_ord_sigma_p: +∀n,m,x. O < n → prime x → +exp x m ≤ n → n < exp x (S m) → +ord n x= ∑_{i < m | dividesb (x\sup (S i)) n} 1. +#n #m #x #posn #primex #Hexp #ltn +lapply (prime_to_lt_SO ? primex) #lt1x +>(exp_ord x n) in ⊢ (???%); // @sigma_p_dividesb1 + [@lt_O_ord_rem // + |// + |@not_divides_ord_rem // + |@le_S_S_to_le @(le_to_lt_to_lt ? (log x n)) + [@le_ord_log // + |@(lt_exp_to_lt x) + [@lt_to_le // + |@(le_to_lt_to_lt ? n ? ? ltn) @le_exp_log // + ] + ] + ] +qed. + +theorem pi_p_primeb1: ∀n. O < n → +n = ∏_{p < S n| primeb p} + (∏_{i < log p n| dividesb (exp p (S i)) n} p). +#n #posn >(pi_p_primeb n posn) in ⊢ (??%?); +@same_bigop + [// + |#p #ltp #primep >exp_sigma @eq_f @eq_ord_sigma_p + [// + |@primeb_true_to_prime // + |@le_exp_log // + |@lt_exp_log @prime_to_lt_SO @primeb_true_to_prime // + ] + ] +qed. + +(* the factorial function *) +theorem eq_fact_pi_p:∀n. + fact n = ∏_{i < S n | leb 1 i} i. +#n elim n // #n1 #Hind whd in ⊢ (??%?); >commutative_times >bigop_Strue + [@eq_f // | % ] +qed. + +theorem eq_sigma_p_div: ∀n,q.O < q → + ∑_{ m < S n | leb (S O) m ∧ dividesb q m} 1 =n/q. +#n #q #posq +@(div_mod_spec_to_eq n q ? (n \mod q) ? (n \mod q)) + [@div_mod_spec_intro + [@lt_mod_m_m // + |elim n + [normalize cases q // + |#n1 #Hind cases (or_div_mod1 n1 q posq) + [* #divq #eqn1 >divides_to_mod_O // + bigop_Strue + [>eqn1 in ⊢ (??%?); @eq_f2 + [bigop_Sfalse + [>(mod_S … posq) + [< plus_n_Sm @eq_f // + |cases (le_to_or_lt_eq (S (mod n1 q)) q ?) + [// + |#eqq @False_ind cases ndiv #Hdiv @Hdiv + %{(S(div n1 q))} not_divides_to_dividesb_false // + ] + ] + ] + ] + |@div_mod_spec_div_mod // + ] +qed. + +definition Atimes ≝ mk_Aop nat 1 times ???. + [#a normalize eq_fact_pi_p +@(trans_eq ?? + (∏_{m < S n | leb 1 m} + (∏_{p < S m | primeb p} + (∏_{i < log p m | dividesb (exp p (S i)) m} p)))) + [@same_bigop [// |#x #Hx1 #Hx2 @pi_p_primeb1 @leb_true_to_le //] + |@(trans_eq ?? + (∏_{m < S n | leb 1 m} + (∏_{p < S m | primeb p ∧ leb p m} + (∏_{ i < log p m | dividesb ((p)\sup(S i)) m} p)))) + [@same_bigop + [// + |#x #Hx1 #Hx2 @same_bigop + [#p #ltp >(le_to_leb_true … (le_S_S_to_le …ltp)) + cases (primeb p) // + |// + ] + ] + |@(trans_eq ?? + (∏_{m < S n | leb 1 m} + (∏_{p < S n | primeb p ∧ leb p m} + (∏_{i < log p m |dividesb ((p)\sup(S i)) m} p)))) + [@same_bigop + [// + |#p #Hp1 #Hp2 @pad_bigop1 + [@Hp1 + |#i #lti #upi >lt_to_leb_false + [cases (primeb i) //|@lti] + ] + ] + |(* make a general theorem *) + @(trans_eq ?? + (∏_{p < S n | primeb p} + (∏_{m < S n | leb p m} + (∏_{i < log p m | dividesb (p^(S i)) m} p)))) + [@(bigop_commute … ACtimes … (lt_O_S n) (lt_O_S n)) + #i #j #lti #ltj + cases (true_or_false (primeb j ∧ leb j i)) #Hc >Hc + [>(le_to_leb_true 1 i) + [// + |@(transitive_le ? j) + [@prime_to_lt_O @primeb_true_to_prime @(andb_true_l ? ? Hc) + |@leb_true_to_le @(andb_true_r ?? Hc) + ] + ] + |cases(leb 1 i) // + ] + |@same_bigop + [// + |#p #Hp1 #Hp2 + @(trans_eq ?? + (∏_{m < S n | leb p m} + (∏_{i < log p n | dividesb (p\sup(S i)) m} p))) + [@same_bigop + [// + |#x #Hx1 #Hx2 @sym_eq + @sym_eq @pad_bigop1 + [@le_log + [@prime_to_lt_SO @primeb_true_to_prime // + |@le_S_S_to_le // + ] + |#i #Hi1 #Hi2 @not_divides_to_dividesb_false + [@lt_O_exp @prime_to_lt_O @primeb_true_to_prime // + |@(not_to_not … (lt_to_not_le x (exp p (S i)) ?)) + [#H @divides_to_le // @(lt_to_le_to_lt ? p) + [@prime_to_lt_O @primeb_true_to_prime // + |@leb_true_to_le // + ] + |@(lt_to_le_to_lt ? (exp p (S(log p x)))) + [@lt_exp_log @prime_to_lt_SO @primeb_true_to_prime // + |@le_exp + [@ prime_to_lt_O @primeb_true_to_prime // + |@le_S_S // + ] + ] + ] + ] + ] + ] + |@ + (trans_eq ? ? + (∏_{i < log p n} + (∏_{m < S n | leb p m ∧ dividesb (p\sup(S i)) m} p))) + [@(bigop_commute ?????? nat 1 ACtimes (λm,i.p) ???) // + cut (p ≤ n) [@le_S_S_to_le //] #lepn + @(lt_O_log … lepn) @(lt_to_le_to_lt … lepn) @prime_to_lt_SO + @primeb_true_to_prime // + |@same_bigop + [// + |#m #ltm #_ >exp_sigma @eq_f + @(trans_eq ?? + (∑_{i < S n |leb 1 i∧dividesb (p\sup(S m)) i} 1)) + [@same_bigop + [#i #lti + cases (true_or_false (dividesb (p\sup(S m)) i)) #Hc >Hc + [cases (true_or_false (leb p i)) #Hp3 >Hp3 + [>le_to_leb_true + [// + |@(transitive_le ? p) + [@prime_to_lt_O @primeb_true_to_prime // + |@leb_true_to_le // + ] + ] + |>lt_to_leb_false + [// + |@not_le_to_lt + @(not_to_not ??? (leb_false_to_not_le ?? Hp3)) #posi + @(transitive_le ? (exp p (S m))) + [>(exp_n_1 p) in ⊢ (?%?); + @le_exp + [@prime_to_lt_O @primeb_true_to_prime // + |@le_S_S @le_O_n + ] + |@(divides_to_le … posi) + @dividesb_true_to_divides // + ] + ] + ] + |cases (leb p i) cases (leb 1 i) // + ] + |// + ] + |@eq_sigma_p_div @lt_O_exp + @prime_to_lt_O @primeb_true_to_prime // + ] + ] + ] + ] + ] + ] + ] + ] + ] +qed. + +theorem fact_pi_p2: ∀n. fact (2*n) = +∏_{p < S (2*n) | primeb p} + (∏_{i < log p (2*n)} + (exp p (2*(n /(exp p (S i))))*(exp p (mod (2*n /(exp p (S i))) 2)))). +#n >fact_pi_p @same_bigop + [// + |#p #ltp #primep @same_bigop + [// + |#i #lti #_ commutative_times in ⊢ (???(?%?)); + cut (0 < p ^ (S i)) + [@lt_O_exp @prime_to_lt_O @primeb_true_to_prime //] + generalize in match (p ^(S i)); #a #posa + >(div_times_times n a 2) // >(commutative_times n 2) + fact_pi_p2 @same_bigop + [// + |#p #ltp #primep @times_pi + ] +qed. + +theorem pi_p_primeb4: ∀n. 1 < n → +∏_{p < S (2*n) | primeb p} + (∏_{i < log p (2*n)}(exp p (2*(n /(exp p (S i)))))) += +∏_{p < S n | primeb p} + (∏_{i < log p (2*n)}(exp p (2*(n /(exp p (S i)))))). +#n #lt1n +@sym_eq @(pad_bigop_nil … ACtimes) + [@le_S_S /2 by / + |#i #ltn #lti %2 + >log_i_2n // + [>bigop_Strue // whd in ⊢ (??(??%)?); eq_div_O // + |@le_S_S_to_le // + ] + ] +qed. + +theorem pi_p_primeb5: ∀n. 1 < n → +∏_{p < S (2*n) | primeb p} + (∏_{i < log p (2*n)} (exp p (2*(n /(exp p (S i)))))) += +∏_{p < S n | primeb p} + (∏_{i < log p n} (exp p (2*(n /(exp p (S i)))))). +#n #lt1n >(pi_p_primeb4 ? lt1n) @same_bigop + [// + |#p #lepn #primebp @sym_eq @(pad_bigop_nil … ACtimes) + [@le_log + [@prime_to_lt_SO @primeb_true_to_prime // + |// + ] + |#i #lelog #lti %2 >eq_div_O // + @(lt_to_le_to_lt ? (exp p (S(log p n)))) + [@lt_exp_log @prime_to_lt_SO @primeb_true_to_prime // + |@le_exp + [@prime_to_lt_O @primeb_true_to_prime // |@le_S_S //] + ] + ] + ] +qed. + +theorem exp_fact_2: ∀n. +exp (fact n) 2 = + ∏_{p < S n| primeb p} + (∏_{i < log p n} (exp p (2*(n /(exp p (S i)))))). +#n >fact_pi_p commutative_times @exp_exp_times + ] + |@exp_pi + ] +qed. + +definition B ≝ λn. +∏_{p < S n | primeb p} + (∏_{i < log p n} (exp p (mod (n /(exp p (S i))) 2))). + +lemma Bdef : ∀n.B n = + ∏_{p < S n | primeb p} + (∏_{i < log p n} (exp p (mod (n /(exp p (S i))) 2))). +// qed-. + +example B_SSSO: B 3 = 6. // +qed. + +example B_SSSSO: B 4 = 6. // +qed. + +example B_SSSSSO: B 5 = 30. // +qed. + +example B_SSSSSSO: B 6 = 20. // +qed. + +example B_SSSSSSSO: B 7 = 140. // +qed. + +example B_SSSSSSSSO: B 8 = 70. // +qed. + +theorem eq_fact_B:∀n. 1 < n → + (2*n)! = exp (n!) 2 * B(2*n). +#n #lt1n >fact_pi_p3 @eq_f2 + [@sym_eq >pi_p_primeb5 [@exp_fact_2|//] |// ] +qed. + +theorem le_B_A: ∀n. B n ≤ A n. +#n >eq_A_A' @le_pi #p #ltp #primep +@le_pi #i #lti #_ >(exp_n_1 p) in ⊢ (??%); @le_exp + [@prime_to_lt_O @primeb_true_to_prime // + |@le_S_S_to_le @lt_mod_m_m @lt_O_S + ] +qed. + +theorem le_B_A4: ∀n. O < n → 2 * B (4*n) ≤ A (4*n). +#n #posn >eq_A_A' +cut (2 < (S (4*n))) + [@le_S_S >(times_n_1 2) in ⊢ (?%?); @le_times //] #H2 +cut (OBdef >(bigop_diff ??? ACtimes ? 2 ? H2) [2:%] +>Adef >(bigop_diff ??? ACtimes ? 2 ? H2) in ⊢ (??%); [2:%] +(bigop_diff ??? ACtimes ? 0 ? Hlog) [2://] + >(bigop_diff ??? ACtimes ? 0 ? Hlog) in ⊢ (??%); [2:%] + ACtimesdef @le_times + [H4 >associative_times + >commutative_times in ⊢ (?(??(??(?(?%?)?)))?); + >div_times [2://] >divides_to_mod_O + [@le_n |%{n} // |@lt_O_S] + |@le_pi #i #lti #H >(exp_n_1 2) in ⊢ (??%); + @le_exp [@lt_O_S |@le_S_S_to_le @lt_mod_m_m @lt_O_S] + ] + |@le_pi #p #ltp #Hp @le_pi #i #lti #H + >(exp_n_1 p) in ⊢ (??%); @le_exp + [@prime_to_lt_O @primeb_true_to_prime @(andb_true_r ?? Hp) + |@le_S_S_to_le @lt_mod_m_m @lt_O_S + ] + ] +qed. + +(* not usefull +theorem le_fact_A:\forall n.S O < n \to +fact (2*n) \le exp (fact n) 2 * A (2*n). +intros. +rewrite > eq_fact_B + [apply le_times_r. + apply le_B_A + |assumption + ] +qed. *) + +theorem lt_SO_to_le_B_exp: ∀n. 1 < n → + B (2*n) ≤ exp 2 (pred (2*n)). +#n #lt1n @(le_times_to_le (exp (fact n) 2)) + [@lt_O_exp // + |<(eq_fact_B … lt1n) exp_2 exp_2 commutative_times in ⊢ (??(?%?)); + >associative_times in ⊢ (??%); <(eq_fact_B … lt1n) + eq_A_A' > eq_A_A' +cut ( + ∏_{p < S n | primeb p} (∏_{i Adef in ⊢ (???%); >Hcut + Adef @same_bigop + [// + |#p #lt1p #primep Hc + [normalize plus_n_O // + |normalize lt_to_leb_false + [normalize @plus_n_O + |@le_S_S @(transitive_le ? (exp p (log p n))) + [@le_exp [@prime_to_lt_O @primeb_true_to_prime //|//] + |@le_exp_log // + ] + ] + ] + ] + |@(trans_eq ?? + (∏_{p < S (2*n) | primeb p} + (∏_{i lt_to_log_O //] + |@same_bigop + [// + |#p #ltp #primep @(pad_bigop_nil … Atimes) + [@le_log + [@prime_to_lt_SO @primeb_true_to_prime //|//] + |#i #lei #iup %2 >le_to_leb_true + [% + |@(lt_to_le_to_lt ? (exp p (S (log p n)))) + [@lt_exp_log @prime_to_lt_SO @primeb_true_to_prime // + |@le_exp + [@prime_to_lt_O @primeb_true_to_prime // + |@le_S_S // + ] + ] + ] + ] + ] + ] + ] + ] +qed. + +theorem le_A_BA1: ∀n. O < n → + A(2*n) ≤ B(2*n)*A n. +#n #posn >(eq_A_2_n … posn) @le_times [2:@le_n] +>Bdef @le_pi #p #ltp #primep @le_pi #i #lti #_ @le_exp + [@prime_to_lt_O @primeb_true_to_prime // + |cases (true_or_false (leb (S n) (exp p (S i)))) #Hc >Hc + [whd in ⊢ (?%?); + cut (2*n/p\sup(S i) = 1) [2: #Hcut >Hcut @le_n] + @(div_mod_spec_to_eq (2*n) (exp p (S i)) + ? (mod (2*n) (exp p (S i))) ? (minus (2*n) (exp p (S i))) ) + [@div_mod_spec_div_mod @lt_O_exp @prime_to_lt_O @primeb_true_to_prime // + |cut (p\sup(S i)≤2*n) + [@(transitive_le ? (exp p (log p (2*n)))) + [@le_exp [@prime_to_lt_O @primeb_true_to_prime // | //] + |@le_exp_log >(times_n_O O) in ⊢ (?%?); @lt_times // + ] + ] #Hcut + @div_mod_spec_intro + [@lt_plus_to_minus + [// |normalize in ⊢ (? % ?); < plus_n_O @lt_plus @leb_true_to_le //] + |>commutative_plus >commutative_times in ⊢ (???(??%)); + < times_n_1 @plus_minus_m_m // + ] + ] + |@le_O_n + ] + ] +qed. + +theorem le_A_BA: ∀n. A(2*n) \le B(2*n)*A n. +#n cases n [@le_n |#m @le_A_BA1 @lt_O_S] +qed. + +theorem le_A_exp: ∀n. A(2*n) ≤ (exp 2 (pred (2*n)))*A n. +#n @(transitive_le ? (B(2*n)*A n)) + [@le_A_BA |@le_times [@le_B_exp |//]] +qed. + +theorem lt_4_to_le_A_exp: ∀n. 4 < n → + A(2*n) ≤ exp 2 ((2*n)-2)*A n. +#n #lt4n @(transitive_le ? (B(2*n)*A n)) + [@le_A_BA|@le_times [@(lt_4_to_le_B_exp … lt4n) |@le_n]] +qed. + +(* two technical lemmas *) +lemma times_2_pred: ∀n. 2*(pred n) \le pred (2*n). +#n cases n + [@le_n|#m @monotonic_le_plus_r @le_n_Sn] +qed. + +lemma le_S_times_2: ∀n. O < n → S n ≤ 2*n. +#n #posn elim posn + [@le_n + |#m #posm #Hind + cut (2*(S m) = S(S(2*m))) [normalize Hcut + @le_S_S @(transitive_le … Hind) @le_n_Sn + ] +qed. + +theorem le_A_exp1: ∀n. + A(exp 2 n) ≤ exp 2 ((2*(exp 2 n)-(S(S n)))). +#n elim n + [@le_n + |#n1 #Hind whd in ⊢ (?(?%)?); >commutative_times + @(transitive_le ??? (le_A_exp ?)) + @(transitive_le ? (2\sup(pred (2*2^n1))*2^(2*2^n1-(S(S n1))))) + [@monotonic_le_times_r // + |commutative_times in ⊢ (%→?); #Hind1 @(transitive_le ? (2*(S(S n2)))) + [@le_S_times_2 @lt_O_S |@monotonic_le_times_r //] + ] + ] #Hcut + @le_S_S_to_le cut(∀a,b. S a + b = S (a+b)) [//] #Hplus S_pred + [>eq_minus_S_pred in ⊢ (??%); >S_pred + [>plus_minus_commutative + [@monotonic_le_minus_l + cut (∀a. 2*a = a + a) [//] #times2 commutative_times @le_n + |@Hcut + ] + |@lt_plus_to_minus_r whd in ⊢ (?%?); + @(lt_to_le_to_lt ? (2*(S(S n1)))) + [>(times_n_1 (S(S n1))) in ⊢ (?%?); >commutative_times + @monotonic_lt_times_l [@lt_O_S |@le_n] + |@monotonic_le_times_r whd in ⊢ (??%); // + ] + ] + |whd >(times_n_1 1) in ⊢ (?%?); @le_times + [@le_n_Sn |@lt_O_exp @lt_O_S] + ] + ] + ] +qed. + +theorem monotonic_A: monotonic nat le A. +#n #m #lenm elim lenm + [@le_n + |#n1 #len #Hind @(transitive_le … Hind) + cut (∏_{p < S n1 | primeb p}(p^(log p n1)) + ≤∏_{p < S n1 | primeb p}(p^(log p (S n1)))) + [@le_pi #p #ltp #primep @le_exp + [@prime_to_lt_O @primeb_true_to_prime // + |@le_log [@prime_to_lt_SO @primeb_true_to_prime // | //] + ] + ] #Hcut + >psi_def in ⊢ (??%); cases (true_or_false (primeb (S n1))) #Hc + [>bigop_Strue in ⊢ (??%); [2://] + >(times_n_1 (A n1)) >commutative_times @le_times + [@lt_O_exp @lt_O_S |@Hcut] + |>bigop_Sfalse in ⊢ (??%); // + ] + ] +qed. + +(* +theorem le_A_exp2: \forall n. O < n \to +A(n) \le (exp (S(S O)) ((S(S O)) * (S(S O)) * n)). +intros. +apply (trans_le ? (A (exp (S(S O)) (S(log (S(S O)) n))))) + [apply monotonic_A. + apply lt_to_le. + apply lt_exp_log. + apply le_n + |apply (trans_le ? ((exp (S(S O)) ((S(S O))*(exp (S(S O)) (S(log (S(S O)) n))))))) + [apply le_A_exp1 + |apply le_exp + [apply lt_O_S + |rewrite > assoc_times.apply le_times_r. + change with ((S(S O))*((S(S O))\sup(log (S(S O)) n))≤(S(S O))*n). + apply le_times_r. + apply le_exp_log. + assumption + ] + ] + ] +qed. +*) + +(* example *) +example A_1: A 1 = 1. // qed. + +example A_2: A 2 = 2. // qed. + +example A_3: A 3 = 6. // qed. + +example A_4: A 4 = 12. // qed. + +(* +(* a better result *) +theorem le_A_exp3: \forall n. S O < n \to +A(n) \le exp (pred n) (2*(exp 2 (2 * n)). +intro. +apply (nat_elim1 n). +intros. +elim (or_eq_eq_S m). +elim H2 + [elim (le_to_or_lt_eq (S O) a) + [rewrite > H3 in ⊢ (? % ?). + apply (trans_le ? ((exp (S(S O)) ((S(S O)*a)))*A a)) + [apply le_A_exp + |apply (trans_le ? (((S(S O)))\sup((S(S O))*a)* + ((pred a)\sup((S(S O)))*((S(S O)))\sup((S(S O))*a)))) + [apply le_times_r. + apply H + [rewrite > H3. + rewrite > times_n_SO in ⊢ (? % ?). + rewrite > sym_times. + apply lt_times_l1 + [apply lt_to_le.assumption + |apply le_n + ] + |assumption + ] + |rewrite > sym_times. + rewrite > assoc_times. + rewrite < exp_plus_times. + apply (trans_le ? + (pred a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m))) + [rewrite > assoc_times. + apply le_times_r. + rewrite < exp_plus_times. + apply le_exp + [apply lt_O_S + |rewrite < H3. + simplify. + rewrite < plus_n_O. + apply le_S.apply le_S. + apply le_n + ] + |apply le_times_l. + rewrite > times_exp. + apply monotonic_exp1. + rewrite > H3. + rewrite > sym_times. + cases a + [apply le_n + |simplify. + rewrite < plus_n_Sm. + apply le_S. + apply le_n + ] + ] + ] + ] + |rewrite < H4 in H3. + simplify in H3. + rewrite > H3. + simplify. + apply le_S_S.apply le_S_S.apply le_O_n + |apply not_lt_to_le.intro. + apply (lt_to_not_le ? ? H1). + rewrite > H3. + apply (le_n_O_elim a) + [apply le_S_S_to_le.assumption + |apply le_O_n + ] + ] + |elim (le_to_or_lt_eq O a (le_O_n ?)) + [apply (trans_le ? (A ((S(S O))*(S a)))) + [apply monotonic_A. + rewrite > H3. + rewrite > times_SSO. + apply le_n_Sn + |apply (trans_le ? ((exp (S(S O)) ((S(S O)*(S a))))*A (S a))) + [apply le_A_exp + |apply (trans_le ? (((S(S O)))\sup((S(S O))*S a)* + (a\sup((S(S O)))*((S(S O)))\sup((S(S O))*(S a))))) + [apply le_times_r. + apply H + [rewrite > H3. + apply le_S_S. + simplify. + rewrite > plus_n_SO. + apply le_plus_r. + rewrite < plus_n_O. + assumption + |apply le_S_S.assumption + ] + |rewrite > sym_times. + rewrite > assoc_times. + rewrite < exp_plus_times. + apply (trans_le ? + (a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m))) + [rewrite > assoc_times. + apply le_times_r. + rewrite < exp_plus_times. + apply le_exp + [apply lt_O_S + |rewrite > times_SSO. + rewrite < H3. + simplify. + rewrite < plus_n_Sm. + rewrite < plus_n_O. + apply le_n + ] + |apply le_times_l. + rewrite > times_exp. + apply monotonic_exp1. + rewrite > H3. + rewrite > sym_times. + apply le_n + ] + ] + ] + ] + |rewrite < H4 in H3.simplify in H3. + apply False_ind. + apply (lt_to_not_le ? ? H1). + rewrite > H3. + apply le_ + ] + ] +qed. +*) + +theorem le_A_exp4: ∀n. 1 < n → + A(n) ≤ (pred n)*exp 2 ((2 * n) -3). +#n @(nat_elim1 n) +#m #Hind cases (even_or_odd m) +#a * #Hm >Hm #Hlt + [cut (0Hm >(times_n_1 a) in ⊢ (?%?); >commutative_times + @monotonic_lt_times_l [@lt_to_le // |@le_n] + |commutative_times in ⊢ (?(?%?)?); + >associative_times; @le_times + [>Hm cases a[@le_n|#b normalize @le_plus_n_r] + |plus_minus_commutative + [@le_n + |>Hm @(transitive_le ? (2*2) ? (le_n_Sn 3)) + @monotonic_le_times_r // + ] + ] + ] + ] + ] + ] + |Hm normalize Hm @le_S_S >(times_n_1 a) in ⊢ (?%?); >commutative_times + @monotonic_lt_times_l // + |@le_S_S // + ] + |cut (pred (S (2*a)) = 2*a) [//] #Spred >Spred + cut (pred (2*(S a)) = S (2 * a)) [normalize //] #Spred1 >Spred1 + cut (2*(S a) = S(S(2*a))) [normalize (commutative_times 2) in ⊢ (???%); >times2 >minus_Sn_m [%] + @le_S_S >(times_n_1 2) in ⊢ (?%?); @monotonic_le_times_r @Ha + ] #Hcut >Hcut + commutative_times in ⊢ (? (? % ?) ?); + >commutative_times in ⊢ (? (? (? % ?) ?) ?); + >associative_times @monotonic_le_times_r + plus_minus_commutative + [normalize >(plus_n_O (a+(a+0))) in ⊢ (?(?(??%)?)?); @le_n + |@le_S_S >(times_n_1 2) in ⊢ (?%?); @monotonic_le_times_r @Ha + ] + ] + ] + |@False_ind Hm in ⊢ (?%?); @(transitive_le … (le_A_exp ?)) + @(transitive_le ? (2\sup(pred(2*a))*(2\sup((2*a)-3)))) + [@monotonic_le_times_r @Hind >Hm >(times_n_1 a) in ⊢ (?%?); + >commutative_times @(monotonic_lt_times_l … (le_n ?)) + @(transitive_lt ? 3) + [@lt_O_S |@(le_times_to_le 2) [@lt_O_S |commutative_times Hm normalize Hm @le_S_S + >(times_n_1 a) in ⊢ (?%?); + >commutative_times @(monotonic_lt_times_l … (le_n ?)) + @(transitive_lt ? 3) + [@lt_O_S |@(le_times_to_le 2) [@lt_O_S |@le_S_S_to_le times2 (times_n_O O) in ⊢ (?%?); @lt_times [@lt_O_S|//] + |normalize in ⊢ (??(??%)); < plus_n_O >exp_plus_times + @le_times [2://] elim posn [//] + #m #le1m #Hind whd in ⊢ (??%); >commutative_times in ⊢ (??%); + @monotonic_le_times_r @(transitive_le … Hind) + >(times_n_1 m) in ⊢ (?%?); >commutative_times + @(monotonic_lt_times_l … (le_n ?)) @le1m + ] + |@le_times_to_le_div2 + [>(times_n_O O) in ⊢ (?%?); @lt_times [@lt_O_S|//] + |@(transitive_le ? ((B (2*n)*(2*n)))) + [commutative_times @le_exp_Al + cases (le_to_or_lt_eq ? ? (le_O_n (n/2))) [//] + #Heq @False_ind @(absurd ?? (lt_to_not_le ?? lt1n)) + >(div_mod n 2) (div_mod n 2) in ⊢ (??%); @le_plus_n_r + ] +qed. + +theorem eq_sigma_pi_SO_n: ∀n.∑_{i < n} 1 = n. +#n elim n // +qed. + +theorem leA_prim: ∀n. + exp n (prim n) \le A n * ∏_{p < S n | primeb p} p. +#n <(exp_sigma (S n) n primeb) exp_Sn @monotonic_le_times_r @(transitive_le ? (A (2*n))) + [@le_B_A |@le_Al] + ] +qed. + +theorem le_exp_prim4l: ∀n. O < n → + exp 2 (S(4*n)) ≤ exp (4*n) (S(prim (4*n))). +#n #posn @(transitive_le ? (2*(4*n*(B (4*n))))) + [>exp_Sn @monotonic_le_times_r + cut (4*n = 2*(2*n)) [Hcut @le_exp_B @lt_to_le whd >(times_n_1 2) in ⊢ (?%?); + @monotonic_le_times_r // + |>exp_Sn commutative_times in ⊢ (?(?%?)?); + >associative_times @monotonic_le_times_r @(transitive_le ? (A (4*n))) + [@le_B_A4 // |@le_Al] + ] +qed. + +theorem le_priml: ∀n. O < n → + 2*n ≤ (S (log 2 (2*n)))*S(prim (2*n)). +#n #posn <(eq_log_exp 2 (2*n) ?) in ⊢ (?%?); + [@(transitive_le ? ((log 2) (exp (2*n) (S(prim (2*n)))))) + [@le_log [@le_n |@le_exp_priml //] + |>commutative_times in ⊢ (??%); @log_exp1 @le_n + ] + |@le_n + ] +qed. + +theorem le_exp_primr: ∀n. + exp n (prim n) ≤ exp 2 (2*(2*n-3)). +#n @(transitive_le ? (exp (A n) 2)) + [>exp_Sn >exp_Sn whd in match (exp ? 0); commutative_times commutative_times @log_exp2 + [@le_n |@lt_to_le //] + |<(eq_log_exp 2 (2*(2*n-3))) in ⊢ (??%); + [@le_log [@le_n |@le_exp_primr] + |@le_n + ] + ] + ] +qed. + +theorem le_priml1: ∀n. O < n → + 2*n/((log 2 n)+2) - 1 ≤ prim (2*n). +#n #posn @le_plus_to_minus @le_times_to_le_div2 + [>commutative_plus @lt_O_S + |>commutative_times in ⊢ (??%); (times_n_1 2) in ⊢ (?%?); @monotonic_lt_times_r // + ] +qed. + +theorem eq_prim_prim_pred: ∀n. 1 < n → + prim (2*n) = prim (pred (2*n)). +#n #ltn +lapply (S_pred (2*n) ?) [>(times_n_1 0) in ⊢ (?%?); @lt_times //] #H2n +lapply (not_prime_times_2 n ltn) #notp2n +whd in ⊢ (??%?); >(not_prime_to_primeb_false … notp2n) whd in ⊢ (??%?); +Heq + Heq + Hn normalize // + ] +qed. + +(* axiom daemon : ∀P:Prop.P. *) + +(* la prova potrebbe essere migliorata *) +theorem le_prim_n3: ∀n. 15 ≤ n → + prim n ≤ pred (n/2). +#n #len cases (even_or_odd (pred n)) #a * #Hpredn + [cut (n = S (2*a)) [Hn @(transitive_le ? (pred a)) + [@le_prim_n2 @(le_times_to_le 2) [//|@le_S_S_to_le Hn @(transitive_le ? (pred a)) + [>eq_prim_prim_pred + [2:@(lt_times_n_to_lt_r 2) Hpredn @le_prim_n2 @le_S_S_to_le @(lt_times_n_to_lt_r 2) (plus_n_O (log i n)) in ⊢ (?%?); >plus_n_Sm + @monotonic_le_plus_r @lt_O_log // + @le_S_S_to_le // + ] + ] + |bigop_Strue in ⊢ (???%); // + cases (true_or_false (dividesb n1 m)) #Hdivides + [>bigop_Strue [@eq_f @Hind| @true_to_andb_true //] + |>bigop_Sfalse + [>not_divides_to_ord_O + [whd in ⊢ (???(?%?)); // + |@dividesb_false_to_not_divides // + |@primeb_true_to_prime // + ] + |>Hprime >Hdivides % + ] + ] +|>bigop_Sfalse [>bigop_Sfalse // |>Hprime %] +] +qed. + +(* integrations to minimization *) +theorem false_to_lt_max: ∀f,n,m.O < n → + f n = false → max m f ≤ n → max m f < n. +#f #n #m #posn #Hfn #Hmax cases (le_to_or_lt_eq ?? Hmax) -Hmax #Hmax + [// + |cases (exists_max_forall_false f m) + [* #_ #Hfmax @False_ind @(absurd ?? not_eq_true_false) // + |* // + ] + ] +qed. + +(* boh ... +theorem lt_max_to_false : ∀f,n,m. + max n f < m → m ≤ n → f m = false. +#f #n elim n + [#m #H1 #H2 @False_ind @(absurd ? H2) @lt_to_not_le // + |#n1 #Hind #m whd in ⊢ (?%?→?); #Hmax #ltm +elim (max_S_max f n1); in H1 ⊢ %. +elim H1. +absurd (m \le S n1).assumption. +apply lt_to_not_le.rewrite < H5.assumption. +elim H1. +apply (le_n_Sm_elim m n1 H2). +intro. +apply H.rewrite < H5.assumption. +apply le_S_S_to_le.assumption. +intro.rewrite > H6.assumption. +qed. *) + +(* integrations to minimization +lemma lt_1_max_prime: ∀n. 1 < n → + 1 < max n (λi:nat.primeb i∧dividesb i n). +#n #lt1n +@(lt_to_le_to_lt ? (smallest_factor n)) + [@lt_SO_smallest_factor // + |@true_to_le_max + [@le_smallest_factor_n + |apply true_to_true_to_andb_true + [apply prime_to_primeb_true. + apply prime_smallest_factor_n. + assumption + |apply divides_to_divides_b_true + [apply lt_O_smallest_factor.apply lt_to_le.assumption + |apply divides_smallest_factor_n. + apply lt_to_le.assumption + ] + ] + ] + ] +qed. *) + +theorem lt_max_to_pi_p_primeb: ∀q,m. Obigop_Strue + [>(exp_ord n m … posm) in ⊢ (??%?); + [@eq_f >(Hind (ord_rem m n)) + [@same_bigop + [#x #ltxn cases (true_or_false (primeb x)) #Hx >Hx + [cases (true_or_false (dividesb x (ord_rem m n))) #Hx1 >Hx1 + [@sym_eq @divides_to_dividesb_true + [@prime_to_lt_O @primeb_true_to_prime // + |@(transitive_divides ? (ord_rem m n)) + [@dividesb_true_to_divides // + |@(divides_ord_rem … posm) @(transitive_lt … ltxn) + @prime_to_lt_SO @primeb_true_to_prime // + ] + ] + |@sym_eq @not_divides_to_dividesb_false + [@prime_to_lt_O @primeb_true_to_prime // + |@(ord_O_to_not_divides … posm) + [@primeb_true_to_prime // + |<(ord_ord_rem n … posm … ltxn) + [@not_divides_to_ord_O + [@primeb_true_to_prime // + |@dividesb_false_to_not_divides // + ] + |@primeb_true_to_prime // + |@primeb_true_to_prime @(andb_true_l ?? Hcase) + ] + ] + ] + ] + |// + ] + |#x #ltxn #Hx @eq_f @ord_ord_rem // + [@primeb_true_to_prime @(andb_true_l ? ? Hcase) + |@primeb_true_to_prime @(andb_true_l ? ? Hx) + ] + ] + |@not_eq_to_le_to_lt + [elim (exists_max_forall_false (λi:nat.primeb i∧dividesb i (ord_rem m n)) (ord_rem m n)) + [* #Hex #Hord_rem cases Hex #x * #H6 #H7 % #H + >H in Hord_rem; #Hn @(absurd ?? (not_divides_ord_rem m n posm ?)) + [@dividesb_true_to_divides @(andb_true_r ?? Hn) + |@prime_to_lt_SO @primeb_true_to_prime @(andb_true_l ?? Hn) + ] + |* #Hall #Hmax >Hmax @lt_to_not_eq @prime_to_lt_O + @primeb_true_to_prime @(andb_true_l ?? Hcase) + ] + |@(transitive_le ? (max m (λi:nat.primeb i∧dividesb i (ord_rem m n)))) + [@le_to_le_max @(divides_to_le … posm) @(divides_ord_rem … posm) + @prime_to_lt_SO @primeb_true_to_prime @(andb_true_l ?? Hcase) + |@(transitive_le ? (max m (λi:nat.primeb i∧dividesb i m))) + [@le_max_f_max_g #i #ltim #Hi + cases (true_or_false (primeb i)) #Hprimei >Hprimei + [@divides_to_dividesb_true + [@prime_to_lt_O @primeb_true_to_prime // + |@(transitive_divides ? (ord_rem m n)) + [@dividesb_true_to_divides @(andb_true_r ?? Hi) + |@(divides_ord_rem … posm) + @prime_to_lt_SO @primeb_true_to_prime + @(andb_true_l ?? Hcase) + ] + ] + |>Hprimei in Hi; #Hi @Hi + ] + |@le_S_S_to_le // + ] + ] + ] + |@(lt_O_ord_rem … posm) @prime_to_lt_SO + @primeb_true_to_prime @(andb_true_l ?? Hcase) + ] + |@prime_to_lt_SO @primeb_true_to_prime @(andb_true_l ?? Hcase) + ] + |// + ] + |cases (le_to_or_lt_eq ?? posm) #Hm + [>bigop_Sfalse + [@(Hind … posm) @false_to_lt_max + [@(lt_to_le_to_lt ? (max m (λi:nat.primeb i∧dividesb i m))) + [@lt_to_le @dae (* portare @lt_SO_max_prime // *) + |@le_S_S_to_le // + ] + |// + |@le_S_S_to_le // + ] + |@Hcase + ] + |primei // + @sym_eq @not_divides_to_dividesb_false + [@prime_to_lt_O @primeb_true_to_prime // + |% #divi @(absurd ?? (le_to_not_lt i 1 ?)) + [@prime_to_lt_SO @(primeb_true_to_prime ? primei) + |@divides_to_le // + ] + ] + |// + ] + ] + ] + ] +qed. + +(* factorization of n into primes *) +theorem pi_p_primeb_dividesb: ∀n. O < n → + n = ∏_{ p < S n | primeb p ∧ dividesb p n} (exp p (ord n p)). +#n #posn @lt_max_to_pi_p_primeb // @le_S_S @le_max_n +qed. + +theorem pi_p_primeb: ∀n. O < n → + n = ∏_{ p < (S n) | primeb p}(exp p (ord n p)). +#n #posn (exp_ord p ? lt1p posn) in ⊢ (??(??%)); +>log_exp // @lt_O_ord_rem // +qed. + +theorem sigma_p_dividesb: +∀m,n,p. O < n → prime p → p ∤ n → +m = ∑_{ i < m | dividesb (p\sup (S i)) ((exp p m)*n)} 1. +#m elim m // -m #m #Hind #n #p #posn #primep #ndivp +>bigop_Strue + [>commutative_plus (Hind n p posn primep ndivp) in ⊢ (? ? % ?); + @same_bigop + [#i #ltim cases (true_or_false (dividesb (p\sup(S i)) (p\sup m*n))) #Hc >Hc + [@sym_eq @divides_to_dividesb_true + [@lt_O_exp @prime_to_lt_O // + |%{((exp p (m - i))*n)} commutative_plus + @plus_minus_m_m @lt_to_le // + ] + |(* @sym_eq *) + @False_ind @(absurd ?? (dividesb_false_to_not_divides ? ? Hc)) + %{((exp p (m - S i))*n)} commutative_plus @plus_minus_m_m // + assumption + |% + ] + ] + |// + ] + |@divides_to_dividesb_true + [@lt_O_exp @prime_to_lt_O // | %{n} //] + ] +qed. + +theorem sigma_p_dividesb1: +∀m,n,p,k. O < n → prime p → p ∤ n → m ≤ k → + m = ∑_{i < k | dividesb (p\sup (S i)) ((exp p m)*n)} 1. +#m #n #p #k #posn #primep #ndivp #lemk +lapply (prime_to_lt_SO ? primep) #lt1p +lapply (prime_to_lt_O ? primep) #posp +>(sigma_p_dividesb m n p posn primep ndivp) in ⊢ (??%?); +>(pad_bigop k m) // @same_bigop + [#i #ltik cases (true_or_false (leb m i)) #Him > Him + [whd in ⊢(??%?); @sym_eq + @not_divides_to_dividesb_false + [@lt_O_exp // + |lapply (leb_true_to_le … Him) -Him #Him + % #Hdiv @(absurd ?? (le_to_not_lt ?? Him)) + (* <(ord_exp p m lt1p) *) >(plus_n_O m) + <(not_divides_to_ord_O ?? primep ndivp) + <(ord_exp p m lt1p) + (times_n_O O) @lt_times // @lt_O_exp // + ] + |@lt_O_exp // + ] + ] + |% + ] + |// + ] +qed. + +theorem eq_ord_sigma_p: +∀n,m,x. O < n → prime x → +exp x m ≤ n → n < exp x (S m) → +ord n x= ∑_{i < m | dividesb (x\sup (S i)) n} 1. +#n #m #x #posn #primex #Hexp #ltn +lapply (prime_to_lt_SO ? primex) #lt1x +>(exp_ord x n) in ⊢ (???%); // @sigma_p_dividesb1 + [@lt_O_ord_rem // + |// + |@not_divides_ord_rem // + |@le_S_S_to_le @(le_to_lt_to_lt ? (log x n)) + [@le_ord_log // + |@(lt_exp_to_lt x) + [@lt_to_le // + |@(le_to_lt_to_lt ? n ? ? ltn) @le_exp_log // + ] + ] + ] +qed. + +theorem pi_p_primeb1: ∀n. O < n → +n = ∏_{p < S n| primeb p} + (∏_{i < log p n| dividesb (exp p (S i)) n} p). +#n #posn >(pi_p_primeb n posn) in ⊢ (??%?); +@same_bigop + [// + |#p #ltp #primep >exp_sigma @eq_f @eq_ord_sigma_p + [// + |@primeb_true_to_prime // + |@le_exp_log // + |@lt_exp_log @prime_to_lt_SO @primeb_true_to_prime // + ] + ] +qed. + +(* the factorial function *) +theorem eq_fact_pi_p:∀n. + fact n = ∏_{i < S n | leb 1 i} i. +#n elim n // #n1 #Hind whd in ⊢ (??%?); >commutative_times >bigop_Strue + [@eq_f // | % ] +qed. + +theorem eq_sigma_p_div: ∀n,q.O < q → + ∑_{ m < S n | leb (S O) m ∧ dividesb q m} 1 =n/q. +#n #q #posq +@(div_mod_spec_to_eq n q ? (n \mod q) ? (n \mod q)) + [@div_mod_spec_intro + [@lt_mod_m_m // + |elim n + [normalize cases q // + |#n1 #Hind cases (or_div_mod1 n1 q posq) + [* #divq #eqn1 >divides_to_mod_O // + bigop_Strue + [>eqn1 in ⊢ (??%?); @eq_f2 + [bigop_Sfalse + [>(mod_S … posq) + [< plus_n_Sm @eq_f // + |cases (le_to_or_lt_eq (S (mod n1 q)) q ?) + [// + |#eqq @False_ind cases ndiv #Hdiv @Hdiv + %{(S(div n1 q))} not_divides_to_dividesb_false // + ] + ] + ] + ] + |@div_mod_spec_div_mod // + ] +qed. + +definition Atimes ≝ mk_Aop nat 1 times ???. + [#a normalize eq_fact_pi_p +@(trans_eq ?? + (∏_{m < S n | leb 1 m} + (∏_{p < S m | primeb p} + (∏_{i < log p m | dividesb (exp p (S i)) m} p)))) + [@same_bigop [// |#x #Hx1 #Hx2 @pi_p_primeb1 @leb_true_to_le //] + |@(trans_eq ?? + (∏_{m < S n | leb 1 m} + (∏_{p < S m | primeb p ∧ leb p m} + (∏_{ i < log p m | dividesb ((p)\sup(S i)) m} p)))) + [@same_bigop + [// + |#x #Hx1 #Hx2 @same_bigop + [#p #ltp >(le_to_leb_true … (le_S_S_to_le …ltp)) + cases (primeb p) // + |// + ] + ] + |@(trans_eq ?? + (∏_{m < S n | leb 1 m} + (∏_{p < S n | primeb p ∧ leb p m} + (∏_{i < log p m |dividesb ((p)\sup(S i)) m} p)))) + [@same_bigop + [// + |#p #Hp1 #Hp2 @sym_eq (* COMPLETARE + apply false_to_eq_pi_p + [assumption + |intros.rewrite > lt_to_leb_false + [elim primeb;reflexivity|assumption] + ] *) + @daemon + ] + |(* make a general theorem *) + @(trans_eq ?? + (∏_{p < S n | primeb p} + (∏_{m < S n | leb p m} + (∏_{i < log p m | dividesb ((p)\sup(S i)) m} p)))) + [@daemon + (* PORTARE + @pi_p_pi_p1. + intros. + apply (bool_elim ? (primeb y \landy x));intros + [rewrite > (le_to_leb_true (S O) x) + [reflexivity + |apply (trans_le ? y) + [apply prime_to_lt_O. + apply primeb_true_to_prime. + apply (andb_true_true ? ? H2) + |apply leb_true_to_le. + apply (andb_true_true_r ? ? H2) + ] + ] + |elim (leb (S O) x);reflexivity + ] *) + |@same_bigop + [// + |#p #Hp1 #Hp2 + @(trans_eq ?? + (∏_{m < S n | leb p m} + (∏_{i < log p n | dividesb (p\sup(S i)) m} p))) + [@same_bigop + [// + |#x #Hx1 #Hx2 @sym_eq + @sym_eq @pad_bigop1 + [@le_log + [@prime_to_lt_SO @primeb_true_to_prime // + |@le_S_S_to_le // + ] + |#i #Hi1 #Hi2 @not_divides_to_dividesb_false + [@lt_O_exp @prime_to_lt_O @primeb_true_to_prime // + |@(not_to_not … (lt_to_not_le x (exp p (S i)) ?)) + [#H @divides_to_le // @(lt_to_le_to_lt ? p) + [@prime_to_lt_O @primeb_true_to_prime // + |@leb_true_to_le // + ] + |@(lt_to_le_to_lt ? (exp p (S(log p x)))) + [@lt_exp_log @prime_to_lt_SO @primeb_true_to_prime // + |@le_exp + [@ prime_to_lt_O @primeb_true_to_prime // + |@le_S_S // + ] + ] + ] + ] + ] + ] + |@ + (trans_eq ? ? + (∏_{i < log p n} + (∏_{m < S n | leb p m ∧ dividesb (p\sup(S i)) m} p))) + [@(bigop_commute ?????? nat 1 ACtimes (λm,i.p) ???) // + cut (p ≤ n) [@le_S_S_to_le //] #lepn + @(lt_O_log … lepn) @(lt_to_le_to_lt … lepn) @prime_to_lt_SO + @primeb_true_to_prime // + |@same_bigop + [// + |#m #ltm #_ >exp_sigma @eq_f + @(trans_eq ?? + (∑_{i < S n |leb 1 i∧dividesb (p\sup(S m)) i} 1)) + [@same_bigop + [#i #lti + cases (true_or_false (dividesb (p\sup(S m)) i)) #Hc >Hc + [cases (true_or_false (leb p i)) #Hp3 >Hp3 + [>le_to_leb_true + [// + |@(transitive_le ? p) + [@prime_to_lt_O @primeb_true_to_prime // + |@leb_true_to_le // + ] + ] + |>lt_to_leb_false + [// + |@not_le_to_lt + @(not_to_not ??? (leb_false_to_not_le ?? Hp3)) #posi + @(transitive_le ? (exp p (S m))) + [>(exp_n_1 p) in ⊢ (?%?); + @le_exp + [@prime_to_lt_O @primeb_true_to_prime // + |@le_S_S @le_O_n + ] + |@(divides_to_le … posi) + @dividesb_true_to_divides // + ] + ] + ] + |cases (leb p i) cases (leb 1 i) // + ] + |// + ] + |@eq_sigma_p_div @lt_O_exp + @prime_to_lt_O @primeb_true_to_prime // + ] + ] + ] + ] + ] + ] + ] + ] + ] +qed. + +theorem fact_pi_p2: ∀n. fact (2*n) = +∏_{p < S (2*n) | primeb p} + (∏_{i < log p (2*n)} + (exp p (2*(n /(exp p (S i))))*(exp p (mod (2*n /(exp p (S i))) 2)))). +#n >fact_pi_p @same_bigop + [// + |#p #ltp #primep @same_bigop + [// + |#i #lti #_ commutative_times in ⊢ (???(?%?)); + cut (0 < p ^ (S i)) + [@lt_O_exp @prime_to_lt_O @primeb_true_to_prime //] + generalize in match (p ^(S i)); #a #posa + >(div_times_times n a 2) // >(commutative_times n 2) + fact_pi_p2 @same_bigop + [// + |#p #ltp #primep @times_pi + ] +qed. + +theorem pi_p_primeb4: ∀n. 1 < n → +∏_{p < S (2*n) | primeb p} + (∏_{i < log p (2*n)}(exp p (2*(n /(exp p (S i)))))) += +∏_{p < S n | primeb p} + (∏_{i < log p (2*n)}(exp p (2*(n /(exp p (S i)))))). +#n #lt1n +@sym_eq @(pad_bigop_nil … ACtimes) + [@le_S_S /2 by / + |#i #ltn #lti %2 + >log_i_2n // + [>bigop_Strue // whd in ⊢ (??(??%)?); eq_div_O // + |@le_S_S_to_le // + ] + ] +qed. + +theorem pi_p_primeb5: ∀n. 1 < n → +∏_{p < S (2*n) | primeb p} + (∏_{i < log p (2*n)} (exp p (2*(n /(exp p (S i)))))) += +∏_{p < S n | primeb p} + (∏_{i < log p n} (exp p (2*(n /(exp p (S i)))))). +#n #lt1n >(pi_p_primeb4 ? lt1n) @same_bigop + [// + |#p #lepn #primebp @sym_eq @(pad_bigop_nil … ACtimes) + [@le_log + [@prime_to_lt_SO @primeb_true_to_prime // + |// + ] + |#i #lelog #lti %2 >eq_div_O // + @(lt_to_le_to_lt ? (exp p (S(log p n)))) + [@lt_exp_log @prime_to_lt_SO @primeb_true_to_prime // + |@le_exp + [@prime_to_lt_O @primeb_true_to_prime // |@le_S_S //] + ] + ] + ] +qed. + +theorem exp_fact_2: ∀n. +exp (fact n) 2 = + ∏_{p < S n| primeb p} + (∏_{i < log p n} (exp p (2*(n /(exp p (S i)))))). +#n >fact_pi_p commutative_times @exp_exp_times + ] + |@exp_pi + ] +qed. + +definition B ≝ λn. +∏_{p < S n | primeb p} + (∏_{i < log p n} (exp p (mod (n /(exp p (S i))) 2))). + +lemma Bdef : ∀n.B n = + ∏_{p < S n | primeb p} + (∏_{i < log p n} (exp p (mod (n /(exp p (S i))) 2))). +// qed-. + +example B_SSSO: B 3 = 6. // +qed. + +example B_SSSSO: B 4 = 6. // +qed. + +example B_SSSSSO: B 5 = 30. // +qed. + +example B_SSSSSSO: B 6 = 20. // +qed. + +example B_SSSSSSSO: B 7 = 140. // +qed. + +example B_SSSSSSSSO: B 8 = 70. // +qed. + +theorem eq_fact_B:∀n. 1 < n → + (2*n)! = exp (n!) 2 * B(2*n). +#n #lt1n >fact_pi_p3 @eq_f2 + [@sym_eq >pi_p_primeb5 [@exp_fact_2|//] |// ] +qed. + +theorem le_B_A: ∀n. B n ≤ A n. +#n >eq_A_A' @le_pi #p #ltp #primep +@le_pi #i #lti #_ >(exp_n_1 p) in ⊢ (??%); @le_exp + [@prime_to_lt_O @primeb_true_to_prime // + |@le_S_S_to_le @lt_mod_m_m @lt_O_S + ] +qed. + +theorem le_B_A4: ∀n. O < n → 2 * B (4*n) ≤ A (4*n). +#n #posn >eq_A_A' +cut (2 < (S (4*n))) + [@le_S_S >(times_n_1 2) in ⊢ (?%?); @le_times //] #H2 +cut (OBdef >(bigop_diff ??? ACtimes ? 2 ? H2) [2:%] +>Adef >(bigop_diff ??? ACtimes ? 2 ? H2) in ⊢ (??%); [2:%] +(bigop_diff ??? ACtimes ? 0 ? Hlog) [2://] + >(bigop_diff ??? ACtimes ? 0 ? Hlog) in ⊢ (??%); [2:%] + ACtimesdef @le_times + [H4 >associative_times + >commutative_times in ⊢ (?(??(??(?(?%?)?)))?); + >div_times [2://] >divides_to_mod_O + [@le_n |%{n} // |@lt_O_S] + |@le_pi #i #lti #H >(exp_n_1 2) in ⊢ (??%); + @le_exp [@lt_O_S |@le_S_S_to_le @lt_mod_m_m @lt_O_S] + ] + |@le_pi #p #ltp #Hp @le_pi #i #lti #H + >(exp_n_1 p) in ⊢ (??%); @le_exp + [@prime_to_lt_O @primeb_true_to_prime @(andb_true_r ?? Hp) + |@le_S_S_to_le @lt_mod_m_m @lt_O_S + ] + ] +qed. + +(* not usefull +theorem le_fact_A:\forall n.S O < n \to +fact (2*n) \le exp (fact n) 2 * A (2*n). +intros. +rewrite > eq_fact_B + [apply le_times_r. + apply le_B_A + |assumption + ] +qed. *) + +theorem lt_SO_to_le_B_exp: ∀n. 1 < n → + B (2*n) ≤ exp 2 (pred (2*n)). +#n #lt1n @(le_times_to_le (exp (fact n) 2)) + [@lt_O_exp // + |<(eq_fact_B … lt1n) exp_2 exp_2 commutative_times in ⊢ (??(?%?)); + >associative_times in ⊢ (??%); <(eq_fact_B … lt1n) + eq_A_A' > eq_A_A' +cut ( + ∏_{p < S n | primeb p} (∏_{i Adef in ⊢ (???%); >Hcut + Adef @same_bigop + [// + |#p #lt1p #primep Hc + [normalize plus_n_O // + |normalize lt_to_leb_false + [normalize @plus_n_O + |@le_S_S @(transitive_le ? (exp p (log p n))) + [@le_exp [@prime_to_lt_O @primeb_true_to_prime //|//] + |@le_exp_log // + ] + ] + ] + ] + |@(trans_eq ?? + (∏_{p < S (2*n) | primeb p} + (∏_{i lt_to_log_O //] + |@same_bigop + [// + |#p #ltp #primep @(pad_bigop_nil … Atimes) + [@le_log + [@prime_to_lt_SO @primeb_true_to_prime //|//] + |#i #lei #iup %2 >le_to_leb_true + [% + |@(lt_to_le_to_lt ? (exp p (S (log p n)))) + [@lt_exp_log @prime_to_lt_SO @primeb_true_to_prime // + |@le_exp + [@prime_to_lt_O @primeb_true_to_prime // + |@le_S_S // + ] + ] + ] + ] + ] + ] + ] + ] +qed. + +theorem le_A_BA1: ∀n. O < n → + A(2*n) ≤ B(2*n)*A n. +#n #posn >(eq_A_2_n … posn) @le_times [2:@le_n] +>Bdef @le_pi #p #ltp #primep @le_pi #i #lti #_ @le_exp + [@prime_to_lt_O @primeb_true_to_prime // + |cases (true_or_false (leb (S n) (exp p (S i)))) #Hc >Hc + [whd in ⊢ (?%?); + cut (2*n/p\sup(S i) = 1) [2: #Hcut >Hcut @le_n] + @(div_mod_spec_to_eq (2*n) (exp p (S i)) + ? (mod (2*n) (exp p (S i))) ? (minus (2*n) (exp p (S i))) ) + [@div_mod_spec_div_mod @lt_O_exp @prime_to_lt_O @primeb_true_to_prime // + |cut (p\sup(S i)≤2*n) + [@(transitive_le ? (exp p (log p (2*n)))) + [@le_exp [@prime_to_lt_O @primeb_true_to_prime // | //] + |@le_exp_log >(times_n_O O) in ⊢ (?%?); @lt_times // + ] + ] #Hcut + @div_mod_spec_intro + [@lt_plus_to_minus + [// |normalize in ⊢ (? % ?); < plus_n_O @lt_plus @leb_true_to_le //] + |>commutative_plus >commutative_times in ⊢ (???(??%)); + < times_n_1 @plus_minus_m_m // + ] + ] + |@le_O_n + ] + ] +qed. + +theorem le_A_BA: ∀n. A(2*n) \le B(2*n)*A n. +#n cases n [@le_n |#m @le_A_BA1 @lt_O_S] +qed. + +theorem le_A_exp: ∀n. A(2*n) ≤ (exp 2 (pred (2*n)))*A n. +#n @(transitive_le ? (B(2*n)*A n)) + [@le_A_BA |@le_times [@le_B_exp |//]] +qed. + +theorem lt_4_to_le_A_exp: ∀n. 4 < n → + A(2*n) ≤ exp 2 ((2*n)-2)*A n. +#n #lt4n @(transitive_le ? (B(2*n)*A n)) + [@le_A_BA|@le_times [@(lt_4_to_le_B_exp … lt4n) |@le_n]] +qed. + +(* two technical lemmas *) +lemma times_2_pred: ∀n. 2*(pred n) \le pred (2*n). +#n cases n + [@le_n|#m @monotonic_le_plus_r @le_n_Sn] +qed. + +lemma le_S_times_2: ∀n. O < n → S n ≤ 2*n. +#n #posn elim posn + [@le_n + |#m #posm #Hind + cut (2*(S m) = S(S(2*m))) [normalize Hcut + @le_S_S @(transitive_le … Hind) @le_n_Sn + ] +qed. + +theorem le_A_exp1: ∀n. + A(exp 2 n) ≤ exp 2 ((2*(exp 2 n)-(S(S n)))). +#n elim n + [@le_n + |#n1 #Hind whd in ⊢ (?(?%)?); >commutative_times + @(transitive_le ??? (le_A_exp ?)) + @(transitive_le ? (2\sup(pred (2*2^n1))*2^(2*2^n1-(S(S n1))))) + [@monotonic_le_times_r // + |commutative_times in ⊢ (%→?); #Hind1 @(transitive_le ? (2*(S(S n2)))) + [@le_S_times_2 @lt_O_S |@monotonic_le_times_r //] + ] + ] #Hcut + @le_S_S_to_le cut(∀a,b. S a + b = S (a+b)) [//] #Hplus S_pred + [>eq_minus_S_pred in ⊢ (??%); >S_pred + [>plus_minus_commutative + [@monotonic_le_minus_l + cut (∀a. 2*a = a + a) [//] #times2 commutative_times @le_n + |@Hcut + ] + |@lt_plus_to_minus_r whd in ⊢ (?%?); + @(lt_to_le_to_lt ? (2*(S(S n1)))) + [>(times_n_1 (S(S n1))) in ⊢ (?%?); >commutative_times + @monotonic_lt_times_l [@lt_O_S |@le_n] + |@monotonic_le_times_r whd in ⊢ (??%); // + ] + ] + |whd >(times_n_1 1) in ⊢ (?%?); @le_times + [@le_n_Sn |@lt_O_exp @lt_O_S] + ] + ] + ] +qed. + +theorem monotonic_A: monotonic nat le A. +#n #m #lenm elim lenm + [@le_n + |#n1 #len #Hind @(transitive_le … Hind) + cut (∏_{p < S n1 | primeb p}(p^(log p n1)) + ≤∏_{p < S n1 | primeb p}(p^(log p (S n1)))) + [@le_pi #p #ltp #primep @le_exp + [@prime_to_lt_O @primeb_true_to_prime // + |@le_log [@prime_to_lt_SO @primeb_true_to_prime // | //] + ] + ] #Hcut + >psi_def in ⊢ (??%); cases (true_or_false (primeb (S n1))) #Hc + [>bigop_Strue in ⊢ (??%); [2://] + >(times_n_1 (A n1)) >commutative_times @le_times + [@lt_O_exp @lt_O_S |@Hcut] + |>bigop_Sfalse in ⊢ (??%); // + ] + ] +qed. + +(* +theorem le_A_exp2: \forall n. O < n \to +A(n) \le (exp (S(S O)) ((S(S O)) * (S(S O)) * n)). +intros. +apply (trans_le ? (A (exp (S(S O)) (S(log (S(S O)) n))))) + [apply monotonic_A. + apply lt_to_le. + apply lt_exp_log. + apply le_n + |apply (trans_le ? ((exp (S(S O)) ((S(S O))*(exp (S(S O)) (S(log (S(S O)) n))))))) + [apply le_A_exp1 + |apply le_exp + [apply lt_O_S + |rewrite > assoc_times.apply le_times_r. + change with ((S(S O))*((S(S O))\sup(log (S(S O)) n))≤(S(S O))*n). + apply le_times_r. + apply le_exp_log. + assumption + ] + ] + ] +qed. +*) + +(* example *) +example A_1: A 1 = 1. // qed. + +example A_2: A 2 = 2. // qed. + +example A_3: A 3 = 6. // qed. + +example A_4: A 4 = 12. // qed. + +(* +(* a better result *) +theorem le_A_exp3: \forall n. S O < n \to +A(n) \le exp (pred n) (2*(exp 2 (2 * n)). +intro. +apply (nat_elim1 n). +intros. +elim (or_eq_eq_S m). +elim H2 + [elim (le_to_or_lt_eq (S O) a) + [rewrite > H3 in ⊢ (? % ?). + apply (trans_le ? ((exp (S(S O)) ((S(S O)*a)))*A a)) + [apply le_A_exp + |apply (trans_le ? (((S(S O)))\sup((S(S O))*a)* + ((pred a)\sup((S(S O)))*((S(S O)))\sup((S(S O))*a)))) + [apply le_times_r. + apply H + [rewrite > H3. + rewrite > times_n_SO in ⊢ (? % ?). + rewrite > sym_times. + apply lt_times_l1 + [apply lt_to_le.assumption + |apply le_n + ] + |assumption + ] + |rewrite > sym_times. + rewrite > assoc_times. + rewrite < exp_plus_times. + apply (trans_le ? + (pred a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m))) + [rewrite > assoc_times. + apply le_times_r. + rewrite < exp_plus_times. + apply le_exp + [apply lt_O_S + |rewrite < H3. + simplify. + rewrite < plus_n_O. + apply le_S.apply le_S. + apply le_n + ] + |apply le_times_l. + rewrite > times_exp. + apply monotonic_exp1. + rewrite > H3. + rewrite > sym_times. + cases a + [apply le_n + |simplify. + rewrite < plus_n_Sm. + apply le_S. + apply le_n + ] + ] + ] + ] + |rewrite < H4 in H3. + simplify in H3. + rewrite > H3. + simplify. + apply le_S_S.apply le_S_S.apply le_O_n + |apply not_lt_to_le.intro. + apply (lt_to_not_le ? ? H1). + rewrite > H3. + apply (le_n_O_elim a) + [apply le_S_S_to_le.assumption + |apply le_O_n + ] + ] + |elim (le_to_or_lt_eq O a (le_O_n ?)) + [apply (trans_le ? (A ((S(S O))*(S a)))) + [apply monotonic_A. + rewrite > H3. + rewrite > times_SSO. + apply le_n_Sn + |apply (trans_le ? ((exp (S(S O)) ((S(S O)*(S a))))*A (S a))) + [apply le_A_exp + |apply (trans_le ? (((S(S O)))\sup((S(S O))*S a)* + (a\sup((S(S O)))*((S(S O)))\sup((S(S O))*(S a))))) + [apply le_times_r. + apply H + [rewrite > H3. + apply le_S_S. + simplify. + rewrite > plus_n_SO. + apply le_plus_r. + rewrite < plus_n_O. + assumption + |apply le_S_S.assumption + ] + |rewrite > sym_times. + rewrite > assoc_times. + rewrite < exp_plus_times. + apply (trans_le ? + (a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m))) + [rewrite > assoc_times. + apply le_times_r. + rewrite < exp_plus_times. + apply le_exp + [apply lt_O_S + |rewrite > times_SSO. + rewrite < H3. + simplify. + rewrite < plus_n_Sm. + rewrite < plus_n_O. + apply le_n + ] + |apply le_times_l. + rewrite > times_exp. + apply monotonic_exp1. + rewrite > H3. + rewrite > sym_times. + apply le_n + ] + ] + ] + ] + |rewrite < H4 in H3.simplify in H3. + apply False_ind. + apply (lt_to_not_le ? ? H1). + rewrite > H3. + apply le_ + ] + ] +qed. +*) + +theorem le_A_exp4: ∀n. 1 < n → + A(n) ≤ (pred n)*exp 2 ((2 * n) -3). +#n @(nat_elim1 n) +#m #Hind cases (even_or_odd m) +#a * #Hm >Hm #Hlt + [cut (0Hm >(times_n_1 a) in ⊢ (?%?); >commutative_times + @monotonic_lt_times_l [@lt_to_le // |@le_n] + |commutative_times in ⊢ (?(?%?)?); + >associative_times; @le_times + [>Hm cases a[@le_n|#b normalize @le_plus_n_r] + |plus_minus_commutative + [@le_n + |>Hm @(transitive_le ? (2*2) ? (le_n_Sn 3)) + @monotonic_le_times_r // + ] + ] + ] + ] + ] + ] + |Hm normalize Hm @le_S_S >(times_n_1 a) in ⊢ (?%?); >commutative_times + @monotonic_lt_times_l // + |@le_S_S // + ] + |cut (pred (S (2*a)) = 2*a) [//] #Spred >Spred + cut (pred (2*(S a)) = S (2 * a)) [normalize //] #Spred1 >Spred1 + cut (2*(S a) = S(S(2*a))) [normalize (commutative_times 2) in ⊢ (???%); >times2 >minus_Sn_m [%] + @le_S_S >(times_n_1 2) in ⊢ (?%?); @monotonic_le_times_r @Ha + ] #Hcut >Hcut + commutative_times in ⊢ (? (? % ?) ?); + >commutative_times in ⊢ (? (? (? % ?) ?) ?); + >associative_times @monotonic_le_times_r + plus_minus_commutative + [normalize >(plus_n_O (a+(a+0))) in ⊢ (?(?(??%)?)?); @le_n + |@le_S_S >(times_n_1 2) in ⊢ (?%?); @monotonic_le_times_r @Ha + ] + ] + ] + |@False_ind Hm in ⊢ (?%?); @(transitive_le … (le_A_exp ?)) + @(transitive_le ? (2\sup(pred(2*a))*(2\sup((2*a)-3)))) + [@monotonic_le_times_r @Hind >Hm >(times_n_1 a) in ⊢ (?%?); + >commutative_times @(monotonic_lt_times_l … (le_n ?)) + @(transitive_lt ? 3) + [@lt_O_S |@(le_times_to_le 2) [@lt_O_S |commutative_times Hm normalize Hm @le_S_S + >(times_n_1 a) in ⊢ (?%?); + >commutative_times @(monotonic_lt_times_l … (le_n ?)) + @(transitive_lt ? 3) + [@lt_O_S |@(le_times_to_le 2) [@lt_O_S |@le_S_S_to_le times2 (times_n_O O) in ⊢ (?%?); @lt_times [@lt_O_S|//] + |normalize in ⊢ (??(??%)); < plus_n_O >exp_plus_times + @le_times [2://] elim posn [//] + #m #le1m #Hind whd in ⊢ (??%); >commutative_times in ⊢ (??%); + @monotonic_le_times_r @(transitive_le … Hind) + >(times_n_1 m) in ⊢ (?%?); >commutative_times + @(monotonic_lt_times_l … (le_n ?)) @le1m + ] + |@le_times_to_le_div2 + [>(times_n_O O) in ⊢ (?%?); @lt_times [@lt_O_S|//] + |@(transitive_le ? ((B (2*n)*(2*n)))) + [commutative_times @le_exp_Al + cases (le_to_or_lt_eq ? ? (le_O_n (n/2))) [//] + #Heq @False_ind @(absurd ?? (lt_to_not_le ?? lt1n)) + >(div_mod n 2) (div_mod n 2) in ⊢ (??%); @le_plus_n_r + ] +qed. + +theorem eq_sigma_pi_SO_n: ∀n.∑_{i < n} 1 = n. +#n elim n // +qed. + +theorem leA_prim: ∀n. + exp n (prim n) \le A n * ∏_{p < S n | primeb p} p. +#n <(exp_sigma (S n) n primeb) exp_Sn @monotonic_le_times_r @(transitive_le ? (A (2*n))) + [@le_B_A |@le_Al] + ] +qed. + +theorem le_exp_prim4l: ∀n. O < n → + exp 2 (S(4*n)) ≤ exp (4*n) (S(prim (4*n))). +#n #posn @(transitive_le ? (2*(4*n*(B (4*n))))) + [>exp_Sn @monotonic_le_times_r + cut (4*n = 2*(2*n)) [Hcut @le_exp_B @lt_to_le whd >(times_n_1 2) in ⊢ (?%?); + @monotonic_le_times_r // + |>exp_Sn commutative_times in ⊢ (?(?%?)?); + >associative_times @monotonic_le_times_r @(transitive_le ? (A (4*n))) + [@le_B_A4 // |@le_Al] + ] +qed. + +theorem le_priml: ∀n. O < n → + 2*n ≤ (S (log 2 (2*n)))*S(prim (2*n)). +#n #posn <(eq_log_exp 2 (2*n) ?) in ⊢ (?%?); + [@(transitive_le ? ((log 2) (exp (2*n) (S(prim (2*n)))))) + [@le_log [@le_n |@le_exp_priml //] + |>commutative_times in ⊢ (??%); @log_exp1 @le_n + ] + |@le_n + ] +qed. + +theorem le_exp_primr: ∀n. + exp n (prim n) ≤ exp 2 (2*(2*n-3)). +#n @(transitive_le ? (exp (A n) 2)) + [>exp_Sn >exp_Sn whd in match (exp ? 0); commutative_times commutative_times @log_exp2 + [@le_n |@lt_to_le //] + |<(eq_log_exp 2 (2*(2*n-3))) in ⊢ (??%); + [@le_log [@le_n |@le_exp_primr] + |@le_n + ] + ] + ] +qed. + +theorem le_priml1: ∀n. O < n → + 2*n/((log 2 n)+2) - 1 ≤ prim (2*n). +#n #posn @le_plus_to_minus @le_times_to_le_div2 + [>commutative_plus @lt_O_S + |>commutative_times in ⊢ (??%); 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/matita/matita/lib/arithmetics/factorial.ma b/matita/matita/lib/arithmetics/factorial.ma index a95eaaef1..fc2320a94 100644 --- a/matita/matita/lib/arithmetics/factorial.ma +++ b/matita/matita/lib/arithmetics/factorial.ma @@ -15,11 +15,14 @@ let rec fact n ≝ match n with [ O ⇒ 1 | S m ⇒ fact m * S m]. - + interpretation "factorial" 'fact n = (fact n). +lemma factS: ∀n. (S n)! = (S n)*n!. +#n >commutative_times // qed. + theorem le_1_fact : ∀n. 1 ≤ n!. -#n (elim n) normalize /2/ +#n (elim n) normalize /2 by lt_minus_to_plus/ qed. theorem le_2_fact : ∀n. 1 < n → 2 ≤ n!. @@ -38,7 +41,7 @@ theorem lt_n_fact_n: ∀n. 2 < n → n < n!. #n (cases n) [#H @False_ind /2/ |#m #lt2 normalize @(lt_to_le_to_lt ? (2*(S m))) // - @le_times // @le_2_fact /2/ + @le_times // @le_2_fact /2 by lt_plus_to_lt_l/ qed. (* approximations *) @@ -79,118 +82,64 @@ cut (2^(2*(S n)) = 2^(2*n)*2*2) [>H //] #H1 >H1 [@lt_to_le_to_lt_times //|>H // | //] ] qed. - -(* a slightly better result -theorem fact3: \forall n.O < n \to -(exp 2 (2*n))*(exp (fact n) 2) \le 2*n*fact (2*n). -intros. -elim H - [simplify.apply le_n - |rewrite > times_SSO. - rewrite > factS. - rewrite < times_exp. - change in ⊢ (? (? % ?) ?) with ((S(S O))*((S(S O))*(exp (S(S O)) ((S(S O))*n1)))). - rewrite > assoc_times. - rewrite > assoc_times in ⊢ (? (? ? %) ?). - rewrite < assoc_times in ⊢ (? (? ? (? ? %)) ?). - rewrite < sym_times in ⊢ (? (? ? (? ? (? % ?))) ?). - rewrite > assoc_times in ⊢ (? (? ? (? ? %)) ?). - apply (trans_le ? (((S(S O))*((S(S O))*((S n1)\sup((S(S O)))*((S(S O))*n1*((S(S O))*n1)!)))))) - [apply le_times_r. - apply le_times_r. - apply le_times_r. - assumption - |rewrite > factS. - rewrite > factS. - rewrite < times_SSO. - rewrite > assoc_times in ⊢ (? ? %). - apply le_times_r. - rewrite < assoc_times. - change in ⊢ (? (? (? ? %) ?) ?) with ((S n1)*((S n1)*(S O))). - rewrite < assoc_times in ⊢ (? (? % ?) ?). - rewrite < times_n_SO. - rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?). - rewrite < assoc_times in ⊢ (? ? %). - rewrite < assoc_times in ⊢ (? ? (? % ?)). - apply le_times_r. - apply le_times_l. - apply le_S.apply le_n + +(* a sligtly better result *) +theorem exp_to_fact2: ∀n.O < n → + (exp 2 (2*n))*(exp (fact n) 2) \le 2*n*fact (2*n). +#n #posn elim posn + [@le_n + |#m #le1m #Hind + cut (2*(S m) = S(S (2*m))) [normalize //] #H2 >H2 in ⊢ (?%?); + >factS (commutative_times ? 2) >associative_times + >associative_times in ⊢ (??%); @monotonic_le_times_r + whd in match (exp 2 (S ?)); >(commutative_times ? 2) >associative_times + @(transitive_le ? (2*((2*m*(2*m)!)*(S m)^2))) + [@le_times [//] >commutative_times in ⊢ (?(??%)?); exp_2 commutative_times in ⊢ (??%); + @le_times [2:@le_n] >H2 >factS >commutative_times factS in \vdash (? % ?). -rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash(? % ?). -rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?). -rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?). -rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?). -apply le_times_l. -apply leb_true_to_le.reflexivity. -qed. +theorem le_fact_10: fact (2*5) ≤ (exp 2 ((2*5)-2))*(fact 5)*(fact 5). +>factS in ⊢ (?%?); >factS in ⊢ (?%?); factS in ⊢ (?%?); factS in ⊢ (?%?); factS in ⊢ (?%?); assoc_times. -rewrite > assoc_times. -apply eq_f. -rewrite < assoc_times. -rewrite < assoc_times. -rewrite > sym_times in \vdash (? ? (? % ?) ?). -reflexivity. +theorem ab_times_cd: ∀a,b,c,d.(a*b)*(c*d)=(a*c)*(b*d). +// qed. (* an even better result *) -theorem lt_SSSSO_to_fact: \forall n.4 times_SSO. - change in \vdash (? ? (? (? (? ? %) ?) ?)) with (2*n1 - O); - rewrite < minus_n_O. - rewrite > factS. - rewrite > factS. - rewrite < assoc_times. - rewrite > factS. - apply (trans_le ? ((2*(S n1))*(2*(S n1))*(fact (2*n1)))) - [apply le_times_l. - rewrite > times_SSO. - apply le_times_r. - apply le_n_Sn - |apply (trans_le ? (2*S n1*(2*S n1)*(2\sup(2*n1-2)*n1!*n1!))) - [apply le_times_r.assumption - |rewrite > assoc_times. - rewrite > ab_times_cd in \vdash (? (? ? %) ?). - rewrite < assoc_times. - apply le_times_l. - rewrite < assoc_times in \vdash (? (? ? %) ?). - rewrite > ab_times_cd. - apply le_times_l. - rewrite < exp_S. - rewrite < exp_S. - apply le_exp - [apply lt_O_S - |rewrite > eq_minus_S_pred. - rewrite < S_pred - [rewrite > eq_minus_S_pred. - rewrite < S_pred - [rewrite < minus_n_O. - apply le_n - |elim H1;simplify - [apply lt_O_S - |apply lt_O_S - ] - ] - |elim H1;simplify - [apply lt_O_S - |rewrite < plus_n_Sm. - rewrite < minus_n_O. - apply lt_O_S - ] - ] +theorem lt_4_to_fact: ∀n.4H2 + whd in match (minus (S(S ?)) 2); factS >factS factS + @(transitive_le ? ((2*(S m))*(2*(S m))*(fact (2*m)))) + [@le_times [2:@le_n] >H2 @le_times // + |@(transitive_le ? (2*S m*(2*S m)*(2\sup(2*m-2)*m!*m!))) + [@monotonic_le_times_r // + |>associative_times >ab_times_cd in ⊢ (?(??%)?); + ab_times_cd @le_times [2:@le_n] >commutative_times + >(commutative_times 2) @(le_exp (S(S ((2*m)-2)))) [//] + >eq_minus_S_pred >S_pred + [>eq_minus_S_pred >S_pred [HfS + [%1 %{n1} /2/ + |%2 #i #lei + cases (le_to_or_lt_eq ?? lei) #Hi + [@H @le_S_S_to_le @Hi | destruct (Hi) //] + ] + ] + ] +qed. + +theorem exists_max_forall_false:∀f,n. +((∃i. i < n ∧ f i = true) ∧ (f (max n f) = true))∨ +((∀i. i < n → f i = false) ∧ (max n f) = O). +#f #n +cases (exists_forall_lt f n) + [#H %1 % // @(f_max_true f n) @H + |#H %2 % [@H | @max_not_exists @H + ] +qed. + (* minimization *) (* min k b f is the minimun i, b ≤ i < b + k s.t. f i; @@ -237,7 +263,7 @@ lemma min_exists: ∀f.∀t,m. m < t → f m = true → [#b #lebm #ismin #eqtb @False_ind @(absurd … lebm) false_min /2/ @Hind // + [#ltbm >false_min /2 by le_n/ @Hind // [#i #H #H1 @ismin /2/ | >eqt normalize //] |#eqbm >true_min // ]