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
  22 let rec list_divides l n \def
  23   match l with
  24   [ nil ⇒ false
  25   | cons (m:nat) (tl:list nat) ⇒ orb (divides_b m n) (list_divides tl n) ].
  26
  27 definition lprim : nat \to list nat \def
  28   \lambda n.let rec aux m acc \def
  29      match m with
  30      [ O => acc
  31      | S m1 => match (list_divides acc (n-m1)) with
  32        [ true => aux m1 acc
  33        | false => aux m1 (n-m1::acc)]]
  34   in aux (pred n) [].
  35
  36 let rec list_n_aux n k \def
  37     match n with
  38     [ O => nil nat
  39     | S n1 => k::list_n_aux n1 (S k) ].
  40
  41 definition list_n : nat \to list nat \def
  42   \lambda n.list_n_aux (pred n) 2.
  43
  44 let rec sieve_aux l1 l2 t on t \def
  45   match t with
  46   [ O => l1
  47   | S t1 => match l2 with
  48     [ nil => l1
  49     | cons n tl => sieve_aux (n::l1) (filter nat tl (\lambda x.notb (divides_b n x))) t1]].
  50
  51 definition sieve : nat \to list nat \def
  52   \lambda m.sieve_aux [] (list_n m) m.
  53
  54 lemma divides_to_prime_divides : \forall n,m.1 < m \to m < n \to m \divides n \to
  55  \exists p.p \leq m \land prime p \land p \divides n.
  56 intros;apply (ex_intro ? ? (nth_prime (max_prime_factor m)));split
  57   [split
  58      [apply divides_to_le
  59         [apply lt_to_le;assumption
  60         |apply divides_max_prime_factor_n;assumption]
  61      |apply prime_nth_prime;]
  62   |apply (transitive_divides ? ? ? ? H2);apply divides_max_prime_factor_n;
  63    assumption]
  64 qed.
  65
  66 definition sorted_lt \def sorted ? lt.
  67 definition sorted_gt \def sorted ? gt.
  68
  69 lemma sieve_prime : \forall t,k,l2,l1.
  70   (\forall p.(in_list ? p l1 \to prime p \land p \leq k \land \forall x.in_list ? x l2 \to p < x) \land
  71              (prime p \to p \leq k \to (\forall x.in_list ? x l2 \to p < x) \to in_list ? p l1)) \to
  72   (\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
  73              (2 \leq x \to x \leq k \to (\forall p.in_list ? p l1 \to \lnot p \divides x) \to
  74               in_list ? x l2)) \to
  75   length ? l2 \leq t \to
  76   sorted_gt l1 \to
  77   sorted_lt l2 \to
  78   sorted_gt (sieve_aux l1 l2 t) \land
  79   \forall p.(in_list ? p (sieve_aux l1 l2 t) \to prime p \land p \leq k) \land
  80             (prime p \to p \leq k \to in_list ? p (sieve_aux l1 l2 t)).
  81 intro.elim t 0
  82   [intros;cut (l2 = [])
  83      [|generalize in match H2;elim l2
  84         [reflexivity
  85         |simplify in H6;elim (not_le_Sn_O ? H6)]]
  86    simplify;split
  87      [assumption
  88      |intro;elim (H p);split;intros
  89         [elim (H5 H7);assumption
  90         |apply (H6 H7 H8);rewrite > Hcut;intros;elim (not_in_list_nil ? ? H9)]]
  91   |intros 4;elim l2
  92      [simplify;split;
  93         [assumption
  94         |intro;elim (H1 p);split;intros
  95            [elim (H6 H8);assumption
  96            |apply (H7 H8 H9);intros;elim (not_in_list_nil ? ? H10)]]
  97      |simplify;elim (H k (filter ? l (\lambda x.notb (divides_b t1 x))) (t1::l1))
  98         [split;
  99            [assumption
 100            |intro;apply H8;]
 101         |split;intros
 102            [elim (in_list_cons_case ? ? ? ? H7);
 103               [rewrite > H8;split
 104                  [split
 105                     [unfold;intros;split
 106                        [elim (H3 t1);elim H9
 107                           [elim H11;assumption
 108                           |apply in_list_head]
 109                        |intros;elim (le_to_or_lt_eq ? ? (divides_to_le ? ? ? H9))
 110                           [elim (divides_to_prime_divides ? ? H10 H11 H9);elim H12;
 111                            elim H13;clear H13 H12;elim (H3 t1);elim H12
 112                              [clear H13 H12;elim (H18 ? ? H14);elim (H2 a);
 113                               apply H13
 114                                 [assumption
 115                                 |elim H17;apply (trans_le ? ? ? ? H20);
 116                                  apply (trans_le ? ? ? H15);
 117                                  apply lt_to_le;assumption
 118                                 |intros;apply (trans_le ? (S m))
 119                                    [apply le_S_S;assumption
 120                                    |apply (trans_le ? ? ? H11);
 121                                     elim (in_list_cons_case ? ? ? ? H19)
 122                                       [rewrite > H20;apply le_n
 123                                       |apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);assumption]]]
 124                              |apply in_list_head]
 125                           |elim (H3 t1);elim H11
 126                              [elim H13;apply lt_to_le;assumption
 127                              |apply in_list_head]
 128                           |assumption]]
 129                     |elim (H3 t1);elim H9
 130                        [elim H11;assumption
 131                        |apply in_list_head]]
 132                  |intros;elim (le_to_or_lt_eq t1 x)
 133                     [assumption
 134                     |rewrite > H10 in H9;lapply (in_list_filter_to_p_true ? ? ? H9);
 135                      lapply (divides_n_n x);
 136                      rewrite > (divides_to_divides_b_true ? ? ? Hletin1) in Hletin
 137                        [simplify in Hletin;destruct Hletin
 138                        |rewrite < H10;elim (H3 t1);elim H11
 139                           [elim H13;apply lt_to_le;assumption
 140                           |apply in_list_head]]
 141                     |apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);apply (in_list_filter ? ? ? H9)]]
 142                  |elim (H2 p);elim (H9 H8);split
 143                     [assumption
 144                     |intros;apply H12;apply in_list_cons;apply (in_list_filter ? ? ? H13)]]
 145            |elim (decidable_eq_nat p t1)
 146               [rewrite > H10;apply in_list_head
 147               |apply in_list_cons;elim (H2 p);apply (H12 H7 H8);intros;
 148                apply (trans_le ? t1)
 149                  [elim (decidable_lt p t1)
 150                     [assumption
 151                     |lapply (not_lt_to_le ? ? H14);
 152                      lapply (decidable_divides t1 p)
 153                        [elim Hletin1
 154                           [elim H7;lapply (H17 ? H15)
 155                              [elim H10;symmetry;assumption
 156                              |elim (H3 t1);elim H18
 157                                 [elim H20;assumption
 158                                 |apply in_list_head]]
 159                           |elim (Not_lt_n_n p);apply H9;apply in_list_filter_r
 160                              [elim (H3 p);apply (in_list_tail ? ? t1)
 161                                 [apply H17
 162                                    [apply prime_to_lt_SO;assumption
 163                                    |assumption
 164                                    |intros;elim H7;intro;lapply (H20 ? H21)
 165                                       [rewrite > Hletin2 in H18;elim (H11 H18);
 166                                        lapply (H23 t1)
 167                                          [elim (lt_to_not_le ? ? Hletin3 Hletin)
 168                                          |apply in_list_head]
 169                                       |apply prime_to_lt_SO;elim (H2 p1);elim (H22 H18);
 170                                        elim H24;assumption]]
 171                                 |unfold;intro;apply H15;rewrite > H18;apply divides_n_n]
 172                              |rewrite > (not_divides_to_divides_b_false ? ? ? H15);
 173                                 [reflexivity
 174                                 |elim (H3 t1);elim H16
 175                                    [elim H18;apply lt_to_le;assumption
 176                                    |apply in_list_head]]]]
 177                        |elim (H3 t1);elim H15
 178                           [elim H17;apply lt_to_le;assumption
 179                           |apply in_list_head]]]
 180                  |elim (in_list_cons_case ? ? ? ? H13)
 181                     [rewrite > H14;apply le_n
 182                     |apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);assumption]]]]
 183          |elim (H3 x);split;intros;
 184             [split
 185                [elim H7
 186                   [assumption
 187                   |apply in_list_cons;apply (in_list_filter ? ? ? H9)]
 188                |intros;elim (in_list_cons_case ? ? ? ? H10)
 189                   [rewrite > H11;intro;lapply (in_list_filter_to_p_true ? ? ? H9);
 190                    rewrite > (divides_to_divides_b_true ? ? ? H12) in Hletin
 191                      [simplify in Hletin;destruct Hletin
 192                      |elim (H3 t1);elim H13
 193                         [elim H15;apply lt_to_le;assumption
 194                         |apply in_list_head]]
 195                   |elim H7
 196                      [apply H13;assumption
 197                      |apply in_list_cons;apply (in_list_filter ? ? ? H9)]]]
 198             |elim (in_list_cons_case ? ? ? ? (H8 ? ? ?))
 199                [elim (H11 x)
 200                   [rewrite > H12;apply in_list_head
 201                   |apply divides_n_n]
 202                |assumption
 203                |assumption
 204                |intros;apply H11;apply in_list_cons;assumption
 205                |apply in_list_filter_r;
 206                   [assumption
 207                   |lapply (H11 t1)
 208                      [rewrite > (not_divides_to_divides_b_false ? ? ? Hletin);
 209                         [reflexivity
 210                         |elim (H3 t1);elim H13
 211                            [elim H15;apply lt_to_le;assumption
 212                            |apply in_list_head]]
 213                      |apply in_list_head]]]]
 214          |apply (trans_le ? ? ? (le_length_filter ? ? ?));apply le_S_S_to_le;
 215           apply H4
 216          |apply sort_cons
 217             [assumption
 218             |intros;unfold;elim (H2 y);elim (H8 H7);
 219              apply H11;apply in_list_head]
 220          |generalize in match (sorted_cons_to_sorted ? ? ? ? H6);elim l
 221             [simplify;assumption
 222             |simplify;elim (notb (divides_b t1 t2));simplify
 223                [lapply (sorted_cons_to_sorted ? ? ? ? H8);lapply (H7 Hletin);
 224                 apply (sort_cons ? ? ? ? Hletin1);intros;
 225                 apply (sorted_to_minimum ? ? ? ? H8);apply (in_list_filter ? ? ? H9);
 226                |apply H7;apply (sorted_cons_to_sorted ? ? ? ? H8)]]]]]
 227 qed.
 228
 229 lemma le_list_n_aux_k_k : \forall n,m,k.in_list ? n (list_n_aux m k) \to
 230                           k \leq n.
 231 intros 2;elim m
 232   [simplify in H;elim (not_in_list_nil ? ? H)
 233   |simplify in H1;elim (in_list_cons_case ? ? ? ? H1)
 234      [rewrite > H2;apply le_n
 235      |apply lt_to_le;apply H;assumption]]
 236 qed.
 237
 238 lemma in_list_SSO_list_n : \forall n.2 \leq n \to in_list ? 2 (list_n n).
 239 intros;elim H;simplify
 240   [apply in_list_head
 241   |generalize in match H2;elim H1;simplify;apply in_list_head]
 242 qed.
 243
 244 lemma le_SSO_list_n : \forall m,n.in_list nat n (list_n m) \to 2 \leq n.
 245 intros;unfold list_n in H;apply (le_list_n_aux_k_k ? ? ? H);
 246 qed.
 247
 248 lemma le_list_n_aux : \forall n,m,k.in_list ? n (list_n_aux m k) \to n \leq k+m-1.
 249 intros 2;elim m
 250   [simplify in H;elim (not_in_list_nil ? ? H)
 251   |simplify in H1;elim (in_list_cons_case ? ? ? ? H1)
 252      [rewrite > H2;rewrite < plus_n_Sm;simplify;rewrite < minus_n_O;
 253       rewrite > plus_n_O in \vdash (? % ?);apply le_plus_r;apply le_O_n
 254      |rewrite < plus_n_Sm;apply (H (S k));assumption]]
 255 qed.
 256
 257 lemma le_list_n : \forall n,m.in_list ? n (list_n m) \to n \leq m.
 258 intros;unfold list_n in H;lapply (le_list_n_aux ? ? ? H);
 259 simplify in Hletin;generalize in match H;generalize in match Hletin;elim m
 260    [simplify in H2;elim (not_in_list_nil ? ? H2)
 261    |simplify in H2;assumption]
 262 qed.
 263
 264
 265 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).
 266 intros 3;elim H 0
 267   [intros;simplify;rewrite < plus_n_Sm in H2;simplify in H2;
 268    rewrite < plus_n_O in H2;rewrite < minus_n_O in H2;
 269    rewrite > (antisymmetric_le k n H1 H2);apply in_list_head
 270   |intros 5;simplify;generalize in match H2;elim H3
 271      [apply in_list_head
 272      |apply in_list_cons;apply H6
 273         [apply le_S_S;assumption
 274         |rewrite < plus_n_Sm in H7;apply H7]]]
 275 qed.
 276
 277 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).
 278 intros;unfold list_n;apply le_list_n_aux_r
 279   [elim H;simplify
 280      [apply lt_O_S
 281      |generalize in match H4;elim H3;
 282         [apply lt_O_S
 283         |simplify in H7;apply le_S;assumption]]
 284   |assumption
 285   |simplify;generalize in match H2;elim H;simplify;assumption]
 286 qed.
 287
 288 lemma le_length_list_n : \forall n. length ? (list_n n) \leq n.
 289 intro;cut (\forall n,k.length ? (list_n_aux n k) \leq (S n))
 290   [elim n;simplify
 291      [apply le_n
 292      |apply Hcut]
 293   |intro;elim n1;simplify
 294      [apply le_O_n
 295      |apply le_S_S;apply H]]
 296 qed.
 297
 298 lemma sorted_list_n_aux : \forall n,k.sorted_lt (list_n_aux n k).
 299 intro.elim n 0
 300   [simplify;intro;apply sort_nil
 301   |intro;simplify;intros 2;apply sort_cons
 302      [apply H
 303      |intros;lapply (le_list_n_aux_k_k ? ? ? H1);assumption]]
 304 qed.
 305
 306 definition list_of_primes \def \lambda n.\lambda l.
 307 \forall p.in_list nat p l  \to prime p \land p \leq n.
 308
 309 lemma sieve_sound1 : \forall n.2 \leq n \to
 310 sorted_gt (sieve n) \land list_of_primes n (sieve n).
 311 intros;elim (sieve_prime n n (list_n n) [])
 312   [split
 313      [assumption
 314      |intro;unfold sieve in H3;elim (H2 p);elim (H3 H5);split;assumption]
 315   |split;intros
 316      [elim (not_in_list_nil ? ? H1)
 317      |lapply (lt_to_not_le ? ? (H3 2 ?))
 318         [apply in_list_SSO_list_n;assumption
 319         |elim Hletin;apply prime_to_lt_SO;assumption]]
 320   |split;intros
 321      [split
 322         [split
 323            [apply (le_SSO_list_n ? ? H1)
 324            |apply (le_list_n ? ? H1)]
 325         |intros;elim (not_in_list_nil ? ? H2)]
 326      |apply le_list_n_r;assumption]
 327   |apply le_length_list_n
 328   |apply sort_nil
 329   |elim n;simplify
 330      [apply sort_nil
 331      |elim n1;simplify
 332         [apply sort_nil
 333         |simplify;apply sort_cons
 334            [apply sorted_list_n_aux
 335            |intros;lapply (le_list_n_aux_k_k ? ? ? H3);
 336             assumption]]]]
 337 qed.
 338
 339 lemma sieve_sorted : \forall n.sorted_gt (sieve n).
 340 intros;elim (decidable_le 2 n)
 341   [elim (sieve_sound1 ? H);assumption
 342   |generalize in match (le_S_S_to_le ? ? (not_le_to_lt ? ? H));cases n
 343      [intro;simplify;apply sort_nil
 344      |intros;lapply (le_S_S_to_le ? ? H1);rewrite < (le_n_O_to_eq ? Hletin);
 345       simplify;apply sort_nil]]
 346 qed.
 347
 348 lemma in_list_sieve_to_prime : \forall n,p.2 \leq n \to in_list ? p (sieve n) \to
 349                                prime p.
 350 intros;elim (sieve_sound1 ? H);elim (H3 ? H1);assumption;
 351 qed.
 352
 353 lemma in_list_sieve_to_leq : \forall n,p.2 \leq n \to in_list ? p (sieve n) \to
 354                              p \leq n.
 355 intros;elim (sieve_sound1 ? H);elim (H3 ? H1);assumption;
 356 qed.
 357
 358 lemma sieve_sound2 : \forall n,p.p \leq n \to prime p \to in_list ? p (sieve n).
 359 intros;elim (sieve_prime n n (list_n n) [])
 360   [elim (H3 p);apply H5;assumption
 361   |split
 362      [intro;elim (not_in_list_nil ? ? H2)
 363      |intros;lapply (lt_to_not_le ? ? (H4 2 ?))
 364         [apply in_list_SSO_list_n;apply (trans_le ? ? ? ? H);
 365          apply prime_to_lt_SO;assumption
 366         |elim Hletin;apply prime_to_lt_SO;assumption]]
 367   |split;intros
 368      [split;intros
 369         [split
 370            [apply (le_SSO_list_n ? ? H2)
 371            |apply (le_list_n ? ? H2)]
 372         |elim (not_in_list_nil ? ? H3)]
 373      |apply le_list_n_r
 374         [apply (trans_le ? ? ? H2 H3)
 375         |assumption
 376         |assumption]]
 377   |apply le_length_list_n
 378   |apply sort_nil
 379   |elim n;simplify
 380      [apply sort_nil
 381      |elim n1;simplify
 382         [apply sort_nil
 383         |simplify;apply sort_cons
 384            [apply sorted_list_n_aux
 385            |intros;lapply (le_list_n_aux_k_k ? ? ? H4);
 386             assumption]]]]
 387 qed.
 388
 389 let rec checker l \def
 390     match l with
 391       [ nil => true
 392       | cons h1 t1 => match t1 with
 393          [ nil => true
 394          | cons h2 t2 => (andb (checker t1) (leb h1 (2*h2))) ]].
 395
 396 lemma checker_cons : \forall t,l.checker (t::l) = true \to checker l = true.
 397 intros 2;simplify;intro;generalize in match H;elim l
 398   [reflexivity
 399   |change in H2 with (andb (checker (t1::l1)) (leb t (t1+(t1+O))) = true);
 400    apply (andb_true_true ? ? H2)]
 401 qed.
 402
 403 theorem checker_sound : \forall l1,l2,l,x,y.l = l1@(x::y::l2) \to
 404                         checker l = true \to x \leq 2*y.
 405 intro;elim l1 0
 406   [simplify;intros 5;rewrite > H;simplify;intro;
 407    apply leb_true_to_le;apply (andb_true_true_r ? ? H1);
 408   |simplify;intros;rewrite > H1 in H2;lapply (checker_cons ? ? H2);
 409    apply (H l2 ? ? ? ? Hletin);reflexivity]
 410 qed.
 411
 412 definition bertrand \def \lambda n.
 413 \exists p.n < p \land p \le 2*n \land (prime p).
 414
 415 definition not_bertrand \def \lambda n.
 416 \forall p.n < p \to p \le 2*n \to \not (prime p).
 417
 418 (*
 419 lemma list_of_primes_SO: \forall l.list_of_primes 1 l \to
 420 l = [].
 421 intro.cases l;intros
 422   [reflexivity
 423   |apply False_ind.unfold in H.
 424    absurd ((prime n) \land n \le 1)
 425     [apply H.
 426      apply in_list_head
 427     |intro.elim H1.
 428      elim H2.
 429      apply (lt_to_not_le ? ? H4 H3)
 430     ]
 431   ]
 432 qed.
 433 *)
 434
 435 lemma min_prim : \forall n.\exists p. n < p \land prime p \land
 436                  \forall q.prime q \to q < p \to q \leq n.
 437 intro;elim (le_to_or_lt_eq ? ? (le_O_n n))
 438    [apply (ex_intro ? ? (min_aux (S (n!)) (S n) primeb));
 439     split
 440       [split
 441          [apply le_min_aux;
 442          |apply primeb_true_to_prime;apply f_min_aux_true;elim (ex_prime n);
 443             [apply (ex_intro ? ? a);elim H1;elim H2;split
 444                [split
 445                   [assumption
 446                   |rewrite > plus_n_O;apply le_plus
 447                      [assumption
 448                      |apply le_O_n]]
 449                |apply prime_to_primeb_true;assumption]
 450             |assumption]]
 451       |intros;apply not_lt_to_le;intro;lapply (lt_min_aux_to_false ? ? ? ? H3 H2);
 452        rewrite > (prime_to_primeb_true ? H1) in Hletin;destruct Hletin]
 453    |apply (ex_intro ? ? 2);split
 454       [split
 455          [rewrite < H;apply lt_O_S
 456          |apply primeb_true_to_prime;reflexivity]
 457       |intros;elim (lt_to_not_le ? ? H2);apply prime_to_lt_SO;assumption]]
 458 qed.
 459
 460 theorem list_of_primes_to_bertrand: \forall n,pn,l.0 < n \to prime pn \to n <pn \to
 461 list_of_primes pn l  \to
 462 (\forall p. prime p \to p \le pn \to in_list nat p l) \to
 463 (\forall p. in_list nat p l \to 2 < p \to
 464 \exists pp. in_list nat pp l \land pp < p \land p \le 2*pp) \to bertrand n.
 465 intros.
 466 elim (min_prim n).
 467 apply (ex_intro ? ? a).
 468 elim H6.clear H6.elim H7.clear H7.
 469 split
 470   [split
 471     [assumption
 472     |elim (le_to_or_lt_eq ? ? (prime_to_lt_SO ? H9))
 473       [elim (H5 a)
 474         [elim H10.clear H10.elim H11.clear H11.
 475          apply (trans_le ? ? ? H12).
 476          apply le_times_r.
 477          apply H8
 478           [unfold in H3.
 479            elim (H3 a1 H10).
 480            assumption
 481           |assumption
 482           ]
 483         |apply H4
 484           [assumption
 485           |apply not_lt_to_le.intro.
 486            apply (lt_to_not_le ? ? H2).
 487            apply H8;assumption
 488           ]
 489         |assumption
 490         ]
 491       |rewrite < H7.
 492        apply O_lt_const_to_le_times_const.
 493        assumption
 494       ]
 495     ]
 496   |assumption
 497   ]
 498 qed.
 499
 500 let rec check_list l \def
 501   match l with
 502   [ nil \Rightarrow true
 503   | cons (hd:nat) tl \Rightarrow
 504     match tl with
 505      [ nil \Rightarrow eqb hd 2
 506      | cons hd1 tl1 \Rightarrow
 507       (leb (S hd1) hd \land leb hd (2*hd1) \land check_list tl)
 508     ]
 509   ]
 510 .
 511
 512 lemma check_list1: \forall n,m,l.(check_list (n::m::l)) = true \to
 513 m < n \land n \le 2*m \land (check_list (m::l)) = true \land ((check_list l) = true).
 514 intros 3.
 515 change in ⊢ (? ? % ?→?) with (leb (S m) n \land leb n (2*m) \land check_list (m::l)).
 516 intro.
 517 lapply (andb_true_true ? ? H) as H1.
 518 lapply (andb_true_true_r ? ? H) as H2.clear H.
 519 lapply (andb_true_true ? ? H1) as H3.
 520 lapply (andb_true_true_r ? ? H1) as H4.clear H1.
 521 split
 522   [split
 523     [split
 524       [apply leb_true_to_le.assumption
 525       |apply leb_true_to_le.assumption
 526       ]
 527     |assumption
 528     ]
 529   |generalize in match H2.
 530    cases l
 531     [intro.reflexivity
 532     |change in ⊢ (? ? % ?→?) with (leb (S n1) m \land leb m (2*n1) \land check_list (n1::l1)).
 533      intro.
 534      lapply (andb_true_true_r ? ? H) as H2.
 535      assumption
 536     ]
 537   ]
 538 qed.
 539
 540 theorem check_list2: \forall l. check_list l = true \to
 541 \forall p. in_list nat p l \to 2 < p \to
 542 \exists pp. in_list nat pp l \land pp < p \land p \le 2*pp.
 543 intro.elim l 2
 544   [intros.apply False_ind.apply (not_in_list_nil ? ? H1)
 545   |cases l1;intros
 546     [lapply (in_list_singleton_to_eq ? ? ? H2) as H4.
 547      apply False_ind.
 548      apply (lt_to_not_eq ? ? H3).
 549      apply sym_eq.apply eqb_true_to_eq.
 550      rewrite > H4.apply H1
 551     |elim (check_list1 ? ? ? H1).clear H1.
 552      elim H4.clear H4.
 553      elim H1.clear H1.
 554      elim (in_list_cons_case ? ? ? ? H2)
 555       [apply (ex_intro ? ? n).
 556        split
 557         [split
 558           [apply in_list_cons.apply in_list_head
 559           |rewrite > H1.assumption
 560           ]
 561         |rewrite > H1.assumption
 562         ]
 563       |elim (H H6 p H1 H3).clear H.
 564        apply (ex_intro ? ? a).
 565        elim H8.clear H8.
 566        elim H.clear H.
 567        split
 568         [split
 569           [apply in_list_cons.assumption
 570           |assumption
 571           ]
 572         |assumption
 573         ]
 574       ]
 575     ]
 576   ]
 577 qed.
 578
 579 (* qualcosa che non va con gli S *)
 580 lemma le_to_bertrand : \forall n.O < n \to n \leq exp 2 8 \to bertrand n.
 581 intros.
 582 apply (list_of_primes_to_bertrand ? (S(exp 2 8)) (sieve (S(exp 2 8))))
 583   [assumption
 584   |apply primeb_true_to_prime.reflexivity
 585   |apply (le_to_lt_to_lt ? ? ? H1).
 586    apply le_n
 587   |lapply (sieve_sound1 (S(exp 2 8))) as H
 588     [elim H.assumption
 589     |apply leb_true_to_le.reflexivity
 590     ]
 591   |intros.apply (sieve_sound2 ? ? H3 H2)
 592   |apply check_list2.
 593    reflexivity
 594   ]
 595 qed.
 596
 597 (*lemma pippo : \forall k,n.in_list ? (nth_prime (S k)) (sieve n) \to
 598               \exists l.sieve n = l@((nth_prime (S k))::(sieve (nth_prime k))).
 599 intros;elim H;elim H1;clear H H1;apply (ex_intro ? ? a);
 600 cut (a1 = sieve (nth_prime k))
 601   [rewrite < Hcut;assumption
 602   |lapply (sieve_sorted n);generalize in match H2*)
 603
 604 (* old proof by Wilmer
 605 lemma le_to_bertrand : \forall n.O < n \to n \leq exp 2 8 \to bertrand n.
 606 intros;
 607 elim (min_prim n);apply (ex_intro ? ? a);elim H2;elim H3;clear H2 H3;
 608 cut (a \leq 257)
 609   [|apply not_lt_to_le;intro;apply (le_to_not_lt ? ? H1);apply (H4 ? ? H2);
 610     apply primeb_true_to_prime;reflexivity]
 611 split
 612    [split
 613       [assumption
 614       |elim (prime_to_nth_prime a H6);generalize in match H2;cases a1
 615          [simplify;intro;rewrite < H3;rewrite < plus_n_O;
 616           change in \vdash (? % ?) with (1+1);apply le_plus;assumption
 617          |intro;lapply (H4 (nth_prime n1))
 618             [apply (trans_le ? (2*(nth_prime n1)))
 619                [rewrite < H3;
 620                 cut (\exists l1,l2.sieve 257 = l1@((nth_prime (S n1))::((nth_prime n1)::l2)))
 621                   [elim Hcut1;elim H7;clear Hcut1 H7;
 622                    apply (checker_sound a2 a3 (sieve 257))
 623                      [apply H8
 624                      |reflexivity]
 625                   |elim (sieve_sound2 257 (nth_prime (S n1)) ? ?)
 626                      [elim (sieve_sound2 257 (nth_prime n1) ? ?)
 627                         [elim H8;
 628                          cut (\forall p.in_list ? p (a3@(nth_prime n1::a4)) \to prime p)
 629                            [|rewrite < H9;intros;apply (in_list_sieve_to_prime 257 p ? H10);
 630                             apply leb_true_to_le;reflexivity]
 631                          apply (ex_intro ? ? a2);apply (ex_intro ? ? a4);
 632                          elim H7;clear H7 H8;
 633                          cut ((nth_prime n1)::a4 = a5)
 634                            [|generalize in match H10;
 635                              lapply (sieve_sorted 257);
 636                              generalize in match Hletin1;
 637                              rewrite > H9 in ⊢ (? %→? ? % ?→?);
 638                              generalize in match Hcut1;
 639                              generalize in match a2;
 640                              elim a3 0
 641                                [intro;elim l
 642                                   [change in H11 with (nth_prime n1::a4 = nth_prime (S n1)::a5);
 643                                    destruct H11;elim (eq_to_not_lt ? ? Hcut2);
 644                                    apply increasing_nth_prime
 645                                   |change in H12 with (nth_prime n1::a4 = t::(l1@(nth_prime (S n1)::a5)));
 646                                    destruct H12;
 647                                    change in H11 with (sorted_gt (nth_prime n1::l1@(nth_prime (S n1)::a5)));
 648                                    lapply (sorted_to_minimum ? ? ? H11 (nth_prime (S n1)))
 649                                      [unfold in Hletin2;elim (le_to_not_lt ? ? (lt_to_le ? ? Hletin2));
 650                                       apply increasing_nth_prime
 651                                      |apply (ex_intro ? ? l1);apply (ex_intro ? ? a5);reflexivity]]
 652                                |intros 5;elim l1
 653                                   [change in H12 with (t::(l@(nth_prime n1::a4)) = nth_prime (S n1)::a5);
 654                                    destruct H12;cut (l = [])
 655                                      [rewrite > Hcut2;reflexivity
 656                                      |change in H11 with (sorted_gt (nth_prime (S n1)::(l@(nth_prime n1::a4))));
 657                                       generalize in match H11;generalize in match H8;cases l;intros
 658                                         [reflexivity
 659                                         |lapply (sorted_cons_to_sorted ? ? ? H13);
 660                                          lapply (sorted_to_minimum ? ? ? H13 n2)
 661                                            [simplify in Hletin2;lapply (sorted_to_minimum ? ? ? Hletin2 (nth_prime n1))
 662                                               [unfold in Hletin3;unfold in Hletin4;
 663                                                elim (lt_nth_prime_to_not_prime ? ? Hletin4 Hletin3);
 664                                                apply H12;
 665                                                apply (ex_intro ? ? [nth_prime (S n1)]);
 666                                                apply (ex_intro ? ? (l2@(nth_prime n1::a4)));
 667                                                reflexivity
 668                                               |apply (ex_intro ? ? l2);apply (ex_intro ? ? a4);reflexivity]
 669                                            |simplify;apply in_list_head]]]
 670                                   |change in H13 with (t::(l@(nth_prime n1::a4)) = t1::(l2@(nth_prime (S n1)::a5)));
 671                                    destruct H13;apply (H7 l2 ? ? Hcut3)
 672                                      [intros;apply H8;simplify;apply in_list_cons;
 673                                       assumption
 674                                      |simplify in H12;
 675                                       apply (sorted_cons_to_sorted ? ? ? H12)]]]]
 676                          rewrite > Hcut2 in ⊢ (? ? ? (? ? ? (? ? ? %)));
 677                          apply H10
 678                         |apply (trans_le ? ? ? Hletin);apply lt_to_le;
 679                          apply (trans_le ? ? ? H5 Hcut)
 680                         |apply prime_nth_prime]
 681                      |rewrite > H3;assumption
 682                      |apply prime_nth_prime]]
 683                |apply le_times_r;assumption]
 684             |apply prime_nth_prime
 685             |rewrite < H3;apply increasing_nth_prime]]]
 686    |assumption]
 687 qed. *)
 688
 689 lemma not_not_bertrand_to_bertrand1: \forall n.
 690 \lnot (not_bertrand n) \to \forall x. n \le x \to x \le 2*n \to
 691 (\forall p.x < p \to p \le 2*n \to \not (prime p))
 692 \to \exists p.n < p \land p \le  x \land (prime p).
 693 intros 4.elim H1
 694   [apply False_ind.apply H.assumption
 695   |apply (bool_elim ? (primeb (S n1)));intro
 696     [apply (ex_intro ? ? (S n1)).
 697      split
 698       [split
 699         [apply le_S_S.assumption
 700         |apply le_n
 701         ]
 702       |apply primeb_true_to_prime.assumption
 703       ]
 704     |elim H3
 705       [elim H7.clear H7.
 706        elim H8.clear H8.
 707        apply (ex_intro ? ? a).
 708        split
 709         [split
 710           [assumption
 711           |apply le_S.assumption
 712           ]
 713         |assumption
 714         ]
 715       |apply lt_to_le.assumption
 716       |elim (le_to_or_lt_eq ? ? H7)
 717         [apply H5;assumption
 718         |rewrite < H9.
 719          apply primeb_false_to_not_prime.
 720          assumption
 721         ]
 722       ]
 723     ]
 724   ]
 725 qed.
 726
 727 theorem not_not_bertrand_to_bertrand: \forall n.
 728 \lnot (not_bertrand n) \to bertrand n.
 729 unfold bertrand.intros.
 730 apply (not_not_bertrand_to_bertrand1 ? ? (2*n))
 731   [assumption
 732   |apply le_times_n.apply le_n_Sn
 733   |apply le_n
 734   |intros.apply False_ind.
 735    apply (lt_to_not_le ? ? H1 H2)
 736   ]
 737 qed.
 738
 739 (* not used
 740 theorem divides_pi_p_to_divides: \forall p,n,b,g.prime p \to
 741 divides p (pi_p n b g) \to \exists i. (i < n \and (b i = true \and
 742 divides p (g i))).
 743 intros 2.elim n
 744   [simplify in H1.
 745    apply False_ind.
 746    apply (le_to_not_lt p 1)
 747     [apply divides_to_le
 748       [apply le_n
 749       |assumption
 750       ]
 751     |elim H.assumption
 752     ]
 753   |apply (bool_elim ? (b n1));intro
 754     [rewrite > (true_to_pi_p_Sn ? ? ? H3) in H2.
 755      elim (divides_times_to_divides ? ? ? H1 H2)
 756       [apply (ex_intro ? ? n1).
 757        split
 758         [apply le_n
 759         |split;assumption
 760         ]
 761       |elim (H ? ? H1 H4).
 762        elim H5.
 763        apply (ex_intro ? ? a).
 764        split
 765         [apply lt_to_le.apply le_S_S.assumption
 766         |assumption
 767         ]
 768       ]
 769     |rewrite > (false_to_pi_p_Sn ? ? ? H3) in H2.
 770      elim (H ? ? H1 H2).
 771      elim H4.
 772      apply (ex_intro ? ? a).
 773      split
 774       [apply lt_to_le.apply le_S_S.assumption
 775       |assumption
 776       ]
 777     ]
 778   ]
 779 qed.
 780
 781 theorem divides_B: \forall n,p.prime p \to p \divides (B n) \to
 782 p \le n \land \exists i.mod (n /(exp p (S i))) 2 \neq O.
 783 intros.
 784 unfold B in H1.
 785 elim (divides_pi_p_to_divides ? ? ? ? H H1).
 786 elim H2.clear H2.
 787 elim H4.clear H4.
 788 elim (divides_pi_p_to_divides ? ? ? ? H H5).clear H5.
 789 elim H4.clear H4.
 790 elim H6.clear H6.
 791 cut (p = a)
 792   [split
 793     [rewrite > Hcut.apply le_S_S_to_le.assumption
 794     |apply (ex_intro ? ? a1).
 795      rewrite > Hcut.
 796      intro.
 797      change in H7:(? ? %) with (exp a ((n/(exp a (S a1))) \mod 2)).
 798      rewrite > H6 in H7.
 799      simplify in H7.
 800      absurd (p \le 1)
 801       [apply divides_to_le[apply lt_O_S|assumption]
 802       |apply lt_to_not_le.elim H.assumption
 803       ]
 804     ]
 805   |apply (divides_exp_to_eq ? ? ? H ? H7).
 806    apply primeb_true_to_prime.
 807    assumption
 808   ]
 809 qed.
 810 *)
 811
 812 definition k \def \lambda n,p.
 813 sigma_p (log p n) (λi:nat.true) (λi:nat.((n/(exp p (S i))\mod 2))).
 814
 815 theorem le_k: \forall n,p. k n p \le log p n.
 816 intros.unfold k.elim (log p n)
 817   [apply le_n
 818   |rewrite > true_to_sigma_p_Sn
 819     [rewrite > plus_n_SO.
 820      rewrite > sym_plus in ⊢ (? ? %).
 821      apply le_plus
 822       [apply le_S_S_to_le.
 823        apply lt_mod_m_m.
 824        apply lt_O_S
 825       |assumption
 826       ]
 827     |reflexivity
 828     ]
 829   ]
 830 qed.
 831
 832 definition B1 \def
 833 \lambda n. pi_p (S n) primeb (\lambda p.(exp p (k n p))).
 834
 835 theorem eq_B_B1: \forall n. B n = B1 n.
 836 intros.unfold B.unfold B1.
 837 apply eq_pi_p
 838   [intros.reflexivity
 839   |intros.unfold k.
 840    apply exp_sigma_p1
 841   ]
 842 qed.
 843
 844 definition B_split1 \def \lambda n.
 845 pi_p (S n) primeb (\lambda p.(exp p (bool_to_nat (leb (k n p) 1)* (k n p)))).
 846
 847 definition B_split2 \def \lambda n.
 848 pi_p (S n) primeb (\lambda p.(exp p (bool_to_nat (leb 2 (k n p))* (k n p)))).
 849
 850 theorem eq_B1_times_B_split1_B_split2: \forall n.
 851 B1 n = B_split1 n * B_split2 n.
 852 intro.unfold B1.unfold B_split1.unfold B_split2.
 853 rewrite < times_pi_p.
 854 apply eq_pi_p
 855   [intros.reflexivity
 856   |intros.apply (bool_elim ? (leb (k n x) 1));intro
 857     [rewrite > (lt_to_leb_false 2 (k n x))
 858       [simplify.rewrite < plus_n_O.
 859        rewrite < times_n_SO.reflexivity
 860       |apply le_S_S.apply leb_true_to_le.assumption
 861       ]
 862     |rewrite > (le_to_leb_true 2 (k n x))
 863       [simplify.rewrite < plus_n_O.
 864        rewrite < plus_n_O.reflexivity
 865       |apply not_le_to_lt.apply leb_false_to_not_le.assumption
 866       ]
 867     ]
 868   ]
 869 qed.
 870
 871 lemma lt_div_to_times: \forall n,m,q. O < q \to n/q < m \to n < q*m.
 872 intros.
 873 cut (O < m) as H2
 874   [apply not_le_to_lt.
 875    intro.apply (lt_to_not_le ? ? H1).
 876    apply le_times_to_le_div;assumption
 877   |apply (ltn_to_ltO ? ? H1)
 878   ]
 879 qed.
 880
 881 lemma lt_to_div_O:\forall n,m. n < m \to n / m = O.
 882 intros.
 883 apply (div_mod_spec_to_eq n m (n/m) (n \mod m) O n)
 884   [apply div_mod_spec_div_mod.
 885    apply (ltn_to_ltO ? ? H)
 886   |apply div_mod_spec_intro
 887     [assumption
 888     |reflexivity
 889     ]
 890   ]
 891 qed.
 892
 893 (* the value of n could be smaller *)
 894 lemma k1: \forall n,p. 18 \le n \to p \le n \to 2*n/ 3 < p\to k (2*n) p = O.
 895 intros.unfold k.
 896 elim (log p (2*n))
 897   [reflexivity
 898   |rewrite > true_to_sigma_p_Sn
 899     [rewrite > H3.
 900      rewrite < plus_n_O.
 901      cases n1
 902       [rewrite < exp_n_SO.
 903        cut (2*n/p = 2) as H4
 904         [rewrite > H4.reflexivity
 905         |apply lt_to_le_times_to_lt_S_to_div
 906           [apply (ltn_to_ltO ? ? H2)
 907           |rewrite < sym_times.
 908            apply le_times_r.
 909            assumption
 910           |rewrite > sym_times in ⊢ (? ? %).
 911            apply lt_div_to_times
 912             [apply lt_O_S
 913             |assumption
 914             ]
 915           ]
 916         ]
 917       |cut (2*n/(p)\sup(S (S n2)) = O) as H4
 918         [rewrite > H4.reflexivity
 919         |apply lt_to_div_O.
 920          apply (le_to_lt_to_lt ? (exp ((2*n)/3) 2))
 921           [apply (le_times_to_le (exp 3 2))
 922             [apply leb_true_to_le.reflexivity
 923             |rewrite > sym_times in ⊢ (? ? %).
 924              rewrite > times_exp.
 925              apply (trans_le ? (exp n 2))
 926               [rewrite < assoc_times.
 927                rewrite > exp_SSO in ⊢ (? ? %).
 928                apply le_times_l.
 929                assumption
 930               |apply monotonic_exp1.
 931                apply (le_plus_to_le 3).
 932                change in ⊢ (? ? %) with ((S(2*n/3))*3).
 933                apply (trans_le ? (2*n))
 934                 [simplify in ⊢ (? ? %).
 935                  rewrite < plus_n_O.
 936                  apply le_plus_l.
 937                  apply (trans_le ? 18 ? ? H).
 938                  apply leb_true_to_le.reflexivity
 939                 |apply lt_to_le.
 940                  apply lt_div_S.
 941                  apply lt_O_S
 942                 ]
 943               ]
 944             ]
 945           |apply (lt_to_le_to_lt ? (exp p 2))
 946             [apply lt_exp1
 947               [apply lt_O_S
 948               |assumption
 949               ]
 950             |apply le_exp
 951               [apply (ltn_to_ltO ? ? H2)
 952               |apply le_S_S.apply le_S_S.apply le_O_n
 953               ]
 954             ]
 955           ]
 956         ]
 957       ]
 958     |reflexivity
 959     ]
 960   ]
 961 qed.
 962
 963 theorem le_B_split1_teta:\forall n.18 \le n \to not_bertrand n \to
 964 B_split1 (2*n) \le teta (2 * n / 3).
 965 intros.unfold B_split1.unfold teta.
 966 apply (trans_le ? (pi_p (S (2*n)) primeb (λp:nat.(p)\sup(bool_to_nat (eqb (k (2*n) p) 1)))))
 967   [apply le_pi_p.intros.
 968    apply le_exp
 969     [apply prime_to_lt_O.apply primeb_true_to_prime.assumption
 970     |apply (bool_elim ? (leb (k (2*n) i) 1));intro
 971       [elim (le_to_or_lt_eq ? ? (leb_true_to_le ? ? H4))
 972         [lapply (le_S_S_to_le ? ? H5) as H6.
 973          apply (le_n_O_elim ? H6).
 974          rewrite < times_n_O.
 975          apply le_n
 976         |rewrite > (eq_to_eqb_true ? ? H5).
 977          rewrite > H5.apply le_n
 978         ]
 979       |apply le_O_n
 980       ]
 981     ]
 982   |apply (trans_le ? (pi_p (S (2*n/3)) primeb (λp:nat.(p)\sup(bool_to_nat (eqb (k (2*n) p) 1)))))
 983     [apply (eq_ind ? ? ? (le_n ?)).
 984      apply or_false_eq_SO_to_eq_pi_p
 985       [apply le_S_S.
 986        apply le_times_to_le_div2
 987         [apply lt_O_S
 988         |rewrite > sym_times in ⊢ (? ? %).
 989          apply le_times_n.
 990          apply leb_true_to_le.reflexivity
 991         ]
 992       |intros.
 993        unfold not_bertrand in H1.
 994        elim (decidable_le (S n) i)
 995         [left.
 996          apply not_prime_to_primeb_false.
 997          apply H1
 998           [assumption
 999           |apply le_S_S_to_le.assumption
1000           ]
1001         |right.
1002          rewrite > k1
1003           [reflexivity
1004           |assumption
1005           |apply le_S_S_to_le.
1006            apply not_le_to_lt.assumption
1007           |assumption
1008           ]
1009         ]
1010       ]
1011     |apply le_pi_p.intros.
1012      elim (eqb (k (2*n) i) 1)
1013       [rewrite < exp_n_SO.apply le_n
1014       |simplify.apply prime_to_lt_O.
1015        apply primeb_true_to_prime.
1016        assumption
1017       ]
1018     ]
1019   ]
1020 qed.
1021
1022 theorem le_B_split2_exp: \forall n. exp 2 7 \le n \to
1023 B_split2 (2*n) \le exp (2*n) (pred(sqrt(2*n)/2)).
1024 intros.unfold B_split2.
1025 cut (O < n)
1026   [apply (trans_le ? (pi_p (S (sqrt (2*n))) primeb
1027         (λp:nat.(p)\sup(bool_to_nat (leb 2 (k (2*n) p))*k (2*n) p))))
1028     [apply (eq_ind ? ? ? (le_n ?)).
1029      apply or_false_eq_SO_to_eq_pi_p
1030       [apply le_S_S.
1031        apply le_sqrt_n_n
1032       |intros.
1033        apply (bool_elim ? (leb 2 (k (2*n) i)));intro
1034         [apply False_ind.
1035          apply (lt_to_not_le ? ? H1).unfold sqrt.
1036          apply f_m_to_le_max
1037           [apply le_S_S_to_le.assumption
1038           |apply le_to_leb_true.
1039            rewrite < exp_SSO.
1040            apply not_lt_to_le.intro.
1041            apply (le_to_not_lt 2 (log i (2*n)))
1042             [apply (trans_le ? (k (2*n) i))
1043               [apply leb_true_to_le.assumption
1044               |apply le_k
1045               ]
1046             |apply le_S_S.unfold log.apply f_false_to_le_max
1047               [apply (ex_intro ? ? O).split
1048                 [apply le_O_n
1049                 |apply le_to_leb_true.simplify.
1050                  apply (trans_le ? n)
1051                   [assumption.
1052                   |apply le_plus_n_r
1053                   ]
1054                 ]
1055               |intros.apply lt_to_leb_false.
1056                apply (lt_to_le_to_lt ? (exp i 2))
1057                 [assumption
1058                 |apply le_exp
1059                   [apply (ltn_to_ltO ? ? H1)
1060                   |assumption
1061                   ]
1062                 ]
1063               ]
1064             ]
1065           ]
1066         |right.reflexivity
1067         ]
1068       ]
1069     |apply (trans_le ? (pi_p (S (sqrt (2*n))) primeb (λp:nat.2*n)))
1070       [apply le_pi_p.intros.
1071        apply (trans_le ? (exp i (log i (2*n))))
1072         [apply le_exp
1073           [apply prime_to_lt_O.
1074            apply primeb_true_to_prime.
1075            assumption
1076           |apply (bool_elim ? (leb 2 (k (2*n) i)));intro
1077             [simplify in ⊢ (? (? % ?) ?).
1078              rewrite > sym_times.
1079              rewrite < times_n_SO.
1080              apply le_k
1081             |apply le_O_n
1082             ]
1083           ]
1084         |apply le_exp_log.
1085          rewrite > (times_n_O O) in ⊢ (? % ?).
1086          apply lt_times
1087           [apply lt_O_S
1088           |assumption
1089           ]
1090         ]
1091       |apply (trans_le ? (exp (2*n) (prim(sqrt (2*n)))))
1092         [unfold prim.
1093          apply (eq_ind ? ? ? (le_n ?)).
1094          apply exp_sigma_p
1095         |apply le_exp
1096           [rewrite > (times_n_O O) in ⊢ (? % ?).
1097            apply lt_times
1098             [apply lt_O_S
1099             |assumption
1100             ]
1101           |apply le_prim_n3.
1102            unfold sqrt.
1103            apply f_m_to_le_max
1104             [apply (trans_le ? (2*(exp 2 7)))
1105               [apply leb_true_to_le.reflexivity
1106               |apply le_times_r.assumption
1107               ]
1108             |apply le_to_leb_true.
1109              apply (trans_le ? (2*(exp 2 7)))
1110               [apply leb_true_to_le.reflexivity
1111               |apply le_times_r.assumption
1112               ]
1113             ]
1114           ]
1115         ]
1116       ]
1117     ]
1118   |apply (lt_to_le_to_lt ? ? ? ? H).
1119    apply leb_true_to_le.reflexivity
1120   ]
1121 qed.
1122
1123 theorem not_bertrand_to_le_B:
1124 \forall n.exp 2 7 \le n \to not_bertrand n \to
1125 B (2*n) \le (exp 2 (2*(2 * n / 3)))*(exp (2*n) (pred(sqrt(2*n)/2))).
1126 intros.
1127 rewrite > eq_B_B1.
1128 rewrite > eq_B1_times_B_split1_B_split2.
1129 apply le_times
1130   [apply (trans_le ? (teta ((2*n)/3)))
1131     [apply le_B_split1_teta
1132       [apply (trans_le ? ? ? ? H).
1133        apply leb_true_to_le.reflexivity
1134       |assumption
1135       ]
1136     |apply le_teta
1137     ]
1138   |apply le_B_split2_exp.
1139    assumption
1140   ]
1141 qed.
1142
1143 (*
1144 theorem not_bertrand_to_le1:
1145 \forall n.18 \le n \to not_bertrand n \to
1146 exp 2 (2*n) \le (exp 2 (2*(2 * n / 3)))*(exp (2*n) (S(sqrt(2*n)))).
1147 *)
1148
1149 theorem le_times_div_m_m: \forall n,m. O < m \to n/m*m \le n.
1150 intros.
1151 rewrite > (div_mod n m) in ⊢ (? ? %)
1152   [apply le_plus_n_r
1153   |assumption
1154   ]
1155 qed.
1156
1157 theorem not_bertrand_to_le1:
1158 \forall n.exp 2 7 \le n \to not_bertrand n \to
1159 (exp 2 (2*n / 3)) \le (exp (2*n) (sqrt(2*n)/2)).
1160 intros.
1161 apply (le_times_to_le (exp 2 (2*(2 * n / 3))))
1162   [apply lt_O_exp.apply lt_O_S
1163   |rewrite < exp_plus_times.
1164    apply (trans_le ? (exp 2 (2*n)))
1165     [apply le_exp
1166       [apply lt_O_S
1167       |rewrite < sym_plus.
1168        change in ⊢ (? % ?) with (3*(2*n/3)).
1169        rewrite > sym_times.
1170        apply le_times_div_m_m.
1171        apply lt_O_S
1172       ]
1173 (* weaker form
1174        rewrite < distr_times_plus.
1175        apply le_times_r.
1176        apply (trans_le ? ((2*n + n)/3))
1177         [apply le_plus_div.apply lt_O_S
1178         |rewrite < sym_plus.
1179          change in ⊢ (? (? % ?) ?) with (3*n).
1180          rewrite < sym_times.
1181          rewrite > lt_O_to_div_times
1182           [apply le_n
1183           |apply lt_O_S
1184           ]
1185         ]
1186       ] *)
1187     |apply (trans_le ? (2*n*B(2*n)))
1188       [apply le_exp_B.
1189        apply (trans_le ? ? ? ? H).
1190        apply leb_true_to_le.reflexivity
1191       |rewrite > S_pred in ⊢ (? ? (? ? (? ? %)))
1192         [rewrite > exp_S.
1193          rewrite < assoc_times.
1194          rewrite < sym_times in ⊢ (? ? (? % ?)).
1195          rewrite > assoc_times in ⊢ (? ? %).
1196          apply le_times_r.
1197          apply not_bertrand_to_le_B;assumption
1198         |apply le_times_to_le_div
1199           [apply lt_O_S
1200           |apply (trans_le ? (sqrt (exp 2 8)))
1201             [apply leb_true_to_le.reflexivity
1202             |apply monotonic_sqrt.
1203              change in ⊢ (? % ?) with (2*(exp 2 7)).
1204              apply le_times_r.
1205              assumption
1206             ]
1207           ]
1208         ]
1209       ]
1210     ]
1211   ]
1212 qed.
1213
1214 theorem not_bertrand_to_le2:
1215 \forall n.exp 2 7 \le n \to not_bertrand n \to
1216 2*n / 3 \le (sqrt(2*n)/2)*S(log 2 (2*n)).
1217 intros.
1218 rewrite < (eq_log_exp 2)
1219   [apply (trans_le ? (log 2 ((exp (2*n) (sqrt(2*n)/2)))))
1220     [apply le_log
1221       [apply le_n
1222       |apply not_bertrand_to_le1;assumption
1223       ]
1224     |apply log_exp1.
1225      apply le_n
1226     ]
1227   |apply le_n
1228   ]
1229 qed.
1230
1231 theorem tech1: \forall a,b,c,d.O < b \to O < d \to
1232 (a/b)*(c/d) \le (a*c)/(b*d).
1233 intros.
1234 apply le_times_to_le_div
1235   [rewrite > (times_n_O O).
1236    apply lt_times;assumption
1237   |rewrite > assoc_times.
1238    rewrite < assoc_times in ⊢ (? (? ? %) ?).
1239    rewrite < sym_times in ⊢ (? (? ? (? % ?)) ?).
1240    rewrite > assoc_times.
1241    rewrite < assoc_times.
1242    apply le_times;
1243    rewrite > sym_times;apply le_times_div_m_m;assumption
1244   ]
1245 qed.
1246
1247 theorem tech: \forall n. 2*(S(log 2 (2*n))) \le sqrt (2*n) \to
1248 (sqrt(2*n)/2)*S(log 2 (2*n)) \le 2*n / 4.
1249 intros.
1250 cut (4*(S(log 2 (2*n))) \le 2* sqrt(2*n))
1251   [rewrite > sym_times.
1252    apply le_times_to_le_div
1253     [apply lt_O_S
1254     |rewrite < assoc_times.
1255      apply (trans_le ? (2*sqrt(2*n)*(sqrt (2*n)/2)))
1256       [apply le_times_l.assumption
1257       |apply (trans_le ? ((2*sqrt(2*n)*(sqrt(2*n))/2)))
1258         [apply le_times_div_div_times.
1259          apply lt_O_S
1260         |rewrite > assoc_times.
1261          rewrite > sym_times.
1262          rewrite > lt_O_to_div_times.
1263          apply leq_sqrt_n.
1264          apply lt_O_S
1265         ]
1266       ]
1267     ]
1268   |change in ⊢ (? (? % ?) ?) with (2*2).
1269    rewrite > assoc_times.
1270    apply le_times_r.
1271    assumption
1272   ]
1273 qed.
1274
1275 theorem lt_div_S_div: \forall n,m. O < m \to exp m 2 \le n \to
1276 n/(S m) < n/m.
1277 intros.
1278 apply lt_times_to_lt_div.
1279 apply (lt_to_le_to_lt ? (S(n/m)*m))
1280   [apply lt_div_S.assumption
1281   |rewrite > sym_times in ⊢ (? ? %). simplify.
1282    rewrite > sym_times in ⊢ (? ? (? ? %)).
1283    apply le_plus_l.
1284    apply le_times_to_le_div
1285     [assumption
1286     |rewrite < exp_SSO.
1287      assumption
1288     ]
1289   ]
1290 qed.
1291
1292 theorem exp_plus_SSO: \forall a,b. exp (a+b) 2 = (exp a 2) + 2*a*b + (exp b 2).
1293 intros.
1294 rewrite > exp_SSO.
1295 rewrite > distr_times_plus.
1296 rewrite > times_plus_l.
1297 rewrite < exp_SSO.
1298 rewrite > assoc_plus.
1299 rewrite > assoc_plus.
1300 apply eq_f.
1301 rewrite > times_plus_l.
1302 rewrite < exp_SSO.
1303 rewrite < assoc_plus.
1304 rewrite < sym_times.
1305 rewrite > plus_n_O in ⊢ (? ? (? (? ? %) ?) ?).
1306 rewrite > assoc_times.
1307 apply eq_f2;reflexivity.
1308 qed.
1309
1310 theorem tech3: \forall n. (exp 2 8) \le n \to 2*(S(log 2 (2*n))) \le sqrt (2*n).
1311 intros.
1312 lapply (le_log 2 ? ? (le_n ?) H) as H1.
1313 rewrite > exp_n_SO in ⊢ (? (? ? (? (? ? (? % ?)))) ?).
1314 rewrite > log_exp
1315   [rewrite > sym_plus.
1316    rewrite > plus_n_Sm.
1317    unfold sqrt.
1318    apply f_m_to_le_max
1319     [apply le_times_r.
1320      apply (trans_le ? (2*log 2 n))
1321       [rewrite < times_SSO_n.
1322        apply le_plus_r.
1323        apply (trans_le ? 8)
1324         [apply leb_true_to_le.reflexivity
1325         |rewrite < (eq_log_exp 2)
1326           [assumption
1327           |apply le_n
1328           ]
1329         ]
1330       |apply (trans_le ? ? ? ? (le_exp_log 2 ? ? )).
1331        apply le_times_SSO_n_exp_SSO_n.
1332        apply (lt_to_le_to_lt ? ? ? ? H).
1333        apply leb_true_to_le.reflexivity
1334       ]
1335     |apply le_to_leb_true.
1336      rewrite > assoc_times.
1337      apply le_times_r.
1338      rewrite > sym_times.
1339      rewrite > assoc_times.
1340      rewrite < exp_SSO.
1341      rewrite > exp_plus_SSO.
1342      rewrite > distr_times_plus.
1343      rewrite > distr_times_plus.
1344      rewrite > assoc_plus.
1345      apply (trans_le ? (4*exp (log 2 n) 2))
1346       [change in ⊢ (? ? (? % ?)) with (2*2).
1347        rewrite > assoc_times in ⊢ (? ? %).
1348        rewrite < times_SSO_n in ⊢ (? ? %).
1349        apply le_plus_r.
1350        rewrite < times_SSO_n in ⊢ (? ? %).
1351        apply le_plus
1352         [rewrite > sym_times in ⊢ (? (? ? %) ?).
1353          rewrite < assoc_times.
1354          rewrite < assoc_times.
1355          change in ⊢ (? (? % ?) ?) with 8.
1356          rewrite > exp_SSO.
1357          apply le_times_l.
1358          (* strange things here *)
1359          rewrite < (eq_log_exp 2)
1360           [assumption
1361           |apply le_n
1362           ]
1363         |apply (trans_le ? (log 2 n))
1364           [change in ⊢ (? % ?) with 8.
1365            rewrite < (eq_log_exp 2)
1366             [assumption
1367             |apply le_n
1368             ]
1369           |rewrite > exp_n_SO in ⊢ (? % ?).
1370            apply le_exp
1371             [apply lt_O_log
1372               [apply (lt_to_le_to_lt ? ? ? ? H).
1373                apply leb_true_to_le.reflexivity
1374               |apply (lt_to_le_to_lt ? ? ? ? H).
1375                apply leb_true_to_le.reflexivity
1376               ]
1377             |apply le_n_Sn
1378             ]
1379           ]
1380         ]
1381       |change in ⊢ (? (? % ?) ?) with (exp 2 2).
1382        apply (trans_le ? ? ? ? (le_exp_log 2 ? ?))
1383         [apply le_times_exp_n_SSO_exp_SSO_n
1384           [apply le_n
1385           |change in ⊢ (? % ?) with 8.
1386            rewrite < (eq_log_exp 2)
1387             [assumption
1388             |apply le_n
1389             ]
1390           ]
1391         |apply (lt_to_le_to_lt ? ? ? ? H).
1392          apply leb_true_to_le.reflexivity
1393         ]
1394       ]
1395     ]
1396   |apply le_n
1397   |apply (lt_to_le_to_lt ? ? ? ? H).
1398    apply leb_true_to_le.reflexivity
1399   ]
1400 qed.
1401
1402 theorem le_to_bertrand2:
1403 \forall n. (exp 2 8) \le n \to bertrand n.
1404 intros.
1405 apply not_not_bertrand_to_bertrand.unfold.intro.
1406 absurd (2*n / 3 \le (sqrt(2*n)/2)*S(log 2 (2*n)))
1407   [apply not_bertrand_to_le2
1408     [apply (trans_le ? ? ? ? H).
1409      apply le_exp
1410       [apply lt_O_S
1411       |apply le_n_Sn
1412       ]
1413     |assumption
1414     ]
1415   |apply lt_to_not_le.
1416    apply (le_to_lt_to_lt ? ? ? ? (lt_div_S_div ? ? ? ?))
1417     [apply tech.apply tech3.assumption
1418     |apply lt_O_S
1419     |apply (trans_le ? (2*exp 2 8))
1420       [apply leb_true_to_le.reflexivity
1421       |apply le_times_r.assumption
1422       ]
1423     ]
1424   ]
1425 qed.
1426
1427 theorem bertrand_n :
1428 \forall n. O < n \to bertrand n.
1429 intros;elim (decidable_le n 256)
1430   [apply le_to_bertrand;assumption
1431   |apply le_to_bertrand2;apply lt_to_le;apply not_le_to_lt;apply H1]
1432 qed.
1433
1434 (* test
1435 theorem mod_exp: eqb (mod (exp 2 8) 13) O = false.
1436 reflexivity.
1437 *)