From 16f4598e9d2ada0b471e7d5cbe84295c7e34c27c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 6 Jun 2008 10:07:22 +0000 Subject: [PATCH] sieve.ma now depends only on primes.ma --- helm/software/matita/library/depends | 2 +- helm/software/matita/library/nat/sieve.ma | 47 +++++++++++++++-------- 2 files changed, 31 insertions(+), 18 deletions(-) diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends index 8250ca244..943790600 100644 --- a/helm/software/matita/library/depends +++ b/helm/software/matita/library/depends @@ -81,4 +81,4 @@ nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma nat/chebyshev.ma nat/factorial2.ma nat/factorization.ma nat/log.ma nat/pi_p.ma nat/log.ma datatypes/constructors.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/minimization.ma nat/primes.ma nat/relevant_equations.ma nat/times.ma nat/plus.ma -nat/sieve.ma list/sort.ma nat/factorization.ma nat/sqrt.ma +nat/sieve.ma list/sort.ma nat/primes.ma diff --git a/helm/software/matita/library/nat/sieve.ma b/helm/software/matita/library/nat/sieve.ma index 6b428d578..3525bc0b2 100644 --- a/helm/software/matita/library/nat/sieve.ma +++ b/helm/software/matita/library/nat/sieve.ma @@ -12,9 +12,8 @@ (* *) (**************************************************************************) -include "nat/sqrt.ma". +include "nat/primes.ma". include "list/sort.ma". -include "nat/factorization.ma". let rec list_n_aux n k \def match n with @@ -78,21 +77,35 @@ intro.elim t 0 [elim H11;assumption |apply in_list_head] |intros;elim (le_to_or_lt_eq ? ? (divides_to_le ? ? ? H9)) - [elim (divides_to_prime_divides ? ? H10 H11 H9);elim H12; - elim H13;clear H13 H12;elim (H3 a);elim H12 - [clear H13 H12;elim (H18 ? ? H14);elim (H2 a1); - apply H13 - [assumption - |elim H17;apply (trans_le ? ? ? ? H20); - apply (trans_le ? ? ? H15); - apply lt_to_le;assumption - |intros;apply (trans_le ? (S m)) - [apply le_S_S;assumption - |apply (trans_le ? ? ? H11); - elim (in_list_cons_case ? ? ? ? H19) - [rewrite > H20;apply le_n - |apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);assumption]]] - |apply in_list_head] + [cut (1 < a) as Lt1a; [2: apply (trans_lt ??? H10 H11)] + letin a1 ≝ (smallest_factor a); + lapply (divides_smallest_factor_n a) as H14; + [2: apply (trans_lt ? (S O) ? ? Lt1a); + apply lt_O_S + | fold unfold a1 a1 in H14; + lapply (prime_smallest_factor_n a Lt1a) as H16; + fold unfold a1 a1 in H16; + cut (a1 ≤ m) as H15; + [2: generalize in match (leb_to_Prop a1 m); + elim (leb a1 m); simplify in H12; + [ assumption + | elim (lt_smallest_factor_to_not_divides a m Lt1a H10 ? H9); + apply (not_le_to_lt ?? H12)] + | clearbody a1; + elim (H3 a);elim H12 + [clear H13 H12;elim (H18 ? ? H14);elim (H2 a1); + apply H13 + [assumption + |elim H17;apply (trans_le ? ? ? ? H20); + apply (trans_le ? ? ? H15); + apply lt_to_le;assumption + |intros;apply (trans_le ? (S m)) + [apply le_S_S;assumption + |apply (trans_le ? ? ? H11); + elim (in_list_cons_case ? ? ? ? H19) + [rewrite > H20;apply le_n + |apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);assumption]]] + |apply in_list_head]]] |elim (H3 a);elim H11 [elim H13;apply lt_to_le;assumption |apply in_list_head] -- 2.39.2