]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/arithmetics/chebyshev/bertrand256.ma
progress
[helm.git] / 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 @bertrand_up @lt_to_le @not_le_to_lt @len]
240 qed.
241