From: Wilmer Ricciotti Date: Wed, 27 Feb 2008 17:03:01 +0000 (+0000) Subject: the proof of bertrand's conjecture is now complete X-Git-Tag: make_still_working~5573 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=286b2c5ed05fc545a2ac69af4cd39d1f35a53b68;p=helm.git the proof of bertrand's conjecture is now complete --- diff --git a/helm/software/matita/library/nat/bertrand.ma b/helm/software/matita/library/nat/bertrand.ma index d3472d675..bb4fde497 100644 --- a/helm/software/matita/library/nat/bertrand.ma +++ b/helm/software/matita/library/nat/bertrand.ma @@ -43,13 +43,14 @@ 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 + +let rec list_n_aux n k \def match n with [ O => nil nat - | S n1 => k::aux n1 (S k) ] - in aux (pred n) 2. + | 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 @@ -116,12 +117,19 @@ intros;elim H;elim H2;rewrite > H3;elim a |assumption]] qed. -axiom sieve_monotonic : \forall n.sieve (S n) = sieve n \lor sieve (S n) = (S n)::sieve n. - -axiom daemon : False. +lemma in_list_head : \forall x,l.in_list nat x (x::l). +intros;apply (ex_intro ? ? []);apply (ex_intro ? ? l);reflexivity; +qed. -axiom in_list_cons_case : \forall A,x,a,l.in_list A x (a::l) \to +lemma in_list_cons_case : \forall A,x,a,l.in_list A x (a::l) \to x = a \lor in_list A x l. +intros;elim H;elim H1;clear H H1;generalize in match H2;elim a1 + [simplify in H;destruct H;left;reflexivity + |simplify in H1;destruct H1;right; + apply (ex_intro ? ? l1); + apply (ex_intro ? ? a2); + reflexivity] +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. @@ -135,9 +143,6 @@ intros;apply (ex_intro ? ? (nth_prime (max_prime_factor m)));split 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 @@ -147,160 +152,392 @@ intros;elim l |simplify;apply le_S;assumption]] qed. +inductive sorted (P:nat \to nat \to Prop): list nat \to Prop \def +| sort_nil : sorted P [] +| sort_cons : \forall x,l.sorted P l \to (\forall y.in_list ? y l \to P x y) + \to sorted P (x::l). + +definition sorted_lt : list nat \to Prop \def \lambda l.sorted lt l. + +definition sorted_gt : list nat \to Prop \def \lambda l.sorted gt l. + +lemma sorted_cons_to_sorted : \forall P,x,l.sorted P (x::l) \to sorted P l. +intros;inversion H;intros + [destruct H1 + |destruct H4;assumption] +qed. + +lemma sorted_to_minimum : \forall P,x,l.sorted P (x::l) \to + \forall y.in_list ? y l \to P x y. +intros;inversion H;intros; + [destruct H2 + |destruct H5;apply H4;assumption] +qed. + +lemma not_in_list_nil : \forall A,a.\lnot in_list A a []. +intros;intro;elim H;elim H1;generalize in match H2;elim a1 + [simplify in H3;destruct H3 + |simplify in H4;destruct H4] +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 + (\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 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]] + |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;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 + [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 t1 x))) (t1::l1)) + [split; + [assumption + |intro;apply H8;] + |split;intros + [elim (in_list_cons_case ? ? ? ? H7); + [rewrite > H8;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 + [elim (H3 t1);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 t1);elim H12 + [clear H13 H12;elim (H18 ? ? H14);elim (H2 a); + apply H13 [assumption - |apply (trans_le ? ? ? ? H15); - apply (trans_le ? ? ? H13); + |elim H17;apply (trans_le ? ? ? ? H20); + apply (trans_le ? ? ? H15); apply lt_to_le;assumption - |intros; - (* sfruttare il fatto che a < t1 - e t1 è il minimo di t1::l *) - elim daemon] + |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]]] |unfold;apply (ex_intro ? ? []); apply (ex_intro ? ? l); reflexivity] - |elim daemon (* aggiungere hp: ogni elemento di l2 è >= 2 *) + |elim (H3 t1);elim H11 + [elim H13;apply lt_to_le;assumption + |apply in_list_head] |assumption]] - |elim (H3 t1);elim H7 - [assumption + |elim (H3 t1);elim H9 + [elim H11;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); + |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 - |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 + |rewrite < H10;elim (H3 t1);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 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); + |intros;apply H12;apply in_list_cons;apply (in_list_filter ? ? ? H13)]] + |elim (decidable_eq_nat p t1) + [rewrite > H10;apply (ex_intro ? ? []);apply (ex_intro ? ? l1); reflexivity - |apply in_list_cons;elim (H2 p1);apply (H10 H5 H6);intros; + |apply in_list_cons;elim (H2 p);apply (H12 H7 H8);intros; apply (trans_le ? t1) - [elim (decidable_lt p1 t1) + [elim (decidable_lt p t1) [assumption - |lapply (not_lt_to_le ? ? H12); - lapply (decidable_divides t1 p1) + |lapply (not_lt_to_le ? ? H14); + lapply (decidable_divides t1 p) [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 H7;lapply (H17 ? H15) + [elim H10;symmetry;assumption + |elim (H3 t1);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 ? ? t1) + [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 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); + |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 daemon (* usare il solito >= 2 *)]]] - |elim daemon (* come sopra *)]] - |elim daemon (* t1::l è ordinata *)]]] - |intro;elim (H3 x);split;intros; + |elim (H3 t1);elim H16 + [elim H18;apply lt_to_le;assumption + |apply in_list_head]]]] + |elim (H3 t1);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 H5 + [elim H7 [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 + |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 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] + |elim (H3 t1);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 (H9 t1) + |lapply (H11 t1) [rewrite > (not_divides_to_divides_b_false ? ? ? Hletin); [reflexivity - |(* solito >= 2 *) - elim daemon] + |elim (H3 t1);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 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 t1 t2));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 in_list_singleton_to_eq : \forall A,x,y.in_list A x [y] \to x = y. +intros;elim H;elim H1;generalize in match H2;elim a + [simplify in H3;destruct H3;reflexivity + |simplify in H4;destruct H4;generalize in match Hcut1;elim l + [simplify in H4;destruct H4 + |simplify in H5;destruct H5]] +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 H1;elim H2;generalize in match H3;elim a + [simplify in H4;destruct H4;apply le_n + |simplify in H5;destruct H5;apply lt_to_le;apply (H (S k)); + apply (ex_intro ? ? l);apply (ex_intro ? ? a1);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 (ex_intro ? ? []);apply (ex_intro ? ? []); + simplify;reflexivity + |generalize in match H2;elim H1 + [simplify;apply (ex_intro ? ? []);apply (ex_intro ? ? [3]);simplify;reflexivity + |simplify;apply (ex_intro ? ? []);apply (ex_intro ? ? (list_n_aux n2 3)); + simplify;reflexivity]] +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 H1;elim H2;generalize in match H3;elim a + [simplify in H4;destruct H4;rewrite < plus_n_Sm;simplify;rewrite < minus_n_O; + rewrite > plus_n_O in \vdash (? % ?);apply le_plus_r;apply le_O_n + |simplify in H5;destruct H5;rewrite < plus_n_Sm;apply (H (S k)); + apply (ex_intro ? ? l);apply (ex_intro ? ? a1);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 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 +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 + (\forall p.in_list ? p (sieve n) \to + prime p \land p \leq 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 - [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]] + [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;apply sort_nil + |intros;lapply (le_S_S_to_le ? ? H1);rewrite < (le_n_O_to_eq ? Hletin); + 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 + | cons h1 t1 => match t1 with + [ nil => true + | cons h2 t2 => (andb (checker t1) (leb h1 (2*h2))) ]]. + +lemma checker_cons : \forall t,l.checker (t::l) = true \to checker l = true. +intros 2;simplify;intro;generalize in match H;elim l + [reflexivity + |change in H2 with (andb (checker (t1::l1)) (leb t (t1+(t1+O))) = true); + apply (andb_true_true ? ? H2)] +qed. + +theorem checker_sound : \forall l1,l2,l,x,y.l = l1@(x::y::l2) \to + checker l = true \to x \leq 2*y. +intro;elim l1 0 + [simplify;intros 5;rewrite > H;simplify;intro; + apply leb_true_to_le;apply (andb_true_true_r ? ? H1); + |simplify;intros;rewrite > H1 in H2;lapply (checker_cons ? ? H2); + apply (H l2 ? ? ? ? Hletin);reflexivity] qed. definition bertrand \def \lambda n. @@ -309,6 +546,122 @@ definition bertrand \def \lambda n. definition not_bertrand \def \lambda n. \forall p.n < p \to p \le 2*n \to \not (prime p). +lemma min_prim : \forall n.\exists p. n < p \land prime p \land + \forall q.prime q \to q < p \to q \leq n. +intro;elim (le_to_or_lt_eq ? ? (le_O_n n)) + [apply (ex_intro ? ? (min_aux (S (n!)) (S n) primeb)); + split + [split + [apply le_min_aux; + |apply primeb_true_to_prime;apply f_min_aux_true;elim (ex_prime n); + [apply (ex_intro ? ? a);elim H1;elim H2;split + [split + [assumption + |rewrite > plus_n_O;apply le_plus + [assumption + |apply le_O_n]] + |apply prime_to_primeb_true;assumption] + |assumption]] + |intros;apply not_lt_to_le;intro;lapply (lt_min_aux_to_false ? ? ? ? H3 H2); + rewrite > (prime_to_primeb_true ? H1) in Hletin;destruct Hletin] + |apply (ex_intro ? ? 2);split + [split + [rewrite < H;apply lt_O_S + |apply primeb_true_to_prime;reflexivity] + |intros;elim (lt_to_not_le ? ? H2);apply prime_to_lt_SO;assumption]] +qed. + +(*lemma pippo : \forall k,n.in_list ? (nth_prime (S k)) (sieve n) \to + \exists l.sieve n = l@((nth_prime (S k))::(sieve (nth_prime k))). +intros;elim H;elim H1;clear H H1;apply (ex_intro ? ? a); +cut (a1 = sieve (nth_prime k)) + [rewrite < Hcut;assumption + |lapply (sieve_sorted n);generalize in match H2*) + +lemma le_to_bertrand : \forall n.O < n \to n \leq exp 2 8 \to bertrand n. +intros; +elim (min_prim n);apply (ex_intro ? ? a);elim H2;elim H3;clear H2 H3; +cut (a \leq 257) + [|apply not_lt_to_le;intro;apply (le_to_not_lt ? ? H1);apply (H4 ? ? H2); + apply primeb_true_to_prime;reflexivity] +split + [split + [assumption + |elim (prime_to_nth_prime a H6);generalize in match H2;cases a1 + [simplify;intro;rewrite < H3;rewrite < plus_n_O; + change in \vdash (? % ?) with (1+1);apply le_plus;assumption + |intro;lapply (H4 (nth_prime n1)) + [apply (trans_le ? (2*(nth_prime n1))) + [rewrite < H3; + cut (\exists l1,l2.sieve 257 = l1@((nth_prime (S n1))::((nth_prime n1)::l2))) + [elim Hcut1;elim H7;clear Hcut1 H7; + apply (checker_sound a2 a3 (sieve 257)) + [apply H8 + |reflexivity] + |elim (sieve_sound2 257 (nth_prime (S n1)) ? ?) + [elim (sieve_sound2 257 (nth_prime n1) ? ?) + [elim H8; + cut (\forall p.in_list ? p (a3@(nth_prime n1::a4)) \to prime p) + [|rewrite < H9;intros;apply (in_list_sieve_to_prime 257 p ? H10); + apply leb_true_to_le;reflexivity] + apply (ex_intro ? ? a2);apply (ex_intro ? ? a4); + elim H7;clear H7 H8; + cut ((nth_prime n1)::a4 = a5) + [|generalize in match H10; + lapply (sieve_sorted 257); + generalize in match Hletin1; + rewrite > H9 in ⊢ (? %→? ? % ?→?); + generalize in match Hcut1; + generalize in match a2; + elim a3 0 + [intro;elim l + [change in H11 with (nth_prime n1::a4 = nth_prime (S n1)::a5); + destruct H11;elim (eq_to_not_lt ? ? Hcut2); + apply increasing_nth_prime + |change in H12 with (nth_prime n1::a4 = t::(l1@(nth_prime (S n1)::a5))); + destruct H12; + change in H11 with (sorted_gt (nth_prime n1::l1@(nth_prime (S n1)::a5))); + lapply (sorted_to_minimum ? ? ? H11 (nth_prime (S n1))) + [unfold in Hletin2;elim (le_to_not_lt ? ? (lt_to_le ? ? Hletin2)); + apply increasing_nth_prime + |apply (ex_intro ? ? l1);apply (ex_intro ? ? a5);reflexivity]] + |intros 5;elim l1 + [change in H12 with (t::(l@(nth_prime n1::a4)) = nth_prime (S n1)::a5); + destruct H12;cut (l = []) + [rewrite > Hcut2;reflexivity + |change in H11 with (sorted_gt (nth_prime (S n1)::(l@(nth_prime n1::a4)))); + generalize in match H11;generalize in match H8;cases l;intros + [reflexivity + |lapply (sorted_cons_to_sorted ? ? ? H13); + lapply (sorted_to_minimum ? ? ? H13 n2) + [simplify in Hletin2;lapply (sorted_to_minimum ? ? ? Hletin2 (nth_prime n1)) + [unfold in Hletin3;unfold in Hletin4; + elim (lt_nth_prime_to_not_prime ? ? Hletin4 Hletin3); + apply H12; + apply (ex_intro ? ? [nth_prime (S n1)]); + apply (ex_intro ? ? (l2@(nth_prime n1::a4))); + reflexivity + |apply (ex_intro ? ? l2);apply (ex_intro ? ? a4);reflexivity] + |simplify;apply in_list_head]]] + |change in H13 with (t::(l@(nth_prime n1::a4)) = t1::(l2@(nth_prime (S n1)::a5))); + destruct H13;apply (H7 l2 ? ? Hcut3) + [intros;apply H8;simplify;apply in_list_cons; + assumption + |simplify in H12; + apply (sorted_cons_to_sorted ? ? ? H12)]]]] + rewrite > Hcut2 in ⊢ (? ? ? (? ? ? (? ? ? %))); + apply H10 + |apply (trans_le ? ? ? Hletin);apply lt_to_le; + apply (trans_le ? ? ? H5 Hcut) + |apply prime_nth_prime] + |rewrite > H3;assumption + |apply prime_nth_prime]] + |apply le_times_r;assumption] + |apply prime_nth_prime + |rewrite < H3;apply increasing_nth_prime]]] + |assumption] +qed. + lemma not_not_bertrand_to_bertrand1: \forall n. \lnot (not_bertrand n) \to \forall x. n \le x \to x \le 2*n \to (\forall p.x < p \to p \le 2*n \to \not (prime p)) @@ -1022,7 +1375,7 @@ rewrite > log_exp ] qed. -theorem le_to_bertrand: +theorem le_to_bertrand2: \forall n. (exp 2 8) \le n \to bertrand n. intros. apply not_not_bertrand_to_bertrand.unfold.intro. @@ -1047,6 +1400,13 @@ absurd (2*n / 3 \le (sqrt(2*n)/2)*S(log 2 (2*n))) ] qed. +theorem bertrand_n : +\forall n. O < n \to bertrand n. +intros;elim (decidable_le n 256) + [apply le_to_bertrand;assumption + |apply le_to_bertrand2;apply lt_to_le;apply not_le_to_lt;apply H1] +qed. + (* test theorem mod_exp: eqb (mod (exp 2 8) 13) O = false. reflexivity.