some old auto yurned into autobatch

diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma
index b39e419ad6dc0d5fa2fd8553e54f556faeb9d58d..35540f87ae8cd59d698c3f93d7737e8a8afffd8f 100644 (file)
--- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma
+++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma
@@ -30,7 +30,7 @@ theorem lift_inv_lref_1: \forall l, i, j1, x.
                          (i <= j1 \land 
                           \exists j2. (l + j1 == j2) \land x = lref j2
                          ).
- intros. inversion H; clear H; intros; subst; auto depth = 5.
+ intros. inversion H; clear H; intros; subst; autobatch depth = 5.
 qed.
 
 theorem lift_inv_bind_1: \forall l, i, r, u1, t1, x.
@@ -39,7 +39,7 @@ theorem lift_inv_bind_1: \forall l, i, r, u1, t1, x.
                          Lift l i u1 u2 \land
                          Lift l (succ i) t1 t2 \land
                          x = intb r u2 t2.
- intros. inversion H; clear H; intros; subst. auto depth = 5.
+ intros. inversion H; clear H; intros; subst. autobatch depth = 5.
 qed.
 
 theorem lift_inv_flat_1: \forall l, i, r, u1, t1, x.
@@ -48,7 +48,7 @@ theorem lift_inv_flat_1: \forall l, i, r, u1, t1, x.
                          Lift l i u1 u2 \land
                          Lift l i t1 t2 \land
                          x = intf r u2 t2.
- intros. inversion H; clear H; intros; subst. auto depth = 5.
+ intros. inversion H; clear H; intros; subst. autobatch depth = 5.
 qed.
 
 theorem lift_inv_sort_2: \forall l, i, x, h.
@@ -63,7 +63,7 @@ theorem lift_inv_lref_2: \forall l, i, x, j2.
                          (i <= j2 \land 
                           \exists j1. (l + j1 == j2) \land x = lref j1
                          ).
- intros. inversion H; clear H; intros; subst; auto depth = 5.
+ intros. inversion H; clear H; intros; subst; autobatch depth = 5.
 qed.
 
 theorem lift_inv_bind_2: \forall l, i, r, x, u2, t2.
@@ -72,7 +72,7 @@ theorem lift_inv_bind_2: \forall l, i, r, x, u2, t2.
                          Lift l i u1 u2 \land
                          Lift l (succ i) t1 t2 \land
                          x = intb r u1 t1.
- intros. inversion H; clear H; intros; subst. auto depth = 5.
+ intros. inversion H; clear H; intros; subst. autobatch depth = 5.
 qed.
 
 theorem lift_inv_flat_2: \forall l, i, r, x, u2, t2.
@@ -81,7 +81,7 @@ theorem lift_inv_flat_2: \forall l, i, r, x, u2, t2.
                          Lift l i u1 u2 \land
                          Lift l i t1 t2 \land
                          x = intf r u1 t1.
- intros. inversion H; clear H; intros; subst. auto depth = 5.
+ intros. inversion H; clear H; intros; subst. autobatch depth = 5.
 qed.
 
 (* Corollaries of inversion properties ***************************************)
@@ -91,7 +91,7 @@ theorem lift_inv_lref_1_gt: \forall l, i, j1, x.
                             i > j1 \to x = lref j1.
  intros.
  lapply linear lift_inv_lref_1 to H. decompose; subst;
