From e6282b0c066eee7329560e1929150776ca64aa4a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 17 Nov 2017 16:26:22 +0000 Subject: [PATCH] - dependences on ceq and ceq_ext fixed - lfeq (was lleq) reintroduced - some renaming --- .../basic_2/i_static/tc_lfxs_lfeq.ma | 23 ++--------- .../{drops_ext2.ma => drops_cext2.ma} | 1 - .../lambdadelta/basic_2/relocation/lreq.ma | 2 +- .../basic_2/rt_transition/cpr_ext.ma | 2 +- .../basic_2/rt_transition/cpx_ext.ma | 2 +- .../lambdadelta/basic_2/static/lfdeq.ma | 8 ---- .../lambdadelta/basic_2/static/lfeq.ma | 39 +++++++++++++++++++ .../lambdadelta/basic_2/static/lfxs.ma | 2 +- .../lambdadelta/basic_2/static/lfxs_drops.ma | 2 +- .../syntax/{lenv_ceq.ma => ceq_ext.ma} | 4 +- .../basic_2/syntax/ceq_ext_ceq_ext.ma | 4 +- .../basic_2/syntax/{lenv_ext2.ma => cext2.ma} | 0 .../lambdadelta/basic_2/syntax/tdeq_ext.ma | 2 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 7 +++- 14 files changed, 58 insertions(+), 40 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/relocation/{drops_ext2.ma => drops_cext2.ma} (97%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma rename matita/matita/contribs/lambdadelta/basic_2/syntax/{lenv_ceq.ma => ceq_ext.ma} (92%) rename matita/matita/contribs/lambdadelta/basic_2/syntax/{lenv_ext2.ma => cext2.ma} (100%) 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_ext2.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_cext2.ma similarity index 97% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ext2.ma rename to matita/matita/contribs/lambdadelta/basic_2/relocation/drops_cext2.ma index 58e535867..f2a857d64 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ext2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_cext2.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/syntax/lenv_ext2.ma". include "basic_2/relocation/drops.ma". (* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************) 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/lenv_ceq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/ceq_ext.ma similarity index 92% rename from matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_ceq.ma rename to matita/matita/contribs/lambdadelta/basic_2/syntax/ceq_ext.ma index 8ae1e8148..f89840135 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_ceq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/ceq_ext.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "basic_2/syntax/lenv_ext2.ma". +include "basic_2/syntax/cext2.ma". -(* EXTENSION TO BINDERS OF A CONTEXT-SENSITIVE RELATION FOR TERMS ***********) +(* CONTEXT-AWARE SYNTACTIC EQUIVALENCE FOR BINDERS **************************) definition ceq_ext: lenv → relation bind ≝ cext2 ceq. 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/lenv_ext2.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/cext2.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_ext2.ma rename to matita/matita/contribs/lambdadelta/basic_2/syntax/cext2.ma 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" ] -- 2.39.2