]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/minimization.ma
Dummy dependent products in inductive types arities are no longer cleaned.
[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 generalize in match H1.
240 elim (max_S_max f n1).
241 elim H3.
242 absurd (m \le S n1).assumption.
243 apply lt_to_not_le.rewrite < H6.assumption.
244 elim H3.
245 apply (le_n_Sm_elim m n1 H2).
246 intro.
247 apply H.rewrite < H6.assumption.
248 apply le_S_S_to_le.assumption.
249 intro.rewrite > H7.assumption.
250 qed.
251
252 theorem f_false_to_le_max: \forall f,n,p. (∃i:nat.i≤n∧f i=true) \to
253 (\forall m. p < m \to f m = false)
254 \to max n f \le p.
255 intros.
256 apply not_lt_to_le.intro.
257 apply not_eq_true_false.
258 rewrite < (H1 ? H2).
259 apply sym_eq.
260 apply f_max_true.
261 assumption.
262 qed.
263
264 definition max_spec \def \lambda f:nat \to bool.\lambda n,m: nat.
265 m \le n \land (f m)=true \land (\forall i. m < i \to i \le n \to (f i = false)).
266
267 theorem max_spec_to_max: \forall f:nat \to bool.\forall n,m:nat.
268 max_spec f n m \to max n f = m.
269 intros 2.
270 elim n
271   [elim H.elim H1.apply (le_n_O_elim ? H3).
272    apply max_O_f
273   |elim H1.
274    elim (max_S_max f n1)
275     [elim H4.
276      rewrite > H6.
277      apply le_to_le_to_eq
278       [apply not_lt_to_le.
279        unfold Not.intro.
280        apply not_eq_true_false.
281        rewrite < H5.
282        apply H3
283         [assumption|apply le_n]
284       |elim H2.assumption
285       ]
286     |elim H4.
287      rewrite > H6.
288      apply H.
289      elim H2.
290      split
291       [split
292         [elim (le_to_or_lt_eq ? ? H7)
293           [apply le_S_S_to_le.assumption
294           |apply False_ind.
295            apply not_eq_true_false.
296            rewrite < H8.
297            rewrite > H9.
298            assumption
299           ]
300         |assumption
301         ]
302       |intros.
303        apply H3
304         [assumption|apply le_S.assumption]
305       ]
306     ]
307   ]
308 qed.
309  
310 let rec min_aux off n f \def
311   match f n with 
312   [ true \Rightarrow n
313   | false \Rightarrow 
314       match off with
315       [ O \Rightarrow n
316       | (S p) \Rightarrow min_aux p (S n) f]].
317
318 definition min : nat \to (nat \to bool) \to nat \def
319 \lambda n.\lambda f. min_aux n O f.
320
321 theorem min_aux_O_f: \forall f:nat \to bool. \forall i :nat.
322 min_aux O i f = i.
323 intros.simplify.
324 elim (f i).reflexivity.
325 simplify.reflexivity.
326 qed.
327
328 theorem min_O_f : \forall f:nat \to bool.
329 min O f = O.
330 intro.apply (min_aux_O_f f O).
331 qed.
332
333 theorem min_aux_S : \forall f: nat \to bool. \forall i,n:nat.
334 ((f n) = true \land min_aux (S i) n f = n) \lor 
335 ((f n) = false \land min_aux (S i) n f = min_aux i (S n) f).
336 intros.simplify.elim (f n).
337 simplify.left.split.reflexivity.reflexivity.
338 simplify.right.split.reflexivity.reflexivity.
339 qed.
340
341 theorem f_min_aux_true: \forall f:nat \to bool. \forall off,m:nat.
342 (\exists i. le m i \land le i (off + m) \land f i = true) \to
343 f (min_aux off m f) = true. 
344 intros 2.
345 elim off.elim H.elim H1.elim H2.
346 cut (a = m).
347 rewrite > (min_aux_O_f f).rewrite < Hcut.assumption.
348 apply (antisym_le a m).assumption.assumption.
349 simplify.
350 apply (bool_ind (\lambda b:bool.
351 (f m = b) \to (f (match b in bool with
352 [ true \Rightarrow m
353 | false  \Rightarrow (min_aux n (S m) f)])) = true)).
354 intro; assumption.
355 intro. apply H.
356 elim H1.elim H3.elim H4.
357 elim (le_to_or_lt_eq ? a H6). 
358 apply (ex_intro nat ? a).
359 split.split.
360 assumption.
361 rewrite < plus_n_Sm; assumption.
362 assumption.
363 absurd (f a = false).rewrite < H8.assumption.
364 rewrite > H5.
365 apply not_eq_true_false.
366 reflexivity.
367 qed.
368
369 theorem lt_min_aux_to_false : \forall f:nat \to bool. 
370 \forall n,off,m:nat. n \leq m \to m < (min_aux off n f) \to f m = false.
371 intros 3.
372 generalize in match n; clear n.
373 elim off.absurd (le n1 m).assumption.
374 apply lt_to_not_le.rewrite < (min_aux_O_f f n1).assumption.
375 elim (le_to_or_lt_eq ? ? H1);
376  [ unfold lt in H3;
377    apply (H (S n1));
378    [ assumption
379    | elim (min_aux_S f n n1);
380      [ elim H4;
381        elim (not_le_Sn_n n1);
382        rewrite > H6 in H2;
383        apply (lt_to_le (S n1) n1 ?).
384        apply (le_to_lt_to_lt (S n1) m n1 ? ?);
385         [apply (H3).
386         |apply (H2).
387         ]
388      | elim H4;
389        rewrite < H6;
390        assumption
391      ]
392    ]
393  | rewrite < H3 in H2 ⊢ %.
394    elim (min_aux_S f n n1);
395     [ elim H4;
396       rewrite > H6 in H2;
397       unfold lt in H2;
398       elim (not_le_Sn_n ? H2)
399     | elim H4;
400       assumption
401     ]
402  ]
403 qed.
404
405
406 lemma le_min_aux : \forall f:nat \to bool. 
407 \forall n,off:nat. n \leq (min_aux off n f).
408 intros 3.
409 generalize in match n. clear n.
410 elim off.
411 rewrite > (min_aux_O_f f n1).apply le_n.
412 elim (min_aux_S f n n1).
413 elim H1.rewrite > H3.apply le_n.
414 elim H1.rewrite > H3.
415 apply (transitive_le ? (S n1));
416  [ apply le_n_Sn
417  | apply (H (S n1))
418  ]
419 qed.
420
421 theorem le_min_aux_r : \forall f:nat \to bool. 
422 \forall n,off:nat. (min_aux off n f) \le n+off.
423 intros.
424 generalize in match n. clear n.
425 elim off.simplify.
426 elim (f n1).simplify.rewrite < plus_n_O.apply le_n.
427 simplify.rewrite < plus_n_O.apply le_n.
428 simplify.elim (f n1).
429 simplify.
430 apply (le_plus_n_r (S n) n1).
431 simplify.rewrite < plus_n_Sm.
432 apply (H (S n1)).
433 qed.