From: Ferruccio Guidi Date: Fri, 15 Feb 2013 14:17:58 +0000 (+0000) Subject: we reformulate the extended computation to simplify the proof of its X-Git-Tag: make_still_working~1256 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=18bc3082b332504f60345245e716b62ae628e3a7 we reformulate the extended computation to simplify the proof of its normalization property --- diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index 5b8fd2863..69fca343b 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -74,39 +74,41 @@ define STATS_TEMPLATE $$(STT_$(1)): @printf '\x1B[1;40;37m' - @printf '%-15s %-43s' 'Statistics for:' $(1) + @printf '%-15s %-44s' 'Statistics for:' $(1) @printf '\x1B[0m\n' @printf '\x1B[1;40;35m' @printf '%-8s %6i' Chars $$(S1) - @printf ' %-8s %3i' Pages $$(S2) + @printf ' %-8s %4i' Pages $$(S2) @printf ' %-26s' '' @printf '\x1B[0m\n' @printf '\x1B[1;40;36m' @printf '%-8s %6i' Files $$(S4) - @printf ' %-8s %3i' Sources $$(word 1, $$(S5)) + @printf ' %-8s %4i' Sources $$(word 1, $$(S5)) @printf ' %-7s %4i' Objects $$(word 2, $$(S5)) @printf ' %-11s' '' @printf '\x1B[0m\n' @printf '\x1B[1;40;32m' @printf '%-8s %6i' Theorems $$(P1) - @printf ' %-8s %3i' Lemmas $$(P2) + @printf ' %-8s %4i' Lemmas $$(P2) @printf ' %-7s %4i' Facts $$(P3) @printf ' %-6s %4i' Proofs $$(P4) @printf '\x1B[0m\n' @printf '\x1B[1;40;33m' @printf '%-8s %6i' Declared $$(C1) - @printf ' %-8s %3i' Defined $$(C2) + @printf ' %-8s %4i' Defined $$(C2) @printf ' %-26s' '' @printf '\x1B[0m\n' @printf '\x1B[1;40;31m' @printf '%-8s %6i' Axioms $$(M1) - @printf ' %-8s %3i' Comments $$(M2) + @printf ' %-8s %4i' Comments $$(M2) @printf ' %-7s %4i' Marks $$(M3) @printf ' %-11s' '' @printf '\x1B[0m\n' endef -$(foreach PKG, $(PACKAGES), $(eval $(call STATS_TEMPLATE,$(PKG)))) +ifeq ($(MAKECMDGOALS), stats) + $(foreach PKG, $(PACKAGES), $(eval $(call STATS_TEMPLATE,$(PKG)))) +endif stats: $(STTS) @@ -154,6 +156,8 @@ define SUMMARY_TEMPLATE @printf 'class "number" { 2 } { 4 } { 6 }\n\n' >> $$@ endef -$(foreach PKG, $(PACKAGES), $(eval $(call SUMMARY_TEMPLATE,$(PKG)))) +ifeq ($(MAKECMDGOALS), tbls) + $(foreach PKG, $(PACKAGES), $(eval $(call SUMMARY_TEMPLATE,$(PKG)))) +endif tbls: $(TBLS) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs.ma new file mode 100644 index 000000000..1db0aec2b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs.ma @@ -0,0 +1,46 @@ +(**************************************************************************) +(* ___ *) +(* ||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.ma". +include "basic_2/computation/cprs.ma". + +(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************) + +definition dxprs: ∀h. sd h → lenv → relation term ≝ λh,g,L,T1,T2. + ∃∃T. ⦃h, L⦄ ⊢ T1 •*[g] T & L ⊢ T ➡* T2. + +interpretation "decomposed extended parallel computation (term)" + 'DecomposedXPRedStar h g L T1 T2 = (dxprs h g L T1 T2). + +(* 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 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 dxprs_strap1: ∀h,g,L,T1,T,T2. + ⦃h, L⦄ ⊢ T1 •*➡*[g] T → L ⊢ T ➡ T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2. +#h #g #L #T1 #T #T2 * /3 width=5/ +qed. + +lemma dxprs_strap2: ∀h,g,L,T1,T,T2,l. + ⦃h, L⦄ ⊢ T1 •[g, l+1] T → ⦃h, L⦄ ⊢ T •*➡*[g] T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2. +#h #g #L #T1 #T #T2 #l #HT1 * /3 width=4/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_aaa.ma new file mode 100644 index 000000000..57c72a7b0 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_aaa.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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_aaa.ma". +include "basic_2/computation/cprs_aaa.ma". +include "basic_2/computation/dxprs.ma". + +(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************) + +(* Properties on atomic arity assignment for terms **************************) + +lemma dxprs_aaa: ∀h,g,L,T,A. L ⊢ T ⁝ A → ∀U. ⦃h, L⦄ ⊢ T •*➡*[g] U → L ⊢ U ⁝ A. +#h #g #L #T #A #HT #U * /3 width=5/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_dxprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_dxprs.ma new file mode 100644 index 000000000..772cbd94a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_dxprs.ma @@ -0,0 +1,33 @@ +(**************************************************************************) +(* ___ *) +(* ||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_sstas.ma". +include "basic_2/computation/cprs_cprs.ma". +include "basic_2/computation/dxprs.ma". + +(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************) + +(* Advanced properties ******************************************************) + +lemma dxprs_cprs_trans: ∀h,g,L,T1,T,T2. + ⦃h, L⦄ ⊢ T1 •*➡*[g] T → L ⊢ T ➡* T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2. +#h #g #L #T1 #T #T2 * #T0 #HT10 #HT0 #HT2 +lapply (cprs_trans … HT0 … HT2) -T /2 width=3/ +qed-. + +lemma sstas_dxprs_trans: ∀h,g,L,T1,T,T2. + ⦃h, L⦄ ⊢ T1 •*[g] T → ⦃h, L⦄ ⊢ T •*➡*[g] T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2. +#h #g #L #T1 #T #T2 #HT1 * #T0 #HT0 #HT02 +lapply (sstas_trans … HT1 … HT0) -T /2 width=3/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lift.ma new file mode 100644 index 000000000..431a9f511 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lift.ma @@ -0,0 +1,52 @@ +(**************************************************************************) +(* ___ *) +(* ||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_lift.ma". +include "basic_2/computation/cprs_lift.ma". +include "basic_2/computation/dxprs.ma". + +(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************) + +(* Advanced inversion lemmas *************************************************) + +lemma dxprs_inv_abst1: ∀h,g,a,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓛ{a}V1. T1 •*➡*[g] U2 → + ∃∃V2,T2. L ⊢ V1 ➡* V2 & ⦃h, L.ⓛV1⦄ ⊢ T1 •*➡*[g] T2 & + U2 = ⓛ{a}V2. T2. +#h #g #a #L #V1 #T1 #U2 * #X #H1 #H2 +elim (sstas_inv_bind1 … H1) -H1 #U #HTU1 #H destruct +elim (cprs_inv_abst1 Abst V1 … H2) -H2 #V2 #T2 #HV12 #HUT2 #H destruct /3 width=5/ +qed-. + +(* Advanced properties ******************************************************) + +lemma ssta_cprs_dxprs: ∀h,g,L,T1,T,T2,l. ⦃h, L⦄ ⊢ T1 •[g, l+1] T → + L ⊢ T ➡* T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2. +/3 width=3/ qed. + +(* Relocation properties ****************************************************) + +lemma dxprs_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K → ∀T1,U1. ⇧[d, e] T1 ≡ U1 → + ∀h,g,T2. ⦃h, K⦄ ⊢ T1 •*➡*[g] T2 → ∀U2. ⇧[d, e] T2 ≡ U2 → + ⦃h, L⦄ ⊢ U1 •*➡*[g] U2. +#L #K #d #e #HLK #T1 #U1 #HTU1 #h #g #T2 * #T +elim (lift_total T d e) /3 width=11/ +qed. + +lemma dxprs_inv_lift1: ∀L,K,d,e. ⇩[d, e] L ≡ K → + ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀h,g,U2. ⦃h, L⦄ ⊢ U1 •*➡*[g] U2 → + ∃∃T2. ⇧[d, e] T2 ≡ U2 & ⦃h, K⦄ ⊢ T1 •*➡*[g] T2. +#L #K #d #e #HLK #T1 #U1 #HTU1 #h #g #U2 * #U #HU1 #HU2 +elim (sstas_inv_lift1 … HU1 … HLK … HTU1) -U1 #T #HT1 #HTU +elim (cprs_inv_lift1 … HLK … HTU … HU2) -U -L /3 width=5/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lsubss.ma new file mode 100644 index 000000000..a9a5cd84e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lsubss.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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) /4 width=5/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/xprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/xprs.ma deleted file mode 100644 index 854c5da27..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/xprs.ma +++ /dev/null @@ -1,64 +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". -include "basic_2/reducibility/xpr.ma". -(* -include "basic_2/reducibility/cnf.ma". -*) -(* EXTENDED PARALLEL COMPUTATION ON TERMS ***********************************) - -definition xprs: ∀h. sd h → lenv → relation term ≝ - λh,g,L. TC … (xpr h g L). - -interpretation "extended parallel computation (term)" - 'XPRedStar h g L T1 T2 = (xprs h g L T1 T2). - -(* Basic eliminators ********************************************************) - -lemma xprs_ind: ∀h,g,L,T1. ∀R:predicate term. R T1 → - (∀T,T2. ⦃h, L⦄ ⊢ T1 •➡*[g] T → ⦃h, L⦄ ⊢ T •➡[g] T2 → R T → R T2) → - ∀T2. ⦃h, L⦄ ⊢ T1 •➡*[g] T2 → R T2. -#h #g #L #T1 #R #HT1 #IHT1 #T2 #HT12 -@(TC_star_ind … HT1 IHT1 … HT12) // -qed-. - -lemma xprs_ind_dx: ∀h,g,L,T2. ∀R:predicate term. R T2 → - (∀T1,T. ⦃h, L⦄ ⊢ T1 •➡[g] T → ⦃h, L⦄ ⊢ T •➡*[g] T2 → R T → R T1) → - ∀T1. ⦃h, L⦄ ⊢ T1 •➡*[g] T2 → R T1. -#h #g #L #T2 #R #HT2 #IHT2 #T1 #HT12 -@(TC_star_ind_dx … HT2 IHT2 … HT12) // -qed-. - -(* Basic properties *********************************************************) - -lemma xprs_refl: ∀h,g,L. reflexive … (xprs h g L). -/2 width=1/ qed. - -lemma xprs_strap1: ∀h,g,L,T1,T,T2. - ⦃h, L⦄ ⊢ T1 •➡*[g] T → ⦃h, L⦄ ⊢ T •➡[g] T2 → ⦃h, L⦄ ⊢ T1 •➡*[g] T2. -/2 width=3/ qed. - -lemma xprs_strap2: ∀h,g,L,T1,T,T2. - ⦃h, L⦄ ⊢ T1 •➡[g] T → ⦃h, L⦄ ⊢ T •➡*[g] T2 → ⦃h, L⦄ ⊢ T1 •➡*[g] T2. -/2 width=3/ qed. - -(* Basic inversion lemmas ***************************************************) -(* -axiom xprs_inv_cnf1: ∀L,T,U. L ⊢ T ➡* U → L ⊢ 𝐍⦃T⦄ → T = U. -#L #T #U #H @(xprs_ind_dx … H) -T // -#T0 #T #H1T0 #_ #IHT #H2T0 -lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1/ -qed-. -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/xprs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/xprs_aaa.ma deleted file mode 100644 index 5beb8fe19..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/xprs_aaa.ma +++ /dev/null @@ -1,24 +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/reducibility/xpr_aaa.ma". -include "basic_2/computation/xprs.ma". - -(* EXTENDED PARALLEL COMPUTATION ON TERMS ***********************************) - -(* Properties on atomic arity assignment for terms **************************) - -lemma xprs_aaa: ∀h,g,L,T,A. L ⊢ T ⁝ A → ∀U. ⦃h, L⦄ ⊢ T •➡*[g] U → L ⊢ U ⁝ A. -#h #g #L #T #A #HT #U #H @(xprs_ind … H) -U // /2 width=5/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/xprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/xprs_cprs.ma deleted file mode 100644 index 13a4f8889..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/xprs_cprs.ma +++ /dev/null @@ -1,24 +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/computation/cprs.ma". -include "basic_2/computation/xprs.ma". - -(* EXTENDED PARALLEL COMPUTATION ON TERMS ***********************************) - -(* properties on context sensitive parallel computation for terms ***********) - -lemma cprs_xprs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → ⦃h, L⦄ ⊢ T1 •➡*[g] T2. -#h #g #L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=3/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/xprs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/xprs_lift.ma deleted file mode 100644 index cb151a194..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/xprs_lift.ma +++ /dev/null @@ -1,50 +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/reducibility/xpr_lift.ma". -include "basic_2/computation/cprs.ma". -include "basic_2/computation/xprs.ma". - -(* EXTENDED PARALLEL COMPUTATION ON TERMS ***********************************) - -(* Advanced forward lemmas **************************************************) - -lemma xprs_fwd_abst1: ∀h,g,a,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓛ{a}V1. T1 •➡*[g] U2 → - ∃∃V2,T2. L ⊢ V1 ➡* V2 & U2 = ⓛ{a}V2. T2. -#h #g #a #L #V1 #T1 #U2 #H @(xprs_ind … H) -U2 /2 width=4/ -#U #U2 #_ #HU2 * #V #T #HV1 #H destruct -elim (xpr_inv_abst1 … HU2) -HU2 #V2 #T2 #HV2 #_ #H destruct /3 width=4/ -qed-. - -(* Relocation properties ****************************************************) - -lemma xprs_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K → ∀T1,U1. ⇧[d, e] T1 ≡ U1 → - ∀h,g,T2. ⦃h, K⦄ ⊢ T1 •➡*[g] T2 → ∀U2. ⇧[d, e] T2 ≡ U2 → - ⦃h, L⦄ ⊢ U1 •➡*[g] U2. -#L #K #d #e #HLK #T1 #U1 #HTU1 #h #g #T2 #HT12 @(xprs_ind … HT12) -T2 -[ -HLK #T2 #HT12 - <(lift_mono … HTU1 … HT12) -T1 // -| -HTU1 #T #T2 #_ #HT2 #IHT2 #U2 #HTU2 - elim (lift_total T d e) #U #HTU - lapply (xpr_lift … HLK … HTU … HTU2 … HT2) -T2 -HLK /3 width=3/ -] -qed. - -lemma xprs_inv_lift1: ∀L,K,d,e. ⇩[d, e] L ≡ K → - ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀h,g,U2. ⦃h, L⦄ ⊢ U1 •➡*[g] U2 → - ∃∃T2. ⇧[d, e] T2 ≡ U2 & ⦃h, K⦄ ⊢ T1 •➡*[g] T2. -#L #K #d #e #HLK #T1 #U1 #HTU1 #h #g #U2 #HU12 @(xprs_ind … HU12) -U2 /2 width=3/ --HTU1 #U #U2 #_ #HU2 * #T #HTU #HT1 -elim (xpr_inv_lift1 … HLK … HTU … HU2) -U -HLK /3 width=5/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/xprs_lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/xprs_lsubss.ma deleted file mode 100644 index c883c14f3..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/xprs_lsubss.ma +++ /dev/null @@ -1,27 +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/reducibility/xpr_lsubss.ma". -include "basic_2/computation/xprs.ma". - -(* EXTENDED PARALLEL COMPUTATION ON TERMS ***********************************) - -(* Properties on lenv ref for stratified type assignment ********************) - -lemma lsubss_xprs_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 #H @(xprs_ind … H) -T2 // -#T #T2 #_ #HT2 #IHT1 -lapply (lsubss_xpr_trans … HL12 … HT2) -L2 /2 width=3/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/xprs_xprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/xprs_xprs.ma deleted file mode 100644 index 9593f0550..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/xprs_xprs.ma +++ /dev/null @@ -1,20 +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/computation/xprs.ma". - -(* EXTENDED PARALLEL COMPUTATION ON TERMS ***********************************) - -theorem xprs_trans: ∀h,g,L. transitive … (xprs h g L). -/2 width=3/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma index 2be571525..e39a5764a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma @@ -12,8 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/computation/cprs.ma". -include "basic_2/computation/xprs.ma". +include "basic_2/computation/dxprs.ma". include "basic_2/equivalence/cpcs.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) @@ -24,7 +23,7 @@ inductive snv (h:sh) (g:sd h): lenv → predicate term ≝ | snv_bind: ∀a,I,L,V,T. snv h g L V → snv h g (L.ⓑ{I}V) T → snv h g L (ⓑ{a,I}V.T) | snv_appl: ∀a,L,V,W,W0,T,U,l. snv h g L V → snv h g L T → ⦃h, L⦄ ⊢ V •[g, l + 1] W → L ⊢ W ➡* W0 → - ⦃h, L⦄ ⊢ T •➡*[g] ⓛ{a}W0.U → snv h g L (ⓐV.T) + ⦃h, L⦄ ⊢ T •*➡*[g] ⓛ{a}W0.U → snv h g L (ⓐV.T) | snv_cast: ∀L,W,T,U,l. snv h g L W → snv h g L T → ⦃h, L⦄ ⊢ T •[g, l + 1] U → L ⊢ U ⬌* W → snv h g L (ⓝW.T) . @@ -49,6 +48,19 @@ lemma snv_inv_lref: ∀h,g,L,i. ⦃h, L⦄ ⊩ #i :[g] → ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V & ⦃h, K⦄ ⊩ V :[g]. /2 width=3/ qed-. +fact snv_inv_gref_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀p. X = §p → ⊥. +#h #g #L #X * -L -X +[ #L #k #p #H destruct +| #I #L #K #V #i #_ #_ #p #H destruct +| #a #I #L #V #T #_ #_ #p #H destruct +| #a #L #V #W #W0 #T #U #l #_ #_ #_ #_ #_ #p #H destruct +| #L #W #T #U #l #_ #_ #_ #_ #p #H destruct +] +qed. + +lemma snv_inv_gref: ∀h,g,L,p. ⦃h, L⦄ ⊩ §p :[g] → ⊥. +/2 width=7/ qed-. + fact snv_inv_bind_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀a,I,V,T. X = ⓑ{a,I}V.T → ⦃h, L⦄ ⊩ V :[g] ∧ ⦃h, L.ⓑ{I}V⦄ ⊩ T :[g]. #h #g #L #X * -L -X @@ -67,7 +79,7 @@ lemma snv_inv_bind: ∀h,g,a,I,L,V,T. ⦃h, L⦄ ⊩ ⓑ{a,I}V.T :[g] → fact snv_inv_appl_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀V,T. X = ⓐV.T → ∃∃a,W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] & ⦃h, L⦄ ⊢ V •[g, l + 1] W & L ⊢ W ➡* W0 & - ⦃h, L⦄ ⊢ T •➡*[g] ⓛ{a}W0.U. + ⦃h, L⦄ ⊢ T •*➡*[g] ⓛ{a}W0.U. #h #g #L #X * -L -X [ #L #k #V #T #H destruct | #I #L #K #V0 #i #_ #_ #V #T #H destruct @@ -80,7 +92,7 @@ qed. lemma snv_inv_appl: ∀h,g,L,V,T. ⦃h, L⦄ ⊩ ⓐV.T :[g] → ∃∃a,W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] & ⦃h, L⦄ ⊢ V •[g, l + 1] W & L ⊢ W ➡* W0 & - ⦃h, L⦄ ⊢ T •➡*[g] ⓛ{a}W0.U. + ⦃h, L⦄ ⊢ T •*➡*[g] ⓛ{a}W0.U. /2 width=3/ qed-. fact snv_inv_cast_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀W,T. X = ⓝW.T → 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 3d4761da8..3ebe6e485 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma @@ -13,8 +13,8 @@ (**************************************************************************) include "basic_2/computation/csn_aaa.ma". -include "basic_2/computation/xprs_aaa.ma". -include "basic_2/computation/xprs_cprs.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,8 +28,8 @@ 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 (xprs_aaa h g … HV W0 ?) [ /3 width=3/ ] -W #HW0 - lapply (xprs_aaa … HT … HTU) -HTU #H + lapply (dxprs_aaa h g … HV W0 ?) [ -HTU /2 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/ | #L #W #T #U #l #_ #_ #HTU #HUW * #B #HW * #A #HT diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma index 6d79ef571..ec9be23a4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/computation/xprs_lift.ma". +include "basic_2/computation/dxprs_lift.ma". include "basic_2/equivalence/cpcs_cpcs.ma". include "basic_2/dynamic/snv.ma". @@ -42,7 +42,7 @@ lemma snv_lift: ∀h,g,K,T. ⦃h, K⦄ ⊩ T :[g] → ∀L,d,e. ⇩[d, e] L ≡ elim (lift_total T1 (d+1) e) #U1 #HTU1 @(snv_appl … a … W0 … W1 … U1 l) [ /2 width=4/ | /2 width=4/ | /2 width=9/ | /2 width=9/ ] - @(xprs_lift … HLK … HTU … HT1) /2 width=1/ + @(dxprs_lift … HLK … HTU … HT1) /2 width=1/ | #K #V0 #T #V #l #_ #_ #HTV #HV0 #IHV0 #IHT #L #d #e #HLK #X #H elim (lift_inv_flat1 … H) -H #W0 #U #HVW0 #HTU #H destruct elim (lift_total V d e) #W #HVW @@ -68,7 +68,7 @@ lemma snv_inv_lift: ∀h,g,L,U. ⦃h, L⦄ ⊩ U :[g] → ∀K,d,e. ⇩[d, e] L elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct elim (ssta_inv_lift1 … HW0 … HLK … HVW) -HW0 #V0 #HV0 #HVW0 elim (cprs_inv_lift1 … HLK … HVW0 … HW01) -W0 #V1 #HVW1 #HV01 - elim (xprs_inv_lift1 … HLK … HTU … HU1) -HU1 #X #H #HTU + elim (dxprs_inv_lift1 … HLK … HTU … HU1) -HU1 #X #H #HTU elim (lift_inv_bind2 … H) -H #Y #T1 #HY #HTU1 #H destruct lapply (lift_inj … HY … HVW1) -HY #H destruct /3 width=8/ | #L #W0 #U #W #l #_ #_ #HUW #HW0 #IHW0 #IHU #K #d #e #HLK #X #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma deleted file mode 100644 index cb7e54413..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma +++ /dev/null @@ -1,180 +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_ltpss_dx.ma". -include "basic_2/computation/xprs_lift.ma". -include "basic_2/equivalence/lsubse_ssta.ma". -include "basic_2/equivalence/fpcs_cpcs.ma". -include "basic_2/equivalence/lfpcs_fpcs.ma". -include "basic_2/dynamic/snv_ssta.ma". - -(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) - -(* Properties on context-free parallel reduction for local environments *****) - -fact ssta_ltpr_tpr_aux: ∀h,g,n. ( - ∀L,T2. ♯{L,T2} < n → - ∀T1. L ⊢ T1 ⬌* T2 → ⦃h, L⦄ ⊩ T1 :[g] → ⦃h, L⦄ ⊩ T2 :[g] → - ∀U1,l1. ⦃h, L⦄ ⊢ T1 •[g, l1] U1 → - ∀U2,l2. ⦃h, L⦄ ⊢ T2 •[g, l2] U2 → - L ⊢ U1 ⬌* U2 ∧ l1 = l2 - ) → ( - ∀L,T. ♯{L,T} < n → ⦃h, L⦄ ⊩ T :[g] → - ∀U,l. ⦃h, L⦄ ⊢ T •[g, l + 1] U → ⦃h, L⦄ ⊩ U :[g] - ) → ( - ∀L1,T1. ♯{L1,T1} < n → - ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → - ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L1⦄ ⊩ T1 :[g] → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄ - ) → - ∀L1,T1. ♯{L1,T1} = n → - ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → - ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L1⦄ ⊩ T1 :[g] → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄. -#h #g #n #IH3 #IH2 #IH1 #L1 * * [|||| *] -[ #k #_ #Y #l #H1 #L2 #HL12 #X #H2 #_ -IH3 -IH2 -IH1 - elim (ssta_inv_sort1 … H1) -H1 #Hkl #H destruct - >(tpr_inv_atom1 … H2) -X /4 width=6/ -| #i #Hn #U1 #l #H1 #L2 #HL12 #X #H2 #H3 destruct -IH3 -IH2 - elim (ssta_inv_lref1 … H1) -H1 * #K1 - >(tpr_inv_atom1 … H2) -X - elim (snv_inv_lref … H3) -H3 #I0 #K0 #V0 #H #HV1 - [ #V1 #W1 #HLK1 #HVW1 #HWU1 - lapply (ldrop_mono … H … HLK1) -H #H destruct - lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1 - elim (ltpr_ldrop_conf … HLK1 … HL12) #X #H #HLK2 - elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct - elim (IH1 … HVW1 K2 … HV12) -IH1 -HVW1 -HV12 // -HV1 -HKV1 #W2 #HVW2 #HW12 - lapply (ldrop_fwd_ldrop2 … HLK1) -V1 #H1 - lapply (ldrop_fwd_ldrop2 … HLK2) #H2 - elim (lift_total W2 0 (i+1)) #U2 #HWU2 - lapply (fpcs_lift … HW12 … H1 H2 … HWU1 … HWU2) -H1 -H2 -W1 [ /3 width=1/ ] /3 width=6/ - | #V1 #W1 #l0 #HLK1 #HVW1 #HVU1 #H destruct - lapply (ldrop_mono … H … HLK1) -H #H destruct - lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1 - elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 #X #H #HLK2 - elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct - elim (IH1 … HVW1 K2 … HV12) -IH1 -HVW1 // -HV1 -HK12 -HKV1 #W2 #HVW2 #_ -W1 - elim (lift_total V2 0 (i+1)) #U2 #HVU2 - lapply (tpr_lift … HV12 … HVU1 … HVU2) -V1 /4 width=6/ - ] -| #p #Hn #U1 #l #H1 -IH3 -IH1 - elim (ssta_inv_gref1 … H1) -| #a #I #V1 #T1 #Hn #Y #l #H1 #L2 #HL12 #X #H2 #H3 destruct -IH3 -IH2 - elim (ssta_inv_bind1 … H1) -H1 #U1 #HTU1 #H destruct - elim (snv_inv_bind … H3) -H3 #_ #HT1 - elim (tpr_inv_bind1 … H2) -H2 * - [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct - elim (IH1 … HTU1 (L2.ⓑ{I}V2) … HT10) -IH1 -HTU1 -HT10 // -T1 /3 width=1/ -HL12 #U0 #HTU0 #HU10 - lapply (tps_lsubs_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 [ /2 width=1/ ] #HT02 - elim (ssta_tps_conf … HTU0 … HT02) -T0 #U2 #HTU2 #HU02 - lapply (cpr_intro … U0 … HU02) -HU02 // #HU02 - lapply (fpcs_fpr_strap1 … HU10 (L2.ⓑ{I}V2) U2 ?) [ /2 width=1/ ] -U0 #HU12 - lapply (fpcs_fwd_shift … HU12 a) -HU12 /3 width=3/ - | #T2 #HT12 #HT2 #H1 #H2 destruct - elim (IH1 … HTU1 (L2.ⓓV1) … HT12) -IH1 -HTU1 -HT12 // -T1 [2: /3 width=1/ ] -HL12 #U2 #HTU2 #HU12 - lapply (fpcs_fwd_shift … HU12 true) -HU12 #HU12 - elim (ssta_inv_lift1 … HTU2 … HT2) -T2 [3: /2 width=1/ |2: skip ] #U #HXU #HU2 - lapply (fpcs_fpr_strap1 … HU12 L2 U ?) -HU12 [ /3 width=3/ ] -U2 /2 width=3/ - ] -| #V1 #T1 #Hn #Y #l #H1 #L2 #HL12 #X #H2 #H3 destruct - elim (ssta_inv_appl1 … H1) -H1 #U1 #HTU1 #H destruct - elim (snv_inv_appl … H3) -H3 #a #W1 #W10 #U10 #l0 #HV1 #HT1 #HVW1 #HW10 #HTU10 - elim (tpr_inv_appl1 … H2) -H2 * - [ #V2 #T2 #HV12 #HT12 #H destruct -a -l0 -W1 -W10 -U10 -HV1 -IH3 -IH2 - elim (IH1 … HTU1 … HL12 … HT12 HT1) -IH1 -HTU1 -HL12 -HT12 -HT1 // /3 width=5/ - | #b #V2 #W #T2 #T20 #HV12 #HT20 #H1 #H2 destruct - elim (snv_inv_bind … HT1) -HT1 #HW #HT2 - elim (ssta_inv_bind1 … HTU1) -HTU1 #U2 #HTU2 #H destruct - elim (xprs_fwd_abst1 … HTU10) -HTU10 #W0 #U0 #HW0 #H destruct - lapply (cprs_div … HW10 … HW0) -W0 #HW1 - elim (ssta_fwd_correct … HVW1) (tpr_inv_atom1 … H) -X // -| #I #L1 #K1 #V1 #i #HLK1 #HV1 #L2 #HL12 #X #H #H1 #H2 destruct -IH2 - >(tpr_inv_atom1 … H) -X - elim (ltpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 - elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct - lapply (IH1 … HV1 … HK12 V2 ? ?) -IH1 -HV1 -HK12 /4 width=1/ -HV12 /3 width=4/ -HLK1 /3 width=5/ -| #a #I #L1 #V1 #T1 #HV1 #HT1 #L2 #HL12 #X #H #H1 #H2 destruct -IH2 - elim (tpr_inv_bind1 … H) -H * - [ #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 … 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 (snv_inv_lift … HT2 L2 … HXT2) -T2 // /2 width=1/ - ] -| #a #L1 #V1 #W1 #W10 #T1 #U1 #l #HV1 #HT1 #HVW1 #HW10 #HTU1 #L2 #HL12 #X #H #H1 #H2 destruct - elim (tpr_inv_appl1 … H) -H * - [ #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 … HT1 … HTU1 ?) -IH1 -HT1 // /2 width=1/ #H - elim (snv_inv_bind … H) -H #HW10 #HU1 - elim (IH2 … HVW1 … HL12 … HV12 HV1 ?) -IH2 -HVW1 -HL12 -HV12 -HV1 /2 width=1/ #W2 #HVW2 #HW12 - lapply (fpcs_canc_sn L1 L1 … W10 … HW12) -HW12 /3 width=1/ -W1 #HW102 - @(snv_appl … HV2 HT2 HVW2) -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr_1.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr_1.ma new file mode 100644 index 000000000..4beecd835 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr_1.ma @@ -0,0 +1,136 @@ +(**************************************************************************) +(* ___ *) +(* ||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_ltpss_dx.ma". +include "basic_2/computation/dxprs_lift.ma". +include "basic_2/equivalence/lsubse_ssta.ma". +include "basic_2/equivalence/fpcs_cpcs.ma". +include "basic_2/equivalence/lfpcs_fpcs.ma". +include "basic_2/dynamic/snv_ssta.ma". + +(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) + +(* Properties on context-free parallel reduction for local environments *****) + +fact ssta_ltpr_tpr_aux: ∀h,g,n. ( + ∀L,T2. ♯{L,T2} < n → + ∀T1. L ⊢ T1 ⬌* T2 → ⦃h, L⦄ ⊩ T1 :[g] → ⦃h, L⦄ ⊩ T2 :[g] → + ∀U1,l1. ⦃h, L⦄ ⊢ T1 •[g, l1] U1 → + ∀U2,l2. ⦃h, L⦄ ⊢ T2 •[g, l2] U2 → + L ⊢ U1 ⬌* U2 ∧ l1 = l2 + ) → ( + ∀L,T. ♯{L,T} < n → ⦃h, L⦄ ⊩ T :[g] → + ∀U,l. ⦃h, L⦄ ⊢ T •[g, l + 1] U → ⦃h, L⦄ ⊩ U :[g] + ) → ( + ∀L1,T1. ♯{L1,T1} < n → + ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → + ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L1⦄ ⊩ T1 :[g] → + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄ + ) → + ∀L1,T1. ♯{L1,T1} = n → + ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → + ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L1⦄ ⊩ T1 :[g] → + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄. +#h #g #n #IH3 #IH2 #IH1 #L1 * * [|||| *] +[ #k #_ #Y #l #H1 #L2 #HL12 #X #H2 #_ -IH3 -IH2 -IH1 + elim (ssta_inv_sort1 … H1) -H1 #Hkl #H destruct + >(tpr_inv_atom1 … H2) -X /4 width=6/ +| #i #Hn #U1 #l #H1 #L2 #HL12 #X #H2 #H3 destruct -IH3 -IH2 + elim (ssta_inv_lref1 … H1) -H1 * #K1 + >(tpr_inv_atom1 … H2) -X + elim (snv_inv_lref … H3) -H3 #I0 #K0 #V0 #H #HV1 + [ #V1 #W1 #HLK1 #HVW1 #HWU1 + lapply (ldrop_mono … H … HLK1) -H #H destruct + lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1 + elim (ltpr_ldrop_conf … HLK1 … HL12) #X #H #HLK2 + elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct + elim (IH1 … HVW1 K2 … HV12) -IH1 -HVW1 -HV12 // -HV1 -HKV1 #W2 #HVW2 #HW12 + lapply (ldrop_fwd_ldrop2 … HLK1) -V1 #H1 + lapply (ldrop_fwd_ldrop2 … HLK2) #H2 + elim (lift_total W2 0 (i+1)) #U2 #HWU2 + lapply (fpcs_lift … HW12 … H1 H2 … HWU1 … HWU2) -H1 -H2 -W1 [ /3 width=1/ ] /3 width=6/ + | #V1 #W1 #l0 #HLK1 #HVW1 #HVU1 #H destruct + lapply (ldrop_mono … H … HLK1) -H #H destruct + lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1 + elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 #X #H #HLK2 + elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct + elim (IH1 … HVW1 K2 … HV12) -IH1 -HVW1 // -HV1 -HK12 -HKV1 #W2 #HVW2 #_ -W1 + elim (lift_total V2 0 (i+1)) #U2 #HVU2 + lapply (tpr_lift … HV12 … HVU1 … HVU2) -V1 /4 width=6/ + ] +| #p #Hn #U1 #l #H1 -IH3 -IH1 + elim (ssta_inv_gref1 … H1) +| #a #I #V1 #T1 #Hn #Y #l #H1 #L2 #HL12 #X #H2 #H3 destruct -IH3 -IH2 + elim (ssta_inv_bind1 … H1) -H1 #U1 #HTU1 #H destruct + elim (snv_inv_bind … H3) -H3 #_ #HT1 + elim (tpr_inv_bind1 … H2) -H2 * + [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct + elim (IH1 … HTU1 (L2.ⓑ{I}V2) … HT10) -IH1 -HTU1 -HT10 // -T1 /3 width=1/ -HL12 #U0 #HTU0 #HU10 + lapply (tps_lsubs_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 [ /2 width=1/ ] #HT02 + elim (ssta_tps_conf … HTU0 … HT02) -T0 #U2 #HTU2 #HU02 + lapply (cpr_intro … U0 … HU02) -HU02 // #HU02 + lapply (fpcs_fpr_strap1 … HU10 (L2.ⓑ{I}V2) U2 ?) [ /2 width=1/ ] -U0 #HU12 + lapply (fpcs_fwd_shift … HU12 a) -HU12 /3 width=3/ + | #T2 #HT12 #HT2 #H1 #H2 destruct + elim (IH1 … HTU1 (L2.ⓓV1) … HT12) -IH1 -HTU1 -HT12 // -T1 [2: /3 width=1/ ] -HL12 #U2 #HTU2 #HU12 + lapply (fpcs_fwd_shift … HU12 true) -HU12 #HU12 + elim (ssta_inv_lift1 … HTU2 … HT2) -T2 [3: /2 width=1/ |2: skip ] #U #HXU #HU2 + lapply (fpcs_fpr_strap1 … HU12 L2 U ?) -HU12 [ /3 width=3/ ] -U2 /2 width=3/ + ] +| #V1 #T1 #Hn #Y #l #H1 #L2 #HL12 #X #H2 #H3 destruct + elim (ssta_inv_appl1 … H1) -H1 #U1 #HTU1 #H destruct + elim (snv_inv_appl … H3) -H3 #a #W1 #W10 #U10 #l0 #HV1 #HT1 #HVW1 #HW10 #HTU10 + elim (tpr_inv_appl1 … H2) -H2 * + [ #V2 #T2 #HV12 #HT12 #H destruct -a -l0 -W1 -W10 -U10 -HV1 -IH3 -IH2 + elim (IH1 … HTU1 … HL12 … HT12 HT1) -IH1 -HTU1 -HL12 -HT12 -HT1 // /3 width=5/ + | #b #V2 #W #T2 #T20 #HV12 #HT20 #H1 #H2 destruct + elim (snv_inv_bind … HT1) -HT1 #HW #HT2 + elim (ssta_inv_bind1 … HTU1) -HTU1 #U2 #HTU2 #H destruct + elim (dxprs_inv_abst1 … HTU10) -HTU10 #W0 #U0 #HW0 #_ #H destruct + lapply (cprs_div … HW10 … HW0) -W0 #HW1 + elim (ssta_fwd_correct … HVW1) (tpr_inv_atom1 … H2) -X // +| #i #Hn #H1 #L2 #HL12 #X #H2 destruct -IH2 + elim (snv_inv_lref … H1) -H1 #I #K1 #V1 #HLK1 #HV1 + >(tpr_inv_atom1 … H2) -X + 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/ +| #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 + elim (snv_inv_bind … H1) -H1 #HV1 #HT1 + elim (tpr_inv_bind1 … H2) -H2 * + [ #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 … 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 (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 … 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 + lapply (fpcs_canc_sn L1 L1 … W10 W1 … HW12) -HW12 /3 width=1/ -W10 #HW12 + @(snv_appl … HV2 HT2 HVW2) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/sstas/sstas.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/sstas/sstas.etc index 5954145d9..37d8cdb68 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/sstas/sstas.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/sstas/sstas.etc @@ -12,10 +12,6 @@ (* *) (**************************************************************************) -notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 •* break [ g ] break term 46 T2 )" - non associative with precedence 45 - for @{ 'StaticTypeStar $h $g $L $T1 $T2 }. - include "basic_2/static/ssta.ma". (* ITERATED STRATIFIED STATIC TYPE ASSIGNMENTON TERMS ***********************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xpr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xpr.etc new file mode 100644 index 000000000..1e17654ca --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xpr.etc @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 • ➡ break [ term 46 g ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'XPRed $h $g $L $T1 $T2 }. + +include "basic_2/static/ssta.ma". +include "basic_2/reducibility/cpr.ma". + +(* EXTENDED PARALLEL REDUCTION ON TERMS *************************************) + +inductive xpr (h) (g) (L) (T1) (T2): Prop ≝ +| xpr_cpr : L ⊢ T1 ➡ T2 → xpr h g L T1 T2 +| xpr_ssta: ∀l. ⦃h, L⦄ ⊢ T1 •[g, l + 1] T2 → xpr h g L T1 T2 +. + +interpretation + "extended parallel reduction (term)" + 'XPRed h g L T1 T2 = (xpr h g L T1 T2). + +(* Basic properties *********************************************************) + +lemma xpr_refl: ∀h,g,L. reflexive … (xpr h g L). +/2 width=1/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xpr_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xpr_aaa.etc new file mode 100644 index 000000000..98fe01347 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xpr_aaa.etc @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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_aaa.ma". +include "basic_2/reducibility/cpr_aaa.ma". +include "basic_2/reducibility/xpr.ma". + +(* EXTENDED PARALLEL REDUCTION ON TERMS *************************************) + +(* Properties on atomic arity assignment for terms **************************) + +lemma xpr_aaa: ∀h,g,L,T,A. L ⊢ T ⁝ A → ∀U. ⦃h, L⦄ ⊢ T •➡[g] U → L ⊢ U ⁝ A. +#h #g #L #T #A #HT #U * /2 width=3/ /2 width=6/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xpr_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xpr_lift.etc new file mode 100644 index 000000000..8f5deca51 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xpr_lift.etc @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/cpr_lift.ma". +include "basic_2/reducibility/xpr.ma". + +(* EXTENDED PARALLEL REDUCTION ON TERMS *************************************) + +(* Advanced inversion lemmas ************************************************) + +lemma xpr_inv_abst1: ∀h,g,a,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓛ{a}V1.T1 •➡[g] U2 → + ∃∃V2,T2. L ⊢ V1 ➡ V2 & ⦃h, L. ⓛV1⦄ ⊢ T1 •➡[g] T2 & + U2 = ⓛ{a}V2. T2. +#h #g #a #L #V1 #T1 #U2 * +[ #H elim (cpr_inv_abst1 … H Abst V1) /3 width=5/ +| #l #H elim (ssta_inv_bind1 … H) /3 width=5/ +] +qed-. + +(* Relocation properties ****************************************************) + +lemma xpr_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K → + ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀T2,U2. ⇧[d, e] T2 ≡ U2 → + ∀h,g. ⦃h, K⦄ ⊢ T1 •➡[g] T2 → ⦃h, L⦄ ⊢ U1 •➡[g] U2. +#L #K #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #h #g * +/3 width=9/ /3 width=10/ +qed. + +lemma xpr_inv_lift1: ∀L,K,d,e. ⇩[d, e] L ≡ K → + ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀h,g,U2. ⦃h, L⦄ ⊢ U1 •➡[g] U2 → + ∃∃T2. ⇧[d, e] T2 ≡ U2 & ⦃h, K⦄ ⊢ T1 •➡[g] T2. +#L #K #d #e #HLK #T1 #U1 #HTU1 #h #g #U2 * [ #HU12 | #l #HU12 ] +[ elim (cpr_inv_lift1 … HLK … HTU1 … HU12) -L -U1 /3 width=3/ +| elim (ssta_inv_lift1 … HU12 … HLK … HTU1) -L -U1 /3 width=4/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xpr_lsubss.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xpr_lsubss.etc new file mode 100644 index 000000000..bc66cd2cd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xpr_lsubss.etc @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/xpr.ma". + +(* EXTENDED PARALLEL REDUCTION ON TERMS *************************************) + +(* Properties on lenv ref for stratified type assignment ********************) + +lemma lsubss_xpr_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 * [ | #l ] #HT12 +[ lapply (lsubss_fwd_lsubs2 … HL12) -HL12 /3 width=3/ +| /3 width=4/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs.etc new file mode 100644 index 000000000..bffc4e735 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs.etc @@ -0,0 +1,72 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 • ➡ * break [ term 46 g ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'XPRedStar $h $g $L $T1 $T2 }. + +notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ • ⬊ * break [ term 46 g ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'XSN $h $g $L $T }. + +include "basic_2/static/lsubss.ma". +include "basic_2/reducibility/xpr.ma". +(* +include "basic_2/reducibility/cnf.ma". +*) +(* EXTENDED PARALLEL COMPUTATION ON TERMS ***********************************) + +definition xprs: ∀h. sd h → lenv → relation term ≝ + λh,g,L. TC … (xpr h g L). + +interpretation "extended parallel computation (term)" + 'XPRedStar h g L T1 T2 = (xprs h g L T1 T2). + +(* Basic eliminators ********************************************************) + +lemma xprs_ind: ∀h,g,L,T1. ∀R:predicate term. R T1 → + (∀T,T2. ⦃h, L⦄ ⊢ T1 •➡*[g] T → ⦃h, L⦄ ⊢ T •➡[g] T2 → R T → R T2) → + ∀T2. ⦃h, L⦄ ⊢ T1 •➡*[g] T2 → R T2. +#h #g #L #T1 #R #HT1 #IHT1 #T2 #HT12 +@(TC_star_ind … HT1 IHT1 … HT12) // +qed-. + +lemma xprs_ind_dx: ∀h,g,L,T2. ∀R:predicate term. R T2 → + (∀T1,T. ⦃h, L⦄ ⊢ T1 •➡[g] T → ⦃h, L⦄ ⊢ T •➡*[g] T2 → R T → R T1) → + ∀T1. ⦃h, L⦄ ⊢ T1 •➡*[g] T2 → R T1. +#h #g #L #T2 #R #HT2 #IHT2 #T1 #HT12 +@(TC_star_ind_dx … HT2 IHT2 … HT12) // +qed-. + +(* Basic properties *********************************************************) + +lemma xprs_refl: ∀h,g,L. reflexive … (xprs h g L). +/2 width=1/ qed. + +lemma xprs_strap1: ∀h,g,L,T1,T,T2. + ⦃h, L⦄ ⊢ T1 •➡*[g] T → ⦃h, L⦄ ⊢ T •➡[g] T2 → ⦃h, L⦄ ⊢ T1 •➡*[g] T2. +/2 width=3/ qed. + +lemma xprs_strap2: ∀h,g,L,T1,T,T2. + ⦃h, L⦄ ⊢ T1 •➡[g] T → ⦃h, L⦄ ⊢ T •➡*[g] T2 → ⦃h, L⦄ ⊢ T1 •➡*[g] T2. +/2 width=3/ qed. + +(* Basic inversion lemmas ***************************************************) +(* +axiom xprs_inv_cnf1: ∀L,T,U. L ⊢ T ➡* U → L ⊢ 𝐍⦃T⦄ → T = U. +#L #T #U #H @(xprs_ind_dx … H) -T // +#T0 #T #H1T0 #_ #IHT #H2T0 +lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1/ +qed-. +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_aaa.etc new file mode 100644 index 000000000..5beb8fe19 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_aaa.etc @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/xpr_aaa.ma". +include "basic_2/computation/xprs.ma". + +(* EXTENDED PARALLEL COMPUTATION ON TERMS ***********************************) + +(* Properties on atomic arity assignment for terms **************************) + +lemma xprs_aaa: ∀h,g,L,T,A. L ⊢ T ⁝ A → ∀U. ⦃h, L⦄ ⊢ T •➡*[g] U → L ⊢ U ⁝ A. +#h #g #L #T #A #HT #U #H @(xprs_ind … H) -U // /2 width=5/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_cprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_cprs.etc new file mode 100644 index 000000000..13a4f8889 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_cprs.etc @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/cprs.ma". +include "basic_2/computation/xprs.ma". + +(* EXTENDED PARALLEL COMPUTATION ON TERMS ***********************************) + +(* properties on context sensitive parallel computation for terms ***********) + +lemma cprs_xprs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → ⦃h, L⦄ ⊢ T1 •➡*[g] T2. +#h #g #L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=3/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_lift.etc new file mode 100644 index 000000000..cb151a194 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_lift.etc @@ -0,0 +1,50 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/xpr_lift.ma". +include "basic_2/computation/cprs.ma". +include "basic_2/computation/xprs.ma". + +(* EXTENDED PARALLEL COMPUTATION ON TERMS ***********************************) + +(* Advanced forward lemmas **************************************************) + +lemma xprs_fwd_abst1: ∀h,g,a,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓛ{a}V1. T1 •➡*[g] U2 → + ∃∃V2,T2. L ⊢ V1 ➡* V2 & U2 = ⓛ{a}V2. T2. +#h #g #a #L #V1 #T1 #U2 #H @(xprs_ind … H) -U2 /2 width=4/ +#U #U2 #_ #HU2 * #V #T #HV1 #H destruct +elim (xpr_inv_abst1 … HU2) -HU2 #V2 #T2 #HV2 #_ #H destruct /3 width=4/ +qed-. + +(* Relocation properties ****************************************************) + +lemma xprs_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K → ∀T1,U1. ⇧[d, e] T1 ≡ U1 → + ∀h,g,T2. ⦃h, K⦄ ⊢ T1 •➡*[g] T2 → ∀U2. ⇧[d, e] T2 ≡ U2 → + ⦃h, L⦄ ⊢ U1 •➡*[g] U2. +#L #K #d #e #HLK #T1 #U1 #HTU1 #h #g #T2 #HT12 @(xprs_ind … HT12) -T2 +[ -HLK #T2 #HT12 + <(lift_mono … HTU1 … HT12) -T1 // +| -HTU1 #T #T2 #_ #HT2 #IHT2 #U2 #HTU2 + elim (lift_total T d e) #U #HTU + lapply (xpr_lift … HLK … HTU … HTU2 … HT2) -T2 -HLK /3 width=3/ +] +qed. + +lemma xprs_inv_lift1: ∀L,K,d,e. ⇩[d, e] L ≡ K → + ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀h,g,U2. ⦃h, L⦄ ⊢ U1 •➡*[g] U2 → + ∃∃T2. ⇧[d, e] T2 ≡ U2 & ⦃h, K⦄ ⊢ T1 •➡*[g] T2. +#L #K #d #e #HLK #T1 #U1 #HTU1 #h #g #U2 #HU12 @(xprs_ind … HU12) -U2 /2 width=3/ +-HTU1 #U #U2 #_ #HU2 * #T #HTU #HT1 +elim (xpr_inv_lift1 … HLK … HTU … HU2) -U -HLK /3 width=5/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_lsubss.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_lsubss.etc new file mode 100644 index 000000000..c883c14f3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_lsubss.etc @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/xpr_lsubss.ma". +include "basic_2/computation/xprs.ma". + +(* EXTENDED PARALLEL COMPUTATION ON TERMS ***********************************) + +(* Properties on lenv ref for stratified type assignment ********************) + +lemma lsubss_xprs_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 #H @(xprs_ind … H) -T2 // +#T #T2 #_ #HT2 #IHT1 +lapply (lsubss_xpr_trans … HL12 … HT2) -L2 /2 width=3/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_xprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_xprs.etc new file mode 100644 index 000000000..9593f0550 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/xpr/xprs_xprs.etc @@ -0,0 +1,20 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/xprs.ma". + +(* EXTENDED PARALLEL COMPUTATION ON TERMS ***********************************) + +theorem xprs_trans: ∀h,g,L. transitive … (xprs h g L). +/2 width=3/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation.ma index e378dc719..71e9fae60 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation.ma @@ -264,6 +264,10 @@ notation "hvbox( h ⊢ break term 46 L1 • ⊑ [ term 46 g ] break term 46 L2 ) (* Unwind *******************************************************************) +notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 •* break [ term 46 g ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'StaticTypeStar $h $g $L $T1 $T2 }. + notation "hvbox( L1 ⊢ ⧫ * break term 46 T ≡ break term 46 L2 )" non associative with precedence 45 for @{ 'Unwind $L1 $T $L2 }. @@ -336,10 +340,6 @@ notation "hvbox( ⦃ term 46 L1 ⦄ ➡ ➡ break ⦃ term 46 L2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPRedAlt $L1 $L2 }. -notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 • ➡ break [ term 46 g ] break term 46 T2 )" - non associative with precedence 45 - for @{ 'XPRed $h $g $L $T1 $T2 }. - (* Computation **************************************************************) notation "hvbox( T1 ➡ * break term 46 T2 )" @@ -394,13 +394,13 @@ notation "hvbox( T1 ⊑ break [ term 46 R ] break term 46 T2 )" non associative with precedence 45 for @{ 'CrSubEq $T1 $R $T2 }. -notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 • ➡ * break [ term 46 g ] break term 46 T2 )" +notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 • * ➡ * break [ term 46 g ] break term 46 T2 )" non associative with precedence 45 - for @{ 'XPRedStar $h $g $L $T1 $T2 }. + for @{ 'DecomposedXPRedStar $h $g $L $T1 $T2 }. -notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ • ⬊ * break [ term 46 g ] break term 46 T2 )" +notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ • * ⬊ * break [ term 46 g ] break term 46 T2 )" non associative with precedence 45 - for @{ 'XSN $h $g $L $T }. + for @{ 'DecomposedXSN $h $g $L $T }. (* Conversion ***************************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr.ma deleted file mode 100644 index 7375349ef..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr.ma +++ /dev/null @@ -1,32 +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". -include "basic_2/reducibility/cpr.ma". - -(* EXTENDED PARALLEL REDUCTION ON TERMS *************************************) - -inductive xpr (h) (g) (L) (T1) (T2): Prop ≝ -| xpr_cpr : L ⊢ T1 ➡ T2 → xpr h g L T1 T2 -| xpr_ssta: ∀l. ⦃h, L⦄ ⊢ T1 •[g, l + 1] T2 → xpr h g L T1 T2 -. - -interpretation - "extended parallel reduction (term)" - 'XPRed h g L T1 T2 = (xpr h g L T1 T2). - -(* Basic properties *********************************************************) - -lemma xpr_refl: ∀h,g,L. reflexive … (xpr h g L). -/2 width=1/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr_aaa.ma deleted file mode 100644 index 98fe01347..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr_aaa.ma +++ /dev/null @@ -1,25 +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_aaa.ma". -include "basic_2/reducibility/cpr_aaa.ma". -include "basic_2/reducibility/xpr.ma". - -(* EXTENDED PARALLEL REDUCTION ON TERMS *************************************) - -(* Properties on atomic arity assignment for terms **************************) - -lemma xpr_aaa: ∀h,g,L,T,A. L ⊢ T ⁝ A → ∀U. ⦃h, L⦄ ⊢ T •➡[g] U → L ⊢ U ⁝ A. -#h #g #L #T #A #HT #U * /2 width=3/ /2 width=6/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr_lift.ma deleted file mode 100644 index 8f5deca51..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr_lift.ma +++ /dev/null @@ -1,48 +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/reducibility/cpr_lift.ma". -include "basic_2/reducibility/xpr.ma". - -(* EXTENDED PARALLEL REDUCTION ON TERMS *************************************) - -(* Advanced inversion lemmas ************************************************) - -lemma xpr_inv_abst1: ∀h,g,a,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓛ{a}V1.T1 •➡[g] U2 → - ∃∃V2,T2. L ⊢ V1 ➡ V2 & ⦃h, L. ⓛV1⦄ ⊢ T1 •➡[g] T2 & - U2 = ⓛ{a}V2. T2. -#h #g #a #L #V1 #T1 #U2 * -[ #H elim (cpr_inv_abst1 … H Abst V1) /3 width=5/ -| #l #H elim (ssta_inv_bind1 … H) /3 width=5/ -] -qed-. - -(* Relocation properties ****************************************************) - -lemma xpr_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K → - ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀T2,U2. ⇧[d, e] T2 ≡ U2 → - ∀h,g. ⦃h, K⦄ ⊢ T1 •➡[g] T2 → ⦃h, L⦄ ⊢ U1 •➡[g] U2. -#L #K #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #h #g * -/3 width=9/ /3 width=10/ -qed. - -lemma xpr_inv_lift1: ∀L,K,d,e. ⇩[d, e] L ≡ K → - ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀h,g,U2. ⦃h, L⦄ ⊢ U1 •➡[g] U2 → - ∃∃T2. ⇧[d, e] T2 ≡ U2 & ⦃h, K⦄ ⊢ T1 •➡[g] T2. -#L #K #d #e #HLK #T1 #U1 #HTU1 #h #g #U2 * [ #HU12 | #l #HU12 ] -[ elim (cpr_inv_lift1 … HLK … HTU1 … HU12) -L -U1 /3 width=3/ -| elim (ssta_inv_lift1 … HU12 … HLK … HTU1) -L -U1 /3 width=4/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr_lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr_lsubss.ma deleted file mode 100644 index bc66cd2cd..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr_lsubss.ma +++ /dev/null @@ -1,28 +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/reducibility/xpr.ma". - -(* EXTENDED PARALLEL REDUCTION ON TERMS *************************************) - -(* Properties on lenv ref for stratified type assignment ********************) - -lemma lsubss_xpr_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 * [ | #l ] #HT12 -[ lapply (lsubss_fwd_lsubs2 … HL12) -HL12 /3 width=3/ -| /3 width=4/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_aaa.ma index d14083a45..01841483c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_aaa.ma @@ -38,4 +38,3 @@ lemma ssta_aaa: ∀h,g,L,T,A. L ⊢ T ⁝ A → ∀U,l. ⦃h, L⦄ ⊢ T •[g, lapply (ssta_inv_cast1 … H) -H /2 width=2/ ] qed. - diff --git a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas.ma b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas.ma new file mode 100644 index 000000000..3928e49cc --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas.ma @@ -0,0 +1,84 @@ +(**************************************************************************) +(* ___ *) +(* ||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". + +(* 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. + +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/ +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/ +] +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-. + +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/ +] +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/ +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 new file mode 100644 index 000000000..fbf485841 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_aaa.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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_aaa.ma". +include "basic_2/unwind/sstas.ma". + +(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************) + +(* Properties on atomic arity assignment for terms **************************) + +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/ +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 new file mode 100644 index 000000000..7273963a3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lift.ma @@ -0,0 +1,53 @@ +(**************************************************************************) +(* ___ *) +(* ||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/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/ +| #T0 #U0 #l0 #HTU0 #_ #IHU01 #L2 #d #e #HL21 #T2 #HT02 #U2 #HU12 + elim (lift_total U0 d e) /3 width=10/ +] +qed. + +(* Inversion lemmas on relocation *******************************************) + +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/ +] +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 new file mode 100644 index 000000000..ba2910da8 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lsubss.ma @@ -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_alt … H) -T /3 width=4/ /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/ +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 new file mode 100644 index 000000000..84f2d805b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_ltpss_dx.ma @@ -0,0 +1,55 @@ +(**************************************************************************) +(* ___ *) +(* ||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_ltpss_dx.ma". +include "basic_2/unwind/sstas.ma". + +(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************) + +(* Properties about dx parallel unfold **************************************) + +lemma sstas_ltpss_dx_tpss_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. +#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/ +] +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. + +lemma sstas_ltpss_dx_conf: ∀h,g,L1,T,U1. ⦃h, L1⦄ ⊢ T •*[g] U1 → + ∀L2,d,e. L1 ▶* [d, e] L2 → + ∃∃U2. ⦃h, L2⦄ ⊢ T •*[g] U2 & L2 ⊢ U1 ▶* [d, e] U2. +/2 width=5/ qed. + +lemma sstas_tpss_conf: ∀h,g,L,T1,U1. ⦃h, L⦄ ⊢ T1 •*[g] U1 → + ∀T2,d,e. L ⊢ T1 ▶* [d, e] T2 → + ∃∃U2. ⦃h, L⦄ ⊢ T2 •*[g] U2 & L ⊢ U1 ▶* [d, e] U2. +/2 width=5/ qed. + +lemma sstas_tps_conf: ∀h,g,L,T1,U1. ⦃h, L⦄ ⊢ T1 •*[g] U1 → + ∀T2,d,e. L ⊢ T1 ▶ [d, e] T2 → + ∃∃U2. ⦃h, L⦄ ⊢ T2 •*[g] U2 & L ⊢ U1 ▶* [d, e] U2. +/2 width=5/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_ltpss_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_ltpss_sn.ma new file mode 100644 index 000000000..0a00fd9d8 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_ltpss_sn.ma @@ -0,0 +1,53 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unfold/ltpss_sn_alt.ma". +include "basic_2/unwind/sstas_ltpss_dx.ma". + +(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS ************************) + +(* Properties about sn parallel unfold *****************************************) + +lemma sstas_ltpss_sn_conf: ∀h,g,L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 → + ∀T,U1. ⦃h, L1⦄ ⊢ T •*[g] U1 → + ∃∃U2. L1 ⊢ U1 ▶* [d, e] U2 & ⦃h, L2⦄ ⊢ T •*[g] U2. +#h #g #L1 #L2 #d #e #H +lapply (ltpss_sn_ltpssa … H) -H #H @(ltpssa_ind … H) -L2 /2 width=3/ +#L #L2 #HL1 #HL2 #IHL1 #T #U1 #H1 +lapply (ltpssa_ltpss_sn … HL1) -HL1 #HL1 +lapply (ltpss_sn_dx_trans_eq … HL1 … HL2) -HL1 #HL12 +elim (IHL1 … H1) -IHL1 -H1 #U #HU1 #HTU +elim (sstas_ltpss_dx_conf … HTU … HL2) -HTU -HL2 #U2 #H2 #HU2 +lapply (ltpss_sn_tpss_trans_eq … HU2 … HL12) -HU2 -HL12 #HU2 +lapply (tpss_trans_eq … HU1 HU2) -U /2 width=3/ +qed. + +lemma sstas_ltpss_sn_tpss_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 & + L1 ⊢ U1 ▶* [d, e] U2. +#h #g #L1 #T1 #U1 #HTU1 #L2 #d #e #HL12 #T2 #HT12 +elim (sstas_ltpss_sn_conf … HL12 … HTU1) -HTU1 #U #HU1 #HT1U +elim (sstas_tpss_conf … HT1U … HT12) -T1 #U2 #HTU2 #HU2 +lapply (ltpss_sn_tpss_trans_eq … HU2 … HL12) -HU2 -HL12 #HU2 +lapply (tpss_trans_eq … HU1 HU2) -U /2 width=3/ +qed. + +lemma sstas_ltpss_sn_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 & + L1 ⊢ U1 ▶* [d, e] U2. +/3 width=3/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_sstas.ma b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_sstas.ma new file mode 100644 index 000000000..e7e99c001 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_sstas.ma @@ -0,0 +1,52 @@ +(**************************************************************************) +(* ___ *) +(* ||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_ssta.ma". +include "basic_2/unwind/sstas.ma". + +(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************) + +(* Advanced inversion lemmas ************************************************) + +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 // +#T0 #U0 #l0 #HTU0 #_ #_ #T1 #HT01 +elim (ssta_mono … HTU0 … HT01)