- [ auto
+ [ autobatch
  | lapply linear nle_false to H2, H1. decompose
  ].
 qed.
@@ -102,7 +102,7 @@ theorem lift_inv_lref_1_le: \forall l, i, j1, x.
  intros.
  lapply linear lift_inv_lref_1 to H. decompose; subst;
  [ lapply linear nle_false to H1, H2. decompose
- | auto
+ | autobatch
  ].
 qed.
 
@@ -113,7 +113,7 @@ theorem lift_inv_lref_1_le_nplus: \forall l, i, j1, x.
  intros.
  lapply linear lift_inv_lref_1 to H. decompose; subst;
  [ lapply linear nle_false to H1, H3. decompose
- | lapply linear nplus_mono to H2, H4. subst. auto
+ | lapply linear nplus_mono to H2, H4. subst. autobatch
  ].
 qed.
 
@@ -122,7 +122,7 @@ theorem lift_inv_lref_2_gt: \forall l, i, x, j2.
                             i > j2 \to x = lref j2.
  intros.
  lapply linear lift_inv_lref_2 to H. decompose; subst;
- [ auto
+ [ autobatch
  | lapply linear nle_false to H2, H1. decompose
  ].
  qed.
@@ -133,7 +133,7 @@ theorem lift_inv_lref_2_le: \forall l, i, x, j2.
  intros.
  lapply linear lift_inv_lref_2 to H. decompose; subst;
  [ lapply linear nle_false to H1, H2. decompose
- | auto
+ | autobatch
  ].
 qed.
 
@@ -144,6 +144,6 @@ theorem lift_inv_lref_2_le_nplus: \forall l, i, x, j2.
  intros.
  lapply linear lift_inv_lref_2 to H. decompose; subst;
  [ lapply linear nle_false to H1, H3. decompose
- | lapply linear nplus_inj_2 to H2, H4. subst. auto
+ | lapply linear nplus_inj_2 to H2, H4. subst. autobatch
  ].
 qed.

diff --git a/matita/contribs/RELATIONAL/NLE/inv.ma b/matita/contribs/RELATIONAL/NLE/inv.ma
index 0007f3bc1f76989346485889092f6831c3631434..9d46d6cac8db613465d0eaef1006d635c62d36ef 100644 (file)
--- a/matita/contribs/RELATIONAL/NLE/inv.ma
+++ b/matita/contribs/RELATIONAL/NLE/inv.ma
@@ -35,5 +35,6 @@ qed.
 
 theorem nle_inv_succ_2: \forall y,x. x <= succ y \to
                         x = zero \lor \exists z. x = succ z \land z <= y.
- intros. inversion H; clear H; intros; subst; auto depth = 4.
+ intros. inversion H; clear H; intros; subst;
+ autobatch depth = 4.
 qed.

diff --git a/matita/contribs/RELATIONAL/NLE/order.ma b/matita/contribs/RELATIONAL/NLE/order.ma
index 7ff57caa3e5fec2dd9b8a5ef099a6d70063f0c09..c50e7befd15b761cb0ee55035fecb7f95a2daf38 100644 (file)
--- a/matita/contribs/RELATIONAL/NLE/order.ma
+++ b/matita/contribs/RELATIONAL/NLE/order.ma
@@ -17,37 +17,37 @@ set "baseuri" "cic:/matita/RELATIONAL/NLE/order".
 include "NLE/inv.ma".
 
 theorem nle_refl: \forall x. x <= x.
- intros; elim x; clear x; auto.
+ intros; elim x; clear x; autobatch.
 qed.
 
 theorem nle_trans: \forall x,y. x <= y \to
                    \forall z. y <= z \to x <= z.
  intros 3. elim H; clear H x y;
- [ auto
+ [ autobatch
  | lapply linear nle_inv_succ_1 to H3. decompose. subst. 
-   auto
+   autobatch
  ].
 qed.
 
 theorem nle_false: \forall x,y. x <= y \to y < x \to False.
- intros 3; elim H; clear H x y; auto.
+ intros 3; elim H; clear H x y; autobatch.
 qed.
 
 theorem nle_irrefl: \forall x. x < x \to False.
- intros. auto.
+ intros. autobatch.
 qed.
 
 theorem nle_irrefl_ei: \forall x, z. z <= x \to z = succ x \to False.
- intros 3. elim H; clear H x z; subst. auto.
+ intros 3. elim H; clear H x z; subst. autobatch.
 qed.
 
 theorem nle_irrefl_smart: \forall x. x < x \to False.
- intros 1. elim x; clear x; auto.
+ intros 1. elim x; clear x; autobatch.
 qed.
 
 theorem nle_lt_or_eq: \forall y, x. x <= y \to x < y \lor x = y.
  intros. elim H; clear H x y;
  [ elim n; clear n
  | decompose
- ]; auto.
+ ]; autobatch.
 qed.

diff --git a/matita/contribs/RELATIONAL/NLE/props.ma b/matita/contribs/RELATIONAL/NLE/props.ma
index db1476309eeca1e40e17833d0705519e1e49c6b8..3654b7d898bcb0c29f0136f50cd8f40245225db2 100644 (file)
--- a/matita/contribs/RELATIONAL/NLE/props.ma
+++ b/matita/contribs/RELATIONAL/NLE/props.ma
@@ -17,15 +17,15 @@ set "baseuri" "cic:/matita/RELATIONAL/NLE/props".
 include "NLE/order.ma".
 
 theorem nle_trans_succ: \forall x,y. x <= y \to x <= succ y.
- intros. elim H; clear H x y; auto.
+ intros. elim H; clear H x y; autobatch.
 qed.
 
 theorem nle_gt_or_le: \forall x, y. y > x \lor y <= x.
  intros 2; elim y; clear y;
- [ auto
+ [ autobatch
  | decompose;
    [ lapply linear nle_inv_succ_1 to H1
    | lapply linear nle_lt_or_eq to H1
-   ]; decompose; subst; auto depth = 4
+   ]; decompose; subst; autobatch depth = 4
  ].
 qed.

diff --git a/matita/contribs/RELATIONAL/NPlus/fun.ma b/matita/contribs/RELATIONAL/NPlus/fun.ma
index 4b31c570f2355007ea5c4f78a83ae66eee1b63b8..66847cf934fcc7c603c709bd074a2a481bf8068d 100644 (file)
--- a/matita/contribs/RELATIONAL/NPlus/fun.ma
+++ b/matita/contribs/RELATIONAL/NPlus/fun.ma
@@ -20,7 +20,7 @@ include "NPlus/inv.ma".
 
 theorem nplus_total: \forall p,q. \exists r. p + q == r.
  intros 2. elim q; clear q;
- [ auto | decompose. auto ].
+ [ autobatch | decompose. autobatch ].
 qed.
 
 theorem nplus_mono: \forall p,q,r1. (p + q == r1) \to 
@@ -28,7 +28,7 @@ theorem nplus_mono: \forall p,q,r1. (p + q == r1) \to
  intros 4. elim H; clear H q r1;
  [ lapply linear nplus_inv_zero_2 to H1
  | lapply linear nplus_inv_succ_2 to H3. decompose
- ]; subst; auto.
+ ]; subst; autobatch.
 qed.
 
 theorem nplus_inj_1: \forall p1, q, r. (p1 + q == r) \to
@@ -36,5 +36,5 @@ theorem nplus_inj_1: \forall p1, q, r. (p1 + q == r) \to
  intros 4. elim H; clear H q r;
  [ lapply linear nplus_inv_zero_2 to H1
  | lapply linear nplus_inv_succ_2_3 to H3
- ]; auto.
+ ]; autobatch.
 qed.

