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 (* check *)
 159 theorem primes_below_to_bertrand:
 160 ∀pm,l.prime pm → primes_below l (S pm)  →
 161   (∀p. mem ? p l → 2 < p → ∃pp. mem ? pp l ∧ pp < p ∧ p ≤ 2*pp)
 162     → ∀n.0 < n → n < pm → bertrand n.
 163 #pm #l #primepm * * #Hall #Hbelow #Hcomplete #H #n #posn #ltn
 164 cases (min_prim n) #p1 * * #ltnp1 #primep1 #Hmin
 165 %{p1} % // % [//]
 166 cases(le_to_or_lt_eq ? ? (prime_to_lt_SO ? primep1)) #Hp1
 167   [cases (H … Hp1)
 168     [#x * * #memxl #ltxp1 #Hp1 @(transitive_le … Hp1) @monotonic_le_times_r
 169      @Hmin [@Hall //|//]
 170     |@Hcomplete [//] @le_S_S @not_lt_to_le % #ltpm @(absurd ? ltn)
 171      @le_to_not_lt @Hmin //
 172     ]
 173   |<Hp1 >(times_n_1 2) in ⊢ (?%?); @monotonic_le_times_r //
 174   ]
 175 qed.
 176
 177 let rec checker l ≝
 178   match l with
 179   [ nil ⇒ true
 180   | cons hd tl ⇒
 181     match tl with
 182      [ nil ⇒ true
 183      | cons hd1 tl1 ⇒
 184        leb (S hd) hd1 ∧ leb hd1 (2*hd) ∧ checker tl
 185     ]
 186   ].
 187
 188 lemma checker_ab: ∀a,b,l.checker (a::b::l) =
 189   (leb (S a) b ∧ leb b (2*a) ∧ checker (b::l)).
 190 // qed.
 191
 192 lemma checker_abl: ∀a,b,l.checker (a::b::l) = true →
 193   a < b ∧ b ≤ 2*a ∧ checker (b::l) = true.
 194 #a #b #l >checker_ab #H
 195 % [% [@leb_true_to_le @(andb_true_l … (andb_true_l … H))
 196      |@leb_true_to_le @(andb_true_r … (andb_true_l … H))
 197      ]
 198   |@(andb_true_r … H)
 199   ]
 200 qed.
 201
 202 theorem checker_spec: ∀tl,a,l. checker l = true → l = a::tl →
 203   ∀p. mem ? p tl → ∃pp. mem nat pp l ∧ pp < p ∧ p ≤ 2*pp.
 204 #tl elim tl
 205   [#a #l #_ #_ #p whd in ⊢ (%→?); @False_ind
 206   |#b #tl #Hind #a #l #Hc #Hl #p #Hmem >Hl in Hc;
 207    #Hc cases(checker_abl … Hc) *
 208    #ltab #leb #Hc2 cases Hmem #Hc
 209     [>Hc -Hc %{a} % [ % [ % % |//]|//]
 210     |cases(Hind b (b::tl) Hc2 (refl …) ? Hc) #pp * * #Hmemnp #ltpp #lepp
 211      %{pp} % [ % [ %2 //|//]|//]
 212     ]
 213   ]
 214 qed.
 215
 216 lemma bertrand_down : ∀n.O < n → n ≤ 2^8 → bertrand n.
 217 #n #posn #len
 218 cut (∃it.it=2^8) [%{(2^8)} %] * #it #itdef
 219 lapply(primes_below_lop … it) * * #Hall #Hbelow #Hcomplete
 220 @(primes_below_to_bertrand (S it) (list_of_primes it) … posn)
 221   [@primeb_true_to_prime >itdef %
 222   |>(plus_n_O it) in ⊢ (??%); >plus_n_Sm >plus_n_Sm @primes_below_lop
 223   |#p #memp #lt2p @(checker_spec (tail ? (list_of_primes it)) 2 (list_of_primes it))
 224     [>itdef %
 225     |>itdef @eq_lop @lt_O_S
 226     |>eq_lop in memp; [2:>itdef @lt_O_S] *
 227       [#eqp2 @False_ind @(absurd ? lt2p) @le_to_not_lt >eqp2 @le_n
 228       |#H @H
 229       ]
 230     ]
 231   |@le_S_S >itdef @len
 232   ]
 233 qed.
 234
 235 theorem bertrand :
 236 ∀n. O < n → bertrand n.
 237 #n #posn elim (decidable_le n 256)
 238   [@bertrand_down //
 239   |#len @le_to_bertrand2 @lt_to_le @not_le_to_lt @len]
 240 qed.
 241