include "nat/sqrt.ma".
include "nat/chebyshev_teta.ma".
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
+ [ 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 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;elim l in H ⊢ %
+ [reflexivity
+ |change in H1 with (andb (checker (a::l1)) (leb t (a+(a+O))) = true);
+ apply (andb_true_true ? ? H1)]
+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.
\exists p.n < p \land p \le 2*n \land (prime p).
definition not_bertrand \def \lambda n.
\forall p.n < p \to p \le 2*n \to \not (prime p).
+(*
+lemma list_of_primes_SO: \forall l.list_of_primes 1 l \to
+l = [].
+intro.cases l;intros
+ [reflexivity
+ |apply False_ind.unfold in H.
+ absurd ((prime n) \land n \le 1)
+ [apply H.
+ apply in_list_head
+ |intro.elim H1.
+ elim H2.
+ apply (lt_to_not_le ? ? H4 H3)
+ ]
+ ]
+qed.
+*)
+
+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.
+
+theorem list_of_primes_to_bertrand: \forall n,pn,l.0 < n \to prime pn \to n <pn \to
+list_of_primes pn l \to
+(\forall p. prime p \to p \le pn \to in_list nat p l) \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) \to bertrand n.
+intros.
+elim (min_prim n).
+apply (ex_intro ? ? a).
+elim H6.clear H6.elim H7.clear H7.
+split
+ [split
+ [assumption
+ |elim (le_to_or_lt_eq ? ? (prime_to_lt_SO ? H9))
+ [elim (H5 a)
+ [elim H10.clear H10.elim H11.clear H11.
+ apply (trans_le ? ? ? H12).
+ apply le_times_r.
+ apply H8
+ [unfold in H3.
+ elim (H3 a1 H10).
+ assumption
+ |assumption
+ ]
+ |apply H4
+ [assumption
+ |apply not_lt_to_le.intro.
+ apply (lt_to_not_le ? ? H2).
+ apply H8;assumption
+ ]
+ |assumption
+ ]
+ |rewrite < H7.
+ apply O_lt_const_to_le_times_const.
+ assumption
+ ]
+ ]
+ |assumption
+ ]
+qed.
+
+let rec check_list l \def
+ match l with
+ [ nil \Rightarrow true
+ | cons (hd:nat) tl \Rightarrow
+ match tl with
+ [ nil \Rightarrow eqb hd 2
+ | cons hd1 tl1 \Rightarrow
+ (leb (S hd1) hd \land leb hd (2*hd1) \land check_list tl)
+ ]
+ ]
+.
+
+lemma check_list1: \forall n,m,l.(check_list (n::m::l)) = true \to
+m < n \land n \le 2*m \land (check_list (m::l)) = true \land ((check_list l) = true).
+intros 3.
+change in ⊢ (? ? % ?→?) with (leb (S m) n \land leb n (2*m) \land check_list (m::l)).
+intro.
+lapply (andb_true_true ? ? H) as H1.
+lapply (andb_true_true_r ? ? H) as H2.clear H.
+lapply (andb_true_true ? ? H1) as H3.
+lapply (andb_true_true_r ? ? H1) as H4.clear H1.
+split
+ [split
+ [split
+ [apply leb_true_to_le.assumption
+ |apply leb_true_to_le.assumption
+ ]
+ |assumption
+ ]
+ |generalize in match H2.
+ cases l
+ [intro.reflexivity
+ |change in ⊢ (? ? % ?→?) with (leb (S n1) m \land leb m (2*n1) \land check_list (n1::l1)).
+ intro.
+ lapply (andb_true_true_r ? ? H) as H2.
+ assumption
+ ]
+ ]
+qed.
+
+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
+ ]
+ ]
+ ]
+ ]
+qed.
+
+(* qualcosa che non va con gli S *)
+lemma le_to_bertrand : \forall n.O < n \to n \leq exp 2 8 \to bertrand n.
+intros.
+apply (list_of_primes_to_bertrand ? (S(exp 2 8)) (sieve (S(exp 2 8))))
+ [assumption
+ |apply primeb_true_to_prime.reflexivity
+ |apply (le_to_lt_to_lt ? ? ? H1).
+ apply le_n
+ |lapply (sieve_sound1 (S(exp 2 8))) as H
+ [elim H.assumption
+ |apply leb_true_to_le.reflexivity
+ ]
+ |intros.apply (sieve_sound2 ? ? H3 H2)
+ |apply check_list2.
+ reflexivity
+ ]
+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*)
+
+(* old proof by Wilmer
+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))
]
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.
]
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.
projects / helm.git / blobdiff