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