From: Claudio Sacerdoti Coen Date: Thu, 5 Jun 2008 21:16:11 +0000 (+0000) Subject: Eratosthene's sieve factorized out of nat/bertrand.ma. Nothing added not X-Git-Tag: make_still_working~5081 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2490d1bf464e276c581ca7b0b7956df2b0f7a490;p=helm.git Eratosthene's sieve factorized out of nat/bertrand.ma. Nothing added not removed. In theory, sieve.ma ishould not depend on nth_prime.ma and factorization.ma. In practice, a proof requires factorization that, in turn, depends on nth_prime.ma. To be investigated. --- diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends index b274f1b91..8250ca244 100644 --- a/helm/software/matita/library/depends +++ b/helm/software/matita/library/depends @@ -21,7 +21,7 @@ higher_order_defs/ordering.ma logic/equality.ma higher_order_defs/relations.ma logic/connectives.ma Q/q.ma Z/compare.ma Z/plus.ma nat/factorization.ma Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma -Q/times.ma Q/inv.ma Q/q.ma +Q/times.ma Q/inv.ma Q/inv.ma Q/q.ma datatypes/compare.ma datatypes/constructors.ma logic/equality.ma @@ -68,7 +68,7 @@ nat/o.ma nat/binomial.ma nat/sqrt.ma nat/orders.ma logic/connectives.ma higher_order_defs/ordering.ma nat/nat.ma nat/euler_theorem.ma nat/nat.ma nat/map_iter_p.ma nat/totient.ma nat/primes.ma logic/connectives.ma nat/div_and_mod.ma nat/factorial.ma nat/minimization.ma nat/sigma_and_pi.ma -nat/bertrand.ma list/in.ma list/sort.ma nat/chebyshev.ma nat/chebyshev_teta.ma nat/o.ma nat/sqrt.ma +nat/bertrand.ma list/in.ma list/sort.ma nat/chebyshev.ma nat/chebyshev_teta.ma nat/o.ma nat/sieve.ma nat/sqrt.ma nat/chinese_reminder.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma nat/factorial.ma nat/le_arith.ma nat/lt_arith.ma nat/div_and_mod.ma @@ -81,3 +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 diff --git a/helm/software/matita/library/nat/bertrand.ma b/helm/software/matita/library/nat/bertrand.ma index 4d8596b6e..7a0363a58 100644 --- a/helm/software/matita/library/nat/bertrand.ma +++ b/helm/software/matita/library/nat/bertrand.ma @@ -18,6 +18,7 @@ include "nat/chebyshev.ma". include "list/in.ma". include "list/sort.ma". include "nat/o.ma". +include "nat/sieve.ma". let rec list_divides l n \def match l with @@ -33,359 +34,6 @@ definition lprim : nat \to list nat \def | false => aux m1 (n-m1::acc)]] in aux (pred n) []. -let rec list_n_aux n k \def - match n with - [ O => nil nat - | S n1 => k::list_n_aux n1 (S k) ]. - -definition list_n : nat \to list nat \def - \lambda n.list_n_aux (pred n) 2. - -let rec sieve_aux l1 l2 t on t \def - match t with - [ O => l1 - | S t1 => match l2 with - [ nil => l1 - | cons n tl => sieve_aux (n::l1) (filter nat tl (\lambda x.notb (divides_b n x))) t1]]. - -definition sieve : nat \to list nat \def - \lambda m.sieve_aux [] (list_n m) m. - -lemma divides_to_prime_divides : \forall n,m.1 < m \to m < n \to m \divides n \to - \exists p.p \leq m \land prime p \land p \divides n. -intros;apply (ex_intro ? ? (nth_prime (max_prime_factor m)));split - [split - [apply divides_to_le - [apply lt_to_le;assumption - |apply divides_max_prime_factor_n;assumption] - |apply prime_nth_prime;] - |apply (transitive_divides ? ? ? ? H2);apply divides_max_prime_factor_n; - assumption] -qed. - -definition sorted_lt \def sorted ? lt. -definition sorted_gt \def sorted ? gt. - -lemma sieve_prime : \forall t,k,l2,l1. - (\forall p.(in_list ? p l1 \to prime p \land p \leq k \land \forall x.in_list ? x l2 \to p < x) \land - (prime p \to p \leq k \to (\forall x.in_list ? x l2 \to p < x) \to in_list ? p l1)) \to - (\forall x.(in_list ? x l2 \to 2 \leq x \land x \leq k \land \forall p.in_list ? p l1 \to \lnot p \divides x) \land - (2 \leq x \to x \leq k \to (\forall p.in_list ? p l1 \to \lnot p \divides x) \to - in_list ? x l2)) \to - length ? l2 \leq t \to - sorted_gt l1 \to - sorted_lt l2 \to - sorted_gt (sieve_aux l1 l2 t) \land - \forall p.(in_list ? p (sieve_aux l1 l2 t) \to prime p \land p \leq k) \land - (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 - [reflexivity - |simplify in H6;elim (not_le_Sn_O ? H6)]] - simplify;split - [assumption - |intro;elim (H p);split;intros - [elim (H5 H7);assumption - |apply (H6 H7 H8);rewrite > Hcut;intros;elim (not_in_list_nil ? ? H9)]] - |intros 4;elim l2 - [simplify;split; - [assumption - |intro;elim (H1 p);split;intros - [elim (H6 H8);assumption - |apply (H7 H8 H9);intros;elim (not_in_list_nil ? ? H10)]] - |simplify;elim (H k (filter ? l (\lambda x.notb (divides_b a x))) (a::l1)) - [split; - [assumption - |intro;apply H8;] - |split;intros - [elim (in_list_cons_case ? ? ? ? H7); - [rewrite > H8;split - [split - [unfold;intros;split - [elim (H3 a);elim H9 - [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] - |elim (H3 a);elim H11 - [elim H13;apply lt_to_le;assumption - |apply in_list_head] - |assumption]] - |elim (H3 a);elim H9 - [elim H11;assumption - |apply in_list_head]] - |intros;elim (le_to_or_lt_eq a x) - [assumption - |rewrite > H10 in H9;lapply (in_list_filter_to_p_true ? ? ? H9); - lapply (divides_n_n x); - rewrite > (divides_to_divides_b_true ? ? ? Hletin1) in Hletin - [simplify in Hletin;destruct Hletin - |rewrite < H10;elim (H3 a);elim H11 - [elim H13;apply lt_to_le;assumption - |apply in_list_head]] - |apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);apply (in_list_filter ? ? ? H9)]] - |elim (H2 p);elim (H9 H8);split - [assumption - |intros;apply H12;apply in_list_cons;apply (in_list_filter ? ? ? H13)]] - |elim (decidable_eq_nat p a) - [rewrite > H10;apply in_list_head - |apply in_list_cons;elim (H2 p);apply (H12 H7 H8);intros; - apply (trans_le ? a) - [elim (decidable_lt p a) - [assumption - |lapply (not_lt_to_le ? ? H14); - lapply (decidable_divides a p) - [elim Hletin1 - [elim H7;lapply (H17 ? H15) - [elim H10;symmetry;assumption - |elim (H3 a);elim H18 - [elim H20;assumption - |apply in_list_head]] - |elim (Not_lt_n_n p);apply H9;apply in_list_filter_r - [elim (H3 p);apply (in_list_tail ? ? a) - [apply H17 - [apply prime_to_lt_SO;assumption - |assumption - |intros;elim H7;intro;lapply (H20 ? H21) - [rewrite > Hletin2 in H18;elim (H11 H18); - lapply (H23 a) - [elim (lt_to_not_le ? ? Hletin3 Hletin) - |apply in_list_head] - |apply prime_to_lt_SO;elim (H2 p1);elim (H22 H18); - elim H24;assumption]] - |unfold;intro;apply H15;rewrite > H18;apply divides_n_n] - |rewrite > (not_divides_to_divides_b_false ? ? ? H15); - [reflexivity - |elim (H3 a);elim H16 - [elim H18;apply lt_to_le;assumption - |apply in_list_head]]]] - |elim (H3 a);elim H15 - [elim H17;apply lt_to_le;assumption - |apply in_list_head]]] - |elim (in_list_cons_case ? ? ? ? H13) - [rewrite > H14;apply le_n - |apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);assumption]]]] - |elim (H3 x);split;intros; - [split - [elim H7 - [assumption - |apply in_list_cons;apply (in_list_filter ? ? ? H9)] - |intros;elim (in_list_cons_case ? ? ? ? H10) - [rewrite > H11;intro;lapply (in_list_filter_to_p_true ? ? ? H9); - rewrite > (divides_to_divides_b_true ? ? ? H12) in Hletin - [simplify in Hletin;destruct Hletin - |elim (H3 a);elim H13 - [elim H15;apply lt_to_le;assumption - |apply in_list_head]] - |elim H7 - [apply H13;assumption - |apply in_list_cons;apply (in_list_filter ? ? ? H9)]]] - |elim (in_list_cons_case ? ? ? ? (H8 ? ? ?)) - [elim (H11 x) - [rewrite > H12;apply in_list_head - |apply divides_n_n] - |assumption - |assumption - |intros;apply H11;apply in_list_cons;assumption - |apply in_list_filter_r; - [assumption - |lapply (H11 a) - [rewrite > (not_divides_to_divides_b_false ? ? ? Hletin); - [reflexivity - |elim (H3 a);elim H13 - [elim H15;apply lt_to_le;assumption - |apply in_list_head]] - |apply in_list_head]]]] - |apply (trans_le ? ? ? (le_length_filter ? ? ?));apply le_S_S_to_le; - apply H4 - |apply sort_cons - [assumption - |intros;unfold;elim (H2 y);elim (H8 H7); - apply H11;apply in_list_head] - |generalize in match (sorted_cons_to_sorted ? ? ? ? H6);elim l - [simplify;assumption - |simplify;elim (notb (divides_b a a1));simplify - [lapply (sorted_cons_to_sorted ? ? ? ? H8);lapply (H7 Hletin); - apply (sort_cons ? ? ? ? Hletin1);intros; - apply (sorted_to_minimum ? ? ? ? H8);apply (in_list_filter ? ? ? H9); - |apply H7;apply (sorted_cons_to_sorted ? ? ? ? H8)]]]]] -qed. - -lemma le_list_n_aux_k_k : \forall n,m,k.in_list ? n (list_n_aux m k) \to - k \leq n. -intros 2;elim m - [simplify in H;elim (not_in_list_nil ? ? H) - |simplify in H1;elim (in_list_cons_case ? ? ? ? H1) - [rewrite > H2;apply le_n - |apply lt_to_le;apply H;assumption]] -qed. - -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] -qed. - -lemma le_SSO_list_n : \forall m,n.in_list nat n (list_n m) \to 2 \leq n. -intros;unfold list_n in H;apply (le_list_n_aux_k_k ? ? ? H); -qed. - -lemma le_list_n_aux : \forall n,m,k.in_list ? n (list_n_aux m k) \to n \leq k+m-1. -intros 2;elim m - [simplify in H;elim (not_in_list_nil ? ? H) - |simplify in H1;elim (in_list_cons_case ? ? ? ? H1) - [rewrite > H2;rewrite < plus_n_Sm;simplify;rewrite < minus_n_O; - rewrite > plus_n_O in \vdash (? % ?);apply le_plus_r;apply le_O_n - |rewrite < plus_n_Sm;apply (H (S k));assumption]] -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] -qed. - - -lemma le_list_n_aux_r : \forall n,m.O < m \to \forall k.k \leq n \to n \leq k+m-1 \to in_list ? n (list_n_aux m k). -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 - [apply in_list_head - |apply in_list_cons;apply H6 - [apply le_S_S;assumption - |rewrite < plus_n_Sm in H7;apply H7]]] -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; - [apply lt_O_S - |simplify in H7;apply le_S;assumption]] - |assumption - |simplify;generalize in match H2;elim H;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)) - [elim n;simplify - [apply le_n - |apply Hcut] - |intro;elim n1;simplify - [apply le_O_n - |apply le_S_S;apply H]] -qed. - -lemma sorted_list_n_aux : \forall n,k.sorted_lt (list_n_aux n k). -intro.elim n 0 - [simplify;intro;apply sort_nil - |intro;simplify;intros 2;apply sort_cons - [apply H - |intros;lapply (le_list_n_aux_k_k ? ? ? H1);assumption]] -qed. - -definition list_of_primes \def \lambda n.\lambda l. -\forall p.in_list nat p l \to prime p \land p \leq n. - -lemma sieve_sound1 : \forall n.2 \leq n \to -sorted_gt (sieve n) \land list_of_primes n (sieve n). -intros;elim (sieve_prime n n (list_n n) []) - [split - [assumption - |intro;unfold sieve in H3;elim (H2 p);elim (H3 H5);split;assumption] - |split;intros - [elim (not_in_list_nil ? ? H1) - |lapply (lt_to_not_le ? ? (H3 2 ?)) - [apply in_list_SSO_list_n;assumption - |elim Hletin;apply prime_to_lt_SO;assumption]] - |split;intros - [split - [split - [apply (le_SSO_list_n ? ? H1) - |apply (le_list_n ? ? H1)] - |intros;elim (not_in_list_nil ? ? H2)] - |apply le_list_n_r;assumption] - |apply le_length_list_n - |apply sort_nil - |elim n;simplify - [apply sort_nil - |elim n1;simplify - [apply sort_nil - |simplify;apply sort_cons - [apply sorted_list_n_aux - |intros;lapply (le_list_n_aux_k_k ? ? ? H3); - assumption]]]] -qed. - -lemma sieve_sorted : \forall n.sorted_gt (sieve n). -intros;elim (decidable_le 2 n) - [elim (sieve_sound1 ? H);assumption - |generalize in match (le_S_S_to_le ? ? (not_le_to_lt ? ? H));cases n - [intro;simplify;apply sort_nil - |intros;lapply (le_S_S_to_le ? ? H1);rewrite < (le_n_O_to_eq ? Hletin); - simplify;apply sort_nil]] -qed. - -lemma in_list_sieve_to_prime : \forall n,p.2 \leq n \to in_list ? p (sieve n) \to - prime p. -intros;elim (sieve_sound1 ? H);elim (H3 ? H1);assumption; -qed. - -lemma in_list_sieve_to_leq : \forall n,p.2 \leq n \to in_list ? p (sieve n) \to - p \leq n. -intros;elim (sieve_sound1 ? H);elim (H3 ? H1);assumption; -qed. - -lemma sieve_sound2 : \forall n,p.p \leq n \to prime p \to in_list ? p (sieve n). -intros;elim (sieve_prime n n (list_n n) []) - [elim (H3 p);apply H5;assumption - |split - [intro;elim (not_in_list_nil ? ? H2) - |intros;lapply (lt_to_not_le ? ? (H4 2 ?)) - [apply in_list_SSO_list_n;apply (trans_le ? ? ? ? H); - apply prime_to_lt_SO;assumption - |elim Hletin;apply prime_to_lt_SO;assumption]] - |split;intros - [split;intros - [split - [apply (le_SSO_list_n ? ? H2) - |apply (le_list_n ? ? H2)] - |elim (not_in_list_nil ? ? H3)] - |apply le_list_n_r - [apply (trans_le ? ? ? H2 H3) - |assumption - |assumption]] - |apply le_length_list_n - |apply sort_nil - |elim n;simplify - [apply sort_nil - |elim n1;simplify - [apply sort_nil - |simplify;apply sort_cons - [apply sorted_list_n_aux - |intros;lapply (le_list_n_aux_k_k ? ? ? H4); - assumption]]]] -qed. - let rec checker l \def match l with [ nil => true diff --git a/helm/software/matita/library/nat/factorization.ma b/helm/software/matita/library/nat/factorization.ma index f17fe0308..d649fbe14 100644 --- a/helm/software/matita/library/nat/factorization.ma +++ b/helm/software/matita/library/nat/factorization.ma @@ -74,6 +74,18 @@ cut (\exists i. nth_prime i = smallest_factor n); assumption; *) ] qed. +lemma divides_to_prime_divides : \forall n,m.1 < m \to m < n \to m \divides n \to + \exists p.p \leq m \land prime p \land p \divides n. +intros;apply (ex_intro ? ? (nth_prime (max_prime_factor m)));split + [split + [apply divides_to_le + [apply lt_to_le;assumption + |apply divides_max_prime_factor_n;assumption] + |apply prime_nth_prime;] + |apply (transitive_divides ? ? ? ? H2);apply divides_max_prime_factor_n; + assumption] +qed. + theorem divides_to_max_prime_factor : \forall n,m. (S O) < n \to O < m \to n \divides m \to max_prime_factor n \le max_prime_factor m. intros.unfold max_prime_factor. diff --git a/helm/software/matita/library/nat/sieve.ma b/helm/software/matita/library/nat/sieve.ma new file mode 100644 index 000000000..6b428d578 --- /dev/null +++ b/helm/software/matita/library/nat/sieve.ma @@ -0,0 +1,359 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / Matita is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +include "nat/sqrt.ma". +include "list/sort.ma". +include "nat/factorization.ma". + +let rec list_n_aux n k \def + match n with + [ O => nil nat + | S n1 => k::list_n_aux n1 (S k) ]. + +definition list_n : nat \to list nat \def + \lambda n.list_n_aux (pred n) 2. + +let rec sieve_aux l1 l2 t on t \def + match t with + [ O => l1 + | S t1 => match l2 with + [ nil => l1 + | cons n tl => sieve_aux (n::l1) (filter nat tl (\lambda x.notb (divides_b n x))) t1]]. + +definition sieve : nat \to list nat \def + \lambda m.sieve_aux [] (list_n m) m. + +definition sorted_lt \def sorted ? lt. +definition sorted_gt \def sorted ? gt. + +lemma sieve_prime : \forall t,k,l2,l1. + (\forall p.(in_list ? p l1 \to prime p \land p \leq k \land \forall x.in_list ? x l2 \to p < x) \land + (prime p \to p \leq k \to (\forall x.in_list ? x l2 \to p < x) \to in_list ? p l1)) \to + (\forall x.(in_list ? x l2 \to 2 \leq x \land x \leq k \land \forall p.in_list ? p l1 \to \lnot p \divides x) \land + (2 \leq x \to x \leq k \to (\forall p.in_list ? p l1 \to \lnot p \divides x) \to + in_list ? x l2)) \to + length ? l2 \leq t \to + sorted_gt l1 \to + sorted_lt l2 \to + sorted_gt (sieve_aux l1 l2 t) \land + \forall p.(in_list ? p (sieve_aux l1 l2 t) \to prime p \land p \leq k) \land + (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 + [reflexivity + |simplify in H6;elim (not_le_Sn_O ? H6)]] + simplify;split + [assumption + |intro;elim (H p);split;intros + [elim (H5 H7);assumption + |apply (H6 H7 H8);rewrite > Hcut;intros;elim (not_in_list_nil ? ? H9)]] + |intros 4;elim l2 + [simplify;split; + [assumption + |intro;elim (H1 p);split;intros + [elim (H6 H8);assumption + |apply (H7 H8 H9);intros;elim (not_in_list_nil ? ? H10)]] + |simplify;elim (H k (filter ? l (\lambda x.notb (divides_b a x))) (a::l1)) + [split; + [assumption + |intro;apply H8;] + |split;intros + [elim (in_list_cons_case ? ? ? ? H7); + [rewrite > H8;split + [split + [unfold;intros;split + [elim (H3 a);elim H9 + [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] + |elim (H3 a);elim H11 + [elim H13;apply lt_to_le;assumption + |apply in_list_head] + |assumption]] + |elim (H3 a);elim H9 + [elim H11;assumption + |apply in_list_head]] + |intros;elim (le_to_or_lt_eq a x) + [assumption + |rewrite > H10 in H9;lapply (in_list_filter_to_p_true ? ? ? H9); + lapply (divides_n_n x); + rewrite > (divides_to_divides_b_true ? ? ? Hletin1) in Hletin + [simplify in Hletin;destruct Hletin + |rewrite < H10;elim (H3 a);elim H11 + [elim H13;apply lt_to_le;assumption + |apply in_list_head]] + |apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);apply (in_list_filter ? ? ? H9)]] + |elim (H2 p);elim (H9 H8);split + [assumption + |intros;apply H12;apply in_list_cons;apply (in_list_filter ? ? ? H13)]] + |elim (decidable_eq_nat p a) + [rewrite > H10;apply in_list_head + |apply in_list_cons;elim (H2 p);apply (H12 H7 H8);intros; + apply (trans_le ? a) + [elim (decidable_lt p a) + [assumption + |lapply (not_lt_to_le ? ? H14); + lapply (decidable_divides a p) + [elim Hletin1 + [elim H7;lapply (H17 ? H15) + [elim H10;symmetry;assumption + |elim (H3 a);elim H18 + [elim H20;assumption + |apply in_list_head]] + |elim (Not_lt_n_n p);apply H9;apply in_list_filter_r + [elim (H3 p);apply (in_list_tail ? ? a) + [apply H17 + [apply prime_to_lt_SO;assumption + |assumption + |intros;elim H7;intro;lapply (H20 ? H21) + [rewrite > Hletin2 in H18;elim (H11 H18); + lapply (H23 a) + [elim (lt_to_not_le ? ? Hletin3 Hletin) + |apply in_list_head] + |apply prime_to_lt_SO;elim (H2 p1);elim (H22 H18); + elim H24;assumption]] + |unfold;intro;apply H15;rewrite > H18;apply divides_n_n] + |rewrite > (not_divides_to_divides_b_false ? ? ? H15); + [reflexivity + |elim (H3 a);elim H16 + [elim H18;apply lt_to_le;assumption + |apply in_list_head]]]] + |elim (H3 a);elim H15 + [elim H17;apply lt_to_le;assumption + |apply in_list_head]]] + |elim (in_list_cons_case ? ? ? ? H13) + [rewrite > H14;apply le_n + |apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);assumption]]]] + |elim (H3 x);split;intros; + [split + [elim H7 + [assumption + |apply in_list_cons;apply (in_list_filter ? ? ? H9)] + |intros;elim (in_list_cons_case ? ? ? ? H10) + [rewrite > H11;intro;lapply (in_list_filter_to_p_true ? ? ? H9); + rewrite > (divides_to_divides_b_true ? ? ? H12) in Hletin + [simplify in Hletin;destruct Hletin + |elim (H3 a);elim H13 + [elim H15;apply lt_to_le;assumption + |apply in_list_head]] + |elim H7 + [apply H13;assumption + |apply in_list_cons;apply (in_list_filter ? ? ? H9)]]] + |elim (in_list_cons_case ? ? ? ? (H8 ? ? ?)) + [elim (H11 x) + [rewrite > H12;apply in_list_head + |apply divides_n_n] + |assumption + |assumption + |intros;apply H11;apply in_list_cons;assumption + |apply in_list_filter_r; + [assumption + |lapply (H11 a) + [rewrite > (not_divides_to_divides_b_false ? ? ? Hletin); + [reflexivity + |elim (H3 a);elim H13 + [elim H15;apply lt_to_le;assumption + |apply in_list_head]] + |apply in_list_head]]]] + |apply (trans_le ? ? ? (le_length_filter ? ? ?));apply le_S_S_to_le; + apply H4 + |apply sort_cons + [assumption + |intros;unfold;elim (H2 y);elim (H8 H7); + apply H11;apply in_list_head] + |generalize in match (sorted_cons_to_sorted ? ? ? ? H6);elim l + [simplify;assumption + |simplify;elim (notb (divides_b a a1));simplify + [lapply (sorted_cons_to_sorted ? ? ? ? H8);lapply (H7 Hletin); + apply (sort_cons ? ? ? ? Hletin1);intros; + apply (sorted_to_minimum ? ? ? ? H8);apply (in_list_filter ? ? ? H9); + |apply H7;apply (sorted_cons_to_sorted ? ? ? ? H8)]]]]] +qed. + +definition list_of_primes \def \lambda n.\lambda l. +\forall p.in_list nat p l \to prime p \land p \leq n. + +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] +qed. + +lemma le_list_n_aux_k_k : \forall n,m,k.in_list ? n (list_n_aux m k) \to + k \leq n. +intros 2;elim m + [simplify in H;elim (not_in_list_nil ? ? H) + |simplify in H1;elim (in_list_cons_case ? ? ? ? H1) + [rewrite > H2;apply le_n + |apply lt_to_le;apply H;assumption]] +qed. + +lemma le_SSO_list_n : \forall m,n.in_list nat n (list_n m) \to 2 \leq n. +intros;unfold list_n in H;apply (le_list_n_aux_k_k ? ? ? H); +qed. + +lemma le_list_n_aux : \forall n,m,k.in_list ? n (list_n_aux m k) \to n \leq k+m-1. +intros 2;elim m + [simplify in H;elim (not_in_list_nil ? ? H) + |simplify in H1;elim (in_list_cons_case ? ? ? ? H1) + [rewrite > H2;rewrite < plus_n_Sm;simplify;rewrite < minus_n_O; + rewrite > plus_n_O in \vdash (? % ?);apply le_plus_r;apply le_O_n + |rewrite < plus_n_Sm;apply (H (S k));assumption]] +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] +qed. + + +lemma le_list_n_aux_r : \forall n,m.O < m \to \forall k.k \leq n \to n \leq k+m-1 \to in_list ? n (list_n_aux m k). +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 + [apply in_list_head + |apply in_list_cons;apply H6 + [apply le_S_S;assumption + |rewrite < plus_n_Sm in H7;apply H7]]] +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; + [apply lt_O_S + |simplify in H7;apply le_S;assumption]] + |assumption + |simplify;generalize in match H2;elim H;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)) + [elim n;simplify + [apply le_n + |apply Hcut] + |intro;elim n1;simplify + [apply le_O_n + |apply le_S_S;apply H]] +qed. + +lemma sorted_list_n_aux : \forall n,k.sorted_lt (list_n_aux n k). +intro.elim n 0 + [simplify;intro;apply sort_nil + |intro;simplify;intros 2;apply sort_cons + [apply H + |intros;lapply (le_list_n_aux_k_k ? ? ? H1);assumption]] +qed. + +lemma sieve_sound1 : \forall n.2 \leq n \to +sorted_gt (sieve n) \land list_of_primes n (sieve n). +intros;elim (sieve_prime n n (list_n n) []) + [split + [assumption + |intro;unfold sieve in H3;elim (H2 p);elim (H3 H5);split;assumption] + |split;intros + [elim (not_in_list_nil ? ? H1) + |lapply (lt_to_not_le ? ? (H3 2 ?)) + [apply in_list_SSO_list_n;assumption + |elim Hletin;apply prime_to_lt_SO;assumption]] + |split;intros + [split + [split + [apply (le_SSO_list_n ? ? H1) + |apply (le_list_n ? ? H1)] + |intros;elim (not_in_list_nil ? ? H2)] + |apply le_list_n_r;assumption] + |apply le_length_list_n + |apply sort_nil + |elim n;simplify + [apply sort_nil + |elim n1;simplify + [apply sort_nil + |simplify;apply sort_cons + [apply sorted_list_n_aux + |intros;lapply (le_list_n_aux_k_k ? ? ? H3); + assumption]]]] +qed. + +lemma sieve_sorted : \forall n.sorted_gt (sieve n). +intros;elim (decidable_le 2 n) + [elim (sieve_sound1 ? H);assumption + |generalize in match (le_S_S_to_le ? ? (not_le_to_lt ? ? H));cases n + [intro;simplify;apply sort_nil + |intros;lapply (le_S_S_to_le ? ? H1);rewrite < (le_n_O_to_eq ? Hletin); + simplify;apply sort_nil]] +qed. + +lemma in_list_sieve_to_prime : \forall n,p.2 \leq n \to in_list ? p (sieve n) \to + prime p. +intros;elim (sieve_sound1 ? H);elim (H3 ? H1);assumption; +qed. + +lemma in_list_sieve_to_leq : \forall n,p.2 \leq n \to in_list ? p (sieve n) \to + p \leq n. +intros;elim (sieve_sound1 ? H);elim (H3 ? H1);assumption; +qed. + +lemma sieve_sound2 : \forall n,p.p \leq n \to prime p \to in_list ? p (sieve n). +intros;elim (sieve_prime n n (list_n n) []) + [elim (H3 p);apply H5;assumption + |split + [intro;elim (not_in_list_nil ? ? H2) + |intros;lapply (lt_to_not_le ? ? (H4 2 ?)) + [apply in_list_SSO_list_n;apply (trans_le ? ? ? ? H); + apply prime_to_lt_SO;assumption + |elim Hletin;apply prime_to_lt_SO;assumption]] + |split;intros + [split;intros + [split + [apply (le_SSO_list_n ? ? H2) + |apply (le_list_n ? ? H2)] + |elim (not_in_list_nil ? ? H3)] + |apply le_list_n_r + [apply (trans_le ? ? ? H2 H3) + |assumption + |assumption]] + |apply le_length_list_n + |apply sort_nil + |elim n;simplify + [apply sort_nil + |elim n1;simplify + [apply sort_nil + |simplify;apply sort_cons + [apply sorted_list_n_aux + |intros;lapply (le_list_n_aux_k_k ? ? ? H4); + assumption]]]] +qed. +