From: Ferruccio Guidi Date: Fri, 17 Nov 2017 16:26:22 +0000 (+0000) Subject: - dependences on ceq and ceq_ext fixed X-Git-Tag: make_still_working~403 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=e6282b0c066eee7329560e1929150776ca64aa4a - dependences on ceq and ceq_ext fixed - lfeq (was lleq) reintroduced - some renaming --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lfeq.ma index 8f247592c..53782a58d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lfeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lfeq.ma @@ -12,29 +12,13 @@ (* *) (**************************************************************************) -(* include "basic_2/static/lfeq.ma". -*) include "basic_2/static/lfxs_lfxs.ma". include "basic_2/i_static/tc_lfxs_fqup.ma". -include "basic_2/notation/relations/lazyeqsn_3.ma". - -definition ceq_ext: relation3 lenv bind bind ≝ - cext2 (λL,T1,T2. T1 = T2). - -definition lfeq: relation3 term lenv lenv ≝ - lfxs (λL,T1,T2. T1 = T2). - -interpretation - "syntactic equivalence on referred entries (local environment)" - 'LazyEqSn T L1 L2 = (lfeq T L1 L2). - -axiom lfeq_lfxs_trans: ∀R,L1,L,T. L1 ≡[T] L → - ∀L2. L ⪤*[R, T] L2 → L1 ⪤*[R, T] L2. - -axiom cext2_inv_LTC: ∀R,L,I1,I2. cext2 (LTC … R) L I1 I2 → LTC … (cext2 R) L I1 I2. (* +axiom cext2_inv_LTC: ∀R,L,I1,I2. cext2 (LTC … R) L I1 I2 → LTC … (cext2 R) L I1 I2. + #R #L #I1 #I2 * -I1 -I2 [ /2 width=1 by ext2_unit, inj/ | #I #V1 #V2 #HV12 @@ -51,9 +35,10 @@ lemma pippo: ∀RN,RP. (∀L. reflexive … (RP L)) → [ @step [3: *) +(* axiom lexs_frees_confluent_LTC_sn: ∀RN,RP. lexs_frees_confluent RN RP → lexs_frees_confluent (LTC … RN) RP. -(* + #RN #RP #HR #f1 #L1 #T #Hf1 #L2 #H *) (* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_cext2.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_cext2.ma new file mode 100644 index 000000000..f2a857d64 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_cext2.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/relocation/drops.ma". + +(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************) + +(* Properties with the extension to binders of a context-sensitive relation *) + +lemma cext2_d_liftable2_sn: ∀R. d_liftable2_sn … lifts R → + d_liftable2_sn … liftsb (cext2 R). +#R #HR #K #I1 #I2 * -I1 -I2 #I [| #T1 #T2 #HT12 ] +#b #f #L #HLK #Z1 #H +[ lapply (liftsb_inv_unit_sn … H) +| lapply (liftsb_inv_pair_sn … H) * #U1 #HTU1 +] -H #H destruct /3 width=3 by ext2_unit, ex2_intro/ +elim (HR … HT12 … HLK … HTU1) -HR -b -K -T1 /3 width=3 by ext2_pair, ex2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ext2.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ext2.ma deleted file mode 100644 index 58e535867..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ext2.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/syntax/lenv_ext2.ma". -include "basic_2/relocation/drops.ma". - -(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************) - -(* Properties with the extension to binders of a context-sensitive relation *) - -lemma cext2_d_liftable2_sn: ∀R. d_liftable2_sn … lifts R → - d_liftable2_sn … liftsb (cext2 R). -#R #HR #K #I1 #I2 * -I1 -I2 #I [| #T1 #T2 #HT12 ] -#b #f #L #HLK #Z1 #H -[ lapply (liftsb_inv_unit_sn … H) -| lapply (liftsb_inv_pair_sn … H) * #U1 #HTU1 -] -H #H destruct /3 width=3 by ext2_unit, ex2_intro/ -elim (HR … HT12 … HLK … HTU1) -HR -b -K -T1 /3 width=3 by ext2_pair, ex2_intro/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma index 1442fa552..cc3e75b0a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/lazyeqsn_3.ma". -include "basic_2/syntax/lenv_ceq.ma". +include "basic_2/syntax/ceq_ext.ma". include "basic_2/relocation/lexs.ma". (* RANGED EQUIVALENCE FOR LOCAL ENVIRONMENTS ********************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_ext.ma index 434efb137..b47bfc3e9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_ext.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_ext.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/syntax/lenv_ext2.ma". +include "basic_2/syntax/cext2.ma". include "basic_2/rt_transition/cpm.ma". (* CONTEXT-SENSITIVE PARALLEL R-TRANSITION FOR BINDERS **********************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_ext.ma index e250ab490..16e73c92b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_ext.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_ext.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/syntax/lenv_ext2.ma". +include "basic_2/syntax/cext2.ma". include "basic_2/rt_transition/cpx.ma". (* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR BINDERS ***********) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma index 8a770328f..df8af706d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma @@ -195,11 +195,3 @@ lemma lfdeq_fwd_flat_dx: ∀h,o,I,L1,L2,V,T. L1 ≛[h, o, ⓕ{I}V.T] L2 → L1 lemma lfdeq_fwd_dx: ∀h,o,I2,L1,K2. ∀T:term. L1 ≛[h, o, T] K2.ⓘ{I2} → ∃∃I1,K1. L1 = K1.ⓘ{I1}. /2 width=5 by lfxs_fwd_dx/ qed-. - -(* Basic_2A1: removed theorems 10: - lleq_ind lleq_fwd_lref - lleq_fwd_drop_sn lleq_fwd_drop_dx - lleq_skip lleq_lref lleq_free - lleq_Y lleq_ge_up lleq_ge - -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma new file mode 100644 index 000000000..cc3fce365 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma @@ -0,0 +1,39 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/lazyeqsn_3.ma". +include "basic_2/static/lfxs.ma". + +(* SYNTACTIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *********) + +(* Basic_2A1: was: lleq *) +definition lfeq: relation3 term lenv lenv ≝ + lfxs ceq. + +interpretation + "syntactic equivalence on referred entries (local environment)" + 'LazyEqSn T L1 L2 = (lfeq T L1 L2). + +(***************************************************) + +axiom lfeq_lfxs_trans: ∀R,L1,L,T. L1 ≡[T] L → + ∀L2. L ⪤*[R, T] L2 → L1 ⪤*[R, T] L2. + +(* Basic_2A1: removed theorems 10: + lleq_ind lleq_fwd_lref + lleq_fwd_drop_sn lleq_fwd_drop_dx + lleq_skip lleq_lref lleq_free + lleq_Y lleq_ge_up lleq_ge + +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma index 8fddc5896..9c0cc9c4a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma @@ -14,7 +14,7 @@ include "ground_2/relocation/rtmap_id.ma". include "basic_2/notation/relations/relationstar_4.ma". -include "basic_2/syntax/lenv_ext2.ma". +include "basic_2/syntax/cext2.ma". include "basic_2/relocation/lexs.ma". include "basic_2/static/frees.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma index 0eec7d41e..99b1ece94 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) +include "basic_2/relocation/drops_cext2.ma". include "basic_2/relocation/drops_lexs.ma". -include "basic_2/relocation/drops_ext2.ma". include "basic_2/static/frees_drops.ma". include "basic_2/static/lfxs.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/ceq_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/ceq_ext.ma new file mode 100644 index 000000000..f89840135 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/ceq_ext.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/syntax/cext2.ma". + +(* CONTEXT-AWARE SYNTACTIC EQUIVALENCE FOR BINDERS **************************) + +definition ceq_ext: lenv → relation bind ≝ + cext2 ceq. + +(* Basic properties *********************************************************) + +lemma ceq_ext_refl (L): reflexive … (ceq_ext L). +/2 width=1 by ext2_refl/ qed. + +(* Basic inversion lemmas ***************************************************) + +lemma ceq_ext_inv_eq: ∀L,I1,I2. ceq_ext L I1 I2 → I1 = I2. +#L #I1 #I2 * -I1 -I2 // +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/ceq_ext_ceq_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/ceq_ext_ceq_ext.ma index 440bddba4..2ab3768a0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/ceq_ext_ceq_ext.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/ceq_ext_ceq_ext.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "basic_2/syntax/lenv_ceq.ma". +include "basic_2/syntax/ceq_ext.ma". -(* CONTEXT-DEPENDENT SYNTACTIC EQUIVALENCE FOR BINDERS **********************) +(* CONTEXT-AWARE SYNTACTIC EQUIVALENCE FOR BINDERS **************************) (* Main properties **********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/cext2.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/cext2.ma new file mode 100644 index 000000000..6595ba704 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/cext2.ma @@ -0,0 +1,33 @@ +(**************************************************************************) +(* ___ *) +(* ||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/syntax/ext2.ma". +include "basic_2/syntax/lenv.ma". + +(* EXTENSION TO BINDERS OF A CONTEXT-SENSITIVE RELATION FOR TERMS ***********) + +definition cext2: (lenv → relation term) → lenv → relation bind ≝ + λR,L. ext2 (R L). + +(* Basic properties *********************************************************) + +lemma cext2_sym: ∀R. (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) → + ∀L1,L2,I1,I2. cext2 R L1 I1 I2 → cext2 R L2 I2 I1. +#R #HR #L1 #L2 #I1 #I2 * /3 width=2 by ext2_pair/ +qed-. + +lemma cext2_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) → + ∀L,I1,I2. cext2 R1 L I1 I2 → cext2 R2 L I1 I2. +#R1 #R2 #HR #L #I1 #I2 * /3 width=2 by ext2_unit, ext2_pair/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_ceq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_ceq.ma deleted file mode 100644 index 8ae1e8148..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_ceq.ma +++ /dev/null @@ -1,31 +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/syntax/lenv_ext2.ma". - -(* EXTENSION TO BINDERS OF A CONTEXT-SENSITIVE RELATION FOR TERMS ***********) - -definition ceq_ext: lenv → relation bind ≝ - cext2 ceq. - -(* Basic properties *********************************************************) - -lemma ceq_ext_refl (L): reflexive … (ceq_ext L). -/2 width=1 by ext2_refl/ qed. - -(* Basic inversion lemmas ***************************************************) - -lemma ceq_ext_inv_eq: ∀L,I1,I2. ceq_ext L I1 I2 → I1 = I2. -#L #I1 #I2 * -I1 -I2 // -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_ext2.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_ext2.ma deleted file mode 100644 index 6595ba704..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_ext2.ma +++ /dev/null @@ -1,33 +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/syntax/ext2.ma". -include "basic_2/syntax/lenv.ma". - -(* EXTENSION TO BINDERS OF A CONTEXT-SENSITIVE RELATION FOR TERMS ***********) - -definition cext2: (lenv → relation term) → lenv → relation bind ≝ - λR,L. ext2 (R L). - -(* Basic properties *********************************************************) - -lemma cext2_sym: ∀R. (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) → - ∀L1,L2,I1,I2. cext2 R L1 I1 I2 → cext2 R L2 I2 I1. -#R #HR #L1 #L2 #I1 #I2 * /3 width=2 by ext2_pair/ -qed-. - -lemma cext2_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) → - ∀L,I1,I2. cext2 R1 L I1 I2 → cext2 R2 L I1 I2. -#R1 #R2 #HR #L #I1 #I2 * /3 width=2 by ext2_unit, ext2_pair/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_ext.ma index 7cfeee246..93a3be18d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_ext.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_ext.ma @@ -13,8 +13,8 @@ (**************************************************************************) include "basic_2/notation/relations/stareq_5.ma". +include "basic_2/syntax/cext2.ma". include "basic_2/syntax/tdeq.ma". -include "basic_2/syntax/lenv_ext2.ma". (* EXTENDED DEGREE-BASED EQUIVALENCE ****************************************) 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 d960b5859..7d4282e13 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 @@ -170,6 +170,9 @@ table { [ "lfdeq ( ? ≛[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfdeq" * ] } ] + [ { "syntactic equivalence on referred entries" * } { + [ "lfeq ( ? ≡[?] ? )" * ] + } [ { "generic extension on referred entries" * } { [ "lfxs ( ? ⦻*[?,?] ? )" "lfxs_length" + "lfxs_drops" + "lfxs_fqup" + "lfxs_lfxs" * ] } @@ -207,7 +210,7 @@ table { [ { "relocation" * } { [ { "generic slicing for local environments" * } { [ "drops_vector ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" * ] - [ "drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" "drops_lstar" + "drops_weight" + "drops_length" + "drops_ext2" + "drops_lexs" + "drops_lreq" + "drops_drops" * ] + [ "drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" "drops_lstar" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_lexs" + "drops_lreq" + "drops_drops" * ] } ] [ { "generic relocation" * } { @@ -356,7 +359,7 @@ class "italic" { 1 } } ] [ { "pointwise extension of a relation" * } { - [ "lpx_sn" "lpx_sn_alt" + "lpx_sn_tc" + "lpx_sn_drop" + "lpx_sn_lpx_sn" * ] + [ "lpx_sn" "lpx_sn_alt" + "lpx_sn_drop" + "lpx_sn_lpx_sn" * ] } ] [ "cpx_lreq" + "cpr_cir" + "fpb_lift" + "fpbq_lift" ]