From 7bedf1797ba168f0742194b2add69575e5d4a5cd Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 13 Oct 2012 21:35:45 +0000 Subject: [PATCH] - parallel reduction for local environments: we proved the equivalence between the old context-sensitive version and the focalized version - as a result, the context-sensitive version disappears with its derivatives --- matita/matita/contribs/lambda_delta/Makefile | 12 ++-- .../computation/{lcprs_aaa.ma => cprs_aaa.ma} | 14 +--- .../basic_2/computation/cprs_cprs.ma | 10 +-- .../{cprs_lcpr.ma => cprs_lfpr.ma} | 6 +- .../{cprs_lcprs.ma => cprs_lfprs.ma} | 16 ++--- .../basic_2/computation/cprs_tstc.ma | 2 +- .../computation/{csn_lcpr.ma => csn_lfpr.ma} | 14 ++-- .../basic_2/computation/csn_tstc_vector.ma | 2 +- .../computation/{lcprs.ma => lfprs.ma} | 30 ++++---- .../basic_2/computation/lfprs_aaa.ma | 31 ++++++++ .../{lcprs_cprs.ma => lfprs_cprs.ma} | 10 +-- .../{lcprs_lcprs.ma => lfprs_lfprs.ma} | 24 +++---- .../basic_2/conversion/{lcpc.ma => lfpc.ma} | 18 ++--- .../conversion/{lcpc_lcpc.ma => lfpc_lfpc.ma} | 8 +-- .../lambda_delta/basic_2/dynamic/snv_aaa.ma | 2 +- .../equivalence/{lcpcs_aaa.ma => cpcs_aaa.ma} | 15 +--- .../lambda_delta/basic_2/equivalence/lcpcs.ma | 70 ------------------- .../basic_2/equivalence/lcpcs_lcprs.ma | 48 ------------- .../lambda_delta/basic_2/equivalence/lfpcs.ma | 70 +++++++++++++++++++ .../basic_2/equivalence/lfpcs_aaa.ma | 30 ++++++++ .../{lcpcs_lcpcs.ma => lfpcs_lfpcs.ma} | 34 ++++----- .../basic_2/equivalence/lfpcs_lfprs.ma | 48 +++++++++++++ .../lambda_delta/basic_2/grammar/cl_shift.ma | 2 +- .../basic_2/grammar/lenv_append.ma | 22 +++++- .../lambda_delta/basic_2/grammar/lenv_px.ma | 28 +++++++- .../contribs/lambda_delta/basic_2/notation.ma | 30 ++++---- .../lambda_delta/basic_2/reducibility/cfpr.ma | 55 +++++++++++++++ .../basic_2/reducibility/cfpr_aaa.ma | 29 ++++++++ .../basic_2/reducibility/cfpr_cpr.ma | 66 +++++++++++++++++ .../basic_2/reducibility/cfpr_ltpss.ma | 39 +++++++++++ .../reducibility/{lcpr_aaa.ma => cpr_aaa.ma} | 11 +-- .../basic_2/reducibility/cpr_lift.ma | 2 +- .../basic_2/reducibility/cpr_tpss.ma | 30 ++++++++ .../lambda_delta/basic_2/reducibility/fpr.ma | 42 ++++++----- .../basic_2/reducibility/fpr_cpr.ma | 61 ++++++++++++++++ .../basic_2/reducibility/{lcpr.ma => lfpr.ma} | 14 ++-- .../basic_2/reducibility/lfpr_aaa.ma | 25 +++++++ .../basic_2/reducibility/lfpr_alt.ma | 63 +++++++---------- .../reducibility/{lcpr_cpr.ma => lfpr_cpr.ma} | 8 +-- .../basic_2/reducibility/lfpr_fpr.ma | 31 ++++++++ .../{lcpr_lcpr.ma => lfpr_lfpr.ma} | 8 +-- .../lambda_delta/basic_2/reducibility/ltpr.ma | 13 ++++ .../lambda_delta/basic_2/reducibility/tpr.ma | 24 +++++-- .../basic_2/reducibility/xpr_aaa.ma | 2 +- .../lambda_delta/basic_2/unfold/ltpss_dx.ma | 5 ++ .../basic_2/unfold/ltpss_sn_ltpss_sn.ma | 11 +-- 46 files changed, 785 insertions(+), 350 deletions(-) rename matita/matita/contribs/lambda_delta/basic_2/computation/{lcprs_aaa.ma => cprs_aaa.ma} (71%) rename matita/matita/contribs/lambda_delta/basic_2/computation/{cprs_lcpr.ma => cprs_lfpr.ma} (89%) rename matita/matita/contribs/lambda_delta/basic_2/computation/{cprs_lcprs.ma => cprs_lfprs.ma} (83%) rename matita/matita/contribs/lambda_delta/basic_2/computation/{csn_lcpr.ma => csn_lfpr.ma} (93%) rename matita/matita/contribs/lambda_delta/basic_2/computation/{lcprs.ma => lfprs.ma} (60%) create mode 100644 matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_aaa.ma rename matita/matita/contribs/lambda_delta/basic_2/computation/{lcprs_cprs.ma => lfprs_cprs.ma} (79%) rename matita/matita/contribs/lambda_delta/basic_2/computation/{lcprs_lcprs.ma => lfprs_lfprs.ma} (60%) rename matita/matita/contribs/lambda_delta/basic_2/conversion/{lcpc.ma => lfpc.ma} (69%) rename matita/matita/contribs/lambda_delta/basic_2/conversion/{lcpc_lcpc.ma => lfpc_lfpc.ma} (81%) rename matita/matita/contribs/lambda_delta/basic_2/equivalence/{lcpcs_aaa.ma => cpcs_aaa.ma} (73%) delete mode 100644 matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs.ma delete mode 100644 matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_lcprs.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_aaa.ma rename matita/matita/contribs/lambda_delta/basic_2/equivalence/{lcpcs_lcpcs.ma => lfpcs_lfpcs.ma} (54%) create mode 100644 matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_lfprs.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_aaa.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_cpr.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_ltpss.ma rename matita/matita/contribs/lambda_delta/basic_2/reducibility/{lcpr_aaa.ma => cpr_aaa.ma} (76%) create mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_tpss.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr_cpr.ma rename matita/matita/contribs/lambda_delta/basic_2/reducibility/{lcpr.ma => lfpr.ma} (78%) create mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_aaa.ma rename matita/matita/contribs/lambda_delta/basic_2/reducibility/{lcpr_cpr.ma => lfpr_cpr.ma} (83%) create mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_fpr.ma rename matita/matita/contribs/lambda_delta/basic_2/reducibility/{lcpr_lcpr.ma => lfpr_lfpr.ma} (87%) diff --git a/matita/matita/contribs/lambda_delta/Makefile b/matita/matita/contribs/lambda_delta/Makefile index 964277d7f..a1bea3529 100644 --- a/matita/matita/contribs/lambda_delta/Makefile +++ b/matita/matita/contribs/lambda_delta/Makefile @@ -47,17 +47,17 @@ stats: $(PACKAGES:%=%.stats) %.stats: @printf '\x1B[1;40;37m' - @printf '%-15s %-42s' 'Statistics for:' $* + @printf '%-15s %-43s' 'Statistics for:' $* @printf '\x1B[0m\n' @printf '\x1B[1;40;35m' @printf '%-8s %6i' Chars $(CHARS) @printf ' %-8s %5i' Lines `cat $(MAS) | wc -l` @printf ' %-6s %3i' Pages `echo $$(($(CHARS) / 5120))` - @printf ' %-10s' '' + @printf ' %-11s' '' @printf '\x1B[0m\n' @printf '\x1B[1;40;36m' @printf '%-8s %6i' Sources `ls $(MAS) | wc -l` - @printf ' %-40s' '' + @printf ' %-41s' '' # @printf ' %-8s %5i' Objs `ls *.vo | wc -l` # @printf ' %-6s %3i' Files `ls *.v | wc -l` @printf '\x1B[0m\n' @@ -65,18 +65,18 @@ stats: $(PACKAGES:%=%.stats) @printf '%-8s %6i' Theorems `grep "theorem " $(MAS) | wc -l` @printf ' %-8s %5i' Lemmas `grep "lemma " $(MAS) | wc -l` @printf ' %-6s %3i' Facts `grep "fact " $(MAS) | wc -l` - @printf ' %-6s %3i' Proofs `grep qed $(MAS) | wc -l` + @printf ' %-6s %4i' Proofs `grep qed $(MAS) | wc -l` @printf '\x1B[0m\n' @printf '\x1B[1;40;33m' @printf '%-8s %6i' Defs `grep "definition\|let rec\|inductive\|record" $(MAS) | wc -l` - @printf ' %-40s' '' + @printf ' %-41s' '' # @printf ' %-8s %5i' Local `grep "Local" *.v | wc -l` @printf '\x1B[0m\n' @printf '\x1B[1;40;31m' @printf '%-8s %6i' Axioms `grep axiom $(MAS) | wc -l` @printf ' %-8s %5i' Comments `grep "(\*[^*:]*$$" $(MAS) | wc -l` @printf ' %-6s %3i' Marks `grep "(\*\*)" $(MAS) | wc -l` - @printf ' %-10s' '' + @printf ' %-11s' '' @printf '\x1B[0m\n' # summary #################################################################### diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_aaa.ma similarity index 71% rename from matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_aaa.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/cprs_aaa.ma index 73a6261e3..e04e3c784 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_aaa.ma @@ -12,24 +12,14 @@ (* *) (**************************************************************************) -include "basic_2/reducibility/lcpr_aaa.ma". +include "basic_2/reducibility/cpr_aaa.ma". include "basic_2/computation/cprs.ma". -include "basic_2/computation/lcprs.ma". -(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *************) +(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) (* Properties about atomic arity assignment on terms ************************) -lemma aaa_lcprs_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. L1 ⊢ ➡* L2 → L2 ⊢ T ⁝ A. -#L1 #T #A #HT #L2 #HL12 -@(TC_Conf3 … (λL,A. L ⊢ T ⁝ A) … HT ? HL12) /2 width=3/ -qed. - lemma aaa_cprs_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ T2 ⁝ A. #L #T1 #A #HT1 #T2 #HT12 @(TC_Conf3 … HT1 ? HT12) /2 width=3/ qed. - -lemma aaa_lcprs_cprs_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/computation/cprs_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma index d350f0977..8f94b0fa7 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma @@ -14,8 +14,8 @@ include "basic_2/reducibility/cpr_lift.ma". include "basic_2/reducibility/cpr_cpr.ma". -include "basic_2/reducibility/lcpr_cpr.ma". -include "basic_2/computation/cprs_lcpr.ma". +include "basic_2/reducibility/lfpr_cpr.ma". +include "basic_2/computation/cprs_lfpr.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) @@ -45,7 +45,7 @@ lemma cpr_abbr1: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV1 ⊢ T1 ➡ T lemma cpr_abbr2: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV2 ⊢ T1 ➡ T2 → ∀a. L ⊢ ⓓ{a}V1. T1 ➡* ⓓ{a}V2. T2. #L #V1 #V2 #HV12 #T1 #T2 #HT12 -lapply (lcpr_cpr_trans (L. ⓓV1) … HT12) /2 width=1/ +lapply (lfpr_cpr_trans (L. ⓓV1) … HT12) /2 width=1/ qed. (* Basic_1: was: pr3_strip *) @@ -117,7 +117,7 @@ lemma cprs_abbr2_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV2 ⊢ T1 #L #V1 #V2 #HV12 #T1 #T2 #HT12 #a @(cprs_ind_dx … HT12) -T1 [ /2 width=1/ | #T1 #T #HT1 #_ #IHT1 - lapply (lcpr_cpr_trans (L. ⓓV1) … HT1) -HT1 /2 width=1/ #HT1 + lapply (lfpr_cpr_trans (L. ⓓV1) … HT1) -HT1 /2 width=1/ #HT1 @(cprs_trans … IHT1) -IHT1 /2 width=1/ ] qed. @@ -142,7 +142,7 @@ lemma cprs_beta_dx: ∀L,V1,V2,W,T1,T2. qed. (* Basic_1: was only: pr3_pr2_pr3_t pr3_wcpr0_t *) -lemma lcpr_cprs_trans: ∀L1,L2. L1 ⊢ ➡ L2 → +lemma lcpr_cprs_trans: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2. #L1 #L2 #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 // #T #T2 #_ #HT2 #IHT2 diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcpr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lfpr.ma similarity index 89% rename from matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcpr.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lfpr.ma index 86f2a13ea..a06643577 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lfpr.ma @@ -14,12 +14,12 @@ include "basic_2/reducibility/ltpr_tps.ma". include "basic_2/reducibility/cpr_ltpss.ma". -include "basic_2/reducibility/lcpr.ma". +include "basic_2/reducibility/lfpr.ma". include "basic_2/computation/cprs.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) -(* Properties concerning context-sensitive parallel reduction on lenv's *****) +(* Properties concerning focalized parallel reduction on local environments *) 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. @@ -41,6 +41,6 @@ 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. +lemma lfpr_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/computation/cprs_lcprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lfprs.ma similarity index 83% rename from matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcprs.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lfprs.ma index 9131ba4c2..33620d01c 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lfprs.ma @@ -13,21 +13,21 @@ (**************************************************************************) include "basic_2/computation/cprs_cprs.ma". -include "basic_2/computation/lcprs_lcprs.ma". +include "basic_2/computation/lfprs_lfprs.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) -(* Properties exploiting context-senstive computation on local environments *) +(* Properties on focalized computation for local environments ***************) (* Basic_1: was just: pr3_pr3_pr3_t *) -lemma lcprs_cprs_trans: ∀L1,L2. L1 ⊢ ➡* L2 → +lemma lfprs_cprs_trans: ∀L1,L2. ⦃L1⦄ ➡* ⦃L2⦄ → ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2. -#L1 #L2 #HL12 @(lcprs_ind … HL12) -L2 // /3 width=3/ +#L1 #L2 #HL12 @(lfprs_ind … HL12) -L2 // /3 width=3/ qed. -lemma lcprs_cpr_trans: ∀L1,L2. L1 ⊢ ➡* L2 → +lemma lfprs_cpr_trans: ∀L1,L2. ⦃L1⦄ ➡* ⦃L2⦄ → ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡* T2. -/3 width=3 by lcprs_cprs_trans, inj/ qed. +/3 width=3 by lfprs_cprs_trans, inj/ qed. (* Advanced inversion lemmas ************************************************) @@ -44,9 +44,9 @@ lemma cprs_inv_abbr1: ∀a,L,V1,T1,U2. L ⊢ ⓓ{a}V1. T1 ➡* U2 → [ #V #V2 #T2 #HV0 #HV2 #HT02 #H destruct lapply (cpr_intro … HV0 … HV2) -HV2 #HV02 lapply (ltpr_cpr_trans (L.ⓓV0) … HT02) /2 width=1/ -V #HT02 - lapply (lcprs_cprs_trans (L. ⓓV1) … HT02) -HT02 /2 width=1/ /4 width=5/ + lapply (lfprs_cprs_trans (L. ⓓV1) … HT02) -HT02 /2 width=1/ /4 width=5/ | #T2 #HT02 #HUT2 - lapply (lcprs_cpr_trans (L.ⓓV1) … HT02) -HT02 /2 width=1/ -V0 #HT02 + lapply (lfprs_cpr_trans (L.ⓓV1) … HT02) -HT02 /2 width=1/ -V0 #HT02 lapply (cprs_trans … HT10 … HT02) -T0 /3 width=3/ ] | #U1 #HTU1 #HU01 diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma index ab8329cbc..f7afb8df7 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma @@ -14,7 +14,7 @@ include "basic_2/grammar/tstc.ma". include "basic_2/computation/cprs_lift.ma". -include "basic_2/computation/cprs_lcprs.ma". +include "basic_2/computation/cprs_lfprs.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lfpr.ma similarity index 93% rename from matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/csn_lfpr.ma index 58807c524..444dcf8f3 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lfpr.ma @@ -22,7 +22,7 @@ include "basic_2/computation/csn_alt.ma". (* Advanced properties ******************************************************) -lemma csn_lcpr_conf: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T. L1 ⊢ ⬊* T → L2 ⊢ ⬊* T. +lemma csn_lfpr_conf: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T. L1 ⊢ ⬊* T → L2 ⊢ ⬊* T. #L1 #L2 #HL12 #T #H @(csn_ind_alt … H) -T #T #_ #IHT @csn_intro #T0 #HLT0 #HT0 @IHT /2 width=2/ -IHT -HT0 /2 width=3/ @@ -37,7 +37,7 @@ elim (cpr_inv_abbr1 … H1) -H1 * lapply (ltpr_cpr_trans (L. ⓓV) … HLT1) /2 width=1/ -V0 #HLT1 elim (eq_false_inv_tpair_sn … H2) -H2 [ #HV1 @IHV // /2 width=1/ -HV1 - @(csn_lcpr_conf (L. ⓓV)) /2 width=1/ -HLV1 /2 width=3/ + @(csn_lfpr_conf (L. ⓓV)) /2 width=1/ -HLV1 /2 width=3/ | -IHV -HLV1 * #H destruct /3 width=1/ ] | -IHV -IHT -H2 #T0 #HLT0 #HT0 @@ -58,14 +58,14 @@ elim (cpr_inv_appl1 … H) -H * elim (eq_false_inv_beta … H2) -H2 [ -IHVT #HW0 @IHW -IHW [1,5: // |3: skip ] -HLW0 /2 width=1/ -HW0 @csn_abbr /2 width=3/ -HV - @(csn_lcpr_conf (L. ⓓV)) /2 width=1/ -V0 /2 width=3/ + @(csn_lfpr_conf (L. ⓓV)) /2 width=1/ -V0 /2 width=3/ | -IHW -HLW0 -HV -HT * #H #HVT0 destruct @(IHVT … HVT0) -IHVT -HVT0 // /2 width=1/ ] | -IHW -IHVT -H2 #b #V0 #W0 #T0 #T1 #HLV0 #HLT01 #H1 #H2 destruct - lapply (lcpr_cpr_trans (L. ⓓV) … HLT01) -HLT01 /2 width=1/ #HLT01 + lapply (lfpr_cpr_trans (L. ⓓV) … HLT01) -HLT01 /2 width=1/ #HLT01 @csn_abbr /2 width=3/ -HV - @(csn_lcpr_conf (L. ⓓV)) /2 width=1/ -V0 /2 width=3/ + @(csn_lfpr_conf (L. ⓓV)) /2 width=1/ -V0 /2 width=3/ | -IHW -IHVT -HV -HT -H2 #b #V0 #V1 #W0 #W1 #T0 #T1 #_ #_ #_ #_ #H destruct ] qed. @@ -108,9 +108,9 @@ elim (cpr_inv_appl1 … HL) -HL * | -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #T0 #T1 #_ #_ #H destruct | -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HLW01 #HLT01 #HV03 #H1 #H2 destruct lapply (cpr_lift (L. ⓓW0) … HV12 … HV03 HLV10) -HLV10 -HV12 -HV03 /2 width=1/ #HLV23 - lapply (lcpr_cpr_trans (L. ⓓW0) … HLT01) -HLT01 /2 width=1/ #HLT01 + lapply (lfpr_cpr_trans (L. ⓓW0) … HLT01) -HLT01 /2 width=1/ #HLT01 @csn_abbr /2 width=3/ -HV - @(csn_lcpr_conf (L. ⓓW0)) /2 width=1/ -W1 + @(csn_lfpr_conf (L. ⓓW0)) /2 width=1/ -W1 @(csn_cprs_trans … HVT) -HVT /2 width=1/ ] qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma index 91e3653f3..cfee668b9 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma @@ -14,7 +14,7 @@ include "basic_2/computation/acp_cr.ma". include "basic_2/computation/cprs_tstc_vector.ma". -include "basic_2/computation/csn_lcpr.ma". +include "basic_2/computation/csn_lfpr.ma". include "basic_2/computation/csn_vector.ma". (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERM VECTORS **********************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs.ma similarity index 60% rename from matita/matita/contribs/lambda_delta/basic_2/computation/lcprs.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/lfprs.ma index 7661358dc..a193f3c0a 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs.ma @@ -12,41 +12,39 @@ (* *) (**************************************************************************) -include "basic_2/reducibility/lcpr.ma". +include "basic_2/reducibility/lfpr.ma". -(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *************) +(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************) -definition lcprs: relation lenv ≝ TC … lcpr. +definition lfprs: relation lenv ≝ TC … lfpr. interpretation - "context-sensitive parallel computation (environment)" - 'CPRedStar L1 L2 = (lcprs L1 L2). + "focalized parallel computation (environment)" + 'FocalizedPRedStar L1 L2 = (lfprs L1 L2). (* Basic eliminators ********************************************************) -lemma lcprs_ind: ∀L1. ∀R:predicate lenv. R L1 → - (∀L,L2. L1 ⊢ ➡* L → L ⊢ ➡ L2 → R L → R L2) → - ∀L2. L1 ⊢ ➡* L2 → R L2. +lemma lfprs_ind: ∀L1. ∀R:predicate lenv. R L1 → + (∀L,L2. ⦃L1⦄ ➡* ⦃L⦄ → ⦃L⦄ ➡ ⦃L2⦄ → R L → R L2) → + ∀L2. ⦃L1⦄ ➡* ⦃L2⦄ → R L2. #L1 #R #HL1 #IHL1 #L2 #HL12 @(TC_star_ind … HL1 IHL1 … HL12) // qed-. -lemma lcprs_ind_dx: ∀L2. ∀R:predicate lenv. R L2 → - (∀L1,L. L1 ⊢ ➡ L → L ⊢ ➡* L2 → R L → R L1) → - ∀L1. L1 ⊢ ➡* L2 → R L1. +lemma lfprs_ind_dx: ∀L2. ∀R:predicate lenv. R L2 → + (∀L1,L. ⦃L1⦄ ➡ ⦃L⦄ → ⦃L⦄ ➡* ⦃L2⦄ → R L → R L1) → + ∀L1. ⦃L1⦄ ➡* ⦃L2⦄ → R L1. #L2 #R #HL2 #IHL2 #L1 #HL12 @(TC_star_ind_dx … HL2 IHL2 … HL12) // qed-. (* Basic properties *********************************************************) -lemma lcprs_refl: ∀L. L ⊢ ➡* L. +lemma lfprs_refl: ∀L. ⦃L⦄ ➡* ⦃L⦄. /2 width=1/ qed. -lemma lcprs_strap1: ∀L1,L,L2. - L1 ⊢ ➡* L → L ⊢ ➡ L2 → L1 ⊢ ➡* L2. +lemma lfprs_strap1: ∀L1,L,L2. ⦃L1⦄ ➡* ⦃L⦄ → ⦃L⦄ ➡ ⦃L2⦄ → ⦃L1⦄ ➡* ⦃L2⦄. /2 width=3/ qed. -lemma lcprs_strap2: ∀L1,L,L2. - L1 ⊢ ➡ L → L ⊢ ➡* L2 → L1 ⊢ ➡* L2. +lemma lfprs_strap2: ∀L1,L,L2. ⦃L1⦄ ➡ ⦃L⦄ → ⦃L⦄ ➡* ⦃L2⦄ → ⦃L1⦄ ➡* ⦃L2⦄. /2 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_aaa.ma new file mode 100644 index 000000000..a1337787c --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_aaa.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lfpr_aaa.ma". +include "basic_2/computation/lfprs.ma". + +(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************) + +(* Properties about atomic arity assignment on terms ************************) + +lemma aaa_lfprs_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. ⦃L1⦄ ➡* ⦃L2⦄ → L2 ⊢ T ⁝ A. +#L1 #T #A #HT #L2 #HL12 +@(TC_Conf3 … (λL,A. L ⊢ T ⁝ A) … HT ? HL12) /2 width=3/ +qed. +(* +(* Note: this should be rephrased in terms of fprs *) +lemma aaa_lfprs_cprs_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/computation/lcprs_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_cprs.ma similarity index 79% rename from matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_cprs.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_cprs.ma index 2a33e92e7..b0f7c4a94 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_cprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_cprs.ma @@ -12,16 +12,16 @@ (* *) (**************************************************************************) -include "basic_2/reducibility/lcpr_cpr.ma". +include "basic_2/reducibility/lfpr_cpr.ma". include "basic_2/computation/cprs.ma". -include "basic_2/computation/lcprs.ma". +include "basic_2/computation/lfprs.ma". -(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *************) +(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************) (* Advanced properties ******************************************************) -lemma lcprs_pair_dx: ∀I,L1,L2. L1 ⊢ ➡ L2 → ∀V1,V2. L2 ⊢ V1 ➡* V2 → - L1. ⓑ{I} V1 ⊢ ➡* L2. ⓑ{I} V2. +lemma lfprs_pair_dx: ∀I,L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀V1,V2. L2 ⊢ V1 ➡* V2 → + ⦃L1. ⓑ{I} V1⦄ ➡* ⦃L2. ⓑ{I} V2⦄. #I #L1 #L2 #HL12 #V1 #V2 #H @(cprs_ind … H) -V2 /3 width=1/ /3 width=5/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_lcprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_lfprs.ma similarity index 60% rename from matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_lcprs.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_lfprs.ma index 64851e801..e3866fd2e 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_lcprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_lfprs.ma @@ -12,29 +12,29 @@ (* *) (**************************************************************************) -include "basic_2/reducibility/lcpr_lcpr.ma". -include "basic_2/computation/lcprs_cprs.ma". +include "basic_2/reducibility/lfpr_lfpr.ma". +include "basic_2/computation/lfprs_cprs.ma". -(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *************) +(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************) (* Advanced properties ******************************************************) -lemma lcprs_strip: ∀L,L1. L ⊢ ➡* L1 → ∀L2. L ⊢ ➡ L2 → - ∃∃L0. L1 ⊢ ➡ L0 & L2 ⊢ ➡* L0. +lemma lfprs_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. +theorem lfprs_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. +theorem lfprs_trans: ∀L1,L. ⦃L1⦄ ➡* ⦃L⦄ → ∀L2. ⦃L⦄ ➡* ⦃L2⦄ → ⦃L1⦄ ➡* ⦃L2⦄. /2 width=3/ qed. -lemma lcprs_pair: ∀L1,L2. L1 ⊢ ➡* L2 → ∀V1,V2. L2 ⊢ V1 ➡* V2 → - ∀I. L1. ⓑ{I} V1 ⊢ ➡* L2. ⓑ{I} V2. -#L1 #L2 #H @(lcprs_ind … H) -L2 /2 width=1/ +lemma lfprs_pair: ∀L1,L2. ⦃L1⦄ ➡* ⦃L2⦄ → ∀V1,V2. L2 ⊢ V1 ➡* V2 → + ∀I. ⦃L1. ⓑ{I} V1⦄ ➡* ⦃L2. ⓑ{I} V2⦄. +#L1 #L2 #H @(lfprs_ind … H) -L2 /2 width=1/ #L #L2 #_ #HL2 #IHL1 #V1 #V2 #HV12 #I -@(lcprs_trans … (L.ⓑ{I}V1)) /2 width=1/ +@(lfprs_trans … (L.ⓑ{I}V1)) /2 width=1/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/conversion/lcpc.ma b/matita/matita/contribs/lambda_delta/basic_2/conversion/lfpc.ma similarity index 69% rename from matita/matita/contribs/lambda_delta/basic_2/conversion/lcpc.ma rename to matita/matita/contribs/lambda_delta/basic_2/conversion/lfpc.ma index 6ca577deb..273873abd 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/conversion/lcpc.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/conversion/lfpc.ma @@ -12,26 +12,26 @@ (* *) (**************************************************************************) -include "basic_2/reducibility/lcpr.ma". +include "basic_2/reducibility/lfpr.ma". -(* CONTEXT-SENSITIVE PARALLEL CONVERSION ON LOCAL ENVIRONMENTS **************) +(* FOCALIZED PARALLEL CONVERSION ON LOCAL ENVIRONMENTS **********************) -definition lcpc: relation lenv ≝ - λL1,L2. L1 ⊢ ➡ L2 ∨ L2 ⊢ ➡ L1. +definition lfpc: relation lenv ≝ + λL1,L2. ⦃L1⦄ ➡ ⦃L2⦄ ∨ ⦃L2⦄ ➡ ⦃L1⦄. interpretation - "context-sensitive parallel conversion (local environment)" - 'CPConv L1 L2 = (lcpc L1 L2). + "focalized parallel conversion (local environment)" + 'FocalizedPConv L1 L2 = (lfpc L1 L2). (* Basic properties *********************************************************) -lemma lcpc_refl: ∀L. L ⊢ ⬌ L. +lemma lfpc_refl: ∀L. ⦃L⦄ ⬌ ⦃L⦄. /2 width=1/ qed. -lemma lcpc_sym: ∀L1,L2. L1 ⊢ ⬌ L2 → L2 ⊢ ⬌ L1. +lemma lfpc_sym: ∀L1,L2. ⦃L1⦄ ⬌ ⦃L2⦄ → ⦃L2⦄ ⬌ ⦃L1⦄. #L1 #L2 * /2 width=1/ qed. -lemma lcpc_lcpr: ∀L1,L2. L1 ⊢ ⬌ L2 → ∃∃L. L1 ⊢ ➡ L & L2 ⊢ ➡ L. +lemma lfpc_lfpr: ∀L1,L2. ⦃L1⦄ ⬌ ⦃L2⦄ → ∃∃L. ⦃L1⦄ ➡ ⦃L⦄ & ⦃L2⦄ ➡ ⦃L⦄. #L1 #L2 * /2 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/conversion/lcpc_lcpc.ma b/matita/matita/contribs/lambda_delta/basic_2/conversion/lfpc_lfpc.ma similarity index 81% rename from matita/matita/contribs/lambda_delta/basic_2/conversion/lcpc_lcpc.ma rename to matita/matita/contribs/lambda_delta/basic_2/conversion/lfpc_lfpc.ma index d52bcd101..69e444adb 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/conversion/lcpc_lcpc.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/conversion/lfpc_lfpc.ma @@ -12,12 +12,12 @@ (* *) (**************************************************************************) -include "basic_2/conversion/lcpc.ma". +include "basic_2/conversion/lfpc.ma". -(* CONTEXT-SENSITIVE PARALLEL CONVERSION ON LOCAL ENVIRONMENTS **************) +(* FOCALIZED PARALLEL CONVERSION ON LOCAL ENVIRONMENTS **********************) (* Main properties **********************************************************) -theorem lcpc_conf: ∀L0,L1,L2. L0 ⊢ ⬌ L1 → L0 ⊢ ⬌ L2 → - ∃∃L. L1 ⊢ ⬌ L & L2 ⊢ ⬌ L. +theorem lfpc_conf: ∀L0,L1,L2. ⦃L0⦄ ⬌ ⦃L1⦄ → ⦃L0⦄ ⬌ ⦃L2⦄ → + ∃∃L. ⦃L1⦄ ⬌ ⦃L⦄ & ⦃L2⦄ ⬌ ⦃L⦄. /3 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_aaa.ma index f5953fedb..fd6645538 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_aaa.ma @@ -15,7 +15,7 @@ include "basic_2/computation/csn_aaa.ma". include "basic_2/computation/xprs_aaa.ma". include "basic_2/computation/xprs_cprs.ma". -include "basic_2/equivalence/lcpcs_aaa.ma". +include "basic_2/equivalence/cpcs_aaa.ma". include "basic_2/dynamic/snv.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_aaa.ma similarity index 73% rename from matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_aaa.ma rename to matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_aaa.ma index aa2b8ef2a..363b8acd3 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_aaa.ma @@ -12,24 +12,13 @@ (* *) (**************************************************************************) -include "basic_2/computation/lcprs_aaa.ma". +include "basic_2/computation/cprs_aaa.ma". include "basic_2/equivalence/cpcs_cpcs.ma". -include "basic_2/equivalence/lcpcs_lcpcs.ma". -(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON LOCAL EBVIRONMENTS *************) +(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) (* Main properties about atomic arity assignment on terms *******************) -theorem aaa_lcpcs_mono: ∀L1,L2. L1 ⊢ ⬌* L2 → - ∀T,A1. L1 ⊢ T ⁝ A1 → ∀A2. L2 ⊢ T ⁝ A2 → - A1 = A2. -#L1 #L2 #HL12 #T #A1 #HT1 #A2 #HT2 -elim (lcpcs_inv_lcprs … HL12) -HL12 #L #HL1 #HL2 -lapply (aaa_lcprs_conf … HT1 … HL1) -L1 #HT1 -lapply (aaa_lcprs_conf … HT2 … HL2) -L2 #HT2 -lapply (aaa_mono … HT1 … HT2) -L -T // -qed-. - theorem aaa_cpcs_mono: ∀L,T1,T2. L ⊢ T1 ⬌* T2 → ∀A1. L ⊢ T1 ⁝ A1 → ∀A2. L ⊢ T2 ⁝ A2 → A1 = A2. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs.ma deleted file mode 100644 index d30e504ba..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs.ma +++ /dev/null @@ -1,70 +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/conversion/lcpc.ma". - -(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON LOCAL EBVIRONMENTS *************) - -definition lcpcs: relation lenv ≝ TC … lcpc. - -interpretation "context-sensitive parallel equivalence (local environment)" - 'CPConvStar L1 L2 = (lcpcs L1 L2). - -(* Basic eliminators ********************************************************) - -lemma lcpcs_ind: ∀L1. ∀R:predicate lenv. R L1 → - (∀L,L2. L1 ⊢ ⬌* L → L ⊢ ⬌ L2 → R L → R L2) → - ∀L2. L1 ⊢ ⬌* L2 → R L2. -#L1 #R #HL1 #IHL1 #L2 #HL12 @(TC_star_ind … HL1 IHL1 … HL12) // -qed-. - -lemma lcpcs_ind_dx: ∀L2. ∀R:predicate lenv. R L2 → - (∀L1,L. L1 ⊢ ⬌ L → L ⊢ ⬌* L2 → R L → R L1) → - ∀L1. L1 ⊢ ⬌* L2 → R L1. -#L2 #R #HL2 #IHL2 #L1 #HL12 -@(TC_star_ind_dx … HL2 IHL2 … HL12) // -qed-. - -(* Basic properties *********************************************************) - -lemma lcpcs_refl: ∀L. L ⊢ ⬌* L. -/2 width=1/ qed. - -lemma lcpcs_strap1: ∀L1,L,L2. L1 ⊢ ⬌* L → L ⊢ ⬌ L2 → L1 ⊢ ⬌* L2. -/2 width=3/ qed. - -lemma lcpcs_strap2: ∀L1,L,L2. L1 ⊢ ⬌ L → L ⊢ ⬌* L2 → L1 ⊢ ⬌* L2. -/2 width=3/ qed. - -lemma lcpcs_lcpr_dx: ∀L1,L2. L1 ⊢ ➡ L2 → L1 ⊢ ⬌* L2. -/3 width=1/ qed. - -lemma lcpcs_lcpr_sn: ∀L1,L2. L2 ⊢ ➡ L1 → L1 ⊢ ⬌* L2. -/3 width=1/ qed. - -lemma lcpcs_lcpr_strap1: ∀L1,L. L1 ⊢ ⬌* L → ∀L2. L ⊢ ➡ L2 → L1 ⊢ ⬌* L2. -/3 width=3/ qed. - -lemma lcpcs_lcpr_strap2: ∀L1,L. L1 ⊢ ➡ L → ∀L2. L ⊢ ⬌* L2 → L1 ⊢ ⬌* L2. -/3 width=3/ qed. - -lemma lcpcs_lcpr_div: ∀L1,L. L1 ⊢ ⬌* L → ∀L2. L2 ⊢ ➡ L → L1 ⊢ ⬌* L2. -/3 width=3/ qed. - -lemma lcpcs_lcpr_conf: ∀L1,L. L ⊢ ➡ L1 → ∀L2. L ⊢ ⬌* L2 → L1 ⊢ ⬌* L2. -/3 width=3/ qed. - -lemma lcprs_comm: ∀L1,L2. L1 ⊢ ⬌* L2 → L2 ⊢ ⬌* L1. -#L1 #L2 #H @(lcpcs_ind … H) -L2 // /3 width=3/ -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_lcprs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_lcprs.ma deleted file mode 100644 index 4d2757a2e..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_lcprs.ma +++ /dev/null @@ -1,48 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/computation/lcprs.ma". -include "basic_2/equivalence/lcpcs.ma". - -(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *************) - -(* Properties about context sensitive computation on local environments *****) - -lemma lcpcs_lcprs_dx: ∀L1,L2. L1 ⊢ ➡* L2 → L1 ⊢ ⬌* L2. -#L1 #L2 #H @(lcprs_ind … H) -L2 /width=1/ /3 width=3/ -qed. - -lemma lcpcs_lcprs_sn: ∀L1,L2. L2 ⊢ ➡* L1 → L1 ⊢ ⬌* L2. -#L1 #L2 #H @(lcprs_ind_dx … H) -L2 /width=1/ /3 width=3/ -qed. - -lemma lcpcs_lcprs_strap1: ∀L1,L. L1 ⊢ ⬌* L → ∀L2. L ⊢ ➡* L2 → L1 ⊢ ⬌* L2. -#L1 #L #HL1 #L2 #H @(lcprs_ind … H) -L2 /width=1/ /2 width=3/ -qed. - -lemma lcpcs_lcprs_strap2: ∀L1,L. L1 ⊢ ➡* L → ∀L2. L ⊢ ⬌* L2 → L1 ⊢ ⬌* L2. -#L1 #L #H #L2 #HL2 @(lcprs_ind_dx … H) -L1 /width=1/ /2 width=3/ -qed. - -lemma lcpcs_lcprs_div: ∀L1,L. L1 ⊢ ⬌* L → ∀L2. L2 ⊢ ➡* L → L1 ⊢ ⬌* L2. -#L1 #L #HL1 #L2 #H @(lcprs_ind_dx … H) -L2 /width=1/ /2 width=3/ -qed. - -lemma lcpcs_lcprs_conf: ∀L1,L. L ⊢ ➡* L1 → ∀L2. L ⊢ ⬌* L2 → L1 ⊢ ⬌* L2. -#L1 #L #H #L2 #HL2 @(lcprs_ind … H) -L1 /width=1/ /2 width=3/ -qed. - -lemma lcprs_div: ∀L1,L. L1 ⊢ ➡* L → ∀L2. L2 ⊢ ➡* L → L1 ⊢ ⬌* L2. -#L1 #L #HL1 #L2 #H @(lcprs_ind_dx … H) -L2 /2 width=1/ /2 width=3/ -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs.ma new file mode 100644 index 000000000..c3cbf6c01 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs.ma @@ -0,0 +1,70 @@ +(**************************************************************************) +(* ___ *) +(* ||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/conversion/lfpc.ma". + +(* FOCALIZED PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *********************) + +definition lfpcs: relation lenv ≝ TC … lfpc. + +interpretation "focalized parallel equivalence (local environment)" + 'FocalizedPConvStar L1 L2 = (lfpcs L1 L2). + +(* Basic eliminators ********************************************************) + +lemma lfpcs_ind: ∀L1. ∀R:predicate lenv. R L1 → + (∀L,L2. ⦃L1⦄ ⬌* ⦃L⦄ → ⦃L⦄ ⬌ ⦃L2⦄ → R L → R L2) → + ∀L2. ⦃L1⦄ ⬌* ⦃L2⦄ → R L2. +#L1 #R #HL1 #IHL1 #L2 #HL12 @(TC_star_ind … HL1 IHL1 … HL12) // +qed-. + +lemma lfpcs_ind_dx: ∀L2. ∀R:predicate lenv. R L2 → + (∀L1,L. ⦃L1⦄ ⬌ ⦃L⦄ → ⦃L⦄ ⬌* ⦃L2⦄ → R L → R L1) → + ∀L1. ⦃L1⦄ ⬌* ⦃L2⦄ → R L1. +#L2 #R #HL2 #IHL2 #L1 #HL12 +@(TC_star_ind_dx … HL2 IHL2 … HL12) // +qed-. + +(* Basic properties *********************************************************) + +lemma lfpcs_refl: ∀L. ⦃L⦄ ⬌* ⦃L⦄. +/2 width=1/ qed. + +lemma lfpcs_strap1: ∀L1,L,L2. ⦃L1⦄ ⬌* ⦃L⦄ → ⦃L⦄ ⬌ ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +/2 width=3/ qed. + +lemma lfpcs_strap2: ∀L1,L,L2. ⦃L1⦄ ⬌ ⦃L⦄ → ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +/2 width=3/ qed. + +lemma lfpcs_lfpr_dx: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +/3 width=1/ qed. + +lemma lfpcs_lfpr_sn: ∀L1,L2. ⦃L2⦄ ➡ ⦃L1⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +/3 width=1/ qed. + +lemma lfpcs_lfpr_strap1: ∀L1,L. ⦃L1⦄ ⬌* ⦃L⦄ → ∀L2. ⦃L⦄ ➡ ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +/3 width=3/ qed. + +lemma lfpcs_lfpr_strap2: ∀L1,L. ⦃L1⦄ ➡ ⦃L⦄ → ∀L2. ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +/3 width=3/ qed. + +lemma lfpcs_lfpr_div: ∀L1,L. ⦃L1⦄ ⬌* ⦃L⦄ → ∀L2. ⦃L2⦄ ➡ ⦃L⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +/3 width=3/ qed. + +lemma lfpcs_lfpr_conf: ∀L1,L. ⦃L⦄ ➡ ⦃L1⦄ → ∀L2. ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +/3 width=3/ qed. + +lemma lfprs_comm: ∀L1,L2. ⦃L1⦄ ⬌* ⦃L2⦄ → ⦃L2⦄ ⬌* ⦃L1⦄. +#L1 #L2 #H @(lfpcs_ind … H) -L2 // /3 width=3/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_aaa.ma new file mode 100644 index 000000000..b7cea0b7a --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_aaa.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/computation/lfprs_aaa.ma". +include "basic_2/equivalence/lfpcs_lfpcs.ma". + +(* FOCALIZED PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *********************) + +(* Main properties about atomic arity assignment on terms *******************) + +theorem aaa_lfpcs_mono: ∀L1,L2. ⦃L1⦄ ⬌* ⦃L2⦄ → + ∀T,A1. L1 ⊢ T ⁝ A1 → ∀A2. L2 ⊢ T ⁝ A2 → + A1 = A2. +#L1 #L2 #HL12 #T #A1 #HT1 #A2 #HT2 +elim (lfpcs_inv_lfprs … HL12) -HL12 #L #HL1 #HL2 +lapply (aaa_lfprs_conf … HT1 … HL1) -L1 #HT1 +lapply (aaa_lfprs_conf … HT2 … HL2) -L2 #HT2 +lapply (aaa_mono … HT1 … HT2) -L -T // +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_lcpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_lfpcs.ma similarity index 54% rename from matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_lcpcs.ma rename to matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_lfpcs.ma index 876161bd2..fcbeb9b8a 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_lcpcs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_lfpcs.ma @@ -12,39 +12,39 @@ (* *) (**************************************************************************) -include "basic_2/computation/lcprs_lcprs.ma". -include "basic_2/conversion/lcpc_lcpc.ma". -include "basic_2/equivalence/lcpcs_lcprs.ma". +include "basic_2/computation/lfprs_lfprs.ma". +include "basic_2/conversion/lfpc_lfpc.ma". +include "basic_2/equivalence/lfpcs_lfprs.ma". -(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *************) +(* FOCALIZED PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *********************) (* Advanced inversion lemmas ************************************************) -lemma lcpcs_inv_lcprs: ∀L1,L2. L1 ⊢ ⬌* L2 → - ∃∃L. L1 ⊢ ➡* L & L2 ⊢ ➡* L. -#L1 #L2 #H @(lcpcs_ind … H) -L2 +lemma lfpcs_inv_lfprs: ∀L1,L2. ⦃L1⦄ ⬌* ⦃L2⦄ → + ∃∃L. ⦃L1⦄ ➡* ⦃L⦄ & ⦃L2⦄ ➡* ⦃L⦄. +#L1 #L2 #H @(lfpcs_ind … H) -L2 [ /3 width=3/ | #L #L2 #_ #HL2 * #L0 #HL10 elim HL2 -HL2 #HL2 #HL0 - [ elim (lcprs_strip … HL0 … HL2) -L #L #HL0 #HL2 - lapply (lcprs_strap1 … HL10 … HL0) -L0 /2 width=3/ - | lapply (lcprs_strap2 … HL2 … HL0) -L /2 width=3/ + [ elim (lfprs_strip … HL0 … HL2) -L #L #HL0 #HL2 + lapply (lfprs_strap1 … HL10 … HL0) -L0 /2 width=3/ + | lapply (lfprs_strap2 … HL2 … HL0) -L /2 width=3/ ] ] qed-. (* Advanced properties ******************************************************) -lemma lcpcs_strip: ∀L,L1. L ⊢ ⬌* L1 → ∀L2. L ⊢ ⬌ L2 → - ∃∃L0. L1 ⊢ ⬌ L0 & L2 ⊢ ⬌* L0. +lemma lfpcs_strip: ∀L,L1. ⦃L⦄ ⬌* ⦃L1⦄ → ∀L2. ⦃L⦄ ⬌ ⦃L2⦄ → + ∃∃L0. ⦃L1⦄ ⬌ ⦃L0⦄ & ⦃L2⦄ ⬌* ⦃L0⦄. /3 width=3/ qed. (* Main properties **********************************************************) -theorem lcpcs_trans: ∀L1,L. L1 ⊢ ⬌* L → ∀L2. L ⊢ ⬌* L2 → L1 ⊢ ⬌* L2. +theorem lfpcs_trans: ∀L1,L. ⦃L1⦄ ⬌* ⦃L⦄ → ∀L2. ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. /2 width=3/ qed. -theorem lcpcs_canc_sn: ∀L,L1,L2. L ⊢ ⬌* L1 → L ⊢ ⬌* L2 → L1 ⊢ ⬌* L2. -/3 width=3 by lcpcs_trans, lcprs_comm/ qed. +theorem lfpcs_canc_sn: ∀L,L1,L2. ⦃L⦄ ⬌* ⦃L1⦄ → ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +/3 width=3 by lfpcs_trans, lfprs_comm/ qed. -theorem lcpcs_canc_dx: ∀L,L1,L2. L1 ⊢ ⬌* L → L2 ⊢ ⬌* L → L1 ⊢ ⬌* L2. -/3 width=3 by lcpcs_trans, lcprs_comm/ qed. +theorem lfpcs_canc_dx: ∀L,L1,L2. ⦃L1⦄ ⬌* ⦃L⦄ → ⦃L2⦄ ⬌* ⦃L⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +/3 width=3 by lfpcs_trans, lfprs_comm/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_lfprs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_lfprs.ma new file mode 100644 index 000000000..baf2caf27 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_lfprs.ma @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/computation/lfprs.ma". +include "basic_2/equivalence/lfpcs.ma". + +(* FOCALIZED PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *********************) + +(* Properties on focalized computation for local environments ***************) + +lemma lfpcs_lfprs_dx: ∀L1,L2. ⦃L1⦄ ➡* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +#L1 #L2 #H @(lfprs_ind … H) -L2 /width=1/ /3 width=3/ +qed. + +lemma lfpcs_lfprs_sn: ∀L1,L2. ⦃L2⦄ ➡* ⦃L1⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +#L1 #L2 #H @(lfprs_ind_dx … H) -L2 /width=1/ /3 width=3/ +qed. + +lemma lfpcs_lfprs_strap1: ∀L1,L. ⦃L1⦄ ⬌* ⦃L⦄ → ∀L2. ⦃L⦄ ➡* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +#L1 #L #HL1 #L2 #H @(lfprs_ind … H) -L2 /width=1/ /2 width=3/ +qed. + +lemma lfpcs_lfprs_strap2: ∀L1,L. ⦃L1⦄ ➡* ⦃L⦄ → ∀L2. ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +#L1 #L #H #L2 #HL2 @(lfprs_ind_dx … H) -L1 /width=1/ /2 width=3/ +qed. + +lemma lfpcs_lfprs_div: ∀L1,L. ⦃L1⦄ ⬌* ⦃L⦄ → ∀L2. ⦃L2⦄ ➡* ⦃L⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +#L1 #L #HL1 #L2 #H @(lfprs_ind_dx … H) -L2 /width=1/ /2 width=3/ +qed. + +lemma lfpcs_lfprs_conf: ∀L1,L. ⦃L⦄ ➡* ⦃L1⦄ → ∀L2. ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +#L1 #L #H #L2 #HL2 @(lfprs_ind … H) -L1 /width=1/ /2 width=3/ +qed. + +lemma lfprs_div: ∀L1,L. ⦃L1⦄ ➡* ⦃L⦄ → ∀L2. ⦃L2⦄ ➡* ⦃L⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +#L1 #L #HL1 #L2 #H @(lfprs_ind_dx … H) -L2 /2 width=1/ /2 width=3/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_shift.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_shift.ma index 837b1c670..bbdc8e7d0 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_shift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_shift.ma @@ -26,7 +26,7 @@ interpretation "shift (closure)" 'Append L T = (shift L T). (* Basic properties *********************************************************) lemma shift_append_assoc: ∀L,K. ∀T:term. (L @@ K) @@ T = L @@ K @@ T. -#L #K elim K -K normalize // +#L #K elim K -K // normalize // qed. (* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma index 2f6932188..f58f96076 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma @@ -47,7 +47,8 @@ lemma append_inj_sn: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |K1| = |K2| → | #K1 #I1 #V1 #IH * normalize [ #L1 #L2 #_ append_length in H2; #H elim (plus_xySz_x_false … (sym_eq … H)) | #K2 #I2 #V2 #L1 #L2 #H1 #H2 destruct (**) (* destruct does not simplify well *) - elim (IH … e0 ?) -IH -H1 /2 width=1/ -H2 #H1 #H2 destruct /2 width=1/ + -H1 (**) (* destruct: the destucted equality is not erased *) + elim (IH … e0 ?) -IH // -H2 #H1 #H2 destruct /2 width=1/ ] ] qed-. @@ -100,3 +102,19 @@ lemma lenv_ind_dx: ∀R:predicate lenv. R ⋆ → (∀I,L,V. R L → R (⋆.ⓑ{I}V @@ L)) → ∀L. R L. /3 width=2 by lenv_ind_dx_aux/ qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma length_inv_pos_sn_append: ∀d,L. 1 + d = |L| → + ∃∃I,K,V. d = |K| & L = ⋆. ⓑ{I}V @@ K. +#d >commutative_plus @(nat_ind_plus … d) -d +[ #L #H elim (length_inv_pos_sn … H) -H #I #K #V #H1 #H2 destruct + >(length_inv_zero_sn … H1) -K + @(ex2_3_intro … (⋆)) // (**) (* explicit constructor *) +| #d #IHd #L #H elim (length_inv_pos_sn … H) -H #I #K #V #H1 #H2 destruct + >H1 in IHd; -H1 #IHd + elim (IHd K ?) -IHd // #J #L #W #H1 #H2 destruct + @(ex2_3_intro … (L.ⓑ{I}V)) // (**) (* explicit constructor *) + >append_length /2 width=1/ +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma index c3d05949f..41710626a 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma @@ -74,6 +74,32 @@ lemma lpx_fwd_length: ∀R,L1,L2. lpx R L1 L2 → |L1| = |L2|. #R #L1 #L2 #H elim H -L1 -L2 normalize // qed-. +(* Advanced inversion lemmas ************************************************) + +lemma lpx_inv_append1: ∀R,L1,K1,L. lpx R (K1 @@ L1) L → + ∃∃K2,L2. lpx R K1 K2 & lpx R L1 L2 & L = K2 @@ L2. +#R #L1 elim L1 -L1 normalize +[ #K1 #K2 #HK12 + @(ex3_2_intro … K2 (⋆)) // (**) (* explicit constructor, /2 width=5/ does not work *) +| #L1 #I #V1 #IH #K1 #X #H + elim (lpx_inv_pair1 … H) -H #L #V2 #H1 #HV12 #H destruct + elim (IH … H1) -IH -H1 #K2 #L2 #HK12 #HL12 #H destruct + @(ex3_2_intro … HK12) [2: /2 width=2/ | skip | // ] (* explicit constructor, /3 width=5/ does not work *) +] +qed-. + +lemma lpx_inv_append2: ∀R,L2,K2,L. lpx R L (K2 @@ L2) → + ∃∃K1,L1. lpx R K1 K2 & lpx R L1 L2 & L = K1 @@ L1. +#R #L2 elim L2 -L2 normalize +[ #K2 #K1 #HK12 + @(ex3_2_intro … K1 (⋆)) // (**) (* explicit constructor, /2 width=5/ does not work *) +| #L2 #I #V2 #IH #K2 #X #H + elim (lpx_inv_pair2 … H) -H #L #V1 #H1 #HV12 #H destruct + elim (IH … H1) -IH -H1 #K1 #L1 #HK12 #HL12 #H destruct + @(ex3_2_intro … HK12) [2: /2 width=2/ | skip | // ] (* explicit constructor, /3 width=5/ does not work *) +] +qed-. + (* Basic properties *********************************************************) lemma lpx_refl: ∀R. reflexive ? R → reflexive … (lpx R). @@ -125,7 +151,7 @@ lemma TC_lpx_pair_sn: ∀R. reflexive ? R → /4 width=5 by lpx_refl, lpx_pair, inj, step/ (**) (* too slow without trace *) qed. -lemma lpx_TC: ∀R,L1,L2. TC … (lpx R) L1 L2 → lpx (TC … R) L1 L2. +lemma lpx_TC: ∀R,L1,L2. TC … (lpx R) L1 L2 → lpx (TC … R) L1 L2. #R #L1 #L2 #H elim H -L2 /2 width=1/ /2 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma index ab02943a8..fbbb1085e 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma @@ -308,10 +308,6 @@ notation "hvbox( L ⊢ break term 46 T1 ➡ break term 46 T2 )" non associative with precedence 45 for @{ 'PRed $L $T1 $T2 }. -notation "hvbox( L1 ⊢ ➡ break term 46 L2 )" - non associative with precedence 45 - for @{ 'CPRed $L1 $L2 }. - notation "hvbox( ⦃ L1 ⦄ ➡ break ⦃ L2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPRed $L1 $L2 }. @@ -320,6 +316,10 @@ notation "hvbox( ⦃ L1, break T1 ⦄ ➡ break ⦃ L2 , break T2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPRed $L1 $T1 $L2 $T2 }. +notation "hvbox( L ⊢ break ⦃ L1, break T1 ⦄ ➡ break ⦃ L2 , break T2 ⦄ )" + non associative with precedence 45 + for @{ 'FocalizedPRed $L $L1 $T1 $L2 $T2 }. + notation "hvbox( ⦃ L1 ⦄ ➡ ➡ break ⦃ L2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPRedAlt $L1 $L2 }. @@ -330,27 +330,27 @@ notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 ➸ break [ g ] break (* Computation **************************************************************) -notation "hvbox( T1 ➡* break term 46 T2 )" +notation "hvbox( T1 ➡ * break term 46 T2 )" non associative with precedence 45 for @{ 'PRedStar $T1 $T2 }. -notation "hvbox( L ⊢ break term 46 T1 ➡* break term 46 T2 )" +notation "hvbox( L ⊢ break term 46 T1 ➡ * break term 46 T2 )" non associative with precedence 45 for @{ 'PRedStar $L $T1 $T2 }. -notation "hvbox( T1 ➡➡* break term 46 T2 )" +notation "hvbox( T1 ➡ ➡ * break term 46 T2 )" non associative with precedence 45 for @{ 'PRedStarAlt $T1 $T2 }. -notation "hvbox( L1 ⊢ ➡* break term 46 L2 )" +notation "hvbox( ⦃ L1 ⦄ ➡ * ⦃ L2 ⦄ )" non associative with precedence 45 - for @{ 'CPRedStar $L1 $L2 }. + for @{ 'FocalizedPRedStar $L1 $L2 }. -notation "hvbox( L ⊢ break term 46 T1 ➡* break 𝐍 ⦃ T2 ⦄ )" +notation "hvbox( L ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ T2 ⦄ )" non associative with precedence 45 for @{ 'PEval $L $T1 $T2 }. -notation "hvbox( ⬊ * term 46 T )" +notation "hvbox( ⬊ * term 46 T )" non associative with precedence 45 for @{ 'SN $T }. @@ -384,9 +384,9 @@ notation "hvbox( L ⊢ break term 46 T1 ⬌ break term 46 T2 )" non associative with precedence 45 for @{ 'PConv $L $T1 $T2 }. -notation "hvbox( T1 ⊢ ⬌ break term 46 T2 )" +notation "hvbox( ⦃ L1 ⦄ ⬌ ⦃ L2 ⦄ )" non associative with precedence 45 - for @{ 'CPConv $T1 $T2 }. + for @{ 'FocalizedPConv $L1 $L2 }. (* Equivalence **************************************************************) @@ -394,9 +394,9 @@ notation "hvbox( L ⊢ break term 46 T1 ⬌* break term 46 T2 )" non associative with precedence 45 for @{ 'PConvStar $L $T1 $T2 }. -notation "hvbox( T1 ⊢ ⬌* break term 46 T2 )" +notation "hvbox( ⦃ L1 ⦄ ⬌ * ⦃ L2 ⦄ )" non associative with precedence 45 - for @{ 'CPConvStar $T1 $T2 }. + for @{ 'FocalizedPConvStar $L1 $L2 }. (* Dynamic typing ***********************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr.ma new file mode 100644 index 000000000..95c01d19f --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr.ma @@ -0,0 +1,55 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/reducibility/cpr.ma". +include "basic_2/reducibility/fpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON CLOSURES *************************) + +definition cfpr: lenv → bi_relation lenv term ≝ + λL,L1,T1,L2,T2. |L1| = |L2| ∧ L ⊢ L1 @@ T1 ➡ L2 @@ T2. + +interpretation + "context-sensitive parallel reduction (closure)" + 'FocalizedPRed L L1 T1 L2 T2 = (cfpr L L1 T1 L2 T2). + +(* Basic properties *********************************************************) + +lemma cfpr_refl: ∀L. bi_reflexive … (cfpr L). +/2 width=1/ qed. + +lemma fpr_cfpr: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⋆ ⊢ ⦃L1, T1⦄ ➡ ⦃L2, T2⦄. +#L1 #L2 #T1 #T2 * /3 width=1/ +qed. + +(* Basic inversion lemmas ***************************************************) + +lemma cfpr_inv_atom1: ∀L,L2,T1,T2. L ⊢ ⦃⋆, T1⦄ ➡ ⦃L2, T2⦄ → L ⊢ T1 ➡ T2 ∧ L2 = ⋆. +#L #L2 #T1 #T2 * #H >(length_inv_zero_sn … H) /2 width=1/ +qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma fpr_inv_pair1_sn: ∀I,K1,L2,V1,T1,T2. ⦃⋆.ⓑ{I}V1@@K1, T1⦄ ➡ ⦃L2, T2⦄ → + ∃∃K2,V2. V1 ➡ V2 & + ⋆.ⓑ{I}V2 ⊢ ⦃K1, T1⦄ ➡ ⦃K2, T2⦄ & + L2 = ⋆.ⓑ{I}V2@@K2. +#I1 #K1 #L2 #V1 #T1 #T2 * >append_length #H +elim (length_inv_pos_sn_append … H) -H #I2 #K2 #V2 #HK12 #H destruct +>shift_append_assoc >shift_append_assoc normalize in ⊢ (%→?); #H +elim (tpr_inv_bind1 … H) -H * +[ #V0 #T #T0 #HV10 #HT1 #HT0 #H destruct /5 width=5/ +| #T0 #_ #_ #H destruct +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_aaa.ma new file mode 100644 index 000000000..f893a5c14 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_aaa.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||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_ltpss_sn.ma". +include "basic_2/reducibility/ltpr_aaa.ma". +include "basic_2/reducibility/cpr_aaa.ma". +include "basic_2/reducibility/cfpr_cpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON CLOSURES *************************) + +(* Properties about atomic arity assignment on terms ************************) + +lemma aaa_fpr_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → + ∀L2,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → L2 ⊢ T2 ⁝ A. +#L1 #T1 #A #HT1 #L2 #T2 #H +elim (fpr_inv_all … H) -H +/4 width=5 by aaa_cpr_conf, aaa_ltpr_conf, aaa_ltpss_sn_conf/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_cpr.ma new file mode 100644 index 000000000..f37cb5159 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_cpr.ma @@ -0,0 +1,66 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/unfold/ltpss_sn_alt.ma". +include "basic_2/reducibility/ltpr.ma". +include "basic_2/reducibility/cpr_tpss.ma". +include "basic_2/reducibility/cpr_cpr.ma". +include "basic_2/reducibility/cfpr_ltpss.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON CLOSURES *************************) + +(* Advanced properties ******************************************************) + +lemma fpr_all: ∀L1,L. L1 ➡ L → ∀L2,T1,T2. L ⊢ T1 ➡ T2 → + L ⊢ ▶* [0, |L|] L2 → ⦃L1, T1⦄ ➡ ⦃L2, T2⦄. +#L1 #L #H elim H -L1 -L +[ #L2 #T1 #T2 #HT12 #HL2 + lapply (ltpss_sn_inv_atom1 … HL2) -HL2 #H destruct + lapply (cpr_inv_atom … HT12) -HT12 /2 width=1/ +| #I #L1 #L #V1 #V #_ #HV1 #IH #X #T1 #T2 #HT12 #H + elim (ltpss_sn_inv_tpss21 … H ?) -H // append_length >append_length #H + lapply (injective_plus_r … H) -H #H + @(ex3_1_intro … (⋆.ⓑ{I}V@@Y)) append_length H -H >commutative_plus /3 width=1/ +] +qed-. + +lemma fpr_inv_all: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → + ∃∃L. L1 ➡ L & L ⊢ T1 ➡ T2 & L ⊢ ▶* [0, |L|] L2. +#L1 #L2 #T1 #T2 #H +lapply (fpr_cfpr … H) -H #H +elim (cfpr_inv_all … H) -H /2 width=4/ +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_ltpss.ma new file mode 100644 index 000000000..424911376 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_ltpss.ma @@ -0,0 +1,39 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpr_lift.ma". +include "basic_2/reducibility/cpr_ltpss.ma". +include "basic_2/reducibility/cfpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON CLOSURES *************************) + +(* Advanced inversion lemmas ************************************************) + +lemma cfpr_inv_pair1: ∀I,L,K1,L2,V1,T1,T2. L ⊢ ⦃⋆.ⓑ{I}V1@@K1, T1⦄ ➡ ⦃L2, T2⦄ → + ∃∃K2,V,V2. V1 ➡ V & L ⊢ V ▶* [0, |L|] V2 & + L.ⓑ{I}V ⊢ ⦃K1, T1⦄ ➡ ⦃K2, T2⦄ & + L2 = ⋆.ⓑ{I}V2@@K2. +* #L #K1 #L2 #V1 #T1 #T2 * >append_length #H +elim (length_inv_pos_sn_append … H) -H #I2 #K2 #V2 #HK12 #H destruct +>shift_append_assoc >shift_append_assoc normalize in ⊢ (??%%→?); #H +[ elim (cpr_inv_abbr1 … H) -H * + [ #V #V0 #T0 #HV1 #HV0 #HT10 #H destruct /3 width=7/ + | #T0 #_ #_ #H destruct + ] +| elim (cpr_inv_abst1 … H Abst V2) -H + #V #T * #V0 #HV10 #HV0 #HT1 #H destruct + lapply (ltpss_sn_cpr_trans (L.ⓛV0) … 0 (|L|+1) … HT1) -HT1 /2 width=1/ #HT12 + /3 width=7/ +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_aaa.ma similarity index 76% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_aaa.ma rename to matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_aaa.ma index d25abb4b5..7c1273334 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_aaa.ma @@ -15,20 +15,11 @@ include "basic_2/static/aaa_ltpss_sn.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 *************) +(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) (* 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/reducibility/cpr_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma index 43bce2b1a..b54510e8c 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma @@ -134,7 +134,7 @@ elim (cpr_inv_appl1 … H) -H * elim (simple_inv_bind … HT1) ] qed-. - + (* Relocation properties ****************************************************) (* Basic_1: was: pr2_lift *) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_tpss.ma new file mode 100644 index 000000000..e5afe8737 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_tpss.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/unfold/tpss_tpss.ma". +include "basic_2/reducibility/cpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) + +(* Properties on partial unfold for terms ***********************************) + +lemma cpr_tpss_trans: ∀L,T1,T. L ⊢ T1 ➡ T → + ∀T2. L ⊢ T ▶* [O, |L|] T2 → L ⊢ T1 ➡ T2. +#L #T1 #T * #T0 #HT10 #HT0 #T2 #HT2 +lapply (tpss_trans_eq … HT0 HT2) -T /2 width=3/ +qed. + +lemma cpr_tps_trans: ∀L,T1,T. L ⊢ T1 ➡ T → + ∀T2. L ⊢ T ▶ [O, |L|] T2 → L ⊢ T1 ➡ T2. +/3 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr.ma index b4c15e856..391061565 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr.ma @@ -14,13 +14,13 @@ include "basic_2/reducibility/tpr.ma". -(* FOCALIZED PARALLEL REDUCTION ON CLOSURES *********************************) +(* CONTEXT-FREE PARALLEL REDUCTION ON CLOSURES ******************************) definition fpr: bi_relation lenv term ≝ λL1,T1,L2,T2. |L1| = |L2| ∧ L1 @@ T1 ➡ L2 @@ T2. interpretation - "focalized parallel reduction (closure)" + "context-free parallel reduction (closure)" 'FocalizedPRed L1 T1 L2 T2 = (fpr L1 T1 L2 T2). (* Basic properties *********************************************************) @@ -28,31 +28,37 @@ interpretation lemma fpr_refl: bi_reflexive … fpr. /2 width=1/ qed. +lemma fpr_shift: ∀I1,I2,L1,L2,V1,V2,T1,T2. + ⦃L1, -ⓑ{I1}V1.T1⦄ ➡ ⦃L2, -ⓑ{I2}V2.T2⦄ → + ⦃L1.ⓑ{I1}V1, T1⦄ ➡ ⦃L2.ⓑ{I2}V2, T2⦄. +#I1 #I2 #L1 #L2 #V1 #V2 #T1 #T2 * #HL12 #HT12 +@conj // normalize // (**) (* explicit constructor *) +qed. + (* Basic inversion lemmas ***************************************************) lemma fpr_inv_atom1: ∀L2,T1,T2. ⦃⋆, T1⦄ ➡ ⦃L2, T2⦄ → T1 ➡ T2 ∧ L2 = ⋆. #L2 #T1 #T2 * #H lapply (length_inv_zero_sn … H) -H #H destruct /2 width=1/ qed-. -(* -lemma fpr_inv_pair1: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡ ⦃L2, T2⦄ → - ∃∃K2,V2. ⦃K1, -ⓑ{I}V1.T1⦄ ➡ ⦃K2, -ⓑ{I}V2.T2⦄ & - L2 = K2.ⓑ{I}V2. -#I1 #K1 #L2 #V1 #T1 #T2 * #H -elim (length_inv_pos_sn … H) -H #I2 #K2 #V2 #HK12 #H destruct #H -elim (tpr_fwd_shift_bind_minus … H) // #_ #H0 destruct /3 width=4/ -qed-. -*) + lemma fpr_inv_atom3: ∀L1,T1,T2. ⦃L1,T1⦄ ➡ ⦃⋆,T2⦄ → T1 ➡ T2 ∧ L1 = ⋆. #L1 #T1 #T2 * #H lapply (length_inv_zero_dx … H) -H #H destruct /2 width=1/ qed-. -(* -lemma fpr_inv_pair3: ∀I,L1,K2,V2,T1,T2. ⦃L1, T1⦄ ➡ ⦃K2.ⓑ{I}V2, T2⦄ → - ∃∃K1,V1. ⦃K1, -ⓑ{I}V1.T1⦄ ➡ ⦃K2, -ⓑ{I}V2.T2⦄ & - L1 = K1.ⓑ{I}V1. + +(* Basic forward lemmas *****************************************************) + +lemma fpr_fwd_pair1: ∀I1,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I1}V1, T1⦄ ➡ ⦃L2, T2⦄ → + ∃∃I2,K2,V2. ⦃K1, -ⓑ{I1}V1.T1⦄ ➡ ⦃K2, -ⓑ{I2}V2.T2⦄ & + L2 = K2.ⓑ{I2}V2. +#I1 #K1 #L2 #V1 #T1 #T2 * #H +elim (length_inv_pos_sn … H) -H #I2 #K2 #V2 #HK12 #H destruct /3 width=5/ +qed-. + +lemma fpr_fwd_pair3: ∀I2,L1,K2,V2,T1,T2. ⦃L1, T1⦄ ➡ ⦃K2.ⓑ{I2}V2, T2⦄ → + ∃∃I1,K1,V1. ⦃K1, -ⓑ{I1}V1.T1⦄ ➡ ⦃K2, -ⓑ{I2}V2.T2⦄ & + L1 = K1.ⓑ{I1}V1. #I2 #L1 #K2 #V2 #T1 #T2 * #H -elim (length_inv_pos_dx … H) -H #I1 #K1 #V1 #HK12 #H destruct #H -elim (tpr_fwd_shift_bind_minus … H) // #_ #H0 destruct /3 width=4/ +elim (length_inv_pos_dx … H) -H #I1 #K1 #V1 #HK12 #H destruct /3 width=5/ qed-. -*) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr_cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr_cpr.ma new file mode 100644 index 000000000..e034710b2 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr_cpr.ma @@ -0,0 +1,61 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cfpr_cpr.ma". + +(* FOCALIZED PARALLEL REDUCTION ON CLOSURES *********************************) + +(* Advanced propertis *******************************************************) + +lemma fpr_bind_sn: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ → ∀T1,T2. T1 ➡ T2 → + ∀a,I. ⦃L1, ⓑ{a,I}V1.T1⦄ ➡ ⦃L2, ⓑ{a,I}V2.T2⦄. +#L1 #L2 #V1 #V2 #H #T1 #T2 #HT12 #a #I +elim (fpr_inv_all … H) /3 width=4/ +qed. + +(* Advanced forward lemmas **************************************************) + +lemma fpr_fwd_shift_bind_minus: ∀I1,I2,L1,L2,V1,V2,T1,T2. + ⦃L1, -ⓑ{I1}V1.T1⦄ ➡ ⦃L2, -ⓑ{I2}V2.T2⦄ → + ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ ∧ I1 = I2. +* #I2 #L1 #L2 #V1 #V2 #T1 #T2 #H +elim (fpr_inv_all … H) -H #L #HL1 #H #HL2 +[ elim (cpr_inv_abbr1 … H) -H * + [ #V #V0 #T #HV1 #HV0 #_ #H destruct /4 width=4/ + | #T #_ #_ #H destruct + ] +| elim (cpr_inv_abst1 … H Abst V2) -H + #V #T #HV1 #_ #H destruct /3 width=4/ +] +qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma fpr_inv_pair1: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡ ⦃L2, T2⦄ → + ∃∃K2,V2. ⦃K1, V1⦄ ➡ ⦃K2, V2⦄ & + ⦃K1, -ⓑ{I}V1.T1⦄ ➡ ⦃K2, -ⓑ{I}V2.T2⦄ & + L2 = K2.ⓑ{I}V2. +#I1 #K1 #X #V1 #T1 #T2 #H +elim (fpr_fwd_pair1 … H) -H #I2 #K2 #V2 #HT12 #H destruct +elim (fpr_fwd_shift_bind_minus … HT12) #HV12 #H destruct /2 width=5/ +qed-. + +lemma fpr_inv_pair3: ∀I,L1,K2,V2,T1,T2. ⦃L1, T1⦄ ➡ ⦃K2.ⓑ{I}V2, T2⦄ → + ∃∃K1,V1. ⦃K1, V1⦄ ➡ ⦃K2, V2⦄ & + ⦃K1, -ⓑ{I}V1.T1⦄ ➡ ⦃K2, -ⓑ{I}V2.T2⦄ & + L1 = K1.ⓑ{I}V1. +#I2 #X #K2 #V2 #T1 #T2 #H +elim (fpr_fwd_pair3 … H) -H #I1 #K1 #V1 #HT12 #H destruct +elim (fpr_fwd_shift_bind_minus … HT12) #HV12 #H destruct /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/lfpr.ma similarity index 78% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr.ma rename to matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr.ma index ed93e5cf9..c8adecd25 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr.ma @@ -15,26 +15,26 @@ include "basic_2/unfold/ltpss_sn.ma". include "basic_2/reducibility/ltpr.ma". -(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************) +(* FOCALIZED PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ***********************) -definition lcpr: relation lenv ≝ +definition lfpr: relation lenv ≝ λL1,L2. ∃∃L. L1 ➡ L & L ⊢ ▶* [0, |L|] L2 . interpretation - "context-sensitive parallel reduction (environment)" - 'CPRed L1 L2 = (lcpr L1 L2). + "focalized parallel reduction (environment)" + 'FocalizedPRed L1 L2 = (lfpr L1 L2). (* Basic properties *********************************************************) -lemma lcpr_refl: ∀L. L ⊢ ➡ L. +lemma lfpr_refl: ∀L. ⦃L⦄ ➡ ⦃L⦄. /2 width=3/ qed. -lemma ltpss_sn_lcpr: ∀L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 → L1 ⊢ ➡ L2. +lemma ltpss_sn_lfpr: ∀L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 → ⦃L1⦄ ➡ ⦃L2⦄. /3 width=5/ qed. (* Basic inversion lemmas ***************************************************) -lemma lcpr_inv_atom1: ∀L2. ⋆ ⊢ ➡ L2 → L2 = ⋆. +lemma lfpr_inv_atom1: ∀L2. ⦃⋆⦄ ➡ ⦃L2⦄ → L2 = ⋆. #L2 * #L #HL >(ltpr_inv_atom1 … HL) -HL #HL2 >(ltpss_sn_inv_atom1 … HL2) -HL2 // qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_aaa.ma new file mode 100644 index 000000000..6f6c49df3 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_aaa.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/static/aaa_ltpss_sn.ma". +include "basic_2/reducibility/ltpr_aaa.ma". +include "basic_2/reducibility/lfpr.ma". + +(* FOCALIZED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS **********************) + +(* Properties about atomic arity assignment on terms ************************) + +lemma aaa_lfpr_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. ⦃L1⦄ ➡ ⦃L2⦄ → L2 ⊢ T ⁝ A. +#L1 #T #A #HT #L2 * /3 width=5/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_alt.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_alt.ma index bfb483781..adff7ad07 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_alt.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_alt.ma @@ -13,7 +13,8 @@ (**************************************************************************) include "basic_2/grammar/lenv_px_bi.ma". -include "basic_2/reducibility/fpr.ma". +include "basic_2/reducibility/fpr_cpr.ma". +include "basic_2/reducibility/lfpr_fpr.ma". (* FOCALIZED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS **********************) @@ -29,6 +30,15 @@ interpretation lemma lfpra_refl: reflexive … lfpra. /2 width=1/ qed. +lemma fpr_lfpra: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃L1⦄ ➡➡ ⦃L2⦄. +#L1 elim L1 -L1 +[ #L2 #T1 #T2 #H + elim (fpr_inv_atom1 … H) -H #_ #H destruct // +| #L1 #I #V1 #IH #L2 #T1 #T2 #H + elim (fpr_inv_pair1 … H) -H #L #V #HV1 #HL1 #H destruct /3 width=3/ +] +qed. + (* Basic inversion lemmas ***************************************************) lemma lfpra_inv_atom1: ∀L2. ⦃⋆⦄ ➡➡ ⦃L2⦄ → L2 = ⋆. @@ -47,48 +57,23 @@ lemma lfpra_inv_pair2: ∀L1,K2,I,V2. ⦃L1⦄ ➡➡ ⦃K2. ⓑ{I} V2⦄ → L1 = K1. ⓑ{I} V1. /2 width=1 by lpx_bi_inv_pair2/ qed-. +lemma lfpra_inv_fpr: ∀L1,L2. ⦃L1⦄ ➡➡ ⦃L2⦄ → ∀T.⦃L1, T⦄ ➡ ⦃L2, T⦄. +#L1 #L2 * -L1 -L2 // /3 width=1/ +qed-. + (* Basic forward lemmas *****************************************************) lemma lfpra_fwd_length: ∀L1,L2. ⦃L1⦄ ➡➡ ⦃L2⦄ → |L1| = |L2|. /2 width=2 by lpx_bi_fwd_length/ qed-. -(****************************************************************************) -(* -lemma fpr_lfpra: ∀L1,T1,L2,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃L1⦄ ➡➡ ⦃L2⦄. -#L1 #T1 @(cw_wf_ind … L1 T1) -L1 -T1 * -[ #T1 #_ #L2 #T2 #H - elim (fpr_inv_atom1 … H) -H #_ #H destruct // -| #L1 #I #V1 #T1 #IH #Y #X #H - elim (fpr_inv_pair1 … H) -H #L2 #V2 #HL12 #H destruct - @lpx_bi_pair - [ @(IH … HL12) - | @IH - - /3 width=4/ +(* Main properties **********************************************************) -lemma fpr_lfpra: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃L1⦄ ➡➡ ⦃L2⦄. -#L1 elim L1 -L1 -[ #L2 #T1 #T2 #H - elim (fpr_inv_atom1 … H) -H #_ #H destruct // -| #L1 #I #V1 #IH #L2 #T1 #T2 #H - elim (fpr_inv_pair1 … H) -H #L #V #HL1 #H destruct - @lpx_bi_pair /2 width=3/ - - /4 width=3/ - -(* -include "basic_2/reducibility/lcpr.ma". - -lemma lcpr_pair2: ∀L1,L2. L1 ⊢ ➡ L2 → ∀V1,V2. ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ → - ∀I. L1. ⓑ{I} V1 ⊢ ➡ L2. ⓑ{I} V2. -#L1 #L2 * #L #HL1 #HL2 #V1 #V2 * -#H1 #H2 #I -@(ex2_1_intro … (L.ⓑ{I}V1)) /2 width=1/ -@tpss_ - -(* -<(ltpss_fwd_length … HL2) /4 width=5/ +theorem lfpr_lfpra: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ⦃L1⦄ ➡➡ ⦃L2⦄. +#L1 #L2 #H +lapply (lfpr_inv_fpr … H (⋆0)) -H /2 width=3/ qed. -*) -*) -*) \ No newline at end of file + +theorem lfpra_lfpr: ∀L1,L2. ⦃L1⦄ ➡➡ ⦃L2⦄ → ⦃L1⦄ ➡ ⦃L2⦄. +#L1 #L2 #H +lapply (lfpra_inv_fpr … H (⋆0)) -H /2 width=3/ +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_cpr.ma similarity index 83% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_cpr.ma rename to matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_cpr.ma index 22f3a398c..2a40f58bd 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_cpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_cpr.ma @@ -14,14 +14,14 @@ include "basic_2/unfold/ltpss_sn_ltpss_sn.ma". include "basic_2/reducibility/cpr.ma". -include "basic_2/reducibility/lcpr.ma". +include "basic_2/reducibility/lfpr.ma". -(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************) +(* FOCALIZED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS **********************) (* Advanced properties ****************************************************) -lemma lcpr_pair: ∀L1,L2. L1 ⊢ ➡ L2 → ∀V1,V2. L2 ⊢ V1 ➡ V2 → - ∀I. L1. ⓑ{I} V1 ⊢ ➡ L2. ⓑ{I} V2. +lemma lfpr_pair_cpr: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀V1,V2. L2 ⊢ V1 ➡ V2 → + ∀I. ⦃L1. ⓑ{I} V1⦄ ➡ ⦃L2. ⓑ{I} V2⦄. #L1 #L2 * #L #HL1 #HL2 #V1 #V2 * <(ltpss_sn_fwd_length … HL2) #V #HV1 #HV2 #I lapply (ltpss_sn_tpss_trans_eq … HV2 … HL2) -HV2 #V2 diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_fpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_fpr.ma new file mode 100644 index 000000000..9a226be58 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_fpr.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lfpr.ma". +include "basic_2/reducibility/cfpr_cpr.ma". + +(* FOCALIZED PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ***********************) + +(* Inversion lemmas on context-free parallel reduction for closures *********) + +lemma fpr_lfpr: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃L1⦄ ➡ ⦃L2⦄. +#L1 #L2 #T1 #T2 #H +elim (fpr_inv_all … H) -H /2 width=3/ +qed. + +(* Inversion lemmas on context-free parallel reduction for closures *********) + +lemma lfpr_inv_fpr: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T. ⦃L1, T⦄ ➡ ⦃L2, T⦄. +#L1 #L2 * /2 width=4/ +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_lcpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_lfpr.ma similarity index 87% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_lcpr.ma rename to matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_lfpr.ma index d526b345e..7031e792b 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_lcpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_lfpr.ma @@ -14,14 +14,14 @@ include "basic_2/reducibility/ltpr_ltpss_sn.ma". include "basic_2/reducibility/ltpr_ltpr.ma". -include "basic_2/reducibility/lcpr.ma". +include "basic_2/reducibility/lfpr.ma". -(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ***************) +(* FOCALIZED PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ***********************) (* Main properties **********************************************************) -theorem lcpr_conf: ∀L0,L1,L2. L0 ⊢ ➡ L1 → L0 ⊢ ➡ L2 → - ∃∃L. L1 ⊢ ➡ L & L2 ⊢ ➡ L. +theorem lfpr_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 diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr.ma index 67986d336..a910ea7df 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr.ma @@ -28,6 +28,9 @@ interpretation lemma ltpr_refl: reflexive … ltpr. /2 width=1/ qed. +lemma ltpr_append: ∀K1,K2. K1 ➡ K2 → ∀L1,L2:lenv. L1 ➡ L2 → K1 @@ L1 ➡ K2 @@ L2. +/2 width=1/ qed. + (* Basic inversion lemmas ***************************************************) (* Basic_1: was: wcpr0_gen_sort *) @@ -51,4 +54,14 @@ lemma ltpr_inv_pair2: ∀L1,K2,I,V2. L1 ➡ K2. ⓑ{I} V2 → lemma ltpr_fwd_length: ∀L1,L2. L1 ➡ L2 → |L1| = |L2|. /2 width=2 by lpx_fwd_length/ qed-. +(* Advanced inversion lemmas ************************************************) + +lemma ltpr_inv_append1: ∀K1,L1. ∀L:lenv. K1 @@ L1 ➡ L → + ∃∃K2,L2. K1 ➡ K2 & L1 ➡ L2 & L = K2 @@ L2. +/2 width=1 by lpx_inv_append1/ qed-. + +lemma ltpr_inv_append2: ∀L:lenv. ∀K2,L2. L ➡ K2 @@ L2 → + ∃∃K1,L1. K1 ➡ K2 & L1 ➡ L2 & L = K1 @@ L1. +/2 width=1 by lpx_inv_append2/ qed-. + (* Basic_1: removed theorems 2: wcpr0_getl wcpr0_getl_back *) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma index 16353b450..b05484129 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma @@ -220,11 +220,25 @@ lemma tpr_fwd_shift1: ∀L1,T1,T. L1 @@ T1 ➡ T → ] ] qed-. - -lemma tpr_fwd_shift_bind_minus: ∀L1,L2. |L1| = |L2| → ∀I1,I2,V1,V2,T1,T2. - L1 @@ -ⓑ{I1}V1.T1 ➡ L2 @@ -ⓑ{I2}V2.T2 → - L1 𝟙 L2 ∧ I1 = I2. -#L1 #L2 #HL12 #I1 #I2 #V1 #V2 #T1 #T2 #H +*) + + +(* + >shift_append_assoc >shift_append_assoc >shift_append_assoc >shift_append_assoc normalize #H + elim (tpr_inv_bind1 … H) -H * + [ #V #T #T0 #HV1 #HT1 #HT0 #H destruct /2 width=1/ + | #T #_ #_ #H destruct + ] + + lapply (IH … HT12) + + + >shift_append_assoc >shift_append_assoc >shift_append_assoc #HT12 + lapply (shift_inj … HT12) -HT12 + + + + #L2 #HL12 #I1 #I2 #V1 #V2 #T1 #T2 #H elim (tpr_fwd_shift1 (L1.ⓑ{I1}V1) … H) -H #Y #X #HY #HX elim (ltop_inv_pair1 … HY) -HY #L #V #HL1 #H destruct elim (shift_inj (L2.ⓑ{I2}V2) … HX ?) -HX diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_aaa.ma index 051ef0514..bce096e3b 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_aaa.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/static/ssta_aaa.ma". -include "basic_2/reducibility/lcpr_aaa.ma". +include "basic_2/reducibility/cpr_aaa.ma". include "basic_2/reducibility/xpr.ma". (* EXTENDED PARALLEL REDUCTION ON TERMS *************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx.ma index ad0c002b4..d9d704221 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx.ma @@ -233,6 +233,11 @@ lemma ltpss_dx_append_le: ∀K1,K2,d. K1 ▶* [d, |K1| - d] K2 → L1 @@ K1 ▶* [d, |K1| - d + e] L2 @@ K2. /2 width=1 by ltpss_dx_append_le_aux/ qed. +lemma ltpss_dx_append_zero: ∀K1,K2. K1 ▶* [0, |K1|] K2 → + ∀L1,L2,e. L1 ▶* [0, e] L2 → + L1 @@ K1 ▶* [0, |K1| + e] L2 @@ K2. +/2 width=1/ qed. + lemma ltpss_dx_append_ge: ∀K1,K2,d,e. K1 ▶* [d, e] K2 → ∀L1,L2. L1 ▶* [d - |K1|, e] L2 → |K1| ≤ d → L1 @@ K1 ▶* [d, e] L2 @@ K2. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_ltpss_sn.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_ltpss_sn.ma index ef8e554d0..7aa2c5df2 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_ltpss_sn.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_ltpss_sn.ma @@ -70,14 +70,17 @@ qed. (* Advanced forward lemmas **************************************************) lemma tps_fwd_shift1: ∀L1,L,T1,T,d,e. L ⊢ L1 @@ T1 ▶ [d, e] T → - ∃∃L2,T2. L @@ L1 ⊢ ▶* [d + |L1|, e] L @@ L2 & T = L2 @@ T2. + ∃∃L2,T2. L @@ L1 ⊢ ▶* [d + |L1|, e] L @@ L2 & + L @@ L2 ⊢ T1 ▶ [d + |L1|, e] T2 & + T = L2 @@ T2. #L1 @(lenv_ind_dx … L1) -L1 -[ #L #T1 #T #d #e #_ @ex2_2_intro [3: // |4: // |1,2: skip ] (**) (* /2 width=4/ does not work *) +[ #L #T1 #T #d #e #HT1 + @ex3_2_intro [3: // |5: // |4: normalize /2 width=1/ |1,2: skip ] (**) (* /2 width=4/ does not work *) | #I #L1 #V1 #IH #L #T1 #T #d #e >shift_append_assoc #H elim (tps_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct - elim (IH … HT12) -IH -T1 #L2 #T #HL12 #H destruct + elim (IH … HT12) -IH -HT12 #L2 #T #HL12 #HT1 #H destruct append_length