From f897953a3fff70a0c1de4683c196385d563ce238 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 15 Feb 2013 18:52:30 +0000 Subject: [PATCH] we rephrased sstas in terms of star --- .../lambdadelta/basic_2/computation/dxprs.ma | 9 +- .../basic_2/computation/dxprs_lsubss.ma | 2 +- .../lambdadelta/basic_2/dynamic/snv_aaa.ma | 3 +- .../lambdadelta/basic_2/dynamic/snv_ltpr_2.ma | 22 ++++- .../lambdadelta/basic_2/static/ssta.ma | 3 + .../lambdadelta/basic_2/unwind/sstas.ma | 93 +++++++++---------- .../lambdadelta/basic_2/unwind/sstas_aaa.ma | 2 +- .../lambdadelta/basic_2/unwind/sstas_lift.ma | 25 ++--- .../basic_2/unwind/sstas_lsubss.ma | 4 +- .../basic_2/unwind/sstas_ltpss_dx.ma | 13 +-- .../lambdadelta/basic_2/unwind/sstas_sstas.ma | 9 +- 11 files changed, 88 insertions(+), 97 deletions(-) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs.ma index 1db0aec2b..90663d932 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs.ma @@ -25,15 +25,14 @@ interpretation "decomposed extended parallel computation (term)" (* Basic properties *********************************************************) -lemma dxprs_refl: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ⦃h, L⦄ ⊢ T •*➡*[g] T. -/3 width=3/ qed. +lemma dxprs_refl: ∀h,g,L. reflexive … (dxprs h g L). +/2 width=3/ qed. lemma sstas_dxprs: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •*[g] T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2. /2 width=3/ qed. -lemma cprs_dxprs: ∀h,g,L,T1,T2,U,l. ⦃h, L⦄ ⊢ T1 •[g, l] U → L ⊢ T1 ➡* T2 → - ⦃h, L⦄ ⊢ T1 •*➡*[g] T2. -/3 width=3/ qed. +lemma cprs_dxprs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2. +/2 width=3/ qed. lemma dxprs_strap1: ∀h,g,L,T1,T,T2. ⦃h, L⦄ ⊢ T1 •*➡*[g] T → L ⊢ T ➡ T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lsubss.ma index a9a5cd84e..b1e340b2c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lsubss.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lsubss.ma @@ -22,5 +22,5 @@ include "basic_2/computation/dxprs.ma". lemma lsubss_dxprs_trans: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → ∀T1,T2. ⦃h, L2⦄ ⊢ T1 •*➡*[g] T2 → ⦃h, L1⦄ ⊢ T1 •*➡*[g] T2. #h #g #L1 #L2 #HL12 #T1 #T2 * -lapply (lsubss_fwd_lsubs2 … HL12) /4 width=5/ +lapply (lsubss_fwd_lsubs2 … HL12) /3 width=5/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma index 3ebe6e485..010a1ad7d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma @@ -13,7 +13,6 @@ (**************************************************************************) include "basic_2/computation/csn_aaa.ma". -include "basic_2/computation/dxprs_lift.ma". include "basic_2/computation/dxprs_aaa.ma". include "basic_2/equivalence/cpcs_aaa.ma". include "basic_2/dynamic/snv.ma". @@ -28,7 +27,7 @@ lemma snv_aaa: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → ∃A. L ⊢ T ⁝ A. | #I #L #K #V #i #HLK #_ * /3 width=6/ | #a * #L #V #T #_ #_ * #B #HV * #A #HA /3 width=2/ | #a #L #V #W #W0 #T #U #l #_ #_ #HVW #HW0 #HTU * #B #HV * #X #HT - lapply (dxprs_aaa h g … HV W0 ?) [ -HTU /2 width=4/ ] -W #HW0 (**) (* auto fail without -HTU *) + lapply (dxprs_aaa h g … HV W0 ?) [ -HTU /3 width=4/ ] -W #HW0 (**) (* auto fail without -HTU *) lapply (dxprs_aaa … HT … HTU) -HTU #H elim (aaa_inv_abst … H) -H #B0 #A #H1 #HU #H2 destruct lapply (aaa_mono … H1 … HW0) -W0 #H destruct /3 width=4/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr_2.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr_2.ma index 3a722d9dd..3a6ee2e96 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr_2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr_2.ma @@ -39,7 +39,9 @@ fact snv_ltpr_tpr_aux: ∀h,g,n. ( elim (ltpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) -HLK1 #HLK1 - lapply (IH1 … HV1 … HK12 V2 ?) -IH1 -HV1 -HK12 // -L1 -K1 /4 width=1/ -HV12 /2 width=5/ + lapply (IH1 … HV1 … HK12 V2 ?) -IH1 -HV1 -HK12 // + [ @cprs_dxprs /3 width=1/ (**) (* auto: /4 width=1/ fails *) + ] -HV12 /2 width=5/ | #p #Hn #H1 #L2 #HL12 #X #H2 destruct -IH2 elim (snv_inv_gref … H1) | #a #I #V1 #T1 #Hn #H1 #L2 #HL12 #X #H2 destruct -IH2 @@ -48,18 +50,28 @@ fact snv_ltpr_tpr_aux: ∀h,g,n. ( [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct lapply (tps_lsubs_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02 lapply (cpr_intro (L2.ⓑ{I}V2) … T2 0 1 HT10 ?) -HT10 /2 width=1/ -HT02 #HT12 - lapply (IH1 … HV1 … HL12 V2 ?) -HV1 // /4 width=1/ #HV2 + lapply (IH1 … HV1 … HL12 V2 ?) -HV1 // + [ @cprs_dxprs /3 width=1/ (**) (* auto: /4 width=1/ fails *) + ] #HV2 lapply (IH1 … HT1 (L2.ⓑ{I}V2) … T2 ?) -IH1 -HT1 /3 width=1/ | #T2 #HT12 #HXT2 #H1 #H2 destruct - lapply (IH1 … HT1 (L2.ⓓV1) … T2 ?) -IH1 -HT1 // /4 width=1/ -HT12 -HL12 #HT2 + lapply (IH1 … HT1 (L2.ⓓV1) … T2 ?) -IH1 -HT1 // /2 width=2/ + [ @cprs_dxprs /3 width=1/ (**) (* auto: /4 width=1/ fails *) + ] -HT12 -HL12 #HT2 lapply (snv_inv_lift … HT2 L2 … HXT2) -T2 // /2 width=1/ ] | #V1 #T1 #Hn #H1 #L2 #HL12 #X #H2 destruct elim (snv_inv_appl … H1) -H1 #a #W10 #W1 #U1 #l #HV1 #HT1 #HVW1 #HW10 #HTU1 elim (tpr_inv_appl1 … H2) -H2 * [ #V2 #T2 #HV12 #HT12 #H destruct - lapply (IH1 … HV1 … HL12 V2 ?) // /4 width=1/ #HV2 - lapply (IH1 … HT1 … HL12 T2 ?) // /4 width=1/ #HT2 + lapply (IH1 … HV1 … HL12 V2 ?) + [ @cprs_dxprs /3 width=1/ (**) (* auto: /4 width=1/ fails *) + | // + ] #HV2 + lapply (IH1 … HT1 … HL12 T2 ?) + [ @cprs_dxprs /3 width=1/ (**) (* auto: /4 width=1/ fails *) + | // + ] #HT2 lapply (IH1 … HT1 … HTU1) -IH1 // #H elim (snv_inv_bind … H) -H #HW1 #HU1 elim (IH2 … HVW1 … HL12 … HV12 HV1) -IH2 -HVW1 -HV12 -HV1 // #W2 #HVW2 #HW12 diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma index 7ffa93cb4..ee7a26e22 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma @@ -34,6 +34,9 @@ inductive ssta (h:sh) (g:sd h): nat → lenv → relation term ≝ interpretation "stratified static type assignment (term)" 'StaticType h g l L T U = (ssta h g l L T U). +definition ssta_step: ∀h. sd h → lenv → relation term ≝ λh,g,L,T,U. + ∃l. ⦃h, L⦄ ⊢ T •[g, l+1] U. + (* Basic inversion lemmas ************************************************) fact ssta_inv_sort1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ∀k0. T = ⋆k0 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas.ma b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas.ma index 3928e49cc..c504e4edc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas.ma @@ -16,69 +16,62 @@ include "basic_2/static/ssta.ma". (* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************) -inductive sstas (h:sh) (g:sd h) (L:lenv): relation term ≝ -| sstas_refl: ∀T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → sstas h g L T T -| sstas_step: ∀T,U1,U2,l. ⦃h, L⦄ ⊢ T •[g, l+1] U1 → sstas h g L U1 U2 → - sstas h g L T U2. +(* Note: includes: stass_refl *) +definition sstas: ∀h. sd h → lenv → relation term ≝ + λh,g,L. star … (ssta_step h g L). interpretation "iterated stratified static type assignment (term)" 'StaticTypeStar h g L T U = (sstas h g L T U). (* Basic eliminators ********************************************************) -fact sstas_ind_alt_aux: ∀h,g,L,U2. ∀R:predicate term. - (∀T,l. ⦃h, L⦄ ⊢ U2 •[g , l] T → R U2) → - (∀T,U1,l. ⦃h, L⦄ ⊢ T •[g, l + 1] U1 → - ⦃h, L⦄ ⊢ U1 •* [g] U2 → R U1 → R T - ) → - ∀T,U. ⦃h, L⦄ ⊢ T •*[g] U → U = U2 → R T. -#h #g #L #U2 #R #H1 #H2 #T #U #H elim H -H -T -U /2 width=3/ /3 width=5/ +lemma sstas_ind: ∀h,g,L,T. ∀R:predicate term. + R T → ( + ∀U1,U2,l. ⦃h, L⦄ ⊢ T •* [g] U1 → ⦃h, L⦄ ⊢ U1 •[g, l + 1] U2 → + R U1 → R U2 + ) → + ∀U. ⦃h, L⦄ ⊢ T •*[g] U → R U. +#h #g #L #T #R #IH1 #IH2 #U #H elim H -U // +#U1 #U2 #H * /2 width=5/ qed-. -lemma sstas_ind_alt: ∀h,g,L,U2. ∀R:predicate term. - (∀T,l. ⦃h, L⦄ ⊢ U2 •[g , l] T → R U2) → - (∀T,U1,l. ⦃h, L⦄ ⊢ T •[g, l + 1] U1 → - ⦃h, L⦄ ⊢ U1 •* [g] U2 → R U1 → R T - ) → - ∀T. ⦃h, L⦄ ⊢ T •*[g] U2 → R T. -/3 width=9 by sstas_ind_alt_aux/ qed-. - -(* Basic inversion lemmas ***************************************************) - -fact sstas_inv_bind1_aux: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → - ∀a,J,X,Y. T = ⓑ{a,J}Y.X → - ∃∃Z. ⦃h, L.ⓑ{J}Y⦄ ⊢ X •*[g] Z & U = ⓑ{a,J}Y.Z. -#h #g #L #T #U #H @(sstas_ind_alt … H) -T -[ #U0 #l #HU0 #a #J #X #Y #H destruct - elim (ssta_inv_bind1 … HU0) -HU0 #X0 #HX0 #H destruct /3 width=3/ -| #T0 #U0 #l #HTU0 #_ #IHU0 #a #J #X #Y #H destruct - elim (ssta_inv_bind1 … HTU0) -HTU0 #X0 #HX0 #H destruct - elim (IHU0 a J X0 Y …) -IHU0 // #X1 #HX01 #H destruct /3 width=4/ -] +lemma sstas_ind_dx: ∀h,g,L,U2. ∀R:predicate term. + R U2 → ( + ∀T,U1,l. ⦃h, L⦄ ⊢ T •[g, l + 1] U1 → ⦃h, L⦄ ⊢ U1 •* [g] U2 → + R U1 → R T + ) → + ∀T. ⦃h, L⦄ ⊢ T •*[g] U2 → R T. +#h #g #L #U2 #R #IH1 #IH2 #T #H @(star_ind_l … T H) -T // +#T #T0 * /2 width=5/ qed-. -lemma sstas_inv_bind1: ∀h,g,a,J,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{a,J}Y.X •*[g] U → - ∃∃Z. ⦃h, L.ⓑ{J}Y⦄ ⊢ X •*[g] Z & U = ⓑ{a,J}Y.Z. -/2 width=3 by sstas_inv_bind1_aux/ qed-. +(* Basic properties *********************************************************) + +lemma ssta_sstas: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l+1] U → ⦃h, L⦄ ⊢ T •*[g] U. +/3 width=2/ qed. + +lemma sstas_strap1: ∀h,g,L,T1,T2,U2,l. ⦃h, L⦄ ⊢ T1 •*[g] T2 → ⦃h, L⦄ ⊢ T2 •[g,l+1] U2 → + ⦃h, L⦄ ⊢ T1 •*[g] U2. +/3 width=4 by sstep, ex_intro/ (**) (* auto fails without trace *) +qed. + +lemma sstas_strap2: ∀h,g,L,T1,U1,U2,l. ⦃h, L⦄ ⊢ T1 •[g, l+1] U1 → ⦃h, L⦄ ⊢ U1 •*[g] U2 → + ⦃h, L⦄ ⊢ T1 •*[g] U2. +/3 width=3 by star_compl, ex_intro/ (**) (* auto fails without trace *) +qed. -fact sstas_inv_appl1_aux: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → ∀X,Y. T = ⓐY.X → - ∃∃Z. ⦃h, L⦄ ⊢ X •*[g] Z & U = ⓐY.Z. -#h #g #L #T #U #H @(sstas_ind_alt … H) -T -[ #U0 #l #HU0 #X #Y #H destruct - elim (ssta_inv_appl1 … HU0) -HU0 #X0 #HX0 #H destruct /3 width=3/ -| #T0 #U0 #l #HTU0 #_ #IHU0 #X #Y #H destruct - elim (ssta_inv_appl1 … HTU0) -HTU0 #X0 #HX0 #H destruct - elim (IHU0 X0 Y ?) -IHU0 // #X1 #HX01 #H destruct /3 width=4/ -] +(* Basic inversion lemmas ***************************************************) + +lemma sstas_inv_bind1: ∀h,g,a,I,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{a,I}Y.X •*[g] U → + ∃∃Z. ⦃h, L.ⓑ{I}Y⦄ ⊢ X •*[g] Z & U = ⓑ{a,I}Y.Z. +#h #g #a #I #L #Y #X #U #H @(sstas_ind … H) -U /2 width=3/ +#T #U #l #_ #HTU * #Z #HXZ #H destruct +elim (ssta_inv_bind1 … HTU) -HTU #Z0 #HZ0 #H destruct /3 width=4/ qed-. lemma sstas_inv_appl1: ∀h,g,L,Y,X,U. ⦃h, L⦄ ⊢ ⓐY.X •*[g] U → ∃∃Z. ⦃h, L⦄ ⊢ X •*[g] Z & U = ⓐY.Z. -/2 width=3 by sstas_inv_appl1_aux/ qed-. - -(* Basic forward lemmas *****************************************************) - -lemma sstas_fwd_correct: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → - ∃∃l,W. ⦃h, L⦄ ⊢ U •[g, l] W. -#h #g #L #T #U #H @(sstas_ind_alt … H) -T // /2 width=3/ +#h #g #L #Y #X #U #H @(sstas_ind … H) -U /2 width=3/ +#T #U #l #_ #HTU * #Z #HXZ #H destruct +elim (ssta_inv_appl1 … HTU) -HTU #Z0 #HZ0 #H destruct /3 width=4/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_aaa.ma index fbf485841..6d7cc3c2f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_aaa.ma @@ -21,5 +21,5 @@ include "basic_2/unwind/sstas.ma". lemma sstas_aaa: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → ∀A. L ⊢ T ⁝ A → L ⊢ U ⁝ A. -#h #g #L #T #U #H @(sstas_ind_alt … H) -T // /3 width=6/ +#h #g #L #T #U #H @(sstas_ind_dx … H) -T // /3 width=6/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lift.ma index 7273963a3..ea4b303ef 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lift.ma @@ -17,22 +17,14 @@ include "basic_2/unwind/sstas.ma". (* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************) -(* Advanced properties ******************************************************) - -lemma ssta_sstas: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l+1] U → ⦃h, L⦄ ⊢ T •*[g] U. -#h #g #L #T #U #l #HTU -elim (ssta_fwd_correct … HTU) /3 width=4/ -qed. - (* Properties on relocation *************************************************) lemma sstas_lift: ∀h,g,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 → ∀T2. ⇧[d, e] T1 ≡ T2 → ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 •*[g] U2. -#h #g #L1 #T1 #U1 #H @(sstas_ind_alt … H) -T1 -[ #T1 #l #HUT1 #L2 #d #e #HL21 #X #HX #U2 #HU12 - >(lift_mono … HX … HU12) -X - elim (lift_total T1 d e) /3 width=11/ +#h #g #L1 #T1 #U1 #H @(sstas_ind_dx … H) -T1 +[ #L2 #d #e #HL21 #X #HX #U2 #HU12 + >(lift_mono … HX … HU12) -X // | #T0 #U0 #l0 #HTU0 #_ #IHU01 #L2 #d #e #HL21 #T2 #HT02 #U2 #HU12 elim (lift_total U0 d e) /3 width=10/ ] @@ -43,11 +35,8 @@ qed. lemma sstas_inv_lift1: ∀h,g,L2,T2,U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 → ∀L1,d,e. ⇩[d, e] L2 ≡ L1 → ∀T1. ⇧[d, e] T1 ≡ T2 → ∃∃U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 & ⇧[d, e] U1 ≡ U2. -#h #g #L2 #T2 #U2 #H @(sstas_ind_alt … H) -T2 -[ #T2 #l #HUT2 #L1 #d #e #HL21 #U1 #HU12 - elim (ssta_inv_lift1 … HUT2 … HL21 … HU12) -HUT2 -HL21 /3 width=3/ -| #T0 #U0 #l0 #HTU0 #_ #IHU01 #L1 #d #e #HL21 #U1 #HU12 - elim (ssta_inv_lift1 … HTU0 … HL21 … HU12) -HTU0 -HU12 #U #HU1 #HU0 - elim (IHU01 … HL21 … HU0) -IHU01 -HL21 -U0 /3 width=4/ -] +#h #g #L2 #T2 #U2 #H @(sstas_ind_dx … H) -T2 /2 width=3/ +#T0 #U0 #l0 #HTU0 #_ #IHU01 #L1 #d #e #HL21 #U1 #HU12 +elim (ssta_inv_lift1 … HTU0 … HL21 … HU12) -HTU0 -HU12 #U #HU1 #HU0 +elim (IHU01 … HL21 … HU0) -IHU01 -HL21 -U0 /3 width=4/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lsubss.ma index ba2910da8..5ec33634f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lsubss.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lsubss.ma @@ -21,10 +21,10 @@ include "basic_2/unwind/sstas.ma". lemma lsubss_sstas_trans: ∀h,g,L2,T,U. ⦃h, L2⦄ ⊢ T •*[g] U → ∀L1. h ⊢ L1 •⊑[g] L2 → ⦃h, L1⦄ ⊢ T •*[g] U. -#h #g #L2 #T #U #H @(sstas_ind_alt … H) -T /3 width=4/ /3 width=5/ +#h #g #L2 #T #U #H @(sstas_ind_dx … H) -T // /3 width=5/ qed. lemma lsubss_sstas_conf: ∀h,g,L1,T,U. ⦃h, L1⦄ ⊢ T •*[g] U → ∀L2. h ⊢ L1 •⊑[g] L2 → ⦃h, L2⦄ ⊢ T •*[g] U. -#h #g #L2 #T #U #H @(sstas_ind_alt … H) -T /3 width=4/ /3 width=5/ +#h #g #L2 #T #U #H @(sstas_ind_dx … H) -T // /3 width=5/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_ltpss_dx.ma index 84f2d805b..2a8f8e7d2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_ltpss_dx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_ltpss_dx.ma @@ -24,20 +24,17 @@ lemma sstas_ltpss_dx_tpss_conf: ∀h,g,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 ∀T2. L2 ⊢ T1 ▶* [d, e] T2 → ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 & L2 ⊢ U1 ▶* [d, e] U2. -#h #g #L1 #T1 #U1 #H @(sstas_ind_alt … H) -T1 -[ #T1 #l #HUT1 #L2 #d #e #HL12 #U2 #HU12 - elim (ssta_ltpss_dx_tpss_conf … HUT1 … HL12 … HU12) -HUT1 -HL12 /3 width=3/ -| #T0 #U0 #l0 #HTU0 #_ #IHU01 #L2 #d #e #HL12 #T #HT0 - elim (ssta_ltpss_dx_tpss_conf … HTU0 … HL12 … HT0) -HTU0 -HT0 #U #HTU #HU0 - elim (IHU01 … HL12 … HU0) -IHU01 -HL12 -U0 /3 width=4/ -] +#h #g #L1 #T1 #U1 #H @(sstas_ind_dx … H) -T1 /2 width=3/ +#T0 #U0 #l0 #HTU0 #_ #IHU01 #L2 #d #e #HL12 #T #HT0 +elim (ssta_ltpss_dx_tpss_conf … HTU0 … HL12 … HT0) -HTU0 -HT0 #U #HTU #HU0 +elim (IHU01 … HL12 … HU0) -IHU01 -HL12 -U0 /3 width=4/ qed. lemma sstas_ltpss_dx_tps_conf: ∀h,g,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 → ∀L2,d,e. L1 ▶* [d, e] L2 → ∀T2. L2 ⊢ T1 ▶ [d, e] T2 → ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 & L2 ⊢ U1 ▶* [d, e] U2. -/3 width=5/ qed. +/3 width=7 by step, sstas_ltpss_dx_tpss_conf/ qed. (**) (* auto fails without trace *) lemma sstas_ltpss_dx_conf: ∀h,g,L1,T,U1. ⦃h, L1⦄ ⊢ T •*[g] U1 → ∀L2,d,e. L1 ▶* [d, e] L2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_sstas.ma b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_sstas.ma index e7e99c001..f11a078bf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_sstas.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_sstas.ma @@ -21,7 +21,7 @@ include "basic_2/unwind/sstas.ma". lemma sstas_inv_O: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → ∀T0. ⦃h, L⦄ ⊢ T •[g , 0] T0 → U = T. -#h #g #L #T #U #H @(sstas_ind_alt … H) -T // +#h #g #L #T #U #H @(sstas_ind_dx … H) -T // #T0 #U0 #l0 #HTU0 #_ #_ #T1 #HT01 elim (ssta_mono … HTU0 … HT01)