From 9edc9828ff3c3d074ccc5547a53eadf092c186d8 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 17 Dec 2007 12:07:27 +0000 Subject: [PATCH] A few more lemmas. --- helm/software/matita/library/nat/chebyshev.ma | 10 +- .../software/matita/library/nat/iteration2.ma | 180 +++++++++++++++++- .../software/matita/library/nat/map_iter_p.ma | 42 ---- helm/software/matita/library/nat/minus.ma | 41 ++++ helm/software/matita/library/nat/neper.ma | 80 ++++++-- 5 files changed, 296 insertions(+), 57 deletions(-) diff --git a/helm/software/matita/library/nat/chebyshev.ma b/helm/software/matita/library/nat/chebyshev.ma index fa935be03..2a3695e8e 100644 --- a/helm/software/matita/library/nat/chebyshev.ma +++ b/helm/software/matita/library/nat/chebyshev.ma @@ -22,6 +22,7 @@ include "nat/factorial2.ma". definition prim: nat \to nat \def \lambda n. sigma_p (S n) primeb (\lambda p.(S O)). +(* This is chebishev psi funcion *) definition A: nat \to nat \def \lambda n. pi_p (S n) primeb (\lambda p.exp p (log p n)). @@ -79,6 +80,7 @@ elim (le_to_or_lt_eq ? ? (le_O_n n)) ] qed. +(* an equivalent formulation for psi *) definition A': nat \to nat \def \lambda n. pi_p (S n) primeb (\lambda p.(pi_p (log p n) (\lambda i.true) (\lambda i.p))). @@ -327,7 +329,8 @@ intro.elim q ] ] qed. - + +(* factorization of n into primes *) theorem pi_p_primeb_divides_b: \forall n. O < n \to n = pi_p (S n) (\lambda i.primeb i \land divides_b i n) (\lambda p.exp p (ord n p)). intros. @@ -505,6 +508,7 @@ apply eq_pi_p1 ] qed. +(* the factorial function *) theorem eq_fact_pi_p:\forall n. fact n = pi_p (S n) (\lambda i.leb (S O) i) (\lambda i.i). intro.elim n @@ -590,6 +594,7 @@ apply (div_mod_spec_to_eq n q ? (n \mod q) ? (n \mod q)) ] qed. +(* still another characterization of the factorial *) theorem fact_pi_p: \forall n. fact n = pi_p (S n) primeb (\lambda p.(pi_p (log p n) @@ -1161,8 +1166,7 @@ rewrite > eq_A_SSO_n assumption |cut (i\sup(S i1)≤(S(S O))*n) [apply div_mod_spec_intro - [alias id "lt_plus_to_lt_minus" = "cic:/matita/nat/map_iter_p.ma/lt_plus_to_lt_minus.con". - apply lt_plus_to_lt_minus + [apply lt_plus_to_lt_minus [assumption |simplify in ⊢ (? % ?). rewrite < plus_n_O. diff --git a/helm/software/matita/library/nat/iteration2.ma b/helm/software/matita/library/nat/iteration2.ma index c5236ff4a..6dbbfd572 100644 --- a/helm/software/matita/library/nat/iteration2.ma +++ b/helm/software/matita/library/nat/iteration2.ma @@ -107,6 +107,84 @@ apply (false_to_eq_iter_p_gen); assumption. qed. +theorem or_false_to_eq_sigma_p: +\forall n,m:nat.\forall p:nat \to bool. +\forall g: nat \to nat. +n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false \lor g i = O) +\to sigma_p m p g = sigma_p n p g. +intros. +unfold sigma_p. +apply or_false_eq_baseA_to_eq_iter_p_gen + [intros.reflexivity + |assumption + |assumption + ] +qed. + +theorem bool_to_nat_to_eq_sigma_p: +\forall n:nat.\forall p1,p2:nat \to bool. +\forall g1,g2: nat \to nat. +(\forall i:nat. +bool_to_nat (p1 i)*(g1 i) = bool_to_nat (p2 i)*(g2 i)) +\to sigma_p n p1 g1 = sigma_p n p2 g2. +intros.elim n + [reflexivity + |generalize in match (H n1). + apply (bool_elim ? (p1 n1));intro + [apply (bool_elim ? (p2 n1));intros + [rewrite > true_to_sigma_p_Sn + [rewrite > true_to_sigma_p_Sn + [apply eq_f2 + [simplify in H4. + rewrite > plus_n_O. + rewrite > plus_n_O in ⊢ (? ? ? %). + assumption + |assumption + ] + |assumption + ] + |assumption + ] + |rewrite > true_to_sigma_p_Sn + [rewrite > false_to_sigma_p_Sn + [change in ⊢ (? ? ? %) with (O + sigma_p n1 p2 g2). + apply eq_f2 + [simplify in H4. + rewrite > plus_n_O. + assumption + |assumption + ] + |assumption + ] + |assumption + ] + ] + |apply (bool_elim ? (p2 n1));intros + [rewrite > false_to_sigma_p_Sn + [rewrite > true_to_sigma_p_Sn + [change in ⊢ (? ? % ?) with (O + sigma_p n1 p1 g1). + apply eq_f2 + [simplify in H4. + rewrite < plus_n_O in H4. + assumption + |assumption + ] + |assumption + ] + |assumption + ] + |rewrite > false_to_sigma_p_Sn + [rewrite > false_to_sigma_p_Sn + [assumption + |assumption + ] + |assumption + ] + ] + ] + ] +qed. + theorem sigma_p2 : \forall n,m:nat. \forall p1,p2:nat \to bool. @@ -240,6 +318,90 @@ elim n ] qed. +(* a slightly more general result *) +theorem le_sigma_p1: +\forall n:nat. \forall p1,p2:nat \to bool. \forall g1,g2:nat \to nat. +(\forall i. i < n \to +bool_to_nat (p1 i)*(g1 i) \le bool_to_nat (p2 i)*g2 i) \to +sigma_p n p1 g1 \le sigma_p n p2 g2. +intros. +generalize in match H. +elim n + [apply le_n. + |apply (bool_elim ? (p1 n1));intros + [apply (bool_elim ? (p2 n1));intros + [rewrite > true_to_sigma_p_Sn + [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %) + [apply le_plus + [lapply (H2 n1) as H5 + [rewrite > H3 in H5. + rewrite > H4 in H5. + simplify in H5. + rewrite < plus_n_O in H5. + rewrite < plus_n_O in H5. + assumption + |apply le_S_S.apply le_n + ] + |apply H1.intros. + apply H2.apply le_S.assumption + ] + |assumption + ] + |assumption + ] + |rewrite > true_to_sigma_p_Sn + [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %) + [change in ⊢ (? ? %) with (O + sigma_p n1 p2 g2). + apply le_plus + [lapply (H2 n1) as H5 + [rewrite > H3 in H5. + rewrite > H4 in H5. + simplify in H5. + rewrite < plus_n_O in H5. + assumption + |apply le_S_S.apply le_n + ] + |apply H1.intros. + apply H2.apply le_S.assumption + ] + |assumption + ] + |assumption + ] + ] + |apply (bool_elim ? (p2 n1));intros + [rewrite > false_to_sigma_p_Sn + [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %) + [change in ⊢ (? % ?) with (O + sigma_p n1 p1 g1). + apply le_plus + [lapply (H2 n1) as H5 + [rewrite > H3 in H5. + rewrite > H4 in H5. + simplify in H5. + rewrite < plus_n_O in H5. + assumption + |apply le_S_S.apply le_n + ] + |apply H1.intros. + apply H2.apply le_S.assumption + ] + |assumption + ] + |assumption + ] + |rewrite > false_to_sigma_p_Sn + [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %) + [apply H1.intros. + apply H2.apply le_S.assumption + |assumption + ] + |assumption + ] + ] + ] + ] +qed. + theorem lt_sigma_p: \forall n:nat. \forall p:nat \to bool. \forall g1,g2:nat \to nat. (\forall i. i < n \to p i = true \to g1 i \le g2 i ) \to @@ -539,7 +701,6 @@ rewrite > sym_times. apply eq_sigma_p_sigma_p_times1. qed. - theorem sigma_p_times:\forall n,m:nat. \forall f,f1,f2:nat \to bool. \forall g:nat \to nat \to nat. @@ -801,4 +962,21 @@ apply(iter_p_gen_2_eq nat O plus ? ? ? g h11 h12 h21 h22 n1 m1 n2 m2 p11 p21 p12 | assumption | assumption ] +qed. + +theorem sigma_p_sigma_p: +\forall g: nat \to nat \to nat. +\forall n,m. +\forall p11,p21:nat \to bool. +\forall p12,p22:nat \to nat \to bool. +(\forall x,y. x < n \to y < m \to + (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to +sigma_p n p11 (\lambda x:nat.sigma_p m (p12 x) (\lambda y. g x y)) = +sigma_p m p21 (\lambda y:nat.sigma_p n (p22 y) (\lambda x. g x y)). +intros. +unfold sigma_p.unfold sigma_p. +apply (iter_p_gen_iter_p_gen ? ? ? sym_plus assoc_plus) + [intros.apply sym_eq.apply plus_n_O. + |assumption + ] qed. \ No newline at end of file diff --git a/helm/software/matita/library/nat/map_iter_p.ma b/helm/software/matita/library/nat/map_iter_p.ma index ca5031f22..080f9a45f 100644 --- a/helm/software/matita/library/nat/map_iter_p.ma +++ b/helm/software/matita/library/nat/map_iter_p.ma @@ -578,48 +578,6 @@ elim n ] qed. -(* tutti d spostare *) -theorem lt_minus_to_lt_plus: -\forall n,m,p. n - m < p \to n < m + p. -intros 2. -apply (nat_elim2 ? ? ? ? n m) - [simplify.intros.autobatch. - |intros 2.rewrite < minus_n_O. - intro.assumption - |intros. - simplify. - cut (n1 < m1+p) - [autobatch - |apply H. - apply H1 - ] - ] -qed. - -theorem lt_plus_to_lt_minus: -\forall n,m,p. m \le n \to n < m + p \to n - m < p. -intros 2. -apply (nat_elim2 ? ? ? ? n m) - [simplify.intros 3. - apply (le_n_O_elim ? H). - simplify.intros.assumption - |simplify.intros.assumption. - |intros. - simplify. - apply H - [apply le_S_S_to_le.assumption - |apply le_S_S_to_le.apply H2 - ] - ] -qed. - -theorem minus_m_minus_mn: \forall n,m. n\le m \to n=m-(m-n). -intros. -apply sym_eq. -apply plus_to_minus. -autobatch. -qed. - theorem eq_map_iter_p_transpose2: \forall p.\forall f.associative nat f \to symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. O < k \to k \le n \to (p (S n) = true) \to (p k) = true diff --git a/helm/software/matita/library/nat/minus.ma b/helm/software/matita/library/nat/minus.ma index 11585f206..339e2262c 100644 --- a/helm/software/matita/library/nat/minus.ma +++ b/helm/software/matita/library/nat/minus.ma @@ -296,6 +296,47 @@ apply (lt_minus_to_plus O a b). assumption. qed. +theorem lt_minus_to_lt_plus: +\forall n,m,p. n - m < p \to n < m + p. +intros 2. +apply (nat_elim2 ? ? ? ? n m) + [simplify.intros.autobatch. + |intros 2.rewrite < minus_n_O. + intro.assumption + |intros. + simplify. + cut (n1 < m1+p) + [autobatch + |apply H. + apply H1 + ] + ] +qed. + +theorem lt_plus_to_lt_minus: +\forall n,m,p. m \le n \to n < m + p \to n - m < p. +intros 2. +apply (nat_elim2 ? ? ? ? n m) + [simplify.intros 3. + apply (le_n_O_elim ? H). + simplify.intros.assumption + |simplify.intros.assumption. + |intros. + simplify. + apply H + [apply le_S_S_to_le.assumption + |apply le_S_S_to_le.apply H2 + ] + ] +qed. + +theorem minus_m_minus_mn: \forall n,m. n\le m \to n=m-(m-n). +intros. +apply sym_eq. +apply plus_to_minus. +autobatch. +qed. + theorem distributive_times_minus: distributive nat times minus. unfold distributive. intros. diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma index 890d33c66..df70accbc 100644 --- a/helm/software/matita/library/nat/neper.ma +++ b/helm/software/matita/library/nat/neper.ma @@ -408,7 +408,7 @@ apply le_times_to_le_div ] qed. -theorem sigma_p_log_div: \forall n,b. S O < b \to +theorem sigma_p_log_div1: \forall n,b. S O < b \to sigma_p (S n) (\lambda p.(primeb p \land (leb (S n) (p*p)))) (\lambda p.(log b (n/p))) \le sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\lambda p.(sigma_p n (\lambda i.leb p i) (\lambda i.S((n!/i)*S(log b (S(S(S O)))))))/n! ). @@ -425,14 +425,14 @@ apply le_log_div_sigma_p ] qed. -theorem sigma_p_log_div1: \forall n,b. S O < b \to +theorem sigma_p_log_div2: \forall n,b. S O < b \to sigma_p (S n) (\lambda p.(primeb p \land (leb (S n) (p*p)))) (\lambda p.(log b (n/p))) \le (sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\lambda p.(sigma_p n (\lambda i.leb p i) (\lambda i.S((n!/i)))))*S(log b (S(S(S O))))/n!). intros. apply (trans_le ? (sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\lambda p.(sigma_p n (\lambda i.leb p i) (\lambda i.S((n!/i)*S(log b (S(S(S O)))))))/n! ))) - [apply sigma_P_log_div.assumption + [apply sigma_p_log_div1.assumption |apply le_times_to_le_div [apply lt_O_fact |rewrite > distributive_times_plus_sigma_p. @@ -460,18 +460,76 @@ apply (trans_le ? (sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\ ] ] qed. - -(* + theorem sigma_p_log_div: \forall n,b. S O < b \to sigma_p (S n) (\lambda p.(primeb p \land (leb (S n) (p*p)))) (\lambda p.(log b (n/p))) -\le (sigma_p (S n) (\lambda i.leb (S n) (i*i)) (\lambda i.(prim i)*n!/i))*S(log b (S(S(S O)))/n! -). +\le (sigma_p n (\lambda i.leb (S n) (i*i)) (\lambda i.(prim i)*S(n!/i)))*S(log b (S(S(S O))))/n! +. intros. apply (trans_le ? (sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\lambda p.(sigma_p n (\lambda i.leb p i) (\lambda i.S((n!/i)))))*S(log b (S(S(S O))))/n!)) - [apply sigma_p_log_div1 - |unfold prim. -*) - + [apply sigma_p_log_div2.assumption + |apply monotonic_div + [apply lt_O_fact + |apply le_times_l. + unfold prim. + cut + (sigma_p (S n) (λp:nat.primeb p∧leb (S n) (p*p)) + (λp:nat.sigma_p n (λi:nat.leb p i) (λi:nat.S (n!/i))) + = sigma_p n (λi:nat.leb (S n) (i*i)) + (λi:nat.sigma_p (S n) (\lambda p.primeb p \land leb (S n) (p*p) \land leb p i) (λp:nat.S (n!/i)))) + [rewrite > Hcut. + apply le_sigma_p.intros. + rewrite < sym_times. + rewrite > distributive_times_plus_sigma_p. + rewrite < times_n_SO. + cut + (sigma_p (S n) (λp:nat.primeb p∧leb (S n) (p*p) \land leb p i) (λp:nat.S (n!/i)) + = sigma_p (S i) (\lambda p.primeb p \land leb (S n) (p*p) \land leb p i) (λp:nat.S (n!/i))) + [rewrite > Hcut1. + apply le_sigma_p1.intros. + rewrite < andb_sym. + rewrite < andb_sym in ⊢ (? (? (? (? ? %)) ?) ?). + apply (bool_elim ? (leb i1 i));intros + [apply (bool_elim ? (leb (S n) (i1*i1)));intros + [apply le_n + |apply le_O_n + ] + |apply le_O_n + ] + |apply or_false_to_eq_sigma_p + [apply le_S.assumption + |intros. + left.rewrite > (lt_to_leb_false i1 i) + [rewrite > andb_sym.reflexivity + |assumption + ] + ] + ] + |apply sigma_p_sigma_p.intros. + apply (bool_elim ? (leb x y));intros + [apply (bool_elim ? (leb (S n) (x*x)));intros + [rewrite > le_to_leb_true in ⊢ (? ? ? (? % ?)) + [reflexivity + |apply (trans_le ? (x*x)) + [apply leb_true_to_le.assumption + |apply le_times;apply leb_true_to_le;assumption + ] + ] + |rewrite < andb_sym in ⊢ (? ? (? % ?) ?). + rewrite < andb_sym in ⊢ (? ? ? (? ? (? % ?))). + rewrite < andb_sym in ⊢ (? ? ? %). + reflexivity + ] + |rewrite < andb_sym. + rewrite > andb_assoc in ⊢ (? ? ? %). + rewrite < andb_sym in ⊢ (? ? ? (? % ?)). + reflexivity + ] + ] + ] + ] +qed. + (* theorem le_log_exp_Sn_log_exp_n: \forall n,m,a,p. O < m \to S O < p \to divides n m \to -- 2.39.2