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