apply rule (lem EM) works

[helm.git] / helm / software / matita / library / nat / sieve.ma

diff --git a/helm/software/matita/library/nat/sieve.ma b/helm/software/matita/library/nat/sieve.ma
index 6b428d578c1131b716086dc0c66a8a9952970717..3f6775f605958d66c8407aa7792a255b93c49bab 100644 (file)
--- 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
@@ -51,9 +50,9 @@ lemma sieve_prime : \forall t,k,l2,l1.
             (prime p \to p \leq k \to in_list ? p (sieve_aux l1 l2 t)).
 intro.elim t 0
   [intros;cut (l2 = [])
-     [|generalize in match H2;elim l2
+     [|elim l2 in H2 ⊢ %
         [reflexivity
-        |simplify in H6;elim (not_le_Sn_O ? H6)]]
+        |simplify in H5;elim (not_le_Sn_O ? H5)]]
    simplify;split
      [assumption
      |intro;elim (H p);split;intros
@@ -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]
@@ -203,7 +216,7 @@ definition list_of_primes \def \lambda n.\lambda l.
 lemma in_list_SSO_list_n : \forall n.2 \leq n \to in_list ? 2 (list_n n).
 intros;elim H;simplify
   [apply in_list_head
-  |generalize in match H2;elim H1;simplify;apply in_list_head]
+  |elim H1 in H2 ⊢ %;simplify;apply in_list_head]
 qed.
 
 lemma le_list_n_aux_k_k : \forall n,m,k.in_list ? n (list_n_aux m k) \to
@@ -230,9 +243,9 @@ qed.
 
 lemma le_list_n : \forall n,m.in_list ? n (list_n m) \to n \leq m.
 intros;unfold list_n in H;lapply (le_list_n_aux ? ? ? H);
-simplify in Hletin;generalize in match H;generalize in match Hletin;elim m
-   [simplify in H2;elim (not_in_list_nil ? ? H2)
-   |simplify in H2;assumption]
+simplify in Hletin;elim m in H Hletin ⊢ %
+   [simplify in H;elim (not_in_list_nil ? ? H)
+   |simplify in H;assumption]
 qed.
 
 
@@ -241,23 +254,23 @@ intros 3;elim H 0
   [intros;simplify;rewrite < plus_n_Sm in H2;simplify in H2;
    rewrite < plus_n_O in H2;rewrite < minus_n_O in H2;
    rewrite > (antisymmetric_le k n H1 H2);apply in_list_head
-  |intros 5;simplify;generalize in match H2;elim H3
+  |intros 5;simplify;elim H3 in H2 ⊢ %
      [apply in_list_head
-     |apply in_list_cons;apply H6
+     |apply in_list_cons;apply H5
         [apply le_S_S;assumption
-        |rewrite < plus_n_Sm in H7;apply H7]]]
+        |rewrite < plus_n_Sm in H6;apply H6]]]
 qed.
 
 lemma le_list_n_r : \forall n,m.S O < m \to 2 \leq n \to n \leq m \to in_list ? n (list_n m).
 intros;unfold list_n;apply le_list_n_aux_r
   [elim H;simplify
      [apply lt_O_S
-     |generalize in match H4;elim H3;
+     |elim H3 in H4 ⊢ %;
         [apply lt_O_S
         |simplify in H7;apply le_S;assumption]]
   |assumption
-  |simplify;generalize in match H2;elim H;simplify;assumption]
-qed.  
+  |simplify;elim H in H2 ⊢ %;simplify;assumption]
+qed.
 
 lemma le_length_list_n : \forall n. length ? (list_n n) \leq n.
 intro;cut (\forall n,k.length ? (list_n_aux n k) \leq (S n))