From a631aba16617079b3f4cba2ec5a5ef651090e48c Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 4 Apr 2012 18:47:28 +0000 Subject: [PATCH] - some work on context equivalence of atomic arity assignment --- .../basic_2/computation/cprs_cprs.ma | 17 ++++ .../lambda_delta/basic_2/computation/lcprs.ma | 10 ++- .../basic_2/computation/lcprs_lcprs.ma | 11 ++- .../lambda_delta/basic_2/conversion/lcpc.ma | 37 ++++++++ .../basic_2/conversion/lcpc_lcpc.ma | 23 +++++ .../basic_2/equivalence/cpcs_cpcs.ma | 12 ++- .../lambda_delta/basic_2/equivalence/lcpcs.ma | 70 +++++++++++++++ .../basic_2/equivalence/lcpcs_aaa.ma | 41 +++++++++ .../basic_2/equivalence/lcpcs_lcpcs.ma | 50 +++++++++++ .../basic_2/equivalence/lcpcs_lcprs.ma | 48 +++++++++++ .../basic_2/grammar/lenv_weight.ma | 11 +++ .../contribs/lambda_delta/basic_2/notation.ma | 8 +- .../lambda_delta/basic_2/reducibility/cpr.ma | 2 +- .../basic_2/reducibility/cpr_lift.ma | 9 ++ .../basic_2/reducibility/lcpr_lcpr.ma | 39 +++++++++ .../basic_2/reducibility/ltpr_ltpr.ma | 29 +++++++ .../basic_2/reducibility/ltpr_ltpss.ma | 45 ++++++++++ .../basic_2/substitution/tps_lift.ma | 31 ++++--- .../lambda_delta/basic_2/unfold/ltpss.ma | 6 ++ .../basic_2/unfold/ltpss_ltpss.ma | 85 +++++++++++++++++++ .../lambda_delta/basic_2/unfold/tpss_lift.ma | 7 ++ 21 files changed, 571 insertions(+), 20 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/basic_2/conversion/lcpc.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/conversion/lcpc_lcpc.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_aaa.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_lcpcs.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_lcprs.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_lcpr.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpr.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpss.ma 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 0104d8b27..85b391d2d 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 @@ -21,6 +21,14 @@ include "basic_2/computation/cprs_lcpr.ma". (* Advanced properties ******************************************************) +lemma cprs_abst_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀V,T1,T2. + L.ⓛV ⊢ T1 ➡* T2 → L ⊢ ⓛV1. T1 ➡* ⓛV2. T2. +#L #V1 #V2 #HV12 #V #T1 #T2 #HT12 @(cprs_ind … HT12) -T2 +[ /3 width=2/ +| /3 width=6 by cprs_strap1, cpr_abst/ (**) (* /3 width=6/ is too slow *) +] +qed. + lemma cprs_abbr1_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV1 ⊢ T1 ➡* T2 → L ⊢ ⓓV1. T1 ➡* ⓓV2. T2. #L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cprs_ind_dx … HT12) -T1 @@ -88,6 +96,15 @@ lemma cprs_flat: ∀I,L,T1,T2. L ⊢ T1 ➡* T2 → ∀V1,V2. L ⊢ V1 ➡* V2 @(cprs_trans … IHV1) -IHV1 /2 width=1/ qed. +lemma cprs_abst: ∀L,V1,V2. L ⊢ V1 ➡* V2 → ∀V,T1,T2. + L.ⓛV ⊢ T1 ➡* T2 → L ⊢ ⓛV1. T1 ➡* ⓛV2. T2. +#L #V1 #V2 #HV12 #V #T1 #T2 #HT12 @(cprs_ind … HV12) -V2 +[ lapply (cprs_lsubs_conf … HT12 (L.ⓛV1) ?) -HT12 /2 width=2/ +| #V0 #V2 #_ #HV02 #IHV01 + @(cprs_trans … IHV01) -V1 /2 width=2/ +] +qed. + lemma cprs_abbr1: ∀L,V1,T1,T2. L. ⓓV1 ⊢ T1 ➡* T2 → ∀V2. L ⊢ V1 ➡* V2 → L ⊢ ⓓV1. T1 ➡* ⓓV2. T2. #L #V1 #T1 #T2 #HT12 #V2 #HV12 @(cprs_ind … HV12) -V2 /2 width=1/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs.ma index 312ededfa..7661358dc 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs.ma @@ -27,7 +27,15 @@ interpretation lemma lcprs_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) // +#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. +#L2 #R #HL2 #IHL2 #L1 #HL12 +@(TC_star_ind_dx … HL2 IHL2 … HL12) // qed-. (* Basic properties *********************************************************) 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 03e85b8db..344eae154 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,11 +11,20 @@ (* 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 → + ∃∃L0. L1 ⊢ ➡ L0 & L2 ⊢ ➡* L0. +(* +/3 width=3/ qed. +*) (* Main properties **********************************************************) theorem lcprs_trans: ∀L1,L. L1 ⊢ ➡* L → ∀L2. L ⊢ ➡* L2 → L1 ⊢ ➡* L2. diff --git a/matita/matita/contribs/lambda_delta/basic_2/conversion/lcpc.ma b/matita/matita/contribs/lambda_delta/basic_2/conversion/lcpc.ma new file mode 100644 index 000000000..6ca577deb --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/conversion/lcpc.ma @@ -0,0 +1,37 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/reducibility/lcpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL CONVERSION ON LOCAL ENVIRONMENTS **************) + +definition lcpc: relation lenv ≝ + λL1,L2. L1 ⊢ ➡ L2 ∨ L2 ⊢ ➡ L1. + +interpretation + "context-sensitive parallel conversion (local environment)" + 'CPConv L1 L2 = (lcpc L1 L2). + +(* Basic properties *********************************************************) + +lemma lcpc_refl: ∀L. L ⊢ ⬌ L. +/2 width=1/ qed. + +lemma lcpc_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. +#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/lcpc_lcpc.ma new file mode 100644 index 000000000..d52bcd101 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/conversion/lcpc_lcpc.ma @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||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 CONVERSION ON LOCAL ENVIRONMENTS **************) + +(* Main properties **********************************************************) + +theorem lcpc_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/equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma index b80429770..6054aaeb3 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma @@ -76,7 +76,7 @@ elim (cprs_inv_lift … HLK … HTU2 … HU2) -L -U2 #X #HXU >(lift_inj … HXU … HTU) -X -U -d -e /2 width=3/ qed-. -(* advanced properties ******************************************************) +(* Advanced properties ******************************************************) (* Basic_1: was only: pc3_thin_dx *) lemma cpcs_flat: ∀L,V1,V2. L ⊢ V1 ⬌* V2 → ∀T1,T2. L ⊢ T1 ⬌* T2 → @@ -86,6 +86,14 @@ elim (cpcs_inv_cprs … HV12) -HV12 #V #HV1 #HV2 elim (cpcs_inv_cprs … HT12) -HT12 /3 width=5 by cprs_flat, cprs_div/ (**) (* /3 width=5/ is too slow *) qed. +lemma cpcs_abst: ∀L,V1,V2. L ⊢ V1 ⬌* V2 → + ∀V,T1,T2. L.ⓛV ⊢ T1 ⬌* T2 → L ⊢ ⓛV1. T1 ⬌* ⓛV2. T2. +#L #V1 #V2 #HV12 #V #T1 #T2 #HT12 +elim (cpcs_inv_cprs … HV12) -HV12 +elim (cpcs_inv_cprs … HT12) -HT12 +/3 width=6 by cprs_div, cprs_abst/ (**) (* /3 width=6/ is a bit slow *) +qed. + lemma cpcs_abbr_dx: ∀L,V,T1,T2. L.ⓓV ⊢ T1 ⬌* T2 → L ⊢ ⓓV. T1 ⬌* ⓓV. T2. #L #V #T1 #T2 #HT12 elim (cpcs_inv_cprs … HT12) -HT12 /3 width=5 by cprs_div, cprs_abbr1/ (**) (* /3 width=5/ is a bit slow *) @@ -96,7 +104,7 @@ lemma cpcs_abbr_sn: ∀L,V1,V2,T. L ⊢ V1 ⬌* V2 → L ⊢ ⓓV1. T ⬌* ⓓV2 elim (cpcs_inv_cprs … HV12) -HV12 /3 width=5 by cprs_div, cprs_abbr1/ (**) (* /3 width=5/ is a bit slow *) qed. -(* Basic_1: was: pc3_gen_lift *) +(* Basic_1: was: pc3_lift *) lemma cpcs_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K → ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀T2,U2. ⇧[d, e] T2 ≡ U2 → K ⊢ T1 ⬌* T2 → L ⊢ U1 ⬌* U2. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs.ma new file mode 100644 index 000000000..d30e504ba --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs.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/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_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_aaa.ma new file mode 100644 index 000000000..17c9fb939 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_aaa.ma @@ -0,0 +1,41 @@ +(**************************************************************************) +(* ___ *) +(* ||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_aaa.ma". +include "basic_2/equivalence/cpcs_cpcs.ma". +include "basic_2/equivalence/lcpcs_lcpcs.ma". + +(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON LOCAL EBVIRONMENTS *************) + +(* 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. +#L #T1 #T2 #HT12 #A1 #HA1 #A2 #HA2 +elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2 +lapply (aaa_cprs_conf … HA1 … HT1) -T1 #HA1 +lapply (aaa_cprs_conf … HA2 … HT2) -T2 #HA2 +lapply (aaa_mono … HA1 … HA2) -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/lcpcs_lcpcs.ma new file mode 100644 index 000000000..cc26a5647 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_lcpcs.ma @@ -0,0 +1,50 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/computation/lcprs_lcprs.ma". +include "basic_2/conversion/lcpc_lcpc.ma". +include "basic_2/equivalence/lcpcs_lcprs.ma". + +(* CONTEXT-SENSITIVE 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 +[ /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/ + ] +] +qed-. + +(* Advanced properties ******************************************************) + +lemma lcpcs_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. +/2 width=3/ qed. + +theorem lcpcs_canc_sn: ∀L,L1,L2. L ⊢ ⬌* L1 → L ⊢ ⬌* L2 → L1 ⊢ ⬌* L2. +/3 width=3/ qed. + +theorem lcpcs_canc_dx: ∀L,L1,L2. L1 ⊢ ⬌* L → L2 ⊢ ⬌* L → L1 ⊢ ⬌* 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 new file mode 100644 index 000000000..4d2757a2e --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_lcprs.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/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/grammar/lenv_weight.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma index 990b5c5d0..48ef29453 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma @@ -24,5 +24,16 @@ let rec lw L ≝ match L with interpretation "weight (local environment)" 'Weight L = (lw L). +(* Basic properties *********************************************************) + +lemma lw_pair: ∀I,L,V. #[L] < #[(L.ⓑ{I}V)]. +/3 width=1/ qed. + +(* Basic eliminators ********************************************************) + +axiom lw_wf_ind: ∀R:predicate lenv. + (∀L2. (∀L1. #[L1] < #[L2] → R L1) → R L2) → + ∀L. R L. + (* Basic_1: removed theorems 2: clt_cong clt_head clt_thead *) (* Basic_1: note: clt_thead should be renamed clt_ctail *) diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma index 9ec72083a..06d7d9ed3 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma @@ -308,9 +308,9 @@ notation "hvbox( L ⊢ break term 90 T1 ⬌ break T2 )" non associative with precedence 45 for @{ 'PConv $L $T1 $T2 }. -notation "hvbox( T1 ⬌ break T2 )" +notation "hvbox( T1 ⊢ ⬌ break T2 )" non associative with precedence 45 - for @{ 'PConv $T1 $T2 }. + for @{ 'CPConv $T1 $T2 }. (* Equivalence **************************************************************) @@ -318,6 +318,6 @@ notation "hvbox( L ⊢ break term 90 T1 ⬌* break T2 )" non associative with precedence 45 for @{ 'PConvStar $L $T1 $T2 }. -notation "hvbox( T1 ⬌* break T2 )" +notation "hvbox( T1 ⊢ ⬌* break T2 )" non associative with precedence 45 - for @{ 'PConvStar $T1 $T2 }. + for @{ 'CPConvStar $T1 $T2 }. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma index 953145592..34ad5d844 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma @@ -109,7 +109,7 @@ qed-. (* Basic_1: removed theorems 6: pr2_head_2 pr2_cflat pr2_gen_cflat clear_pr2_trans - pr2_gen_ctail pr2_ctail + pr2_gen_ctail pr2_ctail Basic_1: removed local theorems 3: pr2_free_free pr2_free_delta pr2_delta_delta *) 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 fd4940b7c..eb5fb1471 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 @@ -28,6 +28,15 @@ lapply (ldrop_fwd_ldrop2_length … HLK) #Hi @ex2_1_intro [2: // | skip | @tpss_subst /width=6/ ] (**) (* /3 width=6/ is too slow *) qed. +lemma cpr_abst: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀V,T1,T2. + L.ⓛV ⊢ T1 ➡ T2 → L ⊢ ⓛV1. T1 ➡ ⓛV2. T2. +#L #V1 #V2 * #V0 #HV10 #HV02 #V #T1 #T2 * #T0 #HT10 #HT02 +lapply (tpss_inv_S2 … HT02 L V ?) -HT02 // #HT02 +@(ex2_1_intro … (ⓛV0.T0)) /2 width=1/ -V1 -T1 (**) (* explicit constructors *) +@tpss_bind // -V0 +@(tpss_lsubs_conf (L.ⓛV)) // -T0 -T2 /2 width=1/ +qed. + (* Advanced inversion lemmas ************************************************) (* Basic_1: was: pr2_gen_lref *) 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 new file mode 100644 index 000000000..4b1f9b51a --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_lcpr.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/ltpr_ltpss.ma". +include "basic_2/reducibility/ltpr_ltpr.ma". +include "basic_2/reducibility/lcpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ***************) + +(* Main properties **********************************************************) + +theorem lcpr_conf: ∀L0,L1,L2. L0 ⊢ ➡ L1 → L0 ⊢ ➡ L2 → + ∃∃L. L1 ⊢ ➡ L & L2 ⊢ ➡ L. +#K0 #L1 #L2 * #K1 #HK01 #HKL1 * #K2 #HK02 #HKL2 +lapply (ltpr_fwd_length … HK01) #H +>(ltpr_fwd_length … HK02) in H; #H +elim (ltpr_conf … HK01 … HK02) -K0 #K #HK1 #HK2 +lapply (ltpss_fwd_length … HKL1) #H1 +lapply (ltpss_fwd_length … HKL2) #H2 +>H1 in HKL1 H; -H1 #HKL1 +>H2 in HKL2; -H2 #HKL2 #H +elim (ltpr_ltpss_conf … HKL1 … HK1) -K1 #K1 #HK1 #HLK1 +elim (ltpr_ltpss_conf … HKL2 … HK2) -K2 #K2 #HK2 #HLK2 +elim (ltpss_conf … HK1 … HK2) -K #K #HK1 #HK2 +lapply (ltpr_fwd_length … HLK1) #H1 +lapply (ltpr_fwd_length … HLK2) #H2 +/3 width=5/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpr.ma new file mode 100644 index 000000000..aaeb2064c --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpr.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/reducibility/tpr_tpr.ma". +include "basic_2/reducibility/ltpr.ma". + +(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) + +(* Main properties **********************************************************) + +theorem ltpr_conf: ∀L0:lenv. ∀L1. L0 ➡ L1 → ∀L2. L0 ➡ L2 → + ∃∃L. L1 ➡ L & L2 ➡ L. +#L0 #L1 #H elim H -L0 -L1 /2 width=3/ +#K0 #K1 #I #V0 #V1 #_ #HV01 #IHK01 #L2 #H +elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK02 #HV02 #H destruct +elim (IHK01 … HK02) -K0 #K #HK1 #HK2 +elim (tpr_conf … HV01 HV02) -V0 /3 width=5/ +qed. 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 new file mode 100644 index 000000000..879d4418b --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpss.ma @@ -0,0 +1,45 @@ +(**************************************************************************) +(* ___ *) +(* ||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/tpr_tpss.ma". + +(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) + +(* 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. +#L1 #K1 #d #e #H elim H -L1 -K1 -d -e +[ /2 width=3/ +| #L1 #I #V1 #X #H + elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=5/ +| #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/ +| #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/ +] +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/substitution/tps_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_lift.ma index 3481d7a1c..581f1fda5 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_lift.ma @@ -19,23 +19,32 @@ include "basic_2/substitution/tps.ma". (* Advanced inversion lemmas ************************************************) -fact tps_inv_refl_SO2_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶ T2 → e = 1 → - ∀K,V. ⇩[0, d] L ≡ K. ⓛV → T1 = T2. -#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e +fact tps_inv_S2_aux: ∀L,T1,T2,d,e1. L ⊢ T1 [d, e1] ▶ T2 → ∀e2. e1 = e2 + 1 → + ∀K,V. ⇩[0, d] L ≡ K. ⓛV → L ⊢ T1 [d + 1, e2] ▶ T2. +#L #T1 #T2 #d #e1 #H elim H -L -T1 -T2 -d -e1 [ // -| #L #K0 #V0 #W #i #d #e #Hdi #Hide #HLK0 #_ #H destruct - >(le_to_le_to_eq … Hdi ?) /2 width=1/ -d #K #V #HLK - lapply (ldrop_mono … HLK0 … HLK) #H destruct -| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #H1 #K #V #HLK - >(IHV12 H1 … HLK) -IHV12 >(IHT12 H1 K V) -IHT12 // /2 width=1/ -| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #H1 #K #V #HLK - >(IHV12 H1 … HLK) -IHV12 >(IHT12 H1 … HLK) -IHT12 // +| #L #K0 #V0 #W #i #d #e1 #Hdi #Hide1 #HLK0 #HV0 #e2 #He12 #K #V #HLK destruct + elim (lt_or_ge i (d+1)) #HiSd + [ -Hide1 -HV0 + lapply (le_to_le_to_eq … Hdi ?) /2 width=1/ #H destruct + lapply (ldrop_mono … HLK0 … HLK) #H destruct + | -V -Hdi /2 width=4/ + ] +| /4 width=3/ +| /3 width=3/ ] qed. +lemma tps_inv_S2: ∀L,T1,T2,d,e. L ⊢ T1 [d, e + 1] ▶ T2 → + ∀K,V. ⇩[0, d] L ≡ K. ⓛV → L ⊢ T1 [d + 1, e] ▶ T2. +/2 width=3/ qed-. + lemma tps_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ▶ T2 → ∀K,V. ⇩[0, d] L ≡ K. ⓛV → T1 = T2. -/2 width=8/ qed-. +#L #T1 #T2 #d #HT12 #K #V #HLK +lapply (tps_inv_S2 … T1 T2 … 0 … HLK) -K // -HT12 #HT12 +lapply (tps_inv_refl_O2 … HT12) -HT12 // +qed-. (* Relocation properties ****************************************************) 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 c445f6890..e992e2a77 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma @@ -31,6 +31,12 @@ lemma ltpss_ind: ∀d,e,L1. ∀R:predicate lenv. R L1 → #d #e #L1 #R #HL1 #IHL1 #L2 #HL12 @(TC_star_ind … HL1 IHL1 … HL12) // qed-. +lemma ltpss_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 ltpss_strap: ∀L1,L,L2,d,e. 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 370de3e6e..faa3ce6e5 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 @@ -12,10 +12,13 @@ (* *) (**************************************************************************) +include "basic_2/unfold/tpss_tpss.ma". include "basic_2/unfold/ltpss_tpss.ma". (* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************) +(* Advanced properties ******************************************************) + (* Main properties **********************************************************) theorem ltpss_trans_eq: ∀L1,L,L2,d,e. @@ -53,3 +56,85 @@ lemma ltpss_tpss1_lt: ∀L1,L2,I,V1,V2,d,e. #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd >(plus_minus_m_m d 1) // /2 width=1/ qed. + +fact ltps_conf_aux: ∀K,K1,L1,d1,e1. K1 [d1, e1] ▶ L1 → + ∀K2,L2,d2,e2. K2 [d2, e2] ▶ L2 → K1 = K → K2 = K → + ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶* L. +#K @(lw_wf_ind … K) -K #K #IH #K1 #L1 #d1 #e1 * -K1 -L1 -d1 -e1 +[ -IH /3 width=3/ +| -IH #K1 #I1 #V1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2 + [ /2 width=3/ + | #K2 #I2 #V2 #H1 #H2 destruct /2 width=3/ + | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct /4 width=3/ + | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct /4 width=3/ + ] +| #K1 #L1 #I1 #W1 #V1 #e1 #HKL1 #HWV1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2 + [ -IH #d2 #e2 #H1 #H2 destruct + | -IH #K2 #I2 #V2 #H1 #H2 destruct + @ex2_1_intro [2,3: @inj ] /3 width=5/ (**) (* /4 width=5/ is too slow *) + | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct + elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2 + elim (ltpss_tps_conf … HWV1 … HL1) #U1 #HWU1 #HVU1 + elim (ltpss_tps_conf … HWV2 … HL2) #U2 #HWU2 #HVU2 + elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W + @(ex2_1_intro … (L.ⓑ{I1}W)) (**) (* explicit constructor *) + [ @(ltpss_trans_eq … (L1.ⓑ{I1}U1)) /2 width=1/ + | @(ltpss_trans_eq … (L2.ⓑ{I1}U2)) /2 width=1/ + ] + | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct + elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2 + elim (ltpss_tps_conf … HWV1 … HL1) #U1 #HWU1 #HVU1 + elim (ltpss_tps_conf … HWV2 … HL2) #U2 #HWU2 #HVU2 + elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W + @(ex2_1_intro … (L.ⓑ{I1}W)) (**) (* explicit constructor *) + [ @(ltpss_trans_eq … (L1.ⓑ{I1}U1)) /2 width=1/ + | @(ltpss_trans_eq … (L2.ⓑ{I1}U2)) /2 width=1/ + ] + ] +| #K1 #L1 #I1 #W1 #V1 #d1 #e1 #HKL1 #HWV1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2 + [ -IH #d2 #e2 #H1 #H2 destruct + | -IH #K2 #I2 #V2 #H1 #H2 destruct + @ex2_1_intro [2,3: @inj ] /3 width=5/ (**) (* /4 width=5/ is too slow *) + | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct + elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2 + elim (ltpss_tps_conf … HWV1 … HL1) #U1 #HWU1 #HVU1 + elim (ltpss_tps_conf … HWV2 … HL2) #U2 #HWU2 #HVU2 + elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W + @(ex2_1_intro … (L.ⓑ{I1}W)) (**) (* explicit constructor *) + [ @(ltpss_trans_eq … (L1.ⓑ{I1}U1)) /2 width=1/ + | @(ltpss_trans_eq … (L2.ⓑ{I1}U2)) /2 width=1/ + ] + | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct + elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2 + elim (ltpss_tps_conf … HWV1 … HL1) #U1 #HWU1 #HVU1 + elim (ltpss_tps_conf … HWV2 … HL2) #U2 #HWU2 #HVU2 + elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W + @(ex2_1_intro … (L.ⓑ{I1}W)) (**) (* explicit constructor *) + [ @(ltpss_trans_eq … (L1.ⓑ{I1}U1)) /2 width=1/ + | @(ltpss_trans_eq … (L2.ⓑ{I1}U2)) /2 width=1/ + ] + ] +] +qed. + +lemma ltps_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. +/2 width=7/ qed. + +axiom ltpss_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. +(* +fact ltpss_conf_aux: ∀K1,L1,d1,e1. K1 [d1, e1] ▶* L1 → + ∀K2,L2,d2,e2. K2 [d2, e2] ▶* L2 → K1 = K2 → + ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶* L. +#K1 #L1 #d1 #e1 #H @(ltpss_ind_dx … H) -K1 /2 width=3/ +#X1 #K1 #HXK1 #HKL1 #IHKL1 #K2 #L2 #d2 #e2 #H @(ltpss_ind_dx … H) -K2 +[ -IHKL1 #H destruct + lapply (ltpss_strap … HXK1 HKL1) -K1 /2 width=3/ +| #X2 #K2 #HXK2 #HKL2 #_ #H destruct + elim (ltps_conf … HXK1 … HXK2) -X2 #K #HK1 #HK2 + elim (IHKL1 … HK1 ?) // -K1 #L #HL1 #HKL + @(ex2_1_intro … K) // +*) \ No newline at end of file diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_lift.ma index f12e38877..b54a68e7c 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_lift.ma @@ -67,6 +67,13 @@ elim (tpss_inv_atom1 … H) -H /2 width=1/ * #K #V1 #V2 #j #Hdj #Hjde #HLK #HV12 #HVT2 #H destruct /3 width=6/ qed-. +lemma tpss_inv_S2: ∀L,T1,T2,d,e. L ⊢ T1 [d, e + 1] ▶* T2 → + ∀K,V. ⇩[0, d] L ≡ K. ⓛV → L ⊢ T1 [d + 1, e] ▶* T2. +#L #T1 #T2 #d #e #H #K #V #HLK @(tpss_ind … H) -T2 // +#T #T2 #_ #HT2 #IHT +lapply (tps_inv_S2 … HT2 … HLK) -HT2 -HLK /2 width=3/ +qed-. + lemma tpss_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ▶* T2 → ∀K,V. ⇩[0, d] L ≡ K. ⓛV → T1 = T2. #L #T1 #T2 #d #H #K #V #HLK @(tpss_ind … H) -T2 // -- 2.39.2