1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / Matita is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 include "nat/sqrt.ma".
16 include "nat/chebyshev_teta.ma".
17 include "nat/chebyshev.ma".
18 include "list/list.ma".
21 let rec list_divides l n \def
24 | cons (m:nat) (tl:list nat) ⇒ orb (divides_b m n) (list_divides tl n) ].
26 definition lprim : nat \to list nat \def
27 \lambda n.let rec aux m acc \def
30 | S m1 => match (list_divides acc (n-m1)) with
32 | false => aux m1 (n-m1::acc)]]
35 let rec filter A l p on l \def
38 | cons (a:A) (tl:list A) => match (p a) with
39 [ true => a::(filter A tl p)
40 | false => filter A tl p ]].
42 let rec length A (l:list A) on l \def
45 | cons (a:A) (tl:list A) => S (length A tl) ].
47 let rec list_n_aux n k \def
50 | S n1 => k::list_n_aux n1 (S k) ].
52 definition list_n : nat \to list nat \def
53 \lambda n.list_n_aux (pred n) 2.
55 let rec sieve_aux l1 l2 t on t \def
58 | S t1 => match l2 with
60 | cons n tl => sieve_aux (n::l1) (filter nat tl (\lambda x.notb (divides_b n x))) t1]].
62 definition sieve : nat \to list nat \def
63 \lambda m.sieve_aux [] (list_n m) m.
65 definition ord_list \def
67 \forall a,b,l1,l2.l = l1@(a::b::l2) \to b \leq a.
69 definition in_list \def
70 \lambda A.\lambda a:A.\lambda l:list A.
71 \exists l1,l2.l = l1@(a::l2).
73 lemma in_list_filter_to_p_true : \forall l,x,p.
74 in_list nat x (filter nat l p) \to p x = true.
75 intros;elim H;elim H1;clear H H1;generalize in match H2;generalize in match a;elim l 0
76 [simplify;intro;elim l1
77 [simplify in H;destruct H
78 |simplify in H1;destruct H1]
79 |intros;simplify in H1;apply (bool_elim ? (p t));intro;
80 rewrite > H3 in H1;simplify in H1
81 [generalize in match H1;elim l2
82 [simplify in H4;destruct H4;assumption
83 |simplify in H5;destruct H5;apply (H l3);assumption]
84 |apply (H l2);assumption]]
87 lemma in_list_cons : \forall l,x,y.in_list nat x l \to in_list nat x (y::l).
88 intros;unfold in H;unfold;elim H;elim H1;apply (ex_intro ? ? (y::a));
89 apply (ex_intro ? ? a1);simplify;rewrite < H2;reflexivity.
92 lemma in_list_tail : \forall l,x,y.in_list nat x (y::l) \to x \neq y \to in_list nat x l.
93 intros;elim H;elim H2;generalize in match H3;elim a
94 [simplify in H4;destruct H4;elim H1;reflexivity
95 |simplify in H5;destruct H5;apply (ex_intro ? ? l1);apply (ex_intro ? ? a1);
99 lemma in_list_filter : \forall l,p,x.in_list nat x (filter nat l p) \to in_list nat x l.
100 intros;elim H;elim H1;generalize in match H2;generalize in match a;elim l 0
101 [simplify;intro;elim l1
102 [simplify in H3;destruct H3
103 |simplify in H4;destruct H4]
104 |intros;simplify in H4;apply (bool_elim ? (p t));intro
105 [rewrite > H5 in H4;simplify in H4;generalize in match H4;elim l2
106 [simplify in H6;destruct H6;apply (ex_intro ? ? []);apply (ex_intro ? ? l1);
108 |simplify in H7;destruct H7;apply in_list_cons;apply (H3 ? Hcut1);]
109 |rewrite > H5 in H4;simplify in H4;apply in_list_cons;apply (H3 ? H4);]]
112 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).
113 intros;elim H;elim H2;rewrite > H3;elim a
114 [simplify;rewrite > H1;simplify;apply (ex_intro ? ? []);apply (ex_intro ? ? (filter nat a1 p));
116 |simplify;elim (p t);simplify
117 [apply in_list_cons;assumption
121 lemma in_list_head : \forall x,l.in_list nat x (x::l).
122 intros;apply (ex_intro ? ? []);apply (ex_intro ? ? l);reflexivity;
125 lemma in_list_cons_case : \forall A,x,a,l.in_list A x (a::l) \to
126 x = a \lor in_list A x l.
127 intros;elim H;elim H1;clear H H1;generalize in match H2;elim a1
128 [simplify in H;destruct H;left;reflexivity
129 |simplify in H1;destruct H1;right;
130 apply (ex_intro ? ? l1);
131 apply (ex_intro ? ? a2);
135 lemma divides_to_prime_divides : \forall n,m.1 < m \to m < n \to m \divides n \to
136 \exists p.p \leq m \land prime p \land p \divides n.
137 intros;apply (ex_intro ? ? (nth_prime (max_prime_factor m)));split
140 [apply lt_to_le;assumption
141 |apply divides_max_prime_factor_n;assumption]
142 |apply prime_nth_prime;]
143 |apply (transitive_divides ? ? ? ? H2);apply divides_max_prime_factor_n;
148 lemma le_length_filter : \forall A,l,p.length A (filter A l p) \leq length A l.
151 |simplify;apply (bool_elim ? (p t));intro
152 [simplify;apply le_S_S;assumption
153 |simplify;apply le_S;assumption]]
156 inductive sorted (P:nat \to nat \to Prop): list nat \to Prop \def
157 | sort_nil : sorted P []
158 | sort_cons : \forall x,l.sorted P l \to (\forall y.in_list ? y l \to P x y)
161 definition sorted_lt : list nat \to Prop \def \lambda l.sorted lt l.
163 definition sorted_gt : list nat \to Prop \def \lambda l.sorted gt l.
165 lemma sorted_cons_to_sorted : \forall P,x,l.sorted P (x::l) \to sorted P l.
166 intros;inversion H;intros
168 |destruct H4;assumption]
171 lemma sorted_to_minimum : \forall P,x,l.sorted P (x::l) \to
172 \forall y.in_list ? y l \to P x y.
173 intros;inversion H;intros;
175 |destruct H5;apply H4;assumption]
178 lemma not_in_list_nil : \forall A,a.\lnot in_list A a [].
179 intros;intro;elim H;elim H1;generalize in match H2;elim a1
180 [simplify in H3;destruct H3
181 |simplify in H4;destruct H4]
184 lemma sieve_prime : \forall t,k,l2,l1.
185 (\forall p.(in_list ? p l1 \to prime p \land p \leq k \land \forall x.in_list ? x l2 \to p < x) \land
186 (prime p \to p \leq k \to (\forall x.in_list ? x l2 \to p < x) \to in_list ? p l1)) \to
187 (\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
188 (2 \leq x \to x \leq k \to (\forall p.in_list ? p l1 \to \lnot p \divides x) \to
190 length ? l2 \leq t \to
193 sorted_gt (sieve_aux l1 l2 t) \land
194 \forall p.(in_list ? p (sieve_aux l1 l2 t) \to prime p \land p \leq k) \land
195 (prime p \to p \leq k \to in_list ? p (sieve_aux l1 l2 t)).
197 [intros;cut (l2 = [])
198 [|generalize in match H2;elim l2
200 |simplify in H6;elim (not_le_Sn_O ? H6)]]
203 |intro;elim (H p);split;intros
204 [elim (H5 H7);assumption
205 |apply (H6 H7 H8);rewrite > Hcut;intros;elim (not_in_list_nil ? ? H9)]]
209 |intro;elim (H1 p);split;intros
210 [elim (H6 H8);assumption
211 |apply (H7 H8 H9);intros;elim (not_in_list_nil ? ? H10)]]
212 |simplify;elim (H k (filter ? l (\lambda x.notb (divides_b t1 x))) (t1::l1))
217 [elim (in_list_cons_case ? ? ? ? H7);
221 [elim (H3 t1);elim H9
224 |intros;elim (le_to_or_lt_eq ? ? (divides_to_le ? ? ? H9))
225 [elim (divides_to_prime_divides ? ? H10 H11 H9);elim H12;
226 elim H13;clear H13 H12;elim (H3 t1);elim H12
227 [clear H13 H12;elim (H18 ? ? H14);elim (H2 a);
230 |elim H17;apply (trans_le ? ? ? ? H20);
231 apply (trans_le ? ? ? H15);
232 apply lt_to_le;assumption
233 |intros;apply (trans_le ? (S m))
234 [apply le_S_S;assumption
235 |apply (trans_le ? ? ? H11);
236 elim (in_list_cons_case ? ? ? ? H19)
237 [rewrite > H20;apply le_n
238 |apply lt_to_le;apply (sorted_to_minimum ? ? ? H6);assumption]]]
239 |unfold;apply (ex_intro ? ? []);
240 apply (ex_intro ? ? l);
242 |elim (H3 t1);elim H11
243 [elim H13;apply lt_to_le;assumption
246 |elim (H3 t1);elim H9
248 |apply (ex_intro ? ? []);apply (ex_intro ? ? l);reflexivity]]
249 |intros;elim (le_to_or_lt_eq t1 x)
251 |rewrite > H10 in H9;lapply (in_list_filter_to_p_true ? ? ? H9);
252 lapply (divides_n_n x);
253 rewrite > (divides_to_divides_b_true ? ? ? Hletin1) in Hletin
254 [simplify in Hletin;destruct Hletin
255 |rewrite < H10;elim (H3 t1);elim H11
256 [elim H13;apply lt_to_le;assumption
257 |apply in_list_head]]
258 |apply lt_to_le;apply (sorted_to_minimum ? ? ? H6);apply (in_list_filter ? ? ? H9)]]
259 |elim (H2 p);elim (H9 H8);split
261 |intros;apply H12;apply in_list_cons;apply (in_list_filter ? ? ? H13)]]
262 |elim (decidable_eq_nat p t1)
263 [rewrite > H10;apply (ex_intro ? ? []);apply (ex_intro ? ? l1);
265 |apply in_list_cons;elim (H2 p);apply (H12 H7 H8);intros;
266 apply (trans_le ? t1)
267 [elim (decidable_lt p t1)
269 |lapply (not_lt_to_le ? ? H14);
270 lapply (decidable_divides t1 p)
272 [elim H7;lapply (H17 ? H15)
273 [elim H10;symmetry;assumption
274 |elim (H3 t1);elim H18
276 |apply in_list_head]]
277 |elim (Not_lt_n_n p);apply H9;apply in_list_filter_r
278 [elim (H3 p);apply (in_list_tail ? ? t1)
280 [apply prime_to_lt_SO;assumption
282 |intros;elim H7;intro;lapply (H20 ? H21)
283 [rewrite > Hletin2 in H18;elim (H11 H18);
285 [elim (lt_to_not_le ? ? Hletin3 Hletin)
286 |apply (ex_intro ? ? []);apply (ex_intro ? ? l);
288 |apply prime_to_lt_SO;elim (H2 p1);elim (H22 H18);
289 elim H24;assumption]]
290 |unfold;intro;apply H15;rewrite > H18;apply divides_n_n]
291 |rewrite > (not_divides_to_divides_b_false ? ? ? H15);
293 |elim (H3 t1);elim H16
294 [elim H18;apply lt_to_le;assumption
295 |apply in_list_head]]]]
296 |elim (H3 t1);elim H15
297 [elim H17;apply lt_to_le;assumption
298 |apply in_list_head]]]
299 |elim (in_list_cons_case ? ? ? ? H13)
300 [rewrite > H14;apply le_n
301 |apply lt_to_le;apply (sorted_to_minimum ? ? ? H6);assumption]]]]
302 |elim (H3 x);split;intros;
306 |apply in_list_cons;apply (in_list_filter ? ? ? H9)]
307 |intros;elim (in_list_cons_case ? ? ? ? H10)
308 [rewrite > H11;intro;lapply (in_list_filter_to_p_true ? ? ? H9);
309 rewrite > (divides_to_divides_b_true ? ? ? H12) in Hletin
310 [simplify in Hletin;destruct Hletin
311 |elim (H3 t1);elim H13
312 [elim H15;apply lt_to_le;assumption
313 |apply in_list_head]]
315 [apply H13;assumption
316 |apply in_list_cons;apply (in_list_filter ? ? ? H9)]]]
317 |elim (in_list_cons_case ? ? ? ? (H8 ? ? ?))
319 [rewrite > H12;apply in_list_head
323 |intros;apply H11;apply in_list_cons;assumption
324 |apply in_list_filter_r;
327 [rewrite > (not_divides_to_divides_b_false ? ? ? Hletin);
329 |elim (H3 t1);elim H13
330 [elim H15;apply lt_to_le;assumption
331 |apply in_list_head]]
332 |apply in_list_head]]]]
333 |apply (trans_le ? ? ? (le_length_filter ? ? ?));apply le_S_S_to_le;
337 |intros;unfold;elim (H2 y);elim (H8 H7);
338 apply H11;apply in_list_head]
339 |generalize in match (sorted_cons_to_sorted ? ? ? H6);elim l
341 |simplify;elim (notb (divides_b t1 t2));simplify
342 [lapply (sorted_cons_to_sorted ? ? ? H8);lapply (H7 Hletin);
343 apply (sort_cons ? ? ? Hletin1);intros;
344 apply (sorted_to_minimum ? ? ? H8);apply (in_list_filter ? ? ? H9);
345 |apply H7;apply (sorted_cons_to_sorted ? ? ? H8)]]]]]
348 lemma in_list_singleton_to_eq : \forall A,x,y.in_list A x [y] \to x = y.
349 intros;elim H;elim H1;generalize in match H2;elim a
350 [simplify in H3;destruct H3;reflexivity
351 |simplify in H4;destruct H4;generalize in match Hcut1;elim l
352 [simplify in H4;destruct H4
353 |simplify in H5;destruct H5]]
356 lemma le_list_n_aux_k_k : \forall n,m,k.in_list ? n (list_n_aux m k) \to
359 [simplify in H;elim (not_in_list_nil ? ? H)
360 |simplify in H1;elim H1;elim H2;generalize in match H3;elim a
361 [simplify in H4;destruct H4;apply le_n
362 |simplify in H5;destruct H5;apply lt_to_le;apply (H (S k));
363 apply (ex_intro ? ? l);apply (ex_intro ? ? a1);assumption]]
366 lemma in_list_SSO_list_n : \forall n.2 \leq n \to in_list ? 2 (list_n n).
368 [simplify;apply (ex_intro ? ? []);apply (ex_intro ? ? []);
370 |generalize in match H2;elim H1
371 [simplify;apply (ex_intro ? ? []);apply (ex_intro ? ? [3]);simplify;reflexivity
372 |simplify;apply (ex_intro ? ? []);apply (ex_intro ? ? (list_n_aux n2 3));
373 simplify;reflexivity]]
376 lemma le_SSO_list_n : \forall m,n.in_list nat n (list_n m) \to 2 \leq n.
377 intros;unfold list_n in H;apply (le_list_n_aux_k_k ? ? ? H);
380 lemma le_list_n_aux : \forall n,m,k.in_list ? n (list_n_aux m k) \to n \leq k+m-1.
382 [simplify in H;elim (not_in_list_nil ? ? H)
383 |simplify in H1;elim H1;elim H2;generalize in match H3;elim a
384 [simplify in H4;destruct H4;rewrite < plus_n_Sm;simplify;rewrite < minus_n_O;
385 rewrite > plus_n_O in \vdash (? % ?);apply le_plus_r;apply le_O_n
386 |simplify in H5;destruct H5;rewrite < plus_n_Sm;apply (H (S k));
387 apply (ex_intro ? ? l);apply (ex_intro ? ? a1);assumption]]
390 lemma le_list_n : \forall n,m.in_list ? n (list_n m) \to n \leq m.
391 intros;unfold list_n in H;lapply (le_list_n_aux ? ? ? H);
392 simplify in Hletin;generalize in match H;generalize in match Hletin;elim m
393 [simplify in H2;elim (not_in_list_nil ? ? H2)
394 |simplify in H2;assumption]
398 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).
400 [intros;simplify;rewrite < plus_n_Sm in H2;simplify in H2;
401 rewrite < plus_n_O in H2;rewrite < minus_n_O in H2;
402 rewrite > (antisymmetric_le k n H1 H2);apply in_list_head
403 |intros 5;simplify;generalize in match H2;elim H3
405 |apply in_list_cons;apply H6
406 [apply le_S_S;assumption
407 |rewrite < plus_n_Sm in H7;apply H7]]]
410 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).
411 intros;unfold list_n;apply le_list_n_aux_r
414 |generalize in match H4;elim H3;
416 |simplify in H7;apply le_S;assumption]]
418 |simplify;generalize in match H2;elim H;simplify;assumption]
421 lemma le_length_list_n : \forall n. length ? (list_n n) \leq n.
422 intro;cut (\forall n,k.length ? (list_n_aux n k) \leq (S n))
426 |intro;elim n1;simplify
428 |apply le_S_S;apply H]]
431 lemma sorted_list_n_aux : \forall n,k.sorted_lt (list_n_aux n k).
433 [simplify;intro;apply sort_nil
434 |intro;simplify;intros 2;apply sort_cons
436 |intros;lapply (le_list_n_aux_k_k ? ? ? H1);assumption]]
439 definition list_of_primes \def \lambda n.\lambda l.
440 \forall p.in_list nat p l \to prime p \land p \leq n.
442 lemma sieve_sound1 : \forall n.2 \leq n \to
443 sorted_gt (sieve n) \land list_of_primes n (sieve n).
444 intros;elim (sieve_prime n n (list_n n) [])
447 |intro;unfold sieve in H3;elim (H2 p);elim (H3 H5);split;assumption]
449 [elim (not_in_list_nil ? ? H1)
450 |lapply (lt_to_not_le ? ? (H3 2 ?))
451 [apply in_list_SSO_list_n;assumption
452 |elim Hletin;apply prime_to_lt_SO;assumption]]
456 [apply (le_SSO_list_n ? ? H1)
457 |apply (le_list_n ? ? H1)]
458 |intros;elim (not_in_list_nil ? ? H2)]
459 |apply le_list_n_r;assumption]
460 |apply le_length_list_n
466 |simplify;apply sort_cons
467 [apply sorted_list_n_aux
468 |intros;lapply (le_list_n_aux_k_k ? ? ? H3);
472 lemma sieve_sorted : \forall n.sorted_gt (sieve n).
473 intros;elim (decidable_le 2 n)
474 [elim (sieve_sound1 ? H);assumption
475 |generalize in match (le_S_S_to_le ? ? (not_le_to_lt ? ? H));cases n
476 [intro;apply sort_nil
477 |intros;lapply (le_S_S_to_le ? ? H1);rewrite < (le_n_O_to_eq ? Hletin);
481 lemma in_list_sieve_to_prime : \forall n,p.2 \leq n \to in_list ? p (sieve n) \to
483 intros;elim (sieve_sound1 ? H);elim (H3 ? H1);assumption;
486 lemma in_list_sieve_to_leq : \forall n,p.2 \leq n \to in_list ? p (sieve n) \to
488 intros;elim (sieve_sound1 ? H);elim (H3 ? H1);assumption;
491 lemma sieve_sound2 : \forall n,p.p \leq n \to prime p \to in_list ? p (sieve n).
492 intros;elim (sieve_prime n n (list_n n) [])
493 [elim (H3 p);apply H5;assumption
495 [intro;elim (not_in_list_nil ? ? H2)
496 |intros;lapply (lt_to_not_le ? ? (H4 2 ?))
497 [apply in_list_SSO_list_n;apply (trans_le ? ? ? ? H);
498 apply prime_to_lt_SO;assumption
499 |elim Hletin;apply prime_to_lt_SO;assumption]]
503 [apply (le_SSO_list_n ? ? H2)
504 |apply (le_list_n ? ? H2)]
505 |elim (not_in_list_nil ? ? H3)]
507 [apply (trans_le ? ? ? H2 H3)
510 |apply le_length_list_n
516 |simplify;apply sort_cons
517 [apply sorted_list_n_aux
518 |intros;lapply (le_list_n_aux_k_k ? ? ? H4);
522 let rec checker l \def
525 | cons h1 t1 => match t1 with
527 | cons h2 t2 => (andb (checker t1) (leb h1 (2*h2))) ]].
529 lemma checker_cons : \forall t,l.checker (t::l) = true \to checker l = true.
530 intros 2;simplify;intro;generalize in match H;elim l
532 |change in H2 with (andb (checker (t1::l1)) (leb t (t1+(t1+O))) = true);
533 apply (andb_true_true ? ? H2)]
536 theorem checker_sound : \forall l1,l2,l,x,y.l = l1@(x::y::l2) \to
537 checker l = true \to x \leq 2*y.
539 [simplify;intros 5;rewrite > H;simplify;intro;
540 apply leb_true_to_le;apply (andb_true_true_r ? ? H1);
541 |simplify;intros;rewrite > H1 in H2;lapply (checker_cons ? ? H2);
542 apply (H l2 ? ? ? ? Hletin);reflexivity]
545 definition bertrand \def \lambda n.
546 \exists p.n < p \land p \le 2*n \land (prime p).
548 definition not_bertrand \def \lambda n.
549 \forall p.n < p \to p \le 2*n \to \not (prime p).
552 lemma list_of_primes_SO: \forall l.list_of_primes 1 l \to
556 |apply False_ind.unfold in H.
557 absurd ((prime n) \land n \le 1)
562 apply (lt_to_not_le ? ? H4 H3)
568 lemma min_prim : \forall n.\exists p. n < p \land prime p \land
569 \forall q.prime q \to q < p \to q \leq n.
570 intro;elim (le_to_or_lt_eq ? ? (le_O_n n))
571 [apply (ex_intro ? ? (min_aux (S (n!)) (S n) primeb));
575 |apply primeb_true_to_prime;apply f_min_aux_true;elim (ex_prime n);
576 [apply (ex_intro ? ? a);elim H1;elim H2;split
579 |rewrite > plus_n_O;apply le_plus
582 |apply prime_to_primeb_true;assumption]
584 |intros;apply not_lt_to_le;intro;lapply (lt_min_aux_to_false ? ? ? ? H3 H2);
585 rewrite > (prime_to_primeb_true ? H1) in Hletin;destruct Hletin]
586 |apply (ex_intro ? ? 2);split
588 [rewrite < H;apply lt_O_S
589 |apply primeb_true_to_prime;reflexivity]
590 |intros;elim (lt_to_not_le ? ? H2);apply prime_to_lt_SO;assumption]]
593 theorem list_of_primes_to_bertrand: \forall n,pn,l.0 < n \to prime pn \to n <pn \to
594 list_of_primes pn l \to
595 (\forall p. prime p \to p \le pn \to in_list nat p l) \to
596 (\forall p. in_list nat p l \to 2 < p \to
597 \exists pp. in_list nat pp l \land pp < p \land p \le 2*pp) \to bertrand n.
600 apply (ex_intro ? ? a).
601 elim H6.clear H6.elim H7.clear H7.
605 |elim (le_to_or_lt_eq ? ? (prime_to_lt_SO ? H9))
607 [elim H10.clear H10.elim H11.clear H11.
608 apply (trans_le ? ? ? H12).
618 |apply not_lt_to_le.intro.
619 apply (lt_to_not_le ? ? H2).
625 apply O_lt_const_to_le_times_const.
633 let rec check_list l \def
635 [ nil \Rightarrow true
636 | cons (hd:nat) tl \Rightarrow
638 [ nil \Rightarrow eqb hd 2
639 | cons hd1 tl1 \Rightarrow
640 (leb (S hd1) hd \land leb hd (2*hd1) \land check_list tl)
645 lemma check_list1: \forall n,m,l.(check_list (n::m::l)) = true \to
646 m < n \land n \le 2*m \land (check_list (m::l)) = true \land ((check_list l) = true).
648 change in ⊢ (? ? % ?→?) with (leb (S m) n \land leb n (2*m) \land check_list (m::l)).
650 lapply (andb_true_true ? ? H) as H1.
651 lapply (andb_true_true_r ? ? H) as H2.clear H.
652 lapply (andb_true_true ? ? H1) as H3.
653 lapply (andb_true_true_r ? ? H1) as H4.clear H1.
657 [apply leb_true_to_le.assumption
658 |apply leb_true_to_le.assumption
662 |generalize in match H2.
665 |change in ⊢ (? ? % ?→?) with (leb (S n1) m \land leb m (2*n1) \land check_list (n1::l1)).
667 lapply (andb_true_true_r ? ? H) as H2.
673 theorem check_list2: \forall l. check_list l = true \to
674 \forall p. in_list nat p l \to 2 < p \to
675 \exists pp. in_list nat pp l \land pp < p \land p \le 2*pp.
677 [intros.apply False_ind.apply (not_in_list_nil ? ? H1)
679 [lapply (in_list_singleton_to_eq ? ? ? H2) as H4.
681 apply (lt_to_not_eq ? ? H3).
682 apply sym_eq.apply eqb_true_to_eq.
683 rewrite > H4.apply H1
684 |elim (check_list1 ? ? ? H1).clear H1.
687 elim (in_list_cons_case ? ? ? ? H2)
688 [apply (ex_intro ? ? n).
691 [apply in_list_cons.apply in_list_head
692 |rewrite > H1.assumption
694 |rewrite > H1.assumption
696 |elim (H H6 p H1 H3).clear H.
697 apply (ex_intro ? ? a).
702 [apply in_list_cons.assumption
712 (* qualcosa che non va con gli S *)
713 lemma le_to_bertrand : \forall n.O < n \to n \leq exp 2 8 \to bertrand n.
715 apply (list_of_primes_to_bertrand ? (S(exp 2 8)) (sieve (S(exp 2 8))))
717 |apply primeb_true_to_prime.reflexivity
718 |apply (le_to_lt_to_lt ? ? ? H1).
720 |lapply (sieve_sound1 (S(exp 2 8))) as H
722 |apply leb_true_to_le.reflexivity
724 |intros.apply (sieve_sound2 ? ? H3 H2)
725 |(* se tolgo l'argomento l'apply diventa lenta *)
726 apply (check_list2 (sieve (S(exp 2 8)))).
731 (*lemma pippo : \forall k,n.in_list ? (nth_prime (S k)) (sieve n) \to
732 \exists l.sieve n = l@((nth_prime (S k))::(sieve (nth_prime k))).
733 intros;elim H;elim H1;clear H H1;apply (ex_intro ? ? a);
734 cut (a1 = sieve (nth_prime k))
735 [rewrite < Hcut;assumption
736 |lapply (sieve_sorted n);generalize in match H2*)
738 (* old proof by Wilmer
739 lemma le_to_bertrand : \forall n.O < n \to n \leq exp 2 8 \to bertrand n.
741 elim (min_prim n);apply (ex_intro ? ? a);elim H2;elim H3;clear H2 H3;
743 [|apply not_lt_to_le;intro;apply (le_to_not_lt ? ? H1);apply (H4 ? ? H2);
744 apply primeb_true_to_prime;reflexivity]
748 |elim (prime_to_nth_prime a H6);generalize in match H2;cases a1
749 [simplify;intro;rewrite < H3;rewrite < plus_n_O;
750 change in \vdash (? % ?) with (1+1);apply le_plus;assumption
751 |intro;lapply (H4 (nth_prime n1))
752 [apply (trans_le ? (2*(nth_prime n1)))
754 cut (\exists l1,l2.sieve 257 = l1@((nth_prime (S n1))::((nth_prime n1)::l2)))
755 [elim Hcut1;elim H7;clear Hcut1 H7;
756 apply (checker_sound a2 a3 (sieve 257))
759 |elim (sieve_sound2 257 (nth_prime (S n1)) ? ?)
760 [elim (sieve_sound2 257 (nth_prime n1) ? ?)
762 cut (\forall p.in_list ? p (a3@(nth_prime n1::a4)) \to prime p)
763 [|rewrite < H9;intros;apply (in_list_sieve_to_prime 257 p ? H10);
764 apply leb_true_to_le;reflexivity]
765 apply (ex_intro ? ? a2);apply (ex_intro ? ? a4);
767 cut ((nth_prime n1)::a4 = a5)
768 [|generalize in match H10;
769 lapply (sieve_sorted 257);
770 generalize in match Hletin1;
771 rewrite > H9 in ⊢ (? %→? ? % ?→?);
772 generalize in match Hcut1;
773 generalize in match a2;
776 [change in H11 with (nth_prime n1::a4 = nth_prime (S n1)::a5);
777 destruct H11;elim (eq_to_not_lt ? ? Hcut2);
778 apply increasing_nth_prime
779 |change in H12 with (nth_prime n1::a4 = t::(l1@(nth_prime (S n1)::a5)));
781 change in H11 with (sorted_gt (nth_prime n1::l1@(nth_prime (S n1)::a5)));
782 lapply (sorted_to_minimum ? ? ? H11 (nth_prime (S n1)))
783 [unfold in Hletin2;elim (le_to_not_lt ? ? (lt_to_le ? ? Hletin2));
784 apply increasing_nth_prime
785 |apply (ex_intro ? ? l1);apply (ex_intro ? ? a5);reflexivity]]
787 [change in H12 with (t::(l@(nth_prime n1::a4)) = nth_prime (S n1)::a5);
788 destruct H12;cut (l = [])
789 [rewrite > Hcut2;reflexivity
790 |change in H11 with (sorted_gt (nth_prime (S n1)::(l@(nth_prime n1::a4))));
791 generalize in match H11;generalize in match H8;cases l;intros
793 |lapply (sorted_cons_to_sorted ? ? ? H13);
794 lapply (sorted_to_minimum ? ? ? H13 n2)
795 [simplify in Hletin2;lapply (sorted_to_minimum ? ? ? Hletin2 (nth_prime n1))
796 [unfold in Hletin3;unfold in Hletin4;
797 elim (lt_nth_prime_to_not_prime ? ? Hletin4 Hletin3);
799 apply (ex_intro ? ? [nth_prime (S n1)]);
800 apply (ex_intro ? ? (l2@(nth_prime n1::a4)));
802 |apply (ex_intro ? ? l2);apply (ex_intro ? ? a4);reflexivity]
803 |simplify;apply in_list_head]]]
804 |change in H13 with (t::(l@(nth_prime n1::a4)) = t1::(l2@(nth_prime (S n1)::a5)));
805 destruct H13;apply (H7 l2 ? ? Hcut3)
806 [intros;apply H8;simplify;apply in_list_cons;
809 apply (sorted_cons_to_sorted ? ? ? H12)]]]]
810 rewrite > Hcut2 in ⊢ (? ? ? (? ? ? (? ? ? %)));
812 |apply (trans_le ? ? ? Hletin);apply lt_to_le;
813 apply (trans_le ? ? ? H5 Hcut)
814 |apply prime_nth_prime]
815 |rewrite > H3;assumption
816 |apply prime_nth_prime]]
817 |apply le_times_r;assumption]
818 |apply prime_nth_prime
819 |rewrite < H3;apply increasing_nth_prime]]]
823 lemma not_not_bertrand_to_bertrand1: \forall n.
824 \lnot (not_bertrand n) \to \forall x. n \le x \to x \le 2*n \to
825 (\forall p.x < p \to p \le 2*n \to \not (prime p))
826 \to \exists p.n < p \land p \le x \land (prime p).
828 [apply False_ind.apply H.assumption
829 |apply (bool_elim ? (primeb (S n1)));intro
830 [apply (ex_intro ? ? (S n1)).
833 [apply le_S_S.assumption
836 |apply primeb_true_to_prime.assumption
841 apply (ex_intro ? ? a).
845 |apply le_S.assumption
849 |apply lt_to_le.assumption
850 |elim (le_to_or_lt_eq ? ? H7)
853 apply primeb_false_to_not_prime.
861 theorem not_not_bertrand_to_bertrand: \forall n.
862 \lnot (not_bertrand n) \to bertrand n.
863 unfold bertrand.intros.
864 apply (not_not_bertrand_to_bertrand1 ? ? (2*n))
866 |apply le_times_n.apply le_n_Sn
868 |intros.apply False_ind.
869 apply (lt_to_not_le ? ? H1 H2)
874 theorem divides_pi_p_to_divides: \forall p,n,b,g.prime p \to
875 divides p (pi_p n b g) \to \exists i. (i < n \and (b i = true \and
880 apply (le_to_not_lt p 1)
887 |apply (bool_elim ? (b n1));intro
888 [rewrite > (true_to_pi_p_Sn ? ? ? H3) in H2.
889 elim (divides_times_to_divides ? ? ? H1 H2)
890 [apply (ex_intro ? ? n1).
897 apply (ex_intro ? ? a).
899 [apply lt_to_le.apply le_S_S.assumption
903 |rewrite > (false_to_pi_p_Sn ? ? ? H3) in H2.
906 apply (ex_intro ? ? a).
908 [apply lt_to_le.apply le_S_S.assumption
915 theorem divides_B: \forall n,p.prime p \to p \divides (B n) \to
916 p \le n \land \exists i.mod (n /(exp p (S i))) 2 \neq O.
919 elim (divides_pi_p_to_divides ? ? ? ? H H1).
922 elim (divides_pi_p_to_divides ? ? ? ? H H5).clear H5.
927 [rewrite > Hcut.apply le_S_S_to_le.assumption
928 |apply (ex_intro ? ? a1).
931 change in H7:(? ? %) with (exp a ((n/(exp a (S a1))) \mod 2)).
935 [apply divides_to_le[apply lt_O_S|assumption]
936 |apply lt_to_not_le.elim H.assumption
939 |apply (divides_exp_to_eq ? ? ? H ? H7).
940 apply primeb_true_to_prime.
946 definition k \def \lambda n,p.
947 sigma_p (log p n) (λi:nat.true) (λi:nat.((n/(exp p (S i))\mod 2))).
949 theorem le_k: \forall n,p. k n p \le log p n.
950 intros.unfold k.elim (log p n)
952 |rewrite > true_to_sigma_p_Sn
953 [rewrite > plus_n_SO.
954 rewrite > sym_plus in ⊢ (? ? %).
967 \lambda n. pi_p (S n) primeb (\lambda p.(exp p (k n p))).
969 theorem eq_B_B1: \forall n. B n = B1 n.
970 intros.unfold B.unfold B1.
978 definition B_split1 \def \lambda n.
979 pi_p (S n) primeb (\lambda p.(exp p (bool_to_nat (leb (k n p) 1)* (k n p)))).
981 definition B_split2 \def \lambda n.
982 pi_p (S n) primeb (\lambda p.(exp p (bool_to_nat (leb 2 (k n p))* (k n p)))).
984 theorem eq_B1_times_B_split1_B_split2: \forall n.
985 B1 n = B_split1 n * B_split2 n.
986 intro.unfold B1.unfold B_split1.unfold B_split2.
987 rewrite < times_pi_p.
990 |intros.apply (bool_elim ? (leb (k n x) 1));intro
991 [rewrite > (lt_to_leb_false 2 (k n x))
992 [simplify.rewrite < plus_n_O.
993 rewrite < times_n_SO.reflexivity
994 |apply le_S_S.apply leb_true_to_le.assumption
996 |rewrite > (le_to_leb_true 2 (k n x))
997 [simplify.rewrite < plus_n_O.
998 rewrite < plus_n_O.reflexivity
999 |apply not_le_to_lt.apply leb_false_to_not_le.assumption
1005 lemma lt_div_to_times: \forall n,m,q. O < q \to n/q < m \to n < q*m.
1008 [apply not_le_to_lt.
1009 intro.apply (lt_to_not_le ? ? H1).
1010 apply le_times_to_le_div;assumption
1011 |apply (ltn_to_ltO ? ? H1)
1015 lemma lt_to_div_O:\forall n,m. n < m \to n / m = O.
1017 apply (div_mod_spec_to_eq n m (n/m) (n \mod m) O n)
1018 [apply div_mod_spec_div_mod.
1019 apply (ltn_to_ltO ? ? H)
1020 |apply div_mod_spec_intro
1027 (* the value of n could be smaller *)
1028 lemma k1: \forall n,p. 18 \le n \to p \le n \to 2*n/ 3 < p\to k (2*n) p = O.
1032 |rewrite > true_to_sigma_p_Sn
1036 [rewrite < exp_n_SO.
1037 cut (2*n/p = 2) as H4
1038 [rewrite > H4.reflexivity
1039 |apply lt_to_le_times_to_lt_S_to_div
1040 [apply (ltn_to_ltO ? ? H2)
1041 |rewrite < sym_times.
1044 |rewrite > sym_times in ⊢ (? ? %).
1045 apply lt_div_to_times
1051 |cut (2*n/(p)\sup(S (S n2)) = O) as H4
1052 [rewrite > H4.reflexivity
1054 apply (le_to_lt_to_lt ? (exp ((2*n)/3) 2))
1055 [apply (le_times_to_le (exp 3 2))
1056 [apply leb_true_to_le.reflexivity
1057 |rewrite > sym_times in ⊢ (? ? %).
1058 rewrite > times_exp.
1059 apply (trans_le ? (exp n 2))
1060 [rewrite < assoc_times.
1061 rewrite > exp_SSO in ⊢ (? ? %).
1064 |apply monotonic_exp1.
1065 apply (le_plus_to_le 3).
1066 change in ⊢ (? ? %) with ((S(2*n/3))*3).
1067 apply (trans_le ? (2*n))
1068 [simplify in ⊢ (? ? %).
1071 apply (trans_le ? 18 ? ? H).
1072 apply leb_true_to_le.reflexivity
1079 |apply (lt_to_le_to_lt ? (exp p 2))
1085 [apply (ltn_to_ltO ? ? H2)
1086 |apply le_S_S.apply le_S_S.apply le_O_n
1097 theorem le_B_split1_teta:\forall n.18 \le n \to not_bertrand n \to
1098 B_split1 (2*n) \le teta (2 * n / 3).
1099 intros.unfold B_split1.unfold teta.
1100 apply (trans_le ? (pi_p (S (2*n)) primeb (λp:nat.(p)\sup(bool_to_nat (eqb (k (2*n) p) 1)))))
1101 [apply le_pi_p.intros.
1103 [apply prime_to_lt_O.apply primeb_true_to_prime.assumption
1104 |apply (bool_elim ? (leb (k (2*n) i) 1));intro
1105 [elim (le_to_or_lt_eq ? ? (leb_true_to_le ? ? H4))
1106 [lapply (le_S_S_to_le ? ? H5) as H6.
1107 apply (le_n_O_elim ? H6).
1108 rewrite < times_n_O.
1110 |rewrite > (eq_to_eqb_true ? ? H5).
1111 rewrite > H5.apply le_n
1116 |apply (trans_le ? (pi_p (S (2*n/3)) primeb (λp:nat.(p)\sup(bool_to_nat (eqb (k (2*n) p) 1)))))
1117 [apply (eq_ind ? ? ? (le_n ?)).
1118 apply or_false_eq_SO_to_eq_pi_p
1120 apply le_times_to_le_div2
1122 |rewrite > sym_times in ⊢ (? ? %).
1124 apply leb_true_to_le.reflexivity
1127 unfold not_bertrand in H1.
1128 elim (decidable_le (S n) i)
1130 apply not_prime_to_primeb_false.
1133 |apply le_S_S_to_le.assumption
1139 |apply le_S_S_to_le.
1140 apply not_le_to_lt.assumption
1145 |apply le_pi_p.intros.
1146 elim (eqb (k (2*n) i) 1)
1147 [rewrite < exp_n_SO.apply le_n
1148 |simplify.apply prime_to_lt_O.
1149 apply primeb_true_to_prime.
1156 theorem le_B_split2_exp: \forall n. exp 2 7 \le n \to
1157 B_split2 (2*n) \le exp (2*n) (pred(sqrt(2*n)/2)).
1158 intros.unfold B_split2.
1160 [apply (trans_le ? (pi_p (S (sqrt (2*n))) primeb
1161 (λp:nat.(p)\sup(bool_to_nat (leb 2 (k (2*n) p))*k (2*n) p))))
1162 [apply (eq_ind ? ? ? (le_n ?)).
1163 apply or_false_eq_SO_to_eq_pi_p
1167 apply (bool_elim ? (leb 2 (k (2*n) i)));intro
1169 apply (lt_to_not_le ? ? H1).unfold sqrt.
1171 [apply le_S_S_to_le.assumption
1172 |apply le_to_leb_true.
1174 apply not_lt_to_le.intro.
1175 apply (le_to_not_lt 2 (log i (2*n)))
1176 [apply (trans_le ? (k (2*n) i))
1177 [apply leb_true_to_le.assumption
1180 |apply le_S_S.unfold log.apply f_false_to_le_max
1181 [apply (ex_intro ? ? O).split
1183 |apply le_to_leb_true.simplify.
1184 apply (trans_le ? n)
1189 |intros.apply lt_to_leb_false.
1190 apply (lt_to_le_to_lt ? (exp i 2))
1193 [apply (ltn_to_ltO ? ? H1)
1203 |apply (trans_le ? (pi_p (S (sqrt (2*n))) primeb (λp:nat.2*n)))
1204 [apply le_pi_p.intros.
1205 apply (trans_le ? (exp i (log i (2*n))))
1207 [apply prime_to_lt_O.
1208 apply primeb_true_to_prime.
1210 |apply (bool_elim ? (leb 2 (k (2*n) i)));intro
1211 [simplify in ⊢ (? (? % ?) ?).
1212 rewrite > sym_times.
1213 rewrite < times_n_SO.
1219 rewrite > (times_n_O O) in ⊢ (? % ?).
1225 |apply (trans_le ? (exp (2*n) (prim(sqrt (2*n)))))
1227 apply (eq_ind ? ? ? (le_n ?)).
1230 [rewrite > (times_n_O O) in ⊢ (? % ?).
1238 [apply (trans_le ? (2*(exp 2 7)))
1239 [apply leb_true_to_le.reflexivity
1240 |apply le_times_r.assumption
1242 |apply le_to_leb_true.
1243 apply (trans_le ? (2*(exp 2 7)))
1244 [apply leb_true_to_le.reflexivity
1245 |apply le_times_r.assumption
1252 |apply (lt_to_le_to_lt ? ? ? ? H).
1253 apply leb_true_to_le.reflexivity
1257 theorem not_bertrand_to_le_B:
1258 \forall n.exp 2 7 \le n \to not_bertrand n \to
1259 B (2*n) \le (exp 2 (2*(2 * n / 3)))*(exp (2*n) (pred(sqrt(2*n)/2))).
1262 rewrite > eq_B1_times_B_split1_B_split2.
1264 [apply (trans_le ? (teta ((2*n)/3)))
1265 [apply le_B_split1_teta
1266 [apply (trans_le ? ? ? ? H).
1267 apply leb_true_to_le.reflexivity
1272 |apply le_B_split2_exp.
1278 theorem not_bertrand_to_le1:
1279 \forall n.18 \le n \to not_bertrand n \to
1280 exp 2 (2*n) \le (exp 2 (2*(2 * n / 3)))*(exp (2*n) (S(sqrt(2*n)))).
1283 theorem le_times_div_m_m: \forall n,m. O < m \to n/m*m \le n.
1285 rewrite > (div_mod n m) in ⊢ (? ? %)
1291 theorem not_bertrand_to_le1:
1292 \forall n.exp 2 7 \le n \to not_bertrand n \to
1293 (exp 2 (2*n / 3)) \le (exp (2*n) (sqrt(2*n)/2)).
1295 apply (le_times_to_le (exp 2 (2*(2 * n / 3))))
1296 [apply lt_O_exp.apply lt_O_S
1297 |rewrite < exp_plus_times.
1298 apply (trans_le ? (exp 2 (2*n)))
1301 |rewrite < sym_plus.
1302 change in ⊢ (? % ?) with (3*(2*n/3)).
1303 rewrite > sym_times.
1304 apply le_times_div_m_m.
1308 rewrite < distr_times_plus.
1310 apply (trans_le ? ((2*n + n)/3))
1311 [apply le_plus_div.apply lt_O_S
1312 |rewrite < sym_plus.
1313 change in ⊢ (? (? % ?) ?) with (3*n).
1314 rewrite < sym_times.
1315 rewrite > lt_O_to_div_times
1321 |apply (trans_le ? (2*n*B(2*n)))
1323 apply (trans_le ? ? ? ? H).
1324 apply leb_true_to_le.reflexivity
1325 |rewrite > S_pred in ⊢ (? ? (? ? (? ? %)))
1327 rewrite < assoc_times.
1328 rewrite < sym_times in ⊢ (? ? (? % ?)).
1329 rewrite > assoc_times in ⊢ (? ? %).
1331 apply not_bertrand_to_le_B;assumption
1332 |apply le_times_to_le_div
1334 |apply (trans_le ? (sqrt (exp 2 8)))
1335 [apply leb_true_to_le.reflexivity
1336 |apply monotonic_sqrt.
1337 change in ⊢ (? % ?) with (2*(exp 2 7)).
1348 theorem not_bertrand_to_le2:
1349 \forall n.exp 2 7 \le n \to not_bertrand n \to
1350 2*n / 3 \le (sqrt(2*n)/2)*S(log 2 (2*n)).
1352 rewrite < (eq_log_exp 2)
1353 [apply (trans_le ? (log 2 ((exp (2*n) (sqrt(2*n)/2)))))
1356 |apply not_bertrand_to_le1;assumption
1365 theorem tech1: \forall a,b,c,d.O < b \to O < d \to
1366 (a/b)*(c/d) \le (a*c)/(b*d).
1368 apply le_times_to_le_div
1369 [rewrite > (times_n_O O).
1370 apply lt_times;assumption
1371 |rewrite > assoc_times.
1372 rewrite < assoc_times in ⊢ (? (? ? %) ?).
1373 rewrite < sym_times in ⊢ (? (? ? (? % ?)) ?).
1374 rewrite > assoc_times.
1375 rewrite < assoc_times.
1377 rewrite > sym_times;apply le_times_div_m_m;assumption
1381 theorem tech: \forall n. 2*(S(log 2 (2*n))) \le sqrt (2*n) \to
1382 (sqrt(2*n)/2)*S(log 2 (2*n)) \le 2*n / 4.
1384 cut (4*(S(log 2 (2*n))) \le 2* sqrt(2*n))
1385 [rewrite > sym_times.
1386 apply le_times_to_le_div
1388 |rewrite < assoc_times.
1389 apply (trans_le ? (2*sqrt(2*n)*(sqrt (2*n)/2)))
1390 [apply le_times_l.assumption
1391 |apply (trans_le ? ((2*sqrt(2*n)*(sqrt(2*n))/2)))
1392 [apply le_times_div_div_times.
1394 |rewrite > assoc_times.
1395 rewrite > sym_times.
1396 rewrite > lt_O_to_div_times.
1402 |change in ⊢ (? (? % ?) ?) with (2*2).
1403 rewrite > assoc_times.
1409 theorem lt_div_S_div: \forall n,m. O < m \to exp m 2 \le n \to
1412 apply lt_times_to_lt_div.
1413 apply (lt_to_le_to_lt ? (S(n/m)*m))
1414 [apply lt_div_S.assumption
1415 |rewrite > sym_times in ⊢ (? ? %). simplify.
1416 rewrite > sym_times in ⊢ (? ? (? ? %)).
1418 apply le_times_to_le_div
1426 theorem exp_plus_SSO: \forall a,b. exp (a+b) 2 = (exp a 2) + 2*a*b + (exp b 2).
1429 rewrite > distr_times_plus.
1430 rewrite > times_plus_l.
1432 rewrite > assoc_plus.
1433 rewrite > assoc_plus.
1435 rewrite > times_plus_l.
1437 rewrite < assoc_plus.
1438 rewrite < sym_times.
1439 rewrite > plus_n_O in ⊢ (? ? (? (? ? %) ?) ?).
1440 rewrite > assoc_times.
1441 apply eq_f2;reflexivity.
1444 theorem tech3: \forall n. (exp 2 8) \le n \to 2*(S(log 2 (2*n))) \le sqrt (2*n).
1446 lapply (le_log 2 ? ? (le_n ?) H) as H1.
1447 rewrite > exp_n_SO in ⊢ (? (? ? (? (? ? (? % ?)))) ?).
1449 [rewrite > sym_plus.
1450 rewrite > plus_n_Sm.
1454 apply (trans_le ? (2*log 2 n))
1455 [rewrite < times_SSO_n.
1457 apply (trans_le ? 8)
1458 [apply leb_true_to_le.reflexivity
1459 |rewrite < (eq_log_exp 2)
1464 |apply (trans_le ? ? ? ? (le_exp_log 2 ? ? )).
1465 apply le_times_SSO_n_exp_SSO_n.
1466 apply (lt_to_le_to_lt ? ? ? ? H).
1467 apply leb_true_to_le.reflexivity
1469 |apply le_to_leb_true.
1470 rewrite > assoc_times.
1472 rewrite > sym_times.
1473 rewrite > assoc_times.
1475 rewrite > exp_plus_SSO.
1476 rewrite > distr_times_plus.
1477 rewrite > distr_times_plus.
1478 rewrite > assoc_plus.
1479 apply (trans_le ? (4*exp (log 2 n) 2))
1480 [change in ⊢ (? ? (? % ?)) with (2*2).
1481 rewrite > assoc_times in ⊢ (? ? %).
1482 rewrite < times_SSO_n in ⊢ (? ? %).
1484 rewrite < times_SSO_n in ⊢ (? ? %).
1486 [rewrite > sym_times in ⊢ (? (? ? %) ?).
1487 rewrite < assoc_times.
1488 rewrite < assoc_times.
1489 change in ⊢ (? (? % ?) ?) with 8.
1492 (* strange things here *)
1493 rewrite < (eq_log_exp 2)
1497 |apply (trans_le ? (log 2 n))
1498 [change in ⊢ (? % ?) with 8.
1499 rewrite < (eq_log_exp 2)
1503 |rewrite > exp_n_SO in ⊢ (? % ?).
1506 [apply (lt_to_le_to_lt ? ? ? ? H).
1507 apply leb_true_to_le.reflexivity
1508 |apply (lt_to_le_to_lt ? ? ? ? H).
1509 apply leb_true_to_le.reflexivity
1515 |change in ⊢ (? (? % ?) ?) with (exp 2 2).
1516 apply (trans_le ? ? ? ? (le_exp_log 2 ? ?))
1517 [apply le_times_exp_n_SSO_exp_SSO_n
1519 |change in ⊢ (? % ?) with 8.
1520 rewrite < (eq_log_exp 2)
1525 |apply (lt_to_le_to_lt ? ? ? ? H).
1526 apply leb_true_to_le.reflexivity
1531 |apply (lt_to_le_to_lt ? ? ? ? H).
1532 apply leb_true_to_le.reflexivity
1536 theorem le_to_bertrand2:
1537 \forall n. (exp 2 8) \le n \to bertrand n.
1539 apply not_not_bertrand_to_bertrand.unfold.intro.
1540 absurd (2*n / 3 \le (sqrt(2*n)/2)*S(log 2 (2*n)))
1541 [apply not_bertrand_to_le2
1542 [apply (trans_le ? ? ? ? H).
1549 |apply lt_to_not_le.
1550 apply (le_to_lt_to_lt ? ? ? ? (lt_div_S_div ? ? ? ?))
1551 [apply tech.apply tech3.assumption
1553 |apply (trans_le ? (2*exp 2 8))
1554 [apply leb_true_to_le.reflexivity
1555 |apply le_times_r.assumption
1561 theorem bertrand_n :
1562 \forall n. O < n \to bertrand n.
1563 intros;elim (decidable_le n 256)
1564 [apply le_to_bertrand;assumption
1565 |apply le_to_bertrand2;apply lt_to_le;apply not_le_to_lt;apply H1]
1569 theorem mod_exp: eqb (mod (exp 2 8) 13) O = false.