From 23c056d7fb7269f952a02aad1cac8e400d2653b0 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 7 Nov 2012 16:46:54 +0000 Subject: [PATCH] - commit of the component: static - notation updates missing in former commit --- .../contribs/lambda_delta/basic_2/notation.ma | 24 +++---- .../lambda_delta/basic_2/static/ssta.ma | 64 ++++++++++++++----- .../lambda_delta/basic_2/static/ssta_aaa.ma | 2 +- .../lambda_delta/basic_2/static/ssta_lift.ma | 18 +++--- .../basic_2/static/ssta_ltpss_dx.ma | 7 +- .../lambda_delta/basic_2/static/ssta_ssta.ma | 5 +- 6 files changed, 69 insertions(+), 51 deletions(-) diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma index f53dcf867..affb8af13 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma @@ -162,9 +162,9 @@ notation "hvbox( ⇩ [ d , break e ] break term 46 L1 ≡ break term 46 L2 )" non associative with precedence 45 for @{ 'RDrop $d $e $L1 $L2 }. -notation "hvbox( ⦃ L1, break T1 ⦄ > break ⦃ L2 , break T2 ⦄ )" +notation "hvbox( ⦃ L1, break T1 ⦄ ⧁ break ⦃ L2 , break T2 ⦄ )" non associative with precedence 45 - for @{ 'SupTerm $L1 $T1 $L2 $T2 }. + for @{ 'RestSupTerm $L1 $T1 $L2 $T2 }. notation "hvbox( L ⊢ break ⌘ ⦃ T ⦄ ≡ break term 46 k )" non associative with precedence 45 @@ -192,9 +192,13 @@ notation "hvbox( ⇩ * [ e ] break term 46 L1 ≡ break term 46 L2 )" non associative with precedence 45 for @{ 'RDropStar $e $L1 $L2 }. -notation "hvbox( ⦃ L1, break T1 ⦄ > * break ⦃ L2 , break T2 ⦄ )" +notation "hvbox( ⦃ L1, break T1 ⦄ ⧁ + break ⦃ L2 , break T2 ⦄ )" non associative with precedence 45 - for @{ 'SupTermStar $L1 $T1 $L2 $T2 }. + for @{ 'RestSupTermPlus $L1 $T1 $L2 $T2 }. + +notation "hvbox( ⦃ L1, break T1 ⦄ ⧁ * break ⦃ L2 , break T2 ⦄ )" + non associative with precedence 45 + for @{ 'RestSupTermStar $L1 $T1 $L2 $T2 }. notation "hvbox( T1 break ▶ * [ d , break e ] break term 46 T2 )" non associative with precedence 45 @@ -340,10 +344,6 @@ notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 • ➡ break [ g ] br non associative with precedence 45 for @{ 'XPRed $h $g $L $T1 $T2 }. -notation "hvbox( h ⊢ break ⦃ L1, break T1 ⦄ • ⥸ break [ g ] break ⦃ L2 , break T2 ⦄ )" - non associative with precedence 45 - for @{ 'YPRed $h $g $L1 $T1 $L2 $T2 }. - (* Computation **************************************************************) notation "hvbox( T1 ➡ * break term 46 T2 )" @@ -406,14 +406,6 @@ notation "hvbox( ⦃ h , break L ⦄ ⊢ • ⬊ * break [ g ] break term 46 T2 non associative with precedence 45 for @{ 'XSN $h $g $L $T }. -notation "hvbox( h ⊢ break ⦃ L1, break T1 ⦄ • ⥸ * break [ g ] break ⦃ L2 , break T2 ⦄ )" - non associative with precedence 45 - for @{ 'YPRedStar $h $g $L1 $T1 $L2 $T2 }. - -notation "hvbox( h ⊢ break ⦃ L1, break T1 ⦄ • ⭃ * break [ g ] break ⦃ L2 , break T2 ⦄ )" - non associative with precedence 45 - for @{ 'YPRedStepStar $h $g $L1 $T1 $L2 $T2 }. - (* Conversion ***************************************************************) notation "hvbox( L ⊢ break term 46 T1 ⬌ break term 46 T2 )" diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/ssta.ma b/matita/matita/contribs/lambda_delta/basic_2/static/ssta.ma index ec990f13b..3cd0134bb 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/ssta.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/ssta.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "basic_2/substitution/ldrop.ma". +include "basic_2/unfold/frsups.ma". include "basic_2/static/sd.ma". (* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************) @@ -27,8 +28,7 @@ inductive ssta (h:sh) (g:sd h): nat → lenv → relation term ≝ ssta h g l L (ⓑ{a,I}V.T) (ⓑ{a,I}V.U) | ssta_appl: ∀L,V,T,U,l. ssta h g l L T U → ssta h g l L (ⓐV.T) (ⓐV.U) -| ssta_cast: ∀L,V,W,T,U,l. ssta h g (l - 1) L V W → ssta h g l L T U → - ssta h g l L (ⓝV. T) (ⓝW. U) +| ssta_cast: ∀L,W,T,U,l. ssta h g l L T U → ssta h g l L (ⓝW. T) U . interpretation "stratified static type assignment (term)" @@ -44,7 +44,7 @@ fact ssta_inv_sort1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ∀k0. | #L #K #W #V #U #i #l #_ #_ #_ #k0 #H destruct | #a #I #L #V #T #U #l #_ #k0 #H destruct | #L #V #T #U #l #_ #k0 #H destruct -| #L #V #W #T #U #l #_ #_ #k0 #H destruct +| #L #W #T #U #l #_ #k0 #H destruct qed. (* Basic_1: was just: sty0_gen_sort *) @@ -65,7 +65,7 @@ fact ssta_inv_lref1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ∀j. | #L #K #W #V #U #i #l #HLK #HWV #HWU #j #H destruct /3 width=8/ | #a #I #L #V #T #U #l #_ #j #H destruct | #L #V #T #U #l #_ #j #H destruct -| #L #V #W #T #U #l #_ #_ #j #H destruct +| #L #W #T #U #l #_ #j #H destruct ] qed. @@ -88,7 +88,7 @@ fact ssta_inv_bind1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → | #L #K #W #V #U #i #l #_ #_ #_ #a #I #X #Y #H destruct | #b #J #L #V #T #U #l #HTU #a #I #X #Y #H destruct /2 width=3/ | #L #V #T #U #l #_ #a #I #X #Y #H destruct -| #L #V #W #T #U #l #_ #_ #a #I #X #Y #H destruct +| #L #W #T #U #l #_ #a #I #X #Y #H destruct ] qed. @@ -105,7 +105,7 @@ fact ssta_inv_appl1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ∀X,Y | #L #K #W #V #U #i #l #_ #_ #_ #X #Y #H destruct | #a #I #L #V #T #U #l #_ #X #Y #H destruct | #L #V #T #U #l #HTU #X #Y #H destruct /2 width=3/ -| #L #V #W #T #U #l #_ #_ #X #Y #H destruct +| #L #W #T #U #l #_ #X #Y #H destruct ] qed. @@ -114,31 +114,53 @@ lemma ssta_inv_appl1: ∀h,g,L,Y,X,U,l. ⦃h, L⦄ ⊢ ⓐY.X •[g, l] U → ∃∃Z. ⦃h, L⦄ ⊢ X •[g, l] Z & U = ⓐY.Z. /2 width=3/ qed-. -fact ssta_inv_cast1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ∀X,Y. T = ⓝY.X → - ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y •[g, l-1] Z1 & ⦃h, L⦄ ⊢ X •[g, l] Z2 & - U = ⓝZ1.Z2. +fact ssta_inv_cast1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → + ∀X,Y. T = ⓝY.X → ⦃h, L⦄ ⊢ X •[g, l] U. #h #g #L #T #U #l * -L -T -U -l [ #L #k #l #_ #X #Y #H destruct | #L #K #V #W #U #l #i #_ #_ #_ #X #Y #H destruct | #L #K #W #V #U #l #i #_ #_ #_ #X #Y #H destruct | #a #I #L #V #T #U #l #_ #X #Y #H destruct | #L #V #T #U #l #_ #X #Y #H destruct -| #L #V #W #T #U #l #HVW #HTU #X #Y #H destruct /2 width=5/ +| #L #W #T #U #l #HTU #X #Y #H destruct // ] qed. (* Basic_1: was just: sty0_gen_cast *) lemma ssta_inv_cast1: ∀h,g,L,X,Y,U,l. ⦃h, L⦄ ⊢ ⓝY.X •[g, l] U → - ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y •[g, l-1] Z1 & ⦃h, L⦄ ⊢ X •[g, l] Z2 & - U = ⓝZ1.Z2. + ⦃h, L⦄ ⊢ X •[g, l] U. /2 width=4/ qed-. (* Advanced inversion lemmas ************************************************) +lemma ssta_inv_frsupp: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ⦃L, U⦄ ⧁+ ⦃L, T⦄ → ⊥. +#h #g #L #T #U #l #H elim H -L -T -U -l +[ #L #k #l #_ #H + elim (frsupp_inv_atom1_frsups … H) +| #L #K #V #W #U #i #l #_ #_ #HWU #_ #H + elim (lift_frsupp_trans … (⋆) … H … HWU) -U #X #H + elim (lift_inv_lref2_be … H ? ?) -H // +| #L #K #W #V #U #i #l #_ #_ #HWU #_ #H + elim (lift_frsupp_trans … (⋆) … H … HWU) -U #X #H + elim (lift_inv_lref2_be … H ? ?) -H // +| #a #I #L #V #T #U #l #_ #IHTU #H + elim (frsupp_inv_bind1_frsups … H) -H #H [2: /4 width=4/ ] -IHTU + lapply (frsups_fwd_fw … H) -H normalize + minus_minus_m_m /2 width=1/ /3 width=6/ - | minus_minus_m_m /2 width=1/ /3 width=6/ - |