From: Ferruccio Guidi Date: Thu, 19 Apr 2012 13:06:00 +0000 (+0000) Subject: - firs theorems on native type assignment X-Git-Tag: make_still_working~1809 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=de64015de66a48373ade6cab7508d8f8e2c43af9;p=helm.git - firs theorems on native type assignment - we removed iterated unfold on local environments since transitivity of this unfold is not needed so far --- diff --git a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt index caa897dec..92bd9860d 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt +++ b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt @@ -242,11 +242,7 @@ ty3/dec ty3_inference ty3/fsubst0 ty3_fsubst0 ty3/fsubst0 ty3_csubst0 ty3/fsubst0 ty3_subst0 -ty3/fwd ty3_gen_sort -ty3/fwd ty3_gen_lref -ty3/fwd ty3_gen_bind ty3/fwd ty3_gen_appl -ty3/fwd ty3_gen_cast ty3/fwd tys3_gen_nil ty3/fwd tys3_gen_cons ty3/fwd_nf2 ty3_gen_appl_nf2 @@ -271,12 +267,8 @@ ty3/pr3_props ty3_tred ty3/pr3_props ty3_sconv_pc3 ty3/pr3_props ty3_sred_back ty3/pr3_props ty3_sconv -ty3/props ty3_lift -ty3/props ty3_correct ty3/props ty3_unique ty3/props ty3_gen_abst_abst -ty3/props ty3_typecheck -ty3/props ty3_getl_subst0 ty3/sty0 ty3_sty0 ty3/subst1 ty3_gen_cabbr ty3/subst1 ty3_gen_cvoid diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcpr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcpr.ma index bb7896c30..14bcfd5c4 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcpr.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/reducibility/ltpr_tps.ma". -include "basic_2/reducibility/cpr_ltpsss.ma". +include "basic_2/reducibility/cpr_ltpss.ma". include "basic_2/reducibility/lcpr.ma". include "basic_2/computation/cprs.ma". diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_lcpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_lcpcs.ma index cc26a5647..876161bd2 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_lcpcs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_lcpcs.ma @@ -44,7 +44,7 @@ theorem lcpcs_trans: ∀L1,L. L1 ⊢ ⬌* L → ∀L2. L ⊢ ⬌* L2 → L1 ⊢ /2 width=3/ qed. theorem lcpcs_canc_sn: ∀L,L1,L2. L ⊢ ⬌* L1 → L ⊢ ⬌* L2 → L1 ⊢ ⬌* L2. -/3 width=3/ qed. +/3 width=3 by lcpcs_trans, lcprs_comm/ qed. theorem lcpcs_canc_dx: ∀L,L1,L2. L1 ⊢ ⬌* L → L2 ⊢ ⬌* L → L1 ⊢ ⬌* L2. -/3 width=3/ qed. +/3 width=3 by lcpcs_trans, lcprs_comm/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/aaa_ltpsss.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/aaa_ltpsss.etc new file mode 100644 index 000000000..e3d048809 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/aaa_ltpsss.etc @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||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/ltpsss.ma". +include "basic_2/static/aaa_ltpss.ma". + +(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) + +(* Properties about iterated parallel unfold ********************************) + +lemma aaa_ltpsss_conf: ∀L1,T,A. L1 ⊢ T ÷ A → + ∀L2,d,e. L1 [d, e] ▶** L2 → L2 ⊢ T ÷ A. +#L1 #T #A #HT #L2 #d #e #HL12 +@(TC_Conf3 … (λL,A. L ⊢ T ÷ A) … HT ? HL12) /2 width=5/ +qed. + +lemma aaa_ltpsss_tpss_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. L1 [d, e] ▶** L2 → + ∀T2. L2 ⊢ T1 [d, e] ▶* T2 → L2 ⊢ T2 ÷ A. +/3 width=5/ qed. + +lemma aaa_ltpsss_tps_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. L1 [d, e] ▶** L2 → + ∀T2. L2 ⊢ T1 [d, e] ▶ T2 → L2 ⊢ T2 ÷ A. +/3 width=5/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/cpr_ltpsss.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/cpr_ltpsss.etc new file mode 100644 index 000000000..0890e462b --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/cpr_ltpsss.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/unfold/ltpsss.ma". +include "basic_2/reducibility/cpr_ltpss.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) + +(* Properties on iterated partial unfold on local environments **************) + +lemma ltpsss_cpr_trans: ∀L1,L2,d,e. L1 [d, e] ▶** L2 → + ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡ T2. +#L1 #L2 #d #e #HL12 #T1 #T2 #HT12 @(ltpsss_ind_dx … HL12) -L1 // /2 width=5/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/cprs_lcpr.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/cprs_lcpr.etc new file mode 100644 index 000000000..bb7896c30 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/cprs_lcpr.etc @@ -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/reducibility/ltpr_tps.ma". +include "basic_2/reducibility/cpr_ltpsss.ma". +include "basic_2/reducibility/lcpr.ma". +include "basic_2/computation/cprs.ma". + +(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) + +(* Properties concerning context-sensitive parallel reduction on lenv's *****) + +lemma ltpr_tpss_trans: ∀L1,L2. L1 ➡ L2 → ∀T1,T2,d,e. L2 ⊢ T1 [d, e] ▶* T2 → + ∃∃T. L1 ⊢ T1 [d, e] ▶* T & L1 ⊢ T ➡* T2. +#L1 #L2 #HL12 #T1 #T2 #d #e #H @(tpss_ind … H) -T2 +[ /2 width=3/ +| #T #T2 #_ #HT2 * #T0 #HT10 #HT0 + elim (ltpr_tps_trans … HT2 … HL12) -L2 #T3 #HT3 #HT32 + @(ex2_1_intro … HT10) -T1 (**) (* explicit constructors *) + @(cprs_strap1 … T3 …) /2 width=1/ -HT32 + @(cprs_strap1 … HT0) -HT0 /3 width=3/ +] +qed. + +(* Basic_1: was just: pr3_pr0_pr2_t *) +lemma ltpr_cpr_trans: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡* T2. +#L1 #L2 #HL12 #T1 #T2 * #T #HT1 +<(ltpr_fwd_length … HL12) #HT2 +elim (ltpr_tpss_trans … HL12 … HT2) -L2 /3 width=3/ +qed. + +(* Basic_1: was just: pr3_pr2_pr2_t *) +lemma lcpr_cpr_trans: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡* T2. +#L1 #L2 * /3 width=7/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr.etc new file mode 100644 index 000000000..4d8a341bc --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr.etc @@ -0,0 +1,37 @@ +(**************************************************************************) +(* ___ *) +(* ||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/ltpsss.ma". +include "basic_2/reducibility/ltpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************) + +definition lcpr: relation lenv ≝ + λL1,L2. ∃∃L. L1 ➡ L & L [0, |L|] ▶** L2 +. + +interpretation + "context-sensitive parallel reduction (environment)" + 'CPRed L1 L2 = (lcpr L1 L2). + +(* Basic properties *********************************************************) + +lemma lcpr_refl: ∀L. L ⊢ ➡ L. +/2 width=3/ qed. + +(* Basic inversion lemmas ***************************************************) + +lemma lcpr_inv_atom1: ∀L2. ⋆ ⊢ ➡ L2 → L2 = ⋆. +#L2 * #L #HL >(ltpr_inv_atom1 … HL) -HL #HL2 >(ltpsss_inv_atom1 … HL2) -HL2 // +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_aaa.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_aaa.etc new file mode 100644 index 000000000..77f384e58 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_aaa.etc @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||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/aaa_ltpsss.ma". +include "basic_2/reducibility/ltpr_aaa.ma". +include "basic_2/reducibility/cpr.ma". +include "basic_2/reducibility/lcpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************) + +(* Properties about atomic arity assignment on terms ************************) + +lemma aaa_lcpr_conf: ∀L1,T,A. L1 ⊢ T ÷ A → ∀L2. L1 ⊢ ➡ L2 → L2 ⊢ T ÷ A. +#L1 #T #A #HT #L2 * /3 width=5/ +qed. + +lemma aaa_cpr_conf: ∀L,T1,A. L ⊢ T1 ÷ A → ∀T2. L ⊢ T1 ➡ T2 → L ⊢ T2 ÷ A. +#L #T1 #A #HT1 #T2 * /3 width=5/ +qed. + +lemma aaa_lcpr_cpr_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2. L1 ⊢ ➡ L2 → + ∀T2. L2 ⊢ T1 ➡ T2 → L2 ⊢ T2 ÷ A. +/3 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_cpr.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_cpr.etc new file mode 100644 index 000000000..3d833fc02 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_cpr.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/unfold/ltpsss_ltpsss.ma". +include "basic_2/reducibility/cpr.ma". +include "basic_2/reducibility/lcpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************) + +(* Advanced properties ****************************************************) + +lemma lcpr_pair: ∀L1,L2. L1 ⊢ ➡ L2 → ∀V1,V2. L2 ⊢ V1 ➡ V2 → + ∀I. L1. ⓑ{I} V1 ⊢ ➡ L2. ⓑ{I} V2. +#L1 #L2 * #L #HL1 #HL2 #V1 #V2 * +<(ltpsss_fwd_length … HL2) /4 width=5/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_lcpr.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_lcpr.etc new file mode 100644 index 000000000..5d7e4739e --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_lcpr.etc @@ -0,0 +1,40 @@ +(**************************************************************************) +(* ___ *) +(* ||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/ltpsss_ltpsss.ma". +include "basic_2/reducibility/ltpr_ltpsss.ma". +include "basic_2/reducibility/ltpr_ltpr.ma". +include "basic_2/reducibility/lcpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ***************) + +(* Main properties **********************************************************) + +theorem lcpr_conf: ∀L0,L1,L2. L0 ⊢ ➡ L1 → L0 ⊢ ➡ L2 → + ∃∃L. L1 ⊢ ➡ L & L2 ⊢ ➡ L. +#K0 #L1 #L2 * #K1 #HK01 #HKL1 * #K2 #HK02 #HKL2 +lapply (ltpr_fwd_length … HK01) #H +>(ltpr_fwd_length … HK02) in H; #H +elim (ltpr_conf … HK01 … HK02) -K0 #K #HK1 #HK2 +lapply (ltpsss_fwd_length … HKL1) #H1 +lapply (ltpsss_fwd_length … HKL2) #H2 +>H1 in HKL1 H; -H1 #HKL1 +>H2 in HKL2; -H2 #HKL2 #H +elim (ltpr_ltpsss_conf … HKL1 … HK1) -K1 #K1 #HK1 #HLK1 +elim (ltpr_ltpsss_conf … HKL2 … HK2) -K2 #K2 #HK2 #HLK2 +elim (ltpsss_conf … HK1 … HK2) -K #K #HK1 #HK2 +lapply (ltpr_fwd_length … HLK1) #H1 +lapply (ltpr_fwd_length … HLK2) #H2 +/3 width=5/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpr_ltpsss.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpr_ltpsss.etc new file mode 100644 index 000000000..d0c29e726 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpr_ltpsss.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/unfold/ltpsss.ma". +include "basic_2/reducibility/ltpr_ltpss.ma". + +(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) + +(* Properties on iterated parallel unfold on local environments *************) + +lemma ltpr_ltpsss_conf: ∀L1,K1,d,e. L1 [d, e] ▶** K1 → ∀L2. L1 ➡ L2 → + ∃∃K2. L2 [d, e] ▶** K2 & K1 ➡ K2. +#L1 #K1 #d #e #H @(ltpsss_ind … H) -K1 /2 width=3/ +#K #K1 #_ #HK1 #IHK #L2 #HL12 +elim (IHK … HL12) -L1 #K2 #HLK2 #HK2 +elim (ltpr_ltpss_conf … HK1 … HK2) -K /3 width=3/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss.etc new file mode 100644 index 000000000..58fb3e20b --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss.etc @@ -0,0 +1,83 @@ +(**************************************************************************) +(* ___ *) +(* ||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.ma". + +(* ITERATED PARTIAL UNFOLD ON LOCAL ENVIRONMENTS ****************************) + +definition ltpsss: nat → nat → relation lenv ≝ + λd,e. TC … (ltpss d e). + +interpretation "repeated partial unfold (local environment)" + 'PSubstStars L1 d e L2 = (ltpsss d e L1 L2). + +(* Basic eliminators ********************************************************) + +lemma ltpsss_ind: ∀d,e,L1. ∀R:predicate lenv. R L1 → + (∀L,L2. L1 [d, e] ▶** L → L [d, e] ▶* L2 → R L → R L2) → + ∀L2. L1 [d, e] ▶** L2 → R L2. +#d #e #L1 #R #HL1 #IHL1 #L2 #HL12 @(TC_star_ind … HL1 IHL1 … HL12) // +qed-. + +lemma ltpsss_ind_dx: ∀d,e,L2. ∀R:predicate lenv. R L2 → + (∀L1,L. L1 [d, e] ▶* L → L [d, e] ▶** L2 → R L → R L1) → + ∀L1. L1 [d, e] ▶** L2 → R L1. +#d #e #L2 #R #HL2 #IHL2 #L1 #HL12 @(TC_star_ind_dx … HL2 IHL2 … HL12) // +qed-. + +(* Basic properties *********************************************************) + +lemma ltpsss_strap1: ∀L1,L,L2,d,e. + L1 [d, e] ▶** L → L [d, e] ▶* L2 → L1 [d, e] ▶** L2. +/2 width=3/ qed. + +lemma ltpsss_strap2: ∀L1,L,L2,d,e. + L1 [d, e] ▶* L → L [d, e] ▶** L2 → L1 [d, e] ▶** L2. +/2 width=3/ qed. + +lemma ltpsss_refl: ∀L,d,e. L [d, e] ▶** L. +/2 width=1/ qed. + +lemma ltpsss_weak_all: ∀L1,L2,d,e. L1 [d, e] ▶** L2 → L1 [0, |L2|] ▶** L2. +#L1 #L2 #d #e #H @(ltpsss_ind … H) -L2 // +#L #L2 #_ #HL2 +>(ltpss_fwd_length … HL2) /3 width=5/ +qed. + +(* Basic forward lemmas *****************************************************) + +lemma ltpsss_fwd_length: ∀L1,L2,d,e. L1 [d, e] ▶** L2 → |L1| = |L2|. +#L1 #L2 #d #e #H @(ltpsss_ind … H) -L2 // +#L #L2 #_ #HL2 #IHL12 >IHL12 -IHL12 +/2 width=3 by ltpss_fwd_length/ +qed-. + +(* Basic inversion lemmas ***************************************************) + +lemma ltpsss_inv_refl_O2: ∀d,L1,L2. L1 [d, 0] ▶** L2 → L1 = L2. +#d #L1 #L2 #H @(ltpsss_ind … H) -L2 // +#L #L2 #_ #HL2 #IHL <(ltpss_inv_refl_O2 … HL2) -HL2 // +qed-. + +lemma ltpsss_inv_atom1: ∀d,e,L2. ⋆ [d, e] ▶** L2 → L2 = ⋆. +#d #e #L2 #H @(ltpsss_ind … H) -L2 // +#L #L2 #_ #HL2 #IHL destruct +>(ltpss_inv_atom1 … HL2) -HL2 // +qed-. + +lemma ltpsss_inv_atom2: ∀d,e,L1. L1 [d, e] ▶** ⋆ → L1 = ⋆. +#d #e #L1 #H @(ltpsss_ind_dx … H) -L1 // +#L1 #L #HL1 #_ #IHL2 destruct +>(ltpss_inv_atom2 … HL1) -HL1 // +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_ldrop.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_ldrop.etc new file mode 100644 index 000000000..e4923f9be --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_ldrop.etc @@ -0,0 +1,74 @@ +(**************************************************************************) +(* ___ *) +(* ||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_ldrop.ma". +include "basic_2/unfold/ltpsss.ma". + +(* ITERATED PARTIAL UNFOLD ON LOCAL ENVIRONMENTS ****************************) + +lemma ltpsss_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ▶** L1 → + ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → + d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2. +#L0 #L1 #d1 #e1 #H @(ltpsss_ind … H) -L1 // /3 width=6/ +qed. + +lemma ltpsss_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶** L0 → + ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → + d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2. +#L1 #L0 #d1 #e1 #H @(ltpsss_ind … H) -L0 // /3 width=6/ +qed. + +lemma ltpsss_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ▶** L1 → + ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → + ∃∃L. L2 [0, d1 + e1 - e2] ▶** L & ⇩[0, e2] L1 ≡ L. +#L0 #L1 #d1 #e1 #H @(ltpsss_ind … H) -L1 +[ /2 width=3/ +| #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1 + elim (IHL … HL02 Hd1e2 He2de1) -L0 #L0 #HL20 #HL0 + elim (ltpss_ldrop_conf_be … HL1 … HL0 Hd1e2 He2de1) -L /3 width=3/ +] +qed. + +lemma ltpsss_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ▶** L0 → + ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → + ∃∃L. L [0, d1 + e1 - e2] ▶** L2 & ⇩[0, e2] L1 ≡ L. +#L1 #L0 #d1 #e1 #H @(ltpsss_ind … H) -L0 +[ /2 width=3/ +| #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1 + elim (ltpss_ldrop_trans_be … HL0 … HL02 Hd1e2 He2de1) -L0 #L0 #HL02 #HL0 + elim (IHL … HL0 Hd1e2 He2de1) -L /3 width=3/ +] +qed. + +lemma ltpsss_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ▶** L1 → + ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 → + ∃∃L. L2 [d1 - e2, e1] ▶** L & ⇩[0, e2] L1 ≡ L. +#L0 #L1 #d1 #e1 #H @(ltpsss_ind … H) -L1 +[ /2 width=3/ +| #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #He2d1 + elim (IHL … HL02 He2d1) -L0 #L0 #HL20 #HL0 + elim (ltpss_ldrop_conf_le … HL1 … HL0 He2d1) -L /3 width=3/ +] +qed. + +lemma ltpsss_ldrop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ▶** L0 → + ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 → + ∃∃L. L [d1 - e2, e1] ▶** L2 & ⇩[0, e2] L1 ≡ L. +#L1 #L0 #d1 #e1 #H @(ltpsss_ind … H) -L0 +[ /2 width=3/ +| #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #He2d1 + elim (ltpss_ldrop_trans_le … HL0 … HL02 He2d1) -L0 #L0 #HL02 #HL0 + elim (IHL … HL0 He2d1) -L /3 width=3/ +] +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_ltpsss.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_ltpsss.etc new file mode 100644 index 000000000..36a036727 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_ltpsss.etc @@ -0,0 +1,153 @@ +(**************************************************************************) +(* ___ *) +(* ||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_ltpss.ma". +include "basic_2/unfold/ltpsss_tpss.ma". + +(* ITERATED PARTIAL UNFOLD ON LOCAL ENVIRONMENTS ****************************) + +(* Advanced properties ******************************************************) + +lemma ltpsss_strip: ∀L0,L1,d1,e1. L0 [d1, e1] ▶** L1 → + ∀L2,d2,e2. L0 [d2, e2] ▶* L2 → + ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶** L. +/3 width=3/ qed. + +lemma ltpsss_tpss_trans_eq: ∀L0,L1,d,e. L0 [d, e] ▶** L1 → + ∀T2,U2. L1 ⊢ T2 [d, e] ▶* U2 → L0 ⊢ T2 [d, e] ▶* U2. +#L0 #L1 #d #e #H @(ltpsss_ind … H) -L1 +[ /2 width=1/ +| #L #L1 #_ #HL1 #IHL #T2 #U2 #HTU2 + lapply (ltpss_tpss_trans_eq … HTU2 … HL1) -HL1 -HTU2 /2 width=1/ +] +qed. + +lemma ltpsss_tps_trans_eq: ∀L0,L1,d,e. L0 [d, e] ▶** L1 → + ∀T2,U2. L1 ⊢ T2 [d, e] ▶ U2 → L0 ⊢ T2 [d, e] ▶* U2. +/3 width=3/ qed. + +lemma ltpsss_tpss_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶* T2 → + ∀L2,ds,es. L1 [ds, es] ▶** L2 → + ∃∃T. L2 ⊢ T1 [d, e] ▶* T & L1 ⊢ T2 [ds, es] ▶* T. +#L1 #T1 #T2 #d #e #HT12 #L2 #ds #es #H @(ltpsss_ind … H) -L2 +[ /2 width=3/ +| -HT12 #L #L2 #HL1 #HL2 * #T #HT1 #HT2 + lapply (ltpsss_strap1 … HL1 HL2) -HL1 #HL12 + elim (ltpss_tpss_conf … HT1 … HL2) -L #T0 #HT10 #HT0 + lapply (ltpsss_tpss_trans_eq … HL12 … HT0) -HL12 -HT0 #HT0 + lapply (tpss_trans_eq … HT2 HT0) -T /2 width=3/ +] +qed. + +lemma ltpsss_tps_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶ T2 → + ∀L2,ds,es. L1 [ds, es] ▶** L2 → + ∃∃T. L2 ⊢ T1 [d, e] ▶* T & L1 ⊢ T2 [ds, es] ▶* T. +/3 width=1/ qed. + +(* Advanced forward lemmas **************************************************) + +lemma ltpsss_fwd_tpss21: ∀e,K1,I,V1,L2. 0 < e → K1. ⓑ{I} V1 [0, e] ▶** L2 → + ∃∃K2,V2. K1 [0, e - 1] ▶** K2 & + K1 ⊢ V1 [0, e - 1] ▶* V2 & + L2 = K2. ⓑ{I} V2. +#e #K1 #I #V1 #L2 #He #H @(ltpsss_ind … H) -L2 +[ /2 width=5/ +| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct + elim (ltpss_inv_tpss21 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H + lapply (ltpss_tpss_trans_eq … HV2 … HK2) -HV2 #HV2 + lapply (ltpsss_tpss_trans_eq … HK1 … HV2) -HV2 /3 width=5/ +] +qed-. + +lemma ltpsss_fwd_tpss11: ∀d,e,I,K1,V1,L2. 0 < d → K1. ⓑ{I} V1 [d, e] ▶** L2 → + ∃∃K2,V2. K1 [d - 1, e] ▶** K2 & + K1 ⊢ V1 [d - 1, e] ▶* V2 & + L2 = K2. ⓑ{I} V2. +#d #e #K1 #I #V1 #L2 #Hd #H @(ltpsss_ind … H) -L2 +[ /2 width=5/ +| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct + elim (ltpss_inv_tpss11 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H + lapply (ltpss_tpss_trans_eq … HV2 … HK2) -HV2 #HV2 + lapply (ltpsss_tpss_trans_eq … HK1 … HV2) -HV2 /3 width=5/ +] +qed-. + +lemma ltpsss_fwd_tpss22: ∀I,L1,K2,V2,e. L1 [0, e] ▶** K2. ⓑ{I} V2 → 0 < e → + ∃∃K1,V1. K1 [0, e - 1] ▶** K2 & + K1 ⊢ V1 [0, e - 1] ▶* V2 & + L1 = K1. ⓑ{I} V1. +#I #L1 #K2 #V2 #e #H #He @(ltpsss_ind_dx … H) -L1 +[ /2 width=5/ +| #L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct + elim (ltpss_inv_tpss22 … HL1 ?) -HL1 // #K1 #V1 #HK1 #HV1 #H destruct + lapply (tpss_trans_eq … HV1 HV2) -V #HV12 + lapply (ltpss_tpss_trans_eq … HV12 … HK1) -HV12 /3 width=5/ +] +qed-. + +lemma ltpsss_inv_tpss12: ∀I,L1,K2,V2,d,e. L1 [d, e] ▶** K2. ⓑ{I} V2 → 0 < d → + ∃∃K1,V1. K1 [d - 1, e] ▶** K2 & + K1 ⊢ V1 [d - 1, e] ▶* V2 & + L1 = K1. ⓑ{I} V1. +#I #L1 #K2 #V2 #d #e #H #Hd @(ltpsss_ind_dx … H) -L1 +[ /2 width=5/ +| #L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct + elim (ltpss_inv_tpss12 … HL1 ?) -HL1 // #K1 #V1 #HK1 #HV1 #H destruct + lapply (tpss_trans_eq … HV1 HV2) -V #HV12 + lapply (ltpss_tpss_trans_eq … HV12 … HK1) -HV12 /3 width=5/ +] +qed-. + +(* Main properties **********************************************************) + +theorem ltpsss_conf: ∀L0,L1,d1,e1. L0 [d1, e1] ▶** L1 → + ∀L2,d2,e2. L0 [d2, e2] ▶** L2 → + ∃∃L. L1 [d2, e2] ▶** L & L2 [d1, e1] ▶** L. +/3 width=3/ qed. + +theorem ltpsss_trans_eq: ∀L1,L,L2,d,e. + L1 [d, e] ▶** L → L [d, e] ▶** L2 → L1 [d, e] ▶** L2. +/2 width=3/ qed. + +lemma ltpsss_tpss2: ∀L1,L2,I,V1,V2,e. + L1 [0, e] ▶** L2 → L2 ⊢ V1 [0, e] ▶* V2 → + L1. ⓑ{I} V1 [0, e + 1] ▶** L2. ⓑ{I} V2. +#L1 #L2 #I #V1 #V2 #e #HL12 #H @(tpss_ind … H) -V2 +[ /2 width=1/ +| #V #V2 #_ #HV2 #IHV @(ltpsss_trans_eq … IHV) /2 width=1/ +] +qed. + +lemma ltpsss_tpss2_lt: ∀L1,L2,I,V1,V2,e. + L1 [0, e - 1] ▶** L2 → L2 ⊢ V1 [0, e - 1] ▶* V2 → + 0 < e → L1. ⓑ{I} V1 [0, e] ▶** L2. ⓑ{I} V2. +#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He +>(plus_minus_m_m e 1) // /2 width=1/ +qed. + +lemma ltpsss_tpss1: ∀L1,L2,I,V1,V2,d,e. + L1 [d, e] ▶** L2 → L2 ⊢ V1 [d, e] ▶* V2 → + L1. ⓑ{I} V1 [d + 1, e] ▶** L2. ⓑ{I} V2. +#L1 #L2 #I #V1 #V2 #d #e #HL12 #H @(tpss_ind … H) -V2 +[ /2 width=1/ +| #V #V2 #_ #HV2 #IHV @(ltpsss_trans_eq … IHV) /2 width=1/ +] +qed. + +lemma ltpsss_tpss1_lt: ∀L1,L2,I,V1,V2,d,e. + L1 [d - 1, e] ▶** L2 → L2 ⊢ V1 [d - 1, e] ▶* V2 → + 0 < d → L1. ⓑ{I} V1 [d, e] ▶** L2. ⓑ{I} V2. +#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd +>(plus_minus_m_m d 1) // /2 width=1/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_tps.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_tps.etc new file mode 100644 index 000000000..3f0e25ae9 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_tps.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 *) +(* *) +(**************************************************************************) + +include "basic_2/unfold/ltpss_tps.ma". +include "basic_2/unfold/ltpsss.ma". + +(* ITERATED PARTIAL UNFOLD ON LOCAL ENVIRONMENTS ****************************) + +(* Properties concerning partial substitution on terms **********************) + +lemma ltpsss_tps_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶** L0 → + ∀T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 → + d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ▶ U2. +#L1 #L0 #d1 #e1 #H @(ltpsss_ind … H) -L0 // +#L #L0 #_ #HL0 #IHL #T2 #U2 #d2 #e2 #HTU2 #Hde1d2 +lapply (ltpss_tps_trans_ge … HTU2 … HL0 ?) -HL0 -HTU2 // /2 width=1/ +qed. + +lemma ltpsss_tps_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 → + L0 ⊢ T2 [d2, e2] ▶ U2 → L0 [d1, e1] ▶** L1 → + L1 ⊢ T2 [d2, e2] ▶ U2. +#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HTU2 #H @(ltpsss_ind … H) -L1 // +-HTU2 #L #L1 #_ #HL1 #IHL +lapply (ltpss_tps_conf_ge … IHL … HL1 ?) -HL1 -IHL // +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_tpss.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_tpss.etc new file mode 100644 index 000000000..251a1a186 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_tpss.etc @@ -0,0 +1,74 @@ +(**************************************************************************) +(* ___ *) +(* ||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_tpss.ma". +include "basic_2/unfold/ltpsss.ma". + +(* ITERATED PARTIAL UNFOLD ON LOCAL ENVIRONMENTS ****************************) + +(* Properties concerning partial substitution on terms **********************) + +lemma ltpsss_tps2: ∀L1,L2,I,e. + L1 [0, e] ▶** L2 → ∀V1,V2. L2 ⊢ V1 [0, e] ▶ V2 → + L1. ⓑ{I} V1 [0, e + 1] ▶** L2. ⓑ{I} V2. +#L1 #L2 #I #e #H @(ltpsss_ind … H) -L2 +[ /3 width=1/ +| #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12 + elim (ltpss_tps_trans … HV12 … HL2) -HV12 #V #HV1 #HV2 + lapply (IHL … HV1) -IHL -HV1 /3 width=5/ +] +qed. + +lemma ltpsss_tps2_lt: ∀L1,L2,I,V1,V2,e. + L1 [0, e - 1] ▶** L2 → L2 ⊢ V1 [0, e - 1] ▶ V2 → + 0 < e → L1. ⓑ{I} V1 [0, e] ▶** L2. ⓑ{I} V2. +#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He +>(plus_minus_m_m e 1) // /2 width=1/ +qed. + +lemma ltpsss_tps1: ∀L1,L2,I,d,e. L1 [d, e] ▶** L2 → + ∀V1,V2. L2 ⊢ V1 [d, e] ▶ V2 → + L1. ⓑ{I} V1 [d + 1, e] ▶** L2. ⓑ{I} V2. +#L1 #L2 #I #d #e #H @(ltpsss_ind … H) -L2 +[ /3 width=1/ +| #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12 + elim (ltpss_tps_trans … HV12 … HL2) -HV12 #V #HV1 #HV2 + lapply (IHL … HV1) -IHL -HV1 /3 width=5/ +] +qed. + +lemma ltpsss_tps1_lt: ∀L1,L2,I,V1,V2,d,e. + L1 [d - 1, e] ▶** L2 → L2 ⊢ V1 [d - 1, e] ▶ V2 → + 0 < d → L1. ⓑ{I} V1 [d, e] ▶** L2. ⓑ{I} V2. +#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd +>(plus_minus_m_m d 1) // /2 width=1/ +qed. + +(* Properties concerning partial unfold on terms ****************************) + +lemma ltpsss_tpss_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 → + L0 ⊢ T2 [d2, e2] ▶* U2 → L0 [d1, e1] ▶** L1 → + L1 ⊢ T2 [d2, e2] ▶* U2. +#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HTU2 #H @(ltpsss_ind … H) -L1 // +-HTU2 #L #L1 #_ #HL1 #IHL +lapply (ltpss_tpss_conf_ge … IHL … HL1 ?) -HL1 -IHL // +qed. + +lemma ltpsss_tpss_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶** L0 → + ∀T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶* U2 → + d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ▶* U2. +#L1 #L0 #d1 #e1 #H @(ltpsss_ind … H) -L0 // +#L #L0 #_ #HL0 #IHL #T2 #U2 #d2 #e2 #HTU2 #Hde1d2 +lapply (ltpss_tpss_trans_ge … HTU2 … HL0 ?) -HL0 -HTU2 // /2 width=1/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/notation.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/notation.etc new file mode 100644 index 000000000..6846b7670 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/notation.etc @@ -0,0 +1,21 @@ +(**************************************************************************) +(* ___ *) +(* ||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 FOR THE FORMAL SYSTEM λδ ****************************************) + +(* Unfold *******************************************************************) + +notation "hvbox( T1 break [ d , break e ] ▶** break T2 )" + non associative with precedence 45 + for @{ 'PSubstStars $T1 $d $e $T2 }. diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/aarity.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/aarity.ma index f71f2d62e..0d7db6beb 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/aarity.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/aarity.ma @@ -12,13 +12,15 @@ (* *) (**************************************************************************) -(* THE FORMAL SYSTEM λδ - MATITA SOURCE FILES - * Support for abstract candidates of reducibility closed: 2012 January 27 - * Confluence of context-sensitive parallel reduction closed: 2011 September 21 - * Confluence of context-free parallel reduction closed: 2011 September 6 - * Specification started: 2011 April 17 +(* THE FORMAL SYSTEM λδ: MATITA SOURCE FILES * - Patience on me to gain peace and perfection! - * [ suggested invocation to start formal specifications with ] + * Context-sensitive subject equivalence for atomic arity assignment: 2012 April 16 + * Context-sensitive strong normalization for simply typed terms: 2012 March 15 + * Support for abstract candidates of reducibility closed: 2012 January 27 + * Confluence for context-sensitive parallel reduction: 2011 September 21 + * Confluence for context-free parallel reduction: 2011 September 6 + * Specification starts: 2011 April 17 *) include "ground_2/star.ma". diff --git a/matita/matita/contribs/lambda_delta/basic_2/native/nta.ma b/matita/matita/contribs/lambda_delta/basic_2/native/nta.ma new file mode 100644 index 000000000..99592cdd9 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/native/nta.ma @@ -0,0 +1,51 @@ +(**************************************************************************) +(* ___ *) +(* ||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/sh.ma". +include "basic_2/equivalence/cpcs.ma". + +(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************) + +inductive nta (h:sh): lenv → relation term ≝ +| nta_sort: ∀L,k. nta h L (⋆k) (⋆(next h k)) +| nta_ldef: ∀L,K,V,W,U,i. ⇩[0, i] L ≡ K. ⓓV → nta h K V W → + ⇧[0, i + 1] W ≡ U → nta h L (#i) U +| nta_ldec: ∀L,K,W,V,U,i. ⇩[0, i] L ≡ K. ⓛW → nta h K W V → + ⇧[0, i + 1] W ≡ U → nta h L (#i) U +| nta_bind: ∀I,L,V,W,T,U. nta h L V W → nta h (L. ⓑ{I} V) T U → + nta h L (ⓑ{I}V.T) (ⓑ{I}V.U) +| nta_appl: ∀L,V,W,U,T1,T2. nta h L V W → nta h L W U → nta h (L.ⓛW) T1 T2 → + nta h L (ⓐV.ⓛW.T1) (ⓐV.ⓛW.T2) +| nta_pure: ∀L,V,W,T,U. nta h L T U → nta h L (ⓐV.U) W → + nta h L (ⓐV.T) (ⓐV.U) +| nta_cast: ∀L,T,U. nta h L T U → nta h L (ⓣU. T) U +| nta_conv: ∀L,T,U1,U2,V2. nta h L T U1 → L ⊢ U1 ⬌* U2 → nta h L U2 V2 → + nta h L T U2 +. + +interpretation "native type assignment (term)" + 'NativeType h L T U = (nta h L T U). + +(* Basic properties *********************************************************) + +(* Basic_1: was: ty3_cast *) +lemma nta_cast_old: ∀h,L,W,T,U. + ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ U : W → ⦃h, L⦄ ⊢ ⓣU.T : ⓣW.U. +/4 width=3/ qed. + +(* Basic_1: was: ty3_typecheck *) +lemma nta_typecheck: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∃T0. ⦃h, L⦄ ⊢ ⓣU.T : T0. +/3 width=2/ qed. + +(* Basic_1: removed theorems 1: ty3_getl_subst0 *) diff --git a/matita/matita/contribs/lambda_delta/basic_2/native/nta_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/native/nta_lift.ma new file mode 100644 index 000000000..6e9d1b2a2 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/native/nta_lift.ma @@ -0,0 +1,201 @@ +(**************************************************************************) +(* ___ *) +(* ||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/equivalence/cpcs_cpcs.ma". +include "basic_2/native/nta.ma". + +(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************) + +(* Advanced inversion lemmas ************************************************) + +fact nta_inv_sort_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀k0. T = ⋆k0 → + L ⊢ ⋆(next h k0) ⬌* U. +#h #L #T #U #H elim H -L -T -U +[ #L #k #k0 #H destruct // +| #L #K #V #W #U #i #_ #_ #_ #_ #k0 #H destruct +| #L #K #W #V #U #i #_ #_ #_ #_ #k0 #H destruct +| #I #L #V #W #T #U #_ #_ #_ #_ #k0 #H destruct +| #L #V #W #U #T1 #T2 #_ #_ #_ #_ #_ #_ #k0 #H destruct +| #L #V #W #T #U #_ #_ #_ #_ #k0 #H destruct +| #L #T #U #_ #_ #k0 #H destruct +| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #k0 #H destruct + lapply (IHTU1 ??) -IHTU1 [ // | skip ] #Hk0 + lapply (cpcs_trans … Hk0 … HU12) -U1 // +] +qed. + +(* Basic_1: was: ty3_gen_sort *) +lemma nta_inv_sort: ∀h,L,U,k. ⦃h, L⦄ ⊢ ⋆k : U → L ⊢ ⋆(next h k) ⬌* U. +/2 width=3/ qed-. + +fact nta_inv_lref_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀j. T = #j → + (∃∃K,V,W,U0. ⇩[0, j] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V : W & + ⇧[0, j + 1] W ≡ U0 & L ⊢ U0 ⬌* U + ) ∨ + (∃∃K,W,V,U0. ⇩[0, j] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W : V & + ⇧[0, j + 1] W ≡ U0 & L ⊢ U0 ⬌* U + ). +#h #L #T #U #H elim H -L -T -U +[ #L #k #j #H destruct +| #L #K #V #W #U #i #HLK #HVW #HWU #_ #j #H destruct /3 width=8/ +| #L #K #W #V #U #i #HLK #HWV #HWU #_ #j #H destruct /3 width=8/ +| #I #L #V #W #T #U #_ #_ #_ #_ #j #H destruct +| #L #V #W #U #T1 #T2 #_ #_ #_ #_ #_ #_ #j #H destruct +| #L #V #W #T #U #_ #_ #_ #_ #j #H destruct +| #L #T #U #_ #_ #j #H destruct +| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #j #H destruct + elim (IHTU1 ??) -IHTU1 [4: // |2: skip ] * #K #V #W #U0 #HLK #HVW #HWU0 #HU01 + lapply (cpcs_trans … HU01 … HU12) -U1 /3 width=8/ +] +qed. + +(* Basic_1: was ty3_gen_lref *) +lemma nta_inv_lref: ∀h,L,U,i. ⦃h, L⦄ ⊢ #i : U → + (∃∃K,V,W,U0. ⇩[0, i] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V : W & + ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U + ) ∨ + (∃∃K,W,V,U0. ⇩[0, i] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W : V & + ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U + ). +/2 width=3/ qed-. + +fact nta_inv_bind_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀J,X,Y. T = ⓑ{J}Y.X → + ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y : Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X : Z2 & + L ⊢ ⓑ{J}Y.Z2 ⬌* U. +#h #L #T #U #H elim H -L -T -U +[ #L #k #J #X #Y #H destruct +| #L #K #V #W #U #i #_ #_ #_ #_ #J #X #Y #H destruct +| #L #K #W #V #U #i #_ #_ #_ #_ #J #X #Y #H destruct +| #I #L #V #W #T #U #HVW #HTU #_ #_ #J #X #Y #H destruct /2 width=3/ +| #L #V #W #U #T1 #T2 #_ #_ #_ #_ #_ #_ #J #X #Y #H destruct +| #L #V #W #T #U #_ #_ #_ #_ #J #X #Y #H destruct +| #L #T #U #_ #_ #J #X #Y #H destruct +| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #J #X #Y #H destruct + elim (IHTU1 ????) -IHTU1 [5: // |2,3,4: skip ] #Z1 #Z2 #HZ1 #HZ2 #HU1 + lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=3/ +] +qed. + +(* Basic_1: was: ty3_gen_bind *) +lemma nta_inv_bind: ∀h,J,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{J}Y.X : U → + ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y : Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X : Z2 & + L ⊢ ⓑ{J}Y.Z2 ⬌* U. +/2 width=3/ qed-. + +fact nta_inv_cast_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓣY.X → + ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U. +#h #L #T #U #H elim H -L -T -U +[ #L #k #X #Y #H destruct +| #L #K #V #W #U #i #_ #_ #_ #_ #X #Y #H destruct +| #L #K #W #V #U #i #_ #_ #_ #_ #X #Y #H destruct +| #I #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct +| #L #V #W #U #T1 #T2 #_ #_ #_ #_ #_ #_ #X #Y #H destruct +| #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct +| #L #T #U #HTU #_ #X #Y #H destruct /2 width=1/ +| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #X #Y #H destruct + elim (IHTU1 ???) -IHTU1 [4: // |2,3: skip ] #HXY #HU1 + lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=1/ +] +qed. + +(* Basic_1: was: ty3_gen_cast *) +lemma nta_inv_cast: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓣY.X : U → ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U. +/2 width=3/ qed-. + +(* Properties on relocation *************************************************) + +(* Basic_1: was: ty3_lift *) +lemma nta_lift: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 → + ∀T2. ⇧[d, e] T1 ≡ T2 → ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 : U2. +#h #L1 #T1 #U1 #H elim H -L1 -T1 -U1 +[ #L1 #k #L2 #d #e #HL21 #X1 #H1 #X2 #H2 + >(lift_inv_sort1 … H1) -X1 + >(lift_inv_sort1 … H2) -X2 // +| #L1 #K1 #V1 #W1 #W #i #HLK1 #_ #HW1 #IHVW1 #L2 #d #e #HL21 #X #H #U2 #HWU2 + elim (lift_inv_lref1 … H) * #Hid #H destruct + [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // #W2 #HW12 #HWU2 + elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H + elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct + /3 width=8/ + | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2 + lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/ + ] +| #L1 #K1 #W1 #V1 #W #i #HLK1 #_ #HW1 #IHWV1 #L2 #d #e #HL21 #X #H #U2 #HWU2 + elim (lift_inv_lref1 … H) * #Hid #H destruct + [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // (ltpr_inv_atom1 … HL) -HL #HL2 >(ltpsss_inv_atom1 … HL2) -HL2 // +#L2 * #L #HL >(ltpr_inv_atom1 … HL) -HL #HL2 >(ltpss_inv_atom1 … HL2) -HL2 // qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_aaa.ma index 77f384e58..61ed86b5b 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_aaa.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/static/aaa_ltpsss.ma". +include "basic_2/static/aaa_ltpss.ma". include "basic_2/reducibility/ltpr_aaa.ma". include "basic_2/reducibility/cpr.ma". include "basic_2/reducibility/lcpr.ma". diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_cpr.ma index 3d833fc02..08f63e87f 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_cpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_cpr.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/unfold/ltpsss_ltpsss.ma". +include "basic_2/unfold/ltpss_ltpss.ma". include "basic_2/reducibility/cpr.ma". include "basic_2/reducibility/lcpr.ma". @@ -23,5 +23,5 @@ include "basic_2/reducibility/lcpr.ma". lemma lcpr_pair: ∀L1,L2. L1 ⊢ ➡ L2 → ∀V1,V2. L2 ⊢ V1 ➡ V2 → ∀I. L1. ⓑ{I} V1 ⊢ ➡ L2. ⓑ{I} V2. #L1 #L2 * #L #HL1 #HL2 #V1 #V2 * -<(ltpsss_fwd_length … HL2) /4 width=5/ +<(ltpss_fwd_length … HL2) /4 width=5/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_lcpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_lcpr.ma index 5d7e4739e..2b1f4a4fd 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_lcpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_lcpr.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "basic_2/unfold/ltpsss_ltpsss.ma". -include "basic_2/reducibility/ltpr_ltpsss.ma". +include "basic_2/unfold/ltpss_ltpss.ma". +include "basic_2/reducibility/ltpr_ltpss.ma". include "basic_2/reducibility/ltpr_ltpr.ma". include "basic_2/reducibility/lcpr.ma". @@ -27,13 +27,13 @@ theorem lcpr_conf: ∀L0,L1,L2. L0 ⊢ ➡ L1 → L0 ⊢ ➡ L2 → lapply (ltpr_fwd_length … HK01) #H >(ltpr_fwd_length … HK02) in H; #H elim (ltpr_conf … HK01 … HK02) -K0 #K #HK1 #HK2 -lapply (ltpsss_fwd_length … HKL1) #H1 -lapply (ltpsss_fwd_length … HKL2) #H2 +lapply (ltpss_fwd_length … HKL1) #H1 +lapply (ltpss_fwd_length … HKL2) #H2 >H1 in HKL1 H; -H1 #HKL1 >H2 in HKL2; -H2 #HKL2 #H -elim (ltpr_ltpsss_conf … HKL1 … HK1) -K1 #K1 #HK1 #HLK1 -elim (ltpr_ltpsss_conf … HKL2 … HK2) -K2 #K2 #HK2 #HLK2 -elim (ltpsss_conf … HK1 … HK2) -K #K #HK1 #HK2 +elim (ltpr_ltpss_conf … HKL1 … HK1) -K1 #K1 #HK1 #HLK1 +elim (ltpr_ltpss_conf … HKL2 … HK2) -K2 #K2 #HK2 #HLK2 +elim (ltpss_conf … HK1 … HK2) -K #K #HK1 #HK2 lapply (ltpr_fwd_length … HLK1) #H1 lapply (ltpr_fwd_length … HLK2) #H2 /3 width=5/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpsss.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpsss.ma deleted file mode 100644 index d0c29e726..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpsss.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/unfold/ltpsss.ma". -include "basic_2/reducibility/ltpr_ltpss.ma". - -(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) - -(* Properties on iterated parallel unfold on local environments *************) - -lemma ltpr_ltpsss_conf: ∀L1,K1,d,e. L1 [d, e] ▶** K1 → ∀L2. L1 ➡ L2 → - ∃∃K2. L2 [d, e] ▶** K2 & K1 ➡ K2. -#L1 #K1 #d #e #H @(ltpsss_ind … H) -K1 /2 width=3/ -#K #K1 #_ #HK1 #IHK #L2 #HL12 -elim (IHK … HL12) -L1 #K2 #HLK2 #HK2 -elim (ltpr_ltpss_conf … HK1 … HK2) -K /3 width=3/ -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpsss.ma b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpsss.ma deleted file mode 100644 index e3d048809..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpsss.ma +++ /dev/null @@ -1,34 +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/unfold/ltpsss.ma". -include "basic_2/static/aaa_ltpss.ma". - -(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) - -(* Properties about iterated parallel unfold ********************************) - -lemma aaa_ltpsss_conf: ∀L1,T,A. L1 ⊢ T ÷ A → - ∀L2,d,e. L1 [d, e] ▶** L2 → L2 ⊢ T ÷ A. -#L1 #T #A #HT #L2 #d #e #HL12 -@(TC_Conf3 … (λL,A. L ⊢ T ÷ A) … HT ? HL12) /2 width=5/ -qed. - -lemma aaa_ltpsss_tpss_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. L1 [d, e] ▶** L2 → - ∀T2. L2 ⊢ T1 [d, e] ▶* T2 → L2 ⊢ T2 ÷ A. -/3 width=5/ qed. - -lemma aaa_ltpsss_tps_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. L1 [d, e] ▶** L2 → - ∀T2. L2 ⊢ T1 [d, e] ▶ T2 → L2 ⊢ T2 ÷ A. -/3 width=5/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/sh.ma b/matita/matita/contribs/lambda_delta/basic_2/static/sh.ma index 4eeac01b8..0577b0015 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/sh.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/sh.ma @@ -16,7 +16,7 @@ include "ground_2/arith.ma". (* SORT HIERARCHY ***********************************************************) -(* sort hierarchy specifications *) +(* sort hierarchy specification *) record sh: Type[0] ≝ { next: nat → nat; (* next sort in the hierarchy *) next_lt: ∀k. k < next k (* strict monotonicity condition *) diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma index 74edd2ea2..e70389973 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma @@ -69,7 +69,7 @@ theorem lift_div_le: ∀d1,e1,T1,T. ⇧[d1, e1] T1 ≡ T → ] qed. -(* Note: apparently this was missing in Basic_1 *) +(* Note: apparently this was missing in basic_1 *) theorem lift_div_be: ∀d1,e1,T1,T. ⇧[d1, e1] T1 ≡ T → ∀e,e2,T2. ⇧[d1 + e, e2] T2 ≡ T → e ≤ e1 → e1 ≤ e + e2 → diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss.ma deleted file mode 100644 index 58fb3e20b..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss.ma +++ /dev/null @@ -1,83 +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/unfold/ltpss.ma". - -(* ITERATED PARTIAL UNFOLD ON LOCAL ENVIRONMENTS ****************************) - -definition ltpsss: nat → nat → relation lenv ≝ - λd,e. TC … (ltpss d e). - -interpretation "repeated partial unfold (local environment)" - 'PSubstStars L1 d e L2 = (ltpsss d e L1 L2). - -(* Basic eliminators ********************************************************) - -lemma ltpsss_ind: ∀d,e,L1. ∀R:predicate lenv. R L1 → - (∀L,L2. L1 [d, e] ▶** L → L [d, e] ▶* L2 → R L → R L2) → - ∀L2. L1 [d, e] ▶** L2 → R L2. -#d #e #L1 #R #HL1 #IHL1 #L2 #HL12 @(TC_star_ind … HL1 IHL1 … HL12) // -qed-. - -lemma ltpsss_ind_dx: ∀d,e,L2. ∀R:predicate lenv. R L2 → - (∀L1,L. L1 [d, e] ▶* L → L [d, e] ▶** L2 → R L → R L1) → - ∀L1. L1 [d, e] ▶** L2 → R L1. -#d #e #L2 #R #HL2 #IHL2 #L1 #HL12 @(TC_star_ind_dx … HL2 IHL2 … HL12) // -qed-. - -(* Basic properties *********************************************************) - -lemma ltpsss_strap1: ∀L1,L,L2,d,e. - L1 [d, e] ▶** L → L [d, e] ▶* L2 → L1 [d, e] ▶** L2. -/2 width=3/ qed. - -lemma ltpsss_strap2: ∀L1,L,L2,d,e. - L1 [d, e] ▶* L → L [d, e] ▶** L2 → L1 [d, e] ▶** L2. -/2 width=3/ qed. - -lemma ltpsss_refl: ∀L,d,e. L [d, e] ▶** L. -/2 width=1/ qed. - -lemma ltpsss_weak_all: ∀L1,L2,d,e. L1 [d, e] ▶** L2 → L1 [0, |L2|] ▶** L2. -#L1 #L2 #d #e #H @(ltpsss_ind … H) -L2 // -#L #L2 #_ #HL2 ->(ltpss_fwd_length … HL2) /3 width=5/ -qed. - -(* Basic forward lemmas *****************************************************) - -lemma ltpsss_fwd_length: ∀L1,L2,d,e. L1 [d, e] ▶** L2 → |L1| = |L2|. -#L1 #L2 #d #e #H @(ltpsss_ind … H) -L2 // -#L #L2 #_ #HL2 #IHL12 >IHL12 -IHL12 -/2 width=3 by ltpss_fwd_length/ -qed-. - -(* Basic inversion lemmas ***************************************************) - -lemma ltpsss_inv_refl_O2: ∀d,L1,L2. L1 [d, 0] ▶** L2 → L1 = L2. -#d #L1 #L2 #H @(ltpsss_ind … H) -L2 // -#L #L2 #_ #HL2 #IHL <(ltpss_inv_refl_O2 … HL2) -HL2 // -qed-. - -lemma ltpsss_inv_atom1: ∀d,e,L2. ⋆ [d, e] ▶** L2 → L2 = ⋆. -#d #e #L2 #H @(ltpsss_ind … H) -L2 // -#L #L2 #_ #HL2 #IHL destruct ->(ltpss_inv_atom1 … HL2) -HL2 // -qed-. - -lemma ltpsss_inv_atom2: ∀d,e,L1. L1 [d, e] ▶** ⋆ → L1 = ⋆. -#d #e #L1 #H @(ltpsss_ind_dx … H) -L1 // -#L1 #L #HL1 #_ #IHL2 destruct ->(ltpss_inv_atom2 … HL1) -HL1 // -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_ldrop.ma deleted file mode 100644 index e4923f9be..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_ldrop.ma +++ /dev/null @@ -1,74 +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/unfold/ltpss_ldrop.ma". -include "basic_2/unfold/ltpsss.ma". - -(* ITERATED PARTIAL UNFOLD ON LOCAL ENVIRONMENTS ****************************) - -lemma ltpsss_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ▶** L1 → - ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → - d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2. -#L0 #L1 #d1 #e1 #H @(ltpsss_ind … H) -L1 // /3 width=6/ -qed. - -lemma ltpsss_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶** L0 → - ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → - d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2. -#L1 #L0 #d1 #e1 #H @(ltpsss_ind … H) -L0 // /3 width=6/ -qed. - -lemma ltpsss_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ▶** L1 → - ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → - ∃∃L. L2 [0, d1 + e1 - e2] ▶** L & ⇩[0, e2] L1 ≡ L. -#L0 #L1 #d1 #e1 #H @(ltpsss_ind … H) -L1 -[ /2 width=3/ -| #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1 - elim (IHL … HL02 Hd1e2 He2de1) -L0 #L0 #HL20 #HL0 - elim (ltpss_ldrop_conf_be … HL1 … HL0 Hd1e2 He2de1) -L /3 width=3/ -] -qed. - -lemma ltpsss_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ▶** L0 → - ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → - ∃∃L. L [0, d1 + e1 - e2] ▶** L2 & ⇩[0, e2] L1 ≡ L. -#L1 #L0 #d1 #e1 #H @(ltpsss_ind … H) -L0 -[ /2 width=3/ -| #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1 - elim (ltpss_ldrop_trans_be … HL0 … HL02 Hd1e2 He2de1) -L0 #L0 #HL02 #HL0 - elim (IHL … HL0 Hd1e2 He2de1) -L /3 width=3/ -] -qed. - -lemma ltpsss_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ▶** L1 → - ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 → - ∃∃L. L2 [d1 - e2, e1] ▶** L & ⇩[0, e2] L1 ≡ L. -#L0 #L1 #d1 #e1 #H @(ltpsss_ind … H) -L1 -[ /2 width=3/ -| #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #He2d1 - elim (IHL … HL02 He2d1) -L0 #L0 #HL20 #HL0 - elim (ltpss_ldrop_conf_le … HL1 … HL0 He2d1) -L /3 width=3/ -] -qed. - -lemma ltpsss_ldrop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ▶** L0 → - ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 → - ∃∃L. L [d1 - e2, e1] ▶** L2 & ⇩[0, e2] L1 ≡ L. -#L1 #L0 #d1 #e1 #H @(ltpsss_ind … H) -L0 -[ /2 width=3/ -| #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #He2d1 - elim (ltpss_ldrop_trans_le … HL0 … HL02 He2d1) -L0 #L0 #HL02 #HL0 - elim (IHL … HL0 He2d1) -L /3 width=3/ -] -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_ltpsss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_ltpsss.ma deleted file mode 100644 index 36a036727..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_ltpsss.ma +++ /dev/null @@ -1,153 +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/unfold/ltpss_ltpss.ma". -include "basic_2/unfold/ltpsss_tpss.ma". - -(* ITERATED PARTIAL UNFOLD ON LOCAL ENVIRONMENTS ****************************) - -(* Advanced properties ******************************************************) - -lemma ltpsss_strip: ∀L0,L1,d1,e1. L0 [d1, e1] ▶** L1 → - ∀L2,d2,e2. L0 [d2, e2] ▶* L2 → - ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶** L. -/3 width=3/ qed. - -lemma ltpsss_tpss_trans_eq: ∀L0,L1,d,e. L0 [d, e] ▶** L1 → - ∀T2,U2. L1 ⊢ T2 [d, e] ▶* U2 → L0 ⊢ T2 [d, e] ▶* U2. -#L0 #L1 #d #e #H @(ltpsss_ind … H) -L1 -[ /2 width=1/ -| #L #L1 #_ #HL1 #IHL #T2 #U2 #HTU2 - lapply (ltpss_tpss_trans_eq … HTU2 … HL1) -HL1 -HTU2 /2 width=1/ -] -qed. - -lemma ltpsss_tps_trans_eq: ∀L0,L1,d,e. L0 [d, e] ▶** L1 → - ∀T2,U2. L1 ⊢ T2 [d, e] ▶ U2 → L0 ⊢ T2 [d, e] ▶* U2. -/3 width=3/ qed. - -lemma ltpsss_tpss_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶* T2 → - ∀L2,ds,es. L1 [ds, es] ▶** L2 → - ∃∃T. L2 ⊢ T1 [d, e] ▶* T & L1 ⊢ T2 [ds, es] ▶* T. -#L1 #T1 #T2 #d #e #HT12 #L2 #ds #es #H @(ltpsss_ind … H) -L2 -[ /2 width=3/ -| -HT12 #L #L2 #HL1 #HL2 * #T #HT1 #HT2 - lapply (ltpsss_strap1 … HL1 HL2) -HL1 #HL12 - elim (ltpss_tpss_conf … HT1 … HL2) -L #T0 #HT10 #HT0 - lapply (ltpsss_tpss_trans_eq … HL12 … HT0) -HL12 -HT0 #HT0 - lapply (tpss_trans_eq … HT2 HT0) -T /2 width=3/ -] -qed. - -lemma ltpsss_tps_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶ T2 → - ∀L2,ds,es. L1 [ds, es] ▶** L2 → - ∃∃T. L2 ⊢ T1 [d, e] ▶* T & L1 ⊢ T2 [ds, es] ▶* T. -/3 width=1/ qed. - -(* Advanced forward lemmas **************************************************) - -lemma ltpsss_fwd_tpss21: ∀e,K1,I,V1,L2. 0 < e → K1. ⓑ{I} V1 [0, e] ▶** L2 → - ∃∃K2,V2. K1 [0, e - 1] ▶** K2 & - K1 ⊢ V1 [0, e - 1] ▶* V2 & - L2 = K2. ⓑ{I} V2. -#e #K1 #I #V1 #L2 #He #H @(ltpsss_ind … H) -L2 -[ /2 width=5/ -| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct - elim (ltpss_inv_tpss21 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H - lapply (ltpss_tpss_trans_eq … HV2 … HK2) -HV2 #HV2 - lapply (ltpsss_tpss_trans_eq … HK1 … HV2) -HV2 /3 width=5/ -] -qed-. - -lemma ltpsss_fwd_tpss11: ∀d,e,I,K1,V1,L2. 0 < d → K1. ⓑ{I} V1 [d, e] ▶** L2 → - ∃∃K2,V2. K1 [d - 1, e] ▶** K2 & - K1 ⊢ V1 [d - 1, e] ▶* V2 & - L2 = K2. ⓑ{I} V2. -#d #e #K1 #I #V1 #L2 #Hd #H @(ltpsss_ind … H) -L2 -[ /2 width=5/ -| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct - elim (ltpss_inv_tpss11 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H - lapply (ltpss_tpss_trans_eq … HV2 … HK2) -HV2 #HV2 - lapply (ltpsss_tpss_trans_eq … HK1 … HV2) -HV2 /3 width=5/ -] -qed-. - -lemma ltpsss_fwd_tpss22: ∀I,L1,K2,V2,e. L1 [0, e] ▶** K2. ⓑ{I} V2 → 0 < e → - ∃∃K1,V1. K1 [0, e - 1] ▶** K2 & - K1 ⊢ V1 [0, e - 1] ▶* V2 & - L1 = K1. ⓑ{I} V1. -#I #L1 #K2 #V2 #e #H #He @(ltpsss_ind_dx … H) -L1 -[ /2 width=5/ -| #L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct - elim (ltpss_inv_tpss22 … HL1 ?) -HL1 // #K1 #V1 #HK1 #HV1 #H destruct - lapply (tpss_trans_eq … HV1 HV2) -V #HV12 - lapply (ltpss_tpss_trans_eq … HV12 … HK1) -HV12 /3 width=5/ -] -qed-. - -lemma ltpsss_inv_tpss12: ∀I,L1,K2,V2,d,e. L1 [d, e] ▶** K2. ⓑ{I} V2 → 0 < d → - ∃∃K1,V1. K1 [d - 1, e] ▶** K2 & - K1 ⊢ V1 [d - 1, e] ▶* V2 & - L1 = K1. ⓑ{I} V1. -#I #L1 #K2 #V2 #d #e #H #Hd @(ltpsss_ind_dx … H) -L1 -[ /2 width=5/ -| #L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct - elim (ltpss_inv_tpss12 … HL1 ?) -HL1 // #K1 #V1 #HK1 #HV1 #H destruct - lapply (tpss_trans_eq … HV1 HV2) -V #HV12 - lapply (ltpss_tpss_trans_eq … HV12 … HK1) -HV12 /3 width=5/ -] -qed-. - -(* Main properties **********************************************************) - -theorem ltpsss_conf: ∀L0,L1,d1,e1. L0 [d1, e1] ▶** L1 → - ∀L2,d2,e2. L0 [d2, e2] ▶** L2 → - ∃∃L. L1 [d2, e2] ▶** L & L2 [d1, e1] ▶** L. -/3 width=3/ qed. - -theorem ltpsss_trans_eq: ∀L1,L,L2,d,e. - L1 [d, e] ▶** L → L [d, e] ▶** L2 → L1 [d, e] ▶** L2. -/2 width=3/ qed. - -lemma ltpsss_tpss2: ∀L1,L2,I,V1,V2,e. - L1 [0, e] ▶** L2 → L2 ⊢ V1 [0, e] ▶* V2 → - L1. ⓑ{I} V1 [0, e + 1] ▶** L2. ⓑ{I} V2. -#L1 #L2 #I #V1 #V2 #e #HL12 #H @(tpss_ind … H) -V2 -[ /2 width=1/ -| #V #V2 #_ #HV2 #IHV @(ltpsss_trans_eq … IHV) /2 width=1/ -] -qed. - -lemma ltpsss_tpss2_lt: ∀L1,L2,I,V1,V2,e. - L1 [0, e - 1] ▶** L2 → L2 ⊢ V1 [0, e - 1] ▶* V2 → - 0 < e → L1. ⓑ{I} V1 [0, e] ▶** L2. ⓑ{I} V2. -#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He ->(plus_minus_m_m e 1) // /2 width=1/ -qed. - -lemma ltpsss_tpss1: ∀L1,L2,I,V1,V2,d,e. - L1 [d, e] ▶** L2 → L2 ⊢ V1 [d, e] ▶* V2 → - L1. ⓑ{I} V1 [d + 1, e] ▶** L2. ⓑ{I} V2. -#L1 #L2 #I #V1 #V2 #d #e #HL12 #H @(tpss_ind … H) -V2 -[ /2 width=1/ -| #V #V2 #_ #HV2 #IHV @(ltpsss_trans_eq … IHV) /2 width=1/ -] -qed. - -lemma ltpsss_tpss1_lt: ∀L1,L2,I,V1,V2,d,e. - L1 [d - 1, e] ▶** L2 → L2 ⊢ V1 [d - 1, e] ▶* V2 → - 0 < d → L1. ⓑ{I} V1 [d, e] ▶** L2. ⓑ{I} V2. -#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd ->(plus_minus_m_m d 1) // /2 width=1/ -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_tps.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_tps.ma deleted file mode 100644 index 3f0e25ae9..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_tps.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/unfold/ltpss_tps.ma". -include "basic_2/unfold/ltpsss.ma". - -(* ITERATED PARTIAL UNFOLD ON LOCAL ENVIRONMENTS ****************************) - -(* Properties concerning partial substitution on terms **********************) - -lemma ltpsss_tps_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶** L0 → - ∀T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 → - d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ▶ U2. -#L1 #L0 #d1 #e1 #H @(ltpsss_ind … H) -L0 // -#L #L0 #_ #HL0 #IHL #T2 #U2 #d2 #e2 #HTU2 #Hde1d2 -lapply (ltpss_tps_trans_ge … HTU2 … HL0 ?) -HL0 -HTU2 // /2 width=1/ -qed. - -lemma ltpsss_tps_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 → - L0 ⊢ T2 [d2, e2] ▶ U2 → L0 [d1, e1] ▶** L1 → - L1 ⊢ T2 [d2, e2] ▶ U2. -#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HTU2 #H @(ltpsss_ind … H) -L1 // --HTU2 #L #L1 #_ #HL1 #IHL -lapply (ltpss_tps_conf_ge … IHL … HL1 ?) -HL1 -IHL // -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_tpss.ma deleted file mode 100644 index 251a1a186..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_tpss.ma +++ /dev/null @@ -1,74 +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/unfold/ltpss_tpss.ma". -include "basic_2/unfold/ltpsss.ma". - -(* ITERATED PARTIAL UNFOLD ON LOCAL ENVIRONMENTS ****************************) - -(* Properties concerning partial substitution on terms **********************) - -lemma ltpsss_tps2: ∀L1,L2,I,e. - L1 [0, e] ▶** L2 → ∀V1,V2. L2 ⊢ V1 [0, e] ▶ V2 → - L1. ⓑ{I} V1 [0, e + 1] ▶** L2. ⓑ{I} V2. -#L1 #L2 #I #e #H @(ltpsss_ind … H) -L2 -[ /3 width=1/ -| #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12 - elim (ltpss_tps_trans … HV12 … HL2) -HV12 #V #HV1 #HV2 - lapply (IHL … HV1) -IHL -HV1 /3 width=5/ -] -qed. - -lemma ltpsss_tps2_lt: ∀L1,L2,I,V1,V2,e. - L1 [0, e - 1] ▶** L2 → L2 ⊢ V1 [0, e - 1] ▶ V2 → - 0 < e → L1. ⓑ{I} V1 [0, e] ▶** L2. ⓑ{I} V2. -#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He ->(plus_minus_m_m e 1) // /2 width=1/ -qed. - -lemma ltpsss_tps1: ∀L1,L2,I,d,e. L1 [d, e] ▶** L2 → - ∀V1,V2. L2 ⊢ V1 [d, e] ▶ V2 → - L1. ⓑ{I} V1 [d + 1, e] ▶** L2. ⓑ{I} V2. -#L1 #L2 #I #d #e #H @(ltpsss_ind … H) -L2 -[ /3 width=1/ -| #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12 - elim (ltpss_tps_trans … HV12 … HL2) -HV12 #V #HV1 #HV2 - lapply (IHL … HV1) -IHL -HV1 /3 width=5/ -] -qed. - -lemma ltpsss_tps1_lt: ∀L1,L2,I,V1,V2,d,e. - L1 [d - 1, e] ▶** L2 → L2 ⊢ V1 [d - 1, e] ▶ V2 → - 0 < d → L1. ⓑ{I} V1 [d, e] ▶** L2. ⓑ{I} V2. -#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd ->(plus_minus_m_m d 1) // /2 width=1/ -qed. - -(* Properties concerning partial unfold on terms ****************************) - -lemma ltpsss_tpss_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 → - L0 ⊢ T2 [d2, e2] ▶* U2 → L0 [d1, e1] ▶** L1 → - L1 ⊢ T2 [d2, e2] ▶* U2. -#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HTU2 #H @(ltpsss_ind … H) -L1 // --HTU2 #L #L1 #_ #HL1 #IHL -lapply (ltpss_tpss_conf_ge … IHL … HL1 ?) -HL1 -IHL // -qed. - -lemma ltpsss_tpss_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶** L0 → - ∀T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶* U2 → - d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ▶* U2. -#L1 #L0 #d1 #e1 #H @(ltpsss_ind … H) -L0 // -#L #L0 #_ #HL0 #IHL #T2 #U2 #d2 #e2 #HTU2 #Hde1d2 -lapply (ltpss_tpss_trans_ge … HTU2 … HL0 ?) -HL0 -HTU2 // /2 width=1/ -qed.