From: Ferruccio Guidi Date: Sat, 9 Jun 2018 18:32:48 +0000 (+0200) Subject: update in basic_2 X-Git-Tag: make_still_working~308 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c903bdd93123e6fc2ad63a951024da80c9c28307;p=helm.git update in basic_2 + component rt_equivalence completed! --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/scpes/dpconvstar_8.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/scpes/dpconvstar_8.etc new file mode 100644 index 000000000..f0210a6b8 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/scpes/dpconvstar_8.etc @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 • * ⬌ * [ break term 46 h, break term 46 o, break term 46 n1, break term 46 n2 ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'DPConvStar $h $o $n1 $n2 $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/scpes/scpes.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/scpes/scpes.etc new file mode 100644 index 000000000..657763483 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/scpes/scpes.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/notation/relations/dpconvstar_8.ma". +include "basic_2/computation/scpds.ma". + +(* STRATIFIED DECOMPOSED PARALLEL EQUIVALENCE FOR TERMS *********************) + +definition scpes: ∀h. sd h → nat → nat → relation4 genv lenv term term ≝ + λh,o,d1,d2,G,L,T1,T2. + ∃∃T. ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d1] T & ⦃G, L⦄ ⊢ T2 •*➡*[h, o, d2] T. + +interpretation "stratified decomposed parallel equivalence (term)" + 'DPConvStar h o d1 d2 G L T1 T2 = (scpes h o d1 d2 G L T1 T2). + +(* Basic properties *********************************************************) + +lemma scpds_div: ∀h,o,G,L,T1,T2,T,d1,d2. + ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d1] T → ⦃G, L⦄ ⊢ T2 •*➡*[h, o, d2] T → + ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2. +/2 width=3 by ex2_intro/ qed. + +lemma scpes_sym: ∀h,o,G,L,T1,T2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2 → + ⦃G, L⦄ ⊢ T2 •*⬌*[h, o, d2, d1] T1. +#h #o #G #L #T1 #T2 #L1 #d2 * /2 width=3 by scpds_div/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/scpes/scpes_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/scpes/scpes_aaa.etc new file mode 100644 index 000000000..f42ebdbc9 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/scpes/scpes_aaa.etc @@ -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/computation/scpds_aaa.ma". +include "basic_2/equivalence/scpes.ma". + +(* DECOMPOSED EXTENDED PARALLEL EQUIVALENCE FOR TERMS ***********************) + +(* Main inversion lemmas about atomic arity assignment on terms *************) + +theorem scpes_aaa_mono: ∀h,o,G,L,T1,T2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2 → + ∀A1. ⦃G, L⦄ ⊢ T1 ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T2 ⁝ A2 → + A1 = A2. +#h #o #G #L #T1 #T2 #d1 #d2 * #T #HT1 #HT2 #A1 #HA1 #A2 #HA2 +lapply (scpds_aaa_conf … HA1 … HT1) -T1 #HA1 +lapply (scpds_aaa_conf … HA2 … HT2) -T2 #HA2 +lapply (aaa_mono … HA1 … HA2) -L -T // +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/scpes/scpes_cpcs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/scpes/scpes_cpcs.etc new file mode 100644 index 000000000..f8ef46db1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/scpes/scpes_cpcs.etc @@ -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/computation/scpds_scpds.ma". +include "basic_2/equivalence/cpcs_cpcs.ma". +include "basic_2/equivalence/scpes.ma". + +(* STRATIFIED DECOMPOSED PARALLEL EQUIVALENCE FOR TERMS *********************) + +(* Inversion lemmas on parallel equivalence for terms ***********************) + +lemma scpes_inv_lstas_eq: ∀h,o,G,L,T1,T2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2 → + ∀U1. ⦃G, L⦄ ⊢ T1 •*[h, d1] U1 → + ∀U2. ⦃G, L⦄ ⊢ T2 •*[h, d2] U2 → ⦃G, L⦄ ⊢ U1 ⬌* U2. +#h #o #G #L #T1 #T2 #d1 #d2 * #T #HT1 #HT2 #U1 #HTU1 #U2 #HTU2 +/3 width=8 by scpds_inv_lstas_eq, cprs_div/ +qed-. + +(* Properties on parallel equivalence for terms *****************************) + +lemma cpcs_scpes: ∀h,o,G,L,T1,d11. ⦃G, L⦄ ⊢ T1 ▪[h, o] d11 → + ∀U1,d12. d12 ≤ d11 → ⦃G, L⦄ ⊢ T1 •*[h, d12] U1 → + ∀T2,d21. ⦃G, L⦄ ⊢ T2 ▪[h, o] d21 → + ∀U2,d22. d22 ≤ d21 → ⦃G, L⦄ ⊢ T2 •*[h, d22] U2 → + ⦃G, L⦄ ⊢ U1 ⬌* U2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d12, d22] T2. +#h #o #G #L #T1 #d11 #HT1 #U1 #d12 #Hd121 #HTU1 #T2 #d21 #HT2 #U2 #d22 #Hd221 #HTU2 #HU12 +elim (cpcs_inv_cprs … HU12) -HU12 /3 width=6 by scpds_div, ex4_2_intro/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/scpes/scpes_scpes.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/scpes/scpes_scpes.etc new file mode 100644 index 000000000..24ea20ec0 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/scpes/scpes_scpes.etc @@ -0,0 +1,69 @@ +(**************************************************************************) +(* ___ *) +(* ||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/scpds_scpds.ma". +include "basic_2/equivalence/scpes.ma". + +(* STRATIFIED DECOMPOSED PARALLEL EQUIVALENCE FOR TERMS *********************) + +(* Advanced inversion lemmas ************************************************) + +lemma scpes_inv_abst2: ∀h,o,a,G,L,T1,T2,W2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] ⓛ{a}W2.T2 → + ∃∃W,T. ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d1] ⓛ{a}W.T & ⦃G, L⦄ ⊢ W2 ➡* W & + ⦃G, L.ⓛW2⦄ ⊢ T2 •*➡*[h, o, d2] T. +#h #o #a #G #L #T1 #T2 #W2 #d1 #d2 * #T0 #HT10 #H +elim (scpds_inv_abst1 … H) -H #W #T #HW2 #HT2 #H destruct /2 width=5 by ex3_2_intro/ +qed-. + +(* Advanced properties ******************************************************) + +lemma scpes_refl: ∀h,o,G,L,T,d1,d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ T ▪[h, o] d1 → + ⦃G, L⦄ ⊢ T •*⬌*[h, o, d2, d2] T. +#h #o #G #L #T #d1 #d2 #Hd21 #Hd1 +elim (da_lstas … Hd1 … d2) #U #HTU #_ +/3 width=3 by scpds_div, lstas_scpds/ +qed. + +lemma lstas_scpes_trans: ∀h,o,G,L,T1,d0,d1. ⦃G, L⦄ ⊢ T1 ▪[h, o] d0 → d1 ≤ d0 → + ∀T. ⦃G, L⦄ ⊢ T1 •*[h, d1] T → + ∀T2,d,d2. ⦃G, L⦄ ⊢ T •*⬌*[h,o,d,d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h,o,d1+d,d2] T2. +#h #o #G #L #T1 #d0 #d1 #Hd0 #Hd10 #T #HT1 #T2 #d #d2 * +/3 width=3 by scpds_div, lstas_scpds_trans/ qed-. + +(* Properties on parallel computation for terms *****************************) + +lemma cprs_scpds_div: ∀h,o,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡* T → + ∀d. ⦃G, L⦄ ⊢ T1 ▪[h, o] d → + ∀T2,d2. ⦃G, L⦄ ⊢ T2 •*➡*[h, o, d2] T → + ⦃G, L⦄⊢ T1 •*⬌*[h, o, 0, d2] T2. +#h #o #G #L #T1 #T #HT1 #d #Hd elim (da_lstas … Hd 0) +#X1 #HTX1 #_ elim (cprs_strip … HT1 X1) -HT1 +/3 width=5 by scpds_strap1, scpds_div, lstas_cpr, ex4_2_intro/ +qed. + +(* Main properties **********************************************************) + +theorem scpes_trans: ∀h,o,G,L,T1,T,d1,d. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d] T → + ∀T2,d2. ⦃G, L⦄ ⊢ T •*⬌*[h, o, d, d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2. +#h #o #G #L #T1 #T #d1 #d * #X1 #HT1X1 #HTX1 #T2 #d2 * #X2 #HTX2 #HT2X2 +elim (scpds_conf_eq … HTX1 … HTX2) -T -d /3 width=5 by scpds_cprs_trans, scpds_div/ +qed-. + +theorem scpes_canc_sn: ∀h,o,G,L,T,T1,d,d1. ⦃G, L⦄ ⊢ T •*⬌*[h, o, d, d1] T1 → + ∀T2,d2. ⦃G, L⦄ ⊢ T •*⬌*[h, o, d, d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2. +/3 width=4 by scpes_trans, scpes_sym/ qed-. + +theorem scpes_canc_dx: ∀h,o,G,L,T1,T,d1,d. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d] T → + ∀T2,d2. ⦃G, L⦄ ⊢ T2 •*⬌*[h, o, d2, d] T → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2. +/3 width=4 by scpes_trans, scpes_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpconvstar_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpconvstar_8.ma deleted file mode 100644 index f0210a6b8..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpconvstar_8.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 • * ⬌ * [ break term 46 h, break term 46 o, break term 46 n1, break term 46 n2 ] break term 46 T2 )" - non associative with precedence 45 - for @{ 'DPConvStar $h $o $n1 $n2 $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.ma index 8fc12c258..22d3b8ebf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.ma @@ -18,8 +18,8 @@ include "basic_2/rt_conversion/cpc.ma". (* CONTEXT-SENSITIVE PARALLEL R-EQUIVALENCE FOR TERMS ***********************) -definition cpcs: sh → relation4 genv lenv term term ≝ - λh,G. CTC … (cpc h G). +definition cpcs (h) (G): relation3 lenv term term ≝ + CTC … (cpc h G). interpretation "context-sensitive parallel r-equivalence (term)" 'PConvStar h G L T1 T2 = (cpcs h G L T1 T2). @@ -27,69 +27,77 @@ interpretation "context-sensitive parallel r-equivalence (term)" (* Basic eliminators ********************************************************) (* Basic_2A1: was: cpcs_ind_dx *) -lemma cpcs_ind_sn (h): ∀G,L,T2. ∀R:predicate term. R T2 → - (∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌[h] T → ⦃G, L⦄ ⊢ T ⬌*[h] T2 → R T → R T1) → - ∀T1. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → R T1. +lemma cpcs_ind_sn (h) (G) (L) (T2): + ∀R:predicate term. R T2 → + (∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌[h] T → ⦃G, L⦄ ⊢ T ⬌*[h] T2 → R T → R T1) → + ∀T1. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → R T1. normalize /3 width=6 by TC_star_ind_dx/ qed-. (* Basic_2A1: was: cpcs_ind *) -lemma cpcs_ind_dx (h): ∀G,L,T1. ∀R:predicate term. R T1 → - (∀T,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → ⦃G, L⦄ ⊢ T ⬌[h] T2 → R T → R T2) → - ∀T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → R T2. +lemma cpcs_ind_dx (h) (G) (L) (T1): + ∀R:predicate term. R T1 → + (∀T,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → ⦃G, L⦄ ⊢ T ⬌[h] T2 → R T → R T2) → + ∀T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → R T2. normalize /3 width=6 by TC_star_ind/ qed-. (* Basic properties *********************************************************) (* Basic_1: was: pc3_refl *) -lemma cpcs_refl (h): ∀G. c_reflexive … (cpcs h G). +lemma cpcs_refl (h) (G): c_reflexive … (cpcs h G). /2 width=1 by inj/ qed. (* Basic_1: was: pc3_s *) -lemma cpcs_sym (h): ∀G,L. symmetric … (cpcs h G L). +lemma cpcs_sym (h) (G) (L): symmetric … (cpcs h G L). #h #G #L @TC_symmetric /2 width=1 by cpc_sym/ qed-. -lemma cpc_cpcs (h): ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +lemma cpc_cpcs (h) (G) (L): ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬌[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. /2 width=1 by inj/ qed. (* Basic_2A1: was: cpcs_strap2 *) -lemma cpcs_step_sn (h): ∀G,L,T1,T,T2. ⦃G, L⦄ ⊢ T1 ⬌[h] T → ⦃G, L⦄ ⊢ T ⬌*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +lemma cpcs_step_sn (h) (G) (L): ∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌[h] T → + ∀T2. ⦃G, L⦄ ⊢ T ⬌*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. normalize /2 width=3 by TC_strap/ qed-. (* Basic_2A1: was: cpcs_strap1 *) -lemma cpcs_step_dx (h): ∀G,L,T1,T,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → ⦃G, L⦄ ⊢ T ⬌[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +lemma cpcs_step_dx (h) (G) (L): ∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → + ∀T2. ⦃G, L⦄ ⊢ T ⬌[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. normalize /2 width=3 by step/ qed-. (* Basic_1: was: pc3_pr2_r *) -lemma cpr_cpcs_dx (h): ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +lemma cpr_cpcs_dx (h) (G) (L): ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. /3 width=1 by cpc_cpcs, or_introl/ qed. (* Basic_1: was: pc3_pr2_x *) -lemma cpr_cpcs_sn (h): ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T2 ➡[h] T1 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +lemma cpr_cpcs_sn (h) (G) (L): ∀T1,T2. ⦃G, L⦄ ⊢ T2 ➡[h] T1 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. /3 width=1 by cpc_cpcs, or_intror/ qed. (* Basic_1: was: pc3_pr2_u *) (* Basic_2A1: was: cpcs_cpr_strap2 *) -lemma cpcs_cpr_step_sn (h): ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡[h] T → ∀T2. ⦃G, L⦄ ⊢ T ⬌*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +lemma cpcs_cpr_step_sn (h) (G) (L): ∀T1,T. ⦃G, L⦄ ⊢ T1 ➡[h] T → ∀T2. ⦃G, L⦄ ⊢ T ⬌*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. /3 width=3 by cpcs_step_sn, or_introl/ qed-. (* Basic_2A1: was: cpcs_cpr_strap1 *) -lemma cpcs_cpr_step_dx (h): ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +lemma cpcs_cpr_step_dx (h) (G) (L): ∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → + ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. /3 width=3 by cpcs_step_dx, or_introl/ qed-. -lemma cpcs_cpr_div (h): ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡[h] T → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +lemma cpcs_cpr_div (h) (G) (L): ∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → + ∀T2. ⦃G, L⦄ ⊢ T2 ➡[h] T → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. /3 width=3 by cpcs_step_dx, or_intror/ qed-. -lemma cpr_div (h): ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡[h] T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡[h] T → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +lemma cpr_div (h) (G) (L): ∀T1,T. ⦃G, L⦄ ⊢ T1 ➡[h] T → + ∀T2. ⦃G, L⦄ ⊢ T2 ➡[h] T → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. /3 width=3 by cpr_cpcs_dx, cpcs_step_dx, or_intror/ qed-. (* Basic_1: was: pc3_pr2_u2 *) -lemma cpcs_cpr_conf (h): ∀G,L,T1,T. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ⬌*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +lemma cpcs_cpr_conf (h) (G) (L): ∀T1,T. ⦃G, L⦄ ⊢ T ➡[h] T1 → + ∀T2. ⦃G, L⦄ ⊢ T ⬌*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. /3 width=3 by cpcs_step_sn, or_intror/ qed-. (* Basic_1: removed theorems 9: diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_aaa.ma index 4f9223886..a1361c2f0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_aaa.ma @@ -12,19 +12,19 @@ (* *) (**************************************************************************) -include "basic_2/computation/cpxs_aaa.ma". -include "basic_2/equivalence/cpcs_cpcs.ma". +include "basic_2/rt_computation/cpms_aaa.ma". +include "basic_2/rt_equivalence/cpcs_cprs.ma". (* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) -(* Main inversion lemmas about atomic arity assignment on terms *************) +(* Main inversion lemmas with atomic arity assignment on terms **************) -theorem cpcs_aaa_mono: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 → - ∀A1. ⦃G, L⦄ ⊢ T1 ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T2 ⁝ A2 → - A1 = A2. -#G #L #T1 #T2 #HT12 #A1 #HA1 #A2 #HA2 +theorem cpcs_aaa_mono (h) (G) (L): ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → + ∀A1. ⦃G, L⦄ ⊢ T1 ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T2 ⁝ A2 → + A1 = A2. +#h #G #L #T1 #T2 #HT12 #A1 #HA1 #A2 #HA2 elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2 -lapply (cprs_aaa_conf … HA1 … HT1) -T1 #HA1 -lapply (cprs_aaa_conf … HA2 … HT2) -T2 #HA2 +lapply (cpms_aaa_conf … HA1 … HT1) -T1 #HA1 +lapply (cpms_aaa_conf … HA2 … HT2) -T2 #HA2 lapply (aaa_mono … HA1 … HA2) -L -T // qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_cpc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_cpc.ma new file mode 100644 index 000000000..efccc2d4e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_cpc.ma @@ -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/rt_conversion/cpc_cpc.ma". +include "basic_2/rt_equivalence/cpcs.ma". + +(* CONTEXT-SENSITIVE PARALLEL R-EQUIVALENCE FOR TERMS ***********************) + +(* Properties with context-sensitive parallel r-conversion for terms ********) + +lemma cpcs_strip (h) (G) (L): confluent2 … (cpcs h G L) (cpc h G L). +#h #G #L #T1 #T @TC_strip1 /2 width=3 by cpc_conf/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_cpcs.ma index 7b9645afa..a29055eee 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_cpcs.ma @@ -12,201 +12,40 @@ (* *) (**************************************************************************) -include "basic_2/computation/lprs_cprs.ma". -include "basic_2/conversion/cpc_cpc.ma". -include "basic_2/equivalence/cpcs_cprs.ma". +include "basic_2/rt_equivalence/cpcs_lprs.ma". -(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) - -(* Advanced inversion lemmas ************************************************) - -lemma cpcs_inv_cprs: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 → - ∃∃T. ⦃G, L⦄ ⊢ T1 ➡* T & ⦃G, L⦄ ⊢ T2 ➡* T. -#G #L #T1 #T2 #H @(cpcs_ind … H) -T2 -[ /3 width=3 by ex2_intro/ -| #T #T2 #_ #HT2 * #T0 #HT10 elim HT2 -HT2 #HT2 #HT0 - [ elim (cprs_strip … HT0 … HT2) -T /3 width=3 by cprs_strap1, ex2_intro/ - | /3 width=5 by cprs_strap2, ex2_intro/ - ] -] -qed-. - -(* Basic_1: was: pc3_gen_sort *) -lemma cpcs_inv_sort: ∀G,L,s1,s2. ⦃G, L⦄ ⊢ ⋆s1 ⬌* ⋆s2 → s1 = s2. -#G #L #s1 #s2 #H elim (cpcs_inv_cprs … H) -H -#T #H1 >(cprs_inv_sort1 … H1) -T #H2 -lapply (cprs_inv_sort1 … H2) -L #H destruct // -qed-. - -lemma cpcs_inv_abst1: ∀a,G,L,W1,T1,T. ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ⬌* T → - ∃∃W2,T2. ⦃G, L⦄ ⊢ T ➡* ⓛ{a}W2.T2 & ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* ⓛ{a}W2.T2. -#a #G #L #W1 #T1 #T #H -elim (cpcs_inv_cprs … H) -H #X #H1 #H2 -elim (cprs_inv_abst1 … H1) -H1 #W2 #T2 #HW12 #HT12 #H destruct -/3 width=6 by cprs_bind, ex2_2_intro/ -qed-. - -lemma cpcs_inv_abst2: ∀a,G,L,W1,T1,T. ⦃G, L⦄ ⊢ T ⬌* ⓛ{a}W1.T1 → - ∃∃W2,T2. ⦃G, L⦄ ⊢ T ➡* ⓛ{a}W2.T2 & ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* ⓛ{a}W2.T2. -/3 width=1 by cpcs_inv_abst1, cpcs_sym/ qed-. - -(* Basic_1: was: pc3_gen_sort_abst *) -lemma cpcs_inv_sort_abst: ∀a,G,L,W,T,s. ⦃G, L⦄ ⊢ ⋆s ⬌* ⓛ{a}W.T → ⊥. -#a #G #L #W #T #s #H -elim (cpcs_inv_cprs … H) -H #X #H1 ->(cprs_inv_sort1 … H1) -X #H2 -elim (cprs_inv_abst1 … H2) -H2 #W0 #T0 #_ #_ #H destruct -qed-. - -(* Basic_1: was: pc3_gen_lift *) -lemma cpcs_inv_lift: ∀G,L,K,b,l,k. ⬇[b, l, k] L ≘ K → - ∀T1,U1. ⬆[l, k] T1 ≘ U1 → ∀T2,U2. ⬆[l, k] T2 ≘ U2 → - ⦃G, L⦄ ⊢ U1 ⬌* U2 → ⦃G, K⦄ ⊢ T1 ⬌* T2. -#G #L #K #b #l #k #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HU12 -elim (cpcs_inv_cprs … HU12) -HU12 #U #HU1 #HU2 -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 -l -k /2 width=3 by cprs_div/ -qed-. - -(* Advanced properties ******************************************************) - -lemma lpr_cpcs_trans: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → - ∀T1,T2. ⦃G, L2⦄ ⊢ T1 ⬌* T2 → ⦃G, L1⦄ ⊢ T1 ⬌* T2. -#G #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H -/4 width=5 by cprs_div, lpr_cprs_trans/ -qed-. - -lemma lprs_cpcs_trans: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → - ∀T1,T2. ⦃G, L2⦄ ⊢ T1 ⬌* T2 → ⦃G, L1⦄ ⊢ T1 ⬌* T2. -#G #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H -/4 width=5 by cprs_div, lprs_cprs_trans/ -qed-. - -lemma cpr_cprs_conf_cpcs: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ➡* T1 → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -#G #L #T #T1 #T2 #HT1 #HT2 elim (cprs_strip … HT1 … HT2) -HT1 -HT2 -/2 width=3 by cpr_cprs_div/ -qed-. - -lemma cprs_cpr_conf_cpcs: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ➡* T1 → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T2 ⬌* T1. -#G #L #T #T1 #T2 #HT1 #HT2 elim (cprs_strip … HT1 … HT2) -HT1 -HT2 -/2 width=3 by cprs_cpr_div/ -qed-. - -lemma cprs_conf_cpcs: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ➡* T1 → ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -#G #L #T #T1 #T2 #HT1 #HT2 elim (cprs_conf … HT1 … HT2) -HT1 -HT2 -/2 width=3 by cprs_div/ -qed-. - -lemma lprs_cprs_conf: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → - ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ⦃G, L2⦄ ⊢ T1 ⬌* T2. -#G #L1 #L2 #HL12 #T1 #T2 #HT12 elim (lprs_cprs_conf_dx … HT12 … HL12) -L1 -/2 width=3 by cprs_div/ -qed-. - -(* Basic_1: was: pc3_wcpr0_t *) -(* Basic_1: note: pc3_wcpr0_t should be renamed *) -(* Note: alternative proof /3 width=5 by lprs_cprs_conf, lpr_lprs/ *) -lemma lpr_cprs_conf: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → - ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ⦃G, L2⦄ ⊢ T1 ⬌* T2. -#G #L1 #L2 #HL12 #T1 #T2 #HT12 elim (cprs_lpr_conf_dx … HT12 … HL12) -L1 -/2 width=3 by cprs_div/ -qed-. - -(* Basic_1: was only: pc3_pr0_pr2_t *) -(* Basic_1: note: pc3_pr0_pr2_t should be renamed *) -lemma lpr_cpr_conf: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → - ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L2⦄ ⊢ T1 ⬌* T2. -/3 width=5 by lpr_cprs_conf, cpr_cprs/ qed-. - -(* Basic_1: was only: pc3_thin_dx *) -lemma cpcs_flat: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬌* V2 → ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 → - ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬌* ⓕ{I}V2.T2. -#G #L #V1 #V2 #HV12 #T1 #T2 #HT12 -elim (cpcs_inv_cprs … HV12) -HV12 -elim (cpcs_inv_cprs … HT12) -HT12 -/3 width=5 by cprs_flat, cprs_div/ -qed. - -lemma cpcs_flat_dx_cpr_rev: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V2 ➡ V1 → ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 → - ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬌* ⓕ{I}V2.T2. -/3 width=1 by cpr_cpcs_sn, cpcs_flat/ qed. - -lemma cpcs_bind_dx: ∀a,I,G,L,V,T1,T2. ⦃G, L.ⓑ{I}V⦄ ⊢ T1 ⬌* T2 → - ⦃G, L⦄ ⊢ ⓑ{a,I}V.T1 ⬌* ⓑ{a,I}V.T2. -#a #I #G #L #V #T1 #T2 #HT12 elim (cpcs_inv_cprs … HT12) -HT12 -/3 width=5 by cprs_div, cprs_bind/ -qed. - -lemma cpcs_bind_sn: ∀a,I,G,L,V1,V2,T. ⦃G, L⦄ ⊢ V1 ⬌* V2 → ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T ⬌* ⓑ{a,I}V2. T. -#a #I #G #L #V1 #V2 #T #HV12 elim (cpcs_inv_cprs … HV12) -HV12 -/3 width=5 by cprs_div, cprs_bind/ -qed. - -lemma lsubr_cpcs_trans: ∀G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ⬌* T2 → - ∀L2. L2 ⫃ L1 → ⦃G, L2⦄ ⊢ T1 ⬌* T2. -#G #L1 #T1 #T2 #HT12 elim (cpcs_inv_cprs … HT12) -HT12 -/3 width=5 by cprs_div, lsubr_cprs_trans/ -qed-. - -(* Basic_1: was: pc3_lift *) -lemma cpcs_lift: ∀G,L,K,b,l,k. ⬇[b, l, k] L ≘ K → - ∀T1,U1. ⬆[l, k] T1 ≘ U1 → ∀T2,U2. ⬆[l, k] T2 ≘ U2 → - ⦃G, K⦄ ⊢ T1 ⬌* T2 → ⦃G, L⦄ ⊢ U1 ⬌* U2. -#G #L #K #b #l #k #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HT12 -elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2 -elim (lift_total T l k) /3 width=12 by cprs_div, cprs_lift/ -qed. - -lemma cpcs_strip: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T ⬌* T1 → ∀T2. ⦃G, L⦄ ⊢ T ⬌ T2 → - ∃∃T0. ⦃G, L⦄ ⊢ T1 ⬌ T0 & ⦃G, L⦄ ⊢ T2 ⬌* T0. -#G #L #T1 #T @TC_strip1 /2 width=3 by cpc_conf/ qed-. - -(* More inversion lemmas ****************************************************) - -(* Note: there must be a proof suitable for llpr *) -lemma cpcs_inv_abst_sn: ∀a1,a2,G,L,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{a1}W1.T1 ⬌* ⓛ{a2}W2.T2 → - ∧∧ ⦃G, L⦄ ⊢ W1 ⬌* W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬌* T2 & a1 = a2. -#a1 #a2 #G #L #W1 #W2 #T1 #T2 #H -elim (cpcs_inv_cprs … H) -H #T #H1 #H2 -elim (cprs_inv_abst1 … H1) -H1 #W0 #T0 #HW10 #HT10 #H destruct -elim (cprs_inv_abst1 … H2) -H2 #W #T #HW2 #HT2 #H destruct -lapply (lprs_cprs_conf … (L.ⓛW) … HT2) /2 width=1 by lprs_pair/ -HT2 #HT2 -lapply (lprs_cpcs_trans … (L.ⓛW1) … HT2) /2 width=1 by lprs_pair/ -HT2 #HT2 -/4 width=3 by and3_intro, cprs_div, cpcs_cprs_div, cpcs_sym/ -qed-. - -lemma cpcs_inv_abst_dx: ∀a1,a2,G,L,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{a1}W1.T1 ⬌* ⓛ{a2}W2.T2 → - ∧∧ ⦃G, L⦄ ⊢ W1 ⬌* W2 & ⦃G, L.ⓛW2⦄ ⊢ T1 ⬌* T2 & a1 = a2. -#a1 #a2 #G #L #W1 #W2 #T1 #T2 #HT12 lapply (cpcs_sym … HT12) -HT12 -#HT12 elim (cpcs_inv_abst_sn … HT12) -HT12 /3 width=1 by cpcs_sym, and3_intro/ -qed-. +(* CONTEXT-SENSITIVE PARALLEL R-EQUIVALENCE FOR TERMS ***********************) (* Main properties **********************************************************) (* Basic_1: was pc3_t *) -theorem cpcs_trans: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌* T → ∀T2. ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -#G #L #T1 #T #HT1 #T2 @(trans_TC … HT1) qed-. +theorem cpcs_trans (h) (G) (L): Transitive … (cpcs h G L). +#h #G #L #T1 #T #HT1 #T2 @(trans_TC … HT1) +qed-. -theorem cpcs_canc_sn: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ⬌* T1 → ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. +theorem cpcs_canc_sn (h) (G) (L): left_cancellable … (cpcs h G L). /3 width=3 by cpcs_trans, cpcs_sym/ qed-. -theorem cpcs_canc_dx: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T → ⦃G, L⦄ ⊢ T2 ⬌* T → ⦃G, L⦄ ⊢ T1 ⬌* T2. +theorem cpcs_canc_dx (h) (G) (L): right_cancellable … (cpcs h G L). /3 width=3 by cpcs_trans, cpcs_sym/ qed-. -lemma cpcs_bind1: ∀a,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬌* V2 → - ∀T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬌* T2 → - ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T1 ⬌* ⓑ{a,I}V2. T2. +(* Advanced properties ******************************************************) + +lemma cpcs_bind1 (h) (G) (L): ∀V1,V2. ⦃G, L⦄ ⊢ V1 ⬌*[h] V2 → + ∀I,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬌*[h] T2 → + ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬌*[h] ⓑ{p,I}V2.T2. /3 width=3 by cpcs_trans, cpcs_bind_sn, cpcs_bind_dx/ qed. -lemma cpcs_bind2: ∀a,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬌* V2 → - ∀T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬌* T2 → - ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T1 ⬌* ⓑ{a,I}V2. T2. +lemma cpcs_bind2 (h) (G) (L): ∀V1,V2. ⦃G, L⦄ ⊢ V1 ⬌*[h] V2 → + ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬌*[h] T2 → + ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬌*[h] ⓑ{p,I}V2.T2. /3 width=3 by cpcs_trans, cpcs_bind_sn, cpcs_bind_dx/ qed. +(* Advanced properties with r-transition for full local environments ********) + (* Basic_1: was: pc3_wcpr0 *) -lemma lpr_cpcs_conf: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → - ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ⦃G, L2⦄ ⊢ T1 ⬌* T2. -#G #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H +lemma lpr_cpcs_conf (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ➡[h] L2 → + ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ⬌*[h] T2 → ⦃G, L2⦄ ⊢ T1 ⬌*[h] T2. +#h #G #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/rt_equivalence/cpcs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_cprs.ma index d9db0509f..5292a2665 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_cprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_cprs.ma @@ -12,51 +12,154 @@ (* *) (**************************************************************************) -include "basic_2/computation/cprs.ma". -include "basic_2/equivalence/cpcs.ma". +include "basic_2/rt_computation/cprs_cprs.ma". +include "basic_2/rt_computation/lprs_cpms.ma". +include "basic_2/rt_equivalence/cpcs.ma". -(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) +(* CONTEXT-SENSITIVE PARALLEL R-EQUIVALENCE FOR TERMS ***********************) -(* Properties about context sensitive computation on terms ******************) +(* Inversion lemmas with context sensitive r-computation on terms ***********) + +lemma cpcs_inv_cprs (h) (G) (L): ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → + ∃∃T. ⦃G, L⦄ ⊢ T1 ➡*[h] T & ⦃G, L⦄ ⊢ T2 ➡*[h] T. +#h #G #L #T1 #T2 #H @(cpcs_ind_dx … H) -T2 +[ /3 width=3 by ex2_intro/ +| #T #T2 #_ #HT2 * #T0 #HT10 elim HT2 -HT2 #HT2 #HT0 + [ elim (cprs_strip … HT0 … HT2) -T /3 width=3 by cprs_step_dx, ex2_intro/ + | /3 width=5 by cprs_step_sn, ex2_intro/ + ] +] +qed-. + +(* Advanced inversion lemmas ************************************************) + +(* Basic_1: was: pc3_gen_sort *) +(* Basic_2A1: was: cpcs_inv_sort *) +lemma cpcs_inv_sort_bi (h) (G) (L): ∀s1,s2. ⦃G, L⦄ ⊢ ⋆s1 ⬌*[h] ⋆s2 → s1 = s2. +#h #G #L #s1 #s2 #H elim (cpcs_inv_cprs … H) -H +#T #H1 >(cprs_inv_sort1 … H1) -T #H2 +lapply (cprs_inv_sort1 … H2) -L #H destruct // +qed-. + +(* Basic_2A1: was: cpcs_inv_abst1 *) +lemma cpcs_inv_abst_sn (h) (G) (L): + ∀p,W1,T1,X. ⦃G, L⦄ ⊢ ⓛ{p}W1.T1 ⬌*[h] X → + ∃∃W2,T2. ⦃G, L⦄ ⊢ X ➡*[h] ⓛ{p}W2.T2 & ⦃G, L⦄ ⊢ ⓛ{p}W1.T1 ➡*[h] ⓛ{p}W2.T2. +#h #G #L #p #W1 #T1 #T #H +elim (cpcs_inv_cprs … H) -H #X #H1 #H2 +elim (cpms_inv_abst_sn … H1) -H1 #W2 #T2 #HW12 #HT12 #H destruct +/3 width=6 by cpms_bind, ex2_2_intro/ +qed-. + +(* Basic_2A1: was: cpcs_inv_abst2 *) +lemma cpcs_inv_abst_dx (h) (G) (L): + ∀p,W1,T1,X. ⦃G, L⦄ ⊢ X ⬌*[h] ⓛ{p}W1.T1 → + ∃∃W2,T2. ⦃G, L⦄ ⊢ X ➡*[h] ⓛ{p}W2.T2 & ⦃G, L⦄ ⊢ ⓛ{p}W1.T1 ➡*[h] ⓛ{p}W2.T2. +/3 width=1 by cpcs_inv_abst_sn, cpcs_sym/ qed-. + +(* Basic_1: was: pc3_gen_sort_abst *) +lemma cpcs_inv_sort_abst (h) (G) (L): + ∀p,W,T,s. ⦃G, L⦄ ⊢ ⋆s ⬌*[h] ⓛ{p}W.T → ⊥. +#h #G #L #p #W #T #s #H +elim (cpcs_inv_cprs … H) -H #X #H1 +>(cprs_inv_sort1 … H1) -X #H2 +elim (cpms_inv_abst_sn … H2) -H2 #W0 #T0 #_ #_ #H destruct +qed-. + +(* Properties with context sensitive r-computation on terms *****************) (* Basic_1: was: pc3_pr3_r *) -lemma cpcs_cprs_dx: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -#G #L #T1 #T2 #H @(cprs_ind … H) -T2 -/3 width=3 by cpcs_cpr_strap1, cpcs_strap1, cpc_cpcs/ +lemma cpcs_cprs_dx (h) (G) (L): ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +#h #G #L #T1 #T2 #H @(cprs_ind_dx … H) -T2 +/3 width=3 by cpcs_cpr_step_dx, cpcs_step_dx, cpc_cpcs/ qed. (* Basic_1: was: pc3_pr3_x *) -lemma cpcs_cprs_sn: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T2 ➡* T1 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -#G #L #T1 #T2 #H @(cprs_ind_dx … H) -T2 -/3 width=3 by cpcs_cpr_div, cpcs_strap1, cpcs_cprs_dx/ +lemma cpcs_cprs_sn (h) (G) (L): ∀T1,T2. ⦃G, L⦄ ⊢ T2 ➡*[h] T1 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +#h #G #L #T1 #T2 #H @(cprs_ind_sn … H) -T2 +/3 width=3 by cpcs_cpr_div, cpcs_step_sn, cpcs_cprs_dx/ qed. -lemma cpcs_cprs_strap1: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌* T → ∀T2. ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -#G #L #T1 #T #HT1 #T2 #H @(cprs_ind … H) -T2 /2 width=3 by cpcs_cpr_strap1/ +(* Basic_2A1: was: cpcs_cprs_strap1 *) +lemma cpcs_cprs_step_dx (h) (G) (L): ∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → + ∀T2. ⦃G, L⦄ ⊢ T ➡*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +#h #G #L #T1 #T #HT1 #T2 #H @(cprs_ind_dx … H) -T2 /2 width=3 by cpcs_cpr_step_dx/ qed-. -lemma cpcs_cprs_strap2: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡* T → ∀T2. ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -#G #L #T1 #T #H #T2 #HT2 @(cprs_ind_dx … H) -T1 /2 width=3 by cpcs_cpr_strap2/ +(* Basic_2A1: was: cpcs_cprs_strap2 *) +lemma cpcs_cprs_step_sn (h) (G) (L): ∀T1,T. ⦃G, L⦄ ⊢ T1 ➡*[h] T → + ∀T2. ⦃G, L⦄ ⊢ T ⬌*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +#h #G #L #T1 #T #H #T2 #HT2 @(cprs_ind_sn … H) -T1 /2 width=3 by cpcs_cpr_step_sn/ qed-. -lemma cpcs_cprs_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌* T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡* T → ⦃G, L⦄ ⊢ T1 ⬌* T2. -#G #L #T1 #T #HT1 #T2 #H @(cprs_ind_dx … H) -T2 /2 width=3 by cpcs_cpr_div/ +lemma cpcs_cprs_div (h) (G) (L): ∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → + ∀T2. ⦃G, L⦄ ⊢ T2 ➡*[h] T → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +#h #G #L #T1 #T #HT1 #T2 #H @(cprs_ind_sn … H) -T2 /2 width=3 by cpcs_cpr_div/ qed-. (* Basic_1: was: pc3_pr3_conf *) -lemma cpcs_cprs_conf: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T ➡* T1 → ∀T2. ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -#G #L #T1 #T #H #T2 #HT2 @(cprs_ind … H) -T1 /2 width=3 by cpcs_cpr_conf/ +lemma cpcs_cprs_conf (h) (G) (L): ∀T1,T. ⦃G, L⦄ ⊢ T ➡*[h] T1 → + ∀T2. ⦃G, L⦄ ⊢ T ⬌*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +#h #G #L #T1 #T #H #T2 #HT2 @(cprs_ind_dx … H) -T1 /2 width=3 by cpcs_cpr_conf/ qed-. (* Basic_1: was: pc3_pr3_t *) (* Basic_1: note: pc3_pr3_t should be renamed *) -lemma cprs_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡* T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡* T → ⦃G, L⦄ ⊢ T1 ⬌* T2. -#G #L #T1 #T #HT1 #T2 #H @(cprs_ind_dx … H) -T2 +lemma cprs_div (h) (G) (L): ∀T1,T. ⦃G, L⦄ ⊢ T1 ➡*[h] T → + ∀T2. ⦃G, L⦄ ⊢ T2 ➡*[h] T → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +#h #G #L #T1 #T #HT1 #T2 #H @(cprs_ind_sn … H) -T2 /2 width=3 by cpcs_cpr_div, cpcs_cprs_dx/ qed. -lemma cprs_cpr_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡* T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡ T → ⦃G, L⦄ ⊢ T1 ⬌* T2. -/3 width=5 by cpr_cprs, cprs_div/ qed-. +lemma cprs_cpr_div (h) (G) (L): ∀T1,T. ⦃G, L⦄ ⊢ T1 ➡*[h] T → + ∀T2. ⦃G, L⦄ ⊢ T2 ➡[h] T → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +/3 width=5 by cpm_cpms, cprs_div/ qed-. + +lemma cpr_cprs_div (h) (G) (L): ∀T1,T. ⦃G, L⦄ ⊢ T1 ➡[h] T → + ∀T2. ⦃G, L⦄ ⊢ T2 ➡*[h] T → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +/3 width=3 by cpm_cpms, cprs_div/ qed-. + +lemma cpr_cprs_conf_cpcs (h) (G) (L): ∀T,T1. ⦃G, L⦄ ⊢ T ➡*[h] T1 → + ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +#h #G #L #T #T1 #HT1 #T2 #HT2 elim (cprs_strip … HT1 … HT2) -HT1 -HT2 +/2 width=3 by cpr_cprs_div/ +qed-. + +lemma cprs_cpr_conf_cpcs (h) (G) (L): ∀T,T1. ⦃G, L⦄ ⊢ T ➡*[h] T1 → + ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 → ⦃G, L⦄ ⊢ T2 ⬌*[h] T1. +#h #G #L #T #T1 #HT1 #T2 #HT2 elim (cprs_strip … HT1 … HT2) -HT1 -HT2 +/2 width=3 by cprs_cpr_div/ +qed-. + +lemma cprs_conf_cpcs (h) (G) (L): ∀T,T1. ⦃G, L⦄ ⊢ T ➡*[h] T1 → + ∀T2. ⦃G, L⦄ ⊢ T ➡*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +#h #G #L #T #T1 #HT1 #T2 #HT2 elim (cprs_conf … HT1 … HT2) -HT1 -HT2 +/2 width=3 by cprs_div/ +qed-. + +(* Basic_1: was only: pc3_thin_dx *) +lemma cpcs_flat (h) (G) (L): ∀V1,V2. ⦃G, L⦄ ⊢ V1 ⬌*[h] V2 → + ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → + ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬌*[h] ⓕ{I}V2.T2. +#h #G #L #V1 #V2 #HV12 #T1 #T2 #HT12 +elim (cpcs_inv_cprs … HV12) -HV12 +elim (cpcs_inv_cprs … HT12) -HT12 +/3 width=5 by cprs_flat, cprs_div/ +qed. + +lemma cpcs_flat_dx_cpr_rev (h) (G) (L): ∀V1,V2. ⦃G, L⦄ ⊢ V2 ➡[h] V1 → + ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → + ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬌*[h] ⓕ{I}V2.T2. +/3 width=1 by cpr_cpcs_sn, cpcs_flat/ qed. -lemma cpr_cprs_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡ T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡* T → ⦃G, L⦄ ⊢ T1 ⬌* T2. -/3 width=3 by cpr_cprs, cprs_div/ qed-. +lemma cpcs_bind_dx (h) (G) (L): ∀I,V,T1,T2. ⦃G, L.ⓑ{I}V⦄ ⊢ T1 ⬌*[h] T2 → + ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V.T1 ⬌*[h] ⓑ{p,I}V.T2. +#h #G #L #I #V #T1 #T2 #HT12 elim (cpcs_inv_cprs … HT12) -HT12 +/3 width=5 by cprs_div, cpms_bind/ +qed. + +lemma cpcs_bind_sn (h) (G) (L): ∀I,V1,V2,T. ⦃G, L⦄ ⊢ V1 ⬌*[h] V2 → + ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T ⬌*[h] ⓑ{p,I}V2.T. +#h #G #L #I #V1 #V2 #T #HV12 elim (cpcs_inv_cprs … HV12) -HV12 +/3 width=5 by cprs_div, cpms_bind/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_drops.ma new file mode 100644 index 000000000..12b24bb03 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_drops.ma @@ -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/rt_equivalence/cpcs_cprs.ma". + +(* CONTEXT-SENSITIVE PARALLEL R-EQUIVALENCE FOR TERMS ***********************) + +(* Properties with generic slicing for local environments *******************) + +(* Basic_1: was: pc3_lift *) +(* Basic_2A1: was: cpcs_lift *) +lemma cpcs_lifts_bi (h) (G): d_liftable2_bi … lifts (cpcs h G). +#h #G #K #T1 #T2 #HT12 #b #f #L #HLK #U1 #HTU1 #U2 #HTU2 +elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2 +elim (lifts_total T f) #U #HU +/3 width=12 by cprs_div, cpms_lifts_bi/ +qed-. + +(* Inversion lemmas with generic slicing for local environments *************) + +(* Basic_1: was: pc3_gen_lift *) +(* Basic_2A1: was cpcs_inv_lift *) +lemma cpcs_inv_lifts_bi (h) (G): d_deliftable2_bi … lifts (cpcs h G). +#h #G #L #U1 #U2 #HU12 #b #f #K #HLK #T1 #HTU1 #T2 #HTU2 +elim (cpcs_inv_cprs … HU12) -HU12 #U #HU1 #HU2 +elim (cpms_inv_lifts_sn … HU1 … HLK … HTU1) -U1 #T #HTU #HT1 +lapply (cpms_inv_lifts_bi … HU2 … HLK … HTU2 … HTU) -L -U -U2 -b -f #HT2 +/2 width=3 by cprs_div/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_lprs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_lprs.ma new file mode 100644 index 000000000..3564a480a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_lprs.ma @@ -0,0 +1,73 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rt_computation/lprs_cprs.ma". +include "basic_2/rt_equivalence/cpcs_cprs.ma". + +(* CONTEXT-SENSITIVE PARALLEL R-EQUIVALENCE FOR TERMS ***********************) + +(* Properties with parallel r-computation for full local environments *******) + +lemma lpr_cpcs_trans (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ➡[h] L2 → + ∀T1,T2. ⦃G, L2⦄ ⊢ T1 ⬌*[h] T2 → ⦃G, L1⦄ ⊢ T1 ⬌*[h] T2. +#h #G #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H + /4 width=5 by cprs_div, lpr_cpms_trans/ +qed-. + +lemma lprs_cpcs_trans (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h] L2 → + ∀T1,T2. ⦃G, L2⦄ ⊢ T1 ⬌*[h] T2 → ⦃G, L1⦄ ⊢ T1 ⬌*[h] T2. +#h #G #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H +/4 width=5 by cprs_div, lprs_cpms_trans/ +qed-. + +lemma lprs_cprs_conf (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h] L2 → + ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ➡*[h] T2 → ⦃G, L2⦄ ⊢ T1 ⬌*[h] T2. +#h #G #L1 #L2 #HL12 #T1 #T2 #HT12 elim (lprs_cprs_conf_dx … HT12 … HL12) -L1 +/2 width=3 by cprs_div/ +qed-. + +(* Basic_1: was: pc3_wcpr0_t *) +(* Basic_1: note: pc3_wcpr0_t should be renamed *) +(* Note: alternative proof /3 width=5 by lprs_cprs_conf, lpr_lprs/ *) +lemma lpr_cprs_conf (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ➡[h] L2 → + ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ➡*[h] T2 → ⦃G, L2⦄ ⊢ T1 ⬌*[h] T2. +#h #G #L1 #L2 #HL12 #T1 #T2 #HT12 elim (cprs_lpr_conf_dx … HT12 … HL12) -L1 +/2 width=3 by cprs_div/ +qed-. + +(* Basic_1: was only: pc3_pr0_pr2_t *) +(* Basic_1: note: pc3_pr0_pr2_t should be renamed *) +lemma lpr_cpr_conf (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ➡[h] L2 → + ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ➡[h] T2 → ⦃G, L2⦄ ⊢ T1 ⬌*[h] T2. +/3 width=5 by lpr_cprs_conf, cpm_cpms/ qed-. + +(* Advanced inversion lemmas ************************************************) + +(* Note: there must be a proof suitable for lfpr *) +lemma cpcs_inv_abst_sn (h) (G) (L): ∀p1,p2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{p1}W1.T1 ⬌*[h] ⓛ{p2}W2.T2 → + ∧∧ ⦃G, L⦄ ⊢ W1 ⬌*[h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬌*[h] T2 & p1 = p2. +#h #G #L #p1 #p2 #W1 #W2 #T1 #T2 #H +elim (cpcs_inv_cprs … H) -H #T #H1 #H2 +elim (cpms_inv_abst_sn … H1) -H1 #W0 #T0 #HW10 #HT10 #H destruct +elim (cpms_inv_abst_sn … H2) -H2 #W #T #HW2 #HT2 #H destruct +lapply (lprs_cprs_conf … (L.ⓛW) … HT2) /2 width=1 by lprs_pair/ -HT2 #HT2 +lapply (lprs_cpcs_trans … (L.ⓛW1) … HT2) /2 width=1 by lprs_pair/ -HT2 #HT2 +/4 width=3 by and3_intro, cprs_div, cpcs_cprs_div, cpcs_sym/ +qed-. + +lemma cpcs_inv_abst_dx (h) (G) (L): ∀p1,p2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{p1}W1.T1 ⬌*[h] ⓛ{p2}W2.T2 → + ∧∧ ⦃G, L⦄ ⊢ W1 ⬌*[h] W2 & ⦃G, L.ⓛW2⦄ ⊢ T1 ⬌*[h] T2 & p1 = p2. +#h #G #L #p1 #p2 #W1 #W2 #T1 #T2 #HT12 lapply (cpcs_sym … HT12) -HT12 +#HT12 elim (cpcs_inv_abst_sn … HT12) -HT12 /3 width=1 by cpcs_sym, and3_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_lsubr.ma new file mode 100644 index 000000000..e0d7fa473 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_lsubr.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_computation/cpms_lsubr.ma". +include "basic_2/rt_equivalence/cpcs_cprs.ma". + +(* CONTEXT-SENSITIVE PARALLEL R-EQUIVALENCE FOR TERMS ***********************) + +(* Properties with restricted refinement for local environments *************) + +lemma lsubr_cpcs_trans (h) (G): lsub_trans … (cpcs h G) lsubr. +#h #G #L1 #T1 #T2 #HT12 elim (cpcs_inv_cprs … HT12) -HT12 +/3 width=5 by cprs_div, lsubr_cpms_trans/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/partial.txt deleted file mode 100644 index 5072a8ac4..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/partial.txt +++ /dev/null @@ -1 +0,0 @@ -cpcs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes.ma deleted file mode 100644 index 657763483..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes.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/notation/relations/dpconvstar_8.ma". -include "basic_2/computation/scpds.ma". - -(* STRATIFIED DECOMPOSED PARALLEL EQUIVALENCE FOR TERMS *********************) - -definition scpes: ∀h. sd h → nat → nat → relation4 genv lenv term term ≝ - λh,o,d1,d2,G,L,T1,T2. - ∃∃T. ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d1] T & ⦃G, L⦄ ⊢ T2 •*➡*[h, o, d2] T. - -interpretation "stratified decomposed parallel equivalence (term)" - 'DPConvStar h o d1 d2 G L T1 T2 = (scpes h o d1 d2 G L T1 T2). - -(* Basic properties *********************************************************) - -lemma scpds_div: ∀h,o,G,L,T1,T2,T,d1,d2. - ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d1] T → ⦃G, L⦄ ⊢ T2 •*➡*[h, o, d2] T → - ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2. -/2 width=3 by ex2_intro/ qed. - -lemma scpes_sym: ∀h,o,G,L,T1,T2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2 → - ⦃G, L⦄ ⊢ T2 •*⬌*[h, o, d2, d1] T1. -#h #o #G #L #T1 #T2 #L1 #d2 * /2 width=3 by scpds_div/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes_aaa.ma deleted file mode 100644 index f42ebdbc9..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes_aaa.ma +++ /dev/null @@ -1,29 +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/scpds_aaa.ma". -include "basic_2/equivalence/scpes.ma". - -(* DECOMPOSED EXTENDED PARALLEL EQUIVALENCE FOR TERMS ***********************) - -(* Main inversion lemmas about atomic arity assignment on terms *************) - -theorem scpes_aaa_mono: ∀h,o,G,L,T1,T2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2 → - ∀A1. ⦃G, L⦄ ⊢ T1 ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T2 ⁝ A2 → - A1 = A2. -#h #o #G #L #T1 #T2 #d1 #d2 * #T #HT1 #HT2 #A1 #HA1 #A2 #HA2 -lapply (scpds_aaa_conf … HA1 … HT1) -T1 #HA1 -lapply (scpds_aaa_conf … HA2 … HT2) -T2 #HA2 -lapply (aaa_mono … HA1 … HA2) -L -T // -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes_cpcs.ma deleted file mode 100644 index f8ef46db1..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes_cpcs.ma +++ /dev/null @@ -1,39 +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/scpds_scpds.ma". -include "basic_2/equivalence/cpcs_cpcs.ma". -include "basic_2/equivalence/scpes.ma". - -(* STRATIFIED DECOMPOSED PARALLEL EQUIVALENCE FOR TERMS *********************) - -(* Inversion lemmas on parallel equivalence for terms ***********************) - -lemma scpes_inv_lstas_eq: ∀h,o,G,L,T1,T2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2 → - ∀U1. ⦃G, L⦄ ⊢ T1 •*[h, d1] U1 → - ∀U2. ⦃G, L⦄ ⊢ T2 •*[h, d2] U2 → ⦃G, L⦄ ⊢ U1 ⬌* U2. -#h #o #G #L #T1 #T2 #d1 #d2 * #T #HT1 #HT2 #U1 #HTU1 #U2 #HTU2 -/3 width=8 by scpds_inv_lstas_eq, cprs_div/ -qed-. - -(* Properties on parallel equivalence for terms *****************************) - -lemma cpcs_scpes: ∀h,o,G,L,T1,d11. ⦃G, L⦄ ⊢ T1 ▪[h, o] d11 → - ∀U1,d12. d12 ≤ d11 → ⦃G, L⦄ ⊢ T1 •*[h, d12] U1 → - ∀T2,d21. ⦃G, L⦄ ⊢ T2 ▪[h, o] d21 → - ∀U2,d22. d22 ≤ d21 → ⦃G, L⦄ ⊢ T2 •*[h, d22] U2 → - ⦃G, L⦄ ⊢ U1 ⬌* U2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d12, d22] T2. -#h #o #G #L #T1 #d11 #HT1 #U1 #d12 #Hd121 #HTU1 #T2 #d21 #HT2 #U2 #d22 #Hd221 #HTU2 #HU12 -elim (cpcs_inv_cprs … HU12) -HU12 /3 width=6 by scpds_div, ex4_2_intro/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes_scpes.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes_scpes.ma deleted file mode 100644 index 24ea20ec0..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes_scpes.ma +++ /dev/null @@ -1,69 +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/scpds_scpds.ma". -include "basic_2/equivalence/scpes.ma". - -(* STRATIFIED DECOMPOSED PARALLEL EQUIVALENCE FOR TERMS *********************) - -(* Advanced inversion lemmas ************************************************) - -lemma scpes_inv_abst2: ∀h,o,a,G,L,T1,T2,W2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] ⓛ{a}W2.T2 → - ∃∃W,T. ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d1] ⓛ{a}W.T & ⦃G, L⦄ ⊢ W2 ➡* W & - ⦃G, L.ⓛW2⦄ ⊢ T2 •*➡*[h, o, d2] T. -#h #o #a #G #L #T1 #T2 #W2 #d1 #d2 * #T0 #HT10 #H -elim (scpds_inv_abst1 … H) -H #W #T #HW2 #HT2 #H destruct /2 width=5 by ex3_2_intro/ -qed-. - -(* Advanced properties ******************************************************) - -lemma scpes_refl: ∀h,o,G,L,T,d1,d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ T ▪[h, o] d1 → - ⦃G, L⦄ ⊢ T •*⬌*[h, o, d2, d2] T. -#h #o #G #L #T #d1 #d2 #Hd21 #Hd1 -elim (da_lstas … Hd1 … d2) #U #HTU #_ -/3 width=3 by scpds_div, lstas_scpds/ -qed. - -lemma lstas_scpes_trans: ∀h,o,G,L,T1,d0,d1. ⦃G, L⦄ ⊢ T1 ▪[h, o] d0 → d1 ≤ d0 → - ∀T. ⦃G, L⦄ ⊢ T1 •*[h, d1] T → - ∀T2,d,d2. ⦃G, L⦄ ⊢ T •*⬌*[h,o,d,d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h,o,d1+d,d2] T2. -#h #o #G #L #T1 #d0 #d1 #Hd0 #Hd10 #T #HT1 #T2 #d #d2 * -/3 width=3 by scpds_div, lstas_scpds_trans/ qed-. - -(* Properties on parallel computation for terms *****************************) - -lemma cprs_scpds_div: ∀h,o,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡* T → - ∀d. ⦃G, L⦄ ⊢ T1 ▪[h, o] d → - ∀T2,d2. ⦃G, L⦄ ⊢ T2 •*➡*[h, o, d2] T → - ⦃G, L⦄⊢ T1 •*⬌*[h, o, 0, d2] T2. -#h #o #G #L #T1 #T #HT1 #d #Hd elim (da_lstas … Hd 0) -#X1 #HTX1 #_ elim (cprs_strip … HT1 X1) -HT1 -/3 width=5 by scpds_strap1, scpds_div, lstas_cpr, ex4_2_intro/ -qed. - -(* Main properties **********************************************************) - -theorem scpes_trans: ∀h,o,G,L,T1,T,d1,d. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d] T → - ∀T2,d2. ⦃G, L⦄ ⊢ T •*⬌*[h, o, d, d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2. -#h #o #G #L #T1 #T #d1 #d * #X1 #HT1X1 #HTX1 #T2 #d2 * #X2 #HTX2 #HT2X2 -elim (scpds_conf_eq … HTX1 … HTX2) -T -d /3 width=5 by scpds_cprs_trans, scpds_div/ -qed-. - -theorem scpes_canc_sn: ∀h,o,G,L,T,T1,d,d1. ⦃G, L⦄ ⊢ T •*⬌*[h, o, d, d1] T1 → - ∀T2,d2. ⦃G, L⦄ ⊢ T •*⬌*[h, o, d, d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2. -/3 width=4 by scpes_trans, scpes_sym/ qed-. - -theorem scpes_canc_dx: ∀h,o,G,L,T1,T,d1,d. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d] T → - ∀T2,d2. ⦃G, L⦄ ⊢ T2 •*⬌*[h, o, d2, d] T → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2. -/3 width=4 by scpes_trans, scpes_sym/ 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 b82479065..f3ce21a86 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 @@ -43,15 +43,9 @@ table { } ] class "prune" - [ { "rt-equivalence" * } { -(* - [ { "decomposed rt-equivalence" * } { - [ [ "" ] "scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "scpes_aaa" + "scpes_cpcs" + "scpes_scpes" * ] - } - ] -*) + [ { "rt-equivalence" * } { [ { "context-sensitive parallel r-equivalence" * } { - [ [ "for terms" ] "cpcs ( ⦃?,?⦄ ⊢ ? ⬌*[?] ? )" (* "cpcs_aaa" + "cpcs_cprs" + "cpcs_cpcs" *) * ] + [ [ "for terms" ] "cpcs ( ⦃?,?⦄ ⊢ ? ⬌*[?] ? )" "cpcs_drops" + "cpcs_lsubr" + "cpcs_aaa" + "cpcs_cprs" + "cpcs_lprs" + "cpcs_cpc" + "cpcs_cpcs" * ] } ] } @@ -66,12 +60,6 @@ table { ] class "sky" [ { "rt-computation" * } { -(* - [ { "decomposed rt-computation" * } { - "scpds_scpds" - } - ] -*) [ { "context-sensitive parallel r-computation" * } { [ [ "for lenvs on all entries" ] "lprs ( ⦃?,?⦄ ⊢ ➡*[?] ? )" "lprs_tc" + "lprs_ctc" + "lprs_length" + "lprs_drops" + "lprs_aaa" + "lprs_lpr" + "lprs_lpxs" + "lprs_cpms" + "lprs_cprs" + "lprs_lprs" * ] [ [ "for binders" ] "cprs_ext" + "( ⦃?,?⦄ ⊢ ? ➡*[?] ?)" * ] @@ -288,6 +276,10 @@ class "capitalize italic" { 0 1 } class "italic" { 2 } (* + [ { "decomposed rt-equivalence" * } { + [ [ "" ] "scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "scpes_aaa" + "scpes_cpcs" + "scpes_scpes" * ] + } + ] [ [ "for lenvs on referred entries" ] "lfpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_ffdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lpxs" + "lfpxs_lfpxs" * ] [ [ "for lenvs on referred entries" ] "lfpr" + "( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lfpr_length" + "lfpr_drops" + "lfpr_fquq" + "lfpr_fqup" + "lfpr_aaa" + "lfpr_lfpx" + "lfpr_lfpr" * ] diff --git a/matita/matita/contribs/lambdadelta/compile_partial.sh b/matita/matita/contribs/lambdadelta/compile_partial.sh index 4ed7b622d..d5789f4b8 100644 --- a/matita/matita/contribs/lambdadelta/compile_partial.sh +++ b/matita/matita/contribs/lambdadelta/compile_partial.sh @@ -1,6 +1,4 @@ ../../matitac.opt `cat partial.txt` -cd basic_2/rt_equivalence/ -../../../../matitac.opt `cat partial.txt` -cd ../dynamic/ +cd basic_2/dynamic/ ../../../../matitac.opt `cat partial.txt` cd ../../ diff --git a/matita/matita/contribs/lambdadelta/partial.txt b/matita/matita/contribs/lambdadelta/partial.txt index 12e10e1fe..40cb2929d 100644 --- a/matita/matita/contribs/lambdadelta/partial.txt +++ b/matita/matita/contribs/lambdadelta/partial.txt @@ -8,5 +8,6 @@ basic_2/i_static basic_2/rt_transition basic_2/rt_computation basic_2/rt_conversion +basic_2/rt_equivalence apps_2/examples/ex_cpr_omega.ma apps_2/models/