From a9e994f4ca8e04743c53ed8cb057ee5dae80c8f9 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 1 Feb 2017 19:52:07 +0000 Subject: [PATCH] - advances in rt_transition - bugs fixed and refactoring of some parked files --- .../{rt_transition => etc}/cpx_lreq.ma | 0 .../basic_2/etc/{ => cpy}/psubst_6.etc | 0 .../basic_2/etc/{ => cpys}/psubststar_6.etc | 0 .../etc/{ => cpys}/psubststaralt_6.etc | 0 .../{rt_transition => etc}/fpb_lift.ma | 0 .../{rt_transition => etc}/fpbq_lift.ma | 0 .../lambdadelta/basic_2/etc/lfpr_main.etc | 80 ------------ .../basic_2/etc/{ => lfxs}/lfxs.etc | 0 .../basic_2/etc/{ => lfxs}/lfxs_drops.etc | 0 .../basic_2/etc/{ => lfxs}/lfxs_fqup.etc | 0 .../basic_2/etc/{ => lfxs}/lfxs_length.etc | 0 .../basic_2/etc/{ => lfxs}/lfxs_lfxs.etc | 0 .../basic_2/etc/{ => lsuby}/lrsubeq_4.etc | 0 .../basic_2/etc/{ => ltls}/droppreds_3.etc | 0 .../basic_2/etc/{ => ltls}/ltls.etc | 0 .../basic_2/etc/{ => notation}/lazyor_5.etc | 0 .../notation.ma => etc/notation/notation.etc} | 0 .../ceq_ceq.etc => rt_transition/cpm_lfxs.ma} | 27 ++--- .../basic_2/rt_transition/cpr_llpx_sn.ma | 47 -------- .../lambdadelta/basic_2/rt_transition/cpx.ma | 31 +++++ .../basic_2/rt_transition/cpx_lfdeq.ma | 114 ++++++++++++++++++ .../ceq.etc => rt_transition/cpx_lfxs.ma} | 34 ++---- .../basic_2/rt_transition/cpx_lleq.ma | 55 --------- .../basic_2/rt_transition/cpx_llpx_sn.ma | 50 -------- .../lambdadelta/basic_2/rt_transition/fpb.ma | 23 ++-- .../basic_2/rt_transition/partial.txt | 5 +- .../lambdadelta/basic_2/static/ffdeq.ma | 2 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 17 +-- 28 files changed, 186 insertions(+), 299 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/{rt_transition => etc}/cpx_lreq.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{ => cpy}/psubst_6.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{ => cpys}/psubststar_6.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{ => cpys}/psubststaralt_6.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{rt_transition => etc}/fpb_lift.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{rt_transition => etc}/fpbq_lift.ma (100%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lfpr_main.etc rename matita/matita/contribs/lambdadelta/basic_2/etc/{ => lfxs}/lfxs.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{ => lfxs}/lfxs_drops.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{ => lfxs}/lfxs_fqup.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{ => lfxs}/lfxs_length.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{ => lfxs}/lfxs_lfxs.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{ => lsuby}/lrsubeq_4.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{ => ltls}/droppreds_3.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{ => ltls}/ltls.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{ => notation}/lazyor_5.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/notation.ma => etc/notation/notation.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/ceq_ceq.etc => rt_transition/cpm_lfxs.ma} (65%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_llpx_sn.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfdeq.ma rename matita/matita/contribs/lambdadelta/basic_2/{etc/ceq.etc => rt_transition/cpx_lfxs.ma} (59%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lleq.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_llpx_sn.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpx_lreq.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lreq.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpx_lreq.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/psubst_6.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/psubst_6.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/psubst_6.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpy/psubst_6.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/psubststar_6.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/psubststar_6.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/psubststar_6.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpys/psubststar_6.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/psubststaralt_6.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/psubststaralt_6.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/psubststaralt_6.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpys/psubststaralt_6.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/fpb_lift.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/fpb_lift.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbq_lift.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/fpbq_lift.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfpr_main.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfpr_main.etc deleted file mode 100644 index bfe23e721..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lfpr_main.etc +++ /dev/null @@ -1,80 +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/lfpr_lfpr.ma". - -(* PARALLEL R-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES ****************) - -definition lfxs_confluent_R: relation2 … ≝ - λRP1,RP2. - ∀L0,T0,T1. RP1 L0 T0 T1 → ∀T2. RP2 L0 T0 T2 → - ∀L1. L0 ⦻*[RP1, T0] L1 → ∀L2. L0 ⦻*[RP2, T0] L2 → - ∃∃L. L1 ⦻*[RP2, T1] L & L2 ⦻*[RP1, T2] L. - -(* Main properties **********************************************************) - -fact lfpr_conf_cpr_atom_atom: - ∀h,I,G,L0. ( - ∀L,T. ⦃G, L0, ⓪{I}⦄ ⊐+ ⦃G, L, T⦄ → - ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 → - ∀L1. ⦃G, L⦄ ⊢ ➡[h, T] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h, T] L2 → - ∃∃K0. ⦃G, L1⦄ ⊢ ➡[h, T1] K0 & ⦃G, L2⦄ ⊢ ➡[h, T2] K0 - ) → - ∀L1. ⦃G, L0⦄ ⊢ ➡[h, ⓪{I}] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h, ⓪{I}] L2 → - ∃∃L. ⦃G, L1⦄ ⊢ ➡[h, ⓪{I}] L & ⦃G, L2⦄ ⊢ ➡[h, ⓪{I}] L. -#h #I #G * [ | #K0 #J #V0 cases I -I [ | * | ] ] -[ #_ #L1 #HL01 #L2 #HL02 - lapply (lfpr_inv_atom_sn … HL01) -HL01 #H destruct - lapply (lfpr_inv_atom_sn … HL02) -HL02 #H destruct - /2 width=3 by ex2_intro/ -| #s #IH #L1 #HL01 #L2 #HL02 - elim (lfxs_inv_sort_pair_sn … HL01) -HL01 #K1 #V1 #HK01 #H destruct - elim (lfxs_inv_sort_pair_sn … HL02) -HL02 #K2 #V2 #HK02 #H destruct - elim (IH … HK01 … HK02) -IH -HK01 -HK02 - /3 width=5 by lfpr_sort, fqu_fqup, fqu_drop, ex2_intro/ -| #IH #L1 #HL01 #L2 #HL02 - elim (lfpr_inv_zero_pair_sn … HL01) -HL01 #K1 #V1 #HK01 #HV01 #H destruct - elim (lfpr_inv_zero_pair_sn … HL02) -HL02 #K2 #V2 #HK02 #HV02 #H destruct - elim (cpr_conf_lfpr … HV01 … HV02 … HK01 … HK02) #V #HV1 #HV2 - elim (IH … HV01 … HV02 … HK01 … HK02) -IH -HV01 -HV02 -HK01 -HK02 - /3 width=5 by lfpr_zero, fqu_fqup, fqu_drop, ex2_intro/ -| #i #IH #L1 #HL01 #L2 #HL02 - elim (lfxs_inv_lref_pair_sn … HL01) -HL01 #K1 #V1 #HK01 #H destruct - elim (lfxs_inv_lref_pair_sn … HL02) -HL02 #K2 #V2 #HK02 #H destruct - elim (IH … HK01 … HK02) -IH -HK01 -HK02 - /3 width=5 by lfpr_lref, fqu_fqup, fqu_drop, ex2_intro/ -| #l #IH #L1 #HL01 #L2 #HL02 - elim (lfxs_inv_gref_pair_sn … HL01) -HL01 #K1 #V1 #HK01 #H destruct - elim (lfxs_inv_gref_pair_sn … HL02) -HL02 #K2 #V2 #HK02 #H destruct - elim (IH … HK01 … HK02) -IH -HK01 -HK02 - /3 width=5 by lfpr_gref, fqu_fqup, fqu_drop, ex2_intro/ -] -qed-. - -theorem lfpr_conf_cpr: ∀h,G. lfxs_confluent_R (cpm 0 h G) (cpm 0 h G). -#h #G #L0 #T0 @(fqup_wf_ind_eq … G L0 T0) -G -L0 -T0 #G #L #T #IH #G0 #L0 * [| * ] -[ #I0 #HG #HL #HT #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct - elim (cpr_inv_atom1_drops … H1) -H1 - elim (cpr_inv_atom1_drops … H2) -H2 - [ #H2 #H1 destruct - /3 width=7 by lfpr_conf_cpr_atom_atom/ - | * #K0 #V0 #V2 * [2: #i2 ] #HLK0 #HV02 #HVT2 #H2 #H1 destruct - -(* - -theorem lpr_conf: ∀G. confluent … (lpr G). -/3 width=6 by lpx_sn_conf, cpr_conf_lpr/ -qed-. - -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lfxs.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_drops.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_drops.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_drops.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_drops.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_fqup.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_fqup.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_fqup.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_fqup.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_length.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_length.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_length.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_length.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_lfxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_lfxs.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_lfxs.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_lfxs.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lrsubeq_4.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lrsubeq_4.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lrsubeq_4.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lrsubeq_4.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/droppreds_3.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ltls/droppreds_3.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/droppreds_3.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/ltls/droppreds_3.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ltls.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ltls/ltls.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/ltls.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/ltls/ltls.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lazyor_5.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/notation/lazyor_5.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lazyor_5.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/notation/lazyor_5.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/notation/notation.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/notation.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/notation/notation.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ceq_ceq.etc b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lfxs.ma similarity index 65% rename from matita/matita/contribs/lambdadelta/basic_2/etc/ceq_ceq.etc rename to matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lfxs.ma index b17b186e2..4ce37d910 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/ceq_ceq.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lfxs.ma @@ -12,26 +12,13 @@ (* *) (**************************************************************************) -include "basic_2/syntax/ceq.ma". +include "basic_2/rt_transition/cpx_lfxs.ma". +include "basic_2/rt_transition/cpm_cpx.ma". -(* CONTEXT-SENSITIVE EQUIVALENCES FOR TERMS *********************************) +(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************) -(* Main properties **********************************************************) +(* Properties with generic extension on referred entries ********************) -theorem ceq_trans (L): Transitive … (ceq L). -// qed-. - -lemma ceq_canc_sn (L): left_cancellable … (ceq L). -// qed-. - -lemma ceq_canc_dx (L): right_cancellable … (ceq L). -// qed-. - -theorem cfull_trans (L): Transitive … (cfull L). -// qed-. - -lemma cfull_canc_sn (L): left_cancellable … (cfull L). -// qed-. - -lemma cfull_canc_dx (L): right_cancellable … (cfull L). -// qed-. \ No newline at end of file +(* Basic_2A1: was just: cpr_llpx_sn_conf *) +lemma cpm_lfxs_conf: ∀R,n,h,G. s_r_confluent1 … (cpm n h G) (lfxs R). +/3 width=5 by cpm_fwd_cpx, cpx_lfxs_conf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_llpx_sn.ma deleted file mode 100644 index 8395d7501..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_llpx_sn.ma +++ /dev/null @@ -1,47 +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/multiple/llpx_sn_drop.ma". -include "basic_2/reduction/cpr.ma". - -(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************) - -(* Properties on lazy sn pointwise extensions *******************************) - -lemma cpr_llpx_sn_conf: ∀R. (∀L. reflexive … (R L)) → d_liftable R → d_deliftable_sn R → - ∀G. b_c_confluent1 … (cpr G) (llpx_sn R 0). -#R #H1R #H2R #H3R #G #Ls #T1 #T2 #H elim H -G -Ls -T1 -T2 -[ // -| #G #Ls #Ks #V1b #V2b #W2b #i #HLKs #_ #HVW2b #IHV12b #Ld #H elim (llpx_sn_inv_lref_ge_sn … H … HLKs) // -H - #Kd #V1l #HLKd #HV1b #HV1sd - lapply (drop_fwd_drop2 … HLKs) -HLKs #HLKs - lapply (drop_fwd_drop2 … HLKd) -HLKd #HLKd - @(llpx_sn_lift_le … HLKs HLKd … HVW2b) -HLKs -HLKd -HVW2b /2 width=1 by/ (**) (* full auto too slow *) -| #a #I #G #Ls #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H - /4 width=5 by llpx_sn_bind_repl_SO, llpx_sn_bind/ -| #I #G #Ls #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H - /3 width=1 by llpx_sn_flat/ -| #G #Ls #V #T1 #T2 #T #_ #HT2 #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H - /3 width=10 by llpx_sn_inv_lift_le, drop_drop/ -| #G #Ls #V #T1 #T2 #_ #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H /2 width=1 by/ -| #a #G #Ls #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H - #HV1 #H elim (llpx_sn_inv_bind_O … H) -H - /4 width=5 by llpx_sn_bind_repl_SO, llpx_sn_flat, llpx_sn_bind/ -| #a #G #Ls #V1 #V2 #V #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H - #HV1 #H elim (llpx_sn_inv_bind_O … H) -H // - #HW1 #HT1 @llpx_sn_bind_O /2 width=1 by/ @llpx_sn_flat (**) (* full auto too slow *) - [ /3 width=10 by llpx_sn_lift_le, drop_drop/ - | /3 width=4 by llpx_sn_bind_repl_O/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma index 7d20bc47f..0241664db 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma @@ -230,3 +230,34 @@ lemma cpx_fwd_bind1_minus: ∀h,I,G,L,V1,T1,T. ⦃G, L⦄ ⊢ -ⓑ{I}V1.T1 ⬈[h #h #I #G #L #V1 #T1 #T * #c #H #p elim (cpg_fwd_bind1_minus … H p) -H /3 width=4 by ex2_2_intro, ex_intro/ qed-. + +(* Basic eliminators ********************************************************) + +lemma cpx_ind: ∀h. ∀R:relation4 genv lenv term term. + (∀I,G,L. R G L (⓪{I}) (⓪{I})) → + (∀G,L,s. R G L (⋆s) (⋆(next h s))) → + (∀I,G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ⬈[h] V2 → R G K V1 V2 → + ⬆*[1] V2 ≡ W2 → R G (K.ⓑ{I}V1) (#0) W2 + ) → (∀I,G,K,V,T,U,i. ⦃G, K⦄ ⊢ #i ⬈[h] T → R G K (#i) T → + ⬆*[1] T ≡ U → R G (K.ⓑ{I}V) (#⫯i) (U) + ) → (∀p,I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[h] T2 → + R G L V1 V2 → R G (L.ⓑ{I}V1) T1 T2 → R G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2) + ) → (∀I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → + R G L V1 V2 → R G L T1 T2 → R G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) + ) → (∀G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ⬈[h] T → R G (L.ⓓV) T1 T → + ⬆*[1] T2 ≡ T → R G L (+ⓓV.T1) T2 + ) → (∀G,L,V,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → R G L T1 T2 → + R G L (ⓝV.T1) T2 + ) → (∀G,L,V1,V2,T. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → R G L V1 V2 → + R G L (ⓝV1.T) V2 + ) → (∀p,G,L,V1,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L⦄ ⊢ W1 ⬈[h] W2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈[h] T2 → + R G L V1 V2 → R G L W1 W2 → R G (L.ⓛW1) T1 T2 → + R G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2) + ) → (∀p,G,L,V1,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V → ⦃G, L⦄ ⊢ W1 ⬈[h] W2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈[h] T2 → + R G L V1 V → R G L W1 W2 → R G (L.ⓓW1) T1 T2 → + ⬆*[1] V ≡ V2 → R G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2) + ) → + ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → R G L T1 T2. +#h #R #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #IH10 #IH11 #G #L #T1 #T2 +* #c #H elim H -c -G -L -T1 -T2 /3 width=4 by ex_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfdeq.ma new file mode 100644 index 000000000..1a4d722e7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfdeq.ma @@ -0,0 +1,114 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lifts_tdeq.ma". +include "basic_2/static/lfdeq.ma". +include "basic_2/rt_transition/lfpx.ma". + +(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************) + +(* Properties with degree-based equivalence for terms ***********************) + +(* Basic_2A1: was just: cpx_lleq_conf *) +lemma cpx_tdeq_conf_lexs: ∀h,o,G. R_confluent2_lfxs … (cpx h G) (cdeq h o) (cpx h G) (cdeq h o). +#h #o #G #L0 #T0 #T1 #H @(cpx_ind … H) -G -L0 -T0 -T1 /2 width=3 by ex2_intro/ +[ #G #L0 #s0 #X0 #H0 #L1 #HL01 #L2 #HL02 + elim (tdeq_inv_sort1 … H0) -H0 #s1 #d1 #Hs0 #Hs1 #H destruct + /4 width=3 by tdeq_sort, deg_next, ex2_intro/ +| #I #G #K0 #V0 #V1 #W1 #_ #IH #HVW1 #T2 #H0 #L1 #H1 #L2 #H2 + >(tdeq_inv_lref1 … H0) -H0 + elim (lfpx_inv_zero_pair_sn … H1) -H1 #K1 #X1 #HK01 #HX1 #H destruct + elim (lfdeq_inv_zero_pair_sn … H2) -H2 #K2 #X2 #HK02 #HX2 #H destruct + elim (IH X2 … HK01 … HK02) // -K0 -V0 #V #HV1 #HV2 + elim (tdeq_lifts … HV1 … HVW1) -V1 /3 width=5 by cpx_delta, ex2_intro/ +| #I #G #K0 #V0 #V1 #W1 #i #_ #IH #HVW1 #T2 #H0 #L1 #H1 #L2 #H2 + >(tdeq_inv_lref1 … H0) -H0 + elim (lfpx_inv_lref_pair_sn … H1) -H1 #K1 #X1 #HK01 #H destruct + elim (lfdeq_inv_lref_pair_sn … H2) -H2 #K2 #X2 #HK02 #H destruct + elim (IH … HK01 … HK02) [|*: //] -K0 -V0 #V #HV1 #HV2 + elim (tdeq_lifts … HV1 … HVW1) -V1 /3 width=5 by cpx_lref, ex2_intro/ +| #p #I #G #L0 #V0 #V1 #T0 #T1 #_ #_ #IHV #IHT #X0 #H0 #L1 #H1 #L2 #H2 + elim (tdeq_inv_pair1 … H0) -H0 #V2 #T2 #HV02 #HT02 #H destruct + elim (lfpx_inv_bind … H1) -H1 #HL01 #H1 + elim (lfdeq_inv_bind … H2) -H2 #HL02 #H2 + lapply (lfdeq_pair_repl_dx … H2 … HV02) -H2 #H2 + elim (IHV … HV02 … HL01 … HL02) -IHV -HV02 -HL01 -HL02 + elim (IHT … HT02 … H1 … H2) -L0 -T0 + /3 width=5 by cpx_bind, tdeq_pair, ex2_intro/ +| #I #G #L0 #V0 #V1 #T0 #T1 #_ #_ #IHV #IHT #X0 #H0 #L1 #H1 #L2 #H2 + elim (tdeq_inv_pair1 … H0) -H0 #V2 #T2 #HV02 #HT02 #H destruct + elim (lfpx_inv_flat … H1) -H1 #HL01 #H1 + elim (lfdeq_inv_flat … H2) -H2 #HL02 #H2 + elim (IHV … HV02 … HL01 … HL02) -IHV -HV02 -HL01 -HL02 + elim (IHT … HT02 … H1 … H2) -L0 -V0 -T0 + /3 width=5 by cpx_flat, tdeq_pair, ex2_intro/ +| #G #L0 #V0 #T0 #T1 #U1 #_ #IH #HUT1 #X0 #H0 #L1 #H1 #L2 #H2 + elim (tdeq_inv_pair1 … H0) -H0 #V2 #T2 #HV02 #HT02 #H destruct + elim (lfpx_inv_bind … H1) -H1 #HL01 #H1 + elim (lfdeq_inv_bind … H2) -H2 #HL02 #H2 + lapply (lfdeq_pair_repl_dx … H2 … HV02) -H2 -HV02 #H2 + elim (IH … HT02 … H1 … H2) -L0 -T0 #T #HT1 + elim (tdeq_inv_lifts … HT1 … HUT1) -T1 + /3 width=5 by cpx_zeta, ex2_intro/ +| #G #L0 #V0 #T0 #T1 #_ #IH #X0 #H0 #L1 #H1 #L2 #H2 + elim (tdeq_inv_pair1 … H0) -H0 #V2 #T2 #_ #HT02 #H destruct + elim (lfpx_inv_flat … H1) -H1 #HL01 #H1 + elim (lfdeq_inv_flat … H2) -H2 #HL02 #H2 + elim (IH … HT02 … H1 … H2) -L0 -V0 -T0 + /3 width=3 by cpx_eps, ex2_intro/ +| #G #L0 #V0 #T0 #T1 #_ #IH #X0 #H0 #L1 #H1 #L2 #H2 + elim (tdeq_inv_pair1 … H0) -H0 #V2 #T2 #HV02 #_ #H destruct + elim (lfpx_inv_flat … H1) -H1 #HL01 #H1 + elim (lfdeq_inv_flat … H2) -H2 #HL02 #H2 + elim (IH … HV02 … HL01 … HL02) -L0 -V0 -T1 + /3 width=3 by cpx_ee, ex2_intro/ +| #p #G #L0 #V0 #V1 #W0 #W1 #T0 #T1 #_ #_ #_ #IHV #IHW #IHT #X0 #H0 #L1 #H1 #L2 #H2 + elim (tdeq_inv_pair1 … H0) -H0 #V2 #X #HV02 #H0 #H destruct + elim (tdeq_inv_pair1 … H0) -H0 #W2 #T2 #HW02 #HT02 #H destruct + elim (lfpx_inv_flat … H1) -H1 #H1LV0 #H1 + elim (lfpx_inv_bind … H1) -H1 #H1LW0 #H1LT0 + elim (lfdeq_inv_flat … H2) -H2 #H2LV0 #H2 + elim (lfdeq_inv_bind … H2) -H2 #H2LW0 #H2LT0 + lapply (lfdeq_pair_repl_dx … H2LT0 … HW02) -H2LT0 #H2LT0 + elim (IHV … HV02 … H1LV0 … H2LV0) -IHV -HV02 -H1LV0 -H2LV0 + elim (IHW … HW02 … H1LW0 … H2LW0) -IHW -HW02 -H1LW0 -H2LW0 + elim (IHT … HT02 … H1LT0 … H2LT0) -L0 -V0 -T0 + /4 width=7 by cpx_beta, tdeq_pair, ex2_intro/ (* note: 2 tdeq_pair *) +| #p #G #L0 #V0 #V1 #U1 #W0 #W1 #T0 #T1 #_ #_ #_ #IHV #IHW #IHT #HVU1 #X0 #H0 #L1 #H1 #L2 #H2 + elim (tdeq_inv_pair1 … H0) -H0 #V2 #X #HV02 #H0 #H destruct + elim (tdeq_inv_pair1 … H0) -H0 #W2 #T2 #HW02 #HT02 #H destruct + elim (lfpx_inv_flat … H1) -H1 #H1LV0 #H1 + elim (lfpx_inv_bind … H1) -H1 #H1LW0 #H1LT0 + elim (lfdeq_inv_flat … H2) -H2 #H2LV0 #H2 + elim (lfdeq_inv_bind … H2) -H2 #H2LW0 #H2LT0 + lapply (lfdeq_pair_repl_dx … H2LT0 … HW02) -H2LT0 #H2LT0 + elim (IHV … HV02 … H1LV0 … H2LV0) -IHV -HV02 -H1LV0 -H2LV0 #V #HV1 + elim (IHW … HW02 … H1LW0 … H2LW0) -IHW -HW02 -H1LW0 -H2LW0 + elim (IHT … HT02 … H1LT0 … H2LT0) -L0 -V0 -T0 + elim (tdeq_lifts … HV1 … HVU1) -V1 + /4 width=9 by cpx_theta, tdeq_pair, ex2_intro/ (* note: 2 tdeq_pair *) +] +qed-. +(* +lemma cpx_lleq_conf: ∀h,o,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ⬈[h, o] T2 → + ∀L1. L2 ≡[T1, 0] L1 → ⦃G, L1⦄ ⊢ T1 ⬈[h, o] T2. +/3 width=3 by lleq_cpx_trans, lleq_sym/ qed-. + +lemma cpx_lleq_conf_sn: ∀h,o,G. s_r_confluent1 … (cpx h o G) (lleq 0). +/3 width=6 by cpx_llpx_sn_conf, lift_mono, ex2_intro/ qed-. + +lemma cpx_lleq_conf_dx: ∀h,o,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ⬈[h, o] T2 → + ∀L1. L1 ≡[T1, 0] L2 → L1 ≡[T2, 0] L2. +/4 width=6 by cpx_lleq_conf_sn, lleq_sym/ qed-. +*) \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ceq.etc b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfxs.ma similarity index 59% rename from matita/matita/contribs/lambdadelta/basic_2/etc/ceq.etc rename to matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfxs.ma index 57ecbaf68..b47cd88bf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/ceq.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfxs.ma @@ -12,31 +12,15 @@ (* *) (**************************************************************************) -include "basic_2/syntax/lenv.ma". +include "basic_2/rt_transition/lfpx_frees.ma". -(* CONTEXT-SENSITIVE EQUIVALENCES FOR TERMS *********************************) +(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************) -definition ceq: relation3 lenv term term ≝ λL,T1,T2. T1 = T2. +(* Properties with generic extension on referred entries ********************) -definition cfull: relation3 lenv term term ≝ λL,T1,T2. ⊤. - -(* Basic properties *********************************************************) - -lemma ceq_refl (L): reflexive … (ceq L). -// qed. - -lemma cfull_refl (L): reflexive … (cfull L). -// qed. - -lemma ceq_sym (L): symmetric … (ceq L). -// qed-. - -lemma cfull_sym (L): symmetric … (cfull L). -// qed-. - -lemma cfull_top (R:relation3 lenv term term) (L) (T1) (T2): - R L T1 T2 → cfull L T1 T2. -// qed-. - -lemma ceq_cfull (L) (T1) (T2): ceq L T1 T2 → cfull L T1 T2. -// qed. +(* Note: lemma 1000 *) +(* Basic_2A1: was just: cpx_llpx_sn_conf *) +lemma cpx_lfxs_conf: ∀R,h,G. s_r_confluent1 … (cpx h G) (lfxs R). +#R #h #G #L1 #T1 #T2 #H #L2 * #f1 #Hf1 elim (cpx_frees_conf … Hf1 … H) -T1 +/3 width=5 by sle_lexs_trans, ex2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lleq.ma deleted file mode 100644 index 946975957..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lleq.ma +++ /dev/null @@ -1,55 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/multiple/lleq_drop.ma". -include "basic_2/reduction/cpx_llpx_sn.ma". - -(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************) - -(* Properties on lazy equivalence for local environments ********************) - -lemma lleq_cpx_trans: ∀h,o,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ⬈[h, o] T2 → - ∀L1. L1 ≡[T1, 0] L2 → ⦃G, L1⦄ ⊢ T1 ⬈[h, o] T2. -#h #o #G #L2 #T1 #T2 #H elim H -G -L2 -T1 -T2 /2 width=2 by cpx_st/ -[ #I #G #L2 #K2 #V1 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV12 #L1 #H elim (lleq_fwd_lref_dx … H … HLK2) -L2 - [ #H elim (ylt_yle_false … H) // - | * /3 width=7 by cpx_delta/ - ] -| #a #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H elim (lleq_inv_bind_O … H) -H - /3 width=1 by cpx_bind/ -| #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H - /3 width=1 by cpx_flat/ -| #G #L2 #V2 #T1 #T #T2 #_ #HT2 #IHT1 #L1 #H elim (lleq_inv_bind_O … H) -H - /3 width=3 by cpx_zeta/ -| #G #L2 #W1 #T1 #T2 #_ #IHT12 #L1 #H elim (lleq_inv_flat … H) -H - /3 width=1 by cpx_eps/ -| #G #L2 #W1 #W2 #T1 #_ #IHW12 #L1 #H elim (lleq_inv_flat … H) -H - /3 width=1 by cpx_ct/ -| #a #G #L1 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H - #HV1 #H elim (lleq_inv_bind_O … H) -H /3 width=1 by cpx_beta/ -| #a #G #L1 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H - #HV1 #H elim (lleq_inv_bind_O … H) -H /3 width=3 by cpx_theta/ -] -qed-. - -lemma cpx_lleq_conf: ∀h,o,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ⬈[h, o] T2 → - ∀L1. L2 ≡[T1, 0] L1 → ⦃G, L1⦄ ⊢ T1 ⬈[h, o] T2. -/3 width=3 by lleq_cpx_trans, lleq_sym/ qed-. - -lemma cpx_lleq_conf_sn: ∀h,o,G. b_c_confluent1 … (cpx h o G) (lleq 0). -/3 width=6 by cpx_llpx_sn_conf, lift_mono, ex2_intro/ qed-. - -lemma cpx_lleq_conf_dx: ∀h,o,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ⬈[h, o] T2 → - ∀L1. L1 ≡[T1, 0] L2 → L1 ≡[T2, 0] L2. -/4 width=6 by cpx_lleq_conf_sn, lleq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_llpx_sn.ma deleted file mode 100644 index ec6255dfc..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_llpx_sn.ma +++ /dev/null @@ -1,50 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/multiple/llpx_sn_drop.ma". -include "basic_2/reduction/cpx.ma". - -(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************) - -(* Properties on lazy sn pointwise extensions *******************************) - -(* Note: lemma 1000 *) -lemma cpx_llpx_sn_conf: ∀R. (∀L. reflexive … (R L)) → d_liftable R → d_deliftable_sn R → - ∀h,o,G. b_c_confluent1 … (cpx h o G) (llpx_sn R 0). -#R #H1R #H2R #H3R #h #o #G #Ls #T1 #T2 #H elim H -G -Ls -T1 -T2 -[ // -| /3 width=4 by llpx_sn_fwd_length, llpx_sn_sort/ -| #I #G #Ls #Ks #V1b #V2b #W2b #i #HLKs #_ #HVW2b #IHV12b #Ld #H elim (llpx_sn_inv_lref_ge_sn … H … HLKs) // -H - #Kd #V1l #HLKd #HV1b #HV1sd - lapply (drop_fwd_drop2 … HLKs) -HLKs #HLKs - lapply (drop_fwd_drop2 … HLKd) -HLKd #HLKd - @(llpx_sn_lift_le … HLKs HLKd … HVW2b) -HLKs -HLKd -HVW2b /2 width=1 by/ (**) (* full auto too slow *) -| #a #I #G #Ls #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H - /4 width=5 by llpx_sn_bind_repl_SO, llpx_sn_bind/ -| #I #G #Ls #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H - /3 width=1 by llpx_sn_flat/ -| #G #Ls #V #T1 #T2 #T #_ #HT2 #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H - /3 width=10 by llpx_sn_inv_lift_le, drop_drop/ -| #G #Ls #V #T1 #T2 #_ #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H /2 width=1 by/ -| #G #Ls #V1 #V2 #T #_ #IHV12 #Ld #H elim (llpx_sn_inv_flat … H) -H /2 width=1 by/ -| #a #G #Ls #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H - #HV1 #H elim (llpx_sn_inv_bind_O … H) -H - /4 width=5 by llpx_sn_bind_repl_SO, llpx_sn_flat, llpx_sn_bind/ -| #a #G #Ls #V1 #V2 #V #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H - #HV1 #H elim (llpx_sn_inv_bind_O … H) -H // - #HW1 #HT1 @llpx_sn_bind_O /2 width=1 by/ @llpx_sn_flat (**) (* full auto too slow *) - [ /3 width=10 by llpx_sn_lift_le, drop_drop/ - | /3 width=4 by llpx_sn_bind_repl_O/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb.ma index cce7d39ff..f0e7362b2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb.ma @@ -13,28 +13,29 @@ (**************************************************************************) include "basic_2/notation/relations/btpredproper_8.ma". -include "basic_2/substitution/fqu.ma". -include "basic_2/multiple/lleq.ma". -include "basic_2/reduction/lpx.ma". +include "basic_2/s_transition/fqu.ma". +include "basic_2/static/lfdeq.ma". +include "basic_2/rt_transition/lfpr_lfpx.ma". -(* "RST" PROPER PARALLEL COMPUTATION FOR CLOSURES ***************************) +(* PROPER PARALLEL RST-TRANSITION FOR CLOSURES ******************************) inductive fpb (h) (o) (G1) (L1) (T1): relation3 genv lenv term ≝ | fpb_fqu: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → fpb h o G1 L1 T1 G2 L2 T2 -| fpb_cpx: ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡[h, o] T2 → (T1 = T2 → ⊥) → fpb h o G1 L1 T1 G1 L1 T2 -| fpb_lpx: ∀L2. ⦃G1, L1⦄ ⊢ ➡[h, o] L2 → (L1 ≡[T1, 0] L2 → ⊥) → fpb h o G1 L1 T1 G1 L2 T1 +| fpb_cpx: ∀T2. ⦃G1, L1⦄ ⊢ T1 ⬈[h] T2 → (T1 ≡[h, o] T2 → ⊥) → fpb h o G1 L1 T1 G1 L1 T2 +| fpb_lpx: ∀L2. ⦃G1, L1⦄ ⊢ ⬈[h, T1] L2 → (L1 ≡[h, o, T1] L2 → ⊥) → fpb h o G1 L1 T1 G1 L2 T1 . interpretation - "'rst' proper parallel reduction (closure)" + "proper parallel rst-transition (closure)" 'BTPRedProper h o G1 L1 T1 G2 L2 T2 = (fpb h o G1 L1 T1 G2 L2 T2). (* Basic properties *********************************************************) -lemma cpr_fpb: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → +(* Basic_2A1: includes: cpr_fpb *) +lemma cpm_fpb: ∀n,h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 → (T1 ≡[h, o] T2 → ⊥) → ⦃G, L, T1⦄ ≻[h, o] ⦃G, L, T2⦄. -/3 width=1 by fpb_cpx, cpr_cpx/ qed. +/3 width=2 by fpb_cpx, cpm_fwd_cpx/ qed. -lemma lpr_fpb: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡ L2 → (L1 ≡[T, 0] L2 → ⊥) → +lemma lpr_fpb: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡[h, T] L2 → (L1 ≡[h, o, T] L2 → ⊥) → ⦃G, L1, T⦄ ≻[h, o] ⦃G, L2, T⦄. -/3 width=1 by fpb_lpx, lpr_lpx/ qed. +/3 width=1 by fpb_lpx, lfpr_fwd_lfpx/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt index f2ca8d42a..d00ba2bea 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt @@ -1,6 +1,7 @@ cpg.ma cpg_simple.ma cpg_drops.ma cpg_lsubr.ma -cpx.ma cpx_simple.ma cpx_drops.ma cpx_fqus.ma cpx_lsubr.ma +cpx.ma cpx_simple.ma cpx_drops.ma cpx_fqus.ma cpx_lsubr.ma cpx_lfxs.ma cpx_lfdeq.ma lfpx.ma lfpx_length.ma lfpx_drops.ma lfpx_fqup.ma lfpx_frees.ma lfpx_aaa.ma -cpm.ma cpm_simple.ma cpm_drops.ma cpm_lsubr.ma cpm_cpx.ma +cpm.ma cpm_simple.ma cpm_drops.ma cpm_lsubr.ma cpm_lfxs.ma cpm_cpx.ma cpr.ma cpr_drops.ma lfpr.ma lfpr_length.ma lfpr_drops.ma lfpr_fqup.ma lfpr_frees.ma lfpr_aaa.ma lfpr_lfpx.ma lfpr_lfpr.ma +fpb.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq.ma index 207e1e2d3..a5c11db63 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq.ma @@ -14,7 +14,7 @@ include "basic_2/notation/relations/lazyeq_8.ma". include "basic_2/syntax/genv.ma". -include "basic_2/static/lfdeq_fqup.ma". +include "basic_2/static/lfdeq.ma". (* DEGREE-BASED EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES ****************) 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 d98e42c5c..e920f2c0d 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 @@ -131,27 +131,27 @@ table { *) class "water" [ { "rt-transition" * } { -(* - [ { "parallel qrst-reduction" * } { - [ "fpbq ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "fpbq_alt ( ⦃?,?,?⦄ ≽≽[?,?] ⦃?,?,?⦄ )" "fpbq_lift" + "fpbq_aaa" * ] - [ "fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpb_lift" + "fpb_lleq" + "fpb_fleq" * ] + [ { "parallel qrst-rtransition" * } { +(* [ "fpbq ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "fpbq_alt ( ⦃?,?,?⦄ ≽≽[?,?] ⦃?,?,?⦄ )" + "fpbq_aaa" * ] *) + [ "fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" (* "fpb_lleq" + "fpb_fleq" *) * ] } ] +(* [ { "context-sensitive rt-reduction" * } { [ "lpx_lleq" * ] - [ "cpx_lreq" + "cpx_llpx_sn" + "cpx_lleq" * ] + [ "cpx_lleq" * ] } ] *) [ { "t-bound context-sensitive rt-transition" * } { [ "lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lfpr_length" + "lfpr_drops" + "lfpr_fqup" + "lfpr_frees" + "lfpr_aaa" + "lfpr_lfpx" + "lfpr_lfpr" * ] - [ "cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" (* + "cpr_llpx_sn" + "cpr_cir" *) * ] - [ "cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_drops" + "cpm_lsubr" + "cpm_cpx" * ] + [ "cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" * ] + [ "cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_drops" + "cpm_lsubr" + "cpm_lfxs" + "cpm_cpx" * ] } ] [ { "uncounted context-sensitive rt-transition" * } { [ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_aaa" * ] - [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" * ] + [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfxs" + "cpx_lfdeq" * ] } ] [ { "counted context-sensitive rt-transition" * } { @@ -360,5 +360,6 @@ class "italic" { 1 } [ "lpx_sn" "lpx_sn_alt" + "lpx_sn_tc" + "lpx_sn_drop" + "lpx_sn_lpx_sn" * ] } ] + [ "cpx_lreq" + "cpr_cir" + "fpb_lift" + "fpbq_lift" ] [ "lleq ( ? ≡[?,?] ? )" "lleq_alt" + "lleq_alt_rec" + "lleq_lreq" + "lleq_drop" + "lleq_fqus" + "lleq_llor" + "lleq_lleq" * ] *) -- 2.39.2