From 5b83f526bc4c63424313df91173b844699eada96 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Fri, 22 Feb 2008 17:34:56 +0000 Subject: [PATCH] sieve of erathostene (proof of soundness almost done) --- helm/software/matita/library/nat/bertrand.ma | 286 +++++++++++++++++++ 1 file changed, 286 insertions(+) diff --git a/helm/software/matita/library/nat/bertrand.ma b/helm/software/matita/library/nat/bertrand.ma index 20302e876..d3472d675 100644 --- a/helm/software/matita/library/nat/bertrand.ma +++ b/helm/software/matita/library/nat/bertrand.ma @@ -15,8 +15,294 @@ include "nat/sqrt.ma". include "nat/chebyshev_teta.ma". include "nat/chebyshev.ma". +include "list/list.ma". include "nat/o.ma". +let rec list_divides l n \def + match l with + [ nil ⇒ false + | cons (m:nat) (tl:list nat) ⇒ orb (divides_b m n) (list_divides tl n) ]. + +definition lprim : nat \to list nat \def + \lambda n.let rec aux m acc \def + match m with + [ O => acc + | S m1 => match (list_divides acc (n-m1)) with + [ true => aux m1 acc + | false => aux m1 (n-m1::acc)]] + in aux (pred n) []. + +let rec filter A l p on l \def + match l with + [ nil => nil A + | cons (a:A) (tl:list A) => match (p a) with + [ true => a::(filter A tl p) + | false => filter A tl p ]]. + +let rec length A (l:list A) on l \def + match l with + [ nil => O + | cons (a:A) (tl:list A) => S (length A tl) ]. + +definition list_n : nat \to list nat \def + \lambda n.let rec aux n k \def + match n with + [ O => nil nat + | S n1 => k::aux n1 (S k) ] + in 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 ord_list \def + \lambda l. + \forall a,b,l1,l2.l = l1@(a::b::l2) \to b \leq a. + +definition in_list \def + \lambda A.\lambda a:A.\lambda l:list A. + \exists l1,l2.l = l1@(a::l2). + +lemma in_list_filter_to_p_true : \forall l,x,p.in_list nat x (filter nat l p) \to p x = true. +intros;elim H;elim H1;clear H H1;generalize in match H2;generalize in match a;elim l 0 + [simplify;intro;elim l1 + [simplify in H;destruct H + |simplify in H1;destruct H1] + |intros;simplify in H1;apply (bool_elim ? (p t));intro; + rewrite > H3 in H1;simplify in H1 + [generalize in match H1;elim l2 + [simplify in H4;destruct H4;assumption + |simplify in H5;destruct H5;apply (H l3);assumption] + |apply (H l2);assumption]] +qed. + +lemma in_list_cons : \forall l,x,y.in_list nat x l \to in_list nat x (y::l). +intros;unfold in H;unfold;elim H;elim H1;apply (ex_intro ? ? (y::a)); +apply (ex_intro ? ? a1);simplify;rewrite < H2;reflexivity. +qed. + +lemma in_list_tail : \forall l,x,y.in_list nat x (y::l) \to x \neq y \to in_list nat x l. +intros;elim H;elim H2;generalize in match H3;elim a + [simplify in H4;destruct H4;elim H1;reflexivity + |simplify in H5;destruct H5;apply (ex_intro ? ? l1);apply (ex_intro ? ? a1); + reflexivity] +qed. + +lemma in_list_filter : \forall l,p,x.in_list nat x (filter nat l p) \to in_list nat x l. +intros;elim H;elim H1;generalize in match H2;generalize in match a;elim l 0 + [simplify;intro;elim l1 + [simplify in H3;destruct H3 + |simplify in H4;destruct H4] + |intros;simplify in H4;apply (bool_elim ? (p t));intro + [rewrite > H5 in H4;simplify in H4;generalize in match H4;elim l2 + [simplify in H6;destruct H6;apply (ex_intro ? ? []);apply (ex_intro ? ? l1); + simplify;reflexivity + |simplify in H7;destruct H7;apply in_list_cons;apply (H3 ? Hcut1);] + |rewrite > H5 in H4;simplify in H4;apply in_list_cons;apply (H3 ? H4);]] +qed. + +lemma in_list_filter_r : \forall l,p,x.in_list nat x l \to p x = true \to in_list nat x (filter nat l p). +intros;elim H;elim H2;rewrite > H3;elim a + [simplify;rewrite > H1;simplify;apply (ex_intro ? ? []);apply (ex_intro ? ? (filter nat a1 p)); + reflexivity + |simplify;elim (p t);simplify + [apply in_list_cons;assumption + |assumption]] +qed. + +axiom sieve_monotonic : \forall n.sieve (S n) = sieve n \lor sieve (S n) = (S n)::sieve n. + +axiom daemon : False. + +axiom in_list_cons_case : \forall A,x,a,l.in_list A x (a::l) \to + x = a \lor in_list A x l. + +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. + +lemma in_list_head : \forall x,l.in_list nat x (x::l). +intros;apply (ex_intro ? ? []);apply (ex_intro ? ? l);reflexivity; +qed. + +lemma le_length_filter : \forall A,l,p.length A (filter A l p) \leq length A l. +intros;elim l + [simplify;apply le_n + |simplify;apply (bool_elim ? (p t));intro + [simplify;apply le_S_S;assumption + |simplify;apply le_S;assumption]] +qed. + +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 x \leq k \land \forall p.in_list ? p l1 \to \lnot p \divides x) \land + ((x \leq k \land \forall p.in_list ? p l1 \to \lnot p \divides x) \to + in_list ? x l2)) \to + length ? l2 \leq t \to + \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 H4;elim (not_le_Sn_O ? H4)]] + simplify;split;intros; + [elim (H p);elim (H4 H3);assumption + |elim (H p);apply (H6 H3 H4);rewrite > Hcut;intros;unfold in H7; + elim H7;elim H8;clear H7 H8;generalize in match H9;elim a + [simplify in H7;destruct H7 + |simplify in H8;destruct H8]] + |intros 4;elim l2 + [simplify;split;intros + [elim (H1 p);elim (H5 H4);assumption + |elim (H1 p);apply (H7 H4 H5);intros;unfold in H8; + elim H8;elim H9;clear H8 H9;generalize in match H10;elim a + [simplify in H8;destruct H8 + |simplify in H9;destruct H9]] + |simplify;elim (H k (filter ? l (\lambda x.notb (divides_b t1 x))) (t1::l1) ? ? ? p) + [split;intros + [apply H5;assumption + |apply H6;assumption] + |intro;split;intros + [elim (in_list_cons_case ? ? ? ? H5); + [rewrite > H6;split + [split + [unfold;intros;split + [elim daemon (* aggiungere hp: ogni elemento di l2 è >= 2 *) + |intros;elim (le_to_or_lt_eq ? ? (divides_to_le ? ? ? H7)) + [elim (divides_to_prime_divides ? ? H8 H9 H7);elim H10; + elim H11;clear H10 H11;elim (H3 t1);elim H10 + [clear H10 H11;elim (H16 ? ? H12);elim (H2 a);clear H10; + apply H11 + [assumption + |apply (trans_le ? ? ? ? H15); + apply (trans_le ? ? ? H13); + apply lt_to_le;assumption + |intros; + (* sfruttare il fatto che a < t1 + e t1 è il minimo di t1::l *) + elim daemon] + |unfold;apply (ex_intro ? ? []); + apply (ex_intro ? ? l); + reflexivity] + |elim daemon (* aggiungere hp: ogni elemento di l2 è >= 2 *) + |assumption]] + |elim (H3 t1);elim H7 + [assumption + |apply (ex_intro ? ? []);apply (ex_intro ? ? l);reflexivity]] + |intros;elim (le_to_or_lt_eq t1 x) + [assumption + |rewrite > H8 in H7;lapply (in_list_filter_to_p_true ? ? ? H7); + lapply (divides_n_n x); + rewrite > (divides_to_divides_b_true ? ? ? Hletin1) in Hletin + [simplify in Hletin;destruct Hletin + |elim daemon (* aggiungere hp: ogni elemento di l2 è >= 2 *)] + |(* sfruttare il fatto che t1 è il minimo di t1::l *) + elim daemon]] + |elim (H2 p1);elim (H7 H6);split + [assumption + |intros;apply H10;apply in_list_cons;apply (in_list_filter ? ? ? H11);]] + |elim (decidable_eq_nat p1 t1) + [rewrite > H8;apply (ex_intro ? ? []);apply (ex_intro ? ? l1); + reflexivity + |apply in_list_cons;elim (H2 p1);apply (H10 H5 H6);intros; + apply (trans_le ? t1) + [elim (decidable_lt p1 t1) + [assumption + |lapply (not_lt_to_le ? ? H12); + lapply (decidable_divides t1 p1) + [elim Hletin1 + [elim H5;lapply (H15 ? H13) + [elim H8;symmetry;assumption + |(* per il solito discorso l2 >= 2 *) + elim daemon] + |elim (Not_lt_n_n p1);apply H7;apply in_list_filter_r + [elim (H3 p1);apply (in_list_tail ? ? t1) + [apply H15;split + [assumption + |intros;elim H5;intro;lapply (H18 ? H19) + [rewrite > Hletin2 in H16;elim (H9 H16); + lapply (H21 t1) + [elim (lt_to_not_le ? ? Hletin3 Hletin) + |apply (ex_intro ? ? []);apply (ex_intro ? ? l); + reflexivity] + |apply prime_to_lt_SO;elim (H2 p2);elim (H20 H16); + elim H22;assumption]] + |unfold;intro;apply H13;rewrite > H16;apply divides_n_n;] + |rewrite > (not_divides_to_divides_b_false ? ? ? H13); + [reflexivity + |elim daemon (* usare il solito >= 2 *)]]] + |elim daemon (* come sopra *)]] + |elim daemon (* t1::l è ordinata *)]]] + |intro;elim (H3 x);split;intros; + [split + [elim H5 + [assumption + |apply in_list_cons;apply (in_list_filter ? ? ? H7)] + |intros;elim (in_list_cons_case ? ? ? ? H8) + [rewrite > H9;intro;lapply (in_list_filter_to_p_true ? ? ? H7); + rewrite > (divides_to_divides_b_true ? ? ? H10) in Hletin + [simplify in Hletin;destruct Hletin + |elim daemon (* dal fatto che ogni elemento di t1::l è >= 2 *)] + |elim H5 + [apply H11;assumption + |apply in_list_cons;apply (in_list_filter ? ? ? H7)]]] + |elim H7;elim (in_list_cons_case ? ? ? ? (H6 ?)) + [elim (H9 x) + [rewrite > H10;unfold; + apply (ex_intro ? ? []);apply (ex_intro ? ? l1); + reflexivity + |apply divides_n_n;] + |split + [assumption + |intros;apply H9;apply in_list_cons;assumption] + |apply in_list_filter_r; + [assumption + |lapply (H9 t1) + [rewrite > (not_divides_to_divides_b_false ? ? ? Hletin); + [reflexivity + |(* solito >= 2 *) + elim daemon] + |apply in_list_head]]]] + |apply (trans_le ? ? ? (le_length_filter ? ? ?));apply le_S_S_to_le; + apply H4]]] +qed. + +lemma sieve_soundness : \forall n.\forall p. + in_list ? p (sieve n) \to + p \leq n \land prime p. +intros;unfold sieve in H;lapply (sieve_prime n (S n) (list_n n) [] ? ? ? p) + [intros;split;intros; + [elim daemon (* H1 is absurd *) + |elim daemon (* da sistemare, bisognerebbe raggiungere l'assurdo sapendo che p1 è primo e < 2 *)] + |intro;split;intros + [split + [elim daemon (* vero, dalla H1 *) + |intros;elim daemon (* H2 è assurda *)] + |elim H1; + (* vera supponendo x >= 2, il che in effetti è doveroso sistemare nel teoremone di prima *) + elim daemon] + |elim daemon (* sempre vero, da dimostrare *) + |elim Hletin;elim (H1 H);split + [elim daemon (* si può ottenere da H *) + |assumption]] +qed. + definition bertrand \def \lambda n. \exists p.n < p \land p \le 2*n \land (prime p). -- 2.39.2