helm/software/matita/library/nat/bertrand.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        Matita is distributed under the terms of the          *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "nat/sqrt.ma".
  16 include "nat/chebyshev_teta.ma".
  17 include "nat/chebyshev.ma".
  18 include "list/in.ma".
  19 include "list/sort.ma".
  20 include "nat/o.ma".
  21 include "nat/sieve.ma".
  22
  23 let rec list_divides l n \def
  24   match l with
  25   [ nil ⇒ false
  26   | cons (m:nat) (tl:list nat) ⇒ orb (divides_b m n) (list_divides tl n) ].
  27
  28 definition lprim : nat \to list nat \def
  29   \lambda n.let rec aux m acc \def
  30      match m with
  31      [ O => acc
  32      | S m1 => match (list_divides acc (n-m1)) with
  33        [ true => aux m1 acc
  34        | false => aux m1 (n-m1::acc)]]
  35   in aux (pred n) [].
  36
  37 let rec checker l \def
  38     match l with
  39       [ nil => true
  40       | cons h1 t1 => match t1 with
  41          [ nil => true
  42          | cons h2 t2 => (andb (checker t1) (leb h1 (2*h2))) ]].
  43
  44 lemma checker_cons : \forall t,l.checker (t::l) = true \to checker l = true.
  45 intros 2;simplify;intro;elim l in H ⊢ %
  46   [reflexivity
  47   |change in H1 with (andb (checker (a::l1)) (leb t (a+(a+O))) = true);
  48    apply (andb_true_true ? ? H1)]
  49 qed.
  50
  51 theorem checker_sound : \forall l1,l2,l,x,y.l = l1@(x::y::l2) \to
  52                         checker l = true \to x \leq 2*y.
  53 intro;elim l1 0
  54   [simplify;intros 5;rewrite > H;simplify;intro;
  55    apply leb_true_to_le;apply (andb_true_true_r ? ? H1);
  56   |simplify;intros;rewrite > H1 in H2;lapply (checker_cons ? ? H2);
  57    apply (H l2 ? ? ? ? Hletin);reflexivity]
  58 qed.
  59
  60 definition bertrand \def \lambda n.
  61 \exists p.n < p \land p \le 2*n \land (prime p).
  62
  63 definition not_bertrand \def \lambda n.
  64 \forall p.n < p \to p \le 2*n \to \not (prime p).
  65
  66 (*
  67 lemma list_of_primes_SO: \forall l.list_of_primes 1 l \to
  68 l = [].
  69 intro.cases l;intros
  70   [reflexivity
  71   |apply False_ind.unfold in H.
  72    absurd ((prime n) \land n \le 1)
  73     [apply H.
  74      apply in_list_head
  75     |intro.elim H1.
  76      elim H2.
  77      apply (lt_to_not_le ? ? H4 H3)
  78     ]
  79   ]
  80 qed.
  81 *)
  82
  83 lemma min_prim : \forall n.\exists p. n < p \land prime p \land
  84                  \forall q.prime q \to q < p \to q \leq n.
  85 intro;elim (le_to_or_lt_eq ? ? (le_O_n n))
  86    [apply (ex_intro ? ? (min_aux (S (n!)) (S n) primeb));
  87     split
  88       [split
  89          [apply le_min_aux;
  90          |apply primeb_true_to_prime;apply f_min_aux_true;elim (ex_prime n);
  91             [apply (ex_intro ? ? a);elim H1;elim H2;split
  92                [split
  93                   [assumption
  94                   |rewrite > plus_n_O;apply le_plus
  95                      [assumption
  96                      |apply le_O_n]]
  97                |apply prime_to_primeb_true;assumption]
  98             |assumption]]
  99       |intros;apply not_lt_to_le;intro;lapply (lt_min_aux_to_false ? ? ? ? H3 H2);
 100        rewrite > (prime_to_primeb_true ? H1) in Hletin;destruct Hletin]
 101    |apply (ex_intro ? ? 2);split
 102       [split
 103          [rewrite < H;apply lt_O_S
 104          |apply primeb_true_to_prime;reflexivity]
 105       |intros;elim (lt_to_not_le ? ? H2);apply prime_to_lt_SO;assumption]]
 106 qed.
 107
 108 theorem list_of_primes_to_bertrand: \forall n,pn,l.0 < n \to prime pn \to n <pn \to
 109 list_of_primes pn l  \to
 110 (\forall p. prime p \to p \le pn \to in_list nat p l) \to
 111 (\forall p. in_list nat p l \to 2 < p \to
 112 \exists pp. in_list nat pp l \land pp < p \land p \le 2*pp) \to bertrand n.
 113 intros.
 114 elim (min_prim n).
 115 apply (ex_intro ? ? a).
 116 elim H6.clear H6.elim H7.clear H7.
 117 split
 118   [split
 119     [assumption
 120     |elim (le_to_or_lt_eq ? ? (prime_to_lt_SO ? H9))
 121       [elim (H5 a)
 122         [elim H10.clear H10.elim H11.clear H11.
 123          apply (trans_le ? ? ? H12).
 124          apply le_times_r.
 125          apply H8
 126           [unfold in H3.
 127            elim (H3 a1 H10).
 128            assumption
 129           |assumption
 130           ]
 131         |apply H4
 132           [assumption
 133           |apply not_lt_to_le.intro.
 134            apply (lt_to_not_le ? ? H2).
 135            apply H8;assumption
 136           ]
 137         |assumption
 138         ]
 139       |rewrite < H7.
 140        apply O_lt_const_to_le_times_const.
 141        assumption
 142       ]
 143     ]
 144   |assumption
 145   ]
 146 qed.
 147
 148 let rec check_list l \def
 149   match l with
 150   [ nil \Rightarrow true
 151   | cons (hd:nat) tl \Rightarrow
 152     match tl with
 153      [ nil \Rightarrow eqb hd 2
 154      | cons hd1 tl1 \Rightarrow
 155       (leb (S hd1) hd \land leb hd (2*hd1) \land check_list tl)
 156     ]
 157   ]
 158 .
 159
 160 lemma check_list1: \forall n,m,l.(check_list (n::m::l)) = true \to
 161 m < n \land n \le 2*m \land (check_list (m::l)) = true \land ((check_list l) = true).
 162 intros 3.
 163 change in ⊢ (? ? % ?→?) with (leb (S m) n \land leb n (2*m) \land check_list (m::l)).
 164 intro.
 165 lapply (andb_true_true ? ? H) as H1.
 166 lapply (andb_true_true_r ? ? H) as H2.clear H.
 167 lapply (andb_true_true ? ? H1) as H3.
 168 lapply (andb_true_true_r ? ? H1) as H4.clear H1.
 169 split
 170   [split
 171     [split
 172       [apply leb_true_to_le.assumption
 173       |apply leb_true_to_le.assumption
 174       ]
 175     |assumption
 176     ]
 177   |generalize in match H2.
 178    cases l
 179     [intro.reflexivity
 180     |change in ⊢ (? ? % ?→?) with (leb (S n1) m \land leb m (2*n1) \land check_list (n1::l1)).
 181      intro.
 182      lapply (andb_true_true_r ? ? H) as H2.
 183      assumption
 184     ]
 185   ]
 186 qed.
 187
 188 theorem check_list2: \forall l. check_list l = true \to
 189 \forall p. in_list nat p l \to 2 < p \to
 190 \exists pp. in_list nat pp l \land pp < p \land p \le 2*pp.
 191 intro.elim l 2
 192   [intros.apply False_ind.apply (not_in_list_nil ? ? H1)
 193   |cases l1;intros
 194     [lapply (in_list_singleton_to_eq ? ? ? H2) as H4.
 195      apply False_ind.
 196      apply (lt_to_not_eq ? ? H3).
 197      apply sym_eq.apply eqb_true_to_eq.
 198      rewrite > H4.apply H1
 199     |elim (check_list1 ? ? ? H1).clear H1.
 200      elim H4.clear H4.
 201      elim H1.clear H1.
 202      elim (in_list_cons_case ? ? ? ? H2)
 203       [apply (ex_intro ? ? n).
 204        split
 205         [split
 206           [apply in_list_cons.apply in_list_head
 207           |rewrite > H1.assumption
 208           ]
 209         |rewrite > H1.assumption
 210         ]
 211       |elim (H H6 p H1 H3).clear H.
 212        apply (ex_intro ? ? a1).
 213        elim H8.clear H8.
 214        elim H.clear H.
 215        split
 216         [split
 217           [apply in_list_cons.assumption
 218           |assumption
 219           ]
 220         |assumption
 221         ]
 222       ]
 223     ]
 224   ]
 225 qed.
 226
 227 (* qualcosa che non va con gli S *)
 228 lemma le_to_bertrand : \forall n.O < n \to n \leq exp 2 8 \to bertrand n.
 229 intros.
 230 apply (list_of_primes_to_bertrand ? (S(exp 2 8)) (sieve (S(exp 2 8))))
 231   [assumption
 232   |apply primeb_true_to_prime.reflexivity
 233   |apply (le_to_lt_to_lt ? ? ? H1).
 234    apply le_n
 235   |lapply (sieve_sound1 (S(exp 2 8))) as H
 236     [elim H.assumption
 237     |apply leb_true_to_le.reflexivity
 238     ]
 239   |intros.apply (sieve_sound2 ? ? H3 H2)
 240   |apply check_list2.
 241    reflexivity
 242   ]
 243 qed.
 244
 245 (*lemma pippo : \forall k,n.in_list ? (nth_prime (S k)) (sieve n) \to
 246               \exists l.sieve n = l@((nth_prime (S k))::(sieve (nth_prime k))).
 247 intros;elim H;elim H1;clear H H1;apply (ex_intro ? ? a);
 248 cut (a1 = sieve (nth_prime k))
 249   [rewrite < Hcut;assumption
 250   |lapply (sieve_sorted n);generalize in match H2*)
 251
 252 (* old proof by Wilmer
 253 lemma le_to_bertrand : \forall n.O < n \to n \leq exp 2 8 \to bertrand n.
 254 intros;
 255 elim (min_prim n);apply (ex_intro ? ? a);elim H2;elim H3;clear H2 H3;
 256 cut (a \leq 257)
 257   [|apply not_lt_to_le;intro;apply (le_to_not_lt ? ? H1);apply (H4 ? ? H2);
 258     apply primeb_true_to_prime;reflexivity]
 259 split
 260    [split
 261       [assumption
 262       |elim (prime_to_nth_prime a H6);generalize in match H2;cases a1
 263          [simplify;intro;rewrite < H3;rewrite < plus_n_O;
 264           change in \vdash (? % ?) with (1+1);apply le_plus;assumption
 265          |intro;lapply (H4 (nth_prime n1))
 266             [apply (trans_le ? (2*(nth_prime n1)))
 267                [rewrite < H3;
 268                 cut (\exists l1,l2.sieve 257 = l1@((nth_prime (S n1))::((nth_prime n1)::l2)))
 269                   [elim Hcut1;elim H7;clear Hcut1 H7;
 270                    apply (checker_sound a2 a3 (sieve 257))
 271                      [apply H8
 272                      |reflexivity]
 273                   |elim (sieve_sound2 257 (nth_prime (S n1)) ? ?)
 274                      [elim (sieve_sound2 257 (nth_prime n1) ? ?)
 275                         [elim H8;
 276                          cut (\forall p.in_list ? p (a3@(nth_prime n1::a4)) \to prime p)
 277                            [|rewrite < H9;intros;apply (in_list_sieve_to_prime 257 p ? H10);
 278                             apply leb_true_to_le;reflexivity]
 279                          apply (ex_intro ? ? a2);apply (ex_intro ? ? a4);
 280                          elim H7;clear H7 H8;
 281                          cut ((nth_prime n1)::a4 = a5)
 282                            [|generalize in match H10;
 283                              lapply (sieve_sorted 257);
 284                              generalize in match Hletin1;
 285                              rewrite > H9 in ⊢ (? %→? ? % ?→?);
 286                              generalize in match Hcut1;
 287                              generalize in match a2;
 288                              elim a3 0
 289                                [intro;elim l
 290                                   [change in H11 with (nth_prime n1::a4 = nth_prime (S n1)::a5);
 291                                    destruct H11;elim (eq_to_not_lt ? ? Hcut2);
 292                                    apply increasing_nth_prime
 293                                   |change in H12 with (nth_prime n1::a4 = t::(l1@(nth_prime (S n1)::a5)));
 294                                    destruct H12;
 295                                    change in H11 with (sorted_gt (nth_prime n1::l1@(nth_prime (S n1)::a5)));
 296                                    lapply (sorted_to_minimum ? ? ? H11 (nth_prime (S n1)))
 297                                      [unfold in Hletin2;elim (le_to_not_lt ? ? (lt_to_le ? ? Hletin2));
 298                                       apply increasing_nth_prime
 299                                      |apply (ex_intro ? ? l1);apply (ex_intro ? ? a5);reflexivity]]
 300                                |intros 5;elim l1
 301                                   [change in H12 with (t::(l@(nth_prime n1::a4)) = nth_prime (S n1)::a5);
 302                                    destruct H12;cut (l = [])
 303                                      [rewrite > Hcut2;reflexivity
 304                                      |change in H11 with (sorted_gt (nth_prime (S n1)::(l@(nth_prime n1::a4))));
 305                                       generalize in match H11;generalize in match H8;cases l;intros
 306                                         [reflexivity
 307                                         |lapply (sorted_cons_to_sorted ? ? ? H13);
 308                                          lapply (sorted_to_minimum ? ? ? H13 n2)
 309                                            [simplify in Hletin2;lapply (sorted_to_minimum ? ? ? Hletin2 (nth_prime n1))
 310                                               [unfold in Hletin3;unfold in Hletin4;
 311                                                elim (lt_nth_prime_to_not_prime ? ? Hletin4 Hletin3);
 312                                                apply H12;
 313                                                apply (ex_intro ? ? [nth_prime (S n1)]);
 314                                                apply (ex_intro ? ? (l2@(nth_prime n1::a4)));
 315                                                reflexivity
 316                                               |apply (ex_intro ? ? l2);apply (ex_intro ? ? a4);reflexivity]
 317                                            |simplify;apply in_list_head]]]
 318                                   |change in H13 with (t::(l@(nth_prime n1::a4)) = t1::(l2@(nth_prime (S n1)::a5)));
 319                                    destruct H13;apply (H7 l2 ? ? Hcut3)
 320                                      [intros;apply H8;simplify;apply in_list_cons;
 321                                       assumption
 322                                      |simplify in H12;
 323                                       apply (sorted_cons_to_sorted ? ? ? H12)]]]]
 324                          rewrite > Hcut2 in ⊢ (? ? ? (? ? ? (? ? ? %)));
 325                          apply H10
 326                         |apply (trans_le ? ? ? Hletin);apply lt_to_le;
 327                          apply (trans_le ? ? ? H5 Hcut)
 328                         |apply prime_nth_prime]
 329                      |rewrite > H3;assumption
 330                      |apply prime_nth_prime]]
 331                |apply le_times_r;assumption]
 332             |apply prime_nth_prime
 333             |rewrite < H3;apply increasing_nth_prime]]]
 334    |assumption]
 335 qed. *)
 336
 337 lemma not_not_bertrand_to_bertrand1: \forall n.
 338 \lnot (not_bertrand n) \to \forall x. n \le x \to x \le 2*n \to
 339 (\forall p.x < p \to p \le 2*n \to \not (prime p))
 340 \to \exists p.n < p \land p \le  x \land (prime p).
 341 intros 4.elim H1
 342   [apply False_ind.apply H.assumption
 343   |apply (bool_elim ? (primeb (S n1)));intro
 344     [apply (ex_intro ? ? (S n1)).
 345      split
 346       [split
 347         [apply le_S_S.assumption
 348         |apply le_n
 349         ]
 350       |apply primeb_true_to_prime.assumption
 351       ]
 352     |elim H3
 353       [elim H7.clear H7.
 354        elim H8.clear H8.
 355        apply (ex_intro ? ? a).
 356        split
 357         [split
 358           [assumption
 359           |apply le_S.assumption
 360           ]
 361         |assumption
 362         ]
 363       |apply lt_to_le.assumption
 364       |elim (le_to_or_lt_eq ? ? H7)
 365         [apply H5;assumption
 366         |rewrite < H9.
 367          apply primeb_false_to_not_prime.
 368          assumption
 369         ]
 370       ]
 371     ]
 372   ]
 373 qed.
 374
 375 theorem not_not_bertrand_to_bertrand: \forall n.
 376 \lnot (not_bertrand n) \to bertrand n.
 377 unfold bertrand.intros.
 378 apply (not_not_bertrand_to_bertrand1 ? ? (2*n))
 379   [assumption
 380   |apply le_times_n.apply le_n_Sn
 381   |apply le_n
 382   |intros.apply False_ind.
 383    apply (lt_to_not_le ? ? H1 H2)
 384   ]
 385 qed.
 386
 387 (* not used
 388 theorem divides_pi_p_to_divides: \forall p,n,b,g.prime p \to
 389 divides p (pi_p n b g) \to \exists i. (i < n \and (b i = true \and
 390 divides p (g i))).
 391 intros 2.elim n
 392   [simplify in H1.
 393    apply False_ind.
 394    apply (le_to_not_lt p 1)
 395     [apply divides_to_le
 396       [apply le_n
 397       |assumption
 398       ]
 399     |elim H.assumption
 400     ]
 401   |apply (bool_elim ? (b n1));intro
 402     [rewrite > (true_to_pi_p_Sn ? ? ? H3) in H2.
 403      elim (divides_times_to_divides ? ? ? H1 H2)
 404       [apply (ex_intro ? ? n1).
 405        split
 406         [apply le_n
 407         |split;assumption
 408         ]
 409       |elim (H ? ? H1 H4).
 410        elim H5.
 411        apply (ex_intro ? ? a).
 412        split
 413         [apply lt_to_le.apply le_S_S.assumption
 414         |assumption
 415         ]
 416       ]
 417     |rewrite > (false_to_pi_p_Sn ? ? ? H3) in H2.
 418      elim (H ? ? H1 H2).
 419      elim H4.
 420      apply (ex_intro ? ? a).
 421      split
 422       [apply lt_to_le.apply le_S_S.assumption
 423       |assumption
 424       ]
 425     ]
 426   ]
 427 qed.
 428
 429 theorem divides_B: \forall n,p.prime p \to p \divides (B n) \to
 430 p \le n \land \exists i.mod (n /(exp p (S i))) 2 \neq O.
 431 intros.
 432 unfold B in H1.
 433 elim (divides_pi_p_to_divides ? ? ? ? H H1).
 434 elim H2.clear H2.
 435 elim H4.clear H4.
 436 elim (divides_pi_p_to_divides ? ? ? ? H H5).clear H5.
 437 elim H4.clear H4.
 438 elim H6.clear H6.
 439 cut (p = a)
 440   [split
 441     [rewrite > Hcut.apply le_S_S_to_le.assumption
 442     |apply (ex_intro ? ? a1).
 443      rewrite > Hcut.
 444      intro.
 445      change in H7:(? ? %) with (exp a ((n/(exp a (S a1))) \mod 2)).
 446      rewrite > H6 in H7.
 447      simplify in H7.
 448      absurd (p \le 1)
 449       [apply divides_to_le[apply lt_O_S|assumption]
 450       |apply lt_to_not_le.elim H.assumption
 451       ]
 452     ]
 453   |apply (divides_exp_to_eq ? ? ? H ? H7).
 454    apply primeb_true_to_prime.
 455    assumption
 456   ]
 457 qed.
 458 *)
 459
 460 definition k \def \lambda n,p.
 461 sigma_p (log p n) (λi:nat.true) (λi:nat.((n/(exp p (S i))\mod 2))).
 462
 463 theorem le_k: \forall n,p. k n p \le log p n.
 464 intros.unfold k.elim (log p n)
 465   [apply le_n
 466   |rewrite > true_to_sigma_p_Sn
 467     [rewrite > plus_n_SO.
 468      rewrite > sym_plus in ⊢ (? ? %).
 469      apply le_plus
 470       [apply le_S_S_to_le.
 471        apply lt_mod_m_m.
 472        apply lt_O_S
 473       |assumption
 474       ]
 475     |reflexivity
 476     ]
 477   ]
 478 qed.
 479
 480 definition B1 \def
 481 \lambda n. pi_p (S n) primeb (\lambda p.(exp p (k n p))).
 482
 483 theorem eq_B_B1: \forall n. B n = B1 n.
 484 intros.unfold B.unfold B1.
 485 apply eq_pi_p
 486   [intros.reflexivity
 487   |intros.unfold k.
 488    apply exp_sigma_p1
 489   ]
 490 qed.
 491
 492 definition B_split1 \def \lambda n.
 493 pi_p (S n) primeb (\lambda p.(exp p (bool_to_nat (leb (k n p) 1)* (k n p)))).
 494
 495 definition B_split2 \def \lambda n.
 496 pi_p (S n) primeb (\lambda p.(exp p (bool_to_nat (leb 2 (k n p))* (k n p)))).
 497
 498 theorem eq_B1_times_B_split1_B_split2: \forall n.
 499 B1 n = B_split1 n * B_split2 n.
 500 intro.unfold B1.unfold B_split1.unfold B_split2.
 501 rewrite < times_pi_p.
 502 apply eq_pi_p
 503   [intros.reflexivity
 504   |intros.apply (bool_elim ? (leb (k n x) 1));intro
 505     [rewrite > (lt_to_leb_false 2 (k n x))
 506       [simplify.rewrite < plus_n_O.
 507        rewrite < times_n_SO.reflexivity
 508       |apply le_S_S.apply leb_true_to_le.assumption
 509       ]
 510     |rewrite > (le_to_leb_true 2 (k n x))
 511       [simplify.rewrite < plus_n_O.
 512        rewrite < plus_n_O.reflexivity
 513       |apply not_le_to_lt.apply leb_false_to_not_le.assumption
 514       ]
 515     ]
 516   ]
 517 qed.
 518
 519 lemma lt_div_to_times: \forall n,m,q. O < q \to n/q < m \to n < q*m.
 520 intros.
 521 cut (O < m) as H2
 522   [apply not_le_to_lt.
 523    intro.apply (lt_to_not_le ? ? H1).
 524    apply le_times_to_le_div;assumption
 525   |apply (ltn_to_ltO ? ? H1)
 526   ]
 527 qed.
 528
 529 lemma lt_to_div_O:\forall n,m. n < m \to n / m = O.
 530 intros.
 531 apply (div_mod_spec_to_eq n m (n/m) (n \mod m) O n)
 532   [apply div_mod_spec_div_mod.
 533    apply (ltn_to_ltO ? ? H)
 534   |apply div_mod_spec_intro
 535     [assumption
 536     |reflexivity
 537     ]
 538   ]
 539 qed.
 540
 541 (* the value of n could be smaller *)
 542 lemma k1: \forall n,p. 18 \le n \to p \le n \to 2*n/ 3 < p\to k (2*n) p = O.
 543 intros.unfold k.
 544 elim (log p (2*n))
 545   [reflexivity
 546   |rewrite > true_to_sigma_p_Sn
 547     [rewrite > H3.
 548      rewrite < plus_n_O.
 549      cases n1
 550       [rewrite < exp_n_SO.
 551        cut (2*n/p = 2) as H4
 552         [rewrite > H4.reflexivity
 553         |apply lt_to_le_times_to_lt_S_to_div
 554           [apply (ltn_to_ltO ? ? H2)
 555           |rewrite < sym_times.
 556            apply le_times_r.
 557            assumption
 558           |rewrite > sym_times in ⊢ (? ? %).
 559            apply lt_div_to_times
 560             [apply lt_O_S
 561             |assumption
 562             ]
 563           ]
 564         ]
 565       |cut (2*n/(p)\sup(S (S n2)) = O) as H4
 566         [rewrite > H4.reflexivity
 567         |apply lt_to_div_O.
 568          apply (le_to_lt_to_lt ? (exp ((2*n)/3) 2))
 569           [apply (le_times_to_le (exp 3 2))
 570             [apply leb_true_to_le.reflexivity
 571             |rewrite > sym_times in ⊢ (? ? %).
 572              rewrite > times_exp.
 573              apply (trans_le ? (exp n 2))
 574               [rewrite < assoc_times.
 575                rewrite > exp_SSO in ⊢ (? ? %).
 576                apply le_times_l.
 577                assumption
 578               |apply monotonic_exp1.
 579                apply (le_plus_to_le 3).
 580                change in ⊢ (? ? %) with ((S(2*n/3))*3).
 581                apply (trans_le ? (2*n))
 582                 [simplify in ⊢ (? ? %).
 583                  rewrite < plus_n_O.
 584                  apply le_plus_l.
 585                  apply (trans_le ? 18 ? ? H).
 586                  apply leb_true_to_le.reflexivity
 587                 |apply lt_to_le.
 588                  apply lt_div_S.
 589                  apply lt_O_S
 590                 ]
 591               ]
 592             ]
 593           |apply (lt_to_le_to_lt ? (exp p 2))
 594             [apply lt_exp1
 595               [apply lt_O_S
 596               |assumption
 597               ]
 598             |apply le_exp
 599               [apply (ltn_to_ltO ? ? H2)
 600               |apply le_S_S.apply le_S_S.apply le_O_n
 601               ]
 602             ]
 603           ]
 604         ]
 605       ]
 606     |reflexivity
 607     ]
 608   ]
 609 qed.
 610
 611 theorem le_B_split1_teta:\forall n.18 \le n \to not_bertrand n \to
 612 B_split1 (2*n) \le teta (2 * n / 3).
 613 intros.unfold B_split1.unfold teta.
 614 apply (trans_le ? (pi_p (S (2*n)) primeb (λp:nat.(p)\sup(bool_to_nat (eqb (k (2*n) p) 1)))))
 615   [apply le_pi_p.intros.
 616    apply le_exp
 617     [apply prime_to_lt_O.apply primeb_true_to_prime.assumption
 618     |apply (bool_elim ? (leb (k (2*n) i) 1));intro
 619       [elim (le_to_or_lt_eq ? ? (leb_true_to_le ? ? H4))
 620         [lapply (le_S_S_to_le ? ? H5) as H6.
 621          apply (le_n_O_elim ? H6).
 622          rewrite < times_n_O.
 623          apply le_n
 624         |rewrite > (eq_to_eqb_true ? ? H5).
 625          rewrite > H5.apply le_n
 626         ]
 627       |apply le_O_n
 628       ]
 629     ]
 630   |apply (trans_le ? (pi_p (S (2*n/3)) primeb (λp:nat.(p)\sup(bool_to_nat (eqb (k (2*n) p) 1)))))
 631     [apply (eq_ind ? ? ? (le_n ?)).
 632      apply or_false_eq_SO_to_eq_pi_p
 633       [apply le_S_S.
 634        apply le_times_to_le_div2
 635         [apply lt_O_S
 636         |rewrite > sym_times in ⊢ (? ? %).
 637          apply le_times_n.
 638          apply leb_true_to_le.reflexivity
 639         ]
 640       |intros.
 641        unfold not_bertrand in H1.
 642        elim (decidable_le (S n) i)
 643         [left.
 644          apply not_prime_to_primeb_false.
 645          apply H1
 646           [assumption
 647           |apply le_S_S_to_le.assumption
 648           ]
 649         |right.
 650          rewrite > k1
 651           [reflexivity
 652           |assumption
 653           |apply le_S_S_to_le.
 654            apply not_le_to_lt.assumption
 655           |assumption
 656           ]
 657         ]
 658       ]
 659     |apply le_pi_p.intros.
 660      elim (eqb (k (2*n) i) 1)
 661       [rewrite < exp_n_SO.apply le_n
 662       |simplify.apply prime_to_lt_O.
 663        apply primeb_true_to_prime.
 664        assumption
 665       ]
 666     ]
 667   ]
 668 qed.
 669
 670 theorem le_B_split2_exp: \forall n. exp 2 7 \le n \to
 671 B_split2 (2*n) \le exp (2*n) (pred(sqrt(2*n)/2)).
 672 intros.unfold B_split2.
 673 cut (O < n)
 674   [apply (trans_le ? (pi_p (S (sqrt (2*n))) primeb
 675         (λp:nat.(p)\sup(bool_to_nat (leb 2 (k (2*n) p))*k (2*n) p))))
 676     [apply (eq_ind ? ? ? (le_n ?)).
 677      apply or_false_eq_SO_to_eq_pi_p
 678       [apply le_S_S.
 679        apply le_sqrt_n_n
 680       |intros.
 681        apply (bool_elim ? (leb 2 (k (2*n) i)));intro
 682         [apply False_ind.
 683          apply (lt_to_not_le ? ? H1).unfold sqrt.
 684          apply f_m_to_le_max
 685           [apply le_S_S_to_le.assumption
 686           |apply le_to_leb_true.
 687            rewrite < exp_SSO.
 688            apply not_lt_to_le.intro.
 689            apply (le_to_not_lt 2 (log i (2*n)))
 690             [apply (trans_le ? (k (2*n) i))
 691               [apply leb_true_to_le.assumption
 692               |apply le_k
 693               ]
 694             |apply le_S_S.unfold log.apply f_false_to_le_max
 695               [apply (ex_intro ? ? O).split
 696                 [apply le_O_n
 697                 |apply le_to_leb_true.simplify.
 698                  apply (trans_le ? n)
 699                   [assumption.
 700                   |apply le_plus_n_r
 701                   ]
 702                 ]
 703               |intros.apply lt_to_leb_false.
 704                apply (lt_to_le_to_lt ? (exp i 2))
 705                 [assumption
 706                 |apply le_exp
 707                   [apply (ltn_to_ltO ? ? H1)
 708                   |assumption
 709                   ]
 710                 ]
 711               ]
 712             ]
 713           ]
 714         |right.reflexivity
 715         ]
 716       ]
 717     |apply (trans_le ? (pi_p (S (sqrt (2*n))) primeb (λp:nat.2*n)))
 718       [apply le_pi_p.intros.
 719        apply (trans_le ? (exp i (log i (2*n))))
 720         [apply le_exp
 721           [apply prime_to_lt_O.
 722            apply primeb_true_to_prime.
 723            assumption
 724           |apply (bool_elim ? (leb 2 (k (2*n) i)));intro
 725             [simplify in ⊢ (? (? % ?) ?).
 726              rewrite > sym_times.
 727              rewrite < times_n_SO.
 728              apply le_k
 729             |apply le_O_n
 730             ]
 731           ]
 732         |apply le_exp_log.
 733          rewrite > (times_n_O O) in ⊢ (? % ?).
 734          apply lt_times
 735           [apply lt_O_S
 736           |assumption
 737           ]
 738         ]
 739       |apply (trans_le ? (exp (2*n) (prim(sqrt (2*n)))))
 740         [unfold prim.
 741          apply (eq_ind ? ? ? (le_n ?)).
 742          apply exp_sigma_p
 743         |apply le_exp
 744           [rewrite > (times_n_O O) in ⊢ (? % ?).
 745            apply lt_times
 746             [apply lt_O_S
 747             |assumption
 748             ]
 749           |apply le_prim_n3.
 750            unfold sqrt.
 751            apply f_m_to_le_max
 752             [apply (trans_le ? (2*(exp 2 7)))
 753               [apply leb_true_to_le.reflexivity
 754               |apply le_times_r.assumption
 755               ]
 756             |apply le_to_leb_true.
 757              apply (trans_le ? (2*(exp 2 7)))
 758               [apply leb_true_to_le.reflexivity
 759               |apply le_times_r.assumption
 760               ]
 761             ]
 762           ]
 763         ]
 764       ]
 765     ]
 766   |apply (lt_to_le_to_lt ? ? ? ? H).
 767    apply leb_true_to_le.reflexivity
 768   ]
 769 qed.
 770
 771 theorem not_bertrand_to_le_B:
 772 \forall n.exp 2 7 \le n \to not_bertrand n \to
 773 B (2*n) \le (exp 2 (2*(2 * n / 3)))*(exp (2*n) (pred(sqrt(2*n)/2))).
 774 intros.
 775 rewrite > eq_B_B1.
 776 rewrite > eq_B1_times_B_split1_B_split2.
 777 apply le_times
 778   [apply (trans_le ? (teta ((2*n)/3)))
 779     [apply le_B_split1_teta
 780       [apply (trans_le ? ? ? ? H).
 781        apply leb_true_to_le.reflexivity
 782       |assumption
 783       ]
 784     |apply le_teta
 785     ]
 786   |apply le_B_split2_exp.
 787    assumption
 788   ]
 789 qed.
 790
 791 (*
 792 theorem not_bertrand_to_le1:
 793 \forall n.18 \le n \to not_bertrand n \to
 794 exp 2 (2*n) \le (exp 2 (2*(2 * n / 3)))*(exp (2*n) (S(sqrt(2*n)))).
 795 *)
 796
 797 theorem le_times_div_m_m: \forall n,m. O < m \to n/m*m \le n.
 798 intros.
 799 rewrite > (div_mod n m) in ⊢ (? ? %)
 800   [apply le_plus_n_r
 801   |assumption
 802   ]
 803 qed.
 804
 805 theorem not_bertrand_to_le1:
 806 \forall n.exp 2 7 \le n \to not_bertrand n \to
 807 (exp 2 (2*n / 3)) \le (exp (2*n) (sqrt(2*n)/2)).
 808 intros.
 809 apply (le_times_to_le (exp 2 (2*(2 * n / 3))))
 810   [apply lt_O_exp.apply lt_O_S
 811   |rewrite < exp_plus_times.
 812    apply (trans_le ? (exp 2 (2*n)))
 813     [apply le_exp
 814       [apply lt_O_S
 815       |rewrite < sym_plus.
 816        change in ⊢ (? % ?) with (3*(2*n/3)).
 817        rewrite > sym_times.
 818        apply le_times_div_m_m.
 819        apply lt_O_S
 820       ]
 821 (* weaker form
 822        rewrite < distr_times_plus.
 823        apply le_times_r.
 824        apply (trans_le ? ((2*n + n)/3))
 825         [apply le_plus_div.apply lt_O_S
 826         |rewrite < sym_plus.
 827          change in ⊢ (? (? % ?) ?) with (3*n).
 828          rewrite < sym_times.
 829          rewrite > lt_O_to_div_times
 830           [apply le_n
 831           |apply lt_O_S
 832           ]
 833         ]
 834       ] *)
 835     |apply (trans_le ? (2*n*B(2*n)))
 836       [apply le_exp_B.
 837        apply (trans_le ? ? ? ? H).
 838        apply leb_true_to_le.reflexivity
 839       |rewrite > S_pred in ⊢ (? ? (? ? (? ? %)))
 840         [rewrite > exp_S.
 841          rewrite < assoc_times.
 842          rewrite < sym_times in ⊢ (? ? (? % ?)).
 843          rewrite > assoc_times in ⊢ (? ? %).
 844          apply le_times_r.
 845          apply not_bertrand_to_le_B;assumption
 846         |apply le_times_to_le_div
 847           [apply lt_O_S
 848           |apply (trans_le ? (sqrt (exp 2 8)))
 849             [apply leb_true_to_le.reflexivity
 850             |apply monotonic_sqrt.
 851              change in ⊢ (? % ?) with (2*(exp 2 7)).
 852              apply le_times_r.
 853              assumption
 854             ]
 855           ]
 856         ]
 857       ]
 858     ]
 859   ]
 860 qed.
 861
 862 theorem not_bertrand_to_le2:
 863 \forall n.exp 2 7 \le n \to not_bertrand n \to
 864 2*n / 3 \le (sqrt(2*n)/2)*S(log 2 (2*n)).
 865 intros.
 866 rewrite < (eq_log_exp 2)
 867   [apply (trans_le ? (log 2 ((exp (2*n) (sqrt(2*n)/2)))))
 868     [apply le_log
 869       [apply le_n
 870       |apply not_bertrand_to_le1;assumption
 871       ]
 872     |apply log_exp1.
 873      apply le_n
 874     ]
 875   |apply le_n
 876   ]
 877 qed.
 878
 879 theorem tech1: \forall a,b,c,d.O < b \to O < d \to
 880 (a/b)*(c/d) \le (a*c)/(b*d).
 881 intros.
 882 apply le_times_to_le_div
 883   [rewrite > (times_n_O O).
 884    apply lt_times;assumption
 885   |rewrite > assoc_times.
 886    rewrite < assoc_times in ⊢ (? (? ? %) ?).
 887    rewrite < sym_times in ⊢ (? (? ? (? % ?)) ?).
 888    rewrite > assoc_times.
 889    rewrite < assoc_times.
 890    apply le_times;
 891    rewrite > sym_times;apply le_times_div_m_m;assumption
 892   ]
 893 qed.
 894
 895 theorem tech: \forall n. 2*(S(log 2 (2*n))) \le sqrt (2*n) \to
 896 (sqrt(2*n)/2)*S(log 2 (2*n)) \le 2*n / 4.
 897 intros.
 898 cut (4*(S(log 2 (2*n))) \le 2* sqrt(2*n))
 899   [rewrite > sym_times.
 900    apply le_times_to_le_div
 901     [apply lt_O_S
 902     |rewrite < assoc_times.
 903      apply (trans_le ? (2*sqrt(2*n)*(sqrt (2*n)/2)))
 904       [apply le_times_l.assumption
 905       |apply (trans_le ? ((2*sqrt(2*n)*(sqrt(2*n))/2)))
 906         [apply le_times_div_div_times.
 907          apply lt_O_S
 908         |rewrite > assoc_times.
 909          rewrite > sym_times.
 910          rewrite > lt_O_to_div_times.
 911          apply leq_sqrt_n.
 912          apply lt_O_S
 913         ]
 914       ]
 915     ]
 916   |change in ⊢ (? (? % ?) ?) with (2*2).
 917    rewrite > assoc_times.
 918    apply le_times_r.
 919    assumption
 920   ]
 921 qed.
 922
 923 theorem lt_div_S_div: \forall n,m. O < m \to exp m 2 \le n \to
 924 n/(S m) < n/m.
 925 intros.
 926 apply lt_times_to_lt_div.
 927 apply (lt_to_le_to_lt ? (S(n/m)*m))
 928   [apply lt_div_S.assumption
 929   |rewrite > sym_times in ⊢ (? ? %). simplify.
 930    rewrite > sym_times in ⊢ (? ? (? ? %)).
 931    apply le_plus_l.
 932    apply le_times_to_le_div
 933     [assumption
 934     |rewrite < exp_SSO.
 935      assumption
 936     ]
 937   ]
 938 qed.
 939
 940 theorem exp_plus_SSO: \forall a,b. exp (a+b) 2 = (exp a 2) + 2*a*b + (exp b 2).
 941 intros.
 942 rewrite > exp_SSO.
 943 rewrite > distr_times_plus.
 944 rewrite > times_plus_l.
 945 rewrite < exp_SSO.
 946 rewrite > assoc_plus.
 947 rewrite > assoc_plus.
 948 apply eq_f.
 949 rewrite > times_plus_l.
 950 rewrite < exp_SSO.
 951 rewrite < assoc_plus.
 952 rewrite < sym_times.
 953 rewrite > plus_n_O in ⊢ (? ? (? (? ? %) ?) ?).
 954 rewrite > assoc_times.
 955 apply eq_f2;reflexivity.
 956 qed.
 957
 958 theorem tech3: \forall n. (exp 2 8) \le n \to 2*(S(log 2 (2*n))) \le sqrt (2*n).
 959 intros.
 960 lapply (le_log 2 ? ? (le_n ?) H) as H1.
 961 rewrite > exp_n_SO in ⊢ (? (? ? (? (? ? (? % ?)))) ?).
 962 rewrite > log_exp
 963   [rewrite > sym_plus.
 964    rewrite > plus_n_Sm.
 965    unfold sqrt.
 966    apply f_m_to_le_max
 967     [apply le_times_r.
 968      apply (trans_le ? (2*log 2 n))
 969       [rewrite < times_SSO_n.
 970        apply le_plus_r.
 971        apply (trans_le ? 8)
 972         [apply leb_true_to_le.reflexivity
 973         |rewrite < (eq_log_exp 2)
 974           [assumption
 975           |apply le_n
 976           ]
 977         ]
 978       |apply (trans_le ? ? ? ? (le_exp_log 2 ? ? )).
 979        apply le_times_SSO_n_exp_SSO_n.
 980        apply (lt_to_le_to_lt ? ? ? ? H).
 981        apply leb_true_to_le.reflexivity
 982       ]
 983     |apply le_to_leb_true.
 984      rewrite > assoc_times.
 985      apply le_times_r.
 986      rewrite > sym_times.
 987      rewrite > assoc_times.
 988      rewrite < exp_SSO.
 989      rewrite > exp_plus_SSO.
 990      rewrite > distr_times_plus.
 991      rewrite > distr_times_plus.
 992      rewrite > assoc_plus.
 993      apply (trans_le ? (4*exp (log 2 n) 2))
 994       [change in ⊢ (? ? (? % ?)) with (2*2).
 995        rewrite > assoc_times in ⊢ (? ? %).
 996        rewrite < times_SSO_n in ⊢ (? ? %).
 997        apply le_plus_r.
 998        rewrite < times_SSO_n in ⊢ (? ? %).
 999        apply le_plus
1000         [rewrite > sym_times in ⊢ (? (? ? %) ?).
1001          rewrite < assoc_times.
1002          rewrite < assoc_times.
1003          change in ⊢ (? (? % ?) ?) with 8.
1004          rewrite > exp_SSO.
1005          apply le_times_l.
1006          (* strange things here *)
1007          rewrite < (eq_log_exp 2)
1008           [assumption
1009           |apply le_n
1010           ]
1011         |apply (trans_le ? (log 2 n))
1012           [change in ⊢ (? % ?) with 8.
1013            rewrite < (eq_log_exp 2)
1014             [assumption
1015             |apply le_n
1016             ]
1017           |rewrite > exp_n_SO in ⊢ (? % ?).
1018            apply le_exp
1019             [apply lt_O_log
1020               [apply (lt_to_le_to_lt ? ? ? ? H).
1021                apply leb_true_to_le.reflexivity
1022               |apply (lt_to_le_to_lt ? ? ? ? H).
1023                apply leb_true_to_le.reflexivity
1024               ]
1025             |apply le_n_Sn
1026             ]
1027           ]
1028         ]
1029       |change in ⊢ (? (? % ?) ?) with (exp 2 2).
1030        apply (trans_le ? ? ? ? (le_exp_log 2 ? ?))
1031         [apply le_times_exp_n_SSO_exp_SSO_n
1032           [apply le_n
1033           |change in ⊢ (? % ?) with 8.
1034            rewrite < (eq_log_exp 2)
1035             [assumption
1036             |apply le_n
1037             ]
1038           ]
1039         |apply (lt_to_le_to_lt ? ? ? ? H).
1040          apply leb_true_to_le.reflexivity
1041         ]
1042       ]
1043     ]
1044   |apply le_n
1045   |apply (lt_to_le_to_lt ? ? ? ? H).
1046    apply leb_true_to_le.reflexivity
1047   ]
1048 qed.
1049
1050 theorem le_to_bertrand2:
1051 \forall n. (exp 2 8) \le n \to bertrand n.
1052 intros.
1053 apply not_not_bertrand_to_bertrand.unfold.intro.
1054 absurd (2*n / 3 \le (sqrt(2*n)/2)*S(log 2 (2*n)))
1055   [apply not_bertrand_to_le2
1056     [apply (trans_le ? ? ? ? H).
1057      apply le_exp
1058       [apply lt_O_S
1059       |apply le_n_Sn
1060       ]
1061     |assumption
1062     ]
1063   |apply lt_to_not_le.
1064    apply (le_to_lt_to_lt ? ? ? ? (lt_div_S_div ? ? ? ?))
1065     [apply tech.apply tech3.assumption
1066     |apply lt_O_S
1067     |apply (trans_le ? (2*exp 2 8))
1068       [apply leb_true_to_le.reflexivity
1069       |apply le_times_r.assumption
1070       ]
1071     ]
1072   ]
1073 qed.
1074
1075 theorem bertrand_n :
1076 \forall n. O < n \to bertrand n.
1077 intros;elim (decidable_le n 256)
1078   [apply le_to_bertrand;assumption
1079   |apply le_to_bertrand2;apply lt_to_le;apply not_le_to_lt;apply H1]
1080 qed.
1081
1082 (* test
1083 theorem mod_exp: eqb (mod (exp 2 8) 13) O = false.
1084 reflexivity.
1085 *)