diff --git a/matita/contribs/RELATIONAL/NPlus/inv.ma b/matita/contribs/RELATIONAL/NPlus/inv.ma
index 5299d5790debc2eacbbd83b5aea99cdc09e69e4f..ea196cd6d9fbb2a9bcf288b4a8af17eb6b9f339e 100644 (file)
--- a/matita/contribs/RELATIONAL/NPlus/inv.ma
+++ b/matita/contribs/RELATIONAL/NPlus/inv.ma
@@ -25,8 +25,8 @@ qed.
 theorem nplus_inv_succ_1: \forall p,q,r. ((succ p) + q == r) \to 
                           \exists s. r = (succ s) \land p + q == s.
  intros. elim H; clear H q r; intros;
- [ auto depth = 4
- | clear H1. decompose. subst. auto depth = 4
+ [ autobatch depth = 4
+ | clear H1. decompose. subst. autobatch depth = 4
  ]
 qed.
 
@@ -36,7 +36,8 @@ qed.
 
 theorem nplus_inv_succ_2: \forall p,q,r. (p + (succ q) == r) \to 
                           \exists s. r = (succ s) \land p + q == s.
- intros. inversion H; clear H; intros; subst. auto depth = 4.
+ intros. inversion H; clear H; intros; subst.
+ autobatch depth = 4.
 qed.
 
 theorem nplus_inv_zero_3: \forall p,q. (p + q == zero) \to 
@@ -47,7 +48,8 @@ qed.
 theorem nplus_inv_succ_3: \forall p,q,r. (p + q == (succ r)) \to
                           \exists s. p = succ s \land (s + q == r) \lor
                                      q = succ s \land p + s == r.
- intros. inversion H; clear H; intros; subst; auto depth = 4.
+ intros. inversion H; clear H; intros; subst;
+ autobatch depth = 4.
 qed.
 
 (* Corollaries to inversion lemmas ******************************************)

diff --git a/matita/contribs/RELATIONAL/NPlus/monoid.ma b/matita/contribs/RELATIONAL/NPlus/monoid.ma
index 368396a778e5afa5cf55634560b56ffdc80a7266..1ccd6417e4d117eb47e14be0c02b2e292638be2a 100644 (file)
--- a/matita/contribs/RELATIONAL/NPlus/monoid.ma
+++ b/matita/contribs/RELATIONAL/NPlus/monoid.ma
@@ -19,12 +19,12 @@ include "NPlus/fun.ma".
 (* Monoidal properties ******************************************************)
 
 theorem nplus_zero_1: \forall q. zero + q == q.
- intros. elim q; clear q; auto.
+ intros. elim q; clear q; autobatch.
 qed.
 
 theorem nplus_succ_1: \forall p,q,r. (p + q == r) \to 
                       (succ p) + q == (succ r).
- intros. elim H; clear H q r; auto.
+ intros. elim H; clear H q r; autobatch.
 qed.
 
 theorem nplus_comm: \forall p, q, x. (p + q == x) \to
@@ -32,11 +32,11 @@ theorem nplus_comm: \forall p, q, x. (p + q == x) \to
  intros 4; elim H; clear H q x;
  [ lapply linear nplus_inv_zero_1 to H1
  | lapply linear nplus_inv_succ_1 to H3. decompose
- ]; subst; auto.
+ ]; subst; autobatch.
 qed.
 
 theorem nplus_comm_rew: \forall p,q,r. (p + q == r) \to q + p == r.
