From: Andrea Asperti Date: Fri, 8 Feb 2008 17:04:43 +0000 (+0000) Subject: progress. X-Git-Tag: make_still_working~5621 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d74bdbdea0586eaa764c53a22e2c660d5367d0d5;p=helm.git progress. --- diff --git a/helm/software/matita/library/nat/binomial.ma b/helm/software/matita/library/nat/binomial.ma index 950576148..1a3410320 100644 --- a/helm/software/matita/library/nat/binomial.ma +++ b/helm/software/matita/library/nat/binomial.ma @@ -141,6 +141,28 @@ rewrite > (lt_to_lt_to_eq_div_div_times_times ? ? (S k)) in ⊢ (? ? ? (? % ?)) apply lt_times;apply lt_O_fact] qed. +theorem lt_O_bc: \forall n,m. m \le n \to O < bc n m. +intro.elim n + [apply (le_n_O_elim ? H). + simplify.apply le_n + |elim (le_to_or_lt_eq ? ? H1) + [generalize in match H2.cases m;intro + [rewrite > bc_n_O.apply le_n + |rewrite > bc1 + [apply (trans_le ? (bc n1 n2)) + [apply H.apply le_S_S_to_le.apply lt_to_le.assumption + |apply le_plus_n_r + ] + |apply le_S_S_to_le.assumption + ] + ] + |rewrite > H2. + rewrite > bc_n_n. + apply le_n + ] + ] +qed. + theorem exp_plus_sigma_p:\forall a,b,n. exp (a+b) n = sigma_p (S n) (\lambda k.true) (\lambda k.(bc n k)*(exp a (n-k))*(exp b k)). diff --git a/helm/software/matita/library/nat/chebyshev_teta.ma b/helm/software/matita/library/nat/chebyshev_teta.ma index bb0f4e838..bdec36391 100644 --- a/helm/software/matita/library/nat/chebyshev_teta.ma +++ b/helm/software/matita/library/nat/chebyshev_teta.ma @@ -22,7 +22,24 @@ include "nat/pi_p.ma". definition teta: nat \to nat \def \lambda n. pi_p (S n) primeb (\lambda p.p). -definition M \def \lambda m.bc (2*m+1) m. +theorem lt_O_teta: \forall n. O < teta n. +intros.elim n + [apply le_n + |unfold teta.apply (bool_elim ? (primeb (S n1)));intro + [rewrite > true_to_pi_p_Sn + [rewrite > (times_n_O O). + apply lt_times + [apply lt_O_S + |assumption + ] + |assumption + ] + |rewrite > false_to_pi_p_Sn;assumption + ] + ] +qed. + +definition M \def \lambda m.bc (S(2*m)) m. theorem lt_M: \forall m. O < m \to M m < exp 2 (2*m). intros. @@ -43,8 +60,8 @@ apply (lt_times_to_lt 2) rewrite < times_n_SO.rewrite < times_n_SO. rewrite < times_n_SO.rewrite < times_n_SO. apply le_plus - [unfold M.rewrite < plus_n_SO.apply le_n - |apply le_plus_l.unfold M.rewrite < plus_n_SO. + [unfold M.apply le_n + |apply le_plus_l.unfold M. change in \vdash (? ? %) with (fact (S(2*m))/(fact (S m)*(fact ((2*m)-m)))). simplify in \vdash (? ? (? ? (? ? (? (? % ?))))). rewrite < plus_n_O.rewrite < minus_plus_m_m. @@ -95,10 +112,291 @@ apply (lt_times_to_lt 2) ] ] |intros.rewrite > sym_times in \vdash (? ? ? %). - + rewrite < times_n_SO. + reflexivity + ] + ] + ] +qed. - - simplify in \vdash (? ? %). +theorem divides_fact_to_divides: \forall p,n. prime p \to divides p n! \to +\exists m.O < m \land m \le n \land divides p m. +intros 3.elim n + [apply False_ind.elim H. + apply (lt_to_not_le ? ? H2). + apply divides_to_le[apply le_n|assumption] + |rewrite > factS in H2. + elim (divides_times_to_divides ? ? ? H H2) + [apply (ex_intro ? ? (S n1)).split + [split + [apply lt_O_S + |apply le_n + ] + |assumption + ] + |elim (H1 H3).elim H4.elim H5. + apply (ex_intro ? ? a).split + [split + [assumption + |apply le_S.assumption + ] + |assumption + ] + ] + ] +qed. + +theorem divides_fact_to_le: \forall p,n. prime p \to divides p n! \to +p \le n. +intros. +elim (divides_fact_to_divides p n H H1). +elim H2.elim H3. +apply (trans_le ? a) + [apply divides_to_le;assumption + |assumption + ] +qed. + +theorem prime_to_divides_M: \forall m,p. prime p \to S m < p \to p \le S(2*m) \to +divides p (M m). +intros.unfold M. +elim (bc2 (S(2*m)) m) + [unfold bc.rewrite > H3. + rewrite > sym_times. + rewrite > lt_O_to_div_times + [elim (divides_times_to_divides p (m!*(S (2*m)-m)!) n2) + [apply False_ind. + elim (divides_times_to_divides p (m!) (S (2*m)-m)!) + [apply (lt_to_not_le ? ? (lt_to_le ? ? H1)). + apply divides_fact_to_le;assumption + |apply (lt_to_not_le ? ? H1). + apply divides_fact_to_le + [assumption + |cut (S m = S(2*m)-m) + [rewrite > Hcut.assumption + |simplify in ⊢ (? ? ? (? (? %) ?)). + rewrite < plus_n_O. + change in ⊢ (? ? ? (? % ?)) with (S m + m). + apply minus_plus_m_m + ] + ] + |assumption + |assumption + ] + |assumption + |assumption + |rewrite < H3. + apply divides_fact + [apply prime_to_lt_O.assumption + |assumption + ] + ] + |rewrite > (times_n_O O). + apply lt_times;apply lt_O_fact + ] + |simplify in ⊢ (? ? (? %)). + rewrite < plus_n_O. + change in ⊢ (? ? %) with (S m + m). + apply le_plus_n + ] +qed. +theorem divides_pi_p_M1: \forall m.\forall i. i \le (S(S(2*m))) \to +divides (pi_p i (\lambda p.leb (S(S m)) p \land primeb p)(\lambda p.p)) (M m). +intros 2. +elim i + [simplify.apply (witness ? ? (M m)).rewrite > sym_times.apply times_n_SO + |apply (bool_elim ? (leb (S (S m)) n \land primeb n));intro + [rewrite > true_to_pi_p_Sn + [apply divides_to_divides_times + [apply primeb_true_to_prime. + apply (andb_true_true_r ? ? H2). + |cut (\forall p.prime p \to n \le p \to ¬p∣pi_p n (λp:nat.leb (S (S m)) p∧primeb p) (λp:nat.p)) + [apply Hcut + [apply primeb_true_to_prime. + apply (andb_true_true_r ? ? H2) + |apply le_n + ] + |intros 2. + elim n + [simplify.intro.elim H3.apply (lt_to_not_le ? ? H6). + apply divides_to_le + [apply le_n + |assumption + ] + |apply (bool_elim ? (leb (S (S m)) n1∧primeb n1));intro + [rewrite > true_to_pi_p_Sn + [intro.elim (divides_times_to_divides ? ? ? H3 H7) + [apply (le_to_not_lt ? ? H5). + apply le_S_S. + apply divides_to_le + [apply prime_to_lt_O. + apply primeb_true_to_prime. + apply (andb_true_true_r ? ? H6) + |assumption + ] + |apply H4 + [apply lt_to_le.assumption + |assumption + ] + ] + |assumption + ] + |rewrite > false_to_pi_p_Sn + [apply H4. + apply lt_to_le.assumption + |assumption + ] + ] + ] + ] + |apply prime_to_divides_M + [apply primeb_true_to_prime. + apply (andb_true_true_r ? ? H2) + |apply leb_true_to_le. + apply (andb_true_true ? ? H2) + |apply le_S_S_to_le.assumption + ] + |apply H. + apply lt_to_le. + assumption + ] + |assumption + ] + |rewrite > false_to_pi_p_Sn + [apply H. + apply lt_to_le. + assumption + |assumption + ] + ] + ] +qed. +theorem divides_pi_p_M:\forall m. +divides (pi_p (S(S(2*m))) (\lambda p.leb (S(S m)) p \land primeb p)(\lambda p.p)) (M m). +intros. +apply divides_pi_p_M1. +apply le_n. +qed. +theorem teta_pi_p_teta: \forall m. teta (S (2*m)) +=pi_p (S (S (2*m))) (λp:nat.leb (S (S m)) p∧primeb p) (λp:nat.p)*teta (S m). +intro.unfold teta. +rewrite > (eq_pi_p1 ? (\lambda p.leb p (S m) \land primeb p) ? (\lambda p.p) (S(S m))) + [rewrite < (false_to_eq_pi_p (S(S m)) (S(S(2*m)))) + [generalize in match (S(S(2*m))).intro. + elim n + [simplify.reflexivity + |apply (bool_elim ? (primeb n1));intro + [rewrite > true_to_pi_p_Sn + [apply (bool_elim ? (leb n1 (S m))); intro + [rewrite > false_to_pi_p_Sn + [rewrite > true_to_pi_p_Sn + [rewrite < assoc_times. + rewrite > sym_times in ⊢ (? ? ? (? % ?)). + rewrite > assoc_times. + apply eq_f. + assumption + |apply true_to_true_to_andb_true;assumption + ] + |rewrite > lt_to_leb_false + [reflexivity + |apply le_S_S. + apply leb_true_to_le. + assumption + ] + ] + |rewrite > true_to_pi_p_Sn + [rewrite > false_to_pi_p_Sn + [rewrite > assoc_times. + apply eq_f. + assumption + |rewrite > H2.reflexivity + ] + |rewrite > H1. + rewrite > le_to_leb_true + [reflexivity + |apply not_le_to_lt. + apply leb_false_to_not_le. + assumption + ] + ] + ] + |assumption + ] + |rewrite > false_to_pi_p_Sn + [rewrite > false_to_pi_p_Sn + [rewrite > false_to_pi_p_Sn + [assumption + |rewrite > H1. + rewrite > andb_sym. + reflexivity + ] + |rewrite > H1. + rewrite > andb_sym. + reflexivity + ] + |assumption + ] + ] + ] + |apply le_S_S.apply le_S_S. + apply le_times_n. + apply le_n_Sn + |intros. + rewrite > lt_to_leb_false + [reflexivity + |assumption + ] + ] + |intros. + rewrite > le_to_leb_true + [reflexivity + |apply le_S_S_to_le. + assumption + ] + |intros.reflexivity + ] +qed. + +theorem div_teta_teta: \forall m. +teta (S(2*m))/teta (S m) = pi_p (S(S(2*m))) (\lambda p.leb (S(S m)) p \land primeb p)(\lambda p.p). +intros.apply (div_mod_spec_to_eq ? ? ? ? ? O (div_mod_spec_div_mod ? ? ? )) + [apply lt_O_teta + |apply div_mod_spec_intro + [apply lt_O_teta + |rewrite < plus_n_O. + apply teta_pi_p_teta + ] + ] +qed. + +theorem le_teta_M_teta: \forall m. +teta (S(2*m)) \le (M m)*teta (S m). +intro. +rewrite > teta_pi_p_teta. +apply le_times_l. +apply divides_to_le + [unfold M.apply lt_O_bc.apply lt_to_le. + apply le_S_S.apply le_times_n. + apply le_n_Sn + |apply divides_pi_p_M + ] +qed. + +theorem lt_O_to_le_teta_M_teta: \forall m. O < m\to +teta (S(2*m)) < exp 2 (2*m)*teta (S m). +intros. +apply (le_to_lt_to_lt ? (M m*teta (S m))) + [apply le_teta_M_teta + |apply lt_times_l1 + [apply lt_O_teta + |apply lt_M. + assumption + ] + ] +qed. + + + diff --git a/helm/software/matita/library/nat/gcd.ma b/helm/software/matita/library/nat/gcd.ma index 9bbce8144..0baa86e3c 100644 --- a/helm/software/matita/library/nat/gcd.ma +++ b/helm/software/matita/library/nat/gcd.ma @@ -101,7 +101,6 @@ qed. theorem divides_gcd_nm: \forall n,m. gcd n m \divides m \land gcd n m \divides n. intros. -(*CSC: simplify simplifies too much because of a redex in gcd *) change with (match leb n m with [ true \Rightarrow @@ -594,7 +593,6 @@ intro.apply (nat_case n) qed. theorem symmetric_gcd: symmetric nat gcd. -(*CSC: bug here: unfold symmetric does not work *) change with (\forall n,m:nat. gcd n m = gcd m n). intros. @@ -904,3 +902,35 @@ cut (n \divides p \lor n \ndivides p) ] qed. +(* +theorem divides_to_divides_times1: \forall p,q,n. prime p \to prime q \to p \neq q \to +divides p n \to divides q n \to divides (p*q) n. +intros.elim H3. +rewrite > H5 in H4. +elim (divides_times_to_divides ? ? ? H1 H4) + [elim H.apply False_ind. + apply H2.apply sym_eq.apply H8 + [assumption + |apply prime_to_lt_SO.assumption + ] + |elim H6. + apply (witness ? ? n1). + rewrite > assoc_times. + rewrite < H7.assumption + ] +qed. +*) + +theorem divides_to_divides_times: \forall p,q,n. prime p \to p \ndivides q \to +divides p n \to divides q n \to divides (p*q) n. +intros.elim H3. +rewrite > H4 in H2. +elim (divides_times_to_divides ? ? ? H H2) + [apply False_ind.apply H1.assumption + |elim H5. + apply (witness ? ? n1). + rewrite > sym_times in ⊢ (? ? ? (? % ?)). + rewrite > assoc_times. + rewrite < H6.assumption + ] +qed. \ No newline at end of file