From 9323611e3819c1382b872a7ada00264991f36217 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 15 Feb 2018 15:19:07 +0100 Subject: [PATCH] integrating the framework with fle ... + new ignores --- .gitignore | 1 + .../lambdadelta/basic_2/i_static/tc_lfxs.ma | 7 --- .../basic_2/i_static/tc_lfxs_lex.ma | 4 +- .../basic_2/i_static/tc_lfxs_tc_lfxs.ma | 10 ++++ .../basic_2/rt_computation/lfpxs_etc.ma | 1 - .../basic_2/rt_computation/lfpxs_lpxs.ma | 2 +- .../basic_2/rt_computation/lfsx.ma | 4 +- .../basic_2/rt_transition/cpm_lfxs.ma | 9 ++- .../basic_2/rt_transition/cpx_etc.ma | 1 - .../basic_2/rt_transition/cpx_lfdeq.ma | 2 +- .../basic_2/rt_transition/cpx_lfxs.ma | 22 +++++-- .../basic_2/rt_transition/lfpr_lfpr.ma | 2 +- .../basic_2/rt_transition/lfpx_lfdeq.ma | 11 ++-- .../lambdadelta/basic_2/static/ffdeq.ma | 6 -- .../lambdadelta/basic_2/static/ffdeq_ffdeq.ma | 6 ++ .../lambdadelta/basic_2/static/fle_fle.ma | 10 +++- .../lambdadelta/basic_2/static/fle_fqup.ma | 12 ++++ .../lambdadelta/basic_2/static/fle_lsubf.ma | 31 ---------- .../lambdadelta/basic_2/static/lfdeq.ma | 21 ++----- .../basic_2/static/lfdeq_length.ma | 19 ++++-- .../lambdadelta/basic_2/static/lfdeq_lfdeq.ma | 8 ++- .../lambdadelta/basic_2/static/lfxs.ma | 23 ++------ .../lambdadelta/basic_2/static/lfxs_fle.ma | 29 ---------- .../lambdadelta/basic_2/static/lfxs_lfxs.ma | 58 ++++++++++++++----- .../lambdadelta/basic_2/web/basic_2_src.tbl | 4 +- 25 files changed, 150 insertions(+), 153 deletions(-) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/fle_lsubf.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/lfxs_fle.ma diff --git a/.gitignore b/.gitignore index 72f97fe46..b782458ea 100644 --- a/.gitignore +++ b/.gitignore @@ -67,6 +67,7 @@ helm/www/lambdadelta/xslt/core.xsl helm/www/lambdadelta/xslt/chc_45.xsl helm/www/lambdadelta/xslt/xhtbl.xsl +matita/matita/contribs/lambdadelta/.depend matita/matita/contribs/lambdadelta/nodes matita/matita/contribs/lambdadelta/token matita/matita/contribs/lambdadelta/2A1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs.ma index 8e3bf8a4d..90b0de1eb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs.ma @@ -67,13 +67,6 @@ lemma tc_lfxs_gref: ∀R,I,L1,L2,V1,V2,l. /3 width=4 by lfxs_gref, tc_lfxs_step_dx, inj/ qed. -lemma tc_lfxs_sym: ∀R. lexs_frees_confluent (cext2 R) cfull → - (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) → - ∀T. symmetric … (tc_lfxs R T). -#R #H1R #H2R #T #L1 #L2 #H elim H -L2 -/4 width=3 by lfxs_sym, tc_lfxs_step_sn, inj/ -qed-. - lemma tc_lfxs_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) → ∀L1,L2,T. L1 ⪤**[R1, T] L2 → L1 ⪤**[R2, T] L2. #R1 #R2 #HR #L1 #L2 #T #H elim H -L2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lex.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lex.ma index 45bf6a472..73ddeb26f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lex.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lex.ma @@ -36,7 +36,7 @@ lemma tc_lfxs_lex_lfeq: ∀R. c_reflexive … R → (* Note: s_rs_transitive_lex_inv_isid could be invoked in the last auto but makes it too slow *) lemma tc_lfxs_inv_lex_lfeq: ∀R. c_reflexive … R → - lexs_frees_confluent (cext2 R) cfull → + lfxs_fle_compatible R → s_rs_transitive … R (λ_.lex R) → lfeq_transitive R → ∀L1,L2,T. L1 ⪤**[R, T] L2 → @@ -50,7 +50,7 @@ lapply (s_rs_transitive_lex_inv_isid … H3R) -H3R #H3R elim (lexs_sdj_split … ceq_ext … HL2 f0 ?) -HL2 [ #L0 #HL0 #HL02 |*: /2 width=1 by ext2_refl, sdj_isid_dx/ ] lapply (lexs_sdj … HL0 f1 ?) /2 width=1 by sdj_isid_sn/ #H - elim (H2R … Hf1 … H) -H #f2 #Hf2 #Hf21 + elim (frees_lexs_conf … Hf1 … H) // -H2R -H #f2 #Hf2 #Hf21 lapply (sle_lexs_trans … HL02 … Hf21) -f1 // #HL02 lapply (lexs_co ?? cfull (LTC … (cext2 R)) … HL1) -HL1 /2 width=1 by ext2_inv_tc/ #HL1 /8 width=11 by lexs_inv_tc_dx, lexs_tc_dx, lexs_co, ext2_tc, ext2_refl, step, ex2_intro/ (**) (* full auto too slow *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_tc_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_tc_lfxs.ma index 62173d926..87f279a9b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_tc_lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_tc_lfxs.ma @@ -12,10 +12,20 @@ (* *) (**************************************************************************) +include "basic_2/static/lfxs_lfxs.ma". include "basic_2/i_static/tc_lfxs.ma". (* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***) +(* Advanced properties ******************************************************) + +lemma tc_lfxs_sym: ∀R. lfxs_fle_compatible R → + (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) → + ∀T. symmetric … (tc_lfxs R T). +#R #H1R #H2R #T #L1 #L2 #H elim H -L2 +/4 width=3 by lfxs_sym, tc_lfxs_step_sn, inj/ +qed-. + (* Main properties **********************************************************) theorem tc_lfxs_trans: ∀R,T. Transitive … (tc_lfxs R T). diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma index e70a8f596..d19718058 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma @@ -1,6 +1,5 @@ include "basic_2/static/lfxs_lex.ma". -include "basic_2/static/lfxs_fle.ma". include "basic_2/rt_transition/cpx_etc.ma". include "basic_2/rt_computation/lfpxs_lpxs.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma index 7839a4b3d..93118b9a0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma @@ -30,4 +30,4 @@ lemma lfpxs_lpxs_lfeq: ∀h,G,L1,L. ⦃G, L1⦄ ⊢ ⬈*[h] L → lemma tc_lfxs_inv_lex_lfeq: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → ∃∃L. ⦃G, L1⦄ ⊢ ⬈*[h] L & L ≡[T] L2. -/3 width=5 by lfpx_frees_conf, lpx_cpxs_trans, lfeq_cpx_trans, tc_lfxs_inv_lex_lfeq/ qed-. +/3 width=5 by lfpx_fle_comp, lpx_cpxs_trans, lfeq_cpx_trans, tc_lfxs_inv_lex_lfeq/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma index bf17640dd..4258c13dd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma @@ -35,7 +35,7 @@ lemma lfsx_ind: ∀h,o,G,T. ∀R:predicate lenv. ) → ∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → R L. #h #o #G #T #R #H0 #L1 #H elim H -L1 -/5 width=1 by lfdeq_sym, SN_intro/ +/5 width=1 by SN_intro/ qed-. (* Basic properties *********************************************************) @@ -44,7 +44,7 @@ qed-. lemma lfsx_intro: ∀h,o,G,L1,T. (∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → (L1 ≛[h, o, T] L2 → ⊥) → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄) → G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄. -/5 width=1 by lfdeq_sym, SN_intro/ qed. +/5 width=1 by SN_intro/ qed. (* Basic_2A1: uses: lsx_sort *) lemma lfsx_sort: ∀h,o,G,L,s. G ⊢ ⬈*[h, o, ⋆s] 𝐒⦃L⦄. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lfxs.ma index e9785d6a3..499a145bf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lfxs.ma @@ -14,17 +14,16 @@ include "basic_2/rt_transition/cpx_lfxs.ma". include "basic_2/rt_transition/cpm_cpx.ma". -include "basic_2/rt_transition/cpr_ext.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************) (* Properties with context-sensitive free variables *************************) -lemma cpm_frees_conf: ∀n,h,G. R_frees_confluent (cpm n h G). -/3 width=6 by cpm_fwd_cpx, cpx_frees_conf/ qed-. +lemma cpm_fle_comp: ∀n,h,G. R_fle_compatible (cpm n h G). +/3 width=6 by cpm_fwd_cpx, cpx_fle_comp/ qed-. -lemma lfpr_frees_conf: ∀h,G. lexs_frees_confluent (cpr_ext h G) cfull. -/5 width=9 by cpm_fwd_cpx, lfpx_frees_conf, lexs_co, cext2_co/ qed-. +lemma lfpr_fle_comp: ∀h,G. lfxs_fle_compatible (cpm 0 h G). +/4 width=5 by cpm_fwd_cpx, lfpx_fle_comp, lfxs_co/ qed-. (* Properties with generic extension on referred entries ********************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_etc.ma index d83d1f063..a6c77b5c9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_etc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_etc.ma @@ -14,7 +14,6 @@ include "basic_2/static/fle_drops.ma". include "basic_2/static/fle_fqup.ma". -include "basic_2/static/fle_lsubf.ma". include "basic_2/static/fle_fle.ma". include "basic_2/static/lfxs_length.ma". include "basic_2/rt_transition/cpx.ma". 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 index f3ccf0616..00b3fca8f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfdeq.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/static/lfdeq.ma". +include "basic_2/static/lfdeq_lfdeq.ma". include "basic_2/rt_transition/cpx_lfxs.ma". (* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfxs.ma index 7d5c920c7..69eab45f9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfxs.ma @@ -12,6 +12,8 @@ (* *) (**************************************************************************) +include "basic_2/syntax/lveq_length.ma". +include "basic_2/relocation/lexs_length.ma". include "basic_2/relocation/drops_lexs.ma". include "basic_2/static/frees_drops.ma". include "basic_2/static/lsubf_frees.ma". @@ -158,18 +160,26 @@ lemma cpx_frees_conf_lexs: ∀h,G,L1,T1,f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 → qed-. (* Basic_2A1: uses: cpx_frees_trans *) -lemma cpx_frees_conf: ∀h,G. R_frees_confluent (cpx h G). -/4 width=7 by cpx_frees_conf_lexs, lexs_refl, ext2_refl/ qed-. +lemma cpx_fle_comp: ∀h,G. R_fle_compatible (cpx h G). +#h #G #L #T1 #T2 #HT12 +elim (frees_total L T1) #f1 #Hf1 +elim (cpx_frees_conf_lexs … Hf1 L … HT12) -HT12 +/3 width=8 by lexs_refl, ext2_refl, ex4_4_intro/ +qed-. (* Basic_2A1: uses: lpx_frees_trans *) -lemma lfpx_frees_conf: ∀h,G. lexs_frees_confluent (cpx_ext h G) cfull. -/2 width=7 by cpx_frees_conf_lexs/ qed-. +lemma lfpx_fle_comp: ∀h,G. lfxs_fle_compatible (cpx h G). +#h #G #L1 #L2 #T * #f1 #Hf1 #HL12 +elim (cpx_frees_conf_lexs h … Hf1 … HL12 T) // #f2 #Hf2 +lapply (lexs_fwd_length … HL12) +/3 width=8 by lveq_length_eq, ex4_4_intro/ (**) (* full auto fails *) +qed-. (* Properties with generic extension on referred entries ********************) (* Note: lemma 1000 *) (* Basic_2A1: uses: 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/ +#R #h #G #L1 #T1 #T2 #H #L2 * #f1 #Hf1 elim (cpx_frees_conf_lexs … Hf1 L1 … H) -T1 +/3 width=5 by lexs_refl, ext2_refl, sle_lexs_trans, ex2_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma index ee7978c14..3db8912af 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma @@ -380,7 +380,7 @@ qed-. (* Main properties **********************************************************) theorem lfpr_conf: ∀h,G,T. confluent … (lfpr h G T). -/3 width=6 by cpr_conf_lfpr, lfpr_frees_conf, lfxs_conf/ qed-. +/3 width=6 by cpr_conf_lfpr, lfpr_fle_comp, lfxs_conf/ qed-. theorem lfpr_bind: ∀h,G,L1,L2,V1. ⦃G, L1⦄ ⊢ ➡[h, V1] L2 → ∀I,V2,T. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[h, T] L2.ⓑ{I}V2 → 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 e7eae9096..1536a6483 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 @@ -15,6 +15,7 @@ include "basic_2/relocation/lifts_tdeq.ma". include "basic_2/static/lfxs_lfxs.ma". include "basic_2/static/lfdeq_fqup.ma". +include "basic_2/static/lfdeq_lfdeq.ma". include "basic_2/rt_transition/cpx_lfxs.ma". include "basic_2/rt_transition/lfpx.ma". @@ -24,19 +25,19 @@ include "basic_2/rt_transition/lfpx.ma". lemma lfpx_pair_sn_split: ∀h,G,L1,L2,V. ⦃G, L1⦄ ⊢ ⬈[h, V] L2 → ∀o,I,T. ∃∃L. ⦃G, L1⦄ ⊢ ⬈[h, ②{I}V.T] L & L ≛[h, o, V] L2. -/3 width=5 by lfpx_frees_conf, lfxs_pair_sn_split/ qed-. +/3 width=5 by lfpx_fle_comp, lfxs_pair_sn_split/ qed-. lemma lfpx_flat_dx_split: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → ∀o,I,V. ∃∃L. ⦃G, L1⦄ ⊢ ⬈[h, ⓕ{I}V.T] L & L ≛[h, o, T] L2. -/3 width=5 by lfpx_frees_conf, lfxs_flat_dx_split/ qed-. +/3 width=5 by lfpx_fle_comp, lfxs_flat_dx_split/ qed-. lemma lfpx_bind_dx_split: ∀h,I,G,L1,L2,V1,T. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈[h, T] L2 → ∀o,p. ∃∃L,V. ⦃G, L1⦄ ⊢ ⬈[h, ⓑ{p,I}V1.T] L & L.ⓑ{I}V ≛[h, o, T] L2 & ⦃G, L1⦄ ⊢ V1 ⬈[h] V. -/3 width=5 by lfpx_frees_conf, lfxs_bind_dx_split/ qed-. +/3 width=5 by lfpx_fle_comp, lfxs_bind_dx_split/ qed-. lemma lfpx_bind_dx_split_void: ∀h,G,K1,L2,T. ⦃G, K1.ⓧ⦄ ⊢ ⬈[h, T] L2 → ∀o,p,I,V. ∃∃K2. ⦃G, K1⦄ ⊢ ⬈[h, ⓑ{p,I}V.T] K2 & K2.ⓧ ≛[h, o, T] L2. -/3 width=5 by lfpx_frees_conf, lfxs_bind_dx_split_void/ qed-. +/3 width=5 by lfpx_fle_comp, lfxs_bind_dx_split_void/ qed-. 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/ @@ -152,7 +153,7 @@ elim (cpx_lfdeq_conf … o … HT01 L2) -HT01 qed-. 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-. +/3 width=6 by lfpx_fle_comp, lfdeq_fle_comp, cpx_tdeq_conf_lexs, lfxs_conf/ qed-. (* Basic_2A1: uses: lleq_lpx_trans *) lemma lfdeq_lfpx_trans: ∀h,o,G,T,L2,K2. ⦃G, L2⦄ ⊢ ⬈[h, T] K2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq.ma index ef74ef3c4..7e4392488 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq.ma @@ -26,12 +26,6 @@ interpretation "degree-based equivalence on referred entries (closure)" 'StarEqSn h o G1 L1 T1 G2 L2 T2 = (ffdeq h o G1 L1 T1 G2 L2 T2). -(* Basic properties *********************************************************) - -lemma ffdeq_sym: ∀h,o. tri_symmetric … (ffdeq h o). -#h #o #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -L1 -T1 /3 width=1 by ffdeq_intro, lfdeq_sym/ -qed-. - (* Basic inversion lemmas ***************************************************) lemma ffdeq_inv_gen: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_ffdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_ffdeq.ma index 47a38804c..101463609 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_ffdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_ffdeq.ma @@ -17,6 +17,12 @@ include "basic_2/static/ffdeq.ma". (* DEGREE-BASED EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES ****************) +(* Advanced properties ******************************************************) + +lemma ffdeq_sym: ∀h,o. tri_symmetric … (ffdeq h o). +#h #o #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -L1 -T1 /3 width=1 by ffdeq_intro, lfdeq_sym/ +qed-. + (* Main properties **********************************************************) theorem ffdeq_trans: ∀h,o. tri_transitive … (ffdeq h o). diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/fle_fle.ma b/matita/matita/contribs/lambdadelta/basic_2/static/fle_fle.ma index 0bd285aca..18574be3d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/fle_fle.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/fle_fle.ma @@ -13,7 +13,6 @@ (**************************************************************************) include "basic_2/syntax/lveq_lveq.ma". -include "basic_2/static/frees_frees.ma". include "basic_2/static/fle_fqup.ma". (* FREE VARIABLES INCLUSION FOR RESTRICTED CLOSURES *************************) @@ -31,6 +30,15 @@ lapply (sle_eq_repl_back2 … Hn … Hgf2) -g2 /2 width=6 by ex3_3_intro/ qed-. +lemma fle_frees_trans_eq: ∀L1,L2. |L1| = |L2| → + ∀T1,T2. ⦃L1, T1⦄ ⊆ ⦃L2, T2⦄ → ∀f2. L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 → + ∃∃f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 & f1 ⊆ f2. +#L1 #L2 #H1L #T1 #T2 #H2L #f2 #Hf2 +elim (fle_frees_trans … H2L … Hf2) -T2 #n1 #n2 #f1 #Hf1 #H2L #Hf12 +elim (lveq_inj_length … H2L) // -L2 #H1 #H2 destruct +/2 width=3 by ex2_intro/ +qed-. + (* Main properties **********************************************************) (* theorem fle_trans: bi_transitive … fle. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/fle_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/static/fle_fqup.ma index c6d61ed91..b50fa075d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/fle_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/fle_fqup.ma @@ -82,3 +82,15 @@ elim (sor_isfin_ex g1 g2) /2 width=3 by frees_fwd_isfin/ #g #Hg #_ @(ex4_4_intro … g Hf2 … HL12) (**) (* full auto too slow *) /4 width=5 by frees_flat, sor_inv_sle_dx, sor_tls, sle_trans/ qed. + +(* Advanced forward lemmas ***************************************************) + +lemma fle_fwd_pair_sn: ∀I1,I2,L1,L2,V1,V2,T1,T2. ⦃L1.ⓑ{I1}V1, T1⦄ ⊆ ⦃L2.ⓑ{I2}V2, T2⦄ → + ⦃L1.ⓧ, T1⦄ ⊆ ⦃L2.ⓑ{I2}V2, T2⦄. +#I1 #I2 #L1 #L2 #V1 #V2 #T1 #T2 * +#n1 #n2 #f1 #f2 #Hf1 #Hf2 #HL12 #Hf12 +elim (lveq_inv_pair_pair … HL12) -HL12 #HL12 #H1 #H2 destruct +elim (frees_total (L1.ⓧ) T1) #g1 #Hg1 +lapply (lsubr_lsubf … Hg1 … Hf1) -Hf1 /2 width=1 by lsubr_unit/ #Hfg1 +/5 width=10 by lsubf_fwd_sle, lveq_bind, sle_trans, ex4_4_intro/ (**) (* full auto too slow *) +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/fle_lsubf.ma b/matita/matita/contribs/lambdadelta/basic_2/static/fle_lsubf.ma deleted file mode 100644 index 7f6af2eaf..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/static/fle_lsubf.ma +++ /dev/null @@ -1,31 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/static/frees_fqup.ma". -include "basic_2/static/lsubf_lsubr.ma". -include "basic_2/static/fle.ma". - -(* FREE VARIABLES INCLUSION FOR RESTRICTED CLOSURES *************************) - -(* Advanced forward lemmas ***************************************************) - -lemma fle_fwd_pair_sn: ∀I1,I2,L1,L2,V1,V2,T1,T2. ⦃L1.ⓑ{I1}V1, T1⦄ ⊆ ⦃L2.ⓑ{I2}V2, T2⦄ → - ⦃L1.ⓧ, T1⦄ ⊆ ⦃L2.ⓑ{I2}V2, T2⦄. -#I1 #I2 #L1 #L2 #V1 #V2 #T1 #T2 * -#n1 #n2 #f1 #f2 #Hf1 #Hf2 #HL12 #Hf12 -elim (lveq_inv_pair_pair … HL12) -HL12 #HL12 #H1 #H2 destruct -elim (frees_total (L1.ⓧ) T1) #g1 #Hg1 -lapply (lsubr_lsubf … Hg1 … Hf1) -Hf1 /2 width=1 by lsubr_unit/ #Hfg1 -/5 width=10 by lsubf_fwd_sle, lveq_bind, sle_trans, ex4_4_intro/ (**) (* full auto too slow *) -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma index f55500bd1..3963c91bd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma @@ -31,8 +31,8 @@ interpretation (* Basic properties ***********************************************************) -lemma frees_tdeq_conf_lexs: ∀h,o,f,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f → ∀T2. T1 ≛[h, o] T2 → - ∀L2. L1 ≛[h, o, f] L2 → L2 ⊢ 𝐅*⦃T2⦄ ≡ f. +lemma frees_tdeq_conf_lfdeq: ∀h,o,f,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f → ∀T2. T1 ≛[h, o] T2 → + ∀L2. L1 ≛[h, o, f] L2 → L2 ⊢ 𝐅*⦃T2⦄ ≡ f. #h #o #f #L1 #T1 #H elim H -f -L1 -T1 [ #f #L1 #s1 #Hf #X #H1 #L2 #_ elim (tdeq_inv_sort1 … H1) -H1 #s2 #d #_ #_ #H destruct @@ -67,26 +67,17 @@ qed-. lemma frees_tdeq_conf: ∀h,o,f,L,T1. L ⊢ 𝐅*⦃T1⦄ ≡ f → ∀T2. T1 ≛[h, o] T2 → L ⊢ 𝐅*⦃T2⦄ ≡ f. -/4 width=7 by frees_tdeq_conf_lexs, lexs_refl, ext2_refl/ qed-. +/4 width=7 by frees_tdeq_conf_lfdeq, lexs_refl, ext2_refl/ qed-. -lemma frees_lexs_conf: ∀h,o,f,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f → - ∀L2. L1 ≛[h, o, f] L2 → L2 ⊢ 𝐅*⦃T⦄ ≡ f. -/2 width=7 by frees_tdeq_conf_lexs, tdeq_refl/ qed-. - -lemma frees_lfdeq_conf_lexs: ∀h,o. lexs_frees_confluent (cdeq_ext h o) cfull. -/3 width=7 by frees_tdeq_conf_lexs, ex2_intro/ qed-. +lemma frees_lfdeq_conf: ∀h,o,f,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f → + ∀L2. L1 ≛[h, o, f] L2 → L2 ⊢ 𝐅*⦃T⦄ ≡ f. +/2 width=7 by frees_tdeq_conf_lfdeq, tdeq_refl/ 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-. -(* Basic_2A1: uses: lleq_sym *) -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/ -qed-. - lemma lfdeq_atom: ∀h,o,I. ⋆ ≛[h, o, ⓪{I}] ⋆. /2 width=1 by lfxs_atom/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma index 37a33504f..1c7dee495 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma @@ -12,17 +12,21 @@ (* *) (**************************************************************************) +include "basic_2/syntax/lveq_length.ma". include "basic_2/relocation/lifts_tdeq.ma". include "basic_2/static/lfxs_length.ma". include "basic_2/static/lfdeq.ma". (* DEGREE-BASED EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ******) -(* Forward lemmas with length for local environments ************************) +(* Advanved properties ******************************************************) -(* Basic_2A1: lleq_fwd_length *) -lemma lfdeq_fwd_length: ∀h,o,L1,L2. ∀T:term. L1 ≛[h, o, T] L2 → |L1| = |L2|. -/2 width=3 by lfxs_fwd_length/ qed-. +lemma lfdeq_fle_comp: ∀h,o. lfxs_fle_compatible (cdeq h o). +#h #o #L1 #L2 #T * #f1 #Hf1 #HL12 +lapply (frees_lfdeq_conf h o … Hf1 … HL12) +lapply (lexs_fwd_length … HL12) +/3 width=8 by lveq_length_eq, ex4_4_intro/ (**) (* full auto fails *) +qed-. (* Properties with length for local environments ****************************) @@ -31,3 +35,10 @@ lemma lfdeq_lifts_bi: ∀L1,L2. |L1| = |L2| → ∀h,o,K1,K2,T. K1 ≛[h, o, T] ∀b,f. ⬇*[b, f] L1 ≡ K1 → ⬇*[b, f] L2 ≡ K2 → ∀U. ⬆*[f] T ≡ U → L1 ≛[h, o, U] L2. /3 width=9 by lfxs_lifts_bi, tdeq_lifts_sn/ qed-. + +(* Forward lemmas with length for local environments ************************) + +(* Basic_2A1: lleq_fwd_length *) +lemma lfdeq_fwd_length: ∀h,o,L1,L2. ∀T:term. L1 ≛[h, o, T] L2 → |L1| = |L2|. +/2 width=3 by lfxs_fwd_length/ qed-. + diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma index 2edd66b91..2fae91f39 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma @@ -15,12 +15,16 @@ include "basic_2/syntax/ext2_ext2.ma". include "basic_2/syntax/tdeq_tdeq.ma". include "basic_2/static/lfxs_lfxs.ma". -include "basic_2/static/lfdeq.ma". +include "basic_2/static/lfdeq_length.ma". (* DEGREE-BASED EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ******) (* Advanced properties ******************************************************) +(* Basic_2A1: uses: lleq_sym *) +lemma lfdeq_sym: ∀h,o,T. symmetric … (lfdeq h o T). +/3 width=3 by lfdeq_fle_comp, lfxs_sym, tdeq_sym/ qed-. + (* Basic_2A1: uses: lleq_dec *) lemma lfdeq_dec: ∀h,o,L1,L2. ∀T:term. Decidable (L1 ≛[h, o, T] L2). /3 width=1 by lfxs_dec, tdeq_dec/ qed-. @@ -46,7 +50,7 @@ theorem lfdeq_bind_void: ∀h,o,p,I,L1,L2,V,T. (* Basic_2A1: uses: lleq_trans *) theorem lfdeq_trans: ∀h,o,T. Transitive … (lfdeq h o T). #h #o #T #L1 #L * #f1 #Hf1 #HL1 #L2 * #f2 #Hf2 #HL2 -lapply (frees_tdeq_conf_lexs … Hf1 T … HL1) // #H0 +lapply (frees_tdeq_conf_lfdeq … Hf1 T … HL1) // #H0 lapply (frees_mono … Hf2 … H0) -Hf2 -H0 /5 width=7 by lexs_trans, lexs_eq_repl_back, tdeq_trans, ext2_trans, ex2_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 80ed1c081..0e7e900d5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma @@ -12,11 +12,10 @@ (* *) (**************************************************************************) -include "ground_2/relocation/rtmap_id.ma". include "basic_2/notation/relations/relationstar_4.ma". include "basic_2/syntax/cext2.ma". include "basic_2/relocation/lexs.ma". -include "basic_2/static/frees.ma". +include "basic_2/static/fle.ma". (* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) @@ -26,16 +25,11 @@ definition lfxs (R) (T): relation lenv ≝ interpretation "generic extension on referred entries (local environment)" 'RelationStar R T L1 L2 = (lfxs R T L1 L2). -definition R_frees_confluent: predicate (relation3 …) ≝ - λRN. - ∀f1,L,T1. L ⊢ 𝐅*⦃T1⦄ ≡ f1 → ∀T2. RN L T1 T2 → - ∃∃f2. L ⊢ 𝐅*⦃T2⦄ ≡ f2 & f2 ⊆ f1. +definition R_fle_compatible: predicate (relation3 …) ≝ λRN. + ∀L,T1,T2. RN L T1 T2 → ⦃L, T2⦄ ⊆ ⦃L, T1⦄. -definition lexs_frees_confluent: relation (relation3 …) ≝ - λRN,RP. - ∀f1,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f1 → - ∀L2. L1 ⪤*[RN, RP, f1] L2 → - ∃∃f2. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 & f2 ⊆ f1. +definition lfxs_fle_compatible: predicate (relation3 …) ≝ λRN. + ∀L1,L2,T. L1 ⪤*[RN, T] L2 → ⦃L2, T⦄ ⊆ ⦃L1, T⦄. definition R_confluent2_lfxs: relation4 (relation3 lenv term term) (relation3 lenv term term) … ≝ @@ -304,13 +298,6 @@ lemma lfxs_bind_repl_dx: ∀R,I,I1,L1,L2,T. /3 width=5 by lexs_pair_repl, ex2_intro/ qed-. -lemma lfxs_sym: ∀R. lexs_frees_confluent (cext2 R) cfull → - (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) → - ∀T. symmetric … (lfxs R T). -#R #H1R #H2R #T #L1 #L2 * #f1 #Hf1 #HL12 elim (H1R … Hf1 … HL12) -Hf1 -/5 width=5 by sle_lexs_trans, lexs_sym, cext2_sym, ex2_intro/ -qed-. - (* Basic_2A1: uses: llpx_sn_co *) lemma lfxs_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) → ∀L1,L2,T. L1 ⪤*[R1, T] L2 → L1 ⪤*[R2, T] L2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_fle.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_fle.ma deleted file mode 100644 index cc067e50a..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_fle.ma +++ /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 "basic_2/syntax/lveq_length.ma". -include "basic_2/static/fle.ma". -include "basic_2/static/lfxs_lfxs.ma". - -(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) - -(* Properties with free variables inclusion for restricted closures *********) - -(* Note: we just need lveq_inv_refl: ∀L,n1,n2. L ≋ⓧ*[n1, n2] L → ∧∧ 0 = n1 & 0 = n2 *) -lemma fle_lfxs_trans: ∀R,L1,T1,T2. ⦃L1, T1⦄ ⊆ ⦃L1, T2⦄ → - ∀L2. L1 ⪤*[R, T2] L2 → L1 ⪤*[R, T1] L2. -#R #L1 #T1 #T2 * #n1 #n2 #f1 #f2 #Hf1 #Hf2 #Hn #Hf #L2 #HL12 -elim (lveq_inj_length … Hn ?) // #H1 #H2 destruct -/4 width=5 by lfxs_inv_frees, sle_lexs_trans, ex2_intro/ -qed-. 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 89949c4b0..f827a1f20 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma @@ -12,19 +12,51 @@ (* *) (**************************************************************************) +include "basic_2/relocation/lexs_length.ma". include "basic_2/relocation/lexs_lexs.ma". include "basic_2/static/frees_drops.ma". +include "basic_2/static/fle_fle.ma". include "basic_2/static/lfxs.ma". (* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) -(* Advanced properties ******************************************************) +(* Advanced inversion lemmas ************************************************) lemma lfxs_inv_frees: ∀R,L1,L2,T. L1 ⪤*[R, T] L2 → ∀f. L1 ⊢ 𝐅*⦃T⦄ ≡ f → L1 ⪤*[cext2 R, cfull, f] L2. #R #L1 #L2 #T * /3 width=6 by frees_mono, lexs_eq_repl_back/ qed-. +lemma frees_lexs_conf: ∀R. lfxs_fle_compatible R → + ∀L1,T,f1. L1 ⊢ 𝐅*⦃T⦄ ≡ f1 → + ∀L2. L1 ⪤*[cext2 R, cfull, f1] L2 → + ∃∃f2. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 & f2 ⊆ f1. +#R #HR #L1 #T #f1 #Hf1 #L2 #H1L +lapply (HR L1 L2 T ?) /2 width=3 by ex2_intro/ #H2L +@(fle_frees_trans_eq … H2L … Hf1) /3 width=4 by lexs_fwd_length, sym_eq/ +qed-. + +(* Properties with free variables inclusion for restricted closures *********) + +(* Note: we just need lveq_inv_refl: ∀L,n1,n2. L ≋ⓧ*[n1, n2] L → ∧∧ 0 = n1 & 0 = n2 *) +lemma fle_lfxs_trans: ∀R,L1,T1,T2. ⦃L1, T1⦄ ⊆ ⦃L1, T2⦄ → + ∀L2. L1 ⪤*[R, T2] L2 → L1 ⪤*[R, T1] L2. +#R #L1 #T1 #T2 * #n1 #n2 #f1 #f2 #Hf1 #Hf2 #Hn #Hf #L2 #HL12 +elim (lveq_inj_length … Hn ?) // #H1 #H2 destruct +/4 width=5 by lfxs_inv_frees, sle_lexs_trans, ex2_intro/ +qed-. + +(* Advanced properties ******************************************************) + +lemma lfxs_sym: ∀R. lfxs_fle_compatible R → + (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) → + ∀T. symmetric … (lfxs R T). +#R #H1R #H2R #T #L1 #L2 +* #f1 #Hf1 #HL12 +elim (frees_lexs_conf … Hf1 … HL12) -Hf1 // +/5 width=5 by sle_lexs_trans, lexs_sym, cext2_sym, ex2_intro/ +qed-. + (* Basic_2A1: uses: llpx_sn_dec *) lemma lfxs_dec: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) → ∀L1,L2,T. Decidable (L1 ⪤*[R, T] L2). @@ -35,7 +67,7 @@ elim (lexs_dec (cext2 R) cfull … L1 L2 f) qed-. lemma lfxs_pair_sn_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) → - lexs_frees_confluent … (cext2 R1) cfull → + lfxs_fle_compatible R1 → ∀L1,L2,V. L1 ⪤*[R1, V] L2 → ∀I,T. ∃∃L. L1 ⪤*[R1, ②{I}V.T] L & L ⪤*[R2, V] L2. #R1 #R2 #HR1 #HR2 #HR #L1 #L2 #V * #f #Hf #HL12 * [ #p ] #I #T @@ -49,12 +81,12 @@ lapply (sor_eq_repl_back1 … Hy … H1) -y1 #Hy lapply (sor_inv_sle_sn … Hy) -y2 #Hfg elim (lexs_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #L #HL1 #HL2 lapply (sle_lexs_trans … HL1 … Hfg) // #H -elim (HR … Hf … H) -HR -Hf -H +elim (frees_lexs_conf … Hf … H) -Hf -H /4 width=7 by sle_lexs_trans, ex2_intro/ qed-. lemma lfxs_flat_dx_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) → - lexs_frees_confluent … (cext2 R1) cfull → + lfxs_fle_compatible R1 → ∀L1,L2,T. L1 ⪤*[R1, T] L2 → ∀I,V. ∃∃L. L1 ⪤*[R1, ⓕ{I}V.T] L & L ⪤*[R2, T] L2. #R1 #R2 #HR1 #HR2 #HR #L1 #L2 #T * #f #Hf #HL12 #I #V @@ -65,12 +97,12 @@ lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy lapply (sor_inv_sle_dx … Hy) -y1 #Hfg elim (lexs_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #L #HL1 #HL2 lapply (sle_lexs_trans … HL1 … Hfg) // #H -elim (HR … Hf … H) -HR -Hf -H +elim (frees_lexs_conf … Hf … H) -Hf -H /4 width=7 by sle_lexs_trans, ex2_intro/ qed-. lemma lfxs_bind_dx_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) → - lexs_frees_confluent … (cext2 R1) cfull → + lfxs_fle_compatible R1 → ∀I,L1,L2,V1,T. L1.ⓑ{I}V1 ⪤*[R1, T] L2 → ∀p. ∃∃L,V. L1 ⪤*[R1, ⓑ{p,I}V1.T] L & L.ⓑ{I}V ⪤*[R2, T] L2 & R1 L1 V1 V. #R1 #R2 #HR1 #HR2 #HR #I #L1 #L2 #V1 #T * #f #Hf #HL12 #p @@ -85,12 +117,12 @@ elim (lexs_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by lapply (sle_lexs_trans … H … Hfg) // #H0 elim (lexs_inv_next1 … H) -H #Z #L #HL1 #H elim (ext2_inv_pair_sn … H) -H #V #HV #H1 #H2 destruct -elim (HR … Hf … H0) -HR -Hf -H0 +elim (frees_lexs_conf … Hf … H0) -Hf -H0 /4 width=7 by sle_lexs_trans, ex3_2_intro, ex2_intro/ qed-. lemma lfxs_bind_dx_split_void: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) → - lexs_frees_confluent … (cext2 R1) cfull → + lfxs_fle_compatible R1 → ∀L1,L2,T. L1.ⓧ ⪤*[R1, T] L2 → ∀p,I,V. ∃∃L. L1 ⪤*[R1, ⓑ{p,I}V.T] L & L.ⓧ ⪤*[R2, T] L2. #R1 #R2 #HR1 #HR2 #HR #L1 #L2 #T * #f #Hf #HL12 #p #I #V @@ -105,7 +137,7 @@ elim (lexs_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by lapply (sle_lexs_trans … H … Hfg) // #H0 elim (lexs_inv_next1 … H) -H #Z #L #HL1 #H elim (ext2_inv_unit_sn … H) -H #H destruct -elim (HR … Hf … H0) -HR -Hf -H0 +elim (frees_lexs_conf … Hf … H0) -Hf -H0 /4 width=7 by sle_lexs_trans, ex2_intro/ (* note: 2 ex2_intro *) qed-. @@ -137,8 +169,8 @@ lapply (lexs_fwd_bind … Hf2) -Hf2 #Hf2 elim (sor_isfin_ex f1 (⫱f2)) qed. theorem lfxs_conf: ∀R1,R2. - lexs_frees_confluent (cext2 R1) cfull → - lexs_frees_confluent (cext2 R2) cfull → + lfxs_fle_compatible R1 → + lfxs_fle_compatible R2 → 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 @@ -146,8 +178,8 @@ 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 (HR1 … Hf … HL01) -HL01 #f1 #Hf1 #H1 - elim (HR2 … Hf … HL02) -HL02 #f2 #Hf2 #H2 + elim (frees_lexs_conf … Hf … HL01) // -HR1 -HL01 #f1 #Hf1 #H1 + elim (frees_lexs_conf … Hf … HL02) // -HR2 -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/ 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 fb78039ee..13c02988a 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 @@ -180,11 +180,11 @@ table { } ] [ { "generic extension of a context-sensitive relation" * } { - [ [ "for lenvs on referred entries" ] "lfxs ( ? ⦻*[?,?] ? )" "lfxs_length" + "lfxs_lex" + "lfxs_drops" + "lfxs_fqup" + "flxs_fle" + "lfxs_lfxs" * ] + [ [ "for lenvs on referred entries" ] "lfxs ( ? ⦻*[?,?] ? )" "lfxs_length" + "lfxs_lex" + "lfxs_drops" + "lfxs_fqup" + "lfxs_lfxs" * ] } ] [ { "context-sensitive free variables" * } { - [ [ "inclusion for restricted closures" ] "fle ( ⦃?,?⦄ ⊆ ⦃?,?⦄ )" "fle_drops" + "fle_fqup" + "fle_lsubf" + "fle_fle" * ] + [ [ "inclusion for restricted closures" ] "fle ( ⦃?,?⦄ ⊆ ⦃?,?⦄ )" "fle_drops" + "fle_fqup" + "fle_fle" * ] [ [ "restricted refinement for lenvs" ] "lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )" "lsubf_lsubr" + "lsubf_frees" + "lsubf_lsubf" * ] [ [ "for terms" ] "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_drops" + "frees_fqup" + "frees_frees" * ] } -- 2.39.2