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