X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fsieve.ma;h=3f6775f605958d66c8407aa7792a255b93c49bab;hb=e189bde1e0a562e8689ff41d55d392431609e749;hp=6b428d578c1131b716086dc0c66a8a9952970717;hpb=2490d1bf464e276c581ca7b0b7956df2b0f7a490;p=helm.git diff --git a/helm/software/matita/library/nat/sieve.ma b/helm/software/matita/library/nat/sieve.ma index 6b428d578..3f6775f60 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 @@ -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))