]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/arithmetics/minimization.ma
partial commit ...
[helm.git] / matita / matita / lib / arithmetics / minimization.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/nat.ma".
13
14 (* maximization *)
15
16 let rec max' i f d ≝
17   match i with 
18   [ O ⇒ d
19   | S j ⇒ 
20       match (f j) with 
21       [ true ⇒ j
22       | false ⇒ max' j f d]].
23       
24 definition max ≝ λn.λf.max' n f O.
25
26 theorem max_O: ∀f. max O f = O.
27 // qed.
28
29 theorem max_cases: ∀f.∀n.
30   (f n = true ∧ max (S n) f = n) ∨ 
31   (f n  = false ∧ max (S n) f = max n f).
32 #f #n normalize cases (f n) normalize /3/ qed.
33
34 theorem le_max_n: ∀f.∀n. max n f ≤ n.
35 #f #n (elim n) // #m #Hind 
36 normalize (cases (f m)) normalize @le_S // 
37 (* non trova Hind *)
38 @Hind
39 qed.
40
41 theorem lt_max_n : ∀f.∀n. O < n → max n f < n.
42 #f #n #posn @(lt_O_n_elim ? posn) #m
43 normalize (cases (f m)) normalize @le_S_S //
44 @le_max_n qed.
45
46 theorem le_to_le_max : ∀f.∀n,m.
47 n ≤ m  → max n f ≤ max m f.
48 #f #n #m #H (elim H) //
49 #i #leni #Hind @(transitive_le … Hind)
50 (cases (max_cases f i)) * #_ /2/ 
51 qed.
52
53 theorem true_to_le_max: ∀f.∀n,m.
54  m < n → f m = true → m ≤ max n f.
55 #f #n (elim n)
56   [#m #ltmO @False_ind /2/
57   |#i #Hind #m #ltm 
58    (cases (le_to_or_lt_eq … (le_S_S_to_le … ltm)))
59     [#ltm #fm @(transitive_le ? (max i f)) 
60       [@Hind /2/ | @le_to_le_max //]
61     |#eqm >eqm #eqf normalize >eqf //
62  ] 
63 qed.
64
65 theorem lt_max_to_false: ∀f.∀n,m.
66  m < n → max n f < m → f m = false.
67 #f #n #m #ltnm #eqf cases(true_or_false (f m)) //
68 #fm @False_ind @(absurd … eqf) @(le_to_not_lt) @true_to_le_max //
69 qed.
70
71 lemma max_exists: ∀f.∀n,m.m < n → f m =true →
72  (∀i. m < i → i < n → f i = false) → max n f = m.
73 #f #n (elim n) #m
74   [#ltO @False_ind /2/ 
75   |#Hind #max #ltmax #fmax #ismax
76    cases (le_to_or_lt_eq …(le_S_S_to_le …(ltmax …)))
77    #ltm normalize 
78      [>(ismax m …) // normalize @(Hind max ltm fmax)
79       #i #Hl #Hr @ismax // @le_S //
80      |<ltm >fmax // 
81      ]
82    ]
83 qed.
84
85 lemma max_not_exists: ∀f.∀n.
86  (∀i. i < n → f i = false) → max n f = O.
87 #f #n #ffalse @(le_gen ? n) #i (elim i) // #j #Hind #ltj
88 normalize >ffalse // @Hind /2/
89 qed.
90
91 lemma fmax_false: ∀f.∀n,m.max n f = m → f m = false → m = O. 
92 #f #n #m (elim n) //
93 #i #Hind normalize cases(true_or_false … (f i)) #fi >fi
94 normalize 
95   [#eqm #fm @False_ind @(absurd … fi) // |@Hind]
96 qed. 
97   
98 inductive max_spec (n:nat) (f:nat→bool) : nat→Prop ≝
99  | found : ∀m:nat.m < n → f m =true →
100  (∀i. m < i → i < n → f i = false) → max_spec n f m
101  | not_found: (∀i.i < n → f i = false) → max_spec n f O.
102  
103 theorem max_spec_to_max: ∀f.∀n,m.
104   max_spec n f m → max n f = m.
105 #f #n #m #spec (cases spec) 
106   [#max #ltmax #fmax #ismax @max_exists // @ismax
107   |#ffalse @max_not_exists @ffalse
108   ] 
109 qed.
110
111 theorem max_to_max_spec: ∀f.∀n,m.
112   max n f = m → max_spec n f m.
113 #f #n #m (cases n)
114   [#eqm <eqm %2 #i #ltiO @False_ind /2/ 
115   |#n #eqm cases(true_or_false (f m)) #fm
116     (* non trova max_to_false *)
117     [%1 /2/
118     |lapply (fmax_false ??? eqm fm) #eqmO >eqmO
119      %2 #i (cases i) // #j #ltj @(lt_max_to_false … ltj) //
120 qed.
121
122 theorem max_f_g: ∀f,g,n.(∀i. i < n → f i = g i) → 
123   max n f = max n g.
124 #f #g #n (elim n) //
125 #m #Hind #ext normalize >ext normalize in Hind; >Hind //
126 #i #ltim @ext @le_S //
127 qed.
128
129 theorem le_max_f_max_g: ∀f,g,n. (∀i. i < n → f i = true → g i =true) →
130 max n f ≤ max n g.
131 #f #g #n (elim n) //
132 #m #Hind #ext normalize (cases (true_or_false (f m))) #Heq >Heq 
133   [>ext //
134   |(cases (g m)) normalize [@le_max_n] @Hind #i #ltim @ext @le_S //
135 qed.
136
137 theorem f_max_true : ∀ f.∀n.
138 (∃i:nat. i < n ∧ f i = true) → f (max n f) = true. 
139 #f #n cases(max_to_max_spec f n (max n f) (refl …)) //
140 #Hall * #x * #ltx #fx @False_ind @(absurd … fx) >Hall /2/
141 qed.
142
143 theorem f_false_to_le_max: ∀f,n,p. (∃i:nat.i<n∧f i=true) →
144   (∀m. p < m → f m = false) → max n f ≤ p.
145 #f #n #p #H1 #H2 @not_lt_to_le % #H3
146 @(absurd ?? not_eq_true_false) <(H2 ? H3) @sym_eq
147 @(f_max_true ? n H1)
148 qed.
149
150 theorem exists_forall_lt:∀f,n. 
151 (∃i. i < n ∧ f i = true) ∨ (∀i. i < n → f i = false).
152 #f #n elim n
153   [%2 #i #lti0 @False_ind @(absurd ? lti0) @le_to_not_lt // 
154   |#n1 *
155     [* #a * #Ha1 #Ha2 %1 %{a} % // @le_S //
156     |#H cases (true_or_false (f n1)) #HfS >HfS
157       [%1 %{n1} /2/
158       |%2 #i #lei 
159        cases (le_to_or_lt_eq ?? lei) #Hi 
160         [@H @le_S_S_to_le @Hi | destruct (Hi) //] 
161       ]
162     ]
163   ]
164 qed.
165      
166 theorem exists_max_forall_false:∀f,n. 
167 ((∃i. i < n ∧ f i = true) ∧ (f (max n f) = true))∨
168 ((∀i. i < n → f i = false) ∧ (max n f) = O).
169 #f #n
170 cases (exists_forall_lt f n)
171   [#H %1 % // @(f_max_true f n) @H
172   |#H %2 % [@H | @max_not_exists @H 
173   ]
174 qed.
175
176
177 theorem false_to_lt_max: ∀f,n,m.O < n →
178   f n = false → max m f ≤ n → max m f < n.
179 #f #n #m #posn #Hfn #Hmax cases (le_to_or_lt_eq ?? Hmax) -Hmax #Hmax 
180   [//
181   |cases (exists_max_forall_false f m)
182     [* #_ #Hfmax @False_ind @(absurd ?? not_eq_true_false) //
183     |* //
184     ]
185   ]
186 qed.
187
188 (* minimization *)
189  
190 (* min k b f is the minimun i, b ≤ i < b + k s.t. f i;  
191    returns  b + k otherwise *)
192    
193 let rec min k b f ≝
194   match k with
195   [ O ⇒ b
196   | S p ⇒ 
197     match f b with
198    [ true ⇒ b
199    | false ⇒ min p (S b) f]].
200
201 definition min0 ≝ λn.λf. min n 0 f.
202
203 theorem min_O_f : ∀f.∀b. min O b f = b.
204 // qed.
205
206 theorem true_min: ∀f.∀b.
207   f b = true → ∀n.min n b f = b.
208 #f #b #fb #n (cases n) // #n normalize >fb normalize //
209 qed.
210
211 theorem false_min: ∀f.∀n,b.
212   f b = false → min (S n) b f = min n (S b) f.
213 #f #n #b #fb normalize >fb normalize //
214 qed.
215
216 (*
217 theorem leb_to_le_min : ∀f.∀n,b1,b2.
218 b1 ≤ b2  → min n b1 f ≤ min n b2 f.
219 #f #n #b1 #b2 #leb (elim n) //
220 #m #Hind normalize (cases (f m)) normalize *)
221
222 theorem le_min_r: ∀f.∀n,b. min n b f ≤ n + b.
223 #f #n normalize (elim n) // #m #Hind #b 
224 normalize (cases (f b)) normalize // 
225 qed.
226
227 theorem le_min_l: ∀f.∀n,b. b ≤ min n b f.
228 #f #n normalize (elim n) // #m #Hind #b 
229 normalize (cases (f b)) normalize /2/ 
230 qed.
231
232 theorem le_to_le_min : ∀f.∀n,m.
233 n ≤ m  → ∀b.min n b f ≤ min m b f.
234 #f @nat_elim2 //
235   [#n #leSO @False_ind /2/ 
236   |#n #m #Hind #leSS #b
237    (cases (true_or_false (f b))) #fb 
238     [lapply (true_min …fb) #H >H >H //
239     |>false_min // >false_min // @Hind /2/
240     ]
241   ]
242 qed.
243
244 theorem true_to_le_min: ∀f.∀n,m,b.
245  b ≤ m → f m = true → min n b f ≤ m.
246 #f #n (elim n) //
247 #i #Hind #m #b #leb (cases (le_to_or_lt_eq … leb))
248   [#ltm #fm normalize (cases (f b)) normalize // @Hind //
249   |#eqm <eqm #eqb normalize >eqb normalize //
250   ] 
251 qed.
252
253 theorem lt_min_to_false: ∀f.∀n,m,b. 
254  b ≤ m → m < min n b f → f m = false.
255 #f #n #m #b #lebm #ltm cases(true_or_false (f m)) //
256 #fm @False_ind @(absurd … ltm) @(le_to_not_lt) @true_to_le_min //
257 qed.
258
259 theorem fmin_true: ∀f.∀n,m,b.
260  m = min n b f → m < n + b → f m = true. 
261 #f #n (elim n)
262   [#m #b normalize #eqmb >eqmb #leSb @(False_ind) 
263    @(absurd … leSb) //
264   |#n #Hind #m #b (cases (true_or_false (f b))) #caseb
265     [>true_min //
266     |>false_min // #eqm #ltm @(Hind m (S b)) /2/
267     ]
268   ]
269 qed.
270
271 lemma min_exists: ∀f.∀t,m. m < t → f m = true →
272 ∀k,b.b ≤ m → (∀i. b ≤ i → i < m → f i = false) → t = k + b → 
273   min k b f = m. 
274 #f #t #m #ltmt #fm #k (elim k)
275   [#b #lebm #ismin #eqtb @False_ind @(absurd … lebm) <eqtb
276    @lt_to_not_le //
277   |#d #Hind #b #lebm #ismin #eqt cases(le_to_or_lt_eq …lebm)
278     [#ltbm >false_min /2 by le_n/ @Hind //
279       [#i #H #H1 @ismin /2/ | >eqt normalize //] 
280     |#eqbm >true_min //
281     ]
282   ]
283 qed.
284
285 lemma min_not_exists: ∀f.∀n,b.
286  (∀i. b ≤ i → i < n + b → f i = false) → min n b f = n + b.
287 #f #n (elim n) // 
288 #p #Hind #b #ffalse >false_min
289   [>Hind // #i #H #H1 @ffalse /2/
290   |@ffalse //
291   ]
292 qed.
293
294 lemma fmin_false: ∀f.∀n,b.let m ≝ min n b f in 
295  f m = false → m = n+b. 
296 #f #n (elim n) //
297 #i #Hind #b normalize cases(true_or_false … (f b)) #fb >fb
298 normalize 
299   [#eqm @False_ind @(absurd … fb) // 
300   |>plus_n_Sm @Hind]
301 qed.
302
303 inductive min_spec (n,b:nat) (f:nat→bool) : nat→Prop ≝
304  | found : ∀m:nat. b ≤ m → m < n + b → f m =true →
305  (∀i. b ≤ i → i < m → f i = false) → min_spec n b f m
306  | not_found: (∀i.b ≤ i → i < (n + b) → f i = false) → min_spec n b f (n+b).
307  
308 theorem min_spec_to_min: ∀f.∀n,b,m.
309   min_spec n b f m → min n b f = m.
310 #f #n #b #m #spec (cases spec) 
311   [#m #lem #ltm #fm #ismin @(min_exists f (n+b)) // @ismin
312   |#ffalse @min_not_exists @ffalse
313   ] 
314 qed.
315
316 theorem min_to_min_spec: ∀f.∀n,b,m.
317   min n b f = m → min_spec n b f m.
318 #f #n #b #m (cases n)
319   [#eqm <eqm %2 #i #lei #lti @False_ind @(absurd … lti) /2/
320   |#n #eqm (* (cases (le_to_or_lt_eq … (le_min_r …))) Stack overflow! *)
321    lapply (le_min_r f (S n) b) >eqm #lem
322    (cases (le_to_or_lt_eq … lem)) #mcase
323     [%1 /2/ #i #H #H1 @(lt_min_to_false f (S n) i b) //
324     |>mcase %2 #i #lebi #lti @(lt_min_to_false f (S n) i b) //
325     ]
326   ]
327 qed.
328
329 theorem min_f_g: ∀f,g,n,b.(∀i. b ≤ i → i < n + b → f i = g i) → 
330   min n b f = min n b g.
331 #f #g #n (elim n) //
332 #m #Hind #b #ext normalize >(ext b (le_n b) ?) // >Hind //
333 #i #ltib #ltim @ext // @lt_to_le //
334 qed.
335
336 theorem le_min_f_min_g: ∀f,g,n,b. (∀i. b ≤ i → i < n +b → f i = true → g i =true) →
337 min n b g ≤ min n b f.
338 #f #g #n (elim n) //
339 #m #Hind #b #ext normalize (cases (true_or_false (f b))) #Heq >Heq 
340   [>ext //
341   |(cases (g b)) normalize /2 by lt_to_le/ @Hind #i #ltb #ltim #fi
342     @ext /2/
343   ]
344 qed.
345
346 theorem f_min_true : ∀ f.∀n,b.
347 (∃i:nat. b ≤ i ∧ i < n + b ∧ f i = true) → f (min n b f) = true. 
348 #f #n #b cases(min_to_min_spec f n b (min n b f) (refl …)) //
349 #Hall * #x * * #leb #ltx #fx @False_ind @(absurd … fx) >Hall /2/
350 qed.
351
352 theorem lt_min : ∀ f.∀n,b.
353 (∃i:nat. b ≤ i ∧ i < n + b ∧ f i = true) → min n b f < n + b. 
354 #f #n #b #H cases H #i * * #lebi #ltin #fi_true  
355 @(le_to_lt_to_lt … ltin) @true_to_le_min //
356 qed.