From bc27cc1925469ddcd2bc3cd4036a6ea8067c5da1 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 27 Sep 2020 14:01:04 +0200 Subject: [PATCH] update in basic_2 + improved definition of fsb + some parked files removed --- .../basic_2/etc/teqx/cpms_reqx.etc | 30 ---- .../lambdadelta/basic_2/etc/teqx/cpr_teqx.etc | 32 ---- .../lambdadelta/basic_2/etc/teqx/cpx_feqx.etc | 34 ---- .../lambdadelta/basic_2/etc/teqx/cpx_req.etc | 58 ------ .../lambdadelta/basic_2/etc/teqx/cpx_reqx.etc | 31 ---- .../basic_2/etc/teqx/cpxs_feqx.etc | 33 ---- .../basic_2/etc/teqx/cpxs_reqx.etc | 48 ----- .../basic_2/etc/teqx/cpxs_teqx.etc | 46 ----- .../lambdadelta/basic_2/etc/teqx/csx_feqx.etc | 27 --- .../lambdadelta/basic_2/etc/teqx/csx_reqx.etc | 36 ---- .../lambdadelta/basic_2/etc/teqx/fpb_feqx.etc | 48 ----- .../lambdadelta/basic_2/etc/teqx/fpb_reqx.etc | 52 ------ .../basic_2/etc/teqx/fpbq_feqx.etc | 27 --- .../lambdadelta/basic_2/etc/teqx/fsb_feqx.etc | 30 ---- .../lambdadelta/basic_2/etc/teqx/lpx_reqx.etc | 56 ------ .../basic_2/etc/teqx/lpxs_feqx.etc | 30 ---- .../basic_2/etc/teqx/lpxs_reqx.etc | 49 ------ .../lambdadelta/basic_2/rt_computation/fsb.ma | 20 ++- .../basic_2/rt_computation/fsb_csx.ma | 4 +- .../basic_2/rt_computation/fsb_feqg.ma | 2 +- .../basic_2/rt_computation/fsb_fpbg.ma | 4 +- .../lambdadelta/basic_2/web/basic_2.ldw.xml | 2 +- .../lambdadelta/ground/lib/relations.ma | 24 ++- .../static_2/etc/teqx/feqx_fqup.etc | 29 --- .../static_2/etc/teqx/feqx_fqus.etc | 32 ---- .../static_2/etc/teqx/feqx_req.etc | 27 --- .../lambdadelta/static_2/etc/teqx/req.etc | 117 ------------- .../static_2/etc/teqx/req_drops.etc | 26 --- .../static_2/etc/teqx/req_fqup.etc | 24 --- .../static_2/etc/teqx/req_length.etc | 36 ---- .../static_2/etc/teqx/reqx_drops.etc | 52 ------ .../static_2/etc/teqx/reqx_fqup.etc | 39 ----- .../static_2/etc/teqx/reqx_fqus.etc | 165 ------------------ .../static_2/etc/teqx/reqx_length.etc | 55 ------ .../lambdadelta/static_2/static/feqx.ma | 5 +- 35 files changed, 35 insertions(+), 1295 deletions(-) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpms_reqx.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpr_teqx.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpx_feqx.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpx_req.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpx_reqx.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpxs_feqx.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpxs_reqx.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpxs_teqx.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/teqx/csx_feqx.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/teqx/csx_reqx.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/teqx/fpb_feqx.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/teqx/fpb_reqx.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/teqx/fpbq_feqx.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/teqx/fsb_feqx.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/teqx/lpx_reqx.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/teqx/lpxs_feqx.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/teqx/lpxs_reqx.etc delete mode 100644 matita/matita/contribs/lambdadelta/static_2/etc/teqx/feqx_fqup.etc delete mode 100644 matita/matita/contribs/lambdadelta/static_2/etc/teqx/feqx_fqus.etc delete mode 100644 matita/matita/contribs/lambdadelta/static_2/etc/teqx/feqx_req.etc delete mode 100644 matita/matita/contribs/lambdadelta/static_2/etc/teqx/req.etc delete mode 100644 matita/matita/contribs/lambdadelta/static_2/etc/teqx/req_drops.etc delete mode 100644 matita/matita/contribs/lambdadelta/static_2/etc/teqx/req_fqup.etc delete mode 100644 matita/matita/contribs/lambdadelta/static_2/etc/teqx/req_length.etc delete mode 100644 matita/matita/contribs/lambdadelta/static_2/etc/teqx/reqx_drops.etc delete mode 100644 matita/matita/contribs/lambdadelta/static_2/etc/teqx/reqx_fqup.etc delete mode 100644 matita/matita/contribs/lambdadelta/static_2/etc/teqx/reqx_fqus.etc delete mode 100644 matita/matita/contribs/lambdadelta/static_2/etc/teqx/reqx_length.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpms_reqx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpms_reqx.etc deleted file mode 100644 index d7215295a..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpms_reqx.etc +++ /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/rt_computation/cpxs_reqx.ma". -include "basic_2/rt_computation/cpms_cpxs.ma". - -(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************) - -(* Properties with sort-irrelevant equivalence for local environments *******) - -lemma cpms_reqx_conf_sn (h) (n) (G) (L1) (L2): - ∀T1,T2. ❪G,L1❫ ⊢ T1 ➡*[h,n] T2 → - L1 ≛[T1] L2 → L1 ≛[T2] L2. -/3 width=5 by cpms_fwd_cpxs, cpxs_reqx_conf_sn/ qed-. - -lemma cpms_reqx_conf_dx (h) (n) (G) (L1) (L2): - ∀T1,T2. ❪G,L2❫ ⊢ T1 ➡*[h,n] T2 → - L1 ≛[T1] L2 → L1 ≛[T2] L2. -/3 width=5 by cpms_fwd_cpxs, cpxs_reqx_conf_dx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpr_teqx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpr_teqx.etc deleted file mode 100644 index 6c05df3d3..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpr_teqx.etc +++ /dev/null @@ -1,32 +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 "static_2/relocation/lifts_teqx.ma". -include "basic_2/rt_transition/cpr_drops_basic.ma". - -(* CONTEXT-SENSITIVE PARALLEL R-TRANSITION FOR TERMS ************************) - -(* Properties with context-free sort-irrelevant equivalence *****************) - -lemma cpr_abbr_pos_tneqx (h) (G) (L) (V) (T1): - ∃∃T2. ❪G,L❫ ⊢ +ⓓV.T1 ➡[h,0] T2 & (+ⓓV.T1 ≛ T2 → ⊥). -#h #G #L #V #U1 -elim (cpr_subst h G (L.ⓓV) U1 … 0) [|*: /2 width=4 by drops_refl/ ] #U2 #T2 #HU12 #HTU2 -elim (teqx_dec U1 U2) [ -HU12 #HU12 | -HTU2 #HnU12 ] -[ elim (teqx_inv_lifts_dx … HU12 … HTU2) -U2 #T1 #HTU1 #_ -T2 - /3 width=9 by cpm_zeta, teqx_lifts_inv_pair_sn, ex2_intro/ -| @(ex2_intro … (+ⓓV.U2)) [ /2 width=1 by cpm_bind/ ] -HU12 #H - elim (teqx_inv_pair … H) -H #_ #_ /2 width=1 by/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpx_feqx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpx_feqx.etc deleted file mode 100644 index 333a402d3..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpx_feqx.etc +++ /dev/null @@ -1,34 +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 "static_2/static/feqx.ma". -include "basic_2/rt_transition/cpx_reqx.ma". -include "basic_2/rt_transition/rpx_reqx.ma". - -(* EXTENDED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS **************) - -(* Properties with sort-irrelevant equivalence for closures *****************) - -(**) (* to update *) -lemma feqx_cpx_trans: - ∀G1,G2,L1,L2,T1,T. ❪G1,L1,T1❫ ≛ ❪G2,L2,T❫ → - ∀T2. ❪G2,L2❫ ⊢ T ⬈ T2 → - ∃∃T0. ❪G1,L1❫ ⊢ T1 ⬈ T0 & ❪G1,L1,T0❫ ≛ ❪G2,L2,T2❫. -#G1 #G2 #L1 #L2 #T1 #T #H #T2 #HT2 -elim (feqx_inv_gen_dx … H) -H #H #HL12 #HT1 destruct -lapply (reqx_cpx_trans … HL12 … HT2) #H -lapply (cpx_reqx_conf_dx … HT2 … HL12) -HT2 -HL12 #HL12 -lapply (teqx_cpx_trans … HT1 … H) -T #HT12 -/3 width=3 by feqx_intro_dx, ex2_intro/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpx_req.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpx_req.etc deleted file mode 100644 index a982ed783..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpx_req.etc +++ /dev/null @@ -1,58 +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 "static_2/static/req_length.ma". -include "static_2/static/req_drops.ma". -include "basic_2/rt_transition/rpx_fsle.ma". - -(* EXTENDED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS **************) - -(* Properties with syntactic equivalence for lenvs on referred entries ******) - -(* Basic_2A1: was: lleq_cpx_trans *) -lemma req_cpx_trans (G): R_transitive_req (cpx G). -#G #L2 #T1 #T2 #H @(cpx_ind … H) -G -L2 -T1 -T2 /2 width=2 by cpx_qu/ -[ #I #G #K2 #V1 #V2 #W2 #_ #IH #HVW2 #L1 #H - elim (req_inv_zero_pair_dx … H) -H #K1 #HK12 #H destruct - /3 width=3 by cpx_delta/ -| #I2 #G #K2 #T #U #i #_ #IH #HTU #L1 #H - elim (req_inv_lref_bind_dx … H) -H #I1 #K1 #HK12 #H destruct - /3 width=3 by cpx_lref/ -| #p #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H - elim (req_inv_bind … H) -H /3 width=1 by cpx_bind/ -| #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H - elim (req_inv_flat … H) -H /3 width=1 by cpx_flat/ -| #G #L2 #V2 #T1 #T #T2 #HT1 #_ #IH #L1 #H - elim (req_inv_bind … H) -H #HV2 #H - lapply (req_inv_lifts_bi … H (Ⓣ) … HT1) -H [6:|*: /3 width=2 by drops_refl, drops_drop/ ] #HT - /3 width=3 by cpx_zeta/ -| #G #L2 #W1 #T1 #T2 #_ #IH #L1 #H - elim (req_inv_flat … H) -H /3 width=1 by cpx_eps/ -| #G #L2 #W1 #W2 #T1 #_ #IH #L1 #H - elim (req_inv_flat … H) -H /3 width=1 by cpx_ee/ -| #p #G #L2 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #H - elim (req_inv_flat … H) -H #HV1 #H - elim (req_inv_bind … H) -H /3 width=1 by cpx_beta/ -| #p #G #L2 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV1 #IHW12 #IHT12 #HV2 #L1 #H - elim (req_inv_flat … H) -H #HV1 #H - elim (req_inv_bind … H) -H /3 width=3 by cpx_theta/ -] -qed-. - -lemma cpx_req_conf (G): R_confluent1_rex (cpx G) ceq. -/3 width=3 by req_cpx_trans, req_sym/ qed-. - -(* Basic_2A1: was: cpx_lleq_conf_sn *) -lemma cpx_req_conf_sn (G): s_r_confluent1 … (cpx G) req. -/2 width=5 by cpx_rex_conf_sn/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpx_reqx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpx_reqx.etc deleted file mode 100644 index 6c1aa906b..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpx_reqx.etc +++ /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 "static_2/static/reqx_reqx.ma". -include "basic_2/rt_transition/rpx_fsle.ma". - -(* EXTENDED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS **************) - -(* Properties with sort-irrelevant equivalence for local environments *******) - -(* Basic_2A1: was just: cpx_lleq_conf_sn *) -lemma cpx_reqx_conf_sn (G): - s_r_confluent1 … (cpx G) reqx. -/3 width=6 by cpx_rex_conf_sn/ qed-. - -(* Basic_2A1: was just: cpx_lleq_conf_dx *) -lemma cpx_reqx_conf_dx (G) (L2): - ∀T1,T2. ❪G,L2❫ ⊢ T1 ⬈ T2 → - ∀L1. L1 ≛[T1] L2 → L1 ≛[T2] L2. -/4 width=5 by cpx_reqx_conf_sn, reqx_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpxs_feqx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpxs_feqx.etc deleted file mode 100644 index 8017c74ce..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpxs_feqx.etc +++ /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 "static_2/static/feqx.ma". -include "basic_2/rt_computation/cpxs_reqx.ma". - -(* EXTENDED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS *************) - -(* Properties with sort-irrelevant equivalence for closures *****************) - -(* to be updated *) -lemma feqx_cpxs_trans: - ∀G1,G2,L1,L2,T1,T. ❪G1,L1,T1❫ ≛ ❪G2,L2,T❫ → - ∀T2. ❪G2,L2❫ ⊢ T ⬈* T2 → - ∃∃T0. ❪G1,L1❫ ⊢ T1 ⬈* T0 & ❪G1,L1,T0❫ ≛ ❪G2,L2,T2❫. -#G1 #G2 #L1 #L2 #T1 #T #H #T2 #H2T2 -elim (feqx_inv_gen_dx … H) -H #H #HL12 #HT1 destruct -lapply (reqx_cpxs_trans … H2T2 … HL12) #H1T2 -lapply (cpxs_reqx_conf_dx … H2T2 … HL12) -HL12 #HL12 -lapply (teqx_cpxs_trans … HT1 … H1T2) -T #HT12 -/3 width=3 by feqx_intro_dx, ex2_intro/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpxs_reqx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpxs_reqx.etc deleted file mode 100644 index ee504e981..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpxs_reqx.etc +++ /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/rt_transition/cpx_reqx.ma". -include "basic_2/rt_computation/cpxs_teqx.ma". - -(* EXTENDED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS *************) - -(* Properties with sort-irrelevant equivalence for local environments *******) - -(* Basic_2A1: was just: lleq_cpxs_trans *) -lemma reqx_cpxs_trans (G): - ∀L0,T0,T1. ❪G,L0❫ ⊢ T0 ⬈* T1 → ∀L2. L2 ≛[T0] L0 → ❪G,L2❫ ⊢ T0 ⬈* T1. -#G #L0 #T0 #T1 #H @(cpxs_ind_dx … H) -T0 // -#T0 #T #H0T0 #_ #IH #L2 #HL2 -lapply (reqx_cpx_trans … HL2 … H0T0) #H2T0 -lapply (IH L2 ?) -IH /2 width=5 by cpx_reqx_conf_dx/ -L0 #H2T1 -/2 width=3 by cpxs_strap2/ -qed-. - -(* Basic_2A1: was just: cpxs_lleq_conf *) -lemma cpxs_reqx_conf (G): - ∀L0,T0,T1. ❪G,L0❫ ⊢ T0 ⬈* T1 → ∀L2. L0 ≛[T0] L2 → ❪G,L2❫ ⊢ T0 ⬈* T1. -/3 width=3 by reqx_cpxs_trans, reqx_sym/ qed-. - -(* Basic_2A1: was just: cpxs_lleq_conf_dx *) -lemma cpxs_reqx_conf_dx (G): - ∀L2,T1,T2. ❪G,L2❫ ⊢ T1 ⬈* T2 → - ∀L1. L1 ≛[T1] L2 → L1 ≛[T2] L2. -#G #L2 #T1 #T2 #H @(cpxs_ind … H) -T2 /3 width=6 by cpx_reqx_conf_dx/ -qed-. - -(* Basic_2A1: was just: lleq_conf_sn *) -lemma cpxs_reqx_conf_sn (G): - ∀L1,T1,T2. ❪G,L1❫ ⊢ T1 ⬈* T2 → - ∀L2. L1 ≛[T1] L2 → L1 ≛[T2] L2. -/4 width=6 by cpxs_reqx_conf_dx, reqx_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpxs_teqx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpxs_teqx.etc deleted file mode 100644 index 0de7eb677..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpxs_teqx.etc +++ /dev/null @@ -1,46 +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/rt_transition/rpx_reqx.ma". -include "basic_2/rt_computation/cpxs.ma". - -(* EXTENDED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS *************) - -(* Properties with sort-irrelevant equivalence for terms ********************) - -lemma teqx_cpxs_trans (G) (L) (T): - ∀T1. T1 ≛ T → ∀T2. ❪G,L❫ ⊢ T ⬈* T2 → ❪G,L❫ ⊢ T1 ⬈* T2. -#G #L #T #T1 #HT1 #T2 #HT2 @(cpxs_ind … HT2) -T2 -[ /3 width=1 by teqx_cpx, cpx_cpxs/ -| /2 width=3 by cpxs_strap1/ -] -qed-. - -(* Note: this requires teqx to be symmetric *) -(* Nasic_2A1: uses: cpxs_neq_inv_step_sn *) -lemma cpxs_tneqx_fwd_step_sn (G) (L): - ∀T1,T2. ❪G,L❫ ⊢ T1 ⬈* T2 → (T1 ≛ T2 → ⊥) → - ∃∃T. ❪G,L❫ ⊢ T1 ⬈ T & T1 ≛ T → ⊥ & ❪G,L❫ ⊢ T ⬈* T2. -#G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1 -[ #H elim H -H // -| #T1 #T0 #HT10 #HT02 #IH #HnT12 - elim (teqx_dec T1 T0) [ -HT10 -HT02 #HT10 | -IH #HnT10 ] - [ elim IH -IH /3 width=3 by teqx_trans/ -HnT12 - #T #HT0 #HnT0 #HT2 - lapply (teqx_cpx_trans … HT10 … HT0) -HT0 #HT1 - /4 width=4 by teqx_canc_sn, ex3_intro/ - | /3 width=4 by ex3_intro/ - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/csx_feqx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/csx_feqx.etc deleted file mode 100644 index dc64354d0..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/csx_feqx.etc +++ /dev/null @@ -1,27 +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 "static_2/static/feqx.ma". -include "basic_2/rt_computation/csx_reqx.ma". - -(* STRONGLY NORMALIZING TERMS FOR EXTENDED PARALLEL RT-TRANSITION ***********) - -(* Properties with sort-irrelevant equivalence for closures *****************) - -lemma csx_feqx_conf: - ∀G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*𝐒 T1 → - ∀G2,L2,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ → ❪G2,L2❫ ⊢ ⬈*𝐒 T2. -#G1 #L1 #T1 #HT1 #G2 #L2 #T2 * -G2 -L2 -T2 -/3 width=3 by csx_reqx_conf, csx_teqx_trans/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/csx_reqx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/csx_reqx.etc deleted file mode 100644 index 5d35690cc..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/csx_reqx.etc +++ /dev/null @@ -1,36 +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/rt_transition/cpx_reqx.ma". -include "basic_2/rt_computation/csx_csx.ma". - -(* STRONGLY NORMALIZING TERMS FOR EXTENDED PARALLEL RT-TRANSITION ***********) - -(* Properties with sort-irrelevant equivalence for local environments *******) - -(* Basic_2A1: uses: csx_lleq_conf *) -lemma csx_reqx_conf (G) (L1): - ∀T. ❪G,L1❫ ⊢ ⬈*𝐒 T → - ∀L2. L1 ≛[T] L2 → ❪G,L2❫ ⊢ ⬈*𝐒 T. -#G #L1 #T #H -@(csx_ind … H) -T #T1 #_ #IH #L2 #HL12 -@csx_intro #T2 #HT12 #HnT12 -lapply (reqx_cpx_trans … HL12 … HT12) -HT12 -/3 width=4 by cpx_reqx_conf_sn/ -qed-. - -(* Basic_2A1: uses: csx_lleq_trans *) -lemma csx_reqx_trans (G) (L2): - ∀L1,T. L1 ≛[T] L2 → ❪G,L2❫ ⊢ ⬈*𝐒 T → ❪G,L1❫ ⊢ ⬈*𝐒 T. -/3 width=3 by csx_reqx_conf, reqx_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/fpb_feqx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/fpb_feqx.etc deleted file mode 100644 index c0e6a4b51..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/fpb_feqx.etc +++ /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 "static_2/s_transition/fqu_teqx.ma". -include "static_2/static/feqx.ma". -include "basic_2/rt_transition/fpb_reqx.ma". - -(* PROPER PARALLEL RST-TRANSITION FOR CLOSURES ******************************) - -(* Properties with degree-based equivalence for closures ********************) - -(* Basic_2A1: uses: fleq_fpb_trans *) -lemma feqx_fpb_trans: - ∀F1,F2,K1,K2,T1,T2. ❪F1,K1,T1❫ ≛ ❪F2,K2,T2❫ → - ∀G2,L2,U2. ❪F2,K2,T2❫ ≻ ❪G2,L2,U2❫ → - ∃∃G1,L1,U1. ❪F1,K1,T1❫ ≻ ❪G1,L1,U1❫ & ❪G1,L1,U1❫ ≛ ❪G2,L2,U2❫. -#F1 #F2 #K1 #K2 #T1 #T2 * -F2 -K2 -T2 -#K2 #T2 #HK12 #HT12 #G2 #L2 #U2 #H12 -elim (teqx_fpb_trans … HT12 … H12) -T2 #K0 #T0 #H #HT0 #HK0 -elim (reqx_fpb_trans … HK12 … H) -K2 #L0 #U0 #H #HUT0 #HLK0 -@(ex2_3_intro … H) -H (**) (* full auto too slow *) -/4 width=3 by feqx_intro_dx, reqx_trans, teqx_reqx_conf_sn, teqx_trans/ -qed-. - -(* Inversion lemmas with degree-based equivalence for closures **************) - -(* Basic_2A1: uses: fpb_inv_fleq *) -lemma fpb_inv_feqx: - ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → - ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ → ⊥. -#G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 -[ #G2 #L2 #T2 #H12 #H elim (feqx_inv_gen_sn … H) -H - /3 width=11 by reqx_fwd_length, fqu_inv_teqx/ -| #T2 #_ #HnT #H elim (feqx_inv_gen_sn … H) -H /2 width=1 by/ -| #L2 #_ #HnL #H elim (feqx_inv_gen_sn … H) -H /2 width=1 by/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/fpb_reqx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/fpb_reqx.etc deleted file mode 100644 index 14a0f8098..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/fpb_reqx.etc +++ /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 "static_2/static/reqx_fqus.ma". -include "basic_2/rt_transition/cpx_reqx.ma". -include "basic_2/rt_transition/lpx_reqx.ma". -include "basic_2/rt_transition/fpb.ma". - -(* PROPER PARALLEL RST-TRANSITION FOR CLOSURES ******************************) - -(* Properties with sort-irrelevant equivalence for local environments *******) - -lemma teqx_fpb_trans: - ∀U2,U1. U2 ≛ U1 → - ∀G1,G2,L1,L2,T1. ❪G1,L1,U1❫ ≻ ❪G2,L2,T1❫ → - ∃∃L,T2. ❪G1,L1,U2❫ ≻ ❪G2,L,T2❫ & T2 ≛ T1 & L ≛[T1] L2. -#U2 #U1 #HU21 #G1 #G2 #L1 #L2 #T1 * -G2 -L2 -T1 -[ #G2 #L2 #T1 #H - elim (teqx_fqu_trans … H … HU21) -H - /3 width=5 by fpb_fqu, ex3_2_intro/ -| #T1 #HUT1 #HnUT1 - lapply (teqx_cpx_trans … HU21 … HUT1) -HUT1 - /6 width=5 by fpb_cpx, teqx_canc_sn, teqx_trans, ex3_2_intro/ -| /6 width=5 by fpb_lpx, rpx_teqx_div, teqx_reqx_conf_sn, ex3_2_intro/ -] -qed-. - -(* Basic_2A1: was just: lleq_fpb_trans *) -lemma reqx_fpb_trans: - ∀F,K1,K2,T. K1 ≛[T] K2 → - ∀G,L2,U. ❪F,K2,T❫ ≻ ❪G,L2,U❫ → - ∃∃L1,U0. ❪F,K1,T❫ ≻ ❪G,L1,U0❫ & U0 ≛ U & L1 ≛[U] L2. -#F #K1 #K2 #T #HT #G #L2 #U * -G -L2 -U -[ #G #L2 #U #H2 elim (reqx_fqu_trans … H2 … HT) -K2 - /3 width=5 by fpb_fqu, ex3_2_intro/ -| #U #HTU #HnTU lapply (reqx_cpx_trans … HT … HTU) -HTU - /5 width=11 by fpb_cpx, cpx_reqx_conf_sn, teqx_trans, teqx_reqx_conf_sn, ex3_2_intro/ (**) (* time: 36s on dev *) -| #L2 #HKL2 #HnKL2 elim (reqx_lpx_trans … HKL2 … HT) -HKL2 - /6 width=5 by fpb_lpx, (* 2x *) reqx_canc_sn, ex3_2_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/fpbq_feqx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/fpbq_feqx.etc deleted file mode 100644 index f5d330427..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/fpbq_feqx.etc +++ /dev/null @@ -1,27 +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 "static_2/static/feqx.ma". -include "basic_2/rt_transition/rpx_reqx.ma". -include "basic_2/rt_transition/fpbq.ma". - -(* PARALLEL RST-TRANSITION FOR CLOSURES *************************************) - -(* Basic_2A1: includes: fleq_fpbq fpbq_lleq *) -lemma fpbq_feqx (G1) (G2): - ∀L1,L2,T1,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫. -#G1 #G2 #L1 #L2 #T1 #T2 #H -elim (feqx_inv_gen_sn … H) #H #HL12 #HT12 destruct -/3 width=3 by fpbq_rcpx, reqx_rpx_trans, teqx_cpx_trans/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/fsb_feqx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/fsb_feqx.etc deleted file mode 100644 index 159663b11..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/fsb_feqx.etc +++ /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/rt_transition/fpb_feqx.ma". -include "basic_2/rt_computation/fsb.ma". - -(* STRONGLY NORMALIZING CLOSURES FOR PARALLEL RST-TRANSITION ****************) - -(* Properties with sort-irrelevant equivalence for closures *****************) - -lemma fsb_feqx_trans: - ∀G1,L1,T1. ≥𝐒 ❪G1,L1,T1❫ → - ∀G2,L2,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ → ≥𝐒 ❪G2,L2,T2❫. -#G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1 -#G1 #L1 #T1 #_ #IH #G2 #L2 #T2 #H12 -@fsb_intro #G #L #T #H2 -elim (feqx_fpb_trans … H12 … H2) -G2 -L2 -T2 -/2 width=5 by/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/lpx_reqx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/lpx_reqx.etc deleted file mode 100644 index dfd367241..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/lpx_reqx.etc +++ /dev/null @@ -1,56 +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 "static_2/static/reqx_req.ma". -include "basic_2/rt_transition/rpx_reqx.ma". -include "basic_2/rt_transition/rpx_lpx.ma". - -(* EXTENDED PARALLEL RT-TRANSITION FOR FULL LOCAL ENVIRONMENTS **************) - -(* Properties with sort-irrelevant equivalence for local environments *******) - -lemma reqx_lpx_trans_rpx (G) (L) (T:term): - ∀L1. L1 ≛[T] L → ∀L2. ❪G,L❫ ⊢ ⬈ L2 → ❪G,L❫ ⊢ ⬈[T] L2. -/3 width=1 by lpx_rpx, reqx_rpx_trans/ qed. - -(* Basic_2A1: uses: lleq_lpx_trans *) -lemma reqx_lpx_trans (G): - ∀L2,K2. ❪G,L2❫ ⊢ ⬈ K2 → ∀L1. ∀T:term. L1 ≛[T] L2 → - ∃∃K1. ❪G,L1❫ ⊢ ⬈ K1 & K1 ≛[T] K2. -#G #L2 #K2 #HLK2 #L1 #T #HL12 -lapply (lpx_rpx … T … HLK2) -HLK2 #HLK2 -lapply (reqx_rpx_trans … HL12 … HLK2) -L2 #H -elim (rpx_fwd_lpx_req … H) -H #K1 #HLK1 #HK12 -/3 width=3 by req_reqx, ex2_intro/ -qed-. - -(* Inversion lemmas with sort-irrelevant equivalence for local environments *) - -lemma rpx_inv_reqx_lpx (G) (T): - ∀L1,L2. ❪G,L1❫ ⊢ ⬈[T] L2 → - ∃∃L. L1 ≛[T] L & ❪G,L❫ ⊢ ⬈ L2. -#G #T #L1 #L2 #H -elim (rpx_inv_req_lpx … H) -H #L #HL1 #HL2 -/3 width=3 by req_reqx, ex2_intro/ -qed-. - -(* Forward lemmas with sort-irrelevant equivalence for local environments ***) - -lemma rpx_fwd_lpx_reqx (G) (T): - ∀L1,L2. ❪G,L1❫ ⊢ ⬈[T] L2 → - ∃∃L. ❪G,L1❫ ⊢ ⬈ L & L ≛[T] L2. -#G #T #L1 #L2 #H -elim (rpx_fwd_lpx_req … H) -H #L #HL1 #HL2 -/3 width=3 by req_reqx, ex2_intro/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/lpxs_feqx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/lpxs_feqx.etc deleted file mode 100644 index 04f5a2b29..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/lpxs_feqx.etc +++ /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 "static_2/static/feqx.ma". -include "basic_2/rt_computation/lpxs_reqx.ma". - -(* EXTENDED PARALLEL RT-COMPUTATION FOR FULL LOCAL ENVIRONMENTS **************) - -(* Properties with sort-irrelevant equivalence on closures ******************) - -lemma feqx_lpxs_trans: - ∀G1,G2,L1,L0,T1,T2. ❪G1,L1,T1❫ ≛ ❪G2,L0,T2❫ → - ∀L2. ❪G2,L0❫ ⊢⬈* L2 → - ∃∃L. ❪G1,L1❫ ⊢⬈* L & ❪G1,L,T1❫ ≛ ❪G2,L2,T2❫. -#G1 #G2 #L1 #L0 #T1 #T2 #H1 #L2 #HL02 -elim (feqx_inv_gen_dx … H1) -H1 #HG #HL10 #HT12 destruct -elim (reqx_lpxs_trans … HL02 … HL10) -L0 #L0 #HL10 #HL02 -/3 width=3 by feqx_intro_dx, ex2_intro/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/lpxs_reqx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/lpxs_reqx.etc deleted file mode 100644 index 886c4dffb..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/lpxs_reqx.etc +++ /dev/null @@ -1,49 +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/rt_transition/lpx_reqx.ma". -include "basic_2/rt_computation/lpxs_lpx.ma". - -(* EXTENDED PARALLEL RT-COMPUTATION FOR FULL LOCAL ENVIRONMENTS *************) - -(* Properties with sort-irrelevant equivalence on referred entries **********) - -(* Basic_2A1: uses: lleq_lpxs_trans *) -lemma reqx_lpxs_trans (G) (T:term): - ∀L2,K2. ❪G,L2❫ ⊢ ⬈* K2 → ∀L1. L1 ≛[T] L2 → - ∃∃K1. ❪G,L1❫ ⊢ ⬈* K1 & K1 ≛[T] K2. -#G #T #L2 #K2 #H @(lpxs_ind_sn … H) -L2 /2 width=3 by ex2_intro/ -#L #L2 #HL2 #_ #IH #L1 #HT -elim (reqx_lpx_trans … HL2 … HT) -L #L #HL1 #HT -elim (IH … HT) -L2 #K #HLK #HT -/3 width=3 by lpxs_step_sn, ex2_intro/ -qed-. - -(* Basic_2A1: uses: lpxs_nlleq_inv_step_sn *) -lemma lpxs_rneqx_inv_step_sn (G) (T:term): - ∀L1,L2. ❪G,L1❫ ⊢ ⬈* L2 → (L1 ≛[T] L2 → ⊥) → - ∃∃L,L0. ❪G,L1❫ ⊢ ⬈ L & L1 ≛[T] L → ⊥ & ❪G,L❫ ⊢ ⬈* L0 & L0 ≛[T] L2. -#G #T #L1 #L2 #H @(lpxs_ind_sn … H) -L1 -[ #H elim H -H // -| #L1 #L #H1 #H2 #IH2 #H12 elim (reqx_dec L1 L T) #H - [ -H1 -H2 elim IH2 -IH2 /3 width=3 by reqx_trans/ -H12 - #L0 #L3 #H1 #H2 #H3 #H4 lapply (reqx_rneqx_trans … H … H2) -H2 - #H2 elim (reqx_lpx_trans … H1 … H) -L - #L #H1 #H lapply (rneqx_reqx_div … H … H2) -H2 - #H2 elim (reqx_lpxs_trans … H3 … H) -L0 - /3 width=8 by reqx_trans, ex4_2_intro/ - | -H12 -IH2 /3 width=6 by ex4_2_intro/ - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb.ma index 30864de70..3f4ccd360 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb.ma @@ -17,28 +17,32 @@ include "basic_2/rt_transition/fpbc.ma". (* STRONGLY NORMALIZING CLOSURES FOR PARALLEL RST-TRANSITION ****************) -inductive fsb: relation3 genv lenv term ≝ -| fsb_intro: ∀G1,L1,T1. - (∀G2,L2,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → fsb G2 L2 T2) → - fsb G1 L1 T1 -. +definition fsb: relation3 genv lenv term ≝ + SN3 … fpb (feqg sfull). interpretation "strong normalization for parallel rst-transition (closure)" 'PRedSubTyStrong G L T = (fsb G L T). +(* Basic properties *********************************************************) + +lemma fsb_intro (G1) (L1) (T1): + (∀G2,L2,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → ≥𝐒 ❪G2,L2,T2❫) → ≥𝐒 ❪G1,L1,T1❫. +/5 width=1 by fpbc_intro, SN3_intro/ qed. + (* Basic eliminators ********************************************************) (* Note: eliminator with shorter ground hypothesis *) -(* Note: to be named fsb_ind when fsb becomes a definition like csx, rsx ****) -lemma fsb_ind_alt (Q:relation3 …): +lemma fsb_ind (Q:relation3 …): (∀G1,L1,T1. ≥𝐒 ❪G1,L1,T1❫ → (∀G2,L2,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → Q G2 L2 T2) → Q G1 L1 T1 ) → ∀G,L,T. ≥𝐒 ❪G,L,T❫ → Q G L T. #Q #IH #G #L #T #H elim H -G -L -T -/4 width=1 by fsb_intro/ +#G1 #L1 #T1 #H1 #IH1 +@IH -IH [ /4 width=1 by SN3_intro/ ] -H1 #G2 #L2 #T2 #H +elim (fpbc_inv_gen sfull … H) -H #H12 #Hn12 /3 width=1 by/ qed-. (* Basic_2A1: removed theorems 6: diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma index 628b3b9df..e3ad463a6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma @@ -25,7 +25,7 @@ include "basic_2/rt_computation/fsb_fpbg.ma". lemma fsb_inv_csx: ∀G,L,T. ≥𝐒 ❪G,L,T❫ → ❪G,L❫ ⊢ ⬈*𝐒 T. -#G #L #T #H @(fsb_ind_alt … H) -G -L -T +#G #L #T #H @(fsb_ind … H) -G -L -T /5 width=1 by csx_intro, cpx_fpbc/ qed-. @@ -76,7 +76,7 @@ lemma csx_ind_fpbc (Q:relation3 …): Q G1 L1 T1 ) → ∀G,L,T. ❪G,L❫ ⊢ ⬈*𝐒 T → Q G L T. -/4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind_alt/ qed-. +/4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind/ qed-. lemma csx_ind_fpbg (Q:relation3 …): (∀G1,L1,T1. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_feqg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_feqg.ma index f2a7640d1..73ae6efed 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_feqg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_feqg.ma @@ -24,7 +24,7 @@ lemma fsb_feqg_trans (S): reflexive … S → symmetric … S → Transitive … S → ∀G1,L1,T1. ≥𝐒 ❪G1,L1,T1❫ → ∀G2,L2,T2. ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → ≥𝐒 ❪G2,L2,T2❫. -#S #H1S #H2S #H3S #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1 +#S #H1S #H2S #H3S #G1 #L1 #T1 #H @(fsb_ind … H) -G1 -L1 -T1 #G1 #L1 #T1 #_ #IH #G2 #L2 #T2 #H12 @fsb_intro #G #L #T #H2 elim (feqg_fpbc_trans … H12 … H2) -G2 -L2 -T2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma index 18902f2cc..afe697426 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma @@ -23,7 +23,7 @@ include "basic_2/rt_computation/fsb_feqg.ma". lemma fsb_fpbs_trans: ∀G1,L1,T1. ≥𝐒 ❪G1,L1,T1❫ → ∀G2,L2,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ → ≥𝐒 ❪G2,L2,T2❫. -#G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1 +#G1 #L1 #T1 #H @(fsb_ind … H) -G1 -L1 -T1 #G1 #L1 #T1 #H1 #IH #G2 #L2 #T2 #H12 elim (fpbs_inv_fpbg … H12) -H12 [ -IH /2 width=9 by fsb_feqg_trans/ @@ -56,7 +56,7 @@ lemma fsb_ind_fpbg_fpbs (Q:relation3 …): ) → ∀G1,L1,T1. ≥𝐒 ❪G1,L1,T1❫ → ∀G2,L2,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ → Q G2 L2 T2. -#Q #IH1 #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1 +#Q #IH1 #G1 #L1 #T1 #H @(fsb_ind … H) -G1 -L1 -T1 #G1 #L1 #T1 #H1 #IH #G2 #L2 #T2 #H12 @IH1 -IH1 [ -IH /2 width=5 by fsb_fpbs_trans/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml index befee2607..e4b19cdd8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml @@ -27,7 +27,7 @@ - Improved rst-transition and related theory. + Improved theory of rst-transition. Sort hierarchy parameter removed from unbound rt-transition diff --git a/matita/matita/contribs/lambdadelta/ground/lib/relations.ma b/matita/matita/contribs/lambdadelta/ground/lib/relations.ma index 3d67a576c..b132d8682 100644 --- a/matita/matita/contribs/lambdadelta/ground/lib/relations.ma +++ b/matita/matita/contribs/lambdadelta/ground/lib/relations.ma @@ -27,14 +27,16 @@ definition replace_2 (A) (B): relation3 (relation2 A B) (relation A) (relation B definition subR2 (S1) (S2): relation (relation2 S1 S2) ≝ λR1,R2. (∀a1,a2. R1 a1 a2 → R2 a1 a2). -interpretation "2-relation inclusion" - 'subseteq R1 R2 = (subR2 ?? R1 R2). +interpretation + "2-relation inclusion" + 'subseteq R1 R2 = (subR2 ?? R1 R2). definition subR3 (S1) (S2) (S3): relation (relation3 S1 S2 S3) ≝ λR1,R2. (∀a1,a2,a3. R1 a1 a2 a3 → R2 a1 a2 a3). -interpretation "3-relation inclusion" - 'subseteq R1 R2 = (subR3 ??? R1 R2). +interpretation + "3-relation inclusion" + 'subseteq R1 R2 = (subR3 ??? R1 R2). (* Properties of relations **************************************************) @@ -107,11 +109,11 @@ definition NF (A): relation A → relation A → predicate A ≝ λR,S,a1. ∀a2. R a1 a2 → S a1 a2. definition NF_dec (A): relation A → relation A → Prop ≝ - λR,S. ∀a1. NF A R S a1 ∨ + λR,S. ∀a1. NF … R S a1 ∨ ∃∃a2. R … a1 a2 & (S a1 a2 → ⊥). inductive SN (A) (R,S:relation A): predicate A ≝ -| SN_intro: ∀a1. (∀a2. R a1 a2 → (S a1 a2 → ⊥) → SN A R S a2) → SN A R S a1 +| SN_intro: ∀a1. (∀a2. R a1 a2 → (S a1 a2 → ⊥) → SN … R S a2) → SN … R S a1 . lemma NF_to_SN (A) (R) (S): ∀a. NF A R S a → SN A R S a. @@ -121,10 +123,10 @@ elim HSa12 -HSa12 /2 width=1 by/ qed. definition NF_sn (A): relation A → relation A → predicate A ≝ - λR,S,a2. ∀a1. R a1 a2 → S a1 a2. + λR,S,a2. ∀a1. R a1 a2 → S a1 a2. inductive SN_sn (A) (R,S:relation A): predicate A ≝ -| SN_sn_intro: ∀a2. (∀a1. R a1 a2 → (S a1 a2 → ⊥) → SN_sn A R S a1) → SN_sn A R S a2 +| SN_sn_intro: ∀a2. (∀a1. R a1 a2 → (S a1 a2 → ⊥) → SN_sn … R S a1) → SN_sn … R S a2 . lemma NF_to_SN_sn (A) (R) (S): ∀a. NF_sn A R S a → SN_sn A R S a. @@ -133,6 +135,12 @@ lemma NF_to_SN_sn (A) (R) (S): ∀a. NF_sn A R S a → SN_sn A R S a. elim HSa12 -HSa12 /2 width=1 by/ qed. +(* Normal form and strong normalization on unboxed triples ******************) + +inductive SN3 (A) (B) (C) (R,S:relation6 A B C A B C): relation3 A B C ≝ +| SN3_intro: ∀a1,b1,c1. (∀a2,b2,c2. R a1 b1 c1 a2 b2 c2 → (S a1 b1 c1 a2 b2 c2 → ⊥) → SN3 … R S a2 b2 c2) → SN3 … R S a1 b1 c1 +. + (* Relations on unboxed triples *********************************************) definition tri_RC (A,B,C): tri_relation A B C → tri_relation A B C ≝ diff --git a/matita/matita/contribs/lambdadelta/static_2/etc/teqx/feqx_fqup.etc b/matita/matita/contribs/lambdadelta/static_2/etc/teqx/feqx_fqup.etc deleted file mode 100644 index 2821e6718..000000000 --- a/matita/matita/contribs/lambdadelta/static_2/etc/teqx/feqx_fqup.etc +++ /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 "static_2/static/reqx_fqup.ma". -include "static_2/static/feqx.ma". - -(* SORT-IRRELEVANT EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES *************) - -(* Properties with sort-irrelevant equivalence for terms ********************) - -lemma teqx_feqx: ∀T1,T2. T1 ≛ T2 → - ∀G,L. ❪G,L,T1❫ ≛ ❪G,L,T2❫. -/2 width=1 by feqx_intro_sn/ qed. - -(* Advanced properties ******************************************************) - -lemma feqx_refl: tri_reflexive … feqx. -/2 width=1 by feqx_intro_sn/ qed. diff --git a/matita/matita/contribs/lambdadelta/static_2/etc/teqx/feqx_fqus.etc b/matita/matita/contribs/lambdadelta/static_2/etc/teqx/feqx_fqus.etc deleted file mode 100644 index 0b370bd33..000000000 --- a/matita/matita/contribs/lambdadelta/static_2/etc/teqx/feqx_fqus.etc +++ /dev/null @@ -1,32 +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 "static_2/static/reqx_fqus.ma". -include "static_2/static/feqx.ma". - -(* SORT-IRRELEVANT EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES *************) - -(* Properties with star-iterated structural successor for closures **********) - -lemma feqx_fqus_trans (b): - ∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≛ ❪G,L,T❫ → - ∀G2,L2,T2. ❪G,L,T❫ ⬂*[b] ❪G2,L2,T2❫ → - ∃∃G,L0,T0. ❪G1,L1,T1❫ ⬂*[b] ❪G,L0,T0❫ & ❪G,L0,T0❫ ≛ ❪G2,L2,T2❫. -#b #G1 #G #L1 #L #T1 #T #H1 #G2 #L2 #T2 #H2 -elim(feqx_inv_gen_dx … H1) -H1 #HG #HL1 #HT1 destruct -elim (reqx_fqus_trans … H2 … HL1) -L #L #T0 #H2 #HT02 #HL2 -elim (teqx_fqus_trans … H2 … HT1) -T #L0 #T #H2 #HT0 #HL0 -lapply (teqx_reqx_conf_sn … HT02 … HL0) -HL0 #HL0 -/4 width=7 by feqx_intro_dx, reqx_trans, teqx_trans, ex2_3_intro/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/etc/teqx/feqx_req.etc b/matita/matita/contribs/lambdadelta/static_2/etc/teqx/feqx_req.etc deleted file mode 100644 index 466275aad..000000000 --- a/matita/matita/contribs/lambdadelta/static_2/etc/teqx/feqx_req.etc +++ /dev/null @@ -1,27 +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 "static_2/static/reqx_req.ma". -include "static_2/static/feqx.ma". - -(* SORT-IRRELEVANT EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES *************) - -(* Properties with syntactic equivalence on referred entries ****************) - -lemma req_feqx_trans: ∀L1,L,T1. L1 ≡[T1] L → - ∀G1,G2,L2,T2. ❪G1,L,T1❫ ≛ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫. -#L1 #L #T1 #HL1 #G1 #G2 #L2 #T2 #H -elim (feqx_inv_gen_sn … H) -H #H #HL2 #T12 destruct -/3 width=3 by feqx_intro_sn, req_reqx_trans/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/etc/teqx/req.etc b/matita/matita/contribs/lambdadelta/static_2/etc/teqx/req.etc deleted file mode 100644 index b53ef1755..000000000 --- a/matita/matita/contribs/lambdadelta/static_2/etc/teqx/req.etc +++ /dev/null @@ -1,117 +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 "static_2/notation/relations/ideqsn_3.ma". -include "static_2/static/rex.ma". - -(* SYNTACTIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *********) - -(* Basic_2A1: was: lleq *) -definition req: relation3 term lenv lenv ≝ - rex ceq. - -interpretation - "syntactic equivalence on referred entries (local environment)" - 'IdEqSn T L1 L2 = (req T L1 L2). - -(* Note: "R_transitive_req R" is equivalent to "R_transitive_rex ceq R R" *) -(* Basic_2A1: uses: lleq_transitive *) -definition R_transitive_req: predicate (relation3 lenv term term) ≝ - λR. ∀L2,T1,T2. R L2 T1 T2 → ∀L1. L1 ≡[T1] L2 → R L1 T1 T2. - -(* Basic inversion lemmas ***************************************************) - -lemma req_inv_bind: - ∀p,I,L1,L2,V,T. L1 ≡[ⓑ[p,I]V.T] L2 → - ∧∧ L1 ≡[V] L2 & L1.ⓑ[I]V ≡[T] L2.ⓑ[I]V. -/2 width=2 by rex_inv_bind/ qed-. - -lemma req_inv_flat: - ∀I,L1,L2,V,T. L1 ≡[ⓕ[I]V.T] L2 → - ∧∧ L1 ≡[V] L2 & L1 ≡[T] L2. -/2 width=2 by rex_inv_flat/ qed-. - -(* Advanced inversion lemmas ************************************************) - -lemma req_inv_zero_pair_sn: - ∀I,L2,K1,V. K1.ⓑ[I]V ≡[#0] L2 → - ∃∃K2. K1 ≡[V] K2 & L2 = K2.ⓑ[I]V. -#I #L2 #K1 #V #H -elim (rex_inv_zero_pair_sn … H) -H #K2 #X #HK12 #HX #H destruct -/2 width=3 by ex2_intro/ -qed-. - -lemma req_inv_zero_pair_dx: - ∀I,L1,K2,V. L1 ≡[#0] K2.ⓑ[I]V → - ∃∃K1. K1 ≡[V] K2 & L1 = K1.ⓑ[I]V. -#I #L1 #K2 #V #H -elim (rex_inv_zero_pair_dx … H) -H #K1 #X #HK12 #HX #H destruct -/2 width=3 by ex2_intro/ -qed-. - -lemma req_inv_lref_bind_sn: - ∀I1,K1,L2,i. K1.ⓘ[I1] ≡[#↑i] L2 → - ∃∃I2,K2. K1 ≡[#i] K2 & L2 = K2.ⓘ[I2]. -/2 width=2 by rex_inv_lref_bind_sn/ qed-. - -lemma req_inv_lref_bind_dx: - ∀I2,K2,L1,i. L1 ≡[#↑i] K2.ⓘ[I2] → - ∃∃I1,K1. K1 ≡[#i] K2 & L1 = K1.ⓘ[I1]. -/2 width=2 by rex_inv_lref_bind_dx/ qed-. - -(* Basic forward lemmas *****************************************************) - -(* Basic_2A1: was: llpx_sn_lrefl *) -(* Basic_2A1: this should have been lleq_fwd_llpx_sn *) -lemma req_fwd_rex (R): - c_reflexive … R → - ∀L1,L2,T. L1 ≡[T] L2 → L1 ⪤[R,T] L2. -#R #HR #L1 #L2 #T * #f #Hf #HL12 -/4 width=7 by sex_co, cext2_co, ex2_intro/ -qed-. - -(* Basic_properties *********************************************************) - -lemma frees_req_conf: - ∀f,L1,T. L1 ⊢ 𝐅+❪T❫ ≘ f → - ∀L2. L1 ≡[T] L2 → L2 ⊢ 𝐅+❪T❫ ≘ f. -#f #L1 #T #H elim H -f -L1 -T -[ /2 width=3 by frees_sort/ -| #f #i #Hf #L2 #H2 - >(rex_inv_atom_sn … H2) -L2 - /2 width=1 by frees_atom/ -| #f #I #L1 #V1 #_ #IH #Y #H2 - elim (req_inv_zero_pair_sn … H2) -H2 #L2 #HL12 #H destruct - /3 width=1 by frees_pair/ -| #f #I #L1 #Hf #Y #H2 - elim (rex_inv_zero_unit_sn … H2) -H2 #g #L2 #_ #_ #H destruct - /2 width=1 by frees_unit/ -| #f #I #L1 #i #_ #IH #Y #H2 - elim (req_inv_lref_bind_sn … H2) -H2 #J #L2 #HL12 #H destruct - /3 width=1 by frees_lref/ -| /2 width=1 by frees_gref/ -| #f1V #f1T #f1 #p #I #L1 #V1 #T1 #_ #_ #Hf1 #IHV #IHT #L2 #H2 - elim (req_inv_bind … H2) -H2 /3 width=5 by frees_bind/ -| #f1V #f1T #f1 #I #L1 #V1 #T1 #_ #_ #Hf1 #IHV #IHT #L2 #H2 - elim (req_inv_flat … H2) -H2 /3 width=5 by frees_flat/ -] -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/static_2/etc/teqx/req_drops.etc b/matita/matita/contribs/lambdadelta/static_2/etc/teqx/req_drops.etc deleted file mode 100644 index fa8ea6d84..000000000 --- a/matita/matita/contribs/lambdadelta/static_2/etc/teqx/req_drops.etc +++ /dev/null @@ -1,26 +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 "static_2/static/rex_drops.ma". -include "static_2/static/req.ma". - -(* SYNTACTIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *********) - -(* Note: req_inv_lifts_dx missing in basic_2A1 *) - -(* Basic_2A1: uses: lleq_inv_lift_le lleq_inv_lift_be lleq_inv_lift_ge *) -lemma req_inv_lifts_bi: ∀L1,L2,U. L1 ≡[U] L2 → ∀b,f. 𝐔❪f❫ → - ∀K1,K2. ⇩*[b,f] L1 ≘ K1 → ⇩*[b,f] L2 ≘ K2 → - ∀T. ⇧*[f] T ≘ U → K1 ≡[T] K2. -/2 width=10 by rex_inv_lifts_bi/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/etc/teqx/req_fqup.etc b/matita/matita/contribs/lambdadelta/static_2/etc/teqx/req_fqup.etc deleted file mode 100644 index 4434b4d69..000000000 --- a/matita/matita/contribs/lambdadelta/static_2/etc/teqx/req_fqup.etc +++ /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 "static_2/static/rex_fqup.ma". -include "static_2/static/req.ma". - -(* SYNTACTIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *********) - -(* Advanced properties ******************************************************) - -(* Basic_2A1: was: lleq_refl *) -lemma req_refl: ∀T. reflexive … (req T). -/2 width=1 by rex_refl/ qed. diff --git a/matita/matita/contribs/lambdadelta/static_2/etc/teqx/req_length.etc b/matita/matita/contribs/lambdadelta/static_2/etc/teqx/req_length.etc deleted file mode 100644 index e5bd7b4a8..000000000 --- a/matita/matita/contribs/lambdadelta/static_2/etc/teqx/req_length.etc +++ /dev/null @@ -1,36 +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 "static_2/static/rex_length.ma". -include "static_2/static/rex_fsle.ma". -include "static_2/static/req.ma". - -(* SYNTACTIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *********) - -(* Advanved properties with free variables inclusion ************************) - -lemma req_fsge_comp: - rex_fsge_compatible ceq. -#L1 #L2 #T #H elim H #f1 #Hf1 #HL12 -lapply (frees_req_conf … Hf1 … H) -H -lapply (sex_fwd_length … HL12) -/3 width=8 by lveq_length_eq, ex4_4_intro/ (**) (* full auto fails *) -qed-. - -(* Advanced properties ******************************************************) - -(* Basic_2A1: uses: lleq_sym *) -lemma req_sym (T): - symmetric … (req T). -/3 width=1 by req_fsge_comp, rex_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/etc/teqx/reqx_drops.etc b/matita/matita/contribs/lambdadelta/static_2/etc/teqx/reqx_drops.etc deleted file mode 100644 index 6711a1d47..000000000 --- a/matita/matita/contribs/lambdadelta/static_2/etc/teqx/reqx_drops.etc +++ /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 "static_2/relocation/lifts_teqx.ma". -include "static_2/static/rex_drops.ma". -include "static_2/static/reqx.ma". - -(* SORT-IRRELEVANT EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ***) - -(* Properties with generic slicing for local environments *******************) - -lemma reqx_lifts_sn: f_dedropable_sn cdeq. -/3 width=5 by rex_liftable_dedropable_sn, teqx_lifts_sn/ qed-. - -(* Inversion lemmas with generic slicing for local environments *************) - -lemma reqx_inv_lifts_sn: f_dropable_sn cdeq. -/2 width=5 by rex_dropable_sn/ qed-. - -lemma reqx_inv_lifts_dx: f_dropable_dx cdeq. -/2 width=5 by rex_dropable_dx/ qed-. - -lemma reqx_inv_lifts_bi: ∀L1,L2,U. L1 ≛[U] L2 → ∀b,f. 𝐔❪f❫ → - ∀K1,K2. ⇩*[b,f] L1 ≘ K1 → ⇩*[b,f] L2 ≘ K2 → - ∀T. ⇧*[f] T ≘ U → K1 ≛[T] K2. -/2 width=10 by rex_inv_lifts_bi/ qed-. - -lemma reqx_inv_lref_pair_sn: ∀L1,L2,i. L1 ≛[#i] L2 → ∀I,K1,V1. ⇩[i] L1 ≘ K1.ⓑ[I]V1 → - ∃∃K2,V2. ⇩[i] L2 ≘ K2.ⓑ[I]V2 & K1 ≛[V1] K2 & V1 ≛ V2. -/2 width=3 by rex_inv_lref_pair_sn/ qed-. - -lemma reqx_inv_lref_pair_dx: ∀L1,L2,i. L1 ≛[#i] L2 → ∀I,K2,V2. ⇩[i] L2 ≘ K2.ⓑ[I]V2 → - ∃∃K1,V1. ⇩[i] L1 ≘ K1.ⓑ[I]V1 & K1 ≛[V1] K2 & V1 ≛ V2. -/2 width=3 by rex_inv_lref_pair_dx/ qed-. - -lemma reqx_inv_lref_pair_bi (L1) (L2) (i): - L1 ≛[#i] L2 → - ∀I1,K1,V1. ⇩[i] L1 ≘ K1.ⓑ[I1]V1 → - ∀I2,K2,V2. ⇩[i] L2 ≘ K2.ⓑ[I2]V2 → - ∧∧ K1 ≛[V1] K2 & V1 ≛ V2 & I1 = I2. -/2 width=6 by rex_inv_lref_pair_bi/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/etc/teqx/reqx_fqup.etc b/matita/matita/contribs/lambdadelta/static_2/etc/teqx/reqx_fqup.etc deleted file mode 100644 index bc021d8b9..000000000 --- a/matita/matita/contribs/lambdadelta/static_2/etc/teqx/reqx_fqup.etc +++ /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 "static_2/static/rex_fqup.ma". -include "static_2/static/reqx.ma". - -(* SORT-IRRELEVANT EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ***) - -(* Advanced properties ******************************************************) - -lemma reqx_refl: ∀T. reflexive … (reqx T). -/2 width=1 by rex_refl/ qed. - -lemma reqx_pair_refl: ∀V1,V2. V1 ≛ V2 → - ∀I,L. ∀T:term. L.ⓑ[I]V1 ≛[T] L.ⓑ[I]V2. -/2 width=1 by rex_pair_refl/ qed. - -(* Advanced inversion lemmas ************************************************) - -lemma reqx_inv_bind_void: ∀p,I,L1,L2,V,T. L1 ≛[ⓑ[p,I]V.T] L2 → - L1 ≛[V] L2 ∧ L1.ⓧ ≛[T] L2.ⓧ. -/2 width=3 by rex_inv_bind_void/ qed-. - -(* Advanced forward lemmas **************************************************) - -lemma reqx_fwd_bind_dx_void: ∀p,I,L1,L2,V,T. - L1 ≛[ⓑ[p,I]V.T] L2 → L1.ⓧ ≛[T] L2.ⓧ. -/2 width=4 by rex_fwd_bind_dx_void/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/etc/teqx/reqx_fqus.etc b/matita/matita/contribs/lambdadelta/static_2/etc/teqx/reqx_fqus.etc deleted file mode 100644 index b5f80fc34..000000000 --- a/matita/matita/contribs/lambdadelta/static_2/etc/teqx/reqx_fqus.etc +++ /dev/null @@ -1,165 +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 "static_2/s_computation/fqus_fqup.ma". -include "static_2/static/reqx_drops.ma". -include "static_2/static/reqx_fqup.ma". -include "static_2/static/reqx_reqx.ma". - -(* SORT-IRRELEVANT EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ***) - -(* Properties with extended structural successor for closures ***************) - -lemma fqu_teqx_conf (b): - ∀G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂[b] ❪G2,L2,T1❫ → - ∀U2. U1 ≛ U2 → - ∃∃L,T2. ❪G1,L1,U2❫ ⬂[b] ❪G2,L,T2❫ & L2 ≛[T1] L & T1 ≛ T2. -#b #G1 #G2 #L1 #L2 #U1 #T1 #H elim H -G1 -G2 -L1 -L2 -U1 -T1 -[ #I #G #L #W #X #H >(teqx_inv_lref1 … H) -X - /2 width=5 by fqu_lref_O, ex3_2_intro/ -| #I #G #L #W1 #U1 #X #H - elim (teqx_inv_pair1 … H) -H #W2 #U2 #HW12 #_ #H destruct - /2 width=5 by fqu_pair_sn, ex3_2_intro/ -| #p #I #G #L #W1 #U1 #Hb #X #H - elim (teqx_inv_pair1 … H) -H #W2 #U2 #HW12 #HU12 #H destruct - /3 width=5 by reqx_pair_refl, fqu_bind_dx, ex3_2_intro/ -| #p #I #G #L #W1 #U1 #Hb #X #H - elim (teqx_inv_pair1 … H) -H #W2 #U2 #HW12 #HU12 #H destruct - /3 width=5 by fqu_clear, ex3_2_intro/ -| #I #G #L #W1 #U1 #X #H - elim (teqx_inv_pair1 … H) -H #W2 #U2 #_ #HU12 #H destruct - /2 width=5 by fqu_flat_dx, ex3_2_intro/ -| #I #G #L #T1 #U1 #HTU1 #U2 #HU12 - elim (teqx_inv_lifts_sn … HU12 … HTU1) -U1 - /3 width=5 by fqu_drop, ex3_2_intro/ -] -qed-. - -lemma teqx_fqu_trans (b): - ∀G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂[b] ❪G2,L2,T1❫ → - ∀U2. U2 ≛ U1 → - ∃∃L,T2. ❪G1,L1,U2❫ ⬂[b] ❪G2,L,T2❫ & T2 ≛ T1 & L ≛[T1] L2. -#b #G1 #G2 #L1 #L2 #U1 #T1 #H12 #U2 #HU21 -elim (fqu_teqx_conf … H12 U2) -H12 -/3 width=5 by reqx_sym, teqx_sym, ex3_2_intro/ -qed-. - -(* Basic_2A1: uses: lleq_fqu_trans *) -lemma reqx_fqu_trans (b): - ∀G1,G2,L2,K2,T,U. ❪G1,L2,T❫ ⬂[b] ❪G2,K2,U❫ → - ∀L1. L1 ≛[T] L2 → - ∃∃K1,U0. ❪G1,L1,T❫ ⬂[b] ❪G2,K1,U0❫ & U0 ≛ U & K1 ≛[U] K2. -#b #G1 #G2 #L2 #K2 #T #U #H elim H -G1 -G2 -L2 -K2 -T -U -[ #I #G #L2 #V2 #L1 #H elim (reqx_inv_zero_pair_dx … H) -H - #K1 #V1 #HV1 #HV12 #H destruct - /3 width=7 by teqx_reqx_conf_sn, fqu_lref_O, ex3_2_intro/ -| * [ #p ] #I #G #L2 #V #T #L1 #H - [ elim (reqx_inv_bind … H) - | elim (reqx_inv_flat … H) - ] -H - /2 width=5 by fqu_pair_sn, ex3_2_intro/ -| #p #I #G #L2 #V #T #Hb #L1 #H elim (reqx_inv_bind … H) -H - /3 width=5 by fqu_bind_dx, ex3_2_intro/ -| #p #I #G #L2 #V #T #Hb #L1 #H elim (reqx_inv_bind_void … H) -H - /3 width=5 by fqu_clear, ex3_2_intro/ -| #I #G #L2 #V #T #L1 #H elim (reqx_inv_flat … H) -H - /2 width=5 by fqu_flat_dx, ex3_2_intro/ -| #I #G #L2 #T #U #HTU #Y #HU - elim (reqx_fwd_dx … HU) #L1 #V1 #H destruct - /5 width=14 by reqx_inv_lifts_bi, fqu_drop, drops_refl, drops_drop, ex3_2_intro/ -] -qed-. - -(* Properties with optional structural successor for closures ***************) - -lemma teqx_fquq_trans (b): - ∀G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂⸮[b] ❪G2,L2,T1❫ → - ∀U2. U2 ≛ U1 → - ∃∃L,T2. ❪G1,L1,U2❫ ⬂⸮[b] ❪G2,L,T2❫ & T2 ≛ T1 & L ≛[T1] L2. -#b #G1 #G2 #L1 #L2 #U1 #T1 #H elim H -H -[ #H #U2 #HU21 elim (teqx_fqu_trans … H … HU21) -U1 - /3 width=5 by fqu_fquq, ex3_2_intro/ -| * #HG #HL #HT destruct /2 width=5 by ex3_2_intro/ -] -qed-. - -(* Basic_2A1: was just: lleq_fquq_trans *) -lemma reqx_fquq_trans (b): - ∀G1,G2,L2,K2,T,U. ❪G1,L2,T❫ ⬂⸮[b] ❪G2,K2,U❫ → - ∀L1. L1 ≛[T] L2 → - ∃∃K1,U0. ❪G1,L1,T❫ ⬂⸮[b] ❪G2,K1,U0❫ & U0 ≛ U & K1 ≛[U] K2. -#b #G1 #G2 #L2 #K2 #T #U #H elim H -H -[ #H #L1 #HL12 elim (reqx_fqu_trans … H … HL12) -L2 /3 width=5 by fqu_fquq, ex3_2_intro/ -| * #HG #HL #HT destruct /2 width=5 by ex3_2_intro/ -] -qed-. - -(* Properties with plus-iterated structural successor for closures **********) - -(* Basic_2A1: was just: lleq_fqup_trans *) -lemma reqx_fqup_trans (b): - ∀G1,G2,L2,K2,T,U. ❪G1,L2,T❫ ⬂+[b] ❪G2,K2,U❫ → - ∀L1. L1 ≛[T] L2 → - ∃∃K1,U0. ❪G1,L1,T❫ ⬂+[b] ❪G2,K1,U0❫ & U0 ≛ U & K1 ≛[U] K2. -#b #G1 #G2 #L2 #K2 #T #U #H @(fqup_ind … H) -G2 -K2 -U -[ #G2 #K2 #U #HTU #L1 #HL12 elim (reqx_fqu_trans … HTU … HL12) -L2 - /3 width=5 by fqu_fqup, ex3_2_intro/ -| #G #G2 #K #K2 #U #U2 #_ #HU2 #IHTU #L1 #HL12 - elim (IHTU … HL12) -L2 #K0 #U0 #HTU #HU0 #HK0 - elim (reqx_fqu_trans … HU2 … HK0) -K #K1 #U1 #HU1 #HU12 #HK12 - elim (teqx_fqu_trans … HU1 … HU0) -U #K3 #U3 #HU03 #HU31 #HK31 - @(ex3_2_intro … K3 U3) (**) (* full auto too slow *) - /3 width=5 by reqx_trans, teqx_reqx_conf_sn, fqup_strap1, teqx_trans/ -] -qed-. - -lemma teqx_fqup_trans (b): - ∀G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂+[b] ❪G2,L2,T1❫ → - ∀U2. U2 ≛ U1 → - ∃∃L,T2. ❪G1,L1,U2❫ ⬂+[b] ❪G2,L,T2❫ & T2 ≛ T1 & L ≛[T1] L2. -#b #G1 #G2 #L1 #L2 #U1 #T1 #H @(fqup_ind_dx … H) -G1 -L1 -U1 -[ #G1 #L1 #U1 #H #U2 #HU21 elim (teqx_fqu_trans … H … HU21) -U1 - /3 width=5 by fqu_fqup, ex3_2_intro/ -| #G1 #G #L1 #L #U1 #U #H #_ #IH #U2 #HU21 - elim (teqx_fqu_trans … H … HU21) -U1 #L0 #T #H1 #HTU #HL0 - lapply (teqx_reqx_div … HTU … HL0) -HL0 #HL0 - elim (IH … HTU) -U #K2 #U1 #H2 #HUT1 #HKL2 - elim (reqx_fqup_trans … H2 … HL0) -L #K #U #H2 #HU1 #HK2 - lapply (teqx_reqx_conf_sn … HUT1 … HK2) -HK2 #HK2 - /3 width=7 by reqx_trans, fqup_strap2, teqx_trans, ex3_2_intro/ -] -qed-. - -(* Properties with star-iterated structural successor for closures **********) - -lemma teqx_fqus_trans (b): - ∀G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂*[b] ❪G2,L2,T1❫ → - ∀U2. U2 ≛ U1 → - ∃∃L,T2. ❪G1,L1,U2❫ ⬂*[b] ❪G2,L,T2❫ & T2 ≛ T1 & L ≛[T1] L2. -#b #G1 #G2 #L1 #L2 #U1 #T1 #H #U2 #HU21 elim(fqus_inv_fqup … H) -H -[ #H elim (teqx_fqup_trans … H … HU21) -U1 /3 width=5 by fqup_fqus, ex3_2_intro/ -| * #HG #HL #HT destruct /2 width=5 by ex3_2_intro/ -] -qed-. - -(* Basic_2A1: was just: lleq_fqus_trans *) -lemma reqx_fqus_trans (b): - ∀G1,G2,L2,K2,T,U. ❪G1,L2,T❫ ⬂*[b] ❪G2,K2,U❫ → - ∀L1. L1 ≛[T] L2 → - ∃∃K1,U0. ❪G1,L1,T❫ ⬂*[b] ❪G2,K1,U0❫ & U0 ≛ U & K1 ≛[U] K2. -#b #G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fqus_inv_fqup … H) -H -[ #H elim (reqx_fqup_trans … H … HL12) -L2 /3 width=5 by fqup_fqus, ex3_2_intro/ -| * #HG #HL #HT destruct /2 width=5 by ex3_2_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/etc/teqx/reqx_length.etc b/matita/matita/contribs/lambdadelta/static_2/etc/teqx/reqx_length.etc deleted file mode 100644 index dafdc4f57..000000000 --- a/matita/matita/contribs/lambdadelta/static_2/etc/teqx/reqx_length.etc +++ /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 "static_2/relocation/lifts_teqx.ma". -include "static_2/static/rex_length.ma". -include "static_2/static/rex_fsle.ma". -include "static_2/static/reqx.ma". - -(* SORT-IRRELEVANT EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ***) - -(* Advanved properties with free variables inclusion ************************) - -lemma reqx_fsge_comp: rex_fsge_compatible cdeq. -#L1 #L2 #T * #f1 #Hf1 #HL12 -lapply (frees_reqx_conf … Hf1 … HL12) -lapply (sex_fwd_length … HL12) -/3 width=8 by lveq_length_eq, ex4_4_intro/ (**) (* full auto fails *) -qed-. - -(* Properties with length for local environments ****************************) - -(* Basic_2A1: uses: lleq_sort *) -lemma reqx_sort_length: ∀L1,L2. |L1| = |L2| → ∀s. L1 ≛[⋆s] L2. -/2 width=1 by rex_sort_length/ qed. - -(* Basic_2A1: uses: lleq_gref *) -lemma reqx_gref_length: ∀L1,L2. |L1| = |L2| → ∀l. L1 ≛[§l] L2. -/2 width=1 by rex_gref_length/ qed. - -lemma reqx_unit_length: ∀L1,L2. |L1| = |L2| → - ∀I. L1.ⓤ[I] ≛[#0] L2.ⓤ[I]. -/2 width=1 by rex_unit_length/ qed. - -(* Basic_2A1: uses: lleq_lift_le lleq_lift_ge *) -lemma reqx_lifts_bi: ∀L1,L2. |L1| = |L2| → ∀K1,K2,T. K1 ≛[T] K2 → - ∀b,f. ⇩*[b,f] L1 ≘ K1 → ⇩*[b,f] L2 ≘ K2 → - ∀U. ⇧*[f] T ≘ U → L1 ≛[U] L2. -/3 width=9 by rex_lifts_bi, teqx_lifts_sn/ qed-. - -(* Forward lemmas with length for local environments ************************) - -(* Basic_2A1: lleq_fwd_length *) -lemma reqx_fwd_length: ∀L1,L2. ∀T:term. L1 ≛[T] L2 → |L1| = |L2|. -/2 width=3 by rex_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/static/feqx.ma b/matita/matita/contribs/lambdadelta/static_2/static/feqx.ma index 9804e73c2..055343f85 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/feqx.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/feqx.ma @@ -17,10 +17,7 @@ include "static_2/static/reqx.ma". include "static_2/static/feqg.ma". (* SORT-IRRELEVANT EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES *************) -(* -definition feqx: relation6 genv lenv term genv lenv term ≝ - feqg sfull. -*) + interpretation "sort-irrelevant equivalence on referred entries (closure)" 'ApproxEqSn G1 L1 T1 G2 L2 T2 = (feqg sfull G1 L1 T1 G2 L2 T2). -- 2.39.2