From 6d1c6a2cfdd1909647db5648b9cd059c61b19b40 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 16 Mar 2017 16:19:05 +0000 Subject: [PATCH] - more commutations with superclosure: fpb_lfdeq - lfpx_lfdeq_conf, whose proof is much simplified w.r.t. basic_2A1 --- .../basic_2/etc/lleq/lleq_drop.etc | 29 ----- .../basic_2/etc/lleq/lleq_fqus.etc | 75 ------------ .../{fpb_lleq.ma => fpb_lfdeq.ma} | 30 ++--- .../basic_2/rt_transition/lfpx_lfdeq.ma | 14 +-- .../basic_2/rt_transition/partial.txt | 2 +- .../lambdadelta/basic_2/static/lfdeq.ma | 16 +++ .../lambdadelta/basic_2/static/lfdeq_drops.ma | 49 ++++++++ .../lambdadelta/basic_2/static/lfdeq_fqup.ma | 4 + .../lambdadelta/basic_2/static/lfdeq_fqus.ma | 109 ++++++++++++++++++ .../lambdadelta/basic_2/static/lfxs.ma | 7 ++ .../lambdadelta/basic_2/static/lfxs_drops.ma | 6 +- .../lambdadelta/basic_2/static/lfxs_lfxs.ma | 16 +-- .../lambdadelta/basic_2/web/basic_2_src.tbl | 6 +- 13 files changed, 223 insertions(+), 140 deletions(-) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq_fqus.etc rename matita/matita/contribs/lambdadelta/basic_2/rt_transition/{fpb_lleq.ma => fpb_lfdeq.ma} (51%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_drops.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqus.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq_drop.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq_drop.etc index aa4fa9e8c..87ceaf096 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq_drop.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq_drop.etc @@ -106,35 +106,6 @@ lemma lleq_fwd_bind_O_dx: ∀a,I,L1,L2,V,T. L1 ≡[ⓑ{a,I}V.T, 0] L2 → L1.ⓑ{I}V ≡[T, 0] L2.ⓑ{I}V. /2 width=2 by llpx_sn_fwd_bind_O_dx/ qed-. -(* Properties on relocation *************************************************) - -lemma lleq_lift_le: ∀K1,K2,T,lt. K1 ≡[T, lt] K2 → - ∀L1,L2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 → - ∀U. ⬆[l, k] T ≡ U → lt ≤ l → L1 ≡[U, lt] L2. -/3 width=10 by llpx_sn_lift_le, lift_mono/ qed-. - -lemma lleq_lift_ge: ∀K1,K2,T,lt. K1 ≡[T, lt] K2 → - ∀L1,L2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 → - ∀U. ⬆[l, k] T ≡ U → l ≤ lt → L1 ≡[U, lt+k] L2. -/2 width=9 by llpx_sn_lift_ge/ qed-. - -(* Inversion lemmas on relocation *******************************************) - -lemma lleq_inv_lift_le: ∀L1,L2,U,lt. L1 ≡[U, lt] L2 → - ∀K1,K2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 → - ∀T. ⬆[l, k] T ≡ U → lt ≤ l → K1 ≡[T, lt] K2. -/3 width=10 by llpx_sn_inv_lift_le, ex2_intro/ qed-. - -lemma lleq_inv_lift_be: ∀L1,L2,U,lt. L1 ≡[U, lt] L2 → - ∀K1,K2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 → - ∀T. ⬆[l, k] T ≡ U → l ≤ lt → lt ≤ l + k → K1 ≡[T, l] K2. -/2 width=11 by llpx_sn_inv_lift_be/ qed-. - -lemma lleq_inv_lift_ge: ∀L1,L2,U,lt. L1 ≡[U, lt] L2 → - ∀K1,K2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 → - ∀T. ⬆[l, k] T ≡ U → l + k ≤ lt → K1 ≡[T, lt-k] K2. -/2 width=9 by llpx_sn_inv_lift_ge/ qed-. - (* Inversion lemmas on negated lazy quivalence for local environments *******) lemma nlleq_inv_bind: ∀a,I,L1,L2,V,T,l. (L1 ≡[ⓑ{a,I}V.T, l] L2 → ⊥) → diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq_fqus.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq_fqus.etc deleted file mode 100644 index bf0cec6d2..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq_fqus.etc +++ /dev/null @@ -1,75 +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/fqus_alt.ma". -include "basic_2/multiple/lleq_drop.ma". - -(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) - -(* Properties on supclosure *************************************************) - -lemma lleq_fqu_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐ ⦃G2, K2, U⦄ → - ∀L1. L1 ≡[T, 0] L2 → - ∃∃K1. ⦃G1, L1, T⦄ ⊐ ⦃G2, K1, U⦄ & K1 ≡[U, 0] K2. -#G1 #G2 #L2 #K2 #T #U #H elim H -G1 -G2 -L2 -K2 -T -U -[ #I #G #L2 #V #L1 #H elim (lleq_inv_lref_ge_dx … H … I L2 V) -H // - #K1 #H1 #H2 lapply (drop_inv_O2 … H1) -H1 - #H destruct /2 width=3 by fqu_lref_O, ex2_intro/ -| * [ #a ] #I #G #L2 #V #T #L1 #H - [ elim (lleq_inv_bind … H) - | elim (lleq_inv_flat … H) - ] -H - /2 width=3 by fqu_pair_sn, ex2_intro/ -| #a #I #G #L2 #V #T #L1 #H elim (lleq_inv_bind_O … H) -H - #H3 #H4 /2 width=3 by fqu_bind_dx, ex2_intro/ -| #I #G #L2 #V #T #L1 #H elim (lleq_inv_flat … H) -H - /2 width=3 by fqu_flat_dx, ex2_intro/ -| #G #L2 #K2 #T #U #k #HLK2 #HTU #L1 #HL12 - elim (drop_O1_le (Ⓕ) (k+1) L1) - [ /3 width=12 by fqu_drop, lleq_inv_lift_le, ex2_intro/ - | lapply (drop_fwd_length_le2 … HLK2) -K2 - lapply (lleq_fwd_length … HL12) -T -U // - ] -] -qed-. - -lemma lleq_fquq_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐⸮ ⦃G2, K2, U⦄ → - ∀L1. L1 ≡[T, 0] L2 → - ∃∃K1. ⦃G1, L1, T⦄ ⊐⸮ ⦃G2, K1, U⦄ & K1 ≡[U, 0] K2. -#G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fquq_inv_gen … H) -H -[ #H elim (lleq_fqu_trans … H … HL12) -L2 /3 width=3 by fqu_fquq, ex2_intro/ -| * #HG #HL #HT destruct /2 width=3 by ex2_intro/ -] -qed-. - -lemma lleq_fqup_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐+ ⦃G2, K2, U⦄ → - ∀L1. L1 ≡[T, 0] L2 → - ∃∃K1. ⦃G1, L1, T⦄ ⊐+ ⦃G2, K1, U⦄ & K1 ≡[U, 0] K2. -#G1 #G2 #L2 #K2 #T #U #H @(fqup_ind … H) -G2 -K2 -U -[ #G2 #K2 #U #HTU #L1 #HL12 elim (lleq_fqu_trans … HTU … HL12) -L2 - /3 width=3 by fqu_fqup, ex2_intro/ -| #G #G2 #K #K2 #U #U2 #_ #HU2 #IHTU #L1 #HL12 elim (IHTU … HL12) -L2 - #K1 #HTU #HK1 elim (lleq_fqu_trans … HU2 … HK1) -K - /3 width=5 by fqup_strap1, ex2_intro/ -] -qed-. - -lemma lleq_fqus_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐* ⦃G2, K2, U⦄ → - ∀L1. L1 ≡[T, 0] L2 → - ∃∃K1. ⦃G1, L1, T⦄ ⊐* ⦃G2, K1, U⦄ & K1 ≡[U, 0] K2. -#G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fqus_inv_gen … H) -H -[ #H elim (lleq_fqup_trans … H … HL12) -L2 /3 width=3 by fqup_fqus, ex2_intro/ -| * #HG #HL #HT destruct /2 width=3 by ex2_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_lfdeq.ma similarity index 51% rename from matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_lleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_lfdeq.ma index 19e8d009a..e37aa68f0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_lfdeq.ma @@ -12,23 +12,25 @@ (* *) (**************************************************************************) -include "basic_2/multiple/lleq_fqus.ma". -include "basic_2/multiple/lleq_lleq.ma". -include "basic_2/reduction/lpx_lleq.ma". -include "basic_2/reduction/fpb.ma". +include "basic_2/static/lfdeq_fqus.ma". +include "basic_2/rt_transition/cpx_lfdeq.ma". +include "basic_2/rt_transition/lfpx_lfdeq.ma". +include "basic_2/rt_transition/fpb.ma". -(* "RST" PROPER PARALLEL COMPUTATION FOR CLOSURES ***************************) +(* PROPER PARALLEL RST-TRANSITION FOR CLOSURES ******************************) -(* Properties on lazy equivalence for local environments ********************) +(* Properties with degree-based equivalence for local environments **********) -lemma lleq_fpb_trans: ∀h,o,F,K1,K2,T. K1 ≡[T, 0] K2 → - ∀G,L2,U. ⦃F, K2, T⦄ ≻[h, o] ⦃G, L2, U⦄ → - ∃∃L1. ⦃F, K1, T⦄ ≻[h, o] ⦃G, L1, U⦄ & L1 ≡[U, 0] L2. +(* Basic_2A1: was just: lleq_fpb_trans *) +lemma lfdeq_fpb_trans: ∀h,o,F,K1,K2,T. K1 ≡[h, o, T] K2 → + ∀G,L2,U. ⦃F, K2, T⦄ ≻[h, o] ⦃G, L2, U⦄ → + ∃∃L1,U0. ⦃F, K1, T⦄ ≻[h, o] ⦃G, L1, U0⦄ & U0 ≡[h, o] U & L1 ≡[h, o, U] L2. #h #o #F #K1 #K2 #T #HT #G #L2 #U * -G -L2 -U -[ #G #L2 #U #H2 elim (lleq_fqu_trans … H2 … HT) -K2 - /3 width=3 by fpb_fqu, ex2_intro/ -| /4 width=10 by fpb_cpx, cpx_lleq_conf_sn, lleq_cpx_trans, ex2_intro/ -| #L2 #HKL2 #HnKL2 elim (lleq_lpx_trans … HKL2 … HT) -HKL2 - /6 width=3 by fpb_lpx, lleq_canc_sn, ex2_intro/ (* 2 lleq_canc_sn *) +[ #G #L2 #U #H2 elim (lfdeq_fqu_trans … H2 … HT) -K2 + /3 width=5 by fpb_fqu, ex3_2_intro/ +| #U #HTU #HnTU elim (lfdeq_cpx_trans … HT … HTU) -HTU + /5 width=10 by fpb_cpx, cpx_lfdeq_conf_sn, tdeq_trans, tdeq_lfdeq_conf_sn, ex3_2_intro/ +| #L2 #HKL2 #HnKL2 elim (lfdeq_lfpx_trans … HKL2 … HT) -HKL2 + /6 width=5 by fpb_lfpx, lfdeq_canc_sn, ex3_2_intro/ (* 2 lleq_canc_sn *) ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma index 1ff13898c..47b09be86 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma @@ -13,8 +13,10 @@ (**************************************************************************) include "basic_2/relocation/lifts_tdeq.ma". +include "basic_2/static/lfxs_lfxs.ma". include "basic_2/static/lfdeq_fqup.ma". -include "basic_2/rt_transition/lfpx.ma". +include "basic_2/rt_transition/lfpx_frees.ma". +include "basic_2/rt_transition/lfpx.ma". (**) (* should be in lfpx_frees.ma *) (* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****) @@ -133,20 +135,16 @@ elim (cpx_lfdeq_conf … o … HT01 L2) -HT01 /3 width=3 by lfdeq_sym, tdeq_sym, ex2_intro/ qed-. -include "basic_2/static/lfxs_lfxs.ma". +lemma lfpx_lfdeq_conf: ∀h,o,G,T. confluent2 … (lfpx h G T) (lfdeq h o T). +/3 width=6 by lfpx_frees_conf, cpx_tdeq_conf_lexs, frees_lfdeq_conf_lexs, lfxs_conf/ qed-. -axiom lfpx_lfdeq_conf: ∀h,o,G,T. confluent2 … (lfpx h G T) (lfdeq h o T). -(* -#H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 -@lfxs_conf -*) (* Basic_2A1: was just: lleq_lpx_trans *) lemma lfdeq_lfpx_trans: ∀h,o,G,T,L2,K2. ⦃G, L2⦄ ⊢ ⬈[h, T] K2 → ∀L1. L1 ≡[h, o, T] L2 → ∃∃K1. ⦃G, L1⦄ ⊢ ⬈[h, T] K1 & K1 ≡[h, o, T] K2. #h #o #G #T #L2 #K2 #HLK2 #L1 #HL12 elim (lfpx_lfdeq_conf … o … HLK2 L1) -/3 width=3 by lfdeq_sym, ex2_intro/ +/3 width=3 by lfdeq_sym, ex2_intro/ qed-. (* (* Properties with supclosure ***********************************************) 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 d300eb0ff..6105414f3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt @@ -5,5 +5,5 @@ cnx.ma cnx_simple.ma cnx_drops.ma cnx_cnx.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 +fpb.ma fpb_lfdeq.ma fpbq.ma fpbq_aaa.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma index e75c4e734..e49ccbfbe 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma @@ -61,6 +61,18 @@ lemma frees_tdeq_conf_lexs: ∀h,o,f,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f → ∀T2 ] qed-. +lemma frees_tdeq_conf: ∀h,o,f,L,T1. L ⊢ 𝐅*⦃T1⦄ ≡ f → + ∀T2. T1 ≡[h, o] T2 → L ⊢ 𝐅*⦃T2⦄ ≡ f. +/3 width=7 by frees_tdeq_conf_lexs, lexs_refl/ qed-. + +lemma frees_lfdeq_conf_lexs: ∀h,o. lexs_frees_confluent (cdeq h o) cfull. +/3 width=7 by frees_tdeq_conf_lexs, ex2_intro/ qed-. + +lemma tdeq_lfdeq_conf_sn: ∀h,o. s_r_confluent1 … (cdeq h o) (lfdeq h o). +#h #o #L1 #T1 #T2 #HT12 #L2 * +/3 width=5 by frees_tdeq_conf, ex2_intro/ +qed-. + lemma lfdeq_sym: ∀h,o,T. symmetric … (lfdeq h o T). #h #o #T #L1 #L2 * /4 width=7 by frees_tdeq_conf_lexs, lfxs_sym, tdeq_sym, ex2_intro/ @@ -160,6 +172,10 @@ lemma lfdeq_fwd_flat_dx: ∀h,o,I,L1,L2,V,T. L1 ≡[h, o, ⓕ{I}V.T] L2 → L1 lemma lfdeq_fwd_pair_sn: ∀h,o,I,L1,L2,V,T. L1 ≡[h, o, ②{I}V.T] L2 → L1 ≡[h, o, V] L2. /2 width=3 by lfxs_fwd_pair_sn/ qed-. +lemma lfdeq_fwd_dx: ∀h,o,I,L1,K2,V2. ∀T:term. L1 ≡[h, o, T] K2.ⓑ{I}V2 → + ∃∃K1,V1. L1 = K1.ⓑ{I}V1. +/2 width=5 by lfxs_fwd_dx/ qed-. + (* Basic_2A1: removed theorems 30: lleq_ind lleq_inv_bind lleq_inv_flat lleq_fwd_length lleq_fwd_lref lleq_fwd_drop_sn lleq_fwd_drop_dx diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_drops.ma new file mode 100644 index 000000000..93b9ccfa1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_drops.ma @@ -0,0 +1,49 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lfxs_drops.ma". +include "basic_2/static/lfdeq_fqup.ma". + +(* DEGREE-BASED EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ******) + +(* Properties with generic slicing for local environments *******************) + +(* Basic_2A1: includes: lleq_lift_le lleq_lift_ge *) +lemma lfdeq_lifts: ∀h,o. dedropable_sn (cdeq h o). +/3 width=5 by lfxs_liftable_dedropable, tdeq_lifts/ qed-. + +(* Inversion lemmas with generic slicing for local environments *************) + +(* Basic_2A1: restricts: lleq_inv_lift_le lleq_inv_lift_be lleq_inv_lift_ge *) +lemma lfdeq_inv_lifts: ∀h,o. dropable_sn (cdeq h o). +/2 width=5 by lfxs_dropable_sn/ qed-. + +(* Note: missing in basic_2A1 *) +lemma lfdeq_inv_lifts_dx: ∀h,o. dropable_dx (cdeq h o). +/2 width=5 by lfxs_dropable_dx/ qed-. + +(* Note: missing in basic_2A1 *) +lemma lfdeq_inv_lifts_bi: ∀h,o,L1,L2,U. L1 ≡[h, o, U] L2 → + ∀K1,K2,i. ⬇*[i] L1 ≡ K1 → ⬇*[i] L2 ≡ K2 → + ∀T. ⬆*[i] T ≡ U → K1 ≡[h, o, T] K2. +/2 width=8 by lfxs_inv_lifts_bi/ qed-. + +lemma lfdeq_inv_lref_sn: ∀h,o,L1,L2,i. L1 ≡[h, o, #i] L2 → ∀I,K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 → + ∃∃K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 & K1 ≡[h, o, V1] K2 & V1 ≡[h, o] V2. +/2 width=3 by lfxs_inv_lref_sn/ qed-. + +lemma lfdeq_inv_lref_dx: ∀h,o,L1,L2,i. L1 ≡[h, o, #i] L2 → ∀I,K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 → + ∃∃K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 & K1 ≡[h, o, V1] K2 & V1 ≡[h, o] V2. +/2 width=3 by lfxs_inv_lref_dx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqup.ma index b6e2a18f6..529236417 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqup.ma @@ -21,3 +21,7 @@ include "basic_2/static/lfdeq.ma". lemma lfdeq_refl: ∀h,o,T. reflexive … (lfdeq h o T). /2 width=1 by lfxs_refl/ qed. + +lemma lfdeq_pair: ∀h,o,V1,V2. V1 ≡[h, o] V2 → + ∀I,L. ∀T:term. L.ⓑ{I}V1 ≡[h, o, T] L.ⓑ{I}V2. +/2 width=1 by lfxs_pair/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqus.ma new file mode 100644 index 000000000..280ab796a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqus.ma @@ -0,0 +1,109 @@ +(**************************************************************************) +(* ___ *) +(* ||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/s_computation/fqus_fqup.ma". +include "basic_2/static/lfdeq_drops.ma". +include "basic_2/static/lfdeq_lfdeq.ma". + +(* DEGREE-BASED EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ******) + +(* Properties with supclosure ***********************************************) + +lemma fqu_tdeq_conf: ∀h,o,G1,G2,L1,L2,U1,T1. ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, T1⦄ → + ∀U2. U1 ≡[h, o] U2 → + ∃∃L,T2. ⦃G1, L1, U2⦄ ⊐ ⦃G2, L, T2⦄ & L2 ≡[h, o, T1] L & T1 ≡[h, o] T2. +#h #o #G1 #G2 #L1 #L2 #U1 #T1 #H elim H -G1 -G2 -L1 -L2 -U1 -T1 +[ #I #G #L #W #X #H >(tdeq_inv_lref1 … H) -H + /2 width=5 by fqu_lref_O, ex3_2_intro/ +| #I #G #L #W1 #U1 #X #H + elim (tdeq_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 #X #H + elim (tdeq_inv_pair1 … H) -H #W2 #U2 #HW12 #HU12 #H destruct + /3 width=5 by lfdeq_pair, fqu_bind_dx, ex3_2_intro/ +| #I #G #L #W1 #U1 #X #H + elim (tdeq_inv_pair1 … H) -H #W2 #U2 #_ #HU12 #H destruct + /2 width=5 by fqu_flat_dx, ex3_2_intro/ +| #I #G #L #W #T1 #U1 #HTU1 #U2 #HU12 + elim (tdeq_inv_lifts … HU12 … HTU1) -U1 #T2 #HTU2 #HT12 + /3 width=5 by fqu_drop, ex3_2_intro/ +] +qed-. + +lemma tdeq_fqu_trans: ∀h,o,G1,G2,L1,L2,U1,T1. ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, T1⦄ → + ∀U2. U2 ≡[h, o] U1 → + ∃∃L,T2. ⦃G1, L1, U2⦄ ⊐ ⦃G2, L, T2⦄ & T2 ≡[h, o] T1 & L ≡[h, o, T1] L2. +#h #o #G1 #G2 #L1 #L2 #U1 #T1 #H12 #U2 #HU21 +elim (fqu_tdeq_conf … o … H12 U2) -H12 +/3 width=5 by lfdeq_sym, tdeq_sym, ex3_2_intro/ +qed-. + +(* Basic_2A1: was just: lleq_fqu_trans *) +lemma lfdeq_fqu_trans: ∀h,o,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐ ⦃G2, K2, U⦄ → + ∀L1. L1 ≡[h, o, T] L2 → + ∃∃K1,U0. ⦃G1, L1, T⦄ ⊐ ⦃G2, K1, U0⦄ & U0 ≡[h, o] U & K1 ≡[h, o, U] K2. +#h #o #G1 #G2 #L2 #K2 #T #U #H elim H -G1 -G2 -L2 -K2 -T -U +[ #I #G #L2 #V2 #L1 #H elim (lfdeq_inv_zero_pair_dx … H) -H + #K1 #V1 #HV1 #HV12 #H destruct + /3 width=7 by tdeq_lfdeq_conf_sn, fqu_lref_O, ex3_2_intro/ +| * [ #p ] #I #G #L2 #V #T #L1 #H + [ elim (lfdeq_inv_bind … H) + | elim (lfdeq_inv_flat … H) + ] -H + /2 width=5 by fqu_pair_sn, ex3_2_intro/ +| #a #I #G #L2 #V #T #L1 #H elim (lfdeq_inv_bind … H) -H + /2 width=5 by fqu_bind_dx, ex3_2_intro/ +| #I #G #L2 #V #T #L1 #H elim (lfdeq_inv_flat … H) -H + /2 width=5 by fqu_flat_dx, ex3_2_intro/ +| #I #G #L2 #V2 #T #U #HTU #Y #HU + elim (lfdeq_fwd_dx … HU) #L1 #V1 #H destruct + /5 width=12 by lfdeq_inv_lifts_bi, fqu_drop, drops_refl, drops_drop, ex3_2_intro/ +] +qed-. + +(* Basic_2A1: was just: lleq_fquq_trans *) +lemma lfdeq_fquq_trans: ∀h,o,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐⸮ ⦃G2, K2, U⦄ → + ∀L1. L1 ≡[h, o, T] L2 → + ∃∃K1,U0. ⦃G1, L1, T⦄ ⊐⸮ ⦃G2, K1, U0⦄ & U0 ≡[h, o] U & K1 ≡[h, o, U] K2. +#h #o #G1 #G2 #L2 #K2 #T #U #H elim H -H +[ #H #L1 #HL12 elim (lfdeq_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-. + +(* Basic_2A1: was just: lleq_fqup_trans *) +lemma lfdeq_fqup_trans: ∀h,o,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐+ ⦃G2, K2, U⦄ → + ∀L1. L1 ≡[h, o, T] L2 → + ∃∃K1,U0. ⦃G1, L1, T⦄ ⊐+ ⦃G2, K1, U0⦄ & U0 ≡[h, o] U & K1 ≡[h, o, U] K2. +#h #o #G1 #G2 #L2 #K2 #T #U #H @(fqup_ind … H) -G2 -K2 -U +[ #G2 #K2 #U #HTU #L1 #HL12 elim (lfdeq_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 (lfdeq_fqu_trans … HU2 … HK0) -K #K1 #U1 #HU1 #HU12 #HK12 + elim (tdeq_fqu_trans … HU1 … HU0) -U #K3 #U3 #HU03 #HU31 #HK31 + @(ex3_2_intro … K3 U3) (**) (* full auto too slow *) + /3 width=5 by lfdeq_trans, tdeq_lfdeq_conf_sn, fqup_strap1, tdeq_trans/ +] +qed-. + +(* Basic_2A1: was just: lleq_fqus_trans *) +lemma lfdeq_fqus_trans: ∀h,o,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐* ⦃G2, K2, U⦄ → + ∀L1. L1 ≡[h, o, T] L2 → + ∃∃K1,U0. ⦃G1, L1, T⦄ ⊐* ⦃G2, K1, U0⦄ & U0 ≡[h, o] U & K1 ≡[h, o, U] K2. +#h #o #G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fqus_inv_fqup … H) -H +[ #H elim (lfdeq_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/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma index a1d50e69f..9f0a1a486 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma @@ -253,6 +253,13 @@ lemma lfxs_fwd_pair_sn: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ②{I}V.T] L2 → L1 ⦻*[R #R * /2 width=4 by lfxs_fwd_flat_sn, lfxs_fwd_bind_sn/ qed-. +lemma lfxs_fwd_dx: ∀R,I,L1,K2,T,V2. L1 ⦻*[R, T] K2.ⓑ{I}V2 → + ∃∃K1,V1. L1 = K1.ⓑ{I}V1. +#R #I #L1 #K2 #T #V2 * #f elim (pn_split f) * #g #Hg #_ #Hf destruct +[ elim (lexs_inv_push2 … Hf) | elim (lexs_inv_next2 … Hf) ] -Hf #K1 #V1 #_ #_ #H destruct +/2 width=3 by ex1_2_intro/ +qed-. + (* Basic_2A1: removed theorems 24: llpx_sn_sort llpx_sn_skip llpx_sn_lref llpx_sn_free llpx_sn_gref llpx_sn_bind llpx_sn_flat diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma index 0a3f287bb..9875361f7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma @@ -70,9 +70,9 @@ elim (lexs_co_dropable_dx … HL12 … HLK2 … H2f) -L2 qed-. (* Basic_2A1: was: llpx_sn_inv_lift_O *) -lemma lfxs_inv_lift_bi: ∀R,L1,L2,U. L1 ⦻*[R, U] L2 → - ∀K1,K2,i. ⬇*[i] L1 ≡ K1 → ⬇*[i] L2 ≡ K2 → - ∀T. ⬆*[i] T ≡ U → K1 ⦻*[R, T] K2. +lemma lfxs_inv_lifts_bi: ∀R,L1,L2,U. L1 ⦻*[R, U] L2 → + ∀K1,K2,i. ⬇*[i] L1 ≡ K1 → ⬇*[i] L2 ≡ K2 → + ∀T. ⬆*[i] T ≡ U → K1 ⦻*[R, T] K2. #R #L1 #L2 #U #HL12 #K1 #K2 #i #HLK1 #HLK2 #T #HTU elim (lfxs_dropable_sn … HLK1 … HL12 … HTU) -L1 -U // #Y #HK12 #HY lapply (drops_mono … HY … HLK2) -L2 -i #H destruct // diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma index 26289760b..56ce31016 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma @@ -36,16 +36,18 @@ theorem lfxs_flat: ∀R,I,L1,L2,V,T. /3 width=7 by frees_fwd_isfin, frees_flat, lexs_join, ex2_intro/ qed. -theorem lfxs_conf: ∀R. lexs_frees_confluent R cfull → - R_confluent2_lfxs R R R R → - ∀T. confluent … (lfxs R T). -#R #H1R #H2R #T #L0 #L1 * #f1 #Hf1 #HL01 #L2 * #f #Hf #HL02 +theorem lfxs_conf: ∀R1,R2. + lexs_frees_confluent R1 cfull → + lexs_frees_confluent R2 cfull → + R_confluent2_lfxs R1 R2 R1 R2 → + ∀T. confluent2 … (lfxs R1 T) (lfxs R2 T). +#R1 #R2 #HR1 #HR2 #HR12 #T #L0 #L1 * #f1 #Hf1 #HL01 #L2 * #f #Hf #HL02 lapply (frees_mono … Hf1 … Hf) -Hf1 #Hf12 lapply (lexs_eq_repl_back … HL01 … Hf12) -f1 #HL01 elim (lexs_conf … HL01 … HL02) /2 width=3 by ex2_intro/ [ | -HL01 -HL02 ] [ #L #HL1 #HL2 - elim (H1R … Hf … HL01) -HL01 #f1 #Hf1 #H1 - elim (H1R … Hf … HL02) -HL02 #f2 #Hf2 #H2 + elim (HR1 … Hf … HL01) -HL01 #f1 #Hf1 #H1 + elim (HR2 … Hf … HL02) -HL02 #f2 #Hf2 #H2 lapply (sle_lexs_trans … HL1 … H1) // -HL1 -H1 #HL1 lapply (sle_lexs_trans … HL2 … H2) // -HL2 -H2 #HL2 /3 width=5 by ex2_intro/ @@ -53,6 +55,6 @@ elim (lexs_conf … HL01 … HL02) /2 width=3 by ex2_intro/ [ | -HL01 -HL02 ] elim (frees_drops_next … Hf … HLK0 … Hgf) -Hf -HLK0 -Hgf #g0 #Hg0 #H0 lapply (sle_lexs_trans … HK01 … H0) // -HK01 #HK01 lapply (sle_lexs_trans … HK02 … H0) // -HK02 #HK02 - elim (H2R … HV01 … HV02 K1 … K2) /2 width=3 by ex2_intro/ + elim (HR12 … HV01 … HV02 K1 … K2) /2 width=3 by ex2_intro/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 8df423ca9..9471aeaff 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 @@ -108,7 +108,7 @@ table { } ] *) - [ { "uncounted context-sensitive rt-transition" * } { + [ { "uncounted context-sensitive rt-computation" * } { (* [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_drop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] [ "cpxs_lreq" + "cpxs_lleq" + "cpxs_aaa" * ] @@ -125,7 +125,7 @@ table { [ { "rt-transition" * } { [ { "parallel rst-transition" * } { [ "fpbq ( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ )" "fpbq_aaa" * ] - [ "fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" (* "fpb_lleq" + "fpb_fleq" *) * ] + [ "fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpb_lfdeq" (* + "fpb_fleq" *) * ] } ] [ { "t-bound context-sensitive rt-transition" * } { @@ -169,7 +169,7 @@ table { ] [ { "degree-based equivalence on referred entries" * } { [ "ffdeq ( ⦃?,?,?⦄ ≡[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_ffdeq" * ] - [ "lfdeq ( ? ≡[?,?,?] ? )" "lfdeq_length" + "lfdeq_fqup" + "lfdeq_lfdeq" * ] + [ "lfdeq ( ? ≡[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfdeq" * ] } ] [ { "generic extension on referred entries" * } { -- 2.39.2