From 8b1bc0a74dbc6c5854cbce31240ae829dfe7e8bf Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 28 Sep 2012 20:45:20 +0000 Subject: [PATCH] - partial commit (static component only) - results on the transitive closure of ltpss --- .../lambda_delta/basic_2/grammar/lenv_px.ma | 2 +- .../static/{aaa_ltpss.ma => aaa_ltpss_dx.ma} | 32 ++++++----- .../aaa_ltpsss.etc => static/aaa_ltpss_sn.ma} | 23 ++++---- .../{ssta_ltpss.ma => ssta_ltpss_dx.ma} | 57 ++++++++++--------- .../basic_2/static/ssta_ltpss_sn.ma | 53 +++++++++++++++++ 5 files changed, 113 insertions(+), 54 deletions(-) rename matita/matita/contribs/lambda_delta/basic_2/static/{aaa_ltpss.ma => aaa_ltpss_dx.ma} (68%) rename matita/matita/contribs/lambda_delta/basic_2/{etc/ltpsss/aaa_ltpsss.etc => static/aaa_ltpss_sn.ma} (59%) rename matita/matita/contribs/lambda_delta/basic_2/static/{ssta_ltpss.ma => ssta_ltpss_dx.ma} (69%) create mode 100644 matita/matita/contribs/lambda_delta/basic_2/static/ssta_ltpss_sn.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma index 9de1599e4..c3d05949f 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma @@ -131,7 +131,7 @@ qed. lemma lpx_inv_TC: ∀R. reflexive ? R → ∀L1,L2. lpx (TC … R) L1 L2 → TC … (lpx R) L1 L2. -#R #HR #L1 #L2 #H elim H -L1 -L2 /2 width=1/ /3 width=3/ +#R #HR #L1 #L2 #H elim H -L1 -L2 /3 width=1/ /3 width=3/ qed. lemma lpx_append: ∀R,K1,K2. lpx R K1 K2 → ∀L1,L2. lpx R L1 L2 → diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss_dx.ma similarity index 68% rename from matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss.ma rename to matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss_dx.ma index c672f02fa..2f2d07360 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss_dx.ma @@ -13,16 +13,17 @@ (**************************************************************************) include "basic_2/unfold/tpss_tpss.ma". -include "basic_2/unfold/ltpss_ldrop.ma". +include "basic_2/unfold/ltpss_dx_ldrop.ma". include "basic_2/static/aaa_lift.ma". (* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) -(* Properties about parallel unfold *****************************************) +(* Properties about dx parallel unfold **************************************) (* Note: lemma 500 *) -lemma aaa_ltpss_tpss_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2,d,e. L1 ▶* [d, e] L2 → - ∀T2. L2 ⊢ T1 ▶* [d, e] T2 → L2 ⊢ T2 ⁝ A. +lemma aaa_ltpss_dx_tpss_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → + ∀L2,d,e. L1 ▶* [d, e] L2 → + ∀T2. L2 ⊢ T1 ▶* [d, e] T2 → L2 ⊢ T2 ⁝ A. #L1 #T1 #A #H elim H -L1 -T1 -A [ #L1 #k #L2 #d #e #_ #T2 #H >(tpss_inv_sort1 … H) -H // @@ -30,21 +31,21 @@ lemma aaa_ltpss_tpss_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2,d,e. L1 ▶* [d elim (tpss_inv_lref1 … H) -H [ #H destruct elim (lt_or_ge i d) #Hdi - [ elim (ltpss_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2 - elim (ltpss_inv_tpss11 … H ?) -H /2 width=1/ -Hdi #K2 #V2 #HK12 #HV12 #H destruct + [ elim (ltpss_dx_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2 + elim (ltpss_dx_inv_tpss11 … H ?) -H /2 width=1/ -Hdi #K2 #V2 #HK12 #HV12 #H destruct /3 width=8 by aaa_lref/ (**) (* too slow without trace *) | elim (lt_or_ge i (d + e)) #Hide - [ elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HLK2 - elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K2 #V2 #HK12 #HV12 #H destruct + [ elim (ltpss_dx_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HLK2 + elim (ltpss_dx_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K2 #V2 #HK12 #HV12 #H destruct /3 width=8 by aaa_lref/ (**) (* too slow without trace *) | -Hdi - lapply (ltpss_ldrop_conf_ge … HL12 … HLK1 ?) -L1 // -Hide + lapply (ltpss_dx_ldrop_conf_ge … HL12 … HLK1 ?) -L1 // -Hide /3 width=8 by aaa_lref/ (**) (* too slow without trace *) ] ] | * #K2 #V2 #W2 #Hdi #Hide #HLK2 #HVW2 #HWT2 - elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HL2K0 - elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K0 #V0 #HK12 #HV12 #H destruct + elim (ltpss_dx_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HL2K0 + elim (ltpss_dx_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K0 #V0 #HK12 #HV12 #H destruct lapply (ldrop_mono … HL2K0 … HLK2) -HL2K0 #H destruct lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 #HLK2 lapply (tpss_trans_eq … HV12 HVW2) -V2 /3 width=7/ @@ -60,12 +61,13 @@ lemma aaa_ltpss_tpss_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2,d,e. L1 ▶* [d ] qed. -lemma aaa_ltpss_tps_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2,d,e. L1 ▶* [d, e] L2 → - ∀T2. L2 ⊢ T1 ▶ [d, e] T2 → L2 ⊢ T2 ⁝ A. +lemma aaa_ltpss_dx_tps_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → + ∀L2,d,e. L1 ▶* [d, e] L2 → + ∀T2. L2 ⊢ T1 ▶ [d, e] T2 → L2 ⊢ T2 ⁝ A. /3 width=7/ qed. -lemma aaa_ltpss_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → - ∀L2,d,e. L1 ▶* [d, e] L2 → L2 ⊢ T ⁝ A. +lemma aaa_ltpss_dx_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → + ∀L2,d,e. L1 ▶* [d, e] L2 → L2 ⊢ T ⁝ A. /2 width=7/ qed. lemma aaa_tpss_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/aaa_ltpsss.etc b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss_sn.ma similarity index 59% rename from matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/aaa_ltpsss.etc rename to matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss_sn.ma index e3d048809..4f2a44827 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/aaa_ltpsss.etc +++ b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss_sn.ma @@ -12,23 +12,26 @@ (* *) (**************************************************************************) -include "basic_2/unfold/ltpsss.ma". -include "basic_2/static/aaa_ltpss.ma". +include "basic_2/unfold/ltpss_sn_alt.ma". +include "basic_2/static/aaa_ltpss_dx.ma". (* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) -(* Properties about iterated parallel unfold ********************************) +(* Properties about sn parallel unfold **************************************) -lemma aaa_ltpsss_conf: ∀L1,T,A. L1 ⊢ T ÷ A → - ∀L2,d,e. L1 [d, e] ▶** L2 → L2 ⊢ T ÷ A. +lemma aaa_ltpss_sn_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → + ∀L2,d,e. L1 ⊢ ▶* [d, e] L2 → L2 ⊢ T ⁝ A. #L1 #T #A #HT #L2 #d #e #HL12 -@(TC_Conf3 … (λL,A. L ⊢ T ÷ A) … HT ? HL12) /2 width=5/ +lapply (ltpss_sn_ltpssa … HL12) -HL12 #HL12 +@(TC_Conf3 … (λL,A. L ⊢ T ⁝ A) … HT ? HL12) /2 width=5/ qed. -lemma aaa_ltpsss_tpss_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. L1 [d, e] ▶** L2 → - ∀T2. L2 ⊢ T1 [d, e] ▶* T2 → L2 ⊢ T2 ÷ A. +lemma aaa_ltpss_sn_tpss_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → + ∀L2,d,e. L1 ⊢ ▶* [d, e] L2 → + ∀T2. L2 ⊢ T1 ▶* [d, e] T2 → L2 ⊢ T2 ⁝ A. /3 width=5/ qed. -lemma aaa_ltpsss_tps_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. L1 [d, e] ▶** L2 → - ∀T2. L2 ⊢ T1 [d, e] ▶ T2 → L2 ⊢ T2 ÷ A. +lemma aaa_ltpss_sn_tps_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → + ∀L2,d,e. L1 ⊢ ▶* [d, e] L2 → + ∀T2. L2 ⊢ T1 ▶ [d, e] T2 → L2 ⊢ T2 ⁝ A. /3 width=5/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/ssta_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/static/ssta_ltpss_dx.ma similarity index 69% rename from matita/matita/contribs/lambda_delta/basic_2/static/ssta_ltpss.ma rename to matita/matita/contribs/lambda_delta/basic_2/static/ssta_ltpss_dx.ma index 8af4b30b7..1839c67bd 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/ssta_ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/ssta_ltpss_dx.ma @@ -13,19 +13,19 @@ (**************************************************************************) include "basic_2/unfold/tpss_tpss.ma". -include "basic_2/unfold/ltpss_tpss.ma". +include "basic_2/unfold/ltpss_dx_tpss.ma". include "basic_2/static/ssta_lift.ma". (* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************) -(* Properties about parallel unfold *****************************************) +(* Properties about dx parallel unfold **************************************) (* Note: apparently this was missing in basic_1 *) -lemma ssta_ltpss_tpss_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → - ∀L2,d,e. L1 ▶* [d, e] L2 → - ∀T2. L2 ⊢ T1 ▶* [d, e] T2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & - L2 ⊢ U1 ▶* [d, e] U2. +lemma ssta_ltpss_dx_tpss_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → + ∀L2,d,e. L1 ▶* [d, e] L2 → + ∀T2. L2 ⊢ T1 ▶* [d, e] T2 → + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & + L2 ⊢ U1 ▶* [d, e] U2. #h #g #L1 #T1 #U #l #H elim H -L1 -T1 -U -l [ #L1 #k1 #l1 #Hkl1 #L2 #d #e #_ #T2 #H >(tpss_inv_sort1 … H) -H /3 width=3/ @@ -33,27 +33,27 @@ lemma ssta_ltpss_tpss_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 elim (tpss_inv_lref1 … H) -H [ | -HVW1 ] [ #H destruct elim (lt_or_ge i d) #Hdi [ -HVW1 | ] - [ elim (ltpss_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2 - elim (ltpss_inv_tpss11 … H ?) -H /2 width=1/ #K2 #V2 #HK12 #HV12 #H destruct + [ elim (ltpss_dx_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2 + elim (ltpss_dx_inv_tpss11 … H ?) -H /2 width=1/ #K2 #V2 #HK12 #HV12 #H destruct elim (IHVW1 … HK12 … HV12) -IHVW1 -HK12 -HV12 #W2 #HVW2 #HW12 lapply (ldrop_fwd_ldrop2 … HLK2) #H elim (lift_total W2 0 (i+1)) #U2 #HWU2 lapply (tpss_lift_ge … HW12 … H … HWU1 … HWU2) // -HW12 -H -HWU1 >minus_plus minus_plus #H lapply (tpss_weak … H d e ? ?) [1,2: normalize [ >commutative_plus minus_plus minus_plus #H lapply (tpss_weak … H d e ? ?) [1,2: normalize [ >commutative_plus