From: Ferruccio Guidi Date: Thu, 14 Mar 2013 23:06:19 +0000 (+0000) Subject: - main proof case closed in the 4th component of preservation X-Git-Tag: make_still_working~1217 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=132d053caaeb9f8311fb0c807a9d7fd8d7acc827;p=helm.git - main proof case closed in the 4th component of preservation - bug fix in Makefile: now both xoa and probe receive both configuration files - useless notion lsubss removed (to be replaced by lsubse) --- diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index 3e5b74eaf..8493b47c0 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -3,11 +3,13 @@ H := @ TRIM := sed "s/ \\+$$//" -XOA_DIR := ../../../components/binaries/xoa -XOA := xoa.native XOA_CONF := ground_2/xoa.conf.xml XOA_TARGETS := ground_2/xoa_notation.ma ground_2/xoa.ma +XOA_DIR := ../../../components/binaries/xoa +XOA := xoa.native +XOA_OPTS := ../../matita.conf.xml $(XOA_CONF) + DEP_DIR := ../../../components/binaries/matitadep DEP := matitadep.native @@ -16,7 +18,7 @@ MAC := mac.native PRB_DIR := ../../../components/binaries/probe PRB := probe.native -PRB_OPTS := ../../matita.conf.xml $(XOA_CONF) -g +PRB_OPTS := $(XOA_OPTS) -g ORIG := . ./orig.sh ORIGS := basic_2/basic_1.orig @@ -50,7 +52,7 @@ xoa: $(XOA_TARGETS) $(XOA_TARGETS): $(XOA_CONF) @echo " EXEC $(XOA) $(XOA_CONF)" - $(H)MATITA_RT_BASE_DIR=../.. $(XOA_DIR)/$(XOA) $(XOA_CONF) + $(H)MATITA_RT_BASE_DIR=../.. $(XOA_DIR)/$(XOA) $(XOA_OPTS) # orig ####################################################################### diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lsubss.ma deleted file mode 100644 index b1e340b2c..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lsubss.ma +++ /dev/null @@ -1,26 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/unwind/sstas_lsubss.ma". -include "basic_2/computation/dxprs.ma". - -(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************) - -(* Properties on lenv ref for stratified type assignment ********************) - -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) /3 width=5/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma index f3238fbd9..2afaa8e06 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma @@ -66,15 +66,14 @@ fact snv_ltpr_tpr_aux: ∀h,g,L0,T0. | #b #V2 #W20 #T20 #T2 #HV12 #HT202 #H1 #H2 destruct elim (snv_inv_bind … HT1) -HT1 #HW20 #HT20 elim (dxprs_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW230 #_ #H destruct -T30 - lapply (cprs_div … HW230 … HW10) -W30 #HW210 - lapply (ltpr_cpcs_conf … HL12 … HW210) -HW210 #HW210 + lapply (cprs_div … HW10 … HW230) -W30 #HW120 + elim (snv_fwd_ssta … HW20) #U20 #l0 #HWU20 + elim (ssta_fwd_correct … HVW1) (lsubss_inv_atom1 … H) -H // +| #I #L1 #L #W #HL1 #IHL1 #X #H + elim (lsubss_inv_pair1 … H) -H * #L2 + [ #HL2 #H destruct /3 width=1/ + | #V #l #H1WV #H2WV #HL2 #H1 #H2 destruct /3 width=3/ + ] +| #L1 #L #V1 #W1 #l #H1VW1 #H2VW1 #HL1 #IHL1 #X #H + elim (lsubss_inv_pair1 … H) -H * #L2 + [ #HL2 #H destruct /3 width=5/ + | #V #l0 #_ #_ #_ #_ #H destruct + ] +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss_ssta.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss_ssta.etc new file mode 100644 index 000000000..f9c628921 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss_ssta.etc @@ -0,0 +1,69 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/static/ssta_lift.ma". +include "basic_2/static/ssta_ssta.ma". +include "basic_2/static/lsubss_ldrop.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED STATIC TYPE ASSIGNMENT *******) + +(* Properties concerning stratified native type assignment ******************) + +lemma lsubss_ssta_trans: ∀h,g,L2,T,U,l. ⦃h, L2⦄ ⊢ T •[g,l] U → + ∀L1. h ⊢ L1 •⊑[g] L2 → ⦃h, L1⦄ ⊢ T •[g,l] U. +#h #g #L2 #T #U #l #H elim H -L2 -T -U -l +[ /2 width=1/ +| #L2 #K2 #V2 #W2 #U2 #i #l #HLK2 #_ #HWU2 #IHVW2 #L1 #HL12 + elim (lsubss_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1 + elim (lsubss_inv_pair2 … H) -H * #K1 [ | -HWU2 -IHVW2 -HLK1 ] + [ #HK12 #H destruct /3 width=6/ + | #V1 #l0 #_ #_ #_ #_ #H destruct + ] +| #L2 #K2 #W2 #V2 #U2 #i #l #HLK2 #HWV2 #HWU2 #IHWV2 #L1 #HL12 + elim (lsubss_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1 + elim (lsubss_inv_pair2 … H) -H * #K1 [ -HWV2 | -IHWV2 ] + [ #HK12 #H destruct /3 width=6/ + | #V1 #l0 #H1 #H2 #_ #H #_ destruct + elim (ssta_fwd_correct … H2) -H2 #V #H + elim (ssta_mono … HWV2 … H) -HWV2 -H /2 width=6/ + ] +| /4 width=1/ +| /3 width=1/ +| /3 width=1/ +] +qed. + +lemma lsubss_ssta_conf: ∀h,g,L1,T,U,l. ⦃h, L1⦄ ⊢ T •[g,l] U → + ∀L2. h ⊢ L1 •⊑[g] L2 → ⦃h, L2⦄ ⊢ T •[g,l] U. +#h #g #L1 #T #U #l #H elim H -L1 -T -U -l +[ /2 width=1/ +| #L1 #K1 #V1 #W1 #U1 #i #l #HLK1 #HVW1 #HWU1 #IHVW1 #L2 #HL12 + elim (lsubss_ldrop_O1_conf … HL12 … HLK1) -L1 #X #H #HLK2 + elim (lsubss_inv_pair1 … H) -H * #K2 [ -HVW1 | -IHVW1 ] + [ #HK12 #H destruct /3 width=6/ + | #V2 #l0 #H1 #H2 #_ #H #_ destruct + elim (ssta_mono … HVW1 … H1) -HVW1 -H1 #H1 #H2 destruct + elim (ssta_fwd_correct … H2) -H2 /2 width=6/ + ] +| #L1 #K1 #W1 #V1 #U1 #i #l #HLK1 #_ #HWU1 #IHWV1 #L2 #HL12 + elim (lsubss_ldrop_O1_conf … HL12 … HLK1) -L1 #X #H #HLK2 + elim (lsubss_inv_pair1 … H) -H * #K2 [ | -HWU1 -IHWV1 -HLK2 ] + [ #HK12 #H destruct /3 width=6/ + | #V2 #l0 #_ #_ #_ #_ #H destruct + ] +| /4 width=1/ +| /3 width=1/ +| /3 width=1/ +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/sstas_lsubss.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/sstas_lsubss.etc new file mode 100644 index 000000000..5ec33634f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/sstas_lsubss.etc @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/static/lsubss_ssta.ma". +include "basic_2/unwind/sstas.ma". + +(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************) + +(* Properties on lenv ref for stratified type assignment ********************) + +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_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_dx … H) -T // /3 width=5/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubss.ma deleted file mode 100644 index 356d7fe11..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubss.ma +++ /dev/null @@ -1,106 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/static/ssta.ma". - -(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED STATIC TYPE ASSIGNMENT *******) - -(* Note: may not be transitive *) -inductive lsubss (h:sh) (g:sd h): relation lenv ≝ -| lsubss_atom: lsubss h g (⋆) (⋆) -| lsubss_pair: ∀I,L1,L2,W. lsubss h g L1 L2 → - lsubss h g (L1. ⓑ{I} W) (L2. ⓑ{I} W) -| lsubss_abbr: ∀L1,L2,V,W,l. ⦃h, L1⦄ ⊢ V •[g, l+1] W → ⦃h, L2⦄ ⊢ V •[g, l+1] W → - lsubss h g L1 L2 → lsubss h g (L1. ⓓV) (L2. ⓛW) -. - -interpretation - "local environment refinement (stratified static type assigment)" - 'CrSubEqS h g L1 L2 = (lsubss h g L1 L2). - -(* Basic inversion lemmas ***************************************************) - -fact lsubss_inv_atom1_aux: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 = ⋆ → L2 = ⋆. -#h #g #L1 #L2 * -L1 -L2 -[ // -| #I #L1 #L2 #V #_ #H destruct -| #L1 #L2 #V #W #l #_ #_ #_ #H destruct -] -qed. - -lemma lsubss_inv_atom1: ∀h,g,L2. h ⊢ ⋆ •⊑[g] L2 → L2 = ⋆. -/2 width=5/ qed-. - -fact lsubss_inv_pair1_aux: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → - ∀I,K1,V. L1 = K1. ⓑ{I} V → - (∃∃K2. h ⊢ K1 •⊑[g] K2 & L2 = K2. ⓑ{I} V) ∨ - ∃∃K2,W,l. ⦃h, K1⦄ ⊢ V •[g,l+1] W & ⦃h, K2⦄ ⊢ V •[g,l+1] W & - h ⊢ K1 •⊑[g] K2 & L2 = K2. ⓛW & I = Abbr. -#h #g #L1 #L2 * -L1 -L2 -[ #I #K1 #V #H destruct -| #J #L1 #L2 #V #HL12 #I #K1 #W #H destruct /3 width=3/ -| #L1 #L2 #V #W #l #H1VW #H2VW #HL12 #I #K1 #V1 #H destruct /3 width=7/ -] -qed. - -lemma lsubss_inv_pair1: ∀h,g,I,K1,L2,V. h ⊢ K1. ⓑ{I} V •⊑[g] L2 → - (∃∃K2. h ⊢ K1 •⊑[g] K2 & L2 = K2. ⓑ{I} V) ∨ - ∃∃K2,W,l. ⦃h, K1⦄ ⊢ V •[g,l+1] W & ⦃h, K2⦄ ⊢ V •[g,l+1] W & - h ⊢ K1 •⊑[g] K2 & L2 = K2. ⓛW & I = Abbr. -/2 width=3/ qed-. - -fact lsubss_inv_atom2_aux: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L2 = ⋆ → L1 = ⋆. -#h #g #L1 #L2 * -L1 -L2 -[ // -| #I #L1 #L2 #V #_ #H destruct -| #L1 #L2 #V #W #l #_ #_ #_ #H destruct -] -qed. - -lemma lsubss_inv_atom2: ∀h,g,L1. h ⊢ L1 •⊑[g] ⋆ → L1 = ⋆. -/2 width=5/ qed-. - -fact lsubss_inv_pair2_aux: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → - ∀I,K2,W. L2 = K2. ⓑ{I} W → - (∃∃K1. h ⊢ K1 •⊑[g] K2 & L1 = K1. ⓑ{I} W) ∨ - ∃∃K1,V,l. ⦃h, K1⦄ ⊢ V •[g,l+1] W & ⦃h, K2⦄ ⊢ V •[g,l+1] W & - h ⊢ K1 •⊑[g] K2 & L1 = K1. ⓓV & I = Abst. -#h #g #L1 #L2 * -L1 -L2 -[ #I #K2 #W #H destruct -| #J #L1 #L2 #V #HL12 #I #K2 #W #H destruct /3 width=3/ -| #L1 #L2 #V #W #l #H1VW #H2VW #HL12 #I #K2 #W2 #H destruct /3 width=7/ -] -qed. - -lemma lsubss_inv_pair2: ∀h,g,I,L1,K2,W. h ⊢ L1 •⊑[g] K2. ⓑ{I} W → - (∃∃K1. h ⊢ K1 •⊑[g] K2 & L1 = K1. ⓑ{I} W) ∨ - ∃∃K1,V,l. ⦃h, K1⦄ ⊢ V •[g,l+1] W & ⦃h, K2⦄ ⊢ V •[g,l+1] W & - h ⊢ K1 •⊑[g] K2 & L1 = K1. ⓓV & I = Abst. -/2 width=3/ qed-. - -(* Basic_forward lemmas *****************************************************) - -lemma lsubss_fwd_lsubs1: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 ≼[0, |L1|] L2. -#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ -qed-. - -lemma lsubss_fwd_lsubs2: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 ≼[0, |L2|] L2. -#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ -qed-. - -(* Basic properties *********************************************************) - -lemma lsubss_refl: ∀h,g,L. h ⊢ L •⊑[g] L. -#h #g #L elim L -L // /2 width=1/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubss_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubss_ldrop.ma deleted file mode 100644 index 82ede6149..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubss_ldrop.ma +++ /dev/null @@ -1,65 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/static/lsubss.ma". - -(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED STATIC TYPE ASSIGNMENT *******) - -(* Properties concerning basic local environment slicing ********************) - -(* Note: the constant 0 cannot be generalized *) -lemma lsubss_ldrop_O1_conf: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → - ∀K1,e. ⇩[0, e] L1 ≡ K1 → - ∃∃K2. h ⊢ K1 •⊑[g] K2 & ⇩[0, e] L2 ≡ K2. -#h #g #L1 #L2 #H elim H -L1 -L2 -[ /2 width=3/ -| #I #L1 #L2 #V #_ #IHL12 #K1 #e #H - elim (ldrop_inv_O1 … H) -H * #He #HLK1 - [ destruct - elim (IHL12 L1 0 ?) -IHL12 // #X #HL12 #H - <(ldrop_inv_refl … H) in HL12; -H /3 width=3/ - | elim (IHL12 … HLK1) -L1 /3 width=3/ - ] -| #L1 #L2 #V #W #l #H1VW #H2VW #_ #IHL12 #K1 #e #H - elim (ldrop_inv_O1 … H) -H * #He #HLK1 - [ destruct - elim (IHL12 L1 0 ?) -IHL12 // #X #HL12 #H - <(ldrop_inv_refl … H) in HL12; -H /3 width=3/ - | elim (IHL12 … HLK1) -L1 /3 width=3/ - ] -] -qed. - -(* Note: the constant 0 cannot be generalized *) -lemma lsubss_ldrop_O1_trans: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → - ∀K2,e. ⇩[0, e] L2 ≡ K2 → - ∃∃K1. h ⊢ K1 •⊑[g] K2 & ⇩[0, e] L1 ≡ K1. -#h #g #L1 #L2 #H elim H -L1 -L2 -[ /2 width=3/ -| #I #L1 #L2 #V #_ #IHL12 #K2 #e #H - elim (ldrop_inv_O1 … H) -H * #He #HLK2 - [ destruct - elim (IHL12 L2 0 ?) -IHL12 // #X #HL12 #H - <(ldrop_inv_refl … H) in HL12; -H /3 width=3/ - | elim (IHL12 … HLK2) -L2 /3 width=3/ - ] -| #L1 #L2 #V #W #l #H1VW #H2VW #_ #IHL12 #K2 #e #H - elim (ldrop_inv_O1 … H) -H * #He #HLK2 - [ destruct - elim (IHL12 L2 0 ?) -IHL12 // #X #HL12 #H - <(ldrop_inv_refl … H) in HL12; -H /3 width=3/ - | elim (IHL12 … HLK2) -L2 /3 width=3/ - ] -] -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubss_lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubss_lsubss.ma deleted file mode 100644 index d9f9496ba..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubss_lsubss.ma +++ /dev/null @@ -1,36 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/static/lsubss_ssta.ma". - -(* LOCAL ENVIRONMENT REFINEMENT FOR STATIC TYPE ASSIGNMENT ******************) - -(* Main properties **********************************************************) - -theorem lsubss_trans: ∀h,g,L1,L. h ⊢ L1 •⊑[g] L → ∀L2. h ⊢ L •⊑[g] L2 → - h ⊢ L1 •⊑[g] L2. -#h #g #L1 #L #H elim H -L1 -L -[ #X #H >(lsubss_inv_atom1 … H) -H // -| #I #L1 #L #W #HL1 #IHL1 #X #H - elim (lsubss_inv_pair1 … H) -H * #L2 - [ #HL2 #H destruct /3 width=1/ - | #V #l #H1WV #H2WV #HL2 #H1 #H2 destruct /3 width=3/ - ] -| #L1 #L #V1 #W1 #l #H1VW1 #H2VW1 #HL1 #IHL1 #X #H - elim (lsubss_inv_pair1 … H) -H * #L2 - [ #HL2 #H destruct /3 width=5/ - | #V #l0 #_ #_ #_ #_ #H destruct - ] -] -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubss_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubss_ssta.ma deleted file mode 100644 index f9c628921..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubss_ssta.ma +++ /dev/null @@ -1,69 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/static/ssta_lift.ma". -include "basic_2/static/ssta_ssta.ma". -include "basic_2/static/lsubss_ldrop.ma". - -(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED STATIC TYPE ASSIGNMENT *******) - -(* Properties concerning stratified native type assignment ******************) - -lemma lsubss_ssta_trans: ∀h,g,L2,T,U,l. ⦃h, L2⦄ ⊢ T •[g,l] U → - ∀L1. h ⊢ L1 •⊑[g] L2 → ⦃h, L1⦄ ⊢ T •[g,l] U. -#h #g #L2 #T #U #l #H elim H -L2 -T -U -l -[ /2 width=1/ -| #L2 #K2 #V2 #W2 #U2 #i #l #HLK2 #_ #HWU2 #IHVW2 #L1 #HL12 - elim (lsubss_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1 - elim (lsubss_inv_pair2 … H) -H * #K1 [ | -HWU2 -IHVW2 -HLK1 ] - [ #HK12 #H destruct /3 width=6/ - | #V1 #l0 #_ #_ #_ #_ #H destruct - ] -| #L2 #K2 #W2 #V2 #U2 #i #l #HLK2 #HWV2 #HWU2 #IHWV2 #L1 #HL12 - elim (lsubss_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1 - elim (lsubss_inv_pair2 … H) -H * #K1 [ -HWV2 | -IHWV2 ] - [ #HK12 #H destruct /3 width=6/ - | #V1 #l0 #H1 #H2 #_ #H #_ destruct - elim (ssta_fwd_correct … H2) -H2 #V #H - elim (ssta_mono … HWV2 … H) -HWV2 -H /2 width=6/ - ] -| /4 width=1/ -| /3 width=1/ -| /3 width=1/ -] -qed. - -lemma lsubss_ssta_conf: ∀h,g,L1,T,U,l. ⦃h, L1⦄ ⊢ T •[g,l] U → - ∀L2. h ⊢ L1 •⊑[g] L2 → ⦃h, L2⦄ ⊢ T •[g,l] U. -#h #g #L1 #T #U #l #H elim H -L1 -T -U -l -[ /2 width=1/ -| #L1 #K1 #V1 #W1 #U1 #i #l #HLK1 #HVW1 #HWU1 #IHVW1 #L2 #HL12 - elim (lsubss_ldrop_O1_conf … HL12 … HLK1) -L1 #X #H #HLK2 - elim (lsubss_inv_pair1 … H) -H * #K2 [ -HVW1 | -IHVW1 ] - [ #HK12 #H destruct /3 width=6/ - | #V2 #l0 #H1 #H2 #_ #H #_ destruct - elim (ssta_mono … HVW1 … H1) -HVW1 -H1 #H1 #H2 destruct - elim (ssta_fwd_correct … H2) -H2 /2 width=6/ - ] -| #L1 #K1 #W1 #V1 #U1 #i #l #HLK1 #_ #HWU1 #IHWV1 #L2 #HL12 - elim (lsubss_ldrop_O1_conf … HL12 … HLK1) -L1 #X #H #HLK2 - elim (lsubss_inv_pair1 … H) -H * #K2 [ | -HWU1 -IHWV1 -HLK2 ] - [ #HK12 #H destruct /3 width=6/ - | #V2 #l0 #_ #_ #_ #_ #H destruct - ] -| /4 width=1/ -| /3 width=1/ -| /3 width=1/ -] -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 deleted file mode 100644 index 5ec33634f..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lsubss.ma +++ /dev/null @@ -1,30 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/static/lsubss_ssta.ma". -include "basic_2/unwind/sstas.ma". - -(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************) - -(* Properties on lenv ref for stratified type assignment ********************) - -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_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_dx … H) -T // /3 width=5/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index ea981eaa5..8a80df07e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -95,7 +95,7 @@ table { } ] [ { "decomposed extended computation" * } { - [ "dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )" "dxprs_lift" + "dxprs_ltpss_dx" + "dxprs_ltpss_sn" + "dxprs_aaa" + "dxpr_lsubss" + "dxprs_dxprs" * ] + [ "dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )" "dxprs_lift" + "dxprs_ltpss_dx" + "dxprs_ltpss_sn" + "dxprs_aaa" + "dxprs_dxprs" * ] } ] [ { "weakly normalizing computation" * } { @@ -163,17 +163,19 @@ table { class "green" [ { "unwind" * } { [ { "iterated stratified static type assignment" * } { - [ "sstas ( ⦃?,?⦄ ⊢ ? •*[?] ? )" "sstas_lift" + "sstas_ltpss_dx" + "sstas_ltpss_sn" + "sstas_aaa" + "sstas_lsubss" + "sstas_sstas" * ] + [ "sstas ( ⦃?,?⦄ ⊢ ? •*[?] ? )" "sstas_lift" + "sstas_ltpss_dx" + "sstas_ltpss_sn" + "sstas_aaa" + "sstas_sstas" * ] } ] } ] class "grass" [ { "static typing" * } { - [ { "local env. ref. for stratified static type assignment" * } { +(* + [ { "local env. ref. for stratified static type assignment" * } { [ "lsubss ( ? •⊑[?] ? )" "lsubss_ldrop" + "lsubss_ssta" + "lsubss_lsubss" * ] } ] +*) [ { "stratified static type assignment" * } { [ "ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )" "ssta_lift" + "ssta_ltpss_dx" + "ssta_ltpss_sn" + "ssta_aaa" + "ssta_ssta" * ] }