matita/matita/lib/arithmetics/chebyshev/bertrand256.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "arithmetics/chebyshev/bertrand.ma".
  13 include "basics/lists/list.ma".
  14
  15 let rec list_divides l n ≝
  16   match l with
  17   [ nil ⇒ false
  18   | cons (m:nat) (tl:list nat) ⇒ orb (dividesb m n) (list_divides tl n) ].
  19
  20 lemma list_divides_true: ∀l,n. list_divides l n = true → ∃p. mem ? p l ∧ p ∣ n.
  21 #l elim l
  22   [#n normalize in ⊢ (%→?); #H destruct (H)
  23   |#a #tl #Hind #b cases (true_or_false (dividesb a b)) #Hcase
  24     [#_ %{a} % [% // | @dividesb_true_to_divides //]
  25     |whd in ⊢ (??%?→?); >Hcase whd in ⊢ (??%?→?); #Htl
  26      cases (Hind b Htl) #d * #memd #divd %{d} % [%2 // | //]
  27     ]
  28   ]
  29 qed.
  30
  31 lemma list_divides_false: ∀l,n. list_divides l n = false →
  32   ∀p. mem ? p l → p \ndivides  n.
  33 #l elim l
  34   [#n #_ #p normalize in ⊢ (%→?); @False_ind
  35   |#a #tl #Hind #b cases (true_or_false (dividesb a b)) #Hcase
  36     [whd in ⊢ (??%?→?); >Hcase whd in ⊢ (??%?→?);
  37      #H destruct (H)
  38     |whd in ⊢ (??%?→?); >Hcase whd in ⊢ (??%?→?); #Htl #d *
  39       [#eqda >eqda @dividesb_false_to_not_divides //
  40       |#memd @Hind //
  41       ]
  42     ]
  43   ]
  44 qed.
  45
  46 let rec lprim m i acc ≝
  47   match m with
  48    [ O ⇒  acc
  49    | S m1 ⇒  match (list_divides acc i) with
  50      [ true ⇒  lprim m1 (S i) acc
  51      | false ⇒ lprim m1 (S i) (acc@[i]) ]].
  52
  53 definition list_of_primes ≝ λn. lprim n 2 [].
  54
  55 lemma lop_Strue: ∀m,i,acc. list_divides acc i =true →
  56   lprim (S m) i acc = lprim m (S i) acc.
  57 #m #i #acc #Hdiv normalize >Hdiv //
  58 qed.
  59
  60 lemma lop_Sfalse: ∀m,i,acc. list_divides acc i = false →
  61   lprim (S m) i acc = lprim m (S i) (acc@[i]).
  62 #m #i #acc #Hdiv normalize >Hdiv %
  63 qed.
  64
  65 lemma list_of_primes_def : ∀n. list_of_primes n = lprim n 2 [].
  66 // qed.
  67
  68 example lprim_ex: lprim 8 2 [ ] = [2; 3; 5; 7]. // qed.
  69
  70 lemma start_lprim: ∀n,m,a,acc.
  71   option_hd ? (lprim n m (a::acc)) = Some ? a.
  72 #n elim n
  73   [#m #a #acc %
  74   |#n1 #Hind #m #a #acc cases (true_or_false (list_divides (a::acc) m)) #Hc
  75     [>lop_Strue [@Hind | //] |>lop_Sfalse [@Hind |//]
  76   ]
  77 qed.
  78
  79 lemma start_lop: ∀n. 1 ≤ n →
  80   option_hd ? (list_of_primes n) = Some ? 2.
  81 #n #posn cases posn //
  82   #m #lem >list_of_primes_def normalize in ⊢ (??(??%)?);
  83   >start_lprim //
  84 qed.
  85
  86 lemma eq_lop: ∀n. 1 ≤ n →
  87   list_of_primes n = 2::(tail ? (list_of_primes n)).
  88 #n #posn lapply (start_lop ? posn) cases (list_of_primes n)
  89   [whd in ⊢ (??%?→?); #H destruct (H)
  90   |normalize #a #l #H destruct (H) //
  91   ]
  92 qed.
  93
  94
  95 (* properties *)
  96
  97 definition all_primes ≝ λl.∀p. mem nat p l → prime p.
  98
  99 definition all_below ≝ λl,n.∀p. mem nat p l → p < n.
 100
 101 definition primes_all ≝ λl,n. ∀p. prime p → p < n → mem nat p l.
 102
 103 definition primes_below ≝ λl,n.
 104   all_primes l ∧ all_below l n ∧ primes_all l n.
 105
 106 lemma ld_to_prime: ∀i,acc. 1 < i →
 107   primes_below acc i → list_divides acc i = false → prime i.
 108 #i #acc #posi * * #Hall #Hbelow #Hcomplete #Hfalse % //
 109 #m #mdivi
 110 cut (m ≤ i)[@divides_to_le [@lt_to_le //|//]] #lemi
 111 cases (le_to_or_lt_eq … lemi) [2://] #ltmi
 112 #lt1m @False_ind
 113 cut (divides (smallest_factor m) i)
 114   [@(transitive_divides … mdivi) @divides_smallest_factor_n @lt_to_le //]
 115 #Hcut @(absurd … Hcut) @(list_divides_false … Hfalse) @Hcomplete
 116   [@prime_smallest_factor_n // | @(le_to_lt_to_lt … ltmi) //]
 117 qed.
 118
 119 lemma lprim_invariant: ∀n,i,acc. 1 < i →
 120   primes_below acc i → primes_below (lprim n i acc) (n+i).
 121 #n elim n
 122   [#i #acc #lt1i #H @H
 123   |#m #Hind #i #acc #lt1i * * #Hall #Hbelow #Hcomplete cases (true_or_false (list_divides acc i)) #Hc
 124     [>(lop_Strue … Hc) whd in ⊢ (??%); >plus_n_Sm @(Hind … (le_S … lt1i)) %
 125       [% [// |#p #memp @le_S @Hbelow //]
 126       |#p #primep #lepi cases (le_to_or_lt_eq … (le_S_S_to_le … lepi))
 127         [#ltpi @Hcomplete //
 128         |#eqpi @False_ind cases (list_divides_true … Hc) #q * #memq #divqi
 129          cases primep #lt1p >eqpi #Hi @(absurd (q=i))
 130           [@Hi [@divqi |@prime_to_lt_SO @Hall //]
 131           |@lt_to_not_eq @Hbelow //
 132           ]
 133         ]
 134       ]
 135     |>(lop_Sfalse … Hc) whd in ⊢ (??%); >plus_n_Sm @(Hind … (le_S … lt1i)) %
 136       [% [#p #memp cases (mem_append ???? memp) -memp #memp
 137            [@Hall //|>(mem_single ??? memp) @(ld_to_prime … Hc) // % [% // |//]]
 138       |#p #memp cases (mem_append ???? memp) -memp #memp
 139          [@le_S @Hbelow // |<(mem_single ??? memp) @le_n]]
 140       |#p #memp #ltp cases (le_to_or_lt_eq … (le_S_S_to_le … ltp))
 141          [#ltpi @mem_append_l1 @Hcomplete //|#eqpi @mem_append_l2 <eqpi % //]
 142       ]
 143     ]
 144   ]
 145 qed.
 146
 147 lemma primes_below2: primes_below [] 2.
 148   %[%[#p @False_ind|#p @False_ind]
 149    |#p #primep #ltp2 @False_ind @(absurd … ltp2) @le_to_not_lt
 150     @prime_to_lt_SO //
 151    ]
 152 qed.
 153
 154 lemma primes_below_lop: ∀n. primes_below (list_of_primes n) (n+2).
 155 #n @lprim_invariant //
 156 qed.
 157
 158 let rec checker l ≝
 159   match l with
 160     [ nil ⇒  true
 161     | cons h1 t1 => match t1 with
 162       [ nil ⇒  true
 163       | cons h2 t2 ⇒ (andb (checker t1) (leb h1 (2*h2))) ]].
 164
 165 lemma checker_ab: ∀a,b,l.
 166   checker (a::b::l) = (andb (checker (b::l)) (leb a (2*b))).
 167 // qed.
 168
 169 lemma checker_cons : ∀a,l.checker (a::l) = true → checker l = true.
 170 #a #l cases l [//|#b #tl >checker_ab #H @(andb_true_l ?? H)]
 171 qed.
 172
 173 theorem list_of_primes_to_bertrand:
 174 ∀n,pn,l.0 < n → prime pn → n < pn → all_primes l  →
 175 (∀p. prime p → p ≤ pn → mem ? p l) →
 176 (∀p. mem ? p l → 2 < p →
 177   ∃pp. mem ? pp l ∧ pp < p ∧ p \le 2*pp) → bertrand n.
 178 #n #pn #l #posn #primepn #ltnp #allprimes #H1 #H2
 179 cases (min_prim n) #p1 * * #ltnp1 #primep1 #Hmin
 180 %{p1} % // % [//]
 181 cases(le_to_or_lt_eq ? ? (prime_to_lt_SO ? primep1)) #Hp1
 182   [cases (H2 … Hp1)
 183     [#x * * #memxl #ltxp1 #H @(transitive_le … H) @monotonic_le_times_r
 184      @Hmin [@allprimes //|//]
 185     |@H1 [//] @not_lt_to_le % #ltpn @(absurd ? ltnp)
 186      @le_to_not_lt @Hmin //
 187     ]
 188   |<Hp1 >(times_n_1 2) in ⊢ (?%?); @monotonic_le_times_r //
 189   ]
 190 qed.
 191
 192 let rec check_list l ≝
 193   match l with
 194   [ nil ⇒ true
 195   | cons (hd:nat) tl ⇒
 196     match tl with
 197      [ nil ⇒ true
 198      | cons hd1 tl1 ⇒
 199       (leb (S hd) hd1 ∧ leb hd1 (2*hd) ∧ check_list tl)
 200     ]
 201   ]
 202 .
 203
 204 lemma check_list_ab: ∀a,b,l.check_list (a::b::l) =
 205   (leb (S a) b ∧ leb b (2*a) ∧ check_list (b::l)).
 206 // qed.
 207
 208 lemma check_list_abl: ∀a,b,l.check_list (a::b::l) = true →
 209   a < b ∧
 210   b ≤ 2*a ∧
 211   check_list (b::l) = true ∧
 212   check_list l = true.
 213 #a #b #l >check_list_ab #H
 214 lapply (andb_true_r ?? H) #H1
 215 lapply (andb_true_l ?? H) -H #H2
 216 lapply (andb_true_r ?? H2) #H3
 217 lapply (andb_true_l ?? H2) -H2 #H4
 218 % [% [% [@(leb_true_to_le … H4) |@(leb_true_to_le … H3)]|@H1]
 219   |lapply H1 cases l
 220     [//
 221     |#c #d >check_list_ab #H @(andb_true_r … H)
 222     ]
 223   ]
 224 qed.
 225
 226 theorem check_list_spec: ∀tl,a,l. check_list l = true → l = a::tl →
 227   ∀p. mem ? p tl → ∃pp. mem nat pp l ∧ pp < p ∧ p ≤ 2*pp.
 228 #tl elim tl
 229   [#a #l #_ #_ #p whd in ⊢ (%→?); @False_ind
 230   |#b #tl #Hind #a #l #Hc #Hl #p #Hmem >Hl in Hc;
 231    #Hc cases(check_list_abl … Hc) * *
 232    #ltab #leb #Hc2 #Hc3 cases Hmem #Hc
 233     [>Hc -Hc %{a} % [ % [ % % |//]|//]
 234     |cases(Hind b (b::tl) Hc2 (refl …) ? Hc) #pp * * #Hmemnp #ltpp #lepp
 235      %{pp} % [ % [ %2 //|//]|//]
 236     ]
 237   ]
 238 qed.
 239
 240 lemma le_to_bertrand : ∀n.O < n → n ≤ 2^8 → bertrand n.
 241 #n #posn #len
 242 cut (∃it.it=2^8) [%{(2^8)} %] * #it #itdef
 243 lapply(primes_below_lop … it) * * #Hall #Hbelow #Hcomplete
 244 @(list_of_primes_to_bertrand ? (S it) (list_of_primes it) posn)
 245   [@primeb_true_to_prime >itdef %
 246   |@le_S_S >itdef @len
 247   |@Hall
 248   |#p #primep #lep @Hcomplete
 249     [@primep |<plus_n_Sm @le_S_S <plus_n_Sm <plus_n_O @lep]
 250   |#p #memp #lt2p @(check_list_spec (tail ? (list_of_primes it)) 2 (list_of_primes it))
 251     [>itdef %
 252     |>itdef @eq_lop @lt_O_S
 253     |>eq_lop in memp; [2:>itdef @lt_O_S] *
 254       [#eqp2 @False_ind @(absurd ? lt2p) @le_to_not_lt >eqp2 @le_n
 255       |#H @H
 256       ]
 257     ]
 258   ]
 259 qed.
 260
 261 theorem bertrand_n :
 262 ∀n. O < n → bertrand n.
 263 #n #posn elim (decidable_le n 256)
 264   [@le_to_bertrand //
 265   |#len @le_to_bertrand2 @lt_to_le @not_le_to_lt @len]
 266 qed.
 267
 268 (* test
 269 theorem mod_exp: eqb (mod (exp 2 8) 13) O = false.
 270 reflexivity.
 271 *)