From: Ferruccio Guidi Date: Fri, 10 May 2013 16:15:53 +0000 (+0000) Subject: - partial commit: we issue the "conversion" and "equivalence" components X-Git-Tag: make_still_working~1157 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7d2817401273978654ca725fb3794a4a465a93bb;p=helm.git - partial commit: we issue the "conversion" and "equivalence" components - we park conversion and equivalence on local environments for the moment --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc.ma b/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc.ma index 5fb614a8c..ab76bac16 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/reducibility/cpr.ma". +include "basic_2/reduction/cpr.ma". (* CONTEXT-SENSITIVE PARALLEL CONVERSION ON TERMS ***************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/conversion/fpc.ma b/matita/matita/contribs/lambdadelta/basic_2/conversion/fpc.ma deleted file mode 100644 index f552d5818..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/conversion/fpc.ma +++ /dev/null @@ -1,40 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/reducibility/fpr.ma". - -(* CONTEXT-FREE PARALLEL CONVERSION ON CLOSURES *****************************) - -definition fpc: bi_relation lenv term ≝ - λL1,T1,L2,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ ∨ ⦃L2, T2⦄ ➡ ⦃L1, T1⦄. - -interpretation - "context-free parallel conversion (closure)" - 'FocalizedPConv L1 T1 L2 T2 = (fpc L1 T1 L2 T2). - -(* Basic properties *********************************************************) - -lemma fpc_refl: bi_reflexive … fpc. -/2 width=1/ qed. - -lemma fpc_sym: bi_symmetric … fpc. -#L1 #L2 #T1 #T2 * /2 width=1/ -qed. - -(* Basic forward lemmas *****************************************************) - -lemma fpc_fwd_fpr: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⬌ ⦃L2, T2⦄ → - ∃∃L,T. ⦃L1, T1⦄ ➡ ⦃L, T⦄ & ⦃L2, T2⦄ ➡ ⦃L, T⦄. -#L1 #L2 #T1 #T2 * /2 width=4/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/conversion/fpc_fpc.ma b/matita/matita/contribs/lambdadelta/basic_2/conversion/fpc_fpc.ma deleted file mode 100644 index 22fc16f37..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/conversion/fpc_fpc.ma +++ /dev/null @@ -1,24 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/conversion/fpc.ma". - -(* CONTEXT-FREE PARALLEL CONVERSION ON CLOSURES *****************************) - -(* Main properties **********************************************************) - -theorem fpc_conf: ∀L0,L1,T0,T1. ⦃L0, T0⦄ ⬌ ⦃L1, T1⦄ → - ∀L2,T2. ⦃L0, T0⦄ ⬌ ⦃L2, T2⦄ → - ∃∃L,T. ⦃L1, T1⦄ ⬌ ⦃L, T⦄ & ⦃L2, T2⦄ ⬌ ⦃L, T⦄. -/3 width=4/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/conversion/lfpc.ma b/matita/matita/contribs/lambdadelta/basic_2/conversion/lfpc.ma deleted file mode 100644 index 273873abd..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/conversion/lfpc.ma +++ /dev/null @@ -1,37 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/reducibility/lfpr.ma". - -(* FOCALIZED PARALLEL CONVERSION ON LOCAL ENVIRONMENTS **********************) - -definition lfpc: relation lenv ≝ - λL1,L2. ⦃L1⦄ ➡ ⦃L2⦄ ∨ ⦃L2⦄ ➡ ⦃L1⦄. - -interpretation - "focalized parallel conversion (local environment)" - 'FocalizedPConv L1 L2 = (lfpc L1 L2). - -(* Basic properties *********************************************************) - -lemma lfpc_refl: ∀L. ⦃L⦄ ⬌ ⦃L⦄. -/2 width=1/ qed. - -lemma lfpc_sym: ∀L1,L2. ⦃L1⦄ ⬌ ⦃L2⦄ → ⦃L2⦄ ⬌ ⦃L1⦄. -#L1 #L2 * /2 width=1/ -qed. - -lemma lfpc_lfpr: ∀L1,L2. ⦃L1⦄ ⬌ ⦃L2⦄ → ∃∃L. ⦃L1⦄ ➡ ⦃L⦄ & ⦃L2⦄ ➡ ⦃L⦄. -#L1 #L2 * /2 width=3/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/conversion/lfpc_lfpc.ma b/matita/matita/contribs/lambdadelta/basic_2/conversion/lfpc_lfpc.ma deleted file mode 100644 index 69e444adb..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/conversion/lfpc_lfpc.ma +++ /dev/null @@ -1,23 +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/lfpc.ma". - -(* FOCALIZED PARALLEL CONVERSION ON LOCAL ENVIRONMENTS **********************) - -(* Main properties **********************************************************) - -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/lambdadelta/basic_2/equivalence/cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma index 44d59982c..49f490bce 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma @@ -16,8 +16,7 @@ include "basic_2/conversion/cpc.ma". (* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) -definition cpcs: lenv → relation term ≝ - λL. TC … (cpc L). +definition cpcs: lenv → relation term ≝ LTC … cpc. interpretation "context-sensitive parallel equivalence (term)" 'PConvStar L T1 T2 = (cpcs L T1 T2). @@ -45,29 +44,23 @@ lemma cpcs_refl: ∀L. reflexive … (cpcs L). (* Basic_1: was: pc3_s *) lemma cpcs_sym: ∀L. symmetric … (cpcs L). -/3 width=1/ qed. +#L @TC_symmetric // qed. lemma cpc_cpcs: ∀L,T1,T2. L ⊢ T1 ⬌ T2 → L ⊢ T2 ⬌* T2. /2 width=1/ qed. lemma cpcs_strap1: ∀L,T1,T,T2. L ⊢ T1 ⬌* T → L ⊢ T ⬌ T2 → L ⊢ T1 ⬌* T2. -/2 width=3/ qed. +#L @step qed. lemma cpcs_strap2: ∀L,T1,T,T2. L ⊢ T1 ⬌ T → L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2. -/2 width=3/ qed. +#L @TC_strap qed. (* Basic_1: was: pc3_pr2_r *) -lemma cpcs_cpr_dx: ∀L,T1,T2. L ⊢ T1 ➡ T2 → L ⊢ T1 ⬌* T2. -/3 width=1/ qed. - -lemma cpcs_tpr_dx: ∀L,T1,T2. T1 ➡ T2 → L ⊢ T1 ⬌* T2. +lemma cpr_cpcs_dx: ∀L,T1,T2. L ⊢ T1 ➡ T2 → L ⊢ T1 ⬌* T2. /3 width=1/ qed. (* Basic_1: was: pc3_pr2_x *) -lemma cpcs_cpr_sn: ∀L,T1,T2. L ⊢ T2 ➡ T1 → L ⊢ T1 ⬌* T2. -/3 width=1/ qed. - -lemma cpcs_tpr_sn: ∀L,T1,T2. T2 ➡ T1 → L ⊢ T1 ⬌* T2. +lemma cpr_cpcs_sn: ∀L,T1,T2. L ⊢ T2 ➡ T1 → L ⊢ T1 ⬌* T2. /3 width=1/ qed. lemma cpcs_cpr_strap1: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2. L ⊢ T ➡ T2 → L ⊢ T1 ⬌* T2. @@ -87,15 +80,13 @@ lemma cpr_div: ∀L,T1,T. L ⊢ T1 ➡ T → ∀T2. L ⊢ T2 ➡ T → L ⊢ T1 lemma cpcs_cpr_conf: ∀L,T1,T. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2. /3 width=3/ qed. -lemma cpcs_tpss_strap1: ∀L,T1,T. L ⊢ T1 ⬌* T → - ∀T2,d,e. L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ⬌* T2. -#L #T1 #T #HT1 #T2 #d #e #HT2 +lemma cpcs_cpss_strap1: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2. L ⊢ T ▶* T2 → L ⊢ T1 ⬌* T2. +#L #T1 #T #HT1 #T2 #HT2 @(cpcs_cpr_strap1 … HT1) -T1 /2 width=3/ qed-. -lemma cpcs_tpss_conf: ∀L,T,T1,d,e. L ⊢ T ▶* [d, e] T1 → - ∀T2. L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2. -#L #T #T1 #d #e #HT1 #T2 #HT2 +lemma cpcs_cpss_conf: ∀L,T,T1. L ⊢ T ▶* T1 → ∀T2. L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2. +#L #T #T1 #HT1 #T2 #HT2 @(cpcs_cpr_conf … HT2) -T2 /2 width=3/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma index 5d0643879..199e49b07 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/computation/cprs_lift.ma". include "basic_2/computation/cprs_cprs.ma". include "basic_2/conversion/cpc_cpc.ma". include "basic_2/equivalence/cpcs_cprs.ma". @@ -46,7 +45,7 @@ lemma cpcs_inv_sort_abst: ∀a,L,W,T,k. L ⊢ ⋆k ⬌* ⓛ{a}W.T → ⊥. #a #L #W #T #k #H elim (cpcs_inv_cprs … H) -H #X #H1 >(cprs_inv_sort1 … H1) -X #H2 -elim (cprs_inv_abst1 Abst W … H2) -H2 #W0 #T0 #_ #_ #H destruct +elim (cprs_fwd_abst1 … H2 Abst W) -H2 #W0 #T0 #_ #_ #H destruct qed-. (* Basic_1: was: pc3_gen_abst *) @@ -54,8 +53,8 @@ lemma cpcs_inv_abst: ∀a1,a2,L,W1,W2,T1,T2. L ⊢ ⓛ{a1}W1.T1 ⬌* ⓛ{a2}W2.T ∧∧ L ⊢ W1 ⬌* W2 & L. ②{I}V ⊢ T1 ⬌* T2 & a1 = a2. #a1 #a2 #L #W1 #W2 #T1 #T2 #H #I #V elim (cpcs_inv_cprs … H) -H #T #H1 #H2 -elim (cprs_inv_abst1 I V … H1) -H1 #W0 #T0 #HW10 #HT10 #H destruct -elim (cprs_inv_abst1 I V … H2) -H2 #W #T #HW2 #HT2 #H destruct /3 width=3/ +elim (cprs_fwd_abst1 … H1 I V) -H1 #W0 #T0 #HW10 #HT10 #H destruct +elim (cprs_fwd_abst1… H2 I V) -H2 #W #T #HW2 #HT2 #H destruct /3 width=3/ qed-. (* Basic_1: was: pc3_gen_abst_shift *) @@ -69,7 +68,7 @@ lemma cpcs_inv_abst1: ∀a,L,W1,T1,T. L ⊢ ⓛ{a}W1.T1 ⬌* T → ∃∃W2,T2. L ⊢ T ➡* ⓛ{a}W2.T2 & L ⊢ ⓛ{a}W1.T1 ➡* ⓛ{a}W2.T2. #a #L #W1 #T1 #T #H elim (cpcs_inv_cprs … H) -H #X #H1 #H2 -elim (cprs_inv_abst1 Abst W1 … H1) -H1 #W2 #T2 #HW12 #HT12 #H destruct +elim (cprs_fwd_abst1 … H1 Abst W1) -H1 #W2 #T2 #HW12 #HT12 #H destruct @(ex2_2_intro … H2) -H2 /2 width=2/ (**) (* explicit constructor, /3 width=6/ is slow *) qed-. @@ -83,18 +82,18 @@ lemma cpcs_inv_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K → L ⊢ U1 ⬌* U2 → K ⊢ T1 ⬌* T2. #L #K #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HU12 elim (cpcs_inv_cprs … HU12) -HU12 #U #HU1 #HU2 -elim (cprs_inv_lift1 … HLK … HTU1 … HU1) -U1 #T #HTU #HT1 -elim (cprs_inv_lift1 … HLK … HTU2 … HU2) -L -U2 #X #HXU +elim (cprs_inv_lift1 … HU1 … HLK … HTU1) -U1 #T #HTU #HT1 +elim (cprs_inv_lift1 … HU2 … HLK … HTU2) -L -U2 #X #HXU >(lift_inj … HXU … HTU) -X -U -d -e /2 width=3/ qed-. (* Advanced properties ******************************************************) -lemma ltpr_cpcs_trans: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L2 ⊢ T1 ⬌* T2 → L1 ⊢ T1 ⬌* T2. +lemma lpr_cpcs_trans: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T1,T2. L2 ⊢ T1 ⬌* T2 → L1 ⊢ T1 ⬌* T2. #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H #T #HT1 #HT2 -lapply (ltpr_cprs_trans … HL12 … HT1) -HT1 -lapply (ltpr_cprs_trans … HL12 … HT2) -L2 /2 width=3/ +lapply (lpr_cprs_trans … HT1 … HL12) -HT1 +lapply (lpr_cprs_trans … HT2 … HL12) -L2 /2 width=3/ qed-. lemma cpr_cprs_conf_cpcs: ∀L,T,T1,T2. L ⊢ T ➡* T1 → L ⊢ T ➡ T2 → L ⊢ T1 ⬌* T2. @@ -112,6 +111,13 @@ lemma cprs_conf_cpcs: ∀L,T,T1,T2. L ⊢ T ➡* T1 → L ⊢ T ➡* T2 → L elim (cprs_conf … HT1 … HT2) /2 width=3/ qed-. +(* Basic_1: was only: pc3_pr0_pr2_t *) +(* Basic_1: note: pc3_pr0_pr2_t should be renamed *) +lemma lpr_cpr_conf: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T1,T2. L1 ⊢ T1 ➡ T2 → L2 ⊢ T1 ⬌* T2. +#L1 #L2 #HL12 #T1 #T2 #HT12 +elim (lpr_cpr_conf_dx … HT12 … HL12) -L1 /3 width=3/ +qed-. + (* Basic_1: was only: pc3_thin_dx *) lemma cpcs_flat: ∀L,V1,V2. L ⊢ V1 ⬌* V2 → ∀T1,T2. L ⊢ T1 ⬌* T2 → ∀I. L ⊢ ⓕ{I}V1. T1 ⬌* ⓕ{I}V2. T2. @@ -120,56 +126,49 @@ 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_flat_dx_tpr_rev: ∀L,V1,V2. V2 ➡ V1 → ∀T1,T2. L ⊢ T1 ⬌* T2 → +lemma cpcs_flat_dx_cpr_rev: ∀L,V1,V2. L ⊢ V2 ➡ V1 → ∀T1,T2. L ⊢ T1 ⬌* T2 → ∀I. L ⊢ ⓕ{I}V1. T1 ⬌* ⓕ{I}V2. T2. /3 width=1/ qed. -lemma cpcs_abst: ∀L,V1,V2. L ⊢ V1 ⬌* V2 → ∀V,T1,T2. L.ⓛV ⊢ T1 ⬌* T2 → - ∀a,I. L ⊢ ⓑ{a,I}V1. T1 ⬌* ⓑ{a,I}V2. T2. +lemma cpcs_ext_bind: ∀L,V1,V2. L ⊢ V1 ⬌* V2 → ∀V,T1,T2. L.ⓛV ⊢ T1 ⬌* T2 → + ∀a,I. L ⊢ ⓑ{a,I}V1.T1 ⬌* ⓑ{a,I}V2.T2. #L #V1 #V2 #HV12 #V #T1 #T2 #HT12 #a #I 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: ∀a,L,V,T1,T2. L.ⓓV ⊢ T1 ⬌* T2 → L ⊢ ⓓ{a}V. T1 ⬌* ⓓ{a}V. T2. -#a #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 *) +/3 width=6 by cprs_div, cprs_ext_bind/ (**) (* /3 width=6/ is a bit slow *) qed. lemma cpcs_bind_dx: ∀a,I,L,V,T1,T2. L.ⓑ{I}V ⊢ T1 ⬌* T2 → L ⊢ ⓑ{a,I}V. T1 ⬌* ⓑ{a,I}V. T2. -#a * /2 width=1/ /2 width=2/ qed. - -lemma cpcs_abbr_sn: ∀a,L,V1,V2,T. L ⊢ V1 ⬌* V2 → L ⊢ ⓓ{a}V1. T ⬌* ⓓ{a}V2. T. -#a #L #V1 #V2 #T #HV12 -elim (cpcs_inv_cprs … HV12) -HV12 /3 width=5 by cprs_div, cprs_abbr1/ (**) (* /3 width=5/ is a bit slow *) +#a #I #L #V #T1 #T2 #HT12 +elim (cpcs_inv_cprs … HT12) -HT12 /3 width=5 by cprs_div, cprs_bind/ (**) (* /3 width=5/ is a bit slow *) qed. lemma cpcs_bind_sn: ∀a,I,L,V1,V2,T. L ⊢ V1 ⬌* V2 → L ⊢ ⓑ{a,I}V1. T ⬌* ⓑ{a,I}V2. T. -#a * /2 width=1/ /2 width=2/ qed. +#a #I #L #V1 #V2 #T #HV12 +elim (cpcs_inv_cprs … HV12) -HV12 /3 width=5 by cprs_div, cprs_bind/ (**) (* /3 width=5/ is a bit slow *) +qed. -lemma cpcs_beta_dx: ∀a,L,V1,V2,W,T1,T2. - L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ⬌* T2 → L ⊢ ⓐV1.ⓛ{a}W.T1 ⬌* ⓓ{a}V2.T2. +lemma cpcs_beta_dx_cpr: ∀a,L,V1,V2,W,T1,T2. + L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ⬌* T2 → L ⊢ ⓐV1.ⓛ{a}W.T1 ⬌* ⓓ{a}V2.T2. #a #L #V1 #V2 #W #T1 #T2 #HV12 #HT12 elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2 -lapply (cprs_beta_dx … HV12 HT1 a) -HV12 -HT1 #HT1 +lapply (cprs_beta_dx a … HV12 HT1) -HV12 -HT1 #HT1 lapply (cprs_lsubr_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2 @(cprs_div … HT1) /2 width=1/ qed. -lemma cpcs_beta_dx_tpr_rev: ∀a,L,V1,V2,W,T1,T2. - V1 ➡ V2 → L.ⓛW ⊢ T2 ⬌* T1 → +lemma cpcs_beta_dx_rev_cpr: ∀a,L,V1,V2,W,T1,T2. + L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T2 ⬌* T1 → L ⊢ ⓓ{a}V2.T2 ⬌* ⓐV1.ⓛ{a}W.T1. /4 width=1/ qed. -(* Note: it does not hold replacing |L1| with |L2| *) lemma cpcs_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ⬌* T2 → - ∀L2. L2 ⊑ [0, |L1|] L1 → L2 ⊢ T1 ⬌* T2. + ∀L2. L2 ⊑ L1 → L2 ⊢ T1 ⬌* T2. #L1 #T1 #T2 #HT12 elim (cpcs_inv_cprs … HT12) -HT12 /3 width=5 by cprs_div, cprs_lsubr_trans/ (**) (* /3 width=5/ is a bit slow *) -qed. +qed-. (* Basic_1: was: pc3_lift *) lemma cpcs_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K → @@ -178,44 +177,47 @@ lemma cpcs_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K → #L #K #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HT12 elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2 elim (lift_total T d e) #U #HTU -lapply (cprs_lift … HLK … HTU1 … HT1 … HTU) -T1 #HU1 -lapply (cprs_lift … HLK … HTU2 … HT2 … HTU) -K -T2 -T -d -e /2 width=3/ +lapply (cprs_lift … HT1 … HLK … HTU1 … HTU) -T1 #HU1 +lapply (cprs_lift … HT2 … HLK … HTU2 … HTU) -K -T2 -T -d -e /2 width=3/ qed. lemma cpcs_strip: ∀L,T1,T. L ⊢ T ⬌* T1 → ∀T2. L ⊢ T ⬌ T2 → ∃∃T0. L ⊢ T1 ⬌ T0 & L ⊢ T2 ⬌* T0. -/3 width=3/ qed. +#L #T1 #T @TC_strip1 /2 width=3/ qed-. (* Main properties **********************************************************) (* Basic_1: was pc3_t *) theorem cpcs_trans: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2. L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2. -/2 width=3/ qed. +#L #T1 #T #HT1 #T2 @(trans_TC … HT1) qed-. theorem cpcs_canc_sn: ∀L,T,T1,T2. L ⊢ T ⬌* T1 → L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2. -/3 width=3 by cpcs_trans, cpcs_sym/ qed. (**) (* /3 width=3/ is too slow *) +/3 width=3 by cpcs_trans, cpcs_sym/ qed-. (**) (* /3 width=3/ is too slow *) theorem cpcs_canc_dx: ∀L,T,T1,T2. L ⊢ T1 ⬌* T → L ⊢ T2 ⬌* T → L ⊢ T1 ⬌* T2. -/3 width=3 by cpcs_trans, cpcs_sym/ qed. (**) (* /3 width=3/ is too slow *) +/3 width=3 by cpcs_trans, cpcs_sym/ qed-. (**) (* /3 width=3/ is too slow *) -lemma cpcs_abbr1: ∀a,L,V1,V2. L ⊢ V1 ⬌* V2 → ∀T1,T2. L.ⓓV1 ⊢ T1 ⬌* T2 → - L ⊢ ⓓ{a}V1. T1 ⬌* ⓓ{a}V2. T2. -#a #L #V1 #V2 #HV12 #T1 #T2 #HT12 -@(cpcs_trans … (ⓓ{a}V1.T2)) /2 width=1/ +lemma cpcs_bind1: ∀a,I,L,V1,V2. L ⊢ V1 ⬌* V2 → ∀T1,T2. L.ⓑ{I}V1 ⊢ T1 ⬌* T2 → + L ⊢ ⓑ{a,I}V1. T1 ⬌* ⓑ{a,I}V2. T2. +#a #I #L #V1 #V2 #HV12 #T1 #T2 #HT12 +@(cpcs_trans … (ⓑ{a,I}V1.T2)) /2 width=1/ qed. -lemma cpcs_abbr2: ∀a,L,V1,V2. L ⊢ V1 ⬌* V2 → ∀T1,T2. L.ⓓV2 ⊢ T1 ⬌* T2 → - L ⊢ ⓓ{a}V1. T1 ⬌* ⓓ{a}V2. T2. -#a #L #V1 #V2 #HV12 #T1 #T2 #HT12 -@(cpcs_trans … (ⓓ{a}V2.T1)) /2 width=1/ +lemma cpcs_bind2: ∀a,I,L,V1,V2. L ⊢ V1 ⬌* V2 → ∀T1,T2. L.ⓑ{I}V2 ⊢ T1 ⬌* T2 → + L ⊢ ⓑ{a,I}V1. T1 ⬌* ⓑ{a,I}V2. T2. +#a #I #L #V1 #V2 #HV12 #T1 #T2 #HT12 +@(cpcs_trans … (ⓑ{a,I}V2.T1)) /2 width=1/ qed. -lemma cpcs_bind1: ∀I,L,V1,T1,T2. L.ⓑ{I}V1 ⊢ T1 ⬌* T2 → ∀V2. L ⊢ V1 ⬌* V2 → - ∀a. L ⊢ ⓑ{a,I}V1. T1 ⬌* ⓑ{a,I}V2. T2. -* /2 width=1/ /2 width=2/ -qed. +(* Basic_1: was: pc3_wcpr0_t *) +(* Basic_1: note: pc3_wcpr0_t should be renamed *) +lemma lpr_cprs_conf: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T1,T2. L1 ⊢ T1 ➡* T2 → L2 ⊢ T1 ⬌* T2. +#L1 #L2 #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 // +/3 width=5 by cpcs_trans, lpr_cpr_conf/ +qed-. -lemma cpcs_bind2: ∀L,V1,V2. L ⊢ V1 ⬌* V2 → ∀I,T1,T2. L.ⓑ{I}V2 ⊢ T1 ⬌* T2 → - ∀a. L ⊢ ⓑ{a,I}V1. T1 ⬌* ⓑ{a,I}V2. T2. -#L #V1 #V2 #HV12 * /2 width=1/ /2 width=2/ -qed. +(* Basic_1: was: pc3_wcpr0 *) +lemma lpr_cpcs_conf: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T1,T2. L1 ⊢ T1 ⬌* T2 → L2 ⊢ T1 ⬌* T2. +#L1 #L2 #HL12 #T1 #T2 #H +elim (cpcs_inv_cprs … H) -H /3 width=5 by cpcs_canc_dx, lpr_cprs_conf/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cprs.ma index cb1f5d76a..8c1fec2e1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cprs.ma @@ -53,7 +53,7 @@ lemma cprs_div: ∀L,T1,T. L ⊢ T1 ➡* T → ∀T2. L ⊢ T2 ➡* T → L ⊢ qed. lemma cprs_cpr_div: ∀L,T1,T. L ⊢ T1 ➡* T → ∀T2. L ⊢ T2 ➡ T → L ⊢ T1 ⬌* T2. -/3 width=5 by step, cprs_div/ qed-. +/3 width=5 by cpr_cprs, cprs_div/ qed-. lemma cpr_cprs_div: ∀L,T1,T. L ⊢ T1 ➡ T → ∀T2. L ⊢ T2 ➡* T → L ⊢ T1 ⬌* T2. -/3 width=3 by step, cprs_div/ qed-. +/3 width=3 by cpr_cprs, cprs_div/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_delift.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_delift.ma deleted file mode 100644 index 7012ec11e..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_delift.ma +++ /dev/null @@ -1,37 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/unfold/delift_lift.ma". -include "basic_2/unfold/delift_delift.ma". -include "basic_2/computation/cprs_delift.ma". -include "basic_2/equivalence/cpcs_cpcs.ma". - -(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) - -(* Properties on inverse basic term relocation ******************************) - -lemma cpcs_zeta_delift_comm: ∀L,V,T1,T2. L.ⓓV ⊢ ▼*[O, 1] T1 ≡ T2 → - L ⊢ T2 ⬌* +ⓓV.T1. -/3 width=1/ qed. - -(* Basic_1: was only: pc3_gen_cabbr *) -lemma thin_cpcs_delift_mono: ∀L,U1,U2. L ⊢ U1 ⬌* U2 → - ∀K,d,e. ▼*[d, e] L ≡ K → ∀T1. L ⊢ ▼*[d, e] U1 ≡ T1 → - ∀T2. L ⊢ ▼*[d, e] U2 ≡ T2 → K ⊢ T1 ⬌* T2. -#L #U1 #U2 #H #K #d #e #HLK #T1 #HTU1 #T2 #HTU2 -elim (cpcs_inv_cprs … H) -H #U #HU1 #HU2 -elim (thin_cprs_delift_conf … HU1 … HLK … HTU1) -U1 #T #HT1 #HUT -elim (thin_cprs_delift_conf … HU2 … HLK … HTU2) -U2 -HLK #X #HT2 #H -lapply (delift_mono … H … HUT) -L #H destruct /2 width=3/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_lpss.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_lpss.ma new file mode 100644 index 000000000..c9bcdc83d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_lpss.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/substitution/lpss_lpss.ma". +include "basic_2/computation/cprs_lpss.ma". +include "basic_2/equivalence/cpcs_cpcs.ma". + +(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) + +(* Properties on sn parallel substitution for local environments ************) + +lemma cpcs_lpss_conf: ∀L1,L2. L1 ⊢ ▶* L2 → ∀T1,T2. L1 ⊢ T1 ⬌* T2 → L2 ⊢ T1 ⬌* T2. +#L1 #L2 #HL12 #T1 #T2 #H +elim (cpcs_inv_cprs … H) -H #T #HT1 #HT2 +elim (cprs_lpss_conf_dx … HT1 … HL12) -HT1 #U1 #H1 #HTU1 +elim (cprs_lpss_conf_dx … HT2 … HL12) -L1 #U2 #H2 #HTU2 +elim (cpss_conf … H1 … H2) -T #U #HU1 #HU2 +lapply (cprs_cpss_trans … HTU1 … HU1) -U1 +lapply (cprs_cpss_trans … HTU2 … HU2) -U2 /2 width=3/ +qed-. + +lemma cpcs_lpss_cpss_conf: ∀L1,L2. L1 ⊢ ▶* L2 → + ∀T,T2. L1 ⊢ T ⬌* T2 → + ∀T1. L2 ⊢ T ▶* T1 → + L2 ⊢ T1 ⬌* T2. +#L1 #L2 #HL12 #T #T2 #HT2 #T1 #HT1 +lapply (cpcs_lpss_conf … HL12 … HT2) -L1 #HT2 +lapply (cpcs_cpss_conf … HT1 … HT2) -T // +qed-. + +lemma cpcs_lpss_cpss2_conf: ∀L1,L2. L1 ⊢ ▶* L2 → ∀T1,T2. L1 ⊢ T1 ⬌* T2 → + ∀T3. L2 ⊢ T1 ▶* T3 → ∀T4. L2 ⊢ T2 ▶* T4 → + L2 ⊢ T3 ⬌* T4. +#L1 #L2 #HL12 #T1 #T2 #HT12 #T3 #HT13 #T4 #HT24 +lapply (cpcs_lpss_cpss_conf … HL12 … HT12 … HT13) -L1 -T1 #HT32 +lapply (cpcs_cpss_strap1 … HT32 … HT24) -T2 // +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_ltpr.ma deleted file mode 100644 index 13713e51e..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_ltpr.ma +++ /dev/null @@ -1,43 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/reducibility/cpr_ltpr.ma". -include "basic_2/equivalence/cpcs_cpcs.ma". - -(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) - -(* Properties about context-free parallel reduction on local environments ***) - -(* Basic_1: was only: pc3_pr0_pr2_t *) -(* Basic_1: note: pc3_pr0_pr2_t should be renamed *) -lemma ltpr_cpr_conf: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L1 ⊢ T1 ➡ T2 → L2 ⊢ T1 ⬌* T2. -#L1 #L2 #HL12 #T1 #T2 #HT12 -elim (cpr_ltpr_conf_eq … HT12 … HL12) -L1 #T #HT1 #HT2 -@(cprs_div … T) /2 width=1/ /3 width=1/ (**) (* /4 width=3/ is too long *) -qed. - -(* Basic_1: was: pc3_wcpr0_t *) -(* Basic_1: note: pc3_wcpr0_t should be renamed *) -lemma ltpr_cprs_conf: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L1 ⊢ T1 ➡* T2 → L2 ⊢ T1 ⬌* T2. -#L1 #L2 #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 // -#T #T2 #_ #HT2 #IHT1 -@(cpcs_trans … IHT1) -T1 /2 width=3/ -qed. - -(* Basic_1: was: pc3_wcpr0 *) -lemma ltpr_cpcs_conf: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L1 ⊢ T1 ⬌* T2 → L2 ⊢ T1 ⬌* T2. -#L1 #L2 #HL12 #T1 #T2 #H -elim (cpcs_inv_cprs … H) -H #T #HT1 #HT2 -@(cpcs_canc_dx … T) /2 width=3/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_ltpss_dx.ma deleted file mode 100644 index 80f418b08..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_ltpss_dx.ma +++ /dev/null @@ -1,50 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/computation/cprs_ltpss_dx.ma". -include "basic_2/equivalence/cpcs_cpcs.ma". - -(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) - -(* Properties concerning dx partial unfold on local environments ************) - -lemma cpcs_ltpss_dx_conf: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → - ∀T1,T2. L1 ⊢ T1 ⬌* T2 → L2 ⊢ T1 ⬌* T2. -#L1 #L2 #d #e #HL12 #T1 #T2 #H -elim (cpcs_inv_cprs … H) -H #T #HT1 #HT2 -elim (cprs_ltpss_dx_conf … HT1 … HL12) -HT1 #U1 #HTU1 #H1 -elim (cprs_ltpss_dx_conf … HT2 … HL12) -L1 #U2 #HTU2 #H2 -elim (tpss_conf_eq … H1 … H2) -T #U #HU1 #HU2 -lapply (cprs_tpss_trans … HTU1 … HU1) -U1 -lapply (cprs_tpss_trans … HTU2 … HU2) -U2 /2 width=3/ -qed-. - -lemma cpcs_ltpss_dx_tpss_conf: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → - ∀T,T2. L1 ⊢ T ⬌* T2 → - ∀T1. L2 ⊢ T ▶* [d, e] T1 → - L2 ⊢ T1 ⬌* T2. -#L1 #L2 #d #e #HL12 #T #T2 #HT2 #T1 #HT1 -lapply (cpcs_ltpss_dx_conf … HL12 … HT2) -L1 #HT2 -lapply (cpcs_tpss_conf … HT1 … HT2) -T // -qed-. - -lemma cpcs_ltpss_dx_tpss2_conf: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → - ∀T1,T2. L1 ⊢ T1 ⬌* T2 → - ∀T3. L2 ⊢ T1 ▶* [d, e] T3 → - ∀T4. L2 ⊢ T2 ▶* [d, e] T4 → - L2 ⊢ T3 ⬌* T4. -#L1 #L2 #d #e #HL12 #T1 #T2 #HT12 #T3 #HT13 #T4 #HT24 -lapply (cpcs_ltpss_dx_tpss_conf … HL12 … HT12 … HT13) -L1 -T1 #HT32 -lapply (cpcs_tpss_strap1 … HT32 … HT24) -T2 // -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_ltpss_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_ltpss_sn.ma deleted file mode 100644 index 5bf1ed57f..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_ltpss_sn.ma +++ /dev/null @@ -1,28 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/equivalence/cpcs_ltpss_dx.ma". - -(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) - -(* Properties concerning sn partial unfold on local environments ************) - -lemma cpcs_ltpss_sn_conf: ∀L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 → - ∀T1,T2. L1 ⊢ T1 ⬌* T2 → L2 ⊢ T1 ⬌* T2. -#L1 #L2 #d #e #H -lapply (ltpss_sn_ltpssa … H) -H #H @(ltpssa_ind … H) -L2 // -#L #L2 #_ #HL2 #IHL1 #T1 #U1 #HTU1 -lapply (IHL1 … HTU1) -IHL1 -HTU1 #HTU1 -lapply (cpcs_ltpss_dx_conf … HL2 … HTU1) -HTU1 -HL2 // -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs.ma deleted file mode 100644 index 45be26781..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs.ma +++ /dev/null @@ -1,76 +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/fpc.ma". - -(* CONTEXT-FREE PARALLEL EQUIVALENCE ON CLOSURES ****************************) - -definition fpcs: bi_relation lenv term ≝ bi_TC … fpc. - -interpretation "context-free parallel equivalence (closure)" - 'FocalizedPConvStar L1 T1 L2 T2 = (fpcs L1 T1 L2 T2). - -(* Basic eliminators ********************************************************) - -lemma fpcs_ind: ∀L1,T1. ∀R:relation2 lenv term. R L1 T1 → - (∀L,L2,T,T2. ⦃L1, T1⦄ ⬌* ⦃L, T⦄ → ⦃L, T⦄ ⬌ ⦃L2, T2⦄ → R L T → R L2 T2) → - ∀L2,T2. ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄ → R L2 T2. -/3 width=7 by bi_TC_star_ind/ qed-. - -lemma fpcs_ind_dx: ∀L2,T2. ∀R:relation2 lenv term. R L2 T2 → - (∀L1,L,T1,T. ⦃L1, T1⦄ ⬌ ⦃L, T⦄ → ⦃L, T⦄ ⬌* ⦃L2, T2⦄ → R L T → R L1 T1) → - ∀L1,T1. ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄ → R L1 T1. -/3 width=7 by bi_TC_star_ind_dx/ qed-. - -(* Basic properties *********************************************************) - -lemma fpcs_refl: bi_reflexive … fpcs. -/2 width=1/ qed. - -lemma fpcs_sym: bi_symmetric … fpcs. -/3 width=1/ qed. - -lemma fpc_fpcs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⬌ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. -/2 width=1/ qed. - -lemma fpcs_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⬌* ⦃L, T⦄ → ⦃L, T⦄ ⬌ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. -/2 width=4/ qed. - -lemma fpcs_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⬌ ⦃L, T⦄ → ⦃L, T⦄ ⬌* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. -/2 width=4/ qed. - -lemma fpcs_fpr_dx: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. -/3 width=1/ qed. - -lemma fpcs_fpr_sn: ∀L1,L2,T1,T2. ⦃L2, T2⦄ ➡ ⦃L1, T1⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. -/3 width=1/ qed. - -lemma fpcs_fpr_strap1: ∀L1,L,T1,T. ⦃L1, T1⦄ ⬌* ⦃L, T⦄ → - ∀L2,T2. ⦃L, T⦄ ➡ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. -/3 width=4/ qed. - -lemma fpcs_fpr_strap2: ∀L1,L,T1,T. ⦃L1, T1⦄ ➡ ⦃L, T⦄ → - ∀L2,T2. ⦃L, T⦄ ⬌* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. -/3 width=4/ qed. - -lemma fpcs_fpr_div: ∀L1,L,T1,T. ⦃L1, T1⦄ ⬌* ⦃L, T⦄ → - ∀L2,T2. ⦃L2, T2⦄ ➡ ⦃L, T⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. -/3 width=4/ qed. - -lemma fpr_div: ∀L1,L,T1,T. ⦃L1, T1⦄ ➡ ⦃L, T⦄ → ∀L2,T2. ⦃L2, T2⦄ ➡ ⦃L, T⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. -/3 width=4/ qed-. - -lemma fpcs_fpr_conf: ∀L1,L,T1,T. ⦃L, T⦄ ➡ ⦃L1, T1⦄ → - ∀L2,T2. ⦃L, T⦄ ⬌* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. -/3 width=4/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_aaa.ma deleted file mode 100644 index 9f4327bff..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_aaa.ma +++ /dev/null @@ -1,30 +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/fprs_aaa.ma". -include "basic_2/equivalence/fpcs_fpcs.ma". - -(* CONTEXT-FREE PARALLEL EQUIVALENCE ON CLOSURES ****************************) - -(* Main properties about atomic arity assignment on terms *******************) - -theorem aaa_fpcs_mono: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄ → - ∀A1. L1 ⊢ T1 ⁝ A1 → ∀A2. L2 ⊢ T2 ⁝ A2 → - A1 = A2. -#L1 #L2 #T1 #T2 #H12 #A1 #HT1 #A2 #HT2 -elim (fpcs_inv_fprs … H12) -H12 #L #T #H1 #H2 -lapply (aaa_fprs_conf … HT1 … H1) -L1 -T1 #HT1 -lapply (aaa_fprs_conf … HT2 … H2) -L2 -T2 #HT2 -lapply (aaa_mono … HT1 … HT2) -L -T // -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_cpcs.ma deleted file mode 100644 index b1288f751..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_cpcs.ma +++ /dev/null @@ -1,86 +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/fprs_cprs.ma". -include "basic_2/equivalence/cpcs_cpcs.ma". -include "basic_2/equivalence/fpcs_fpcs.ma". - -(* CONTEXT-FREE PARALLEL EQUIVALENCE ON CLOSURES ****************************) - -(* Advanced properties ******************************************************) - -lemma fpcs_flat_dx_tpr: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄ → ∀V1,V2. V1 ➡ V2 → - ∀I. ⦃L1, ⓕ{I}V1.T1⦄ ⬌* ⦃L2, ⓕ{I}V2.T2⦄. -#L1 #L2 #T1 #T2 #HT12 -elim (fpcs_inv_fprs … HT12) -HT12 -/3 width=6 by fprs_flat_dx_tpr, fprs_div/ (**) (* auto too slow without trace *) -qed. - -lemma fpcs_shift: ∀I,L1,L2,V1,V2,T1,T2. ⦃L1, -ⓑ{I}V1.T1⦄ ⬌* ⦃L2, -ⓑ{I}V2.T2⦄ → - ⦃L1.ⓑ{I}V1, T1⦄ ⬌* ⦃L2.ⓑ{I}V2, T2⦄. -#I #L1 #L2 #V1 #V2 #T1 #T2 #H12 -elim (fpcs_inv_fprs … H12) -H12 #L #T #H1 #H2 -elim (fprs_bind2_minus … H1) -H1 #W1 #U1 #HTU1 #H destruct -elim (fprs_bind2_minus … H2) -H2 #W2 #U2 #HTU2 #H destruct /2 width=4/ -qed. - -(* Advanced inversion lemmas ************************************************) - -lemma fpcs_inv_shift: ∀I,L1,L2,V1,V2,T1,T2. ⦃L1.ⓑ{I}V1, T1⦄ ⬌* ⦃L2.ⓑ{I}V2, T2⦄ → - ⦃L1, -ⓑ{I}V1.T1⦄ ⬌* ⦃L2, -ⓑ{I}V2.T2⦄. -#I #L1 #L2 #V1 #V2 #T1 #T2 #H12 -elim (fpcs_inv_fprs … H12) -H12 #L #T #H1 #H2 -elim (fprs_inv_pair1 … H1) -H1 #K1 #U1 #_ #HTU1 #H destruct -elim (fprs_inv_pair1 … H2) -H2 #K2 #U2 #_ #HTU2 #H destruct /2 width=4/ -qed-. - -(* Advanced forward lemmas **************************************************) - -lemma fpcs_fwd_bind_minus: ∀I,L1,L2,V1,V2,T1,T2. ⦃L1, -ⓑ{I}V1.T1⦄ ⬌* ⦃L2, -ⓑ{I}V2.T2⦄ → - ∀b. ⦃L1, ⓑ{b,I}V1.T1⦄ ⬌* ⦃L2, ⓑ{b,I}V2.T2⦄. -#I #L1 #L2 #V1 #V2 #T1 #T2 #H12 #b -elim (fpcs_inv_fprs … H12) -H12 #L #T #H1 #H2 -elim (fprs_fwd_bind2_minus … H1 b) -H1 #W1 #U1 #HTU1 #H destruct -elim (fprs_fwd_bind2_minus … H2 b) -H2 #W2 #U2 #HTU2 #H destruct /2 width=4/ -qed-. - -lemma fpcs_fwd_shift: ∀I,L1,L2,V1,V2,T1,T2. ⦃L1.ⓑ{I}V1, T1⦄ ⬌* ⦃L2.ⓑ{I}V2, T2⦄ → - ∀b. ⦃L1, ⓑ{b,I}V1.T1⦄ ⬌* ⦃L2, ⓑ{b,I}V2.T2⦄. -/3 width=1 by fpcs_inv_shift, fpcs_fwd_bind_minus/ qed-. - -lemma fpcs_fwd_abst24: ∀a,L1,L2,V1,V2,T1,T2. ⦃L1, ⓛ{a}V1.T1⦄ ⬌* ⦃L2, ⓛ{a}V2.T2⦄ → - ∀b,I,W. ⦃L1, ⓑ{b,I}W.T1⦄ ⬌* ⦃L2, ⓑ{b,I}W.T2⦄. -#a #L1 #L2 #V1 #V2 #T1 #T2 #H12 #b #I #W -elim (fpcs_inv_fprs … H12) -H12 #L #U #H1 #H2 -elim (fprs_fwd_abst2 … H1 b I W) -H1 #W1 #U1 #HTU1 #H destruct -elim (fprs_fwd_abst2 … H2 b I W) -H2 #W2 #U2 #HTU2 #H destruct /2 width=4/ -qed-. - -lemma fpcs_fwd_abst13: ∀L1,L2,V1,V2,T1,T2. ⦃L1.ⓛV1, T1⦄ ⬌* ⦃L2.ⓛV2, T2⦄ → - ∀I,W. ⦃L1.ⓑ{I}W, T1⦄ ⬌* ⦃L2.ⓑ{I}W, T2⦄. -/4 width=4 by fpcs_fwd_shift, fpcs_fwd_abst24, fpcs_shift/ qed-. - -(* Properties on context-sensitive parallel equivalence for terms ***********) - -lemma cpcs_fpcs: ∀L,T1,T2. L ⊢ T1 ⬌* T2 → ⦃L, T1⦄ ⬌* ⦃L, T2⦄. -#L #T1 #T2 #H -elim (cpcs_inv_cprs … H) -H /3 width=4 by fprs_div, cprs_fprs/ (**) (* too slow without trace *) -qed. - -(* Inversion lemmas on context-sensitive parallel equivalence for terms *****) - -lemma fpcs_inv_cpcs: ∀L,T1,T2. ⦃L, T1⦄ ⬌* ⦃L, T2⦄ → L ⊢ T1 ⬌* T2. -#L #T1 #T2 #H -elim (fpcs_inv_fprs … H) -H /3 width=4 by cprs_div, fprs_fwd_cprs/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_fpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_fpcs.ma deleted file mode 100644 index 270e8dc40..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_fpcs.ma +++ /dev/null @@ -1,66 +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/fprs_fprs.ma". -include "basic_2/conversion/fpc_fpc.ma". -include "basic_2/equivalence/fpcs_fprs.ma". - -(* CONTEXT-FREE PARALLEL EQUIVALENCE ON CLOSURES ****************************) - -(* Advanced inversion lemmas ************************************************) - -lemma fpcs_inv_fprs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄ → - ∃∃L,T. ⦃L1, T1⦄ ➡* ⦃L, T⦄ & ⦃L2, T2⦄ ➡* ⦃L, T⦄. -#L1 #L2 #T1 #T2 #H @(fpcs_ind … H) -L2 -T2 -[ /3 width=4/ -| #L #L2 #T #T2 #_ #HT2 * #L0 #T0 #HT10 elim HT2 -HT2 #HT2 #HT0 - [ elim (fprs_strip … HT2 … HT0) -L -T #L #T #HT2 #HT0 - lapply (fprs_strap1 … HT10 … HT0) -L0 -T0 /2 width=4/ - | lapply (fprs_strap2 … HT2 … HT0) -L -T /2 width=4/ - ] -] -qed-. - -(* Advanced properties ******************************************************) - -lemma fpr_fprs_conf: ∀L,L1,L2,T,T1,T2. ⦃L, T⦄ ➡* ⦃L1, T1⦄ → ⦃L, T⦄ ➡ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. -#L #L1 #L2 #T #T1 #T2 #HT1 #HT2 -elim (fprs_strip … HT2 … HT1) /2 width=4 by fpr_fprs_div/ -qed-. - -lemma fprs_fpr_conf: ∀L,L1,L2,T,T1,T2. ⦃L, T⦄ ➡* ⦃L1, T1⦄ → ⦃L, T⦄ ➡ ⦃L2, T2⦄ → ⦃L2, T2⦄ ⬌* ⦃L1, T1⦄. -#L #L1 #L2 #T #T1 #T2 #HT1 #HT2 -elim (fprs_strip … HT2 … HT1) /2 width=4 by fprs_fpr_div/ -qed-. - -lemma fprs_conf: ∀L,L1,L2,T,T1,T2. ⦃L, T⦄ ➡* ⦃L1, T1⦄ → ⦃L, T⦄ ➡* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. -#L #L1 #L2 #T #T1 #T2 #HT1 #HT2 -elim (fprs_conf … HT1 … HT2) /2 width=4/ -qed-. - -lemma fpcs_strip: ∀L0,L1,T0,T1. ⦃L0, T0⦄ ⬌ ⦃L1, T1⦄ → - ∀L2,T2. ⦃L0, T0⦄ ⬌* ⦃L2, T2⦄ → - ∃∃L,T. ⦃L1, T1⦄ ⬌* ⦃L, T⦄ & ⦃L2, T2⦄ ⬌ ⦃L, T⦄. -/3 width=4/ qed. - -(* Main properties **********************************************************) - -theorem fpcs_trans: bi_transitive … fpcs. -/2 width=4/ qed. - -theorem fpcs_canc_sn: ∀L,L1,L2,T,T1,T2. ⦃L, T⦄ ⬌* ⦃L1, T1⦄ → ⦃L, T⦄ ⬌* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. -/3 width=4 by fpcs_trans, fpcs_sym/ qed. (**) (* /3 width=3/ is too slow *) - -theorem fpcs_canc_dx: ∀L1,L2,L,T1,T2,T. ⦃L1, T1⦄ ⬌* ⦃L, T⦄ → ⦃L2, T2⦄ ⬌* ⦃L, T⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. -/3 width=4 by fpcs_trans, fpcs_sym/ qed. (**) (* /3 width=3/ is too slow *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_fprs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_fprs.ma deleted file mode 100644 index 1d3f71f9e..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_fprs.ma +++ /dev/null @@ -1,55 +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/fprs.ma". -include "basic_2/equivalence/fpcs.ma". - -(* CONTEXT-FREE PARALLEL EQUIVALENCE ON CLOSURES ****************************) - -(* Properties on context-free parallel computation for closures *************) - -(* Note: lemma 1000 *) -lemma fpcs_fprs_dx: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. -#L1 #L2 #T1 #T2 #H @(fprs_ind … H) -L2 -T2 /width=1/ /3 width=4/ -qed. - -lemma fpcs_fprs_sn: ∀L1,L2,T1,T2. ⦃L2, T2⦄ ➡* ⦃L1, T1⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. -#L1 #L2 #T1 #T2 #H @(fprs_ind_dx … H) -L2 -T2 /width=1/ /3 width=4/ -qed. - -lemma fpcs_fprs_strap1: ∀L1,L,T1,T. ⦃L1, T1⦄ ⬌* ⦃L, T⦄ → ∀L2,T2. ⦃L, T⦄ ➡* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. -#L1 #L #T1 #T #HT1 #L2 #T2 #H @(fprs_ind … H) -L2 -T2 /width=1/ /2 width=4/ -qed. - -lemma fpcs_fprs_strap2: ∀L1,L,T1,T. ⦃L1, T1⦄ ➡* ⦃L, T⦄ → ∀L2,T2. ⦃L, T⦄ ⬌* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. -#L1 #L #T1 #T #H #L2 #T2 #HT2 @(fprs_ind_dx … H) -L1 -T1 /width=1/ /2 width=4/ -qed. - -lemma fpcs_fprs_div: ∀L1,L,T1,T. ⦃L1, T1⦄ ⬌* ⦃L, T⦄ → ∀L2,T2. ⦃L2, T2⦄ ➡* ⦃L, T⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. -#L1 #L #T1 #T #HT1 #L2 #T2 #H @(fprs_ind_dx … H) -L2 -T2 /width=1/ /2 width=4/ -qed. - -lemma fpcs_fprs_conf: ∀L1,L,T1,T. ⦃L, T⦄ ➡* ⦃L1, T1⦄ → ∀L2,T2. ⦃L, T⦄ ⬌* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. -#L1 #L #T1 #T #H #T2 #HT2 @(fprs_ind … H) -L1 -T1 /width=1/ /3 width=4 by fpcs_fpr_conf/ (**) (* /2 width=4/ does not work *) -qed. - -lemma fprs_div: ∀L1,L,T1,T. ⦃L1, T1⦄ ➡* ⦃L, T⦄ → ∀L2,T2. ⦃L2, T2⦄ ➡* ⦃L, T⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. -#L1 #L #T1 #T #HT1 #T2 #L2 #H @(fprs_ind_dx … H) -L2 -T2 /2 width=1/ /2 width=4/ -qed. - -lemma fprs_fpr_div: ∀L1,L,T1,T. ⦃L1, T1⦄ ➡* ⦃L, T⦄ → ∀L2,T2. ⦃L2, T2⦄ ➡ ⦃L, T⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. -/3 width=7 by bi_step, fprs_div/ qed-. - -lemma fpr_fprs_div: ∀L1,L,T1,T. ⦃L1, T1⦄ ➡ ⦃L, T⦄ → ∀L2,T2. ⦃L2, T2⦄ ➡* ⦃L, T⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. -/3 width=4 by bi_step, fprs_div/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs.ma deleted file mode 100644 index 5ad9180ac..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs.ma +++ /dev/null @@ -1,72 +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/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: reflexive … lfpcs. -/2 width=1/ qed. - -lemma lfpcs_sym: symmetric … lfpcs. -/3 width=1/ qed. - -lemma lfpc_lfpcs: ∀L1,L2. ⦃L1⦄ ⬌ ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. -/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. diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_aaa.ma deleted file mode 100644 index b7cea0b7a..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_aaa.ma +++ /dev/null @@ -1,30 +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/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/lambdadelta/basic_2/equivalence/lfpcs_fpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_fpcs.ma deleted file mode 100644 index 8f3688890..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_fpcs.ma +++ /dev/null @@ -1,52 +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/fprs_cprs.ma". -include "basic_2/computation/lfprs_fprs.ma". -include "basic_2/equivalence/fpcs_fpcs.ma". -include "basic_2/equivalence/lfpcs_lfpcs.ma". - -(* FOCALIZED PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *********************) - -(* Inversion lemmas on context-free parallel equivalence for closures *******) - -lemma lfpcs_inv_fpcs: ∀L1,L2. ⦃L1⦄ ⬌* ⦃L2⦄ → ∀T. ⦃L1, T⦄ ⬌* ⦃L2, T⦄. -#L1 #L2 #HL12 #T -elim (lfpcs_inv_lfprs … HL12) -HL12 #L #HL1 #HL2 -lapply (lfprs_inv_fprs … HL1 T) -HL1 -lapply (lfprs_inv_fprs … HL2 T) -HL2 /2 width=4/ -qed-. - -(* Properties on context-free parallel equivalence for closures *************) - -lemma fpcs_lfpcs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. -#L1 #L2 #T1 #T2 #HT12 -elim (fpcs_inv_fprs … HT12) -HT12 /3 width=5 by fprs_lfprs, lfprs_div/ (**) (* auto too slow without trace *) -qed. - -lemma fpcs_lift: ∀K1,K2,T1,T2. ⦃K1, T1⦄ ⬌* ⦃K2, T2⦄ → - ∀L1,L2. ⦃L1⦄ ⬌* ⦃L2⦄ → - ∀d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 → - ∀U1,U2. ⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 → - ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄. -#K1 #K2 #T1 #T2 #HT12 #L1 #L2 #HL12 #d #e #HLK1 #HLK2 #U1 #U2 #HTU1 #HTU2 -elim (fpcs_inv_fprs … HT12) -HT12 #K #T #HT1 #HT2 -elim (lift_total T d e) #U #HTU -elim (fprs_lift … HT1 … HLK1 … HTU1 HTU) -K1 -T1 #K1 #HU1 #_ -elim (fprs_lift … HT2 … HLK2 … HTU2 HTU) -K2 -T2 -T #K2 #HU2 #_ -K -d -e -lapply (lfpcs_lfprs_conf K1 … HL12) -HL12 /2 width=3/ #H -lapply (lfpcs_lfprs_strap1 … H K2 ?) -H /2 width=3/ #HK12 -lapply (lfpcs_inv_fpcs … HK12 U) -HK12 #HU -/3 width=4 by fpcs_fprs_strap2, fpcs_fprs_div/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_lfpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_lfpcs.ma deleted file mode 100644 index 1e9521736..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_lfpcs.ma +++ /dev/null @@ -1,50 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/computation/lfprs_lfprs.ma". -include "basic_2/conversion/lfpc_lfpc.ma". -include "basic_2/equivalence/lfpcs_lfprs.ma". - -(* FOCALIZED PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *********************) - -(* Advanced inversion lemmas ************************************************) - -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 (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 lfpcs_strip: ∀L,L1. ⦃L⦄ ⬌* ⦃L1⦄ → ∀L2. ⦃L⦄ ⬌ ⦃L2⦄ → - ∃∃L0. ⦃L1⦄ ⬌ ⦃L0⦄ & ⦃L2⦄ ⬌* ⦃L0⦄. -/3 width=3/ qed. - -(* Main properties **********************************************************) - -theorem lfpcs_trans: ∀L1,L. ⦃L1⦄ ⬌* ⦃L⦄ → ∀L2. ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. -/2 width=3/ qed. - -theorem lfpcs_canc_sn: ∀L,L1,L2. ⦃L⦄ ⬌* ⦃L1⦄ → ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. -/3 width=3 by lfpcs_trans, lfpcs_sym/ qed. - -theorem lfpcs_canc_dx: ∀L,L1,L2. ⦃L1⦄ ⬌* ⦃L⦄ → ⦃L2⦄ ⬌* ⦃L⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. -/3 width=3 by lfpcs_trans, lfpcs_sym/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_lfprs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_lfprs.ma deleted file mode 100644 index baf2caf27..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_lfprs.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/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/lambdadelta/basic_2/equivalence/lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubss.ma index 364f06ade..db3d75f52 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubss.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubss.ma @@ -94,11 +94,11 @@ lemma lsubss_inv_pair2: ∀h,g,I,L1,K2,W2. h ⊢ L1 •⊑[g] K2. ⓑ{I} W2 → (* Basic_forward lemmas *****************************************************) -lemma lsubss_fwd_lsubr1: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 ⊑[0, |L1|] L2. +lemma lsubss_fwd_lsubr1: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 ⊑ L2. #h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ qed-. -lemma lsubss_fwd_lsubr2: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 ⊑[0, |L2|] L2. +lemma lsubss_fwd_lsubr2: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 ⊑ L2. #h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpcs_ltpss_dx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpcs_ltpss_dx.etc new file mode 100644 index 000000000..80f418b08 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpcs_ltpss_dx.etc @@ -0,0 +1,50 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/computation/cprs_ltpss_dx.ma". +include "basic_2/equivalence/cpcs_cpcs.ma". + +(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) + +(* Properties concerning dx partial unfold on local environments ************) + +lemma cpcs_ltpss_dx_conf: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → + ∀T1,T2. L1 ⊢ T1 ⬌* T2 → L2 ⊢ T1 ⬌* T2. +#L1 #L2 #d #e #HL12 #T1 #T2 #H +elim (cpcs_inv_cprs … H) -H #T #HT1 #HT2 +elim (cprs_ltpss_dx_conf … HT1 … HL12) -HT1 #U1 #HTU1 #H1 +elim (cprs_ltpss_dx_conf … HT2 … HL12) -L1 #U2 #HTU2 #H2 +elim (tpss_conf_eq … H1 … H2) -T #U #HU1 #HU2 +lapply (cprs_tpss_trans … HTU1 … HU1) -U1 +lapply (cprs_tpss_trans … HTU2 … HU2) -U2 /2 width=3/ +qed-. + +lemma cpcs_ltpss_dx_tpss_conf: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → + ∀T,T2. L1 ⊢ T ⬌* T2 → + ∀T1. L2 ⊢ T ▶* [d, e] T1 → + L2 ⊢ T1 ⬌* T2. +#L1 #L2 #d #e #HL12 #T #T2 #HT2 #T1 #HT1 +lapply (cpcs_ltpss_dx_conf … HL12 … HT2) -L1 #HT2 +lapply (cpcs_tpss_conf … HT1 … HT2) -T // +qed-. + +lemma cpcs_ltpss_dx_tpss2_conf: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → + ∀T1,T2. L1 ⊢ T1 ⬌* T2 → + ∀T3. L2 ⊢ T1 ▶* [d, e] T3 → + ∀T4. L2 ⊢ T2 ▶* [d, e] T4 → + L2 ⊢ T3 ⬌* T4. +#L1 #L2 #d #e #HL12 #T1 #T2 #HT12 #T3 #HT13 #T4 #HT24 +lapply (cpcs_ltpss_dx_tpss_conf … HL12 … HT12 … HT13) -L1 -T1 #HT32 +lapply (cpcs_tpss_strap1 … HT32 … HT24) -T2 // +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpcs_ltpss_sn.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpcs_ltpss_sn.etc new file mode 100644 index 000000000..5bf1ed57f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpcs_ltpss_sn.etc @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/equivalence/cpcs_ltpss_dx.ma". + +(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) + +(* Properties concerning sn partial unfold on local environments ************) + +lemma cpcs_ltpss_sn_conf: ∀L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 → + ∀T1,T2. L1 ⊢ T1 ⬌* T2 → L2 ⊢ T1 ⬌* T2. +#L1 #L2 #d #e #H +lapply (ltpss_sn_ltpssa … H) -H #H @(ltpssa_ind … H) -L2 // +#L #L2 #_ #HL2 #IHL1 #T1 #U1 #HTU1 +lapply (IHL1 … HTU1) -IHL1 -HTU1 #HTU1 +lapply (cpcs_ltpss_dx_conf … HL2 … HTU1) -HTU1 -HL2 // +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/delift/cpcs_delift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/delift/cpcs_delift.etc new file mode 100644 index 000000000..7012ec11e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/delift/cpcs_delift.etc @@ -0,0 +1,37 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/unfold/delift_lift.ma". +include "basic_2/unfold/delift_delift.ma". +include "basic_2/computation/cprs_delift.ma". +include "basic_2/equivalence/cpcs_cpcs.ma". + +(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) + +(* Properties on inverse basic term relocation ******************************) + +lemma cpcs_zeta_delift_comm: ∀L,V,T1,T2. L.ⓓV ⊢ ▼*[O, 1] T1 ≡ T2 → + L ⊢ T2 ⬌* +ⓓV.T1. +/3 width=1/ qed. + +(* Basic_1: was only: pc3_gen_cabbr *) +lemma thin_cpcs_delift_mono: ∀L,U1,U2. L ⊢ U1 ⬌* U2 → + ∀K,d,e. ▼*[d, e] L ≡ K → ∀T1. L ⊢ ▼*[d, e] U1 ≡ T1 → + ∀T2. L ⊢ ▼*[d, e] U2 ≡ T2 → K ⊢ T1 ⬌* T2. +#L #U1 #U2 #H #K #d #e #HLK #T1 #HTU1 #T2 #HTU2 +elim (cpcs_inv_cprs … H) -H #U #HU1 #HU2 +elim (thin_cprs_delift_conf … HU1 … HLK … HTU1) -U1 #T #HT1 #HUT +elim (thin_cprs_delift_conf … HU2 … HLK … HTU2) -U2 -HLK #X #HT2 #H +lapply (delift_mono … H … HUT) -L #H destruct /2 width=3/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpc.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpc.etc new file mode 100644 index 000000000..f552d5818 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpc.etc @@ -0,0 +1,40 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/reducibility/fpr.ma". + +(* CONTEXT-FREE PARALLEL CONVERSION ON CLOSURES *****************************) + +definition fpc: bi_relation lenv term ≝ + λL1,T1,L2,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ ∨ ⦃L2, T2⦄ ➡ ⦃L1, T1⦄. + +interpretation + "context-free parallel conversion (closure)" + 'FocalizedPConv L1 T1 L2 T2 = (fpc L1 T1 L2 T2). + +(* Basic properties *********************************************************) + +lemma fpc_refl: bi_reflexive … fpc. +/2 width=1/ qed. + +lemma fpc_sym: bi_symmetric … fpc. +#L1 #L2 #T1 #T2 * /2 width=1/ +qed. + +(* Basic forward lemmas *****************************************************) + +lemma fpc_fwd_fpr: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⬌ ⦃L2, T2⦄ → + ∃∃L,T. ⦃L1, T1⦄ ➡ ⦃L, T⦄ & ⦃L2, T2⦄ ➡ ⦃L, T⦄. +#L1 #L2 #T1 #T2 * /2 width=4/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpc_fpc.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpc_fpc.etc new file mode 100644 index 000000000..22fc16f37 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpc_fpc.etc @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/conversion/fpc.ma". + +(* CONTEXT-FREE PARALLEL CONVERSION ON CLOSURES *****************************) + +(* Main properties **********************************************************) + +theorem fpc_conf: ∀L0,L1,T0,T1. ⦃L0, T0⦄ ⬌ ⦃L1, T1⦄ → + ∀L2,T2. ⦃L0, T0⦄ ⬌ ⦃L2, T2⦄ → + ∃∃L,T. ⦃L1, T1⦄ ⬌ ⦃L, T⦄ & ⦃L2, T2⦄ ⬌ ⦃L, T⦄. +/3 width=4/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs.etc new file mode 100644 index 000000000..45be26781 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs.etc @@ -0,0 +1,76 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fpc.ma". + +(* CONTEXT-FREE PARALLEL EQUIVALENCE ON CLOSURES ****************************) + +definition fpcs: bi_relation lenv term ≝ bi_TC … fpc. + +interpretation "context-free parallel equivalence (closure)" + 'FocalizedPConvStar L1 T1 L2 T2 = (fpcs L1 T1 L2 T2). + +(* Basic eliminators ********************************************************) + +lemma fpcs_ind: ∀L1,T1. ∀R:relation2 lenv term. R L1 T1 → + (∀L,L2,T,T2. ⦃L1, T1⦄ ⬌* ⦃L, T⦄ → ⦃L, T⦄ ⬌ ⦃L2, T2⦄ → R L T → R L2 T2) → + ∀L2,T2. ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄ → R L2 T2. +/3 width=7 by bi_TC_star_ind/ qed-. + +lemma fpcs_ind_dx: ∀L2,T2. ∀R:relation2 lenv term. R L2 T2 → + (∀L1,L,T1,T. ⦃L1, T1⦄ ⬌ ⦃L, T⦄ → ⦃L, T⦄ ⬌* ⦃L2, T2⦄ → R L T → R L1 T1) → + ∀L1,T1. ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄ → R L1 T1. +/3 width=7 by bi_TC_star_ind_dx/ qed-. + +(* Basic properties *********************************************************) + +lemma fpcs_refl: bi_reflexive … fpcs. +/2 width=1/ qed. + +lemma fpcs_sym: bi_symmetric … fpcs. +/3 width=1/ qed. + +lemma fpc_fpcs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⬌ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +/2 width=1/ qed. + +lemma fpcs_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⬌* ⦃L, T⦄ → ⦃L, T⦄ ⬌ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +/2 width=4/ qed. + +lemma fpcs_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⬌ ⦃L, T⦄ → ⦃L, T⦄ ⬌* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +/2 width=4/ qed. + +lemma fpcs_fpr_dx: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +/3 width=1/ qed. + +lemma fpcs_fpr_sn: ∀L1,L2,T1,T2. ⦃L2, T2⦄ ➡ ⦃L1, T1⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +/3 width=1/ qed. + +lemma fpcs_fpr_strap1: ∀L1,L,T1,T. ⦃L1, T1⦄ ⬌* ⦃L, T⦄ → + ∀L2,T2. ⦃L, T⦄ ➡ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +/3 width=4/ qed. + +lemma fpcs_fpr_strap2: ∀L1,L,T1,T. ⦃L1, T1⦄ ➡ ⦃L, T⦄ → + ∀L2,T2. ⦃L, T⦄ ⬌* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +/3 width=4/ qed. + +lemma fpcs_fpr_div: ∀L1,L,T1,T. ⦃L1, T1⦄ ⬌* ⦃L, T⦄ → + ∀L2,T2. ⦃L2, T2⦄ ➡ ⦃L, T⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +/3 width=4/ qed. + +lemma fpr_div: ∀L1,L,T1,T. ⦃L1, T1⦄ ➡ ⦃L, T⦄ → ∀L2,T2. ⦃L2, T2⦄ ➡ ⦃L, T⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +/3 width=4/ qed-. + +lemma fpcs_fpr_conf: ∀L1,L,T1,T. ⦃L, T⦄ ➡ ⦃L1, T1⦄ → + ∀L2,T2. ⦃L, T⦄ ⬌* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +/3 width=4/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs_aaa.etc new file mode 100644 index 000000000..9f4327bff --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs_aaa.etc @@ -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/fprs_aaa.ma". +include "basic_2/equivalence/fpcs_fpcs.ma". + +(* CONTEXT-FREE PARALLEL EQUIVALENCE ON CLOSURES ****************************) + +(* Main properties about atomic arity assignment on terms *******************) + +theorem aaa_fpcs_mono: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄ → + ∀A1. L1 ⊢ T1 ⁝ A1 → ∀A2. L2 ⊢ T2 ⁝ A2 → + A1 = A2. +#L1 #L2 #T1 #T2 #H12 #A1 #HT1 #A2 #HT2 +elim (fpcs_inv_fprs … H12) -H12 #L #T #H1 #H2 +lapply (aaa_fprs_conf … HT1 … H1) -L1 -T1 #HT1 +lapply (aaa_fprs_conf … HT2 … H2) -L2 -T2 #HT2 +lapply (aaa_mono … HT1 … HT2) -L -T // +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs_cpcs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs_cpcs.etc new file mode 100644 index 000000000..b1288f751 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs_cpcs.etc @@ -0,0 +1,86 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fprs_cprs.ma". +include "basic_2/equivalence/cpcs_cpcs.ma". +include "basic_2/equivalence/fpcs_fpcs.ma". + +(* CONTEXT-FREE PARALLEL EQUIVALENCE ON CLOSURES ****************************) + +(* Advanced properties ******************************************************) + +lemma fpcs_flat_dx_tpr: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄ → ∀V1,V2. V1 ➡ V2 → + ∀I. ⦃L1, ⓕ{I}V1.T1⦄ ⬌* ⦃L2, ⓕ{I}V2.T2⦄. +#L1 #L2 #T1 #T2 #HT12 +elim (fpcs_inv_fprs … HT12) -HT12 +/3 width=6 by fprs_flat_dx_tpr, fprs_div/ (**) (* auto too slow without trace *) +qed. + +lemma fpcs_shift: ∀I,L1,L2,V1,V2,T1,T2. ⦃L1, -ⓑ{I}V1.T1⦄ ⬌* ⦃L2, -ⓑ{I}V2.T2⦄ → + ⦃L1.ⓑ{I}V1, T1⦄ ⬌* ⦃L2.ⓑ{I}V2, T2⦄. +#I #L1 #L2 #V1 #V2 #T1 #T2 #H12 +elim (fpcs_inv_fprs … H12) -H12 #L #T #H1 #H2 +elim (fprs_bind2_minus … H1) -H1 #W1 #U1 #HTU1 #H destruct +elim (fprs_bind2_minus … H2) -H2 #W2 #U2 #HTU2 #H destruct /2 width=4/ +qed. + +(* Advanced inversion lemmas ************************************************) + +lemma fpcs_inv_shift: ∀I,L1,L2,V1,V2,T1,T2. ⦃L1.ⓑ{I}V1, T1⦄ ⬌* ⦃L2.ⓑ{I}V2, T2⦄ → + ⦃L1, -ⓑ{I}V1.T1⦄ ⬌* ⦃L2, -ⓑ{I}V2.T2⦄. +#I #L1 #L2 #V1 #V2 #T1 #T2 #H12 +elim (fpcs_inv_fprs … H12) -H12 #L #T #H1 #H2 +elim (fprs_inv_pair1 … H1) -H1 #K1 #U1 #_ #HTU1 #H destruct +elim (fprs_inv_pair1 … H2) -H2 #K2 #U2 #_ #HTU2 #H destruct /2 width=4/ +qed-. + +(* Advanced forward lemmas **************************************************) + +lemma fpcs_fwd_bind_minus: ∀I,L1,L2,V1,V2,T1,T2. ⦃L1, -ⓑ{I}V1.T1⦄ ⬌* ⦃L2, -ⓑ{I}V2.T2⦄ → + ∀b. ⦃L1, ⓑ{b,I}V1.T1⦄ ⬌* ⦃L2, ⓑ{b,I}V2.T2⦄. +#I #L1 #L2 #V1 #V2 #T1 #T2 #H12 #b +elim (fpcs_inv_fprs … H12) -H12 #L #T #H1 #H2 +elim (fprs_fwd_bind2_minus … H1 b) -H1 #W1 #U1 #HTU1 #H destruct +elim (fprs_fwd_bind2_minus … H2 b) -H2 #W2 #U2 #HTU2 #H destruct /2 width=4/ +qed-. + +lemma fpcs_fwd_shift: ∀I,L1,L2,V1,V2,T1,T2. ⦃L1.ⓑ{I}V1, T1⦄ ⬌* ⦃L2.ⓑ{I}V2, T2⦄ → + ∀b. ⦃L1, ⓑ{b,I}V1.T1⦄ ⬌* ⦃L2, ⓑ{b,I}V2.T2⦄. +/3 width=1 by fpcs_inv_shift, fpcs_fwd_bind_minus/ qed-. + +lemma fpcs_fwd_abst24: ∀a,L1,L2,V1,V2,T1,T2. ⦃L1, ⓛ{a}V1.T1⦄ ⬌* ⦃L2, ⓛ{a}V2.T2⦄ → + ∀b,I,W. ⦃L1, ⓑ{b,I}W.T1⦄ ⬌* ⦃L2, ⓑ{b,I}W.T2⦄. +#a #L1 #L2 #V1 #V2 #T1 #T2 #H12 #b #I #W +elim (fpcs_inv_fprs … H12) -H12 #L #U #H1 #H2 +elim (fprs_fwd_abst2 … H1 b I W) -H1 #W1 #U1 #HTU1 #H destruct +elim (fprs_fwd_abst2 … H2 b I W) -H2 #W2 #U2 #HTU2 #H destruct /2 width=4/ +qed-. + +lemma fpcs_fwd_abst13: ∀L1,L2,V1,V2,T1,T2. ⦃L1.ⓛV1, T1⦄ ⬌* ⦃L2.ⓛV2, T2⦄ → + ∀I,W. ⦃L1.ⓑ{I}W, T1⦄ ⬌* ⦃L2.ⓑ{I}W, T2⦄. +/4 width=4 by fpcs_fwd_shift, fpcs_fwd_abst24, fpcs_shift/ qed-. + +(* Properties on context-sensitive parallel equivalence for terms ***********) + +lemma cpcs_fpcs: ∀L,T1,T2. L ⊢ T1 ⬌* T2 → ⦃L, T1⦄ ⬌* ⦃L, T2⦄. +#L #T1 #T2 #H +elim (cpcs_inv_cprs … H) -H /3 width=4 by fprs_div, cprs_fprs/ (**) (* too slow without trace *) +qed. + +(* Inversion lemmas on context-sensitive parallel equivalence for terms *****) + +lemma fpcs_inv_cpcs: ∀L,T1,T2. ⦃L, T1⦄ ⬌* ⦃L, T2⦄ → L ⊢ T1 ⬌* T2. +#L #T1 #T2 #H +elim (fpcs_inv_fprs … H) -H /3 width=4 by cprs_div, fprs_fwd_cprs/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs_fpcs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs_fpcs.etc new file mode 100644 index 000000000..270e8dc40 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs_fpcs.etc @@ -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/computation/fprs_fprs.ma". +include "basic_2/conversion/fpc_fpc.ma". +include "basic_2/equivalence/fpcs_fprs.ma". + +(* CONTEXT-FREE PARALLEL EQUIVALENCE ON CLOSURES ****************************) + +(* Advanced inversion lemmas ************************************************) + +lemma fpcs_inv_fprs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄ → + ∃∃L,T. ⦃L1, T1⦄ ➡* ⦃L, T⦄ & ⦃L2, T2⦄ ➡* ⦃L, T⦄. +#L1 #L2 #T1 #T2 #H @(fpcs_ind … H) -L2 -T2 +[ /3 width=4/ +| #L #L2 #T #T2 #_ #HT2 * #L0 #T0 #HT10 elim HT2 -HT2 #HT2 #HT0 + [ elim (fprs_strip … HT2 … HT0) -L -T #L #T #HT2 #HT0 + lapply (fprs_strap1 … HT10 … HT0) -L0 -T0 /2 width=4/ + | lapply (fprs_strap2 … HT2 … HT0) -L -T /2 width=4/ + ] +] +qed-. + +(* Advanced properties ******************************************************) + +lemma fpr_fprs_conf: ∀L,L1,L2,T,T1,T2. ⦃L, T⦄ ➡* ⦃L1, T1⦄ → ⦃L, T⦄ ➡ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +#L #L1 #L2 #T #T1 #T2 #HT1 #HT2 +elim (fprs_strip … HT2 … HT1) /2 width=4 by fpr_fprs_div/ +qed-. + +lemma fprs_fpr_conf: ∀L,L1,L2,T,T1,T2. ⦃L, T⦄ ➡* ⦃L1, T1⦄ → ⦃L, T⦄ ➡ ⦃L2, T2⦄ → ⦃L2, T2⦄ ⬌* ⦃L1, T1⦄. +#L #L1 #L2 #T #T1 #T2 #HT1 #HT2 +elim (fprs_strip … HT2 … HT1) /2 width=4 by fprs_fpr_div/ +qed-. + +lemma fprs_conf: ∀L,L1,L2,T,T1,T2. ⦃L, T⦄ ➡* ⦃L1, T1⦄ → ⦃L, T⦄ ➡* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +#L #L1 #L2 #T #T1 #T2 #HT1 #HT2 +elim (fprs_conf … HT1 … HT2) /2 width=4/ +qed-. + +lemma fpcs_strip: ∀L0,L1,T0,T1. ⦃L0, T0⦄ ⬌ ⦃L1, T1⦄ → + ∀L2,T2. ⦃L0, T0⦄ ⬌* ⦃L2, T2⦄ → + ∃∃L,T. ⦃L1, T1⦄ ⬌* ⦃L, T⦄ & ⦃L2, T2⦄ ⬌ ⦃L, T⦄. +/3 width=4/ qed. + +(* Main properties **********************************************************) + +theorem fpcs_trans: bi_transitive … fpcs. +/2 width=4/ qed. + +theorem fpcs_canc_sn: ∀L,L1,L2,T,T1,T2. ⦃L, T⦄ ⬌* ⦃L1, T1⦄ → ⦃L, T⦄ ⬌* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +/3 width=4 by fpcs_trans, fpcs_sym/ qed. (**) (* /3 width=3/ is too slow *) + +theorem fpcs_canc_dx: ∀L1,L2,L,T1,T2,T. ⦃L1, T1⦄ ⬌* ⦃L, T⦄ → ⦃L2, T2⦄ ⬌* ⦃L, T⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +/3 width=4 by fpcs_trans, fpcs_sym/ qed. (**) (* /3 width=3/ is too slow *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs_fprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs_fprs.etc new file mode 100644 index 000000000..43239eadd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fpcs_fprs.etc @@ -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/computation/fprs.ma". +include "basic_2/equivalence/fpcs.ma". + +(* CONTEXT-FREE PARALLEL EQUIVALENCE ON CLOSURES ****************************) + +(* Properties on context-free parallel computation for closures *************) + +(* Note: was lemma 1000 *) +lemma fpcs_fprs_dx: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +#L1 #L2 #T1 #T2 #H @(fprs_ind … H) -L2 -T2 /width=1/ /3 width=4/ +qed. + +lemma fpcs_fprs_sn: ∀L1,L2,T1,T2. ⦃L2, T2⦄ ➡* ⦃L1, T1⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +#L1 #L2 #T1 #T2 #H @(fprs_ind_dx … H) -L2 -T2 /width=1/ /3 width=4/ +qed. + +lemma fpcs_fprs_strap1: ∀L1,L,T1,T. ⦃L1, T1⦄ ⬌* ⦃L, T⦄ → ∀L2,T2. ⦃L, T⦄ ➡* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +#L1 #L #T1 #T #HT1 #L2 #T2 #H @(fprs_ind … H) -L2 -T2 /width=1/ /2 width=4/ +qed. + +lemma fpcs_fprs_strap2: ∀L1,L,T1,T. ⦃L1, T1⦄ ➡* ⦃L, T⦄ → ∀L2,T2. ⦃L, T⦄ ⬌* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +#L1 #L #T1 #T #H #L2 #T2 #HT2 @(fprs_ind_dx … H) -L1 -T1 /width=1/ /2 width=4/ +qed. + +lemma fpcs_fprs_div: ∀L1,L,T1,T. ⦃L1, T1⦄ ⬌* ⦃L, T⦄ → ∀L2,T2. ⦃L2, T2⦄ ➡* ⦃L, T⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +#L1 #L #T1 #T #HT1 #L2 #T2 #H @(fprs_ind_dx … H) -L2 -T2 /width=1/ /2 width=4/ +qed. + +lemma fpcs_fprs_conf: ∀L1,L,T1,T. ⦃L, T⦄ ➡* ⦃L1, T1⦄ → ∀L2,T2. ⦃L, T⦄ ⬌* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +#L1 #L #T1 #T #H #T2 #HT2 @(fprs_ind … H) -L1 -T1 /width=1/ /3 width=4 by fpcs_fpr_conf/ (**) (* /2 width=4/ does not work *) +qed. + +lemma fprs_div: ∀L1,L,T1,T. ⦃L1, T1⦄ ➡* ⦃L, T⦄ → ∀L2,T2. ⦃L2, T2⦄ ➡* ⦃L, T⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +#L1 #L #T1 #T #HT1 #T2 #L2 #H @(fprs_ind_dx … H) -L2 -T2 /2 width=1/ /2 width=4/ +qed. + +lemma fprs_fpr_div: ∀L1,L,T1,T. ⦃L1, T1⦄ ➡* ⦃L, T⦄ → ∀L2,T2. ⦃L2, T2⦄ ➡ ⦃L, T⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +/3 width=7 by bi_step, fprs_div/ qed-. + +lemma fpr_fprs_div: ∀L1,L,T1,T. ⦃L1, T1⦄ ➡ ⦃L, T⦄ → ∀L2,T2. ⦃L2, T2⦄ ➡* ⦃L, T⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +/3 width=4 by bi_step, fprs_div/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpc.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpc.etc new file mode 100644 index 000000000..273873abd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpc.etc @@ -0,0 +1,37 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/reducibility/lfpr.ma". + +(* FOCALIZED PARALLEL CONVERSION ON LOCAL ENVIRONMENTS **********************) + +definition lfpc: relation lenv ≝ + λL1,L2. ⦃L1⦄ ➡ ⦃L2⦄ ∨ ⦃L2⦄ ➡ ⦃L1⦄. + +interpretation + "focalized parallel conversion (local environment)" + 'FocalizedPConv L1 L2 = (lfpc L1 L2). + +(* Basic properties *********************************************************) + +lemma lfpc_refl: ∀L. ⦃L⦄ ⬌ ⦃L⦄. +/2 width=1/ qed. + +lemma lfpc_sym: ∀L1,L2. ⦃L1⦄ ⬌ ⦃L2⦄ → ⦃L2⦄ ⬌ ⦃L1⦄. +#L1 #L2 * /2 width=1/ +qed. + +lemma lfpc_lfpr: ∀L1,L2. ⦃L1⦄ ⬌ ⦃L2⦄ → ∃∃L. ⦃L1⦄ ➡ ⦃L⦄ & ⦃L2⦄ ➡ ⦃L⦄. +#L1 #L2 * /2 width=3/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpc_lfpc.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpc_lfpc.etc new file mode 100644 index 000000000..69e444adb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpc_lfpc.etc @@ -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/lfpc.ma". + +(* FOCALIZED PARALLEL CONVERSION ON LOCAL ENVIRONMENTS **********************) + +(* Main properties **********************************************************) + +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/lambdadelta/basic_2/etc/lpc/lfpcs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs.etc new file mode 100644 index 000000000..5ad9180ac --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs.etc @@ -0,0 +1,72 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +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: reflexive … lfpcs. +/2 width=1/ qed. + +lemma lfpcs_sym: symmetric … lfpcs. +/3 width=1/ qed. + +lemma lfpc_lfpcs: ∀L1,L2. ⦃L1⦄ ⬌ ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +/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. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs_aaa.etc new file mode 100644 index 000000000..b7cea0b7a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs_aaa.etc @@ -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/lambdadelta/basic_2/etc/lpc/lfpcs_fpcs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs_fpcs.etc new file mode 100644 index 000000000..8f3688890 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs_fpcs.etc @@ -0,0 +1,52 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/computation/fprs_cprs.ma". +include "basic_2/computation/lfprs_fprs.ma". +include "basic_2/equivalence/fpcs_fpcs.ma". +include "basic_2/equivalence/lfpcs_lfpcs.ma". + +(* FOCALIZED PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *********************) + +(* Inversion lemmas on context-free parallel equivalence for closures *******) + +lemma lfpcs_inv_fpcs: ∀L1,L2. ⦃L1⦄ ⬌* ⦃L2⦄ → ∀T. ⦃L1, T⦄ ⬌* ⦃L2, T⦄. +#L1 #L2 #HL12 #T +elim (lfpcs_inv_lfprs … HL12) -HL12 #L #HL1 #HL2 +lapply (lfprs_inv_fprs … HL1 T) -HL1 +lapply (lfprs_inv_fprs … HL2 T) -HL2 /2 width=4/ +qed-. + +(* Properties on context-free parallel equivalence for closures *************) + +lemma fpcs_lfpcs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +#L1 #L2 #T1 #T2 #HT12 +elim (fpcs_inv_fprs … HT12) -HT12 /3 width=5 by fprs_lfprs, lfprs_div/ (**) (* auto too slow without trace *) +qed. + +lemma fpcs_lift: ∀K1,K2,T1,T2. ⦃K1, T1⦄ ⬌* ⦃K2, T2⦄ → + ∀L1,L2. ⦃L1⦄ ⬌* ⦃L2⦄ → + ∀d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 → + ∀U1,U2. ⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 → + ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄. +#K1 #K2 #T1 #T2 #HT12 #L1 #L2 #HL12 #d #e #HLK1 #HLK2 #U1 #U2 #HTU1 #HTU2 +elim (fpcs_inv_fprs … HT12) -HT12 #K #T #HT1 #HT2 +elim (lift_total T d e) #U #HTU +elim (fprs_lift … HT1 … HLK1 … HTU1 HTU) -K1 -T1 #K1 #HU1 #_ +elim (fprs_lift … HT2 … HLK2 … HTU2 HTU) -K2 -T2 -T #K2 #HU2 #_ -K -d -e +lapply (lfpcs_lfprs_conf K1 … HL12) -HL12 /2 width=3/ #H +lapply (lfpcs_lfprs_strap1 … H K2 ?) -H /2 width=3/ #HK12 +lapply (lfpcs_inv_fpcs … HK12 U) -HK12 #HU +/3 width=4 by fpcs_fprs_strap2, fpcs_fprs_div/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs_lfpcs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs_lfpcs.etc new file mode 100644 index 000000000..1e9521736 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs_lfpcs.etc @@ -0,0 +1,50 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/computation/lfprs_lfprs.ma". +include "basic_2/conversion/lfpc_lfpc.ma". +include "basic_2/equivalence/lfpcs_lfprs.ma". + +(* FOCALIZED PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *********************) + +(* Advanced inversion lemmas ************************************************) + +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 (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 lfpcs_strip: ∀L,L1. ⦃L⦄ ⬌* ⦃L1⦄ → ∀L2. ⦃L⦄ ⬌ ⦃L2⦄ → + ∃∃L0. ⦃L1⦄ ⬌ ⦃L0⦄ & ⦃L2⦄ ⬌* ⦃L0⦄. +/3 width=3/ qed. + +(* Main properties **********************************************************) + +theorem lfpcs_trans: ∀L1,L. ⦃L1⦄ ⬌* ⦃L⦄ → ∀L2. ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +/2 width=3/ qed. + +theorem lfpcs_canc_sn: ∀L,L1,L2. ⦃L⦄ ⬌* ⦃L1⦄ → ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +/3 width=3 by lfpcs_trans, lfpcs_sym/ qed. + +theorem lfpcs_canc_dx: ∀L,L1,L2. ⦃L1⦄ ⬌* ⦃L⦄ → ⦃L2⦄ ⬌* ⦃L⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. +/3 width=3 by lfpcs_trans, lfpcs_sym/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs_lfprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs_lfprs.etc new file mode 100644 index 000000000..baf2caf27 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpcs_lfprs.etc @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/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/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 21fd5fcca..9a4a98b86 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -51,28 +51,18 @@ table { ] class "blue" [ { "equivalence" * } { - [ { "focalized equivalence" * } { - [ "lfpcs ( ⦃?⦄ ⬌* ⦃?⦄ )" "lfpcs_aaa" + "lfpcs_fpcs" + "lfpcs_lfprs" + "lfpcs_lfpcs" * ] - [ "fpcs ( ⦃?,?⦄ ⬌* ⦃?,?⦄ )" "fpcs_aaa" + "fpcs_cpcs" + "fpcs_fprs" + "fpcs_fpcs" * ] - } - ] [ { "local env. ref. for stratified static type assignment" * } { [ "lsubss ( ? •⊑[?] ? )" "lsubss_ldrop" + "lsubss_ssta" + "lsubss_cpcs" * ] } ] [ { "context-sensitive equivalence" * } { - [ "cpcs ( ? ⊢ ? ⬌* ? )" "cpcs_ltpss_dx" + "cpcs_ltpss_sn" + "cpcs_delift" + "cpcs_aaa" + "cpcs_ltpr" + "cpcs_cprs" + "cpcs_cpcs" * ] + [ "cpcs ( ? ⊢ ? ⬌* ? )" "cpcs_lpss" + "cpcs_aaa" + "cpcs_cprs" + "cpcs_cpcs" * ] } ] } ] class "sky" [ { "conversion" * } { - [ { "focalized conversion" * } { - [ "lfpc ( ⦃?⦄ ⬌ ⦃?⦄ )" "lfpc_lfpc" * ] - [ "fpc ( ⦃?,?⦄ ⬌ ⦃?,?⦄ )" "fpc_fpc" * ] - } - ] [ { "context-sensitive conversion" * } { [ "cpc ( ? ⊢ ? ⬌ ? )" "cpc_cpc" * ] }