- intros. elim H; clear H q r; auto.
+ intros. elim H; clear H q r; autobatch.
 qed.
 
 theorem nplus_ass: \forall p1, p2, r1. (p1 + p2 == r1) \to
@@ -45,10 +45,10 @@ theorem nplus_ass: \forall p1, p2, r1. (p1 + p2 == r1) \to
                    \forall s3. (p1 + r3 == s3) \to s1 = s3.
  intros 4. elim H; clear H p2 r1;
  [ lapply linear nplus_inv_zero_1 to H2. subst.
-   lapply nplus_mono to H1, H3. subst. auto
+   lapply nplus_mono to H1, H3. subst. autobatch
  | lapply linear nplus_inv_succ_1 to H3. decompose. subst.
    lapply linear nplus_inv_succ_1 to H4. decompose. subst.
-   lapply linear nplus_inv_succ_2 to H5. decompose. subst. auto
+   lapply linear nplus_inv_succ_2 to H5. decompose. subst. autobatch
  ].
 qed.
  
@@ -56,7 +56,7 @@ qed.
 
 theorem nplus_inj_2: \forall p, q1, r. (p + q1 == r) \to
                      \forall q2. (p + q2 == r) \to q1 = q2.
- intros. auto.
+ intros. autobatch.
 qed.
 
 (* Corollaries of nonoidal properties ***************************************)
@@ -71,7 +71,7 @@ theorem nplus_comm_1: \forall p1, q, r1. (p1 + q == r1) \to
  | lapply linear nplus_inv_succ_2 to H3.
    lapply linear nplus_inv_succ_2 to H4. decompose. subst.
    lapply linear nplus_inv_succ_2 to H5. decompose
- ]; subst; auto.
+ ]; subst; autobatch.
 qed.
 
 theorem nplus_comm_1_rew: \forall p1,q,r1. (p1 + q == r1) \to
@@ -81,7 +81,7 @@ theorem nplus_comm_1_rew: \forall p1,q,r1. (p1 + q == r1) \to
  [ lapply linear nplus_inv_zero_2 to H1. subst
  | lapply linear nplus_inv_succ_2 to H3. decompose. subst.
    lapply linear nplus_inv_succ_2 to H4. decompose. subst
- ]; auto.
+ ]; autobatch.
 qed.
 
 (*                      

diff --git a/matita/contribs/RELATIONAL/ZEq/setoid.ma b/matita/contribs/RELATIONAL/ZEq/setoid.ma
index 1b6279fd1c57064bafd1c5b953da58325cb1996d..6721926b10281e551c51710c43ed67d5c66f490e 100644 (file)
--- a/matita/contribs/RELATIONAL/ZEq/setoid.ma
+++ b/matita/contribs/RELATIONAL/ZEq/setoid.ma
@@ -20,11 +20,11 @@ include "ZEq/defs.ma".
 theorem zeq_refl: \forall z. z = z.
  intros. elim z. clear z.
  lapply (nplus_total t t1). decompose.
- auto.
+ autobatch.
 qed.
 
 theorem zeq_sym: \forall z1,z2. z1 = z2 \to z2 = z1.
- intros. elim H. clear H z1 z2. auto.
+ intros. elim H. clear H z1 z2. autobatch.
 qed.
 (*
 theorem zeq_trans: \forall z1,z2. z1 = z2 \to