From: Ferruccio Guidi Date: Sat, 10 Nov 2007 16:54:55 +0000 (+0000) Subject: old subst tactics removed. New destruct tactic used instead X-Git-Tag: 0.4.95@7852~26 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cd85befa31c33698c57d5d5d0d7a2384bb2644f9;p=helm.git old subst tactics removed. New destruct tactic used instead --- diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fun.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fun.ma index c88b2f926..86e8031b4 100644 --- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fun.ma +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fun.ma @@ -39,7 +39,7 @@ theorem lift_mono: \forall l,i,t,t1. Lift l i t t1 \to | lapply linear lift_inv_lref_1_le_nplus to H3, H1, H2 | lapply linear lift_inv_bind_1 to H5. decompose | lapply linear lift_inv_flat_1 to H5. decompose - ]; subst; autobatch. + ]; destruct; autobatch. qed. theorem lift_inj: \forall l,i,t1,t. Lift l i t1 t \to @@ -53,5 +53,5 @@ theorem lift_inj: \forall l,i,t1,t. Lift l i t1 t \to lapply lift_inv_lref_2_le_nplus to H3, H0, H2 | lapply linear lift_inv_bind_2 to H5. decompose | lapply linear lift_inv_flat_2 to H5. decompose - ]; subst; autobatch. + ]; destruct; autobatch. qed. diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma index 87b7bdc8c..95630e43e 100644 --- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma @@ -21,7 +21,7 @@ include "Lift/defs.ma". theorem lift_inv_sort_1: \forall l, i, h, x. Lift l i (sort h) x \to x = sort h. - intros. inversion H; clear H; intros; subst. autobatch. + intros. inversion H; clear H; intros; destruct. autobatch. qed. theorem lift_inv_lref_1: \forall l, i, j1, x. @@ -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; autobatch depth = 5 size = 7. + intros. inversion H; clear H; intros; destruct; autobatch depth = 5 size = 7. 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; autobatch depth = 5 size = 7. + intros. inversion H; clear H; intros; destruct; autobatch depth = 5 size = 7. qed. theorem lift_inv_flat_1: \forall l, i, r, u1, t1, x. @@ -48,13 +48,13 @@ 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. autobatch depth = 5 size = 7. + intros. inversion H; clear H; intros; destruct. autobatch depth = 5 size = 7. qed. theorem lift_inv_sort_2: \forall l, i, x, h. Lift l i x (sort h) \to x = sort h. - intros. inversion H; clear H; intros; subst. autobatch. + intros. inversion H; clear H; intros; destruct. autobatch. qed. theorem lift_inv_lref_2: \forall l, i, x, j2. @@ -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; autobatch depth = 5 size = 10. + intros. inversion H; clear H; intros; destruct; autobatch depth = 5 size = 10. 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. autobatch depth = 5 size = 7. + intros. inversion H; clear H; intros; destruct. autobatch depth = 5 size = 7. 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. autobatch depth = 5 size = 7. + intros. inversion H; clear H; intros; destruct. autobatch depth = 5 size = 7. qed. (* Corollaries of inversion properties ***************************************) @@ -90,7 +90,7 @@ theorem lift_inv_lref_1_gt: \forall l, i, j1, x. Lift l i (lref j1) x \to i > j1 \to x = lref j1. intros. - lapply linear lift_inv_lref_1 to H. decompose; subst; + lapply linear lift_inv_lref_1 to H. decompose; destruct; [ autobatch | lapply linear nle_false to H2, H1. decompose ]. @@ -100,7 +100,7 @@ theorem lift_inv_lref_1_le: \forall l, i, j1, x. Lift l i (lref j1) x \to i <= j1 \to \exists j2. (l + j1 == j2) \land x = lref j2. intros. - lapply linear lift_inv_lref_1 to H. decompose; subst; + lapply linear lift_inv_lref_1 to H. decompose; destruct; [ lapply linear nle_false to H1, H2. decompose | autobatch ]. @@ -111,9 +111,9 @@ theorem lift_inv_lref_1_le_nplus: \forall l, i, j1, x. i <= j1 \to \forall j2. (l + j1 == j2) \to x = lref j2. intros. - lapply linear lift_inv_lref_1 to H. decompose; subst; + lapply linear lift_inv_lref_1 to H. decompose; destruct; [ lapply linear nle_false to H1, H3. decompose - | lapply linear nplus_mono to H2, H4. subst. autobatch + | lapply linear nplus_mono to H2, H4. destruct. autobatch ]. qed. @@ -121,7 +121,7 @@ theorem lift_inv_lref_2_gt: \forall l, i, x, j2. Lift l i x (lref j2) \to i > j2 \to x = lref j2. intros. - lapply linear lift_inv_lref_2 to H. decompose; subst; + lapply linear lift_inv_lref_2 to H. decompose; destruct; [ autobatch | lapply linear nle_false to H2, H1. decompose ]. @@ -131,7 +131,7 @@ theorem lift_inv_lref_2_le: \forall l, i, x, j2. Lift l i x (lref j2) \to i <= j2 \to \exists j1. (l + j1 == j2) \land x = lref j1. intros. - lapply linear lift_inv_lref_2 to H. decompose; subst; + lapply linear lift_inv_lref_2 to H. decompose; destruct; [ lapply linear nle_false to H1, H2. decompose | autobatch ]. @@ -142,8 +142,8 @@ theorem lift_inv_lref_2_le_nplus: \forall l, i, x, j2. i <= j2 \to \forall j1. (l + j1 == j2) \to x = lref j1. intros. - lapply linear lift_inv_lref_2 to H. decompose; subst; + lapply linear lift_inv_lref_2 to H. decompose; destruct; [ lapply linear nle_false to H1, H3. decompose - | lapply linear nplus_inj_2 to H2, H4. subst. autobatch + | lapply linear nplus_inj_2 to H2, H4. destruct. autobatch ]. qed. diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma index 47345e288..9df9cbd63 100644 --- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma @@ -23,27 +23,27 @@ theorem lift_comp: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to \forall i,y. Lift l1 i u1 y \to i1 >= i2 \to (l2 + i1 == i) \to x = y. intros 5. elim H; clear H i1 t1 t2; - [ lapply lift_mono to H1, H2. clear H2. subst. - lapply linear lift_inv_sort_1 to H1. subst. - lapply linear lift_inv_sort_1 to H3. subst. autobatch - | lapply lift_mono to H2, H3. clear H3. subst. + [ lapply lift_mono to H1, H2. clear H2. destruct. + lapply linear lift_inv_sort_1 to H1. destruct. + lapply linear lift_inv_sort_1 to H3. destruct. autobatch + | lapply lift_mono to H2, H3. clear H3. destruct. lapply linear lift_inv_lref_1 to H2. - decompose; subst; clear H2 H5; - lapply linear lift_inv_lref_1_gt to H4; subst; autobatch width = 4 + decompose; destruct; clear H2 H5; + lapply linear lift_inv_lref_1_gt to H4; destruct; autobatch width = 4 | lapply lift_inv_lref_1_le to H3; [ 2: autobatch ]. clear H3. lapply lift_inv_lref_1_le to H4; [ 2: autobatch ]. clear H4. - decompose. subst. clear H6 i2. + decompose. destruct. clear H6 i2. lapply lift_inv_lref_1_le to H5; [ 2: autobatch depth = 4 width = 4 ]. - decompose. subst. clear H5 H1 H7 i. autobatch depth = 4 size = 7 + decompose. destruct. clear H5 H1 H7 i. autobatch depth = 4 size = 7 | clear H1 H3. lapply linear lift_inv_bind_1 to H5. - lapply linear lift_inv_bind_1 to H6. decompose. subst. - lapply linear lift_inv_bind_1 to H7. decompose. subst. + lapply linear lift_inv_bind_1 to H6. decompose. destruct. + lapply linear lift_inv_bind_1 to H7. decompose. destruct. autobatch depth = 4 width = 6 size = 15 | clear H1 H3. lapply linear lift_inv_flat_1 to H5. - lapply linear lift_inv_flat_1 to H6. decompose. subst. - lapply linear lift_inv_flat_1 to H7. decompose. subst. + lapply linear lift_inv_flat_1 to H6. decompose. destruct. + lapply linear lift_inv_flat_1 to H7. decompose. destruct. autobatch depth = 4 width = 6 size = 9 ]. qed. @@ -55,7 +55,7 @@ theorem lift_comp_rew_dx: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to Lift l1 i u1 u2. intros. lapply (lift_total l1 u1 i). decompose. - lapply lift_comp to H, H1, H2, H5, H3, H4. subst. autobatch. + lapply lift_comp to H, H1, H2, H5, H3, H4. destruct. autobatch. qed. theorem lift_comp_rew_sx: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to @@ -65,7 +65,7 @@ theorem lift_comp_rew_sx: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to Lift l1 i1 u1 u2. intros. lapply (lift_total l1 u1 i1). decompose. - lapply lift_comp to H1, H, H5, H2, H3, H4. subst. autobatch. + lapply lift_comp to H1, H, H5, H2, H3, H4. destruct. autobatch. qed. (* theorem lift_trans_le: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to