From: Ferruccio Guidi Date: Tue, 26 Jun 2007 17:58:16 +0000 (+0000) Subject: some old auto yurned into autobatch X-Git-Tag: make_still_working~6238 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ee31ecd9be54fb4a3d815f11d77e88c3c49ff363;p=helm.git some old auto yurned into autobatch --- diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma index b39e419ad..35540f87a 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma +++ b/helm/software/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/helm/software/matita/contribs/RELATIONAL/NLE/inv.ma b/helm/software/matita/contribs/RELATIONAL/NLE/inv.ma index 0007f3bc1..9d46d6cac 100644 --- a/helm/software/matita/contribs/RELATIONAL/NLE/inv.ma +++ b/helm/software/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/helm/software/matita/contribs/RELATIONAL/NLE/order.ma b/helm/software/matita/contribs/RELATIONAL/NLE/order.ma index 7ff57caa3..c50e7befd 100644 --- a/helm/software/matita/contribs/RELATIONAL/NLE/order.ma +++ b/helm/software/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/helm/software/matita/contribs/RELATIONAL/NLE/props.ma b/helm/software/matita/contribs/RELATIONAL/NLE/props.ma index db1476309..3654b7d89 100644 --- a/helm/software/matita/contribs/RELATIONAL/NLE/props.ma +++ b/helm/software/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/helm/software/matita/contribs/RELATIONAL/NPlus/fun.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/fun.ma index 4b31c570f..66847cf93 100644 --- a/helm/software/matita/contribs/RELATIONAL/NPlus/fun.ma +++ b/helm/software/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/helm/software/matita/contribs/RELATIONAL/NPlus/inv.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/inv.ma index 5299d5790..ea196cd6d 100644 --- a/helm/software/matita/contribs/RELATIONAL/NPlus/inv.ma +++ b/helm/software/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/helm/software/matita/contribs/RELATIONAL/NPlus/monoid.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/monoid.ma index 368396a77..1ccd6417e 100644 --- a/helm/software/matita/contribs/RELATIONAL/NPlus/monoid.ma +++ b/helm/software/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/helm/software/matita/contribs/RELATIONAL/ZEq/setoid.ma b/helm/software/matita/contribs/RELATIONAL/ZEq/setoid.ma index 1b6279fd1..6721926b1 100644 --- a/helm/software/matita/contribs/RELATIONAL/ZEq/setoid.ma +++ b/helm/software/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