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