From c44a7c4d35c1bb9651c3596519d8262e52e90ff4 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 24 Nov 2017 19:59:28 +0000 Subject: [PATCH] - equivalence between lfpxs and lpxs + lfeq proved - more descriptions in basic_2_src.tbl --- .../basic_2/i_static/tc_lfxs_lex.ma | 8 +-- .../lambdadelta/basic_2/relocation/lex.ma | 54 +++++++++++----- .../lambdadelta/basic_2/relocation/lex_tc.ma | 32 ++++++++++ .../basic_2/rt_computation/cpxs_lpx.ma | 42 +++++++++++++ .../basic_2/rt_computation/lfpxs_lpxs.ma | 11 +--- .../basic_2/rt_computation/partial.txt | 4 +- .../basic_2/rt_transition/cpx_lfeq.ma | 63 +++++++++++++++++++ .../lambdadelta/basic_2/rt_transition/lpx.ma | 46 +++++++++----- .../lambdadelta/basic_2/static/lfeq.ma | 32 ++++++++++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 25 ++++---- 10 files changed, 262 insertions(+), 55 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/lex_tc.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lpx.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfeq.ma 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 dbcf5fe44..45bf6a472 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 @@ -12,9 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/syntax/ext2_tc.ma". -include "basic_2/relocation/lexs_tc.ma". -include "basic_2/relocation/lex.ma". +include "basic_2/relocation/lex_tc.ma". include "basic_2/static/lfeq_fqup.ma". include "basic_2/static/lfeq_lfeq.ma". include "basic_2/i_static/tc_lfxs_fqup.ma". @@ -36,13 +34,15 @@ lemma tc_lfxs_lex_lfeq: ∀R. c_reflexive … R → (* Inversion lemmas with generic extension of a context sensitive relation **) +(* 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 → - s_rs_transitive_isid cfull (cext2 R) → + s_rs_transitive … R (λ_.lex R) → lfeq_transitive R → ∀L1,L2,T. L1 ⪤**[R, T] L2 → ∃∃L. L1 ⪤[LTC … R] L & L ≡[T] L2. #R #H1R #H2R #H3R #H4R #L1 #L2 #T #H +lapply (s_rs_transitive_lex_inv_isid … H3R) -H3R #H3R @(tc_lfxs_ind_sn … H1R … H) -H -L2 [ /4 width=3 by lfeq_refl, lex_refl, inj, ex2_intro/ | #L0 #L2 #_ #HL02 * #L * #f0 #Hf0 #HL1 #HL0 diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lex.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lex.ma index 3067deb2a..7e4e03c8e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lex.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lex.ma @@ -17,7 +17,7 @@ include "basic_2/notation/relations/relation_3.ma". include "basic_2/syntax/cext2.ma". include "basic_2/relocation/lexs.ma". -(* GENERIC EXTENSION OF A CONTEXT-SENSITIVE REALTION ON TERMS ***************) +(* GENERIC EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS **************) (* Basic_2A1: includes: lpx_sn_atom lpx_sn_pair *) definition lex: (lenv → relation term) → relation lenv ≝ @@ -28,10 +28,22 @@ interpretation "generic extension (local environment)" (* Basic properties *********************************************************) +lemma lex_bind: ∀R,I1,I2,K1,K2. K1 ⪤[R] K2 → cext2 R K1 I1 I2 → + K1.ⓘ{I1} ⪤[R] K2.ⓘ{I2}. +#R #I1 #I2 #K1 #K2 * #f #Hf #HK12 #HI12 +/3 width=3 by lexs_push, isid_push, ex2_intro/ +qed. + (* Basic_2A1: was: lpx_sn_refl *) lemma lex_refl: ∀R. c_reflexive … R → reflexive … (lex R). /4 width=3 by lexs_refl, ext2_refl, ex2_intro/ qed. +(* Advanced properties ******************************************************) + +lemma lex_bind_refl_dx: ∀R. c_reflexive … R → + ∀I,K1,K2. K1 ⪤[R] K2 → K1.ⓘ{I} ⪤[R] K2.ⓘ{I}. +/3 width=3 by ext2_refl, lex_bind/ qed. + (* Basic inversion lemmas ***************************************************) (* Basic_2A1: was: lpx_sn_inv_atom1: *) @@ -39,14 +51,12 @@ lemma lex_inv_atom_sn: ∀R,L2. ⋆ ⪤[R] L2 → L2 = ⋆. #R #L2 * #f #Hf #H >(lexs_inv_atom1 … H) -L2 // qed-. -(* Basic_2A1: was: lpx_sn_inv_pair1 *) -lemma lex_inv_pair_sn: ∀R,I,L2,K1,V1. K1.ⓑ{I}V1 ⪤[R] L2 → - ∃∃K2,V2. K1 ⪤[R] K2 & R K1 V1 V2 & L2 = K2.ⓑ{I}V2. -#R #I #L2 #K1 #V1 * #f #Hf #H +lemma lex_inv_bind_sn: ∀R,I1,L2,K1. K1.ⓘ{I1} ⪤[R] L2 → + ∃∃I2,K2. K1 ⪤[R] K2 & cext2 R K1 I1 I2 & L2 = K2.ⓘ{I2}. +#R #I1 #L2 #K1 * #f #Hf #H lapply (lexs_eq_repl_fwd … H (↑f) ?) -H /2 width=1 by eq_push_inv_isid/ #H -elim (lexs_inv_push1 … H) -H #Z2 #K2 #HK12 #HZ2 #H destruct -elim (ext2_inv_pair_sn … HZ2) -HZ2 #V2 #HV12 #H destruct -/3 width=5 by ex3_2_intro, ex2_intro/ +elim (lexs_inv_push1 … H) -H #I2 #K2 #HK12 #HI12 #H destruct +/3 width=5 by ex2_intro, ex3_2_intro/ qed-. (* Basic_2A1: was: lpx_sn_inv_atom2 *) @@ -54,18 +64,34 @@ lemma lex_inv_atom_dx: ∀R,L1. L1 ⪤[R] ⋆ → L1 = ⋆. #R #L1 * #f #Hf #H >(lexs_inv_atom2 … H) -L1 // qed-. -(* Basic_2A1: was: lpx_sn_inv_pair2 *) -lemma lex_inv_pair_dx: ∀R,I,L1,K2,V2. L1 ⪤[R] K2.ⓑ{I}V2 → - ∃∃K1,V1. K1 ⪤[R] K2 & R K1 V1 V2 & L1 = K1.ⓑ{I}V1. -#R #I #L1 #K2 #V2 * #f #Hf #H +lemma lex_inv_bind_dx: ∀R,I2,L1,K2. L1 ⪤[R] K2.ⓘ{I2} → + ∃∃I1,K1. K1 ⪤[R] K2 & cext2 R K1 I1 I2 & L1 = K1.ⓘ{I1}. +#R #I2 #L1 #K2 * #f #Hf #H lapply (lexs_eq_repl_fwd … H (↑f) ?) -H /2 width=1 by eq_push_inv_isid/ #H -elim (lexs_inv_push2 … H) -H #Z1 #K1 #HK12 #HZ1 #H destruct -elim (ext2_inv_pair_dx … HZ1) -HZ1 #V1 #HV12 #H destruct +elim (lexs_inv_push2 … H) -H #I1 #K1 #HK12 #HI12 #H destruct /3 width=5 by ex3_2_intro, ex2_intro/ qed-. (* Advanced inversion lemmas ************************************************) +(* Basic_2A1: was: lpx_sn_inv_pair1 *) +lemma lex_inv_pair_sn: ∀R,I,L2,K1,V1. K1.ⓑ{I}V1 ⪤[R] L2 → + ∃∃K2,V2. K1 ⪤[R] K2 & R K1 V1 V2 & L2 = K2.ⓑ{I}V2. +#R #I #L2 #K1 #V1 #H +elim (lex_inv_bind_sn … H) -H #Z2 #K2 #HK12 #HZ2 #H destruct +elim (ext2_inv_pair_sn … HZ2) -HZ2 #V2 #HV12 #H destruct +/2 width=5 by ex3_2_intro/ +qed-. + +(* Basic_2A1: was: lpx_sn_inv_pair2 *) +lemma lex_inv_pair_dx: ∀R,I,L1,K2,V2. L1 ⪤[R] K2.ⓑ{I}V2 → + ∃∃K1,V1. K1 ⪤[R] K2 & R K1 V1 V2 & L1 = K1.ⓑ{I}V1. +#R #I #L1 #K2 #V2 #H +elim (lex_inv_bind_dx … H) -H #Z1 #K1 #HK12 #HZ1 #H destruct +elim (ext2_inv_pair_dx … HZ1) -HZ1 #V1 #HV12 #H destruct +/2 width=5 by ex3_2_intro/ +qed-. + (* Basic_2A1: was: lpx_sn_inv_pair *) lemma lex_inv_pair: ∀R,I1,I2,L1,L2,V1,V2. L1.ⓑ{I1}V1 ⪤[R] L2.ⓑ{I2}V2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lex_tc.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lex_tc.ma new file mode 100644 index 000000000..bb3aec919 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lex_tc.ma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||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/ext2_tc.ma". +include "basic_2/relocation/lexs_tc.ma". +include "basic_2/relocation/lex.ma". + +(* GENERIC EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS **************) + +(* Inversion lemmas with transitive closure *********************************) + +lemma s_rs_transitive_lex_inv_isid: ∀R. s_rs_transitive … R (λ_.lex R) → + s_rs_transitive_isid cfull (cext2 R). +#R #HR #f #Hf #L2 #T1 #T2 #H #L1 #HL12 +elim (ext2_tc … H) -H +[ /3 width=1 by ext2_inv_tc, ext2_unit/ +| #I #V1 #V2 #HV12 + @ext2_inv_tc @ext2_pair + @(HR … HV12) -HV12 /2 width=3 by ex2_intro/ (**) (* auto fails *) +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lpx.ma new file mode 100644 index 000000000..c4fcab186 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lpx.ma @@ -0,0 +1,42 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_transition/lpx.ma". +include "basic_2/rt_computation/cpxs_drops.ma". +include "basic_2/rt_computation/cpxs_cpxs.ma". + +(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************) + +(* Properties with uncounted parallel rt-transition for local environments **) + +lemma lpx_cpx_trans: ∀h,G. s_r_transitive … (cpx h G) (λ_.lpx h G). +#h #G #L2 #T1 #T2 #H @(cpx_ind … H) -G -L2 -T1 -T2 +[ /2 width=3 by/ +| /3 width=2 by cpx_cpxs, cpx_ess/ +| #I #G #K2 #V2 #V4 #W4 #_ #IH #HVW4 #L1 #H + elim (lpx_inv_pair_dx … H) -H #K1 #V1 #HK12 #HV12 #H destruct + /4 width=3 by cpxs_delta, cpxs_strap2/ +| #I2 #G #K2 #T #U #i #_ #IH #HTU #L1 #H + elim (lpx_inv_bind_dx … H) -H #I1 #K1 #HK12 #HI12 #H destruct + /4 width=3 by cpxs_lref, cpxs_strap2/ +|5,10: /4 width=1 by cpxs_beta, cpxs_bind, lpx_bind_refl_dx/ +|6,8,9: /3 width=1 by cpxs_flat, cpxs_ee, cpxs_eps/ +| /4 width=3 by cpxs_zeta, lpx_bind_refl_dx/ +| /4 width=3 by cpxs_theta, cpxs_strap1, lpx_bind_refl_dx/ +] +qed-. + +lemma lpx_cpxs_trans: ∀h,G. s_rs_transitive … (cpx h G) (λ_.lpx h G). +#h #G @s_r_trans_LTC1 /2 width=3 by lpx_cpx_trans/ (**) (* full auto fails *) +qed-. 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 98f23aff9..7839a4b3d 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 @@ -13,7 +13,8 @@ (**************************************************************************) include "basic_2/i_static/tc_lfxs_lex.ma". -include "basic_2/rt_transition/lfpx_frees.ma". +include "basic_2/rt_transition/cpx_lfeq.ma". +include "basic_2/rt_computation/cpxs_lpx.ma". include "basic_2/rt_computation/lpxs.ma". include "basic_2/rt_computation/lfpxs.ma". @@ -27,12 +28,6 @@ lemma lfpxs_lpxs_lfeq: ∀h,G,L1,L. ⦃G, L1⦄ ⊢ ⬈*[h] L → (* Inversion lemmas with uncounted parallel rt-computation for local envs ***) -lemma lpx_cpxs_ext_trans: ∀h,G. s_rs_transitive_isid cfull (cpx_ext h G). -#H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 - - lemma tc_lfxs_inv_lex_lfeq: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → ∃∃L. ⦃G, L1⦄ ⊢ ⬈*[h] L & L ≡[T] L2. -#h #G @tc_lfxs_inv_lex_lfeq // -[ @lfpx_frees_conf -| @lpx_cpxs_ext_trans \ No newline at end of file +/3 width=5 by lfpx_frees_conf, lpx_cpxs_trans, lfeq_cpx_trans, tc_lfxs_inv_lex_lfeq/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt index 66da92c66..519cd481c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -1,6 +1,6 @@ -cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_fqus.ma cpxs_lsubr.ma cpxs_lfdeq.ma cpxs_aaa.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma +cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_fqus.ma cpxs_lsubr.ma cpxs_lfdeq.ma cpxs_aaa.ma cpxs_lpx.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma lpxs.ma -lfpxs.ma lfpxs_length.ma lfpxs_drops.ma lfpxs_fqup.ma lfpxs_lfdeq.ma lfpxs_aaa.ma lfpxs_cpxs.ma lfpxs_lfpxs.ma +lfpxs.ma lfpxs_length.ma lfpxs_drops.ma lfpxs_fqup.ma lfpxs_lfdeq.ma lfpxs_aaa.ma lfpxs_cpxs.ma lfpxs_lpxs.ma lfpxs_lfpxs.ma csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_lsubr.ma csx_lfdeq.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_lfpxs.ma csx_csx.ma csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma lfsx.ma lfsx_drops.ma lfsx_fqup.ma lfsx_lfpxs.ma lfsx_lfsx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfeq.ma new file mode 100644 index 000000000..5ffcd5b44 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfeq.ma @@ -0,0 +1,63 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lfeq.ma". +include "basic_2/rt_transition/cpx_lfxs.ma". + +(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************) + +(* Properties with syntactic equivalence for lenvs on referred entries ******) + +(* Basic_2A1: was: lleq_cpx_trans *) +lemma lfeq_cpx_trans: ∀h,G. lfeq_transitive (cpx h G). +#h #G #L2 #T1 #T2 #H @(cpx_ind … H) -G -L2 -T1 -T2 /2 width=2 by cpx_ess/ +[ #I #G #K2 #V1 #V2 #W2 #_ #IH #HVW2 #L1 #H + elim (lfeq_inv_zero_pair_dx … H) -H #K1 #HK12 #H destruct + /3 width=3 by cpx_delta/ +| #I2 #G #K2 #T #U #i #_ #IH #HTU #L1 #H + elim (lfeq_inv_lref_bind_dx … H) -H #I1 #K1 #HK12 #H destruct + /3 width=3 by cpx_lref/ +| #p #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H + elim (lfeq_inv_bind … H) -H /3 width=1 by cpx_bind/ +| #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H + elim (lfeq_inv_flat … H) -H /3 width=1 by cpx_flat/ +| #G #L2 #V2 #T1 #T #T2 #_ #HT2 #IH #L1 #H + elim (lfeq_inv_bind … H) -H /3 width=3 by cpx_zeta/ +| #G #L2 #W1 #T1 #T2 #_ #IH #L1 #H + elim (lfeq_inv_flat … H) -H /3 width=1 by cpx_eps/ +| #G #L2 #W1 #W2 #T1 #_ #IH #L1 #H + elim (lfeq_inv_flat … H) -H /3 width=1 by cpx_ee/ +| #p #G #L2 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #H + elim (lfeq_inv_flat … H) -H #HV1 #H + elim (lfeq_inv_bind … H) -H /3 width=1 by cpx_beta/ +| #p #G #L2 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV1 #IHW12 #IHT12 #HV2 #L1 #H + elim (lfeq_inv_flat … H) -H #HV1 #H + elim (lfeq_inv_bind … H) -H /3 width=3 by cpx_theta/ +] +qed-. +(* +(* Basic_2A1: was: cpx_lleq_conf *) +lemma cpx_lfeq_conf: ∀h,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ⬈[h] T2 → + ∀L1. L2 ≡[T1] L1 → ⦃G, L1⦄ ⊢ T1 ⬈[h] T2. +/3 width=3 by lfeq_cpx_trans, lfeq_sym/ qed-. +*) +(* Basic_2A1: was: cpx_lleq_conf_sn *) +lemma cpx_lfeq_conf_sn: ∀h,G. s_r_confluent1 … (cpx h G) lfeq. +/2 width=5 by cpx_lfxs_conf/ qed-. +(* +(* Basic_2A1: was: cpx_lleq_conf_dx *) +lemma cpx_lfeq_conf_dx: ∀h,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ⬈[h] T2 → + ∀L1. L1 ≡[T1] L2 → L1 ≡[T2] L2. +/4 width=6 by cpx_lfeq_conf_sn, lfeq_sym/ qed-. +*) \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx.ma index cde540dcc..a5d9966be 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx.ma @@ -14,7 +14,7 @@ include "basic_2/notation/relations/predtysn_4.ma". include "basic_2/relocation/lex.ma". -include "basic_2/rt_transition/cpx.ma". +include "basic_2/rt_transition/cpx_ext.ma". (* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENVIRONMENTS ******************) @@ -27,39 +27,57 @@ interpretation (* Basic properties *********************************************************) +lemma lpx_bind: ∀h,G,K1,K2. ⦃G, K1⦄ ⊢ ⬈[h] K2 → + ∀I1,I2. ⦃G, K1⦄ ⊢ I1 ⬈[h] I2 → ⦃G, K1.ⓘ{I1}⦄ ⊢ ⬈[h] K2.ⓘ{I2}. +/2 width=1 by lex_bind/ qed. + +lemma lpx_refl: ∀h,G. reflexive … (lpx h G). +/2 width=1 by lex_refl/ qed. + +(* Advanced properties ******************************************************) + +lemma lpx_bind_refl_dx: ∀h,G,K1,K2. ⦃G, K1⦄ ⊢ ⬈[h] K2 → + ∀I. ⦃G, K1.ⓘ{I}⦄ ⊢ ⬈[h] K2.ⓘ{I}. +/2 width=1 by lex_bind_refl_dx/ qed. (* lemma lpx_pair: ∀h,g,I,G,K1,K2,V1,V2. ⦃G, K1⦄ ⊢ ⬈[h] K2 → ⦃G, K1⦄ ⊢ V1 ⬈[h] V2 → ⦃G, K1.ⓑ{I}V1⦄ ⊢ ⬈[h] K2.ⓑ{I}V2. /2 width=1 by lpx_sn_pair/ qed. *) - -lemma lpx_refl: ∀h,G. reflexive … (lpx h G). -/2 width=1 by lex_refl/ qed. - (* Basic inversion lemmas ***************************************************) (* Basic_2A1: was: lpx_inv_atom1 *) lemma lpx_inv_atom_sn: ∀h,G,L2. ⦃G, ⋆⦄ ⊢ ⬈[h] L2 → L2 = ⋆. /2 width=2 by lex_inv_atom_sn/ qed-. +lemma lpx_inv_bind_sn: ∀h,I1,G,L2,K1. ⦃G, K1.ⓘ{I1}⦄ ⊢ ⬈[h] L2 → + ∃∃I2,K2. ⦃G, K1⦄ ⊢ ⬈[h] K2 & ⦃G, K1⦄ ⊢ I1 ⬈[h] I2 & + L2 = K2.ⓘ{I2}. +/2 width=1 by lex_inv_bind_sn/ qed-. + +(* Basic_2A1: was: lpx_inv_atom2 *) +lemma lpx_inv_atom_dx: ∀h,G,L1. ⦃G, L1⦄ ⊢ ⬈[h] ⋆ → L1 = ⋆. +/2 width=2 by lex_inv_atom_dx/ qed-. + +lemma lpx_inv_bind_dx: ∀h,I2,G,L1,K2. ⦃G, L1⦄ ⊢ ⬈[h] K2.ⓘ{I2} → + ∃∃I1,K1. ⦃G, K1⦄ ⊢ ⬈[h] K2 & ⦃G, K1⦄ ⊢ I1 ⬈[h] I2 & + L1 = K1.ⓘ{I1}. +/2 width=1 by lex_inv_bind_dx/ qed-. + +(* Advanced inversion lemmas ************************************************) + (* Basic_2A1: was: lpx_inv_pair1 *) lemma lpx_inv_pair_sn: ∀h,I,G,L2,K1,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ⬈[h] L2 → ∃∃K2,V2. ⦃G, K1⦄ ⊢ ⬈[h] K2 & ⦃G, K1⦄ ⊢ V1 ⬈[h] V2 & L2 = K2.ⓑ{I}V2. /2 width=1 by lex_inv_pair_sn/ qed-. -(* Basic_2A1: was: lpx_inv_atom2 *) -lemma lpx_inv_atom_dx: ∀h,G,L1. ⦃G, L1⦄ ⊢ ⬈[h] ⋆ → L1 = ⋆. -/2 width=2 by lex_inv_atom_dx/ qed-. - (* Basic_2A1: was: lpx_inv_pair2 *) -lemma lpx_inv_pair2_dx: ∀h,I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ⬈[h] K2.ⓑ{I}V2 → - ∃∃K1,V1. ⦃G, K1⦄ ⊢ ⬈[h] K2 & ⦃G, K1⦄ ⊢ V1 ⬈[h] V2 & - L1 = K1.ⓑ{I}V1. +lemma lpx_inv_pair_dx: ∀h,I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ⬈[h] K2.ⓑ{I}V2 → + ∃∃K1,V1. ⦃G, K1⦄ ⊢ ⬈[h] K2 & ⦃G, K1⦄ ⊢ V1 ⬈[h] V2 & + L1 = K1.ⓑ{I}V1. /2 width=1 by lex_inv_pair_dx/ qed-. -(* Advanced inversion lemmas ************************************************) - lemma lpx_inv_pair: ∀h,I1,I2,G,L1,L2,V1,V2. ⦃G, L1.ⓑ{I1}V1⦄ ⊢ ⬈[h] L2.ⓑ{I2}V2 → ∧∧ ⦃G, L1⦄ ⊢ ⬈[h] L2 & ⦃G, L1⦄ ⊢ V1 ⬈[h] V2 & I1 = I2. /2 width=1 by lex_inv_pair/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma index 1b6257520..286a108ee 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma @@ -39,6 +39,38 @@ lemma lfxs_transitive_lfeq: ∀R. lfxs_transitive ceq R R → lfeq_transitive R. lemma lfeq_transitive_inv_lfxs: ∀R. lfeq_transitive R → lfxs_transitive ceq R R. /2 width=3 by/ qed-. +lemma lfeq_inv_bind: ∀p,I,L1,L2,V,T. L1 ≡[ⓑ{p,I}V.T] L2 → + ∧∧ L1 ≡[V] L2 & L1.ⓑ{I}V ≡[T] L2.ⓑ{I}V. +/2 width=2 by lfxs_inv_bind/ qed-. + +lemma lfeq_inv_flat: ∀I,L1,L2,V,T. L1 ≡[ⓕ{I}V.T] L2 → + ∧∧ L1 ≡[V] L2 & L1 ≡[T] L2. +/2 width=2 by lfxs_inv_flat/ qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma lfeq_inv_zero_pair_sn: ∀I,L2,K1,V. K1.ⓑ{I}V ≡[#0] L2 → + ∃∃K2. K1 ≡[V] K2 & L2 = K2.ⓑ{I}V. +#I #L2 #K1 #V #H +elim (lfxs_inv_zero_pair_sn … H) -H #K2 #X #HK12 #HX #H destruct +/2 width=3 by ex2_intro/ +qed-. + +lemma lfeq_inv_zero_pair_dx: ∀I,L1,K2,V. L1 ≡[#0] K2.ⓑ{I}V → + ∃∃K1. K1 ≡[V] K2 & L1 = K1.ⓑ{I}V. +#I #L1 #K2 #V #H +elim (lfxs_inv_zero_pair_dx … H) -H #K1 #X #HK12 #HX #H destruct +/2 width=3 by ex2_intro/ +qed-. + +lemma lfeq_inv_lref_bind_sn: ∀I1,K1,L2,i. K1.ⓘ{I1} ≡[#⫯i] L2 → + ∃∃I2,K2. K1 ≡[#i] K2 & L2 = K2.ⓘ{I2}. +/2 width=2 by lfxs_inv_lref_bind_sn/ qed-. + +lemma lfeq_inv_lref_bind_dx: ∀I2,K2,L1,i. L1 ≡[#⫯i] K2.ⓘ{I2} → + ∃∃I1,K1. K1 ≡[#i] K2 & L1 = K1.ⓘ{I1}. +/2 width=2 by lfxs_inv_lref_bind_dx/ qed-. + (* Basic forward lemmas *****************************************************) (* Basic_2A1: was: llpx_sn_lrefl *) 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 bfc628f28..dd6ed3880 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 @@ -111,9 +111,9 @@ table { [ [ "strongly normalizing for lenvs on referred entries" ] "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_lfpxs" + "lfsx_lfsx" * ] [ [ "strongly normalizing for term vectors" ] "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ] [ [ "strongly normalizing for terms" ] "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_lfdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ] - [ [ "for lenvs on referred entries" ] "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lfpxs" * ] + [ [ "for lenvs on referred entries" ] "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lpxs" + "lfpxs_lfpxs" * ] [ [ "for lenvs on all entries" ] "lpxs ( ⦃?,?⦄ ⊢ ⬈*[?] ? )" * ] - [ [ "for terms" ] "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_lfdeq" + "cpxs_aaa" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] + [ [ "for terms" ] "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_lfdeq" + "cpxs_aaa" + "cpxs_lpx" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] } ] } @@ -140,7 +140,7 @@ table { [ [ "for lenvs on referred entries" ] "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_cpx" + "lfpx_lfpx" * ] [ [ "for lenvs on all entries" ] "lpx ( ⦃?,?⦄ ⊢ ⬈[?] ? )" * ] [ [ "for binders" ] "cpx_ext ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" * ] - [ [ "for terms" ] "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfxs" * ] + [ [ "for terms" ] "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfxs" + "cpx_lfeq" * ] } ] [ { "counted context-sensitive parallel rt-transition" * } { @@ -214,24 +214,23 @@ table { ] class "orange" [ { "relocation" * } { - [ { "generic slicing for local environments" * } { - [ [ "" ] "drops_vector ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" * ] - [ [ "" ] "drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" "drops_lstar" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_lexs" + "drops_lreq" + "drops_drops" * ] + [ { "generic slicing" * } { + [ [ "for lenvs" ] "drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" "drops_lstar" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_lexs" + "drops_lreq" + "drops_drops" + "drops_vector" * ] } ] [ { "generic relocation" * } { - [ [ "" ] "lifts_bind ( ⬆*[?] ? ≡ ? )" "lifts_weight_bind" + "lifts_lifts_bind" * ] - [ [ "" ] "lifts_vector ( ⬆*[?] ? ≡ ? )" "lifts_lifts_vector" * ] - [ [ "" ] "lifts ( ⬆*[?] ? ≡ ? )" "lifts_simple" + "lifts_weight" + "lifts_tdeq" + "lifts_lifts" * ] + [ [ "for binders" ] "lifts_bind ( ⬆*[?] ? ≡ ? )" "lifts_weight_bind" + "lifts_lifts_bind" * ] + [ [ "for term vectors" ] "lifts_vector ( ⬆*[?] ? ≡ ? )" "lifts_lifts_vector" * ] + [ [ "for terms" ] "lifts ( ⬆*[?] ? ≡ ? )" "lifts_simple" + "lifts_weight" + "lifts_tdeq" + "lifts_lifts" * ] } ] - [ { "ranged equivalence for local environments" * } { - [ [ "" ] "lreq ( ? ≡[?] ? )" "lreq_length" + "lreq_lreq" * ] + [ { "syntactic equivalence" * } { + [ [ "for lenvs on selected entries" ] "lreq ( ? ≡[?] ? )" "lreq_length" + "lreq_lreq" * ] } ] [ { "generic entrywise extension" * } { - [ [ "" ] "lex ( ? ⦻[?] ? )" * ] - [ [ "" ] "lexs ( ? ⦻*[?,?,?] ? )" "lexs_tc" + "lexs_length" + "lexs_lexs" * ] + [ [ "for lenvs of one contex-sensitive relation" ] "lex ( ? ⦻[?] ? )" "lex_tc" * ] + [ [ "for lenvs of two contex-sensitive relations" ] "lexs ( ? ⦻*[?,?,?] ? )" "lexs_tc" + "lexs_length" + "lexs_lexs" * ] } ] } -- 2.39.2