1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / Matita is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/library_autobatch/nat/minimization".
17 include "auto/nat/minus.ma".
25 | (S j) \Rightarrow max j f ]].
27 theorem max_O_f : \forall f: nat \to bool. max O f = O.
29 elim (f O); autobatch.
37 theorem max_S_max : \forall f: nat \to bool. \forall n:nat.
38 (f (S n) = true \land max (S n) f = (S n)) \lor
39 (f (S n) = false \land max (S n) f = max n f).
40 intros.simplify.elim (f (S n));autobatch.
50 theorem le_max_n : \forall f: nat \to bool. \forall n:nat.
57 elim (f (S n1));simplify;autobatch.
67 theorem le_to_le_max : \forall f: nat \to bool. \forall n,m:nat.
68 n\le m \to max n f \le max m f.
72 | apply (trans_le ? (max n1 f))
74 | cut ((f (S n1) = true \land max (S n1) f = (S n1)) \lor
75 (f (S n1) = false \land max (S n1) f = max n1 f))
76 [ elim Hcut;elim H3;rewrite > H5;autobatch
91 theorem f_m_to_le_max: \forall f: nat \to bool. \forall n,m:nat.
92 m\le n \to f m = true \to m \le max n f.
96 (*apply (le_n_O_elim m H).
98 | apply (le_n_Sm_elim m n1 H1);intro
99 [ apply (trans_le ? (max n1 f)); autobatch
105 | apply le_to_le_max.
119 definition max_spec \def \lambda f:nat \to bool.\lambda n: nat.
120 \exists i. (le i n) \land (f i = true) \to
121 (f n) = true \land (\forall i. i < n \to (f i = false)).
123 theorem f_max_true : \forall f:nat \to bool. \forall n:nat.
124 (\exists i:nat. le i n \land f i = true) \to f (max n f) = true.
129 generalize in match H3.
130 apply (le_n_O_elim a H2).
138 apply (bool_ind (\lambda b:bool.
139 (f (S n1) = b) \to (f (match b in bool with
140 [ true \Rightarrow (S n1)
141 | false \Rightarrow (max n1 f)])) = true))
152 generalize in match H5.
153 apply (le_n_Sm_elim a n1 H4)
155 apply (ex_intro nat ? a).
158 [ apply le_S_S_to_le.
163 (* una chiamata di autobatch in questo punto genera segmentation fault*)
165 (* una chiamata di autobatch in questo punto genera segmentation fault*)
166 apply not_eq_true_false.
167 (* una chiamata di autobatch in questo punto genera segmentation fault*)
169 (* una chiamata di autobatch in questo punto genera segmentation fault*)
171 (* una chiamata di autobatch in questo punto genera segmentation fault*)
180 theorem lt_max_to_false : \forall f:nat \to bool.
181 \forall n,m:nat. (max n f) < m \to m \leq n \to f m = false.
184 [ absurd (le m O);autobatch
187 [ apply (lt_O_n_elim m Hcut).
189 | rewrite < (max_O_f f).
193 | generalize in match H1.
194 elim (max_S_max f n1)
198 | apply lt_to_not_le.
203 apply (le_n_Sm_elim m n1 H2)
208 | apply le_S_S_to_le.
219 let rec min_aux off n f \def
221 [ true \Rightarrow (n-off)
225 | (S p) \Rightarrow min_aux p n f]].
227 definition min : nat \to (nat \to bool) \to nat \def
228 \lambda n.\lambda f. min_aux n n f.
230 theorem min_aux_O_f: \forall f:nat \to bool. \forall i :nat.
233 (*una chiamata di autobatch a questo punto porta ad un'elaborazione molto lunga (forse va
234 in loop): dopo circa 3 minuti non era ancora terminata.
237 (*una chiamata di autobatch a questo punto porta ad un'elaborazione molto lunga (forse va
238 in loop): dopo circa 3 minuti non era ancora terminata.
240 elim (f i); autobatch.
247 theorem min_O_f : \forall f:nat \to bool.
250 (* una chiamata di autobatch a questo punto NON conclude la dimostrazione*)
251 apply (min_aux_O_f f O).
254 theorem min_aux_S : \forall f: nat \to bool. \forall i,n:nat.
255 (f (n -(S i)) = true \land min_aux (S i) n f = (n - (S i))) \lor
256 (f (n -(S i)) = false \land min_aux (S i) n f = min_aux i n f).
257 intros.simplify.elim (f (n - (S i)));autobatch.
267 theorem f_min_aux_true: \forall f:nat \to bool. \forall off,m:nat.
268 (\exists i. le (m-off) i \land le i m \land f i = true) \to
269 f (min_aux off m f) = true.
277 (*rewrite > (min_aux_O_f f).
280 | apply (antisym_le a m)
282 | rewrite > (minus_n_O m).
287 apply (bool_ind (\lambda b:bool.
288 (f (m-(S n)) = b) \to (f (match b in bool with
289 [ true \Rightarrow m-(S n)
290 | false \Rightarrow (min_aux n m f)])) = true))
301 elim (le_to_or_lt_eq (m-(S n)) a H6)
302 [ apply (ex_intro nat ? a).
305 [ apply lt_minus_S_n_to_le_minus_n.
311 | absurd (f a = false)
312 [ (* una chiamata di autobatch in questo punto genera segmentation fault*)
316 apply not_eq_true_false
324 theorem lt_min_aux_to_false : \forall f:nat \to bool.
325 \forall n,off,m:nat. (n-off) \leq m \to m < (min_aux off n f) \to f m = false.
329 [ rewrite > minus_n_O.
331 | apply lt_to_not_le.
332 rewrite < (min_aux_O_f f n).
335 | generalize in match H1.
336 elim (min_aux_S f n1 n)
338 absurd (n - S n1 \le m)
340 | apply lt_to_not_le.
345 elim (le_to_or_lt_eq (n -(S n1)) m)
348 (*apply lt_minus_S_n_to_le_minus_n.
361 theorem le_min_aux : \forall f:nat \to bool.
362 \forall n,off:nat. (n-off) \leq (min_aux off n f).
365 [ rewrite < minus_n_O.
367 (*rewrite > (min_aux_O_f f n).
369 | elim (min_aux_S f n1 n)
377 (*apply (trans_le (n-(S n1)) (n-n1))
378 [ apply monotonic_le_minus_r.
386 theorem le_min_aux_r : \forall f:nat \to bool.
387 \forall n,off:nat. (min_aux off n f) \le n.
399 elim (f (n -(S n1)));simplify;autobatch
400 (*[ apply le_plus_to_minus.