]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/minimization.ma
...
[helm.git] / helm / software / matita / library / nat / minimization.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/minus.ma".
16
17 let rec max i f \def
18   match (f i) with 
19   [ true \Rightarrow i
20   | false \Rightarrow 
21       match i with 
22       [ O \Rightarrow O
23       | (S j) \Rightarrow max j f ]].
24
25 theorem max_O_f : \forall f: nat \to bool. max O f = O.
26 intro. simplify.
27 elim (f O).
28 simplify.reflexivity.
29 simplify.reflexivity.
30 qed. 
31
32 theorem max_S_max : \forall f: nat \to bool. \forall n:nat.
33 (f (S n) = true \land max (S n) f = (S n)) \lor 
34 (f (S n) = false \land max (S n) f = max n f).
35 intros.simplify.elim (f (S n)).
36 simplify.left.split.reflexivity.reflexivity.
37 simplify.right.split.reflexivity.reflexivity.
38 qed.
39
40 theorem le_max_n : \forall f: nat \to bool. \forall n:nat.
41 max n f \le n.
42 intros.elim n.rewrite > max_O_f.apply le_n.
43 simplify.elim (f (S n1)).simplify.apply le_n.
44 simplify.apply le_S.assumption.
45 qed.
46
47 theorem le_to_le_max : \forall f: nat \to bool. \forall n,m:nat.
48 n\le m  \to max n f \le max m f.
49 intros.elim H.
50 apply le_n.
51 apply (trans_le ? (max n1 f)).apply H2.
52 cut ((f (S n1) = true \land max (S n1) f = (S n1)) \lor 
53 (f (S n1) = false \land max (S n1) f = max n1 f)).
54 elim Hcut.elim H3.
55 rewrite > H5.
56 apply le_S.apply le_max_n.
57 elim H3.rewrite > H5.apply le_n.
58 apply max_S_max.
59 qed.
60
61 theorem f_m_to_le_max: \forall f: nat \to bool. \forall n,m:nat.
62 m\le n \to f m = true \to m \le max n f.
63 intros 3.elim n.apply (le_n_O_elim m H).
64 apply le_O_n.
65 apply (le_n_Sm_elim m n1 H1).
66 intro.apply (trans_le ? (max n1 f)).
67 apply H.apply le_S_S_to_le.assumption.assumption.
68 apply le_to_le_max.apply le_n_Sn.
69 intro.simplify.rewrite < H3. 
70 rewrite > H2.simplify.apply le_n.
71 qed.
72
73 theorem max_f_g: \forall f,g,n. (\forall i. i \le n \to f i = g i) \to
74 max n f = max n g.
75 intros 3.
76 elim n
77   [simplify.
78    rewrite > (H O)
79     [reflexivity
80     |apply le_n
81     ]
82   |simplify.
83    rewrite > H
84     [rewrite > H1
85       [reflexivity
86       |apply le_n
87       ]
88     |intros.
89      apply H1.
90      apply le_S.
91      assumption
92     ]
93   ]
94 qed.
95
96 theorem le_max_f_max_g: \forall f,g,n. (\forall i. i \le n \to f i = true \to g i =true) \to
97 max n f \le max n g.
98 intros 3.
99 elim n
100   [simplify.
101    elim (f O);apply le_O_n
102   |simplify.
103    apply (bool_elim ? (f (S n1)));intro
104     [rewrite > (H1 (S n1) ? H2)
105       [apply le_n
106       |apply le_n
107       ]
108     |cases (g(S n1))
109       [simplify.
110        apply le_S.
111        apply le_max_n
112       |simplify.
113        apply H.
114        intros.
115        apply H1
116         [apply le_S.assumption
117         |assumption
118         ]
119       ]
120     ]
121   ]
122 qed.
123
124
125 theorem max_O : \forall f:nat \to bool. \forall n:nat.
126 (\forall i:nat. le i n \to f i = false) \to max n f = O.
127 intros 2.elim n
128   [simplify.rewrite > H
129     [reflexivity
130     |apply le_O_n
131     ]
132   |simplify.rewrite > H1
133     [simplify.apply H.
134      intros.
135      apply H1.
136      apply le_S.
137      assumption
138     |apply le_n
139     ]
140   ]
141 qed.
142
143 theorem f_max_true : \forall f:nat \to bool. \forall n:nat.
144 (\exists i:nat. le i n \land f i = true) \to f (max n f) = true. 
145 intros 2.
146 elim n.elim H.elim H1.generalize in match H3.
147 apply (le_n_O_elim a H2).intro.simplify.rewrite > H4.
148 simplify.assumption.
149 simplify.
150 apply (bool_ind (\lambda b:bool.
151 (f (S n1) = b) \to (f (match b in bool with
152 [ true \Rightarrow (S n1)
153 | false  \Rightarrow (max n1 f)])) = true)).
154 simplify.intro.assumption.
155 simplify.intro.apply H.
156 elim H1.elim H3.generalize in match H5.
157 apply (le_n_Sm_elim a n1 H4).
158 intros.
159 apply (ex_intro nat ? a).
160 split.apply le_S_S_to_le.assumption.assumption.
161 intros.apply False_ind.apply not_eq_true_false.
162 rewrite < H2.rewrite < H7.rewrite > H6. reflexivity.
163 reflexivity.
164 qed.
165
166 theorem exists_forall_le:\forall f,n. 
167 (\exists i. i \le n \land f i = true) \lor
168 (\forall i. i \le n \to f i = false).
169 intros.
170 elim n
171   [apply (bool_elim ? (f O));intro
172     [left.apply (ex_intro ? ? O).
173      split[apply le_n|assumption]
174     |right.intros.
175      apply (le_n_O_elim ? H1).
176      assumption
177     ]
178   |elim H
179     [elim H1.elim H2.
180      left.apply (ex_intro ? ? a).
181      split[apply le_S.assumption|assumption]
182     |apply (bool_elim ? (f (S n1)));intro
183       [left.apply (ex_intro ? ? (S n1)).
184        split[apply le_n|assumption]
185       |right.intros.
186        elim (le_to_or_lt_eq ? ? H3)
187         [apply H1.
188          apply le_S_S_to_le.
189          apply H4
190         |rewrite > H4.
191          assumption
192         ]
193       ]
194     ]
195   ]
196 qed.
197      
198 theorem exists_max_forall_false:\forall f,n. 
199 ((\exists i. i \le n \land f i = true) \land (f (max n f) = true))\lor
200 ((\forall i. i \le n \to f i = false) \land (max n f) = O).
201 intros.
202 elim (exists_forall_le f n)
203   [left.split
204     [assumption
205     |apply f_max_true.assumption
206     ]
207   |right.split
208     [assumption
209     |apply max_O.assumption
210     ]
211   ]
212 qed.
213
214 theorem false_to_lt_max: \forall f,n,m.O < n \to
215 f n = false \to max m f \le n \to max m f < n.
216 intros.
217 elim (le_to_or_lt_eq ? ? H2)
218   [assumption
219   |elim (exists_max_forall_false f m)
220     [elim H4.
221      apply False_ind.
222      apply not_eq_true_false.
223      rewrite < H6.
224      rewrite > H3.
225      assumption
226     |elim H4.
227      rewrite > H6.
228      assumption
229     ]
230   ]
231 qed.
232
233 theorem lt_max_to_false : \forall f:nat \to bool. 
234 \forall n,m:nat. (max n f) < m \to m \leq n \to f m = false.
235 intros 2.
236 elim n.absurd (le m O).assumption.
237 cut (O < m).apply (lt_O_n_elim m Hcut).exact not_le_Sn_O.
238 rewrite < (max_O_f f).assumption.
239 elim (max_S_max f n1) in H1 ⊢ %.
240 elim H1.
241 absurd (m \le S n1).assumption.
242 apply lt_to_not_le.rewrite < H5.assumption.
243 elim H1.
244 apply (le_n_Sm_elim m n1 H2).
245 intro.
246 apply H.rewrite < H5.assumption.
247 apply le_S_S_to_le.assumption.
248 intro.rewrite > H6.assumption.
249 qed.
250
251 theorem f_false_to_le_max: \forall f,n,p. (∃i:nat.i≤n∧f i=true) \to
252 (\forall m. p < m \to f m = false)
253 \to max n f \le p.
254 intros.
255 apply not_lt_to_le.intro.
256 apply not_eq_true_false.
257 rewrite < (H1 ? H2).
258 apply sym_eq.
259 apply f_max_true.
260 assumption.
261 qed.
262
263 definition max_spec \def \lambda f:nat \to bool.\lambda n,m: nat.
264 m \le n \land (f m)=true \land (\forall i. m < i \to i \le n \to (f i = false)).
265
266 theorem max_spec_to_max: \forall f:nat \to bool.\forall n,m:nat.
267 max_spec f n m \to max n f = m.
268 intros 2.
269 elim n
270   [elim H.elim H1.apply (le_n_O_elim ? H3).
271    apply max_O_f
272   |elim H1.
273    elim (max_S_max f n1)
274     [elim H4.
275      rewrite > H6.
276      apply le_to_le_to_eq
277       [apply not_lt_to_le.
278        unfold Not.intro.
279        apply not_eq_true_false.
280        rewrite < H5.
281        apply H3
282         [assumption|apply le_n]
283       |elim H2.assumption
284       ]
285     |elim H4.
286      rewrite > H6.
287      apply H.
288      elim H2.
289      split
290       [split
291         [elim (le_to_or_lt_eq ? ? H7)
292           [apply le_S_S_to_le.assumption
293           |apply False_ind.
294            apply not_eq_true_false.
295            rewrite < H8.
296            rewrite > H9.
297            assumption
298           ]
299         |assumption
300         ]
301       |intros.
302        apply H3
303         [assumption|apply le_S.assumption]
304       ]
305     ]
306   ]
307 qed.
308  
309 let rec min_aux off n f \def
310   match f n with 
311   [ true \Rightarrow n
312   | false \Rightarrow 
313       match off with
314       [ O \Rightarrow n
315       | (S p) \Rightarrow min_aux p (S n) f]].
316
317 definition min : nat \to (nat \to bool) \to nat \def
318 \lambda n.\lambda f. min_aux n O f.
319
320 theorem min_aux_O_f: \forall f:nat \to bool. \forall i :nat.
321 min_aux O i f = i.
322 intros.simplify.
323 elim (f i).reflexivity.
324 simplify.reflexivity.
325 qed.
326
327 theorem min_O_f : \forall f:nat \to bool.
328 min O f = O.
329 intro.apply (min_aux_O_f f O).
330 qed.
331
332 theorem min_aux_S : \forall f: nat \to bool. \forall i,n:nat.
333 ((f n) = true \land min_aux (S i) n f = n) \lor 
334 ((f n) = false \land min_aux (S i) n f = min_aux i (S n) f).
335 intros.simplify.elim (f n).
336 simplify.left.split.reflexivity.reflexivity.
337 simplify.right.split.reflexivity.reflexivity.
338 qed.
339
340 theorem f_min_aux_true: \forall f:nat \to bool. \forall off,m:nat.
341 (\exists i. le m i \land le i (off + m) \land f i = true) \to
342 f (min_aux off m f) = true. 
343 intros 2.
344 elim off.elim H.elim H1.elim H2.
345 cut (a = m).
346 rewrite > (min_aux_O_f f).rewrite < Hcut.assumption.
347 apply (antisym_le a m).assumption.assumption.
348 simplify.
349 apply (bool_ind (\lambda b:bool.
350 (f m = b) \to (f (match b in bool with
351 [ true \Rightarrow m
352 | false  \Rightarrow (min_aux n (S m) f)])) = true)).
353 intro; assumption.
354 intro. apply H.
355 elim H1.elim H3.elim H4.
356 elim (le_to_or_lt_eq ? a H6). 
357 apply (ex_intro nat ? a).
358 split.split.
359 assumption.
360 rewrite < plus_n_Sm; assumption.
361 assumption.
362 absurd (f a = false).rewrite < H8.assumption.
363 rewrite > H5.
364 apply not_eq_true_false.
365 reflexivity.
366 qed.
367
368 theorem f_min_true: \forall f:nat \to bool. \forall m:nat.
369 (\exists i. le i m \land f i = true) \to
370 f (min m f) = true.
371 intros.unfold min.
372 apply f_min_aux_true.
373 elim H.clear H.elim H1.clear H1.
374 apply (ex_intro ? ? a).
375 split
376   [split
377     [apply le_O_n
378     |rewrite < plus_n_O.assumption
379     ]
380   |assumption
381   ]
382 qed.
383
384 theorem lt_min_aux_to_false : \forall f:nat \to bool. 
385 \forall n,off,m:nat. n \leq m \to m < (min_aux off n f) \to f m = false.
386 intros 3.
387 generalize in match n; clear n;
388 elim off.absurd (le n1 m).assumption.
389 apply lt_to_not_le.rewrite < (min_aux_O_f f n1).assumption.
390 elim (le_to_or_lt_eq ? ? H1);
391  [ unfold lt in H3;
392    apply (H (S n1));
393    [ assumption
394    | elim (min_aux_S f n n1);
395      [ elim H4;
396        elim (not_le_Sn_n n1);
397        rewrite > H6 in H2;
398        apply (lt_to_le (S n1) n1 ?).
399        apply (le_to_lt_to_lt (S n1) m n1 ? ?);
400         [apply (H3).
401         |apply (H2).
402         ]
403      | elim H4;
404        rewrite < H6;
405        assumption
406      ]
407    ]
408  | rewrite < H3 in H2 ⊢ %.
409    elim (min_aux_S f n n1);
410     [ elim H4;
411       rewrite > H6 in H2;
412       unfold lt in H2;
413       elim (not_le_Sn_n ? H2)
414     | elim H4;
415       assumption
416     ]
417  ]
418 qed.
419
420
421 lemma le_min_aux : \forall f:nat \to bool. 
422 \forall n,off:nat. n \leq (min_aux off n f).
423 intros 3.
424 elim off in n ⊢ %.
425 rewrite > (min_aux_O_f f n1).apply le_n.
426 elim (min_aux_S f n n1).
427 elim H1.rewrite > H3.apply le_n.
428 elim H1.rewrite > H3.
429 apply (transitive_le ? (S n1));
430  [ apply le_n_Sn
431  | apply (H (S n1))
432  ]
433 qed.
434
435 theorem le_min_aux_r : \forall f:nat \to bool. 
436 \forall n,off:nat. (min_aux off n f) \le n+off.
437 intros.
438 elim off in n ⊢ %.simplify.
439 elim (f n1).simplify.rewrite < plus_n_O.apply le_n.
440 simplify.rewrite < plus_n_O.apply le_n.
441 simplify.elim (f n1).
442 simplify.
443 apply (le_plus_n_r (S n) n1).
444 simplify.rewrite < plus_n_Sm.
445 apply (H (S n1)).
446 qed.