From 83fcc60ebb369516f291209925ffa42ba64e24f9 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 16 Apr 2012 14:45:39 +0000 Subject: [PATCH] - subject equivalence for atomic arity assignment completed! - bug fix in partial unfold for local environments (nowthis relation is confluent) --- .../basic_2/computation/cprs_lcpr.ma | 2 +- .../basic_2/computation/lcprs_lcprs.ma | 12 +- .../basic_2/reducibility/cpr_ltpss.ma | 2 +- .../basic_2/reducibility/cpr_ltpsss.ma | 25 +++ .../lambda_delta/basic_2/reducibility/lcpr.ma | 6 +- .../basic_2/reducibility/lcpr_aaa.ma | 2 +- .../basic_2/reducibility/lcpr_cpr.ma | 4 +- .../basic_2/reducibility/lcpr_lcpr.ma | 13 +- .../basic_2/reducibility/ltpr_aaa.ma | 2 +- .../basic_2/reducibility/ltpr_ltpss.ma | 17 +- .../basic_2/reducibility/ltpr_ltpsss.ma | 28 ++++ .../basic_2/reducibility/tpr_tpss.ma | 3 +- .../lambda_delta/basic_2/static/aaa_ltps.ma | 65 -------- .../lambda_delta/basic_2/static/aaa_ltpss.ma | 66 ++++++-- .../lambda_delta/basic_2/static/aaa_ltpsss.ma | 34 ++++ .../lambda_delta/basic_2/unfold/ltpss.ma | 20 +++ .../basic_2/unfold/ltpss_ltpss.ma | 35 ++++ .../lambda_delta/basic_2/unfold/ltpss_tpss.ma | 36 ----- .../lambda_delta/basic_2/unfold/ltpsss.ma | 83 ++++++++++ .../basic_2/unfold/ltpsss_ldrop.ma | 74 +++++++++ .../basic_2/unfold/ltpsss_ltpsss.ma | 153 ++++++++++++++++++ .../lambda_delta/basic_2/unfold/ltpsss_tps.ma | 36 +++++ .../basic_2/unfold/ltpsss_tpss.ma | 74 +++++++++ .../lambda_delta/basic_2/unfold/tpss_alt.ma | 101 ++++++++++++ 24 files changed, 745 insertions(+), 148 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpsss.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpsss.ma delete mode 100644 matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltps.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpsss.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_ldrop.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_ltpsss.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_tps.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_tpss.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_alt.ma 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 14bcfd5c4..bb7896c30 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_ltpss.ma". +include "basic_2/reducibility/cpr_ltpsss.ma". include "basic_2/reducibility/lcpr.ma". include "basic_2/computation/cprs.ma". diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_lcprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_lcprs.ma index 344eae154..64851e801 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_lcprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_lcprs.ma @@ -11,22 +11,24 @@ (* v GNU General Public License Version 2 *) (* *) (**************************************************************************) -(* + include "basic_2/reducibility/lcpr_lcpr.ma". -*) include "basic_2/computation/lcprs_cprs.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *************) (* Advanced properties ******************************************************) -axiom lcprs_strip: ∀L,L1. L ⊢ ➡* L1 → ∀L2. L ⊢ ➡ L2 → +lemma lcprs_strip: ∀L,L1. L ⊢ ➡* L1 → ∀L2. L ⊢ ➡ L2 → ∃∃L0. L1 ⊢ ➡ L0 & L2 ⊢ ➡* L0. -(* /3 width=3/ qed. -*) + (* Main properties **********************************************************) +theorem lcprs_conf: ∀L,L1. L ⊢ ➡* L1 → ∀L2. L ⊢ ➡* L2 → + ∃∃L0. L1 ⊢ ➡* L0 & L2 ⊢ ➡* L0. +/3 width=3/ qed. + theorem lcprs_trans: ∀L1,L. L1 ⊢ ➡* L → ∀L2. L ⊢ ➡* L2 → L1 ⊢ ➡* L2. /2 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpss.ma index 26e045848..a3b31f225 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpss.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/unfold/ltpss_tpss.ma". +include "basic_2/unfold/ltpss_ltpss.ma". include "basic_2/reducibility/cpr.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpsss.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpsss.ma new file mode 100644 index 000000000..0890e462b --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpsss.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/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/reducibility/lcpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr.ma index 51028c240..4d8a341bc 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr.ma @@ -12,13 +12,13 @@ (* *) (**************************************************************************) -include "basic_2/unfold/ltpss.ma". +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 + λL1,L2. ∃∃L. L1 ➡ L & L [0, |L|] ▶** L2 . interpretation @@ -33,5 +33,5 @@ lemma lcpr_refl: ∀L. L ⊢ ➡ L. (* Basic inversion lemmas ***************************************************) lemma lcpr_inv_atom1: ∀L2. ⋆ ⊢ ➡ L2 → L2 = ⋆. -#L2 * #L #HL >(ltpr_inv_atom1 … HL) -HL #HL2 >(ltpss_inv_atom1 … HL2) -HL2 // +#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/reducibility/lcpr_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_aaa.ma index 61ed86b5b..77f384e58 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_ltpss.ma". +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". 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 08f63e87f..3d833fc02 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/ltpss_ltpss.ma". +include "basic_2/unfold/ltpsss_ltpsss.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 * -<(ltpss_fwd_length … HL2) /4 width=5/ +<(ltpsss_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 4b1f9b51a..5d7e4739e 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,7 +12,8 @@ (* *) (**************************************************************************) -include "basic_2/reducibility/ltpr_ltpss.ma". +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". @@ -26,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 (ltpss_fwd_length … HKL1) #H1 -lapply (ltpss_fwd_length … HKL2) #H2 +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_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 +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/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma index baf1abb09..5bf592294 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/static/aaa_ltps.ma". +include "basic_2/static/aaa_ltpss.ma". include "basic_2/static/lsuba_aaa.ma". include "basic_2/reducibility/ltpr_ldrop.ma". diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpss.ma index 879d4418b..ecc2d7443 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpss.ma @@ -18,8 +18,8 @@ include "basic_2/reducibility/tpr_tpss.ma". (* Properties concerning parallel unfold on local environments **************) -lemma ltpr_ltps_conf: ∀L1,K1,d,e. L1 [d, e] ▶ K1 → ∀L2. L1 ➡ L2 → - ∃∃K2. L2 [d, e] ▶* K2 & K1 ➡ K2. +lemma ltpr_ltpss_conf: ∀L1,K1,d,e. L1 [d, e] ▶* K1 → ∀L2. L1 ➡ L2 → + ∃∃K2. L2 [d, e] ▶* K2 & K1 ➡ K2. #L1 #K1 #d #e #H elim H -L1 -K1 -d -e [ /2 width=3/ | #L1 #I #V1 #X #H @@ -27,19 +27,10 @@ lemma ltpr_ltps_conf: ∀L1,K1,d,e. L1 [d, e] ▶ K1 → ∀L2. L1 ➡ L2 → | #L1 #K1 #I #V1 #W1 #e #_ #HVW1 #IHLK1 #X #H elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct elim (IHLK1 … HL12) -L1 #K2 #HLK2 #HK12 - elim (tpr_tps_ltpr … HV12 … HVW1 … HK12) -V1 /3 width=5/ + elim (tpr_tpss_ltpr … HK12 … HV12 … HVW1) -V1 /3 width=5/ | #L1 #K1 #I #V1 #W1 #d #e #_ #HVW1 #IHLK1 #X #H elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct elim (IHLK1 … HL12) -L1 #K2 #HLK2 #HK12 - elim (tpr_tps_ltpr … HV12 … HVW1 … HK12) -V1 /3 width=5/ + elim (tpr_tpss_ltpr … HK12 … HV12 … HVW1) -V1 /3 width=5/ ] qed. - -lemma ltpr_ltpss_conf: ∀L1,K1,d,e. L1 [d, e] ▶* K1 → ∀L2. L1 ➡ L2 → - ∃∃K2. L2 [d, e] ▶* K2 & K1 ➡ K2. -#L1 #K1 #d #e #H @(ltpss_ind … H) -K1 /2 width=3/ -#K #K1 #_ #HK1 #IHK #L2 #HL12 -elim (IHK … HL12) -L1 #K2 #HLK2 #HK2 -elim (ltpr_ltps_conf … HK1 … HK2) -K #K #HK2 #HK1 -lapply (ltpss_trans_eq … HLK2 HK2) -K2 /2 width=3/ -qed. 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 new file mode 100644 index 000000000..d0c29e726 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpsss.ma @@ -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/reducibility/tpr_tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma index 2b36d1018..ec95afc02 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma @@ -52,8 +52,7 @@ lemma tpr_tps_ltpr: ∀T1,T2. T1 ➡ T2 → elim (tpss_strip_neq … HTT2 … HTU2 ?) -T2 /2 width=1/ #T2 #HTT2 #HUT2 lapply (tps_lsubs_conf … HTT2 (L2. ⓑ{I} V2) ?) -HTT2 /2 width=1/ #HTT2 elim (ltpss_tps_conf … HTT2 (L2. ⓑ{I} VV2) (d + 1) e ?) -HTT2 /2 width=1/ #W2 #HTTW2 #HTW2 - lapply (tpss_lsubs_conf … HTTW2 (⋆. ⓑ{I} VV2) ?) -HTTW2 /2 width=1/ #HTTW2 - lapply (tpss_tps … HTTW2) -HTTW2 #HTTW2 + lapply (tps_lsubs_conf … HTTW2 (⋆. ⓑ{I} VV2) ?) -HTTW2 /2 width=1/ #HTTW2 lapply (tpss_lsubs_conf … HTW2 (L2. ⓑ{I} VV2) ?) -HTW2 /2 width=1/ #HTW2 lapply (tpss_trans_eq … HUT2 … HTW2) -T2 /3 width=5/ | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #e #X #H #L2 #HL12 diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltps.ma b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltps.ma deleted file mode 100644 index 162fa3898..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltps.ma +++ /dev/null @@ -1,65 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/substitution/ltps_ldrop.ma". -include "basic_2/static/aaa_lift.ma". - -(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) - -(* Properties about parallel substitution ***********************************) - -(* Note: lemma 500 *) -lemma aaa_ltps_tps_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. L1 [d, e] ▶ L2 → - ∀T2. L2 ⊢ T1 [d, e] ▶ T2 → L2 ⊢ T2 ÷ A. -#L1 #T1 #A #H elim H -L1 -T1 -A -[ #L1 #k #L2 #d #e #_ #T2 #H - >(tps_inv_sort1 … H) -H // -| #I #L1 #K1 #V1 #B #i #HLK1 #_ #IHV1 #L2 #d #e #HL12 #T2 #H - elim (tps_inv_lref1 … H) -H - [ #H destruct - elim (lt_or_ge i d) #Hdi - [ elim (ltps_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2 - elim (ltps_inv_tps11 … H ?) -H /2 width=1/ -Hdi #K2 #V2 #HK12 #HV12 #H destruct - /3 width=8/ - | elim (lt_or_ge i (d + e)) #Hide - [ elim (ltps_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HLK2 - elim (ltps_inv_tps21 … H ?) -H /2 width=1/ -Hdi -Hide #K2 #V2 #HK12 #HV12 #H destruct - /3 width=8/ - | -Hdi - lapply (ltps_ldrop_conf_ge … HL12 … HLK1 ?) -L1 // -Hide #HLK2 - /3 width=8/ - ] - ] - | * #K2 #V2 #Hdi #Hide #HLK2 #HVT2 - elim (ltps_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HL2K0 - elim (ltps_inv_tps21 … H ?) -H /2 width=1/ -Hdi -Hide #K0 #V0 #HK12 #HV12 #H destruct - lapply (ldrop_mono … HL2K0 … HLK2) -HL2K0 #H destruct - lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 /3 width=7/ - ] -| #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #L2 #d #e #HL12 #X #H - elim (tps_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /4 width=4/ -| #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #L2 #d #e #HL12 #X #H - elim (tps_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /4 width=4/ -| #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #L2 #d #e #HL12 #X #H - elim (tps_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /3 width=4/ -| #L1 #V1 #T1 #A #_ #_ #IHV1 #IHT1 #L2 #d #e #HL12 #X #H - elim (tps_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /3 width=4/ -] -qed. - -lemma aaa_ltps_conf: ∀L1,T,A. L1 ⊢ T ÷ A → ∀L2,d,e. L1 [d, e] ▶ L2 → L2 ⊢ T ÷ A. -/2 width=7/ qed. - -lemma aaa_tps_conf: ∀L,T1,A. L ⊢ T1 ÷ A → ∀T2,d,e. L ⊢ T1 [d, e] ▶ T2 → L ⊢ T2 ÷ A. -/2 width=7/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss.ma index 171dd6b9c..9de6b6541 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss.ma @@ -12,23 +12,65 @@ (* *) (**************************************************************************) -include "basic_2/unfold/ltpss.ma". -include "basic_2/static/aaa_ltps.ma". +include "basic_2/unfold/tpss_tpss.ma". +include "basic_2/unfold/ltpss_ldrop.ma". +include "basic_2/static/aaa_lift.ma". (* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) (* Properties about parallel unfold *****************************************) -lemma aaa_ltpss_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/ +(* Note: lemma 500 *) +lemma aaa_ltpss_tpss_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. L1 [d, e] ▶* L2 → + ∀T2. L2 ⊢ T1 [d, e] ▶* T2 → L2 ⊢ T2 ÷ A. +#L1 #T1 #A #H elim H -L1 -T1 -A +[ #L1 #k #L2 #d #e #_ #T2 #H + >(tpss_inv_sort1 … H) -H // +| #I #L1 #K1 #V1 #B #i #HLK1 #_ #IHV1 #L2 #d #e #HL12 #T2 #H + elim (tpss_inv_lref1 … H) -H + [ #H destruct + elim (lt_or_ge i d) #Hdi + [ elim (ltpss_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2 + elim (ltpss_inv_tpss11 … H ?) -H /2 width=1/ -Hdi #K2 #V2 #HK12 #HV12 #H destruct + /3 width=8/ + | elim (lt_or_ge i (d + e)) #Hide + [ elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HLK2 + elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K2 #V2 #HK12 #HV12 #H destruct + /3 width=8/ + | -Hdi + lapply (ltpss_ldrop_conf_ge … HL12 … HLK1 ?) -L1 // -Hide /3 width=8/ + ] + ] + | * #K2 #V2 #W2 #Hdi #Hide #HLK2 #HVW2 #HWT2 + elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HL2K0 + elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K0 #V0 #HK12 #HV12 #H destruct + lapply (ldrop_mono … HL2K0 … HLK2) -HL2K0 #H destruct + lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 #HLK2 + lapply (tpss_trans_eq … HV12 HVW2) -V2 /3 width=7/ + ] +| #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #L2 #d #e #HL12 #X #H + elim (tpss_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /4 width=4/ +| #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #L2 #d #e #HL12 #X #H + elim (tpss_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /4 width=4/ +| #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #L2 #d #e #HL12 #X #H + elim (tpss_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /3 width=4/ +| #L1 #V1 #T1 #A #_ #_ #IHV1 #IHT1 #L2 #d #e #HL12 #X #H + elim (tpss_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /3 width=4/ +] qed. -lemma aaa_tpss_conf: ∀L,T1,A. L ⊢ T1 ÷ A → ∀T2,d,e. L ⊢ T1 [d, e] ▶* T2 → L ⊢ T2 ÷ A. -#L #T1 #A #HT1 #T2 #d #e #HT12 -@(TC_Conf3 … HT1 ? HT12) /2 width=5/ -qed. +lemma aaa_ltpss_tps_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. L1 [d, e] ▶* L2 → + ∀T2. L2 ⊢ T1 [d, e] ▶ T2 → L2 ⊢ T2 ÷ A. +/3 width=7/ qed. -lemma aaa_ltpss_tpss_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. L1 [d, e] ▶* L2 → - ∀T2. L2 ⊢ T1 [d, e] ▶* T2 → L2 ⊢ T2 ÷ A. -/3 width=5/ qed. +lemma aaa_ltpss_conf: ∀L1,T,A. L1 ⊢ T ÷ A → + ∀L2,d,e. L1 [d, e] ▶* L2 → L2 ⊢ T ÷ A. +/2 width=7/ qed. + +lemma aaa_tpss_conf: ∀L,T1,A. L ⊢ T1 ÷ A → + ∀T2,d,e. L ⊢ T1 [d, e] ▶* T2 → L ⊢ T2 ÷ A. +/2 width=7/ qed. + +lemma aaa_tps_conf: ∀L,T1,A. L ⊢ T1 ÷ A → + ∀T2,d,e. L ⊢ T1 [d, e] ▶ T2 → L ⊢ T2 ÷ A. +/2 width=7/ 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 new file mode 100644 index 000000000..e3d048809 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpsss.ma @@ -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/unfold/ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma index a520f2e6f..1baa893e4 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma @@ -33,6 +33,16 @@ interpretation "parallel unfold (local environment)" (* Basic properties *********************************************************) +lemma ltpss_tps2: ∀L1,L2,I,V1,V2,e. + L1 [0, e] ▶* L2 → L2 ⊢ V1 [0, e] ▶ V2 → + L1. ⓑ{I} V1 [0, e + 1] ▶* L2. ⓑ{I} V2. +/3 width=1/ qed. + +lemma ltpss_tps1: ∀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. +/3 width=1/ qed. + lemma ltpss_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. @@ -47,6 +57,16 @@ lemma ltpss_tpss1_lt: ∀L1,L2,I,V1,V2,d,e. >(plus_minus_m_m d 1) /2 width=1/ qed. +lemma ltpss_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. +/3 width=1/ qed. + +lemma ltpss_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. +/3 width=1/ qed. + (* Basic_1: was by definition: csubst1_refl *) lemma ltpss_refl: ∀L,d,e. L [d, e] ▶* L. #L elim L -L // diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma index ce2271b70..d928491c2 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "basic_2/unfold/tpss_tpss.ma". +include "basic_2/unfold/tpss_alt.ma". include "basic_2/unfold/ltpss_tpss.ma". (* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************) @@ -42,6 +43,40 @@ lemma ltpss_tpss_trans_down: ∀L0,L1,T2,U2,d1,e1,d2,e2. d2 + e2 ≤ d1 → ] qed. +fact ltpss_tpss_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e. + L1 ⊢ T2 [d, e] ▶* U2 → ∀L0. L0 [d, e] ▶* L1 → + Y1 = L1 → X2 = T2 → L0 ⊢ T2 [d, e] ▶* U2. +#Y1 #X2 @(cw_wf_ind … Y1 X2) -Y1 -X2 #Y1 #X2 #IH +#L1 #T2 #U2 #d #e #H @(tpss_ind_alt … H) -L1 -T2 -U2 -d -e +[ // +| #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #HV12 #HVW2 #_ #L0 #HL10 #H1 #H2 destruct + lapply (ldrop_fwd_lw … HLK1) #H1 normalize in H1; + elim (ltpss_ldrop_trans_be … HL10 … HLK1 ? ?) -HL10 -HLK1 // /2 width=2/ #X #H #HLK0 + elim (ltpss_inv_tpss22 … H ?) -H /2 width=1/ #K0 #V0 #HK01 #HV01 #H destruct + lapply (tpss_fwd_tw … HV01) #H2 + lapply (transitive_le (#[K1] + #[V0]) … H1) -H1 /2 width=1/ -H2 #H + lapply (tpss_trans_eq … HV01 HV12) -V1 #HV02 + lapply (IH … HV02 … HK01 ? ?) -IH -HV02 -HK01 + [1,3: // |2,4: skip | normalize /2 width=1/ | /2 width=6/ ] +| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #L0 #HL0 #H1 #H2 destruct + lapply (tpss_lsubs_conf … HT12 (L. ⓑ{I} V1) ?) -HT12 /2 width=1/ #HT12 + lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=2/ ] #HV12 + lapply (IH … HT12 (L0. ⓑ{I} V1) ? ? ?) -IH -HT12 [1,3,5: /2 width=2/ |2,4: skip | normalize // ] -HL0 #HT12 + lapply (tpss_lsubs_conf … HT12 (L0. ⓑ{I} V2) ?) -HT12 /2 width=1/ +| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #L0 #HL0 #H1 #H2 destruct + lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=3/ ] + lapply (IH … HT12 … HL0 ? ?) -IH -HT12 [1,3,5: normalize // |2,4: skip ] -HL0 /2 width=1/ +] +qed. + +lemma ltpss_tpss_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 [d, e] ▶* U2 → + ∀L0. L0 [d, e] ▶* L1 → L0 ⊢ T2 [d, e] ▶* U2. +/2 width=5/ qed. + +lemma ltpss_tps_trans_eq: ∀L0,L1,T2,U2,d,e. L0 [d, e] ▶* L1 → + L1 ⊢ T2 [d, e] ▶ U2 → L0 ⊢ T2 [d, e] ▶* U2. +/3 width=3/ qed. + (* Main properties **********************************************************) fact ltpss_conf_aux: ∀K,K1,L1,d1,e1. K1 [d1, e1] ▶* L1 → diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tpss.ma index 2b1b8377c..0a49ef849 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tpss.ma @@ -100,39 +100,3 @@ lemma ltpss_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 → elim (IHTU2 … HL10) -IHTU2 -HL10 /3 width=5/ ] qed. - -fact ltpss_tps_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e. - L1 ⊢ T2 [d, e] ▶ U2 → ∀L0. L0 [d, e] ▶* L1 → - Y1 = L1 → X2 = T2 → L0 ⊢ T2 [d, e] ▶* U2. -#Y1 #X2 @(cw_wf_ind … Y1 X2) -Y1 -X2 #Y1 #X2 #IH -#L1 #T2 #U2 #d #e * -L1 -T2 -U2 -d -e -[ // -| #L1 #K1 #V1 #W1 #i #d #e #Hdi #Hide #HLK1 #HVW1 #L0 #HL10 #H1 #H2 destruct - lapply (ldrop_fwd_lw … HLK1) #H1 normalize in H1; - elim (ltpss_ldrop_trans_be … HL10 … HLK1 ? ?) -HL10 -HLK1 // /2 width=2/ #X #H #HLK0 - elim (ltpss_inv_tpss22 … H ?) -H /2 width=1/ #K0 #V0 #HK01 #HV01 #H destruct - lapply (tpss_fwd_tw … HV01) #H2 - lapply (transitive_le (#[K1] + #[V0]) … H1) -H1 /2 width=1/ -H2 #H - lapply (IH … HV01 … HK01 ? ?) -IH -HV01 -HK01 - [1,3: // |2,4: skip | normalize /2 width=1/ | /3 width=6/ ] -| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct - lapply (tps_lsubs_conf … HT12 (L. ⓑ{I} V1) ?) -HT12 /2 width=1/ #HT12 - lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=2/ ] #HV12 - lapply (IH … HT12 (L0. ⓑ{I} V1) ? ? ?) -IH -HT12 [1,3,5: /2 width=2/ |2,4: skip | normalize // ] -HL0 #HT12 - lapply (tpss_lsubs_conf … HT12 (L0. ⓑ{I} V2) ?) -HT12 /2 width=1/ -| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct - lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=3/ ] - lapply (IH … HT12 … HL0 ? ?) -IH -HT12 [1,3,5: normalize // |2,4: skip ] -HL0 /2 width=1/ -] -qed. - -lemma ltps_tps_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 [d, e] ▶ U2 → - ∀L0. L0 [d, e] ▶ L1 → L0 ⊢ T2 [d, e] ▶* U2. -/2 width=5/ qed. - -lemma ltps_tpss_trans_eq: ∀L0,L1,T2,U2,d,e. L0 [d, e] ▶ L1 → - L1 ⊢ T2 [d, e] ▶* U2 → L0 ⊢ T2 [d, e] ▶* U2. -#L0 #L1 #T2 #U2 #d #e #HL01 #H @(tpss_ind … H) -U2 // -#U #U2 #_ #HU2 #IHU @(tpss_trans_eq … IHU) /2 width=3/ -qed. -*) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss.ma new file mode 100644 index 000000000..58fb3e20b --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss.ma @@ -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/unfold/ltpsss_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_ldrop.ma new file mode 100644 index 000000000..e4923f9be --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_ldrop.ma @@ -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/unfold/ltpsss_ltpsss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_ltpsss.ma new file mode 100644 index 000000000..36a036727 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_ltpsss.ma @@ -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/unfold/ltpsss_tps.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_tps.ma new file mode 100644 index 000000000..3f0e25ae9 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_tps.ma @@ -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/unfold/ltpsss_tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_tpss.ma new file mode 100644 index 000000000..251a1a186 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_tpss.ma @@ -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/unfold/tpss_alt.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_alt.ma new file mode 100644 index 000000000..725dc57f1 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_alt.ma @@ -0,0 +1,101 @@ +(**************************************************************************) +(* ___ *) +(* ||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/tpss_lift.ma". + +(* PARALLEL UNFOLD ON TERMS *************************************************) + +(* alternative definition of tpss *) +inductive tpssa: nat → nat → lenv → relation term ≝ +| tpssa_atom : ∀L,I,d,e. tpssa d e L (⓪{I}) (⓪{I}) +| tpssa_subst: ∀L,K,V1,V2,W2,i,d,e. d ≤ i → i < d + e → + ⇩[0, i] L ≡ K. ⓓV1 → tpssa 0 (d + e - i - 1) K V1 V2 → + ⇧[0, i + 1] V2 ≡ W2 → tpssa d e L (#i) W2 +| tpssa_bind : ∀L,I,V1,V2,T1,T2,d,e. + tpssa d e L V1 V2 → tpssa (d + 1) e (L. ⓑ{I} V2) T1 T2 → + tpssa d e L (ⓑ{I} V1. T1) (ⓑ{I} V2. T2) +| tpssa_flat : ∀L,I,V1,V2,T1,T2,d,e. + tpssa d e L V1 V2 → tpssa d e L T1 T2 → + tpssa d e L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2) +. + +interpretation "parallel unfold (term) alternative" + 'PSubstStarAlt L T1 d e T2 = (tpssa d e L T1 T2). + +(* Basic properties *********************************************************) + +lemma tpssa_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶▶* T2 → + ∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ▶▶* T2. +#L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e +[ // +| #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12 + elim (ldrop_lsubs_ldrop1_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/ +| /4 width=1/ +| /3 width=1/ +] +qed. + +lemma tpssa_refl: ∀T,L,d,e. L ⊢ T [d, e] ▶▶* T. +#T elim T -T // +#I elim I -I /2 width=1/ +qed. + +lemma tpssa_tps_trans: ∀L,T1,T,d,e. L ⊢ T1 [d, e] ▶▶* T → + ∀T2. L ⊢ T [d, e] ▶ T2 → L ⊢ T1 [d, e] ▶▶* T2. +#L #T1 #T #d #e #H elim H -L -T1 -T -d -e +[ #L #I #d #e #X #H + elim (tps_inv_atom1 … H) -H // * /2 width=6/ +| #L #K #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK #_ #HVW2 #IHV12 #T2 #H + lapply (ldrop_fwd_ldrop2 … HLK) #H0LK + lapply (tps_weak … H 0 (d+e) ? ?) -H // #H + elim (tps_inv_lift1_be … H … H0LK … HVW2 ? ?) -H -H0LK -HVW2 // /3 width=6/ +| #L #I #V1 #V #T1 #T #d #e #_ #_ #IHV1 #IHT1 #X #H + elim (tps_inv_bind1 … H) -H #V2 #T2 #HV2 #HT2 #H destruct + lapply (tps_lsubs_conf … HT2 (L.ⓑ{I}V) ?) -HT2 /2 width=1/ #HT2 + lapply (IHV1 … HV2) -IHV1 -HV2 #HV12 + lapply (IHT1 … HT2) -IHT1 -HT2 #HT12 + lapply (tpssa_lsubs_conf … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/ +| #L #I #V1 #V #T1 #T #d #e #_ #_ #IHV1 #IHT1 #X #H + elim (tps_inv_flat1 … H) -H #V2 #T2 #HV2 #HT2 #H destruct /3 width=1/ +] +qed. + +lemma tpss_tpssa: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶* T2 → L ⊢ T1 [d, e] ▶▶* T2. +#L #T1 #T2 #d #e #H @(tpss_ind … H) -T2 // /2 width=3/ +qed. + +(* Basic inversion lemmas ***************************************************) + +lemma tpssa_tpss: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶▶* T2 → L ⊢ T1 [d, e] ▶* T2. +#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e // /2 width=6/ +qed-. + +lemma tpss_ind_alt: ∀R:ℕ→ℕ→lenv→relation term. + (∀L,I,d,e. R d e L (⓪{I}) (⓪{I})) → + (∀L,K,V1,V2,W2,i,d,e. d ≤ i → i < d + e → + ⇩[O, i] L ≡ K.ⓓV1 → K ⊢ V1 [O, d + e - i - 1] ▶* V2 → + ⇧[O, i + 1] V2 ≡ W2 → R O (d+e-i-1) K V1 V2 → R d e L #i W2 + ) → + (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 [d, e] ▶* V2 → + L.ⓑ{I}V2 ⊢ T1 [d + 1, e] ▶* T2 → R d e L V1 V2 → + R (d+1) e (L.ⓑ{I}V2) T1 T2 → R d e L (ⓑ{I}V1.T1) (ⓑ{I}V2.T2) + ) → + (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 [d, e] ▶* V2 → + L⊢ T1 [d, e] ▶* T2 → R d e L V1 V2 → + R d e L T1 T2 → R d e L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) + ) → + ∀d,e,L,T1,T2. L ⊢ T1 [d, e] ▶* T2 → R d e L T1 T2. +#R #H1 #H2 #H3 #H4 #d #e #L #T1 #T2 #H elim (tpss_tpssa … H) -L -T1 -T2 -d -e +// /3 width=1 by tpssa_tpss/ /3 width=7 by tpssa_tpss/ +qed-. -- 2.39.2