From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 6 Jun 2008 10:07:22 +0000 (+0000)
Subject: sieve.ma now depends only on primes.ma
X-Git-Tag: make_still_working~5077
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=16f4598e9d2ada0b471e7d5cbe84295c7e34c27c;p=helm.git

sieve.ma now depends only on primes.ma
---

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]