-
-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]]]
+
+theorem check_list2: \forall l. check_list l = true \to
+\forall p. in_list nat p l \to 2 < p \to
+\exists pp. in_list nat pp l \land pp < p \land p \le 2*pp.
+intro.elim l 2
+ [intros.apply False_ind.apply (not_in_list_nil ? ? H1)
+ |cases l1;intros
+ [lapply (in_list_singleton_to_eq ? ? ? H2) as H4.
+ apply False_ind.
+ apply (lt_to_not_eq ? ? H3).
+ apply sym_eq.apply eqb_true_to_eq.
+ rewrite > H4.apply H1
+ |elim (check_list1 ? ? ? H1).clear H1.
+ elim H4.clear H4.
+ elim H1.clear H1.
+ elim (in_list_cons_case ? ? ? ? H2)
+ [apply (ex_intro ? ? n).
+ split
+ [split
+ [apply in_list_cons.apply in_list_head
+ |rewrite > H1.assumption
+ ]
+ |rewrite > H1.assumption
+ ]
+ |elim (H H6 p H1 H3).clear H.
+ apply (ex_intro ? ? a1).
+ elim H8.clear H8.
+ elim H.clear H.
+ split
+ [split
+ [apply in_list_cons.assumption
+ |assumption
+ ]
+ |assumption
+ ]
+ ]
+ ]
+ ]