(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/minimization".
+set "baseuri" "cic:/matita/library_autobatch/nat/minimization".
include "auto/nat/minus.ma".
theorem max_O_f : \forall f: nat \to bool. max O f = O.
intro. simplify.
-elim (f O); auto.
+elim (f O); autobatch.
(*[ simplify.
reflexivity
| simplify.
theorem max_S_max : \forall f: nat \to bool. \forall n:nat.
(f (S n) = true \land max (S n) f = (S n)) \lor
(f (S n) = false \land max (S n) f = max n f).
-intros.simplify.elim (f (S n));auto.
+intros.simplify.elim (f (S n));autobatch.
(*[ simplify.
left.
split;reflexivity
[ rewrite > max_O_f.
apply le_n
| simplify.
- elim (f (S n1));simplify;auto.
+ elim (f (S n1));simplify;autobatch.
(*[ simplify.
apply le_n
| simplify.
[ apply H2
| cut ((f (S n1) = true \land max (S n1) f = (S n1)) \lor
(f (S n1) = false \land max (S n1) f = max n1 f))
- [ elim Hcut;elim H3;rewrite > H5;auto
+ [ elim Hcut;elim H3;rewrite > H5;autobatch
(*[ elim H3.
rewrite > H5.
apply le_S.
m\le n \to f m = true \to m \le max n f.
intros 3.
elim n
-[ auto.
+[ autobatch.
(*apply (le_n_O_elim m H).
apply le_O_n.*)
| apply (le_n_Sm_elim m n1 H1);intro
- [ apply (trans_le ? (max n1 f)); auto
+ [ apply (trans_le ? (max n1 f)); autobatch
(*[ apply H
[apply le_S_S_to_le.
assumption
| simplify.
rewrite < H3.
rewrite > H2.
- auto
+ autobatch
(*simplify.
apply le_n.*)
]
elim H1.
generalize in match H3.
apply (le_n_O_elim a H2).
- auto
+ autobatch
(*intro.
simplify.
rewrite > H4.
[ true \Rightarrow (S n1)
| false \Rightarrow (max n1 f)])) = true))
- [ auto
+ [ autobatch
(*simplify.
intro.
assumption.*)
apply (le_n_Sm_elim a n1 H4)
[ intros.
apply (ex_intro nat ? a).
- auto
+ autobatch
(*split
[ apply le_S_S_to_le.
assumption.
| assumption.
]*)
| intros.
- (* una chiamata di auto in questo punto genera segmentation fault*)
+ (* una chiamata di autobatch in questo punto genera segmentation fault*)
apply False_ind.
- (* una chiamata di auto in questo punto genera segmentation fault*)
+ (* una chiamata di autobatch in questo punto genera segmentation fault*)
apply not_eq_true_false.
- (* una chiamata di auto in questo punto genera segmentation fault*)
+ (* una chiamata di autobatch in questo punto genera segmentation fault*)
rewrite < H2.
- (* una chiamata di auto in questo punto genera segmentation fault*)
+ (* una chiamata di autobatch in questo punto genera segmentation fault*)
rewrite < H7.
- (* una chiamata di auto in questo punto genera segmentation fault*)
+ (* una chiamata di autobatch in questo punto genera segmentation fault*)
rewrite > H6.
reflexivity.
]
\forall n,m:nat. (max n f) < m \to m \leq n \to f m = false.
intros 2.
elim n
-[ absurd (le m O);auto
+[ absurd (le m O);autobatch
(*[ assumption
| cut (O < m)
[ apply (lt_O_n_elim m Hcut).
| elim H3.
apply (le_n_Sm_elim m n1 H2)
[ intro.
- apply H;auto
+ apply H;autobatch
(*[ rewrite < H6.
assumption
| apply le_S_S_to_le.
assumption
]*)
| intro.
- auto
+ autobatch
(*rewrite > H7.
assumption*)
]
theorem min_aux_O_f: \forall f:nat \to bool. \forall i :nat.
min_aux O i f = i.
intros.simplify.
-(*una chiamata di auto a questo punto porta ad un'elaborazione molto lunga (forse va
+(*una chiamata di autobatch a questo punto porta ad un'elaborazione molto lunga (forse va
in loop): dopo circa 3 minuti non era ancora terminata.
*)
rewrite < minus_n_O.
-(*una chiamata di auto a questo punto porta ad un'elaborazione molto lunga (forse va
+(*una chiamata di autobatch a questo punto porta ad un'elaborazione molto lunga (forse va
in loop): dopo circa 3 minuti non era ancora terminata.
*)
-elim (f i); auto.
+elim (f i); autobatch.
(*[ reflexivity.
simplify
| reflexivity
theorem min_O_f : \forall f:nat \to bool.
min O f = O.
intro.
-(* una chiamata di auto a questo punto NON conclude la dimostrazione*)
+(* una chiamata di autobatch a questo punto NON conclude la dimostrazione*)
apply (min_aux_O_f f O).
qed.
theorem min_aux_S : \forall f: nat \to bool. \forall i,n:nat.
(f (n -(S i)) = true \land min_aux (S i) n f = (n - (S i))) \lor
(f (n -(S i)) = false \land min_aux (S i) n f = min_aux i n f).
-intros.simplify.elim (f (n - (S i)));auto.
+intros.simplify.elim (f (n - (S i)));autobatch.
(*[ simplify.
left.
split;reflexivity.
elim H1.
elim H2.
cut (a = m)
- [ auto.
+ [ autobatch.
(*rewrite > (min_aux_O_f f).
rewrite < Hcut.
assumption*)
(f (m-(S n)) = b) \to (f (match b in bool with
[ true \Rightarrow m-(S n)
| false \Rightarrow (min_aux n m f)])) = true))
- [ auto
+ [ autobatch
(*simplify.
intro.
assumption.*)
elim H4.
elim (le_to_or_lt_eq (m-(S n)) a H6)
[ apply (ex_intro nat ? a).
- split;auto
- (*[ auto.split
+ split;autobatch
+ (*[ autobatch.split
[ apply lt_minus_S_n_to_le_minus_n.
assumption
| assumption
| assumption
]*)
| absurd (f a = false)
- [ (* una chiamata di auto in questo punto genera segmentation fault*)
+ [ (* una chiamata di autobatch in questo punto genera segmentation fault*)
rewrite < H8.
assumption.
| rewrite > H5.
| elim H3.
elim (le_to_or_lt_eq (n -(S n1)) m)
[ apply H
- [ auto
+ [ autobatch
(*apply lt_minus_S_n_to_le_minus_n.
assumption*)
| rewrite < H6.
intros 3.
elim off
[ rewrite < minus_n_O.
- auto
+ autobatch
(*rewrite > (min_aux_O_f f n).
apply le_n.*)
| elim (min_aux_S f n1 n)
[ elim H1.
- auto
+ autobatch
(*rewrite > H3.
apply le_n.*)
| elim H1.
rewrite > H3.
- auto
+ autobatch
(*apply (trans_le (n-(S n1)) (n-n1))
[ apply monotonic_le_minus_r.
apply le_n_Sn.
elim off
[ simplify.
rewrite < minus_n_O.
- elim (f n);auto
+ elim (f n);autobatch
(*[simplify.
apply le_n.
| simplify.
apply le_n.
]*)
| simplify.
- elim (f (n -(S n1)));simplify;auto
+ elim (f (n -(S n1)));simplify;autobatch
(*[ apply le_plus_to_minus.
rewrite < sym_plus.
apply le_plus_n