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).
projects / helm.git / commitdiff