From: Ferruccio Guidi Date: Fri, 24 Apr 2020 21:27:24 +0000 (+0200) Subject: update in staic_2 and basic_2 X-Git-Tag: make_still_working~180 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=647504aa72b84eb49be8177b88a9254174e84d4b;p=helm.git update in staic_2 and basic_2 + an inversion lemma clarifies the link between rpx and req/reqx/lpx + some renaming --- diff --git a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_rpx_fwd.ma b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_rpx_fwd.ma new file mode 100644 index 000000000..c4a6b96c4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_rpx_fwd.ma @@ -0,0 +1,54 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "static_2/static/reqx_fqup.ma". +include "basic_2/rt_transition/lpx.ma". +include "basic_2/rt_transition/rpx.ma". + +(* EXAMPLES *****************************************************************) + +(* Lemma "rpx_fwd_lpx_reqx" is not an inversion *****************************) + +definition L1 (K) (s1) (s0): lenv ≝ K.ⓛ⋆s1.ⓛⓝ#0.⋆s0. + +definition L (K) (s1) (s0): lenv ≝ K.ⓛ⋆s1.ⓛ⋆s0. + +definition L2 (K) (i1) (s0): lenv ≝ K.ⓛ#i1.ⓛ⋆s0. + +definition T: term ≝ #0. + +(* Basic properties *********************************************************) + +lemma ex_rpx_fwd_1 (G) (K) (s1) (s0): + ❪G,L1 K s1 s0❫ ⊢ ⬈ L K s1 s0. +/3 width=1 by lpx_pair, lpx_bind_refl_dx, cpx_eps/ qed. + +lemma ex_rpx_fwd_2 (K) (s1) (s0) (i1) (i0): + L K s1 s0 ≛[T] L2 K i1 i0. +/3 width=1 by reqx_pair, reqx_sort/ qed. + +lemma ex_rpx_fwd_3 (G) (K) (s1) (s0) (i1) (i0): + ❪G,L1 K s1 s0❫ ⊢ ⬈[T] L2 K i1 i0 → ⊥. +#G #K #s1 #s0 #i1 #i0 #H +elim (rpx_inv_zero_pair_sn … H) -H #Y2 #X2 #H #_ normalize #H0 destruct +elim (rpx_inv_flat … H) -H #H #_ +elim (rpx_inv_zero_pair_sn … H) -H #Y2 #X2 #_ #H #H0 destruct +elim (cpx_inv_sort1 … H) #s2 #H destruct +qed-. + +(* Main properties **********************************************************) + +theorem ex_rpx_fwd (G) (K) (s1) (s0) (i1) (i0): + (❪G,L1 K s1 s0❫ ⊢ ⬈ L K s1 s0 → L K s1 s0 ≛[T] L2 K i1 i0 → ❪G,L1 K s1 s0❫ ⊢ ⬈[T] L2 K i1 i0) → ⊥. +/3 width=7 by ex_rpx_fwd_3, ex_rpx_fwd_2, ex_rpx_fwd_1/ qed-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl index 8499b43e3..76794da82 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl @@ -69,7 +69,7 @@ table { class "red" [ { "examples" * } { [ { "terms with special features" * } { - [ "ex_cpr_omega" + "ex_fpbg_refl" + "ex_cnv_eta" * ] + [ "ex_cpr_omega" + "ex_rpx_fwd" + "ex_fpbg_refl" + "ex_cnv_eta" * ] } ] } diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_fsle.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_fsle.ma index 81ee72afb..1fcc7d5d7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_fsle.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_fsle.ma @@ -19,14 +19,17 @@ include "basic_2/rt_transition/cpm_cpx.ma". (* Forward lemmas with free variables inclusion for restricted closures *****) -lemma cpm_fsge_comp: ∀h,n,G. R_fsge_compatible (λL. cpm h G L n). +lemma cpm_fsge_comp (h) (n) (G): + R_fsge_compatible (λL. cpm h G L n). /3 width=6 by cpm_fwd_cpx, cpx_fsge_comp/ qed-. -lemma rpr_fsge_comp: ∀h,G. rex_fsge_compatible (λL. cpm h G L 0). +lemma rpr_fsge_comp (h) (G): + rex_fsge_compatible (λL. cpm h G L 0). /4 width=5 by cpm_fwd_cpx, rpx_fsge_comp, rex_co/ qed-. (* Properties with generic extension on referred entries ********************) (* Basic_2A1: was just: cpr_llpx_sn_conf *) -lemma cpm_rex_conf: ∀R,n,h,G. s_r_confluent1 … (λL. cpm h G L n) (rex R). -/3 width=5 by cpm_fwd_cpx, cpx_rex_conf/ qed-. +lemma cpm_rex_conf_sn (R) (h) (n) (G): + s_r_confluent1 … (λL. cpm h G L n) (rex R). +/3 width=5 by cpm_fwd_cpx, cpx_rex_conf_sn/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_req.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_req.ma index f74d42bab..a982ed783 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_req.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_req.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "static_2/static/req_length.ma". include "static_2/static/req_drops.ma". include "basic_2/rt_transition/rpx_fsle.ma". @@ -20,7 +21,7 @@ include "basic_2/rt_transition/rpx_fsle.ma". (* Properties with syntactic equivalence for lenvs on referred entries ******) (* Basic_2A1: was: lleq_cpx_trans *) -lemma req_cpx_trans (G): req_transitive (cpx G). +lemma req_cpx_trans (G): R_transitive_req (cpx G). #G #L2 #T1 #T2 #H @(cpx_ind … H) -G -L2 -T1 -T2 /2 width=2 by cpx_qu/ [ #I #G #K2 #V1 #V2 #W2 #_ #IH #HVW2 #L1 #H elim (req_inv_zero_pair_dx … H) -H #K1 #HK12 #H destruct @@ -49,6 +50,9 @@ lemma req_cpx_trans (G): req_transitive (cpx G). ] qed-. +lemma cpx_req_conf (G): R_confluent1_rex (cpx G) ceq. +/3 width=3 by req_cpx_trans, req_sym/ qed-. + (* Basic_2A1: was: cpx_lleq_conf_sn *) lemma cpx_req_conf_sn (G): s_r_confluent1 … (cpx G) req. -/2 width=5 by cpx_rex_conf/ qed-. +/2 width=5 by cpx_rex_conf_sn/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_reqx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_reqx.ma index 7c05f8b2c..6c1aa906b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_reqx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_reqx.ma @@ -22,7 +22,7 @@ include "basic_2/rt_transition/rpx_fsle.ma". (* Basic_2A1: was just: cpx_lleq_conf_sn *) lemma cpx_reqx_conf_sn (G): s_r_confluent1 … (cpx G) reqx. -/3 width=6 by cpx_rex_conf/ qed-. +/3 width=6 by cpx_rex_conf_sn/ qed-. (* Basic_2A1: was just: cpx_lleq_conf_dx *) lemma cpx_reqx_conf_dx (G) (L2): diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_feqx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_feqx.ma index 04989deb0..c0e6a4b51 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_feqx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_feqx.ma @@ -30,7 +30,7 @@ lemma feqx_fpb_trans: elim (teqx_fpb_trans … HT12 … H12) -T2 #K0 #T0 #H #HT0 #HK0 elim (reqx_fpb_trans … HK12 … H) -K2 #L0 #U0 #H #HUT0 #HLK0 @(ex2_3_intro … H) -H (**) (* full auto too slow *) -/4 width=3 by feqx_intro_dx, reqx_trans, teqx_reqx_conf, teqx_trans/ +/4 width=3 by feqx_intro_dx, reqx_trans, teqx_reqx_conf_sn, teqx_trans/ qed-. (* Inversion lemmas with degree-based equivalence for closures **************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_reqx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_reqx.ma index 19aeffac6..14a0f8098 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_reqx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_reqx.ma @@ -32,7 +32,7 @@ lemma teqx_fpb_trans: | #T1 #HUT1 #HnUT1 lapply (teqx_cpx_trans … HU21 … HUT1) -HUT1 /6 width=5 by fpb_cpx, teqx_canc_sn, teqx_trans, ex3_2_intro/ -| /6 width=5 by fpb_lpx, rpx_teqx_div, teqx_reqx_conf, ex3_2_intro/ +| /6 width=5 by fpb_lpx, rpx_teqx_div, teqx_reqx_conf_sn, ex3_2_intro/ ] qed-. @@ -45,7 +45,7 @@ lemma reqx_fpb_trans: [ #G #L2 #U #H2 elim (reqx_fqu_trans … H2 … HT) -K2 /3 width=5 by fpb_fqu, ex3_2_intro/ | #U #HTU #HnTU lapply (reqx_cpx_trans … HT … HTU) -HTU - /5 width=11 by fpb_cpx, cpx_reqx_conf_sn, teqx_trans, teqx_reqx_conf, ex3_2_intro/ (**) (* time: 36s on dev *) + /5 width=11 by fpb_cpx, cpx_reqx_conf_sn, teqx_trans, teqx_reqx_conf_sn, ex3_2_intro/ (**) (* time: 36s on dev *) | #L2 #HKL2 #HnKL2 elim (reqx_lpx_trans … HKL2 … HT) -HKL2 /6 width=5 by fpb_lpx, (* 2x *) reqx_canc_sn, ex3_2_intro/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_reqx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_reqx.ma index 73f134d10..dfd367241 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_reqx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_reqx.ma @@ -20,14 +20,37 @@ include "basic_2/rt_transition/rpx_lpx.ma". (* Properties with sort-irrelevant equivalence for local environments *******) -(**) (* to update as reqx_rpx_trans *) +lemma reqx_lpx_trans_rpx (G) (L) (T:term): + ∀L1. L1 ≛[T] L → ∀L2. ❪G,L❫ ⊢ ⬈ L2 → ❪G,L❫ ⊢ ⬈[T] L2. +/3 width=1 by lpx_rpx, reqx_rpx_trans/ qed. + (* Basic_2A1: uses: lleq_lpx_trans *) lemma reqx_lpx_trans (G): ∀L2,K2. ❪G,L2❫ ⊢ ⬈ K2 → ∀L1. ∀T:term. L1 ≛[T] L2 → ∃∃K1. ❪G,L1❫ ⊢ ⬈ K1 & K1 ≛[T] K2. #G #L2 #K2 #HLK2 #L1 #T #HL12 -lapply (lpx_rpx … T HLK2) -HLK2 #HLK2 +lapply (lpx_rpx … T … HLK2) -HLK2 #HLK2 lapply (reqx_rpx_trans … HL12 … HLK2) -L2 #H -elim (rpx_inv_lpx_req … H) -H #K1 #HLK1 #HK12 +elim (rpx_fwd_lpx_req … H) -H #K1 #HLK1 #HK12 +/3 width=3 by req_reqx, ex2_intro/ +qed-. + +(* Inversion lemmas with sort-irrelevant equivalence for local environments *) + +lemma rpx_inv_reqx_lpx (G) (T): + ∀L1,L2. ❪G,L1❫ ⊢ ⬈[T] L2 → + ∃∃L. L1 ≛[T] L & ❪G,L❫ ⊢ ⬈ L2. +#G #T #L1 #L2 #H +elim (rpx_inv_req_lpx … H) -H #L #HL1 #HL2 +/3 width=3 by req_reqx, ex2_intro/ +qed-. + +(* Forward lemmas with sort-irrelevant equivalence for local environments ***) + +lemma rpx_fwd_lpx_reqx (G) (T): + ∀L1,L2. ❪G,L1❫ ⊢ ⬈[T] L2 → + ∃∃L. ❪G,L1❫ ⊢ ⬈ L & L ≛[T] L2. +#G #T #L1 #L2 #H +elim (rpx_fwd_lpx_req … H) -H #L #HL1 #HL2 /3 width=3 by req_reqx, ex2_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_fsle.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_fsle.ma index d4769c838..d7e5e89ea 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_fsle.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_fsle.ma @@ -126,15 +126,15 @@ lemma cpx_fsge_comp (G): R_fsge_compatible (cpx G). (* Note: lemma 1000 *) (* Basic_2A1: uses: cpx_llpx_sn_conf *) -lemma cpx_rex_conf (R) (G): s_r_confluent1 … (cpx G) (rex R). +lemma cpx_rex_conf_sn (R) (G): s_r_confluent1 … (cpx G) (rex R). /3 width=3 by fsge_rex_trans, cpx_fsge_comp/ qed-. (* Advanced properties ******************************************************) -lemma rpx_cpx_conf (G): s_r_confluent1 … (cpx G) (rpx G). -/2 width=5 by cpx_rex_conf/ qed-. +lemma rpx_cpx_conf_sn (G): s_r_confluent1 … (cpx G) (rpx G). +/2 width=5 by cpx_rex_conf_sn/ qed-. lemma rpx_cpx_conf_fsge_dx (G): ∀L0,T0,T1. ❪G,L0❫ ⊢ T0 ⬈ T1 → ∀L2. ❪G,L0❫ ⊢⬈[T0] L2 → ❪L2,T1❫ ⊆ ❪L0,T1❫. -/3 width=5 by rpx_cpx_conf, rpx_fsge_comp/ qed-. +/3 width=5 by rpx_cpx_conf_sn, rpx_fsge_comp/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_lpx.ma index cede8bf52..3d9b9081c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_lpx.ma @@ -13,26 +13,33 @@ (**************************************************************************) include "static_2/static/rex_lex.ma". -include "basic_2/rt_transition/rpx_fsle.ma". +include "basic_2/rt_transition/cpx_req.ma". include "basic_2/rt_transition/lpx.ma". (* EXTENDED PARALLEL RT-TRANSITION FOR REFERRED LOCAL ENVIRONMENTS **********) (* Properties with syntactic equivalence for referred local environments ****) -lemma fleq_rpx (G): - ∀L1,L2,T. L1 ≡[T] L2 → ❪G,L1❫ ⊢ ⬈[T] L2. +lemma req_rpx (G) (T): + ∀L1,L2. L1 ≡[T] L2 → ❪G,L1❫ ⊢ ⬈[T] L2. /2 width=1 by req_fwd_rex/ qed. (* Properties with extended rt-transition for full local envs ***************) -lemma lpx_rpx (G): - ∀L1,L2,T. ❪G,L1❫ ⊢ ⬈ L2 → ❪G,L1❫ ⊢ ⬈[T] L2. +lemma lpx_rpx (G) (T): + ∀L1,L2. ❪G,L1❫ ⊢ ⬈ L2 → ❪G,L1❫ ⊢ ⬈[T] L2. /2 width=1 by rex_lex/ qed. (* Inversion lemmas with extended rt-transition for full local envs *********) -lemma rpx_inv_lpx_req (G): - ∀L1,L2,T. ❪G,L1❫ ⊢ ⬈[T] L2 → +lemma rpx_inv_req_lpx (G) (T): + ∀L1,L2. ❪G,L1❫ ⊢ ⬈[T] L2 → + ∃∃L. L1 ≡[T] L & ❪G,L❫ ⊢ ⬈ L2. +/4 width=13 by cpx_req_conf, rex_inv_req_lex, rex_conf1_next/ qed-. + +(* Forward lemmas with extended rt-transition for full local envs ***********) + +lemma rpx_fwd_lpx_req (G) (T): + ∀L1,L2. ❪G,L1❫ ⊢ ⬈[T] L2 → ∃∃L. ❪G,L1❫ ⊢ ⬈ L & L ≡[T] L2. -/3 width=3 by rpx_fsge_comp, rex_inv_lex_req/ qed-. +/3 width=3 by rpx_fsge_comp, rex_fwd_lex_req/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqx.ma index 29964b29c..5cde4c9f6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqx.ma @@ -41,8 +41,8 @@ lemma rpx_bind_dx_split_void (G): ∃∃K2. ❪G,K1❫ ⊢ ⬈[ⓑ[p,I]V.T] K2 & K2.ⓧ ≛[T] L2. /3 width=5 by rpx_fsge_comp, rex_bind_dx_split_void/ qed-. -lemma rpx_teqx_conf (G): s_r_confluent1 … cdeq (rpx G). -/2 width=5 by teqx_rex_conf/ qed-. +lemma rpx_teqx_conf_sn (G): s_r_confluent1 … cdeq (rpx G). +/2 width=5 by teqx_rex_conf_sn/ qed-. lemma rpx_teqx_div (G): ∀T1,T2. T1 ≛ T2 → ∀L1,L2. ❪G,L1❫ ⊢ ⬈[T2] L2 → ❪G,L1❫ ⊢ ⬈[T1] L2. diff --git a/matita/matita/contribs/lambdadelta/static_2/i_static/rexs_lex.ma b/matita/matita/contribs/lambdadelta/static_2/i_static/rexs_lex.ma index a5a1a42dc..9d582d83b 100644 --- a/matita/matita/contribs/lambdadelta/static_2/i_static/rexs_lex.ma +++ b/matita/matita/contribs/lambdadelta/static_2/i_static/rexs_lex.ma @@ -21,13 +21,15 @@ include "static_2/i_static/rexs_fqup.ma". (* Properties with generic extension of a context sensitive relation ********) -lemma rexs_lex (R): c_reflexive … R → +lemma rexs_lex (R): + c_reflexive … R → ∀L1,L2,T. L1 ⪤[CTC … R] L2 → L1 ⪤*[R,T] L2. #R #HR #L1 #L2 #T * /5 width=7 by rexs_tc, sex_inv_tc_dx, sex_co, ext2_inv_tc, ext2_refl/ qed. -lemma rexs_lex_req (R): c_reflexive … R → +lemma rexs_lex_req (R): + c_reflexive … R → ∀L1,L. L1 ⪤[CTC … R] L → ∀L2,T. L ≡[T] L2 → L1 ⪤*[R,T] L2. /3 width=3 by rexs_lex, rexs_step_dx, req_fwd_rex/ qed. @@ -36,7 +38,7 @@ lemma rexs_lex_req (R): c_reflexive … R → (* Note: s_rs_transitive_lex_inv_isid could be invoked in the last auto but makes it too slow *) lemma rexs_inv_lex_req (R): c_reflexive … R → rex_fsge_compatible R → - s_rs_transitive … R (λ_.lex R) → req_transitive R → + s_rs_transitive … R (λ_.lex R) → R_transitive_req R → ∀L1,L2,T. L1 ⪤*[R,T] L2 → ∃∃L. L1 ⪤[CTC … R] L & L ≡[T] L2. #R #H1R #H2R #H3R #H4R #L1 #L2 #T #H @@ -45,7 +47,7 @@ lapply (s_rs_transitive_lex_inv_isid … H3R) -H3R #H3R [ /4 width=3 by req_refl, lex_refl, inj, ex2_intro/ | #L0 #L2 #_ #HL02 * #L * #f0 #Hf0 #HL1 #HL0 lapply (req_rex_trans … HL0 … HL02) -L0 // * #f1 #Hf1 #HL2 - elim (sex_sdj_split … ceq_ext … HL2 f0 ?) -HL2 + elim (sex_sdj_split_sn … ceq_ext … HL2 f0 ?) -HL2 [ #L0 #HL0 #HL02 |*: /2 width=1 by ext2_refl, sdj_isid_dx/ ] lapply (sex_sdj … HL0 f1 ?) /2 width=1 by sdj_isid_sn/ #H elim (frees_sex_conf_fsge … Hf1 … H) // -H2R -H #f2 #Hf2 #Hf21 diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_sex.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_sex.ma index edec3dcc5..d9a9588a3 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_sex.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_sex.ma @@ -20,7 +20,8 @@ include "static_2/relocation/drops.ma". (* Properties with entrywise extension of context-sensitive relations *******) (**) (* changed after commit 13218 *) -lemma sex_co_dropable_sn: ∀RN,RP. co_dropable_sn (sex RN RP). +lemma sex_co_dropable_sn (RN) (RP): + co_dropable_sn (sex RN RP). #RN #RP #b #f #L1 #K1 #H elim H -f -L1 -K1 [ #f #Hf #_ #f2 #X #H #f1 #Hf2 >(sex_inv_atom1 … H) -X /4 width=3 by sex_atom, drops_atom, ex2_intro/ @@ -41,10 +42,11 @@ lemma sex_co_dropable_sn: ∀RN,RP. co_dropable_sn (sex RN RP). ] qed-. -lemma sex_liftable_co_dedropable_bi: ∀RN,RP. d_liftable2_sn … liftsb RN → d_liftable2_sn … liftsb RP → - ∀f2,L1,L2. L1 ⪤[cfull,RP,f2] L2 → ∀f1,K1,K2. K1 ⪤[RN,RP,f1] K2 → - ∀b,f. ⇩*[b,f] L1 ≘ K1 → ⇩*[b,f] L2 ≘ K2 → - f ~⊚ f1 ≘ f2 → L1 ⪤[RN,RP,f2] L2. +lemma sex_liftable_co_dedropable_bi (RN) (RP): + d_liftable2_sn … liftsb RN → d_liftable2_sn … liftsb RP → + ∀f2,L1,L2. L1 ⪤[cfull,RP,f2] L2 → ∀f1,K1,K2. K1 ⪤[RN,RP,f1] K2 → + ∀b,f. ⇩*[b,f] L1 ≘ K1 → ⇩*[b,f] L2 ≘ K2 → + f ~⊚ f1 ≘ f2 → L1 ⪤[RN,RP,f2] L2. #RN #RP #HRN #HRP #f2 #L1 #L2 #H elim H -f2 -L1 -L2 // #g2 #I1 #I2 #L1 #L2 #HL12 #HI12 #IH #f1 #Y1 #Y2 #HK12 #b #f #HY1 #HY2 #H [ elim (coafter_inv_xxn … H) [ |*: // ] -H #g #g1 #Hg2 #H1 #H2 destruct @@ -68,9 +70,10 @@ lemma sex_liftable_co_dedropable_bi: ∀RN,RP. d_liftable2_sn … liftsb RN → ] qed-. -lemma sex_liftable_co_dedropable_sn: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) → - d_liftable2_sn … liftsb RN → d_liftable2_sn … liftsb RP → - co_dedropable_sn (sex RN RP). +lemma sex_liftable_co_dedropable_sn (RN) (RP): + (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) → + d_liftable2_sn … liftsb RN → d_liftable2_sn … liftsb RP → + co_dedropable_sn (sex RN RP). #RN #RP #H1RN #H1RP #H2RN #H2RP #b #f #L1 #K1 #H elim H -f -L1 -K1 [ #f #Hf #X #f1 #H #f2 #Hf2 >(sex_inv_atom1 … H) -X /4 width=4 by drops_atom, sex_atom, ex3_intro/ @@ -87,9 +90,10 @@ lemma sex_liftable_co_dedropable_sn: ∀RN,RP. (∀L. reflexive … (RN L)) → ] qed-. -fact sex_dropable_dx_aux: ∀RN,RP,b,f,L2,K2. ⇩*[b,f] L2 ≘ K2 → 𝐔❪f❫ → - ∀f2,L1. L1 ⪤[RN,RP,f2] L2 → ∀f1. f ~⊚ f1 ≘ f2 → - ∃∃K1. ⇩*[b,f] L1 ≘ K1 & K1 ⪤[RN,RP,f1] K2. +fact sex_dropable_dx_aux (RN) (RP): + ∀b,f,L2,K2. ⇩*[b,f] L2 ≘ K2 → 𝐔❪f❫ → + ∀f2,L1. L1 ⪤[RN,RP,f2] L2 → ∀f1. f ~⊚ f1 ≘ f2 → + ∃∃K1. ⇩*[b,f] L1 ≘ K1 & K1 ⪤[RN,RP,f1] K2. #RN #RP #b #f #L2 #K2 #H elim H -f -L2 -K2 [ #f #Hf #_ #f2 #X #H #f1 #Hf2 lapply (sex_inv_atom2 … H) -H #H destruct /4 width=3 by sex_atom, drops_atom, ex2_intro/ @@ -109,79 +113,112 @@ fact sex_dropable_dx_aux: ∀RN,RP,b,f,L2,K2. ⇩*[b,f] L2 ≘ K2 → 𝐔❪f ] qed-. -lemma sex_co_dropable_dx: ∀RN,RP. co_dropable_dx (sex RN RP). +lemma sex_co_dropable_dx (RN) (RP): + co_dropable_dx (sex RN RP). /2 width=5 by sex_dropable_dx_aux/ qed-. -lemma sex_drops_conf_next: ∀RN,RP. - ∀f2,L1,L2. L1 ⪤[RN,RP,f2] L2 → - ∀b,f,I1,K1. ⇩*[b,f] L1 ≘ K1.ⓘ[I1] → 𝐔❪f❫ → - ∀f1. f ~⊚ ↑f1 ≘ f2 → - ∃∃I2,K2. ⇩*[b,f] L2 ≘ K2.ⓘ[I2] & K1 ⪤[RN,RP,f1] K2 & RN K1 I1 I2. +lemma sex_drops_conf_next (RN) (RP): + ∀f2,L1,L2. L1 ⪤[RN,RP,f2] L2 → + ∀b,f,I1,K1. ⇩*[b,f] L1 ≘ K1.ⓘ[I1] → 𝐔❪f❫ → + ∀f1. f ~⊚ ↑f1 ≘ f2 → + ∃∃I2,K2. ⇩*[b,f] L2 ≘ K2.ⓘ[I2] & K1 ⪤[RN,RP,f1] K2 & RN K1 I1 I2. #RN #RP #f2 #L1 #L2 #HL12 #b #f #I1 #K1 #HLK1 #Hf #f1 #Hf2 elim (sex_co_dropable_sn … HLK1 … Hf … HL12 … Hf2) -L1 -f2 -Hf #X #HX #HLK2 elim (sex_inv_next1 … HX) -HX #I2 #K2 #HK12 #HI12 #H destruct /2 width=5 by ex3_2_intro/ qed-. -lemma sex_drops_conf_push: ∀RN,RP. - ∀f2,L1,L2. L1 ⪤[RN,RP,f2] L2 → - ∀b,f,I1,K1. ⇩*[b,f] L1 ≘ K1.ⓘ[I1] → 𝐔❪f❫ → - ∀f1. f ~⊚ ⫯f1 ≘ f2 → - ∃∃I2,K2. ⇩*[b,f] L2 ≘ K2.ⓘ[I2] & K1 ⪤[RN,RP,f1] K2 & RP K1 I1 I2. +lemma sex_drops_conf_push (RN) (RP): + ∀f2,L1,L2. L1 ⪤[RN,RP,f2] L2 → + ∀b,f,I1,K1. ⇩*[b,f] L1 ≘ K1.ⓘ[I1] → 𝐔❪f❫ → + ∀f1. f ~⊚ ⫯f1 ≘ f2 → + ∃∃I2,K2. ⇩*[b,f] L2 ≘ K2.ⓘ[I2] & K1 ⪤[RN,RP,f1] K2 & RP K1 I1 I2. #RN #RP #f2 #L1 #L2 #HL12 #b #f #I1 #K1 #HLK1 #Hf #f1 #Hf2 elim (sex_co_dropable_sn … HLK1 … Hf … HL12 … Hf2) -L1 -f2 -Hf #X #HX #HLK2 elim (sex_inv_push1 … HX) -HX #I2 #K2 #HK12 #HI12 #H destruct /2 width=5 by ex3_2_intro/ qed-. -lemma sex_drops_trans_next: ∀RN,RP,f2,L1,L2. L1 ⪤[RN,RP,f2] L2 → - ∀b,f,I2,K2. ⇩*[b,f] L2 ≘ K2.ⓘ[I2] → 𝐔❪f❫ → - ∀f1. f ~⊚ ↑f1 ≘ f2 → - ∃∃I1,K1. ⇩*[b,f] L1 ≘ K1.ⓘ[I1] & K1 ⪤[RN,RP,f1] K2 & RN K1 I1 I2. +lemma sex_drops_trans_next (RN) (RP): + ∀f2,L1,L2. L1 ⪤[RN,RP,f2] L2 → + ∀b,f,I2,K2. ⇩*[b,f] L2 ≘ K2.ⓘ[I2] → 𝐔❪f❫ → + ∀f1. f ~⊚ ↑f1 ≘ f2 → + ∃∃I1,K1. ⇩*[b,f] L1 ≘ K1.ⓘ[I1] & K1 ⪤[RN,RP,f1] K2 & RN K1 I1 I2. #RN #RP #f2 #L1 #L2 #HL12 #b #f #I2 #K2 #HLK2 #Hf #f1 #Hf2 elim (sex_co_dropable_dx … HL12 … HLK2 … Hf … Hf2) -L2 -f2 -Hf #X #HLK1 #HX elim (sex_inv_next2 … HX) -HX #I1 #K1 #HK12 #HI12 #H destruct /2 width=5 by ex3_2_intro/ qed-. -lemma sex_drops_trans_push: ∀RN,RP,f2,L1,L2. L1 ⪤[RN,RP,f2] L2 → - ∀b,f,I2,K2. ⇩*[b,f] L2 ≘ K2.ⓘ[I2] → 𝐔❪f❫ → - ∀f1. f ~⊚ ⫯f1 ≘ f2 → - ∃∃I1,K1. ⇩*[b,f] L1 ≘ K1.ⓘ[I1] & K1 ⪤[RN,RP,f1] K2 & RP K1 I1 I2. +lemma sex_drops_trans_push (RN) (RP): ∀f2,L1,L2. L1 ⪤[RN,RP,f2] L2 → + ∀b,f,I2,K2. ⇩*[b,f] L2 ≘ K2.ⓘ[I2] → 𝐔❪f❫ → + ∀f1. f ~⊚ ⫯f1 ≘ f2 → + ∃∃I1,K1. ⇩*[b,f] L1 ≘ K1.ⓘ[I1] & K1 ⪤[RN,RP,f1] K2 & RP K1 I1 I2. #RN #RP #f2 #L1 #L2 #HL12 #b #f #I2 #K2 #HLK2 #Hf #f1 #Hf2 elim (sex_co_dropable_dx … HL12 … HLK2 … Hf … Hf2) -L2 -f2 -Hf #X #HLK1 #HX elim (sex_inv_push2 … HX) -HX #I1 #K1 #HK12 #HI12 #H destruct /2 width=5 by ex3_2_intro/ qed-. -lemma drops_sex_trans_next: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. reflexive ? (RP L)) → - d_liftable2_sn … liftsb RN → d_liftable2_sn … liftsb RP → - ∀f1,K1,K2. K1 ⪤[RN,RP,f1] K2 → - ∀b,f,I1,L1. ⇩*[b,f] L1.ⓘ[I1] ≘ K1 → - ∀f2. f ~⊚ f1 ≘ ↑f2 → - ∃∃I2,L2. ⇩*[b,f] L2.ⓘ[I2] ≘ K2 & L1 ⪤[RN,RP,f2] L2 & RN L1 I1 I2 & L1.ⓘ[I1] ≡[f] L2.ⓘ[I2]. +lemma drops_sex_trans_next (RN) (RP): + (∀L. reflexive ? (RN L)) → (∀L. reflexive ? (RP L)) → + d_liftable2_sn … liftsb RN → d_liftable2_sn … liftsb RP → + ∀f1,K1,K2. K1 ⪤[RN,RP,f1] K2 → + ∀b,f,I1,L1. ⇩*[b,f] L1.ⓘ[I1] ≘ K1 → + ∀f2. f ~⊚ f1 ≘ ↑f2 → + ∃∃I2,L2. ⇩*[b,f] L2.ⓘ[I2] ≘ K2 & L1 ⪤[RN,RP,f2] L2 & RN L1 I1 I2 & L1.ⓘ[I1] ≡[f] L2.ⓘ[I2]. #RN #RP #H1RN #H1RP #H2RN #H2RP #f1 #K1 #K2 #HK12 #b #f #I1 #L1 #HLK1 #f2 #Hf2 elim (sex_liftable_co_dedropable_sn … H1RN H1RP H2RN H2RP … HLK1 … HK12 … Hf2) -K1 -f1 -H1RN -H1RP -H2RN -H2RP #X #HX #HLK2 #H1L12 elim (sex_inv_next1 … HX) -HX #I2 #L2 #H2L12 #HI12 #H destruct /2 width=6 by ex4_2_intro/ qed-. -lemma drops_sex_trans_push: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. reflexive ? (RP L)) → - d_liftable2_sn … liftsb RN → d_liftable2_sn … liftsb RP → - ∀f1,K1,K2. K1 ⪤[RN,RP,f1] K2 → - ∀b,f,I1,L1. ⇩*[b,f] L1.ⓘ[I1] ≘ K1 → - ∀f2. f ~⊚ f1 ≘ ⫯f2 → - ∃∃I2,L2. ⇩*[b,f] L2.ⓘ[I2] ≘ K2 & L1 ⪤[RN,RP,f2] L2 & RP L1 I1 I2 & L1.ⓘ[I1] ≡[f] L2.ⓘ[I2]. +lemma drops_sex_trans_push (RN) (RP): + (∀L. reflexive ? (RN L)) → (∀L. reflexive ? (RP L)) → + d_liftable2_sn … liftsb RN → d_liftable2_sn … liftsb RP → + ∀f1,K1,K2. K1 ⪤[RN,RP,f1] K2 → + ∀b,f,I1,L1. ⇩*[b,f] L1.ⓘ[I1] ≘ K1 → + ∀f2. f ~⊚ f1 ≘ ⫯f2 → + ∃∃I2,L2. ⇩*[b,f] L2.ⓘ[I2] ≘ K2 & L1 ⪤[RN,RP,f2] L2 & RP L1 I1 I2 & L1.ⓘ[I1] ≡[f] L2.ⓘ[I2]. #RN #RP #H1RN #H1RP #H2RN #H2RP #f1 #K1 #K2 #HK12 #b #f #I1 #L1 #HLK1 #f2 #Hf2 elim (sex_liftable_co_dedropable_sn … H1RN H1RP H2RN H2RP … HLK1 … HK12 … Hf2) -K1 -f1 -H1RN -H1RP -H2RN -H2RP #X #HX #HLK2 #H1L12 elim (sex_inv_push1 … HX) -HX #I2 #L2 #H2L12 #HI12 #H destruct /2 width=6 by ex4_2_intro/ qed-. -lemma drops_atom2_sex_conf: ∀RN,RP,b,f1,L1. ⇩*[b,f1] L1 ≘ ⋆ → 𝐔❪f1❫ → - ∀f,L2. L1 ⪤[RN,RP,f] L2 → - ∀f2. f1 ~⊚ f2 ≘f → ⇩*[b,f1] L2 ≘ ⋆. +lemma drops_atom2_sex_conf (RN) (RP): + ∀b,f1,L1. ⇩*[b,f1] L1 ≘ ⋆ → 𝐔❪f1❫ → + ∀f,L2. L1 ⪤[RN,RP,f] L2 → + ∀f2. f1 ~⊚ f2 ≘f → ⇩*[b,f1] L2 ≘ ⋆. #RN #RP #b #f1 #L1 #H1 #Hf1 #f #L2 #H2 #f2 #H3 elim (sex_co_dropable_sn … H1 … H2 … H3) // -H1 -H2 -H3 -Hf1 #L #H #HL2 lapply (sex_inv_atom1 … H) -H // qed-. + +lemma sex_sdj_split_dx (R1) (R2) (RP): + c_reflexive … R1 → c_reflexive … R2 → c_reflexive … RP → + ∀L1,f1. + (∀g,I,K,n. ⇩[n] L1 ≘ K.ⓘ[I] → ↑g = ⫱*[n] f1 → R_pw_confluent1_sex R1 R1 R2 cfull g K I) → + ∀L2. L1 ⪤[R1,RP,f1] L2 → ∀f2. f1 ∥ f2 → + ∃∃L. L1 ⪤[R2,cfull,f1] L & L ⪤[RP,R1,f2] L2. +#R1 #R2 #RP #HR1 #HR2 #HRP #L1 elim L1 -L1 +[ #f1 #_ #L2 #H #f2 #_ + lapply (sex_inv_atom1 … H) -H #H destruct + /2 width=3 by sex_atom, ex2_intro/ +| #K1 #I1 #IH #f1 elim (pn_split f1) * #g1 #H destruct + #HR #L2 #H #f2 #Hf + [ elim (sex_inv_push1 … H) -H #I2 #K2 #HK12 #HI12 #H destruct + elim (sdj_inv_px … Hf ??) -Hf [1,3: * |*: // ] #g2 #Hg #H destruct + elim (IH … HK12 … Hg) -IH -HK12 -Hg + [1,3: /3 width=5 by sex_next, sex_push, ex2_intro/ + |2,4: /3 width=3 by drops_drop/ + ] + | elim (sex_inv_next1 … H) -H #I2 #K2 #HK12 #HI12 #H destruct + elim (sdj_inv_nx … Hf ??) -Hf [|*: // ] #g2 #Hg #H destruct + elim (IH … HK12 … Hg) -IH -HK12 -Hg + [ /5 width=11 by sex_next, sex_push, drops_refl, ex2_intro/ + | /3 width=3 by drops_drop/ + ] + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/sex.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/sex.ma index 3fba7476a..72909212c 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/sex.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/sex.ma @@ -29,48 +29,62 @@ inductive sex (RN,RP:relation3 lenv bind bind): rtmap → relation lenv ≝ sex RN RP (⫯f) (L1.ⓘ[I1]) (L2.ⓘ[I2]) . -interpretation "generic entrywise extension (local environment)" - 'Relation RN RP f L1 L2 = (sex RN RP f L1 L2). - -definition sex_transitive: relation3 lenv bind bind → relation3 lenv bind bind → - relation3 lenv bind bind → - relation3 lenv bind bind → relation3 lenv bind bind → - relation3 rtmap lenv bind ≝ - λR1,R2,R3,RN,RP,f,L1,I1. - ∀I. R1 L1 I1 I → ∀L2. L1 ⪤[RN,RP,f] L2 → - ∀I2. R2 L2 I I2 → R3 L1 I1 I2. - -definition R_pw_confluent2_sex: relation3 lenv bind bind → relation3 lenv bind bind → - relation3 lenv bind bind → relation3 lenv bind bind → - relation3 lenv bind bind → relation3 lenv bind bind → - relation3 rtmap lenv bind ≝ - λR1,R2,RN1,RP1,RN2,RP2,f,L0,I0. - ∀I1. R1 L0 I0 I1 → ∀I2. R2 L0 I0 I2 → - ∀L1. L0 ⪤[RN1,RP1,f] L1 → ∀L2. L0 ⪤[RN2,RP2,f] L2 → - ∃∃I. R2 L1 I1 I & R1 L2 I2 I. - -definition R_pw_replace3_sex: relation3 lenv bind bind → relation3 lenv bind bind → - relation3 lenv bind bind → relation3 lenv bind bind → - relation3 lenv bind bind → relation3 lenv bind bind → - relation3 rtmap lenv bind ≝ - λR1,R2,RN1,RP1,RN2,RP2,f,L0,I0. - ∀I1. R1 L0 I0 I1 → ∀I2. R2 L0 I0 I2 → - ∀L1. L0 ⪤[RN1,RP1,f] L1 → ∀L2. L0 ⪤[RN2,RP2,f] L2 → - ∀I. R2 L1 I1 I → R1 L2 I2 I. +interpretation + "generic entrywise extension (local environment)" + 'Relation RN RP f L1 L2 = (sex RN RP f L1 L2). + +definition R_pw_transitive_sex: + relation3 lenv bind bind → relation3 lenv bind bind → + relation3 lenv bind bind → + relation3 lenv bind bind → relation3 lenv bind bind → + relation3 rtmap lenv bind ≝ + λR1,R2,R3,RN,RP,f,L1,I1. + ∀I. R1 L1 I1 I → ∀L2. L1 ⪤[RN,RP,f] L2 → + ∀I2. R2 L2 I I2 → R3 L1 I1 I2. + +definition R_pw_confluent1_sex: + relation3 lenv bind bind → relation3 lenv bind bind → + relation3 lenv bind bind → relation3 lenv bind bind → + relation3 rtmap lenv bind ≝ + λR1,R2,RN,RP,f,L1,I1. + ∀I2. R1 L1 I1 I2 → ∀L2. L1 ⪤[RN,RP,f] L2 → R2 L2 I1 I2. + +definition R_pw_confluent2_sex: + relation3 lenv bind bind → relation3 lenv bind bind → + relation3 lenv bind bind → relation3 lenv bind bind → + relation3 lenv bind bind → relation3 lenv bind bind → + relation3 rtmap lenv bind ≝ + λR1,R2,RN1,RP1,RN2,RP2,f,L0,I0. + ∀I1. R1 L0 I0 I1 → ∀I2. R2 L0 I0 I2 → + ∀L1. L0 ⪤[RN1,RP1,f] L1 → ∀L2. L0 ⪤[RN2,RP2,f] L2 → + ∃∃I. R2 L1 I1 I & R1 L2 I2 I. + +definition R_pw_replace3_sex: + relation3 lenv bind bind → relation3 lenv bind bind → + relation3 lenv bind bind → relation3 lenv bind bind → + relation3 lenv bind bind → relation3 lenv bind bind → + relation3 rtmap lenv bind ≝ + λR1,R2,RN1,RP1,RN2,RP2,f,L0,I0. + ∀I1. R1 L0 I0 I1 → ∀I2. R2 L0 I0 I2 → + ∀L1. L0 ⪤[RN1,RP1,f] L1 → ∀L2. L0 ⪤[RN2,RP2,f] L2 → + ∀I. R2 L1 I1 I → R1 L2 I2 I. (* Basic inversion lemmas ***************************************************) -fact sex_inv_atom1_aux: ∀RN,RP,f,X,Y. X ⪤[RN,RP,f] Y → X = ⋆ → Y = ⋆. +fact sex_inv_atom1_aux (RN) (RP): + ∀f,X,Y. X ⪤[RN,RP,f] Y → X = ⋆ → Y = ⋆. #RN #RP #f #X #Y * -f -X -Y // #f #I1 #I2 #L1 #L2 #_ #_ #H destruct qed-. (* Basic_2A1: includes lpx_sn_inv_atom1 *) -lemma sex_inv_atom1: ∀RN,RP,f,Y. ⋆ ⪤[RN,RP,f] Y → Y = ⋆. +lemma sex_inv_atom1 (RN) (RP): + ∀f,Y. ⋆ ⪤[RN,RP,f] Y → Y = ⋆. /2 width=6 by sex_inv_atom1_aux/ qed-. -fact sex_inv_next1_aux: ∀RN,RP,f,X,Y. X ⪤[RN,RP,f] Y → ∀g,J1,K1. X = K1.ⓘ[J1] → f = ↑g → - ∃∃J2,K2. K1 ⪤[RN,RP,g] K2 & RN K1 J1 J2 & Y = K2.ⓘ[J2]. +fact sex_inv_next1_aux (RN) (RP): + ∀f,X,Y. X ⪤[RN,RP,f] Y → ∀g,J1,K1. X = K1.ⓘ[J1] → f = ↑g → + ∃∃J2,K2. K1 ⪤[RN,RP,g] K2 & RN K1 J1 J2 & Y = K2.ⓘ[J2]. #RN #RP #f #X #Y * -f -X -Y [ #f #g #J1 #K1 #H destruct | #f #I1 #I2 #L1 #L2 #HL #HI #g #J1 #K1 #H1 #H2 <(injective_next … H2) -g destruct @@ -80,12 +94,14 @@ fact sex_inv_next1_aux: ∀RN,RP,f,X,Y. X ⪤[RN,RP,f] Y → ∀g,J1,K1. X = K1. qed-. (* Basic_2A1: includes lpx_sn_inv_pair1 *) -lemma sex_inv_next1: ∀RN,RP,g,J1,K1,Y. K1.ⓘ[J1] ⪤[RN,RP,↑g] Y → - ∃∃J2,K2. K1 ⪤[RN,RP,g] K2 & RN K1 J1 J2 & Y = K2.ⓘ[J2]. +lemma sex_inv_next1 (RN) (RP): + ∀g,J1,K1,Y. K1.ⓘ[J1] ⪤[RN,RP,↑g] Y → + ∃∃J2,K2. K1 ⪤[RN,RP,g] K2 & RN K1 J1 J2 & Y = K2.ⓘ[J2]. /2 width=7 by sex_inv_next1_aux/ qed-. -fact sex_inv_push1_aux: ∀RN,RP,f,X,Y. X ⪤[RN,RP,f] Y → ∀g,J1,K1. X = K1.ⓘ[J1] → f = ⫯g → - ∃∃J2,K2. K1 ⪤[RN,RP,g] K2 & RP K1 J1 J2 & Y = K2.ⓘ[J2]. +fact sex_inv_push1_aux (RN) (RP): + ∀f,X,Y. X ⪤[RN,RP,f] Y → ∀g,J1,K1. X = K1.ⓘ[J1] → f = ⫯g → + ∃∃J2,K2. K1 ⪤[RN,RP,g] K2 & RP K1 J1 J2 & Y = K2.ⓘ[J2]. #RN #RP #f #X #Y * -f -X -Y [ #f #g #J1 #K1 #H destruct | #f #I1 #I2 #L1 #L2 #_ #_ #g #J1 #K1 #_ #H elim (discr_next_push … H) @@ -94,21 +110,25 @@ fact sex_inv_push1_aux: ∀RN,RP,f,X,Y. X ⪤[RN,RP,f] Y → ∀g,J1,K1. X = K1. ] qed-. -lemma sex_inv_push1: ∀RN,RP,g,J1,K1,Y. K1.ⓘ[J1] ⪤[RN,RP,⫯g] Y → - ∃∃J2,K2. K1 ⪤[RN,RP,g] K2 & RP K1 J1 J2 & Y = K2.ⓘ[J2]. +lemma sex_inv_push1 (RN) (RP): + ∀g,J1,K1,Y. K1.ⓘ[J1] ⪤[RN,RP,⫯g] Y → + ∃∃J2,K2. K1 ⪤[RN,RP,g] K2 & RP K1 J1 J2 & Y = K2.ⓘ[J2]. /2 width=7 by sex_inv_push1_aux/ qed-. -fact sex_inv_atom2_aux: ∀RN,RP,f,X,Y. X ⪤[RN,RP,f] Y → Y = ⋆ → X = ⋆. +fact sex_inv_atom2_aux (RN) (RP): + ∀f,X,Y. X ⪤[RN,RP,f] Y → Y = ⋆ → X = ⋆. #RN #RP #f #X #Y * -f -X -Y // #f #I1 #I2 #L1 #L2 #_ #_ #H destruct qed-. (* Basic_2A1: includes lpx_sn_inv_atom2 *) -lemma sex_inv_atom2: ∀RN,RP,f,X. X ⪤[RN,RP,f] ⋆ → X = ⋆. +lemma sex_inv_atom2 (RN) (RP): + ∀f,X. X ⪤[RN,RP,f] ⋆ → X = ⋆. /2 width=6 by sex_inv_atom2_aux/ qed-. -fact sex_inv_next2_aux: ∀RN,RP,f,X,Y. X ⪤[RN,RP,f] Y → ∀g,J2,K2. Y = K2.ⓘ[J2] → f = ↑g → - ∃∃J1,K1. K1 ⪤[RN,RP,g] K2 & RN K1 J1 J2 & X = K1.ⓘ[J1]. +fact sex_inv_next2_aux (RN) (RP): + ∀f,X,Y. X ⪤[RN,RP,f] Y → ∀g,J2,K2. Y = K2.ⓘ[J2] → f = ↑g → + ∃∃J1,K1. K1 ⪤[RN,RP,g] K2 & RN K1 J1 J2 & X = K1.ⓘ[J1]. #RN #RP #f #X #Y * -f -X -Y [ #f #g #J2 #K2 #H destruct | #f #I1 #I2 #L1 #L2 #HL #HI #g #J2 #K2 #H1 #H2 <(injective_next … H2) -g destruct @@ -118,12 +138,14 @@ fact sex_inv_next2_aux: ∀RN,RP,f,X,Y. X ⪤[RN,RP,f] Y → ∀g,J2,K2. Y = K2. qed-. (* Basic_2A1: includes lpx_sn_inv_pair2 *) -lemma sex_inv_next2: ∀RN,RP,g,J2,X,K2. X ⪤[RN,RP,↑g] K2.ⓘ[J2] → - ∃∃J1,K1. K1 ⪤[RN,RP,g] K2 & RN K1 J1 J2 & X = K1.ⓘ[J1]. +lemma sex_inv_next2 (RN) (RP): + ∀g,J2,X,K2. X ⪤[RN,RP,↑g] K2.ⓘ[J2] → + ∃∃J1,K1. K1 ⪤[RN,RP,g] K2 & RN K1 J1 J2 & X = K1.ⓘ[J1]. /2 width=7 by sex_inv_next2_aux/ qed-. -fact sex_inv_push2_aux: ∀RN,RP,f,X,Y. X ⪤[RN,RP,f] Y → ∀g,J2,K2. Y = K2.ⓘ[J2] → f = ⫯g → - ∃∃J1,K1. K1 ⪤[RN,RP,g] K2 & RP K1 J1 J2 & X = K1.ⓘ[J1]. +fact sex_inv_push2_aux (RN) (RP): + ∀f,X,Y. X ⪤[RN,RP,f] Y → ∀g,J2,K2. Y = K2.ⓘ[J2] → f = ⫯g → + ∃∃J1,K1. K1 ⪤[RN,RP,g] K2 & RP K1 J1 J2 & X = K1.ⓘ[J1]. #RN #RP #f #X #Y * -f -X -Y [ #f #J2 #K2 #g #H destruct | #f #I1 #I2 #L1 #L2 #_ #_ #g #J2 #K2 #_ #H elim (discr_next_push … H) @@ -132,37 +154,41 @@ fact sex_inv_push2_aux: ∀RN,RP,f,X,Y. X ⪤[RN,RP,f] Y → ∀g,J2,K2. Y = K2. ] qed-. -lemma sex_inv_push2: ∀RN,RP,g,J2,X,K2. X ⪤[RN,RP,⫯g] K2.ⓘ[J2] → - ∃∃J1,K1. K1 ⪤[RN,RP,g] K2 & RP K1 J1 J2 & X = K1.ⓘ[J1]. +lemma sex_inv_push2 (RN) (RP): + ∀g,J2,X,K2. X ⪤[RN,RP,⫯g] K2.ⓘ[J2] → + ∃∃J1,K1. K1 ⪤[RN,RP,g] K2 & RP K1 J1 J2 & X = K1.ⓘ[J1]. /2 width=7 by sex_inv_push2_aux/ qed-. (* Basic_2A1: includes lpx_sn_inv_pair *) -lemma sex_inv_next: ∀RN,RP,f,I1,I2,L1,L2. - L1.ⓘ[I1] ⪤[RN,RP,↑f] L2.ⓘ[I2] → - L1 ⪤[RN,RP,f] L2 ∧ RN L1 I1 I2. +lemma sex_inv_next (RN) (RP): + ∀f,I1,I2,L1,L2. + L1.ⓘ[I1] ⪤[RN,RP,↑f] L2.ⓘ[I2] → + L1 ⪤[RN,RP,f] L2 ∧ RN L1 I1 I2. #RN #RP #f #I1 #I2 #L1 #L2 #H elim (sex_inv_next1 … H) -H #I0 #L0 #HL10 #HI10 #H destruct /2 width=1 by conj/ qed-. -lemma sex_inv_push: ∀RN,RP,f,I1,I2,L1,L2. - L1.ⓘ[I1] ⪤[RN,RP,⫯f] L2.ⓘ[I2] → - L1 ⪤[RN,RP,f] L2 ∧ RP L1 I1 I2. +lemma sex_inv_push (RN) (RP): + ∀f,I1,I2,L1,L2. + L1.ⓘ[I1] ⪤[RN,RP,⫯f] L2.ⓘ[I2] → + L1 ⪤[RN,RP,f] L2 ∧ RP L1 I1 I2. #RN #RP #f #I1 #I2 #L1 #L2 #H elim (sex_inv_push1 … H) -H #I0 #L0 #HL10 #HI10 #H destruct /2 width=1 by conj/ qed-. -lemma sex_inv_tl: ∀RN,RP,f,I1,I2,L1,L2. L1 ⪤[RN,RP,⫱f] L2 → - RN L1 I1 I2 → RP L1 I1 I2 → - L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2]. +lemma sex_inv_tl (RN) (RP): + ∀f,I1,I2,L1,L2. L1 ⪤[RN,RP,⫱f] L2 → + RN L1 I1 I2 → RP L1 I1 I2 → + L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2]. #RN #RP #f #I1 #I2 #L2 #L2 elim (pn_split f) * /2 width=1 by sex_next, sex_push/ qed-. (* Basic forward lemmas *****************************************************) -lemma sex_fwd_bind: ∀RN,RP,f,I1,I2,L1,L2. - L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2] → - L1 ⪤[RN,RP,⫱f] L2. +lemma sex_fwd_bind (RN) (RP): + ∀f,I1,I2,L1,L2. + L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2] → L1 ⪤[RN,RP,⫱f] L2. #RN #RP #f #I1 #I2 #L1 #L2 #Hf elim (pn_split f) * #g #H destruct [ elim (sex_inv_push … Hf) | elim (sex_inv_next … Hf) ] -Hf // @@ -170,7 +196,8 @@ qed-. (* Basic properties *********************************************************) -lemma sex_eq_repl_back: ∀RN,RP,L1,L2. eq_repl_back … (λf. L1 ⪤[RN,RP,f] L2). +lemma sex_eq_repl_back (RN) (RP): + ∀L1,L2. eq_repl_back … (λf. L1 ⪤[RN,RP,f] L2). #RN #RP #L1 #L2 #f1 #H elim H -f1 -L1 -L2 // #f1 #I1 #I2 #L1 #L2 #_ #HI #IH #f2 #H [ elim (eq_inv_nx … H) -H /3 width=3 by sex_next/ @@ -178,40 +205,45 @@ lemma sex_eq_repl_back: ∀RN,RP,L1,L2. eq_repl_back … (λf. L1 ⪤[RN,RP,f] L ] qed-. -lemma sex_eq_repl_fwd: ∀RN,RP,L1,L2. eq_repl_fwd … (λf. L1 ⪤[RN,RP,f] L2). +lemma sex_eq_repl_fwd (RN) (RP): + ∀L1,L2. eq_repl_fwd … (λf. L1 ⪤[RN,RP,f] L2). #RN #RP #L1 #L2 @eq_repl_sym /2 width=3 by sex_eq_repl_back/ (**) (* full auto fails *) qed-. -lemma sex_refl: ∀RN,RP. c_reflexive … RN → c_reflexive … RP → - ∀f.reflexive … (sex RN RP f). +lemma sex_refl (RN) (RP): + c_reflexive … RN → c_reflexive … RP → + ∀f.reflexive … (sex RN RP f). #RN #RP #HRN #HRP #f #L generalize in match f; -f elim L -L // #L #I #IH #f elim (pn_split f) * #g #H destruct /2 width=1 by sex_next, sex_push/ qed. -lemma sex_sym: ∀RN,RP. - (∀L1,L2,I1,I2. RN L1 I1 I2 → RN L2 I2 I1) → - (∀L1,L2,I1,I2. RP L1 I1 I2 → RP L2 I2 I1) → - ∀f. symmetric … (sex RN RP f). +lemma sex_sym (RN) (RP): + (∀L1,L2,I1,I2. RN L1 I1 I2 → RN L2 I2 I1) → + (∀L1,L2,I1,I2. RP L1 I1 I2 → RP L2 I2 I1) → + ∀f. symmetric … (sex RN RP f). #RN #RP #HRN #HRP #f #L1 #L2 #H elim H -L1 -L2 -f /3 width=2 by sex_next, sex_push/ qed-. -lemma sex_pair_repl: ∀RN,RP,f,I1,I2,L1,L2. - L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2] → - ∀J1,J2. RN L1 J1 J2 → RP L1 J1 J2 → - L1.ⓘ[J1] ⪤[RN,RP,f] L2.ⓘ[J2]. +lemma sex_pair_repl (RN) (RP): + ∀f,I1,I2,L1,L2. + L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2] → + ∀J1,J2. RN L1 J1 J2 → RP L1 J1 J2 → + L1.ⓘ[J1] ⪤[RN,RP,f] L2.ⓘ[J2]. /3 width=3 by sex_inv_tl, sex_fwd_bind/ qed-. -lemma sex_co: ∀RN1,RP1,RN2,RP2. RN1 ⊆ RN2 → RP1 ⊆ RP2 → - ∀f,L1,L2. L1 ⪤[RN1,RP1,f] L2 → L1 ⪤[RN2,RP2,f] L2. +lemma sex_co (RN1) (RP1) (RN2) (RP2): + RN1 ⊆ RN2 → RP1 ⊆ RP2 → + ∀f,L1,L2. L1 ⪤[RN1,RP1,f] L2 → L1 ⪤[RN2,RP2,f] L2. #RN1 #RP1 #RN2 #RP2 #HRN #HRP #f #L1 #L2 #H elim H -f -L1 -L2 /3 width=1 by sex_atom, sex_next, sex_push/ qed-. -lemma sex_co_isid: ∀RN1,RP1,RN2,RP2. RP1 ⊆ RP2 → - ∀f,L1,L2. L1 ⪤[RN1,RP1,f] L2 → 𝐈❪f❫ → - L1 ⪤[RN2,RP2,f] L2. +lemma sex_co_isid (RN1) (RP1) (RN2) (RP2): + RP1 ⊆ RP2 → + ∀f,L1,L2. L1 ⪤[RN1,RP1,f] L2 → 𝐈❪f❫ → + L1 ⪤[RN2,RP2,f] L2. #RN1 #RP1 #RN2 #RP2 #HR #f #L1 #L2 #H elim H -f -L1 -L2 // #f #I1 #I2 #K1 #K2 #_ #HI12 #IH #H [ elim (isid_inv_next … H) -H // @@ -219,9 +251,10 @@ lemma sex_co_isid: ∀RN1,RP1,RN2,RP2. RP1 ⊆ RP2 → ] qed-. -lemma sex_sdj: ∀RN,RP. RP ⊆ RN → - ∀f1,L1,L2. L1 ⪤[RN,RP,f1] L2 → - ∀f2. f1 ∥ f2 → L1 ⪤[RP,RN,f2] L2. +lemma sex_sdj (RN) (RP): + RP ⊆ RN → + ∀f1,L1,L2. L1 ⪤[RN,RP,f1] L2 → + ∀f2. f1 ∥ f2 → L1 ⪤[RP,RN,f2] L2. #RN #RP #HR #f1 #L1 #L2 #H elim H -f1 -L1 -L2 // #f1 #I1 #I2 #L1 #L2 #_ #HI12 #IH #f2 #H12 [ elim (sdj_inv_nx … H12) -H12 [2,3: // ] @@ -231,9 +264,10 @@ lemma sex_sdj: ∀RN,RP. RP ⊆ RN → ] qed-. -lemma sle_sex_trans: ∀RN,RP. RN ⊆ RP → - ∀f2,L1,L2. L1 ⪤[RN,RP,f2] L2 → - ∀f1. f1 ⊆ f2 → L1 ⪤[RN,RP,f1] L2. +lemma sle_sex_trans (RN) (RP): + RN ⊆ RP → + ∀f2,L1,L2. L1 ⪤[RN,RP,f2] L2 → + ∀f1. f1 ⊆ f2 → L1 ⪤[RN,RP,f1] L2. #RN #RP #HR #f2 #L1 #L2 #H elim H -f2 -L1 -L2 // #f2 #I1 #I2 #L1 #L2 #_ #HI12 #IH #f1 #H12 [ elim (pn_split f1) * ] @@ -244,9 +278,10 @@ lemma sle_sex_trans: ∀RN,RP. RN ⊆ RP → ] qed-. -lemma sle_sex_conf: ∀RN,RP. RP ⊆ RN → - ∀f1,L1,L2. L1 ⪤[RN,RP,f1] L2 → - ∀f2. f1 ⊆ f2 → L1 ⪤[RN,RP,f2] L2. +lemma sle_sex_conf (RN) (RP): + RP ⊆ RN → + ∀f1,L1,L2. L1 ⪤[RN,RP,f1] L2 → + ∀f2. f1 ⊆ f2 → L1 ⪤[RN,RP,f2] L2. #RN #RP #HR #f1 #L1 #L2 #H elim H -f1 -L1 -L2 // #f1 #I1 #I2 #L1 #L2 #_ #HI12 #IH #f2 #H12 [2: elim (pn_split f2) * ] @@ -257,9 +292,10 @@ lemma sle_sex_conf: ∀RN,RP. RP ⊆ RN → ] qed-. -lemma sex_sle_split: ∀R1,R2,RP. c_reflexive … R1 → c_reflexive … R2 → - ∀f,L1,L2. L1 ⪤[R1,RP,f] L2 → ∀g. f ⊆ g → - ∃∃L. L1 ⪤[R1,RP,g] L & L ⪤[R2,cfull,f] L2. +lemma sex_sle_split_sn (R1) (R2) (RP): + c_reflexive … R1 → c_reflexive … R2 → + ∀f,L1,L2. L1 ⪤[R1,RP,f] L2 → ∀g. f ⊆ g → + ∃∃L. L1 ⪤[R1,RP,g] L & L ⪤[R2,cfull,f] L2. #R1 #R2 #RP #HR1 #HR2 #f #L1 #L2 #H elim H -f -L1 -L2 [ /2 width=3 by sex_atom, ex2_intro/ ] #f #I1 #I2 #L1 #L2 #_ #HI12 #IH #y #H @@ -270,9 +306,10 @@ lemma sex_sle_split: ∀R1,R2,RP. c_reflexive … R1 → c_reflexive … R2 → ] qed-. -lemma sex_sdj_split: ∀R1,R2,RP. c_reflexive … R1 → c_reflexive … R2 → - ∀f,L1,L2. L1 ⪤[R1,RP,f] L2 → ∀g. f ∥ g → - ∃∃L. L1 ⪤[RP,R1,g] L & L ⪤[R2,cfull,f] L2. +lemma sex_sdj_split_sn (R1) (R2) (RP): + c_reflexive … R1 → c_reflexive … R2 → + ∀f,L1,L2. L1 ⪤[R1,RP,f] L2 → ∀g. f ∥ g → + ∃∃L. L1 ⪤[RP,R1,g] L & L ⪤[R2,cfull,f] L2. #R1 #R2 #RP #HR1 #HR2 #f #L1 #L2 #H elim H -f -L1 -L2 [ /2 width=3 by sex_atom, ex2_intro/ ] #f #I1 #I2 #L1 #L2 #_ #HI12 #IH #y #H @@ -283,10 +320,10 @@ lemma sex_sdj_split: ∀R1,R2,RP. c_reflexive … R1 → c_reflexive … R2 → ] qed-. -lemma sex_dec: ∀RN,RP. - (∀L,I1,I2. Decidable (RN L I1 I2)) → - (∀L,I1,I2. Decidable (RP L I1 I2)) → - ∀L1,L2,f. Decidable (L1 ⪤[RN,RP,f] L2). +lemma sex_dec (RN) (RP): + (∀L,I1,I2. Decidable (RN L I1 I2)) → + (∀L,I1,I2. Decidable (RP L I1 I2)) → + ∀L1,L2,f. Decidable (L1 ⪤[RN,RP,f] L2). #RN #RP #HRN #HRP #L1 elim L1 -L1 [ * | #L1 #I1 #IH * ] [ /2 width=1 by sex_atom, or_introl/ | #L2 #I2 #f @or_intror #H diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/sex_sex.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/sex_sex.ma index 342530903..9d3e2df4d 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/sex_sex.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/sex_sex.ma @@ -20,12 +20,12 @@ include "static_2/relocation/drops.ma". (* Main properties **********************************************************) theorem sex_trans_gen (RN1) (RP1) (RN2) (RP2) (RN) (RP): - ∀L1,f. - (∀g,I,K,n. ⇩[n] L1 ≘ K.ⓘ[I] → ↑g = ⫱*[n] f → sex_transitive RN1 RN2 RN RN1 RP1 g K I) → - (∀g,I,K,n. ⇩[n] L1 ≘ K.ⓘ[I] → ⫯g = ⫱*[n] f → sex_transitive RP1 RP2 RP RN1 RP1 g K I) → - ∀L0. L1 ⪤[RN1,RP1,f] L0 → - ∀L2. L0 ⪤[RN2,RP2,f] L2 → - L1 ⪤[RN,RP,f] L2. + ∀L1,f. + (∀g,I,K,n. ⇩[n] L1 ≘ K.ⓘ[I] → ↑g = ⫱*[n] f → R_pw_transitive_sex RN1 RN2 RN RN1 RP1 g K I) → + (∀g,I,K,n. ⇩[n] L1 ≘ K.ⓘ[I] → ⫯g = ⫱*[n] f → R_pw_transitive_sex RP1 RP2 RP RN1 RP1 g K I) → + ∀L0. L1 ⪤[RN1,RP1,f] L0 → + ∀L2. L0 ⪤[RN2,RP2,f] L2 → + L1 ⪤[RN,RP,f] L2. #RN1 #RP1 #RN2 #RP2 #RN #RP #L1 elim L1 -L1 [ #f #_ #_ #L0 #H1 #L2 #H2 lapply (sex_inv_atom1 … H1) -H1 #H destruct @@ -45,13 +45,15 @@ theorem sex_trans_gen (RN1) (RP1) (RN2) (RP2) (RN) (RP): ] qed-. -theorem sex_trans (RN) (RP) (f): (∀g,I,K. sex_transitive RN RN RN RN RP g K I) → - (∀g,I,K. sex_transitive RP RP RP RN RP g K I) → - Transitive … (sex RN RP f). +theorem sex_trans (RN) (RP) (f): + (∀g,I,K. R_pw_transitive_sex RN RN RN RN RP g K I) → + (∀g,I,K. R_pw_transitive_sex RP RP RP RN RP g K I) → + Transitive … (sex RN RP f). /2 width=9 by sex_trans_gen/ qed-. -theorem sex_trans_id_cfull: ∀R1,R2,R3,L1,L,f. L1 ⪤[R1,cfull,f] L → 𝐈❪f❫ → - ∀L2. L ⪤[R2,cfull,f] L2 → L1 ⪤[R3,cfull,f] L2. +theorem sex_trans_id_cfull (R1) (R2) (R3): + ∀L1,L,f. L1 ⪤[R1,cfull,f] L → 𝐈❪f❫ → + ∀L2. L ⪤[R2,cfull,f] L2 → L1 ⪤[R3,cfull,f] L2. #R1 #R2 #R3 #L1 #L #f #H elim H -L1 -L -f [ #f #Hf #L2 #H >(sex_inv_atom1 … H) -L2 // ] #f #I1 #I #K1 #K #HK1 #_ #IH #Hf #L2 #H @@ -61,10 +63,10 @@ elim (sex_inv_push1 … H) -H #I2 #K2 #HK2 #_ #H destruct qed-. theorem sex_conf (RN1) (RP1) (RN2) (RP2): - ∀L,f. - (∀g,I,K,n. ⇩[n] L ≘ K.ⓘ[I] → ↑g = ⫱*[n] f → R_pw_confluent2_sex RN1 RN2 RN1 RP1 RN2 RP2 g K I) → - (∀g,I,K,n. ⇩[n] L ≘ K.ⓘ[I] → ⫯g = ⫱*[n] f → R_pw_confluent2_sex RP1 RP2 RN1 RP1 RN2 RP2 g K I) → - pw_confluent2 … (sex RN1 RP1 f) (sex RN2 RP2 f) L. + ∀L,f. + (∀g,I,K,n. ⇩[n] L ≘ K.ⓘ[I] → ↑g = ⫱*[n] f → R_pw_confluent2_sex RN1 RN2 RN1 RP1 RN2 RP2 g K I) → + (∀g,I,K,n. ⇩[n] L ≘ K.ⓘ[I] → ⫯g = ⫱*[n] f → R_pw_confluent2_sex RP1 RP2 RN1 RP1 RN2 RP2 g K I) → + pw_confluent2 … (sex RN1 RP1 f) (sex RN2 RP2 f) L. #RN1 #RP1 #RN2 #RP2 #L elim L -L [ #f #_ #_ #L1 #H1 #L2 #H2 >(sex_inv_atom1 … H1) >(sex_inv_atom1 … H2) -H2 -H1 /2 width=3 by sex_atom, ex2_intro/ @@ -106,20 +108,20 @@ lemma sex_repl (RN) (RP) (SN) (SP) (L1) (f): ] qed-. -theorem sex_canc_sn: ∀RN,RP,f. Transitive … (sex RN RP f) → - symmetric … (sex RN RP f) → - left_cancellable … (sex RN RP f). +theorem sex_canc_sn (RN) (RP): + ∀f. Transitive … (sex RN RP f) → symmetric … (sex RN RP f) → + left_cancellable … (sex RN RP f). /3 width=3 by/ qed-. -theorem sex_canc_dx: ∀RN,RP,f. Transitive … (sex RN RP f) → - symmetric … (sex RN RP f) → - right_cancellable … (sex RN RP f). +theorem sex_canc_dx (RN) (RP): + ∀f. Transitive … (sex RN RP f) → symmetric … (sex RN RP f) → + right_cancellable … (sex RN RP f). /3 width=3 by/ qed-. -lemma sex_meet: ∀RN,RP,L1,L2. - ∀f1. L1 ⪤[RN,RP,f1] L2 → - ∀f2. L1 ⪤[RN,RP,f2] L2 → - ∀f. f1 ⋒ f2 ≘ f → L1 ⪤[RN,RP,f] L2. +lemma sex_meet (RN) (RP) (L1) (L2): + ∀f1. L1 ⪤[RN,RP,f1] L2 → + ∀f2. L1 ⪤[RN,RP,f2] L2 → + ∀f. f1 ⋒ f2 ≘ f → L1 ⪤[RN,RP,f] L2. #RN #RP #L1 #L2 #f1 #H elim H -f1 -L1 -L2 // #f1 #I1 #I2 #L1 #L2 #_ #HI12 #IH #f2 #H #f #Hf elim (pn_split f2) * #g2 #H2 destruct @@ -129,10 +131,10 @@ try elim (sex_inv_push … H) try elim (sex_inv_next … H) -H ] -Hf /3 width=5 by sex_next, sex_push/ qed-. -lemma sex_join: ∀RN,RP,L1,L2. - ∀f1. L1 ⪤[RN,RP,f1] L2 → - ∀f2. L1 ⪤[RN,RP,f2] L2 → - ∀f. f1 ⋓ f2 ≘ f → L1 ⪤[RN,RP,f] L2. +lemma sex_join (RN) (RP) (L1) (L2): + ∀f1. L1 ⪤[RN,RP,f1] L2 → + ∀f2. L1 ⪤[RN,RP,f2] L2 → + ∀f. f1 ⋓ f2 ≘ f → L1 ⪤[RN,RP,f] L2. #RN #RP #L1 #L2 #f1 #H elim H -f1 -L1 -L2 // #f1 #I1 #I2 #L1 #L2 #_ #HI12 #IH #f2 #H #f #Hf elim (pn_split f2) * #g2 #H2 destruct diff --git a/matita/matita/contribs/lambdadelta/static_2/static/feqx.ma b/matita/matita/contribs/lambdadelta/static_2/static/feqx.ma index 2ec73d338..82867f626 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/feqx.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/feqx.ma @@ -24,26 +24,29 @@ inductive feqx (G) (L1) (T1): relation3 genv lenv term ≝ . interpretation - "sort-irrelevant equivalence on referred entries (closure)" - 'StarEqSn G1 L1 T1 G2 L2 T2 = (feqx G1 L1 T1 G2 L2 T2). + "sort-irrelevant equivalence on referred entries (closure)" + 'StarEqSn G1 L1 T1 G2 L2 T2 = (feqx G1 L1 T1 G2 L2 T2). (* Basic_properties *********************************************************) -lemma feqx_intro_dx (G): ∀L1,L2,T2. L1 ≛[T2] L2 → - ∀T1. T1 ≛ T2 → ❪G,L1,T1❫ ≛ ❪G,L2,T2❫. +lemma feqx_intro_dx (G): + ∀L1,L2,T2. L1 ≛[T2] L2 → + ∀T1. T1 ≛ T2 → ❪G,L1,T1❫ ≛ ❪G,L2,T2❫. /3 width=3 by feqx_intro_sn, teqx_reqx_div/ qed. (* Basic inversion lemmas ***************************************************) -lemma feqx_inv_gen_sn: ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ → - ∧∧ G1 = G2 & L1 ≛[T1] L2 & T1 ≛ T2. +lemma feqx_inv_gen_sn: + ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ → + ∧∧ G1 = G2 & L1 ≛[T1] L2 & T1 ≛ T2. #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=1 by and3_intro/ qed-. -lemma feqx_inv_gen_dx: ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ → - ∧∧ G1 = G2 & L1 ≛[T2] L2 & T1 ≛ T2. +lemma feqx_inv_gen_dx: + ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ → + ∧∧ G1 = G2 & L1 ≛[T2] L2 & T1 ≛ T2. #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 -/3 width=3 by teqx_reqx_conf, and3_intro/ +/3 width=3 by teqx_reqx_conf_sn, and3_intro/ qed-. (* Basic_2A1: removed theorems 6: diff --git a/matita/matita/contribs/lambdadelta/static_2/static/feqx_fqus.ma b/matita/matita/contribs/lambdadelta/static_2/static/feqx_fqus.ma index cf59d2269..0b370bd33 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/feqx_fqus.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/feqx_fqus.ma @@ -19,13 +19,14 @@ include "static_2/static/feqx.ma". (* Properties with star-iterated structural successor for closures **********) -lemma feqx_fqus_trans: ∀b,G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≛ ❪G,L,T❫ → - ∀G2,L2,T2. ❪G,L,T❫ ⬂*[b] ❪G2,L2,T2❫ → - ∃∃G,L0,T0. ❪G1,L1,T1❫ ⬂*[b] ❪G,L0,T0❫ & ❪G,L0,T0❫ ≛ ❪G2,L2,T2❫. +lemma feqx_fqus_trans (b): + ∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≛ ❪G,L,T❫ → + ∀G2,L2,T2. ❪G,L,T❫ ⬂*[b] ❪G2,L2,T2❫ → + ∃∃G,L0,T0. ❪G1,L1,T1❫ ⬂*[b] ❪G,L0,T0❫ & ❪G,L0,T0❫ ≛ ❪G2,L2,T2❫. #b #G1 #G #L1 #L #T1 #T #H1 #G2 #L2 #T2 #H2 elim(feqx_inv_gen_dx … H1) -H1 #HG #HL1 #HT1 destruct elim (reqx_fqus_trans … H2 … HL1) -L #L #T0 #H2 #HT02 #HL2 elim (teqx_fqus_trans … H2 … HT1) -T #L0 #T #H2 #HT0 #HL0 -lapply (teqx_reqx_conf … HT02 … HL0) -HL0 #HL0 +lapply (teqx_reqx_conf_sn … HT02 … HL0) -HL0 #HL0 /4 width=7 by feqx_intro_dx, reqx_trans, teqx_trans, ex2_3_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/static/req.ma b/matita/matita/contribs/lambdadelta/static_2/static/req.ma index fcd79b33a..b53ef1755 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/req.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/req.ma @@ -19,65 +19,73 @@ include "static_2/static/rex.ma". (* Basic_2A1: was: lleq *) definition req: relation3 term lenv lenv ≝ - rex ceq. + rex ceq. interpretation - "syntactic equivalence on referred entries (local environment)" - 'IdEqSn T L1 L2 = (req T L1 L2). + "syntactic equivalence on referred entries (local environment)" + 'IdEqSn T L1 L2 = (req T L1 L2). -(* Note: "req_transitive R" is equivalent to "rex_transitive ceq R R" *) +(* Note: "R_transitive_req R" is equivalent to "R_transitive_rex ceq R R" *) (* Basic_2A1: uses: lleq_transitive *) -definition req_transitive: predicate (relation3 lenv term term) ≝ +definition R_transitive_req: predicate (relation3 lenv term term) ≝ λR. ∀L2,T1,T2. R L2 T1 T2 → ∀L1. L1 ≡[T1] L2 → R L1 T1 T2. (* Basic inversion lemmas ***************************************************) -lemma req_inv_bind: ∀p,I,L1,L2,V,T. L1 ≡[ⓑ[p,I]V.T] L2 → - ∧∧ L1 ≡[V] L2 & L1.ⓑ[I]V ≡[T] L2.ⓑ[I]V. +lemma req_inv_bind: + ∀p,I,L1,L2,V,T. L1 ≡[ⓑ[p,I]V.T] L2 → + ∧∧ L1 ≡[V] L2 & L1.ⓑ[I]V ≡[T] L2.ⓑ[I]V. /2 width=2 by rex_inv_bind/ qed-. -lemma req_inv_flat: ∀I,L1,L2,V,T. L1 ≡[ⓕ[I]V.T] L2 → - ∧∧ L1 ≡[V] L2 & L1 ≡[T] L2. +lemma req_inv_flat: + ∀I,L1,L2,V,T. L1 ≡[ⓕ[I]V.T] L2 → + ∧∧ L1 ≡[V] L2 & L1 ≡[T] L2. /2 width=2 by rex_inv_flat/ qed-. (* Advanced inversion lemmas ************************************************) -lemma req_inv_zero_pair_sn: ∀I,L2,K1,V. K1.ⓑ[I]V ≡[#0] L2 → - ∃∃K2. K1 ≡[V] K2 & L2 = K2.ⓑ[I]V. +lemma req_inv_zero_pair_sn: + ∀I,L2,K1,V. K1.ⓑ[I]V ≡[#0] L2 → + ∃∃K2. K1 ≡[V] K2 & L2 = K2.ⓑ[I]V. #I #L2 #K1 #V #H elim (rex_inv_zero_pair_sn … H) -H #K2 #X #HK12 #HX #H destruct /2 width=3 by ex2_intro/ qed-. -lemma req_inv_zero_pair_dx: ∀I,L1,K2,V. L1 ≡[#0] K2.ⓑ[I]V → - ∃∃K1. K1 ≡[V] K2 & L1 = K1.ⓑ[I]V. +lemma req_inv_zero_pair_dx: + ∀I,L1,K2,V. L1 ≡[#0] K2.ⓑ[I]V → + ∃∃K1. K1 ≡[V] K2 & L1 = K1.ⓑ[I]V. #I #L1 #K2 #V #H elim (rex_inv_zero_pair_dx … H) -H #K1 #X #HK12 #HX #H destruct /2 width=3 by ex2_intro/ qed-. -lemma req_inv_lref_bind_sn: ∀I1,K1,L2,i. K1.ⓘ[I1] ≡[#↑i] L2 → - ∃∃I2,K2. K1 ≡[#i] K2 & L2 = K2.ⓘ[I2]. +lemma req_inv_lref_bind_sn: + ∀I1,K1,L2,i. K1.ⓘ[I1] ≡[#↑i] L2 → + ∃∃I2,K2. K1 ≡[#i] K2 & L2 = K2.ⓘ[I2]. /2 width=2 by rex_inv_lref_bind_sn/ qed-. -lemma req_inv_lref_bind_dx: ∀I2,K2,L1,i. L1 ≡[#↑i] K2.ⓘ[I2] → - ∃∃I1,K1. K1 ≡[#i] K2 & L1 = K1.ⓘ[I1]. +lemma req_inv_lref_bind_dx: + ∀I2,K2,L1,i. L1 ≡[#↑i] K2.ⓘ[I2] → + ∃∃I1,K1. K1 ≡[#i] K2 & L1 = K1.ⓘ[I1]. /2 width=2 by rex_inv_lref_bind_dx/ qed-. (* Basic forward lemmas *****************************************************) (* Basic_2A1: was: llpx_sn_lrefl *) (* Basic_2A1: this should have been lleq_fwd_llpx_sn *) -lemma req_fwd_rex: ∀R. c_reflexive … R → - ∀L1,L2,T. L1 ≡[T] L2 → L1 ⪤[R,T] L2. +lemma req_fwd_rex (R): + c_reflexive … R → + ∀L1,L2,T. L1 ≡[T] L2 → L1 ⪤[R,T] L2. #R #HR #L1 #L2 #T * #f #Hf #HL12 /4 width=7 by sex_co, cext2_co, ex2_intro/ qed-. (* Basic_properties *********************************************************) -lemma frees_req_conf: ∀f,L1,T. L1 ⊢ 𝐅+❪T❫ ≘ f → - ∀L2. L1 ≡[T] L2 → L2 ⊢ 𝐅+❪T❫ ≘ f. +lemma frees_req_conf: + ∀f,L1,T. L1 ⊢ 𝐅+❪T❫ ≘ f → + ∀L2. L1 ≡[T] L2 → L2 ⊢ 𝐅+❪T❫ ≘ f. #f #L1 #T #H elim H -f -L1 -T [ /2 width=3 by frees_sort/ | #f #i #Hf #L2 #H2 diff --git a/matita/matita/contribs/lambdadelta/static_2/static/req_fsle.ma b/matita/matita/contribs/lambdadelta/static_2/static/req_fsle.ma index efafbb903..b58cafd67 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/req_fsle.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/req_fsle.ma @@ -20,7 +20,8 @@ include "static_2/static/req.ma". (* Properties with free variables inclusion for restricted closures *********) -lemma req_fsle_comp: rex_fsle_compatible ceq. +lemma req_fsle_comp: + rex_fsle_compatible ceq. #L1 #L2 #T #HL12 elim (frees_total L1 T) /4 width=8 by frees_req_conf, rex_fwd_length, lveq_length_eq, sle_refl, ex4_4_intro/ @@ -28,6 +29,7 @@ qed. (* Forward lemmas with free variables inclusion for restricted closures *****) -lemma req_rex_trans: ∀R. req_transitive R → - ∀L1,L,T. L1 ≡[T] L → ∀L2. L ⪤[R,T] L2 → L1 ⪤[R,T] L2. +lemma req_rex_trans (R): + R_transitive_req R → + ∀L1,L,T. L1 ≡[T] L → ∀L2. L ⪤[R,T] L2 → L1 ⪤[R,T] L2. /4 width=16 by req_fsle_comp, rex_trans_fsle, rex_trans_next/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/static/req_length.ma b/matita/matita/contribs/lambdadelta/static_2/static/req_length.ma new file mode 100644 index 000000000..e5bd7b4a8 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/static/req_length.ma @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "static_2/static/rex_length.ma". +include "static_2/static/rex_fsle.ma". +include "static_2/static/req.ma". + +(* SYNTACTIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *********) + +(* Advanved properties with free variables inclusion ************************) + +lemma req_fsge_comp: + rex_fsge_compatible ceq. +#L1 #L2 #T #H elim H #f1 #Hf1 #HL12 +lapply (frees_req_conf … Hf1 … H) -H +lapply (sex_fwd_length … HL12) +/3 width=8 by lveq_length_eq, ex4_4_intro/ (**) (* full auto fails *) +qed-. + +(* Advanced properties ******************************************************) + +(* Basic_2A1: uses: lleq_sym *) +lemma req_sym (T): + symmetric … (req T). +/3 width=1 by req_fsge_comp, rex_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/static/reqx.ma b/matita/matita/contribs/lambdadelta/static_2/static/reqx.ma index 25d445ee6..251814a3b 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/reqx.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/reqx.ma @@ -18,21 +18,22 @@ include "static_2/static/rex.ma". (* SORT-IRRELEVANT EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ***) -definition reqx: relation3 term lenv lenv ≝ - rex cdeq. +definition reqx: relation3 … ≝ + rex cdeq. interpretation - "sort-irrelevant equivalence on referred entries (local environment)" - 'StarEqSn T L1 L2 = (reqx T L1 L2). + "sort-irrelevant equivalence on referred entries (local environment)" + 'StarEqSn T L1 L2 = (reqx T L1 L2). interpretation - "sort-irrelevant ranged equivalence (local environment)" - 'StarEqSn f L1 L2 = (sex cdeq_ext cfull f L1 L2). + "sort-irrelevant ranged equivalence (local environment)" + 'StarEqSn f L1 L2 = (sex cdeq_ext cfull f L1 L2). (* Basic properties ***********************************************************) -lemma frees_teqx_conf_reqx: ∀f,L1,T1. L1 ⊢ 𝐅+❪T1❫ ≘ f → ∀T2. T1 ≛ T2 → - ∀L2. L1 ≛[f] L2 → L2 ⊢ 𝐅+❪T2❫ ≘ f. +lemma frees_teqx_conf_reqx: + ∀f,L1,T1. L1 ⊢ 𝐅+❪T1❫ ≘ f → ∀T2. T1 ≛ T2 → + ∀L2. L1 ≛[f] L2 → L2 ⊢ 𝐅+❪T2❫ ≘ f. #f #L1 #T1 #H elim H -f -L1 -T1 [ #f #L1 #s1 #Hf #X #H1 #L2 #_ elim (teqx_inv_sort1 … H1) -H1 #s2 #H destruct @@ -65,65 +66,77 @@ lemma frees_teqx_conf_reqx: ∀f,L1,T1. L1 ⊢ 𝐅+❪T1❫ ≘ f → ∀T2. T1 ] qed-. -lemma frees_teqx_conf: ∀f,L,T1. L ⊢ 𝐅+❪T1❫ ≘ f → - ∀T2. T1 ≛ T2 → L ⊢ 𝐅+❪T2❫ ≘ f. +lemma frees_teqx_conf: + ∀f,L,T1. L ⊢ 𝐅+❪T1❫ ≘ f → + ∀T2. T1 ≛ T2 → L ⊢ 𝐅+❪T2❫ ≘ f. /4 width=7 by frees_teqx_conf_reqx, sex_refl, ext2_refl/ qed-. -lemma frees_reqx_conf: ∀f,L1,T. L1 ⊢ 𝐅+❪T❫ ≘ f → - ∀L2. L1 ≛[f] L2 → L2 ⊢ 𝐅+❪T❫ ≘ f. +lemma frees_reqx_conf: + ∀f,L1,T. L1 ⊢ 𝐅+❪T❫ ≘ f → + ∀L2. L1 ≛[f] L2 → L2 ⊢ 𝐅+❪T❫ ≘ f. /2 width=7 by frees_teqx_conf_reqx, teqx_refl/ qed-. -lemma teqx_rex_conf (R): s_r_confluent1 … cdeq (rex R). +lemma teqx_rex_conf_sn (R): + s_r_confluent1 … cdeq (rex R). #R #L1 #T1 #T2 #HT12 #L2 * /3 width=5 by frees_teqx_conf, ex2_intro/ qed-. -lemma teqx_rex_div (R): ∀T1,T2. T1 ≛ T2 → - ∀L1,L2. L1 ⪤[R,T2] L2 → L1 ⪤[R,T1] L2. -/3 width=5 by teqx_rex_conf, teqx_sym/ qed-. +lemma teqx_rex_div (R): + ∀T1,T2. T1 ≛ T2 → + ∀L1,L2. L1 ⪤[R,T2] L2 → L1 ⪤[R,T1] L2. +/3 width=5 by teqx_rex_conf_sn, teqx_sym/ qed-. -lemma teqx_reqx_conf: s_r_confluent1 … cdeq reqx. -/2 width=5 by teqx_rex_conf/ qed-. +lemma teqx_reqx_conf_sn: + s_r_confluent1 … cdeq reqx. +/2 width=5 by teqx_rex_conf_sn/ qed-. -lemma teqx_reqx_div: ∀T1,T2. T1 ≛ T2 → - ∀L1,L2. L1 ≛[T2] L2 → L1 ≛[T1] L2. +lemma teqx_reqx_div: + ∀T1,T2. T1 ≛ T2 → + ∀L1,L2. L1 ≛[T2] L2 → L1 ≛[T1] L2. /2 width=5 by teqx_rex_div/ qed-. lemma reqx_atom: ∀I. ⋆ ≛[⓪[I]] ⋆. /2 width=1 by rex_atom/ qed. -lemma reqx_sort: ∀I1,I2,L1,L2,s. - L1 ≛[⋆s] L2 → L1.ⓘ[I1] ≛[⋆s] L2.ⓘ[I2]. +lemma reqx_sort: + ∀I1,I2,L1,L2,s. + L1 ≛[⋆s] L2 → L1.ⓘ[I1] ≛[⋆s] L2.ⓘ[I2]. /2 width=1 by rex_sort/ qed. -lemma reqx_pair: ∀I,L1,L2,V1,V2. - L1 ≛[V1] L2 → V1 ≛ V2 → L1.ⓑ[I]V1 ≛[#0] L2.ⓑ[I]V2. +lemma reqx_pair: + ∀I,L1,L2,V1,V2. + L1 ≛[V1] L2 → V1 ≛ V2 → L1.ⓑ[I]V1 ≛[#0] L2.ⓑ[I]V2. /2 width=1 by rex_pair/ qed. -lemma reqx_unit: ∀f,I,L1,L2. 𝐈❪f❫ → L1 ≛[f] L2 → - L1.ⓤ[I] ≛[#0] L2.ⓤ[I]. +lemma reqx_unit: + ∀f,I,L1,L2. 𝐈❪f❫ → L1 ≛[f] L2 → + L1.ⓤ[I] ≛[#0] L2.ⓤ[I]. /2 width=3 by rex_unit/ qed. -lemma reqx_lref: ∀I1,I2,L1,L2,i. - L1 ≛[#i] L2 → L1.ⓘ[I1] ≛[#↑i] L2.ⓘ[I2]. +lemma reqx_lref: + ∀I1,I2,L1,L2,i. + L1 ≛[#i] L2 → L1.ⓘ[I1] ≛[#↑i] L2.ⓘ[I2]. /2 width=1 by rex_lref/ qed. -lemma reqx_gref: ∀I1,I2,L1,L2,l. - L1 ≛[§l] L2 → L1.ⓘ[I1] ≛[§l] L2.ⓘ[I2]. +lemma reqx_gref: + ∀I1,I2,L1,L2,l. + L1 ≛[§l] L2 → L1.ⓘ[I1] ≛[§l] L2.ⓘ[I2]. /2 width=1 by rex_gref/ qed. -lemma reqx_bind_repl_dx: ∀I,I1,L1,L2.∀T:term. - L1.ⓘ[I] ≛[T] L2.ⓘ[I1] → - ∀I2. I ≛ I2 → - L1.ⓘ[I] ≛[T] L2.ⓘ[I2]. +lemma reqx_bind_repl_dx: + ∀I,I1,L1,L2.∀T:term. L1.ⓘ[I] ≛[T] L2.ⓘ[I1] → + ∀I2. I ≛ I2 → L1.ⓘ[I] ≛[T] L2.ⓘ[I2]. /2 width=2 by rex_bind_repl_dx/ qed-. (* Basic inversion lemmas ***************************************************) -lemma reqx_inv_atom_sn: ∀Y2. ∀T:term. ⋆ ≛[T] Y2 → Y2 = ⋆. +lemma reqx_inv_atom_sn: + ∀Y2. ∀T:term. ⋆ ≛[T] Y2 → Y2 = ⋆. /2 width=3 by rex_inv_atom_sn/ qed-. -lemma reqx_inv_atom_dx: ∀Y1. ∀T:term. Y1 ≛[T] ⋆ → Y1 = ⋆. +lemma reqx_inv_atom_dx: + ∀Y1. ∀T:term. Y1 ≛[T] ⋆ → Y1 = ⋆. /2 width=3 by rex_inv_atom_dx/ qed-. lemma reqx_inv_zero: @@ -135,59 +148,70 @@ lemma reqx_inv_zero: /3 width=9 by or3_intro0, or3_intro1, or3_intro2, ex4_5_intro, ex4_4_intro, conj/ qed-. -lemma reqx_inv_lref: ∀Y1,Y2,i. Y1 ≛[#↑i] Y2 → - ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆ - | ∃∃I1,I2,L1,L2. L1 ≛[#i] L2 & - Y1 = L1.ⓘ[I1] & Y2 = L2.ⓘ[I2]. +lemma reqx_inv_lref: + ∀Y1,Y2,i. Y1 ≛[#↑i] Y2 → + ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆ + | ∃∃I1,I2,L1,L2. L1 ≛[#i] L2 & Y1 = L1.ⓘ[I1] & Y2 = L2.ⓘ[I2]. /2 width=1 by rex_inv_lref/ qed-. (* Basic_2A1: uses: lleq_inv_bind lleq_inv_bind_O *) -lemma reqx_inv_bind: ∀p,I,L1,L2,V,T. L1 ≛[ⓑ[p,I]V.T] L2 → - ∧∧ L1 ≛[V] L2 & L1.ⓑ[I]V ≛[T] L2.ⓑ[I]V. +lemma reqx_inv_bind: + ∀p,I,L1,L2,V,T. L1 ≛[ⓑ[p,I]V.T] L2 → + ∧∧ L1 ≛[V] L2 & L1.ⓑ[I]V ≛[T] L2.ⓑ[I]V. /2 width=2 by rex_inv_bind/ qed-. (* Basic_2A1: uses: lleq_inv_flat *) -lemma reqx_inv_flat: ∀I,L1,L2,V,T. L1 ≛[ⓕ[I]V.T] L2 → - ∧∧ L1 ≛[V] L2 & L1 ≛[T] L2. +lemma reqx_inv_flat: + ∀I,L1,L2,V,T. L1 ≛[ⓕ[I]V.T] L2 → + ∧∧ L1 ≛[V] L2 & L1 ≛[T] L2. /2 width=2 by rex_inv_flat/ qed-. (* Advanced inversion lemmas ************************************************) -lemma reqx_inv_zero_pair_sn: ∀I,Y2,L1,V1. L1.ⓑ[I]V1 ≛[#0] Y2 → - ∃∃L2,V2. L1 ≛[V1] L2 & V1 ≛ V2 & Y2 = L2.ⓑ[I]V2. +lemma reqx_inv_zero_pair_sn: + ∀I,Y2,L1,V1. L1.ⓑ[I]V1 ≛[#0] Y2 → + ∃∃L2,V2. L1 ≛[V1] L2 & V1 ≛ V2 & Y2 = L2.ⓑ[I]V2. /2 width=1 by rex_inv_zero_pair_sn/ qed-. -lemma reqx_inv_zero_pair_dx: ∀I,Y1,L2,V2. Y1 ≛[#0] L2.ⓑ[I]V2 → - ∃∃L1,V1. L1 ≛[V1] L2 & V1 ≛ V2 & Y1 = L1.ⓑ[I]V1. +lemma reqx_inv_zero_pair_dx: + ∀I,Y1,L2,V2. Y1 ≛[#0] L2.ⓑ[I]V2 → + ∃∃L1,V1. L1 ≛[V1] L2 & V1 ≛ V2 & Y1 = L1.ⓑ[I]V1. /2 width=1 by rex_inv_zero_pair_dx/ qed-. -lemma reqx_inv_lref_bind_sn: ∀I1,Y2,L1,i. L1.ⓘ[I1] ≛[#↑i] Y2 → - ∃∃I2,L2. L1 ≛[#i] L2 & Y2 = L2.ⓘ[I2]. +lemma reqx_inv_lref_bind_sn: + ∀I1,Y2,L1,i. L1.ⓘ[I1] ≛[#↑i] Y2 → + ∃∃I2,L2. L1 ≛[#i] L2 & Y2 = L2.ⓘ[I2]. /2 width=2 by rex_inv_lref_bind_sn/ qed-. -lemma reqx_inv_lref_bind_dx: ∀I2,Y1,L2,i. Y1 ≛[#↑i] L2.ⓘ[I2] → - ∃∃I1,L1. L1 ≛[#i] L2 & Y1 = L1.ⓘ[I1]. +lemma reqx_inv_lref_bind_dx: + ∀I2,Y1,L2,i. Y1 ≛[#↑i] L2.ⓘ[I2] → + ∃∃I1,L1. L1 ≛[#i] L2 & Y1 = L1.ⓘ[I1]. /2 width=2 by rex_inv_lref_bind_dx/ qed-. (* Basic forward lemmas *****************************************************) -lemma reqx_fwd_zero_pair: ∀I,K1,K2,V1,V2. - K1.ⓑ[I]V1 ≛[#0] K2.ⓑ[I]V2 → K1 ≛[V1] K2. +lemma reqx_fwd_zero_pair: + ∀I,K1,K2,V1,V2. + K1.ⓑ[I]V1 ≛[#0] K2.ⓑ[I]V2 → K1 ≛[V1] K2. /2 width=3 by rex_fwd_zero_pair/ qed-. (* Basic_2A1: uses: lleq_fwd_bind_sn lleq_fwd_flat_sn *) -lemma reqx_fwd_pair_sn: ∀I,L1,L2,V,T. L1 ≛[②[I]V.T] L2 → L1 ≛[V] L2. +lemma reqx_fwd_pair_sn: + ∀I,L1,L2,V,T. L1 ≛[②[I]V.T] L2 → L1 ≛[V] L2. /2 width=3 by rex_fwd_pair_sn/ qed-. (* Basic_2A1: uses: lleq_fwd_bind_dx lleq_fwd_bind_O_dx *) -lemma reqx_fwd_bind_dx: ∀p,I,L1,L2,V,T. - L1 ≛[ⓑ[p,I]V.T] L2 → L1.ⓑ[I]V ≛[T] L2.ⓑ[I]V. +lemma reqx_fwd_bind_dx: + ∀p,I,L1,L2,V,T. + L1 ≛[ⓑ[p,I]V.T] L2 → L1.ⓑ[I]V ≛[T] L2.ⓑ[I]V. /2 width=2 by rex_fwd_bind_dx/ qed-. (* Basic_2A1: uses: lleq_fwd_flat_dx *) -lemma reqx_fwd_flat_dx: ∀I,L1,L2,V,T. L1 ≛[ⓕ[I]V.T] L2 → L1 ≛[T] L2. +lemma reqx_fwd_flat_dx: + ∀I,L1,L2,V,T. L1 ≛[ⓕ[I]V.T] L2 → L1 ≛[T] L2. /2 width=3 by rex_fwd_flat_dx/ qed-. -lemma reqx_fwd_dx: ∀I2,L1,K2. ∀T:term. L1 ≛[T] K2.ⓘ[I2] → - ∃∃I1,K1. L1 = K1.ⓘ[I1]. +lemma reqx_fwd_dx: + ∀I2,L1,K2. ∀T:term. L1 ≛[T] K2.ⓘ[I2] → + ∃∃I1,K1. L1 = K1.ⓘ[I1]. /2 width=5 by rex_fwd_dx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/static/reqx_fqus.ma b/matita/matita/contribs/lambdadelta/static_2/static/reqx_fqus.ma index 6f9b14b42..b5f80fc34 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/reqx_fqus.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/reqx_fqus.ma @@ -21,9 +21,10 @@ include "static_2/static/reqx_reqx.ma". (* Properties with extended structural successor for closures ***************) -lemma fqu_teqx_conf: ∀b,G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂[b] ❪G2,L2,T1❫ → - ∀U2. U1 ≛ U2 → - ∃∃L,T2. ❪G1,L1,U2❫ ⬂[b] ❪G2,L,T2❫ & L2 ≛[T1] L & T1 ≛ T2. +lemma fqu_teqx_conf (b): + ∀G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂[b] ❪G2,L2,T1❫ → + ∀U2. U1 ≛ U2 → + ∃∃L,T2. ❪G1,L1,U2❫ ⬂[b] ❪G2,L,T2❫ & L2 ≛[T1] L & T1 ≛ T2. #b #G1 #G2 #L1 #L2 #U1 #T1 #H elim H -G1 -G2 -L1 -L2 -U1 -T1 [ #I #G #L #W #X #H >(teqx_inv_lref1 … H) -X /2 width=5 by fqu_lref_O, ex3_2_intro/ @@ -45,22 +46,24 @@ lemma fqu_teqx_conf: ∀b,G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂[b] ❪G2,L2,T1 ] qed-. -lemma teqx_fqu_trans: ∀b,G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂[b] ❪G2,L2,T1❫ → - ∀U2. U2 ≛ U1 → - ∃∃L,T2. ❪G1,L1,U2❫ ⬂[b] ❪G2,L,T2❫ & T2 ≛ T1 & L ≛[T1] L2. +lemma teqx_fqu_trans (b): + ∀G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂[b] ❪G2,L2,T1❫ → + ∀U2. U2 ≛ U1 → + ∃∃L,T2. ❪G1,L1,U2❫ ⬂[b] ❪G2,L,T2❫ & T2 ≛ T1 & L ≛[T1] L2. #b #G1 #G2 #L1 #L2 #U1 #T1 #H12 #U2 #HU21 elim (fqu_teqx_conf … H12 U2) -H12 /3 width=5 by reqx_sym, teqx_sym, ex3_2_intro/ qed-. (* Basic_2A1: uses: lleq_fqu_trans *) -lemma reqx_fqu_trans: ∀b,G1,G2,L2,K2,T,U. ❪G1,L2,T❫ ⬂[b] ❪G2,K2,U❫ → - ∀L1. L1 ≛[T] L2 → - ∃∃K1,U0. ❪G1,L1,T❫ ⬂[b] ❪G2,K1,U0❫ & U0 ≛ U & K1 ≛[U] K2. +lemma reqx_fqu_trans (b): + ∀G1,G2,L2,K2,T,U. ❪G1,L2,T❫ ⬂[b] ❪G2,K2,U❫ → + ∀L1. L1 ≛[T] L2 → + ∃∃K1,U0. ❪G1,L1,T❫ ⬂[b] ❪G2,K1,U0❫ & U0 ≛ U & K1 ≛[U] K2. #b #G1 #G2 #L2 #K2 #T #U #H elim H -G1 -G2 -L2 -K2 -T -U [ #I #G #L2 #V2 #L1 #H elim (reqx_inv_zero_pair_dx … H) -H #K1 #V1 #HV1 #HV12 #H destruct - /3 width=7 by teqx_reqx_conf, fqu_lref_O, ex3_2_intro/ + /3 width=7 by teqx_reqx_conf_sn, fqu_lref_O, ex3_2_intro/ | * [ #p ] #I #G #L2 #V #T #L1 #H [ elim (reqx_inv_bind … H) | elim (reqx_inv_flat … H) @@ -80,9 +83,10 @@ qed-. (* Properties with optional structural successor for closures ***************) -lemma teqx_fquq_trans: ∀b,G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂⸮[b] ❪G2,L2,T1❫ → - ∀U2. U2 ≛ U1 → - ∃∃L,T2. ❪G1,L1,U2❫ ⬂⸮[b] ❪G2,L,T2❫ & T2 ≛ T1 & L ≛[T1] L2. +lemma teqx_fquq_trans (b): + ∀G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂⸮[b] ❪G2,L2,T1❫ → + ∀U2. U2 ≛ U1 → + ∃∃L,T2. ❪G1,L1,U2❫ ⬂⸮[b] ❪G2,L,T2❫ & T2 ≛ T1 & L ≛[T1] L2. #b #G1 #G2 #L1 #L2 #U1 #T1 #H elim H -H [ #H #U2 #HU21 elim (teqx_fqu_trans … H … HU21) -U1 /3 width=5 by fqu_fquq, ex3_2_intro/ @@ -91,9 +95,10 @@ lemma teqx_fquq_trans: ∀b,G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂⸮[b] ❪G2,L2 qed-. (* Basic_2A1: was just: lleq_fquq_trans *) -lemma reqx_fquq_trans: ∀b,G1,G2,L2,K2,T,U. ❪G1,L2,T❫ ⬂⸮[b] ❪G2,K2,U❫ → - ∀L1. L1 ≛[T] L2 → - ∃∃K1,U0. ❪G1,L1,T❫ ⬂⸮[b] ❪G2,K1,U0❫ & U0 ≛ U & K1 ≛[U] K2. +lemma reqx_fquq_trans (b): + ∀G1,G2,L2,K2,T,U. ❪G1,L2,T❫ ⬂⸮[b] ❪G2,K2,U❫ → + ∀L1. L1 ≛[T] L2 → + ∃∃K1,U0. ❪G1,L1,T❫ ⬂⸮[b] ❪G2,K1,U0❫ & U0 ≛ U & K1 ≛[U] K2. #b #G1 #G2 #L2 #K2 #T #U #H elim H -H [ #H #L1 #HL12 elim (reqx_fqu_trans … H … HL12) -L2 /3 width=5 by fqu_fquq, ex3_2_intro/ | * #HG #HL #HT destruct /2 width=5 by ex3_2_intro/ @@ -103,9 +108,10 @@ qed-. (* Properties with plus-iterated structural successor for closures **********) (* Basic_2A1: was just: lleq_fqup_trans *) -lemma reqx_fqup_trans: ∀b,G1,G2,L2,K2,T,U. ❪G1,L2,T❫ ⬂+[b] ❪G2,K2,U❫ → - ∀L1. L1 ≛[T] L2 → - ∃∃K1,U0. ❪G1,L1,T❫ ⬂+[b] ❪G2,K1,U0❫ & U0 ≛ U & K1 ≛[U] K2. +lemma reqx_fqup_trans (b): + ∀G1,G2,L2,K2,T,U. ❪G1,L2,T❫ ⬂+[b] ❪G2,K2,U❫ → + ∀L1. L1 ≛[T] L2 → + ∃∃K1,U0. ❪G1,L1,T❫ ⬂+[b] ❪G2,K1,U0❫ & U0 ≛ U & K1 ≛[U] K2. #b #G1 #G2 #L2 #K2 #T #U #H @(fqup_ind … H) -G2 -K2 -U [ #G2 #K2 #U #HTU #L1 #HL12 elim (reqx_fqu_trans … HTU … HL12) -L2 /3 width=5 by fqu_fqup, ex3_2_intro/ @@ -114,13 +120,14 @@ lemma reqx_fqup_trans: ∀b,G1,G2,L2,K2,T,U. ❪G1,L2,T❫ ⬂+[b] ❪G2,K2,U❫ elim (reqx_fqu_trans … HU2 … HK0) -K #K1 #U1 #HU1 #HU12 #HK12 elim (teqx_fqu_trans … HU1 … HU0) -U #K3 #U3 #HU03 #HU31 #HK31 @(ex3_2_intro … K3 U3) (**) (* full auto too slow *) - /3 width=5 by reqx_trans, teqx_reqx_conf, fqup_strap1, teqx_trans/ + /3 width=5 by reqx_trans, teqx_reqx_conf_sn, fqup_strap1, teqx_trans/ ] qed-. -lemma teqx_fqup_trans: ∀b,G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂+[b] ❪G2,L2,T1❫ → - ∀U2. U2 ≛ U1 → - ∃∃L,T2. ❪G1,L1,U2❫ ⬂+[b] ❪G2,L,T2❫ & T2 ≛ T1 & L ≛[T1] L2. +lemma teqx_fqup_trans (b): + ∀G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂+[b] ❪G2,L2,T1❫ → + ∀U2. U2 ≛ U1 → + ∃∃L,T2. ❪G1,L1,U2❫ ⬂+[b] ❪G2,L,T2❫ & T2 ≛ T1 & L ≛[T1] L2. #b #G1 #G2 #L1 #L2 #U1 #T1 #H @(fqup_ind_dx … H) -G1 -L1 -U1 [ #G1 #L1 #U1 #H #U2 #HU21 elim (teqx_fqu_trans … H … HU21) -U1 /3 width=5 by fqu_fqup, ex3_2_intro/ @@ -129,16 +136,17 @@ lemma teqx_fqup_trans: ∀b,G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂+[b] ❪G2,L2,T lapply (teqx_reqx_div … HTU … HL0) -HL0 #HL0 elim (IH … HTU) -U #K2 #U1 #H2 #HUT1 #HKL2 elim (reqx_fqup_trans … H2 … HL0) -L #K #U #H2 #HU1 #HK2 - lapply (teqx_reqx_conf … HUT1 … HK2) -HK2 #HK2 + lapply (teqx_reqx_conf_sn … HUT1 … HK2) -HK2 #HK2 /3 width=7 by reqx_trans, fqup_strap2, teqx_trans, ex3_2_intro/ ] qed-. (* Properties with star-iterated structural successor for closures **********) -lemma teqx_fqus_trans: ∀b,G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂*[b] ❪G2,L2,T1❫ → - ∀U2. U2 ≛ U1 → - ∃∃L,T2. ❪G1,L1,U2❫ ⬂*[b] ❪G2,L,T2❫ & T2 ≛ T1 & L ≛[T1] L2. +lemma teqx_fqus_trans (b): + ∀G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂*[b] ❪G2,L2,T1❫ → + ∀U2. U2 ≛ U1 → + ∃∃L,T2. ❪G1,L1,U2❫ ⬂*[b] ❪G2,L,T2❫ & T2 ≛ T1 & L ≛[T1] L2. #b #G1 #G2 #L1 #L2 #U1 #T1 #H #U2 #HU21 elim(fqus_inv_fqup … H) -H [ #H elim (teqx_fqup_trans … H … HU21) -U1 /3 width=5 by fqup_fqus, ex3_2_intro/ | * #HG #HL #HT destruct /2 width=5 by ex3_2_intro/ @@ -146,9 +154,10 @@ lemma teqx_fqus_trans: ∀b,G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂*[b] ❪G2,L2,T qed-. (* Basic_2A1: was just: lleq_fqus_trans *) -lemma reqx_fqus_trans: ∀b,G1,G2,L2,K2,T,U. ❪G1,L2,T❫ ⬂*[b] ❪G2,K2,U❫ → - ∀L1. L1 ≛[T] L2 → - ∃∃K1,U0. ❪G1,L1,T❫ ⬂*[b] ❪G2,K1,U0❫ & U0 ≛ U & K1 ≛[U] K2. +lemma reqx_fqus_trans (b): + ∀G1,G2,L2,K2,T,U. ❪G1,L2,T❫ ⬂*[b] ❪G2,K2,U❫ → + ∀L1. L1 ≛[T] L2 → + ∃∃K1,U0. ❪G1,L1,T❫ ⬂*[b] ❪G2,K1,U0❫ & U0 ≛ U & K1 ≛[U] K2. #b #G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fqus_inv_fqup … H) -H [ #H elim (reqx_fqup_trans … H … HL12) -L2 /3 width=5 by fqup_fqus, ex3_2_intro/ | * #HG #HL #HT destruct /2 width=5 by ex3_2_intro/ diff --git a/matita/matita/contribs/lambdadelta/static_2/static/reqx_reqx.ma b/matita/matita/contribs/lambdadelta/static_2/static/reqx_reqx.ma index 3d4c8921c..c43edbdd1 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/reqx_reqx.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/reqx_reqx.ma @@ -20,7 +20,6 @@ include "static_2/static/reqx_length.ma". (* Advanced properties ******************************************************) -(* Basic_2A1: uses: lleq_sym *) lemma reqx_sym: ∀T. symmetric … (reqx T). /3 width=3 by reqx_fsge_comp, rex_sym, teqx_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/static/rex.ma b/matita/matita/contribs/lambdadelta/static_2/static/rex.ma index 4d10fb256..0eb1164eb 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/rex.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/rex.ma @@ -27,8 +27,9 @@ include "static_2/static/frees.ma". definition rex (R) (T): relation lenv ≝ λL1,L2. ∃∃f. L1 ⊢ 𝐅+❪T❫ ≘ f & L1 ⪤[cext2 R,cfull,f] L2. -interpretation "generic extension on referred entries (local environment)" - 'Relation R T L1 L2 = (rex R T L1 L2). +interpretation + "generic extension on referred entries (local environment)" + 'Relation R T L1 L2 = (rex R T L1 L2). definition R_confluent2_rex: relation4 (relation3 lenv term term) @@ -46,23 +47,29 @@ definition R_replace3_rex: ∀L1. L0 ⪤[RP1,T0] L1 → ∀L2. L0 ⪤[RP2,T0] L2 → ∀T. R2 L1 T1 T → R1 L2 T2 T. +definition R_transitive_rex: relation3 ? (relation3 ?? term) … ≝ + λR1,R2,R3. + ∀K1,K,V1. K1 ⪤[R1,V1] K → + ∀V. R1 K1 V1 V → ∀V2. R2 K V V2 → R3 K1 V1 V2. + +definition R_confluent1_rex: relation … ≝ + λR1,R2. + ∀K1,K2,V1. K1 ⪤[R2,V1] K2 → ∀V2. R1 K1 V1 V2 → R1 K2 V1 V2. + definition rex_confluent: relation … ≝ λR1,R2. ∀K1,K,V1. K1 ⪤[R1,V1] K → ∀V. R1 K1 V1 V → ∀K2. K ⪤[R2,V] K2 → K ⪤[R2,V1] K2. -definition rex_transitive: relation3 ? (relation3 ?? term) … ≝ - λR1,R2,R3. - ∀K1,K,V1. K1 ⪤[R1,V1] K → - ∀V. R1 K1 V1 V → ∀V2. R2 K V V2 → R3 K1 V1 V2. - (* Basic inversion lemmas ***************************************************) -lemma rex_inv_atom_sn (R): ∀Y2,T. ⋆ ⪤[R,T] Y2 → Y2 = ⋆. +lemma rex_inv_atom_sn (R): + ∀Y2,T. ⋆ ⪤[R,T] Y2 → Y2 = ⋆. #R #Y2 #T * /2 width=4 by sex_inv_atom1/ qed-. -lemma rex_inv_atom_dx (R): ∀Y1,T. Y1 ⪤[R,T] ⋆ → Y1 = ⋆. +lemma rex_inv_atom_dx (R): + ∀Y1,T. Y1 ⪤[R,T] ⋆ → Y1 = ⋆. #R #I #Y1 * /2 width=4 by sex_inv_atom2/ qed-. @@ -81,11 +88,9 @@ qed-. lemma rex_inv_zero (R): ∀Y1,Y2. Y1 ⪤[R,#0] Y2 → - ∨∨ Y1 = ⋆ ∧ Y2 = ⋆ - | ∃∃I,L1,L2,V1,V2. L1 ⪤[R,V1] L2 & R L1 V1 V2 & - Y1 = L1.ⓑ[I]V1 & Y2 = L2.ⓑ[I]V2 - | ∃∃f,I,L1,L2. 𝐈❪f❫ & L1 ⪤[cext2 R,cfull,f] L2 & - Y1 = L1.ⓤ[I] & Y2 = L2.ⓤ[I]. + ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆ + | ∃∃I,L1,L2,V1,V2. L1 ⪤[R,V1] L2 & R L1 V1 V2 & Y1 = L1.ⓑ[I]V1 & Y2 = L2.ⓑ[I]V2 + | ∃∃f,I,L1,L2. 𝐈❪f❫ & L1 ⪤[cext2 R,cfull,f] L2 & Y1 = L1.ⓤ[I] & Y2 = L2.ⓤ[I]. #R * [ | #Y1 * #I1 [ | #X ] ] #Y2 * #f #H1 #H2 [ lapply (sex_inv_atom1 … H2) -H2 /3 width=1 by or3_intro0, conj/ | elim (frees_inv_unit … H1) -H1 #g #HX #H destruct @@ -246,7 +251,8 @@ elim (rex_inv_zero_pair_sn … H) -H #Y #X #HK12 #_ #H destruct // qed-. (* Basic_2A1: uses: llpx_sn_fwd_pair_sn llpx_sn_fwd_bind_sn llpx_sn_fwd_flat_sn *) -lemma rex_fwd_pair_sn (R): ∀I,L1,L2,V,T. L1 ⪤[R,②[I]V.T] L2 → L1 ⪤[R,V] L2. +lemma rex_fwd_pair_sn (R): + ∀I,L1,L2,V,T. L1 ⪤[R,②[I]V.T] L2 → L1 ⪤[R,V] L2. #R * [ #p ] #I #L1 #L2 #V #T * #f #Hf #HL [ elim (frees_inv_bind … Hf) | elim (frees_inv_flat … Hf) ] -Hf /4 width=6 by sle_sex_trans, sor_inv_sle_sn, ex2_intro/ @@ -260,7 +266,8 @@ lemma rex_fwd_bind_dx (R): qed-. (* Basic_2A1: uses: llpx_sn_fwd_flat_dx *) -lemma rex_fwd_flat_dx (R): ∀I,L1,L2,V,T. L1 ⪤[R,ⓕ[I]V.T] L2 → L1 ⪤[R,T] L2. +lemma rex_fwd_flat_dx (R): + ∀I,L1,L2,V,T. L1 ⪤[R,ⓕ[I]V.T] L2 → L1 ⪤[R,T] L2. #R #I #L1 #L2 #V #T #H elim (rex_inv_flat … H) -H // qed-. @@ -274,7 +281,8 @@ qed-. (* Basic properties *********************************************************) -lemma rex_atom (R): ∀I. ⋆ ⪤[R,⓪[I]] ⋆. +lemma rex_atom (R): + ∀I. ⋆ ⪤[R,⓪[I]] ⋆. #R * /3 width=3 by frees_sort, frees_atom, frees_gref, sex_atom, ex2_intro/ qed. diff --git a/matita/matita/contribs/lambdadelta/static_2/static/rex_drops.ma b/matita/matita/contribs/lambdadelta/static_2/static/rex_drops.ma index 6cb74b4e5..dba0cb30b 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/rex_drops.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/rex_drops.ma @@ -19,25 +19,34 @@ include "static_2/static/rex.ma". (* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) -definition f_dedropable_sn: predicate (relation3 lenv term term) ≝ - λR. ∀b,f,L1,K1. ⇩*[b,f] L1 ≘ K1 → - ∀K2,T. K1 ⪤[R,T] K2 → ∀U. ⇧*[f] T ≘ U → - ∃∃L2. L1 ⪤[R,U] L2 & ⇩*[b,f] L2 ≘ K2 & L1 ≡[f] L2. - -definition f_dropable_sn: predicate (relation3 lenv term term) ≝ - λR. ∀b,f,L1,K1. ⇩*[b,f] L1 ≘ K1 → 𝐔❪f❫ → - ∀L2,U. L1 ⪤[R,U] L2 → ∀T. ⇧*[f] T ≘ U → - ∃∃K2. K1 ⪤[R,T] K2 & ⇩*[b,f] L2 ≘ K2. - -definition f_dropable_dx: predicate (relation3 lenv term term) ≝ - λR. ∀L1,L2,U. L1 ⪤[R,U] L2 → - ∀b,f,K2. ⇩*[b,f] L2 ≘ K2 → 𝐔❪f❫ → ∀T. ⇧*[f] T ≘ U → - ∃∃K1. ⇩*[b,f] L1 ≘ K1 & K1 ⪤[R,T] K2. - -definition f_transitive_next: relation3 … ≝ λR1,R2,R3. - ∀f,L,T. L ⊢ 𝐅+❪T❫ ≘ f → - ∀g,I,K,i. ⇩[i] L ≘ K.ⓘ[I] → ↑g = ⫱*[i] f → - sex_transitive (cext2 R1) (cext2 R2) (cext2 R3) (cext2 R1) cfull g K I. +definition f_dedropable_sn: + predicate (relation3 lenv term term) ≝ λR. + ∀b,f,L1,K1. ⇩*[b,f] L1 ≘ K1 → + ∀K2,T. K1 ⪤[R,T] K2 → ∀U. ⇧*[f] T ≘ U → + ∃∃L2. L1 ⪤[R,U] L2 & ⇩*[b,f] L2 ≘ K2 & L1 ≡[f] L2. + +definition f_dropable_sn: + predicate (relation3 lenv term term) ≝ λR. + ∀b,f,L1,K1. ⇩*[b,f] L1 ≘ K1 → 𝐔❪f❫ → + ∀L2,U. L1 ⪤[R,U] L2 → ∀T. ⇧*[f] T ≘ U → + ∃∃K2. K1 ⪤[R,T] K2 & ⇩*[b,f] L2 ≘ K2. + +definition f_dropable_dx: + predicate (relation3 lenv term term) ≝ λR. + ∀L1,L2,U. L1 ⪤[R,U] L2 → + ∀b,f,K2. ⇩*[b,f] L2 ≘ K2 → 𝐔❪f❫ → ∀T. ⇧*[f] T ≘ U → + ∃∃K1. ⇩*[b,f] L1 ≘ K1 & K1 ⪤[R,T] K2. + +definition f_transitive_next: + relation3 … ≝ λR1,R2,R3. + ∀f,L,T. L ⊢ 𝐅+❪T❫ ≘ f → + ∀g,I,K,i. ⇩[i] L ≘ K.ⓘ[I] → ↑g = ⫱*[i] f → + R_pw_transitive_sex (cext2 R1) (cext2 R2) (cext2 R3) (cext2 R1) cfull g K I. + +definition f_confluent1_next: relation2 … ≝ λR1,R2. + ∀f,L,T. L ⊢ 𝐅+❪T❫ ≘ f → + ∀g,I,K,i. ⇩[i] L ≘ K.ⓘ[I] → ↑g = ⫱*[i] f → + R_pw_confluent1_sex (cext2 R1) (cext2 R1) (cext2 R2) cfull g K I. (* Properties with generic slicing for local environments *******************) @@ -52,7 +61,7 @@ elim (sex_liftable_co_dedropable_sn … HLK1 … HK12 … Hf) -f1 -K1 qed-. lemma rex_trans_next (R1) (R2) (R3): - rex_transitive R1 R2 R3 → f_transitive_next R1 R2 R3. + R_transitive_rex R1 R2 R3 → f_transitive_next R1 R2 R3. #R1 #R2 #R3 #HR #f #L1 #T #Hf #g #I1 #K1 #n #HLK #Hgf #I #H generalize in match HLK; -HLK elim H -I1 -I [ #I #_ #L2 #_ #I2 #H @@ -65,11 +74,23 @@ generalize in match HLK; -HLK elim H -I1 -I ] qed. +lemma rex_conf1_next (R1) (R2): + R_confluent1_rex R1 R2 → f_confluent1_next R1 R2. +#R1 #R2 #HR #f #L1 #T #Hf #g #I1 #K1 #n #HLK #Hgf #I #H +generalize in match HLK; -HLK elim H -I1 -I +[ /2 width=1 by ext2_unit/ +| #I #V1 #V2 #HV12 #HLK1 #K2 #HK12 + elim (frees_inv_drops_next … Hf … HLK1 … Hgf) -f -HLK1 #f #Hf #Hfg + /5 width=5 by ext2_pair, sle_sex_trans, ex2_intro/ +] +qed. + (* Inversion lemmas with generic slicing for local environments *************) (* Basic_2A1: uses: llpx_sn_inv_lift_le llpx_sn_inv_lift_be llpx_sn_inv_lift_ge *) (* Basic_2A1: was: llpx_sn_drop_conf_O *) -lemma rex_dropable_sn (R): f_dropable_sn R. +lemma rex_dropable_sn (R): + f_dropable_sn R. #R #b #f #L1 #K1 #HLK1 #H1f #L2 #U * #f2 #Hf2 #HL12 #T #HTU elim (frees_total K1 T) #f1 #Hf1 lapply (frees_fwd_coafter … Hf2 … HLK1 … HTU … Hf1) -HTU #H2f @@ -79,7 +100,8 @@ qed-. (* Basic_2A1: was: llpx_sn_drop_trans_O *) (* Note: the proof might be simplified *) -lemma rex_dropable_dx (R): f_dropable_dx R. +lemma rex_dropable_dx (R): + f_dropable_dx R. #R #L1 #L2 #U * #f2 #Hf2 #HL12 #b #f #K2 #HLK2 #H1f #T #HTU elim (drops_isuni_ex … H1f L1) #K1 #HLK1 elim (frees_total K1 T) #f1 #Hf1 diff --git a/matita/matita/contribs/lambdadelta/static_2/static/rex_fsle.ma b/matita/matita/contribs/lambdadelta/static_2/static/rex_fsle.ma index ff6588270..e3914f23a 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/rex_fsle.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/rex_fsle.ma @@ -85,7 +85,7 @@ lemma rex_pair_sn_split (R1) (R2): lapply(frees_mono … H … Hf) -H #H1 lapply (sor_eq_repl_back1 … Hy … H1) -y1 #Hy lapply (sor_inv_sle_sn … Hy) -y2 #Hfg -elim (sex_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #L #HL1 #HL2 +elim (sex_sle_split_sn (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #L #HL1 #HL2 lapply (sle_sex_trans … HL1 … Hfg) // #H elim (frees_sex_conf_fsge … Hf … H) -Hf -H /4 width=7 by sle_sex_trans, ex2_intro/ @@ -102,7 +102,7 @@ elim (frees_inv_flat … Hg) #y1 #y2 #_ #H #Hy lapply(frees_mono … H … Hf) -H #H2 lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy lapply (sor_inv_sle_dx … Hy) -y1 #Hfg -elim (sex_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #L #HL1 #HL2 +elim (sex_sle_split_sn (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #L #HL1 #HL2 lapply (sle_sex_trans … HL1 … Hfg) // #H elim (frees_sex_conf_fsge … Hf … H) -Hf -H /4 width=7 by sle_sex_trans, ex2_intro/ @@ -121,7 +121,7 @@ lapply (tl_eq_repl … H2) -H2 #H2 lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy lapply (sor_inv_sle_dx … Hy) -y1 #Hfg lapply (sle_inv_tl_sn … Hfg) -Hfg #Hfg -elim (sex_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #Y #H #HL2 +elim (sex_sle_split_sn (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #Y #H #HL2 lapply (sle_sex_trans … H … Hfg) // #H0 elim (sex_inv_next1 … H) -H #Z #L #HL1 #H elim (ext2_inv_pair_sn … H) -H #V #HV #H1 #H2 destruct @@ -142,7 +142,7 @@ lapply (tl_eq_repl … H2) -H2 #H2 lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy lapply (sor_inv_sle_dx … Hy) -y1 #Hfg lapply (sle_inv_tl_sn … Hfg) -Hfg #Hfg -elim (sex_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #Y #H #HL2 +elim (sex_sle_split_sn (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #Y #H #HL2 lapply (sle_sex_trans … H … Hfg) // #H0 elim (sex_inv_next1 … H) -H #Z #L #HL1 #H elim (ext2_inv_unit_sn … H) -H #H destruct diff --git a/matita/matita/contribs/lambdadelta/static_2/static/rex_lex.ma b/matita/matita/contribs/lambdadelta/static_2/static/rex_lex.ma index 9329d7f84..c40731941 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/rex_lex.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/rex_lex.ma @@ -29,12 +29,28 @@ qed. (* Inversion lemmas with generic extension of a context sensitive relation **) -lemma rex_inv_lex_req (R): +lemma rex_inv_req_lex (R): + c_reflexive … R → f_confluent1_next R ceq → + ∀L1,L2,T. L1 ⪤[R,T] L2 → + ∃∃L. L1 ≡[T] L & L ⪤[R] L2. +#R #H1R #H2R #L1 #L2 #T * #f1 #Hf1 #HL +elim (sex_sdj_split_dx … ceq_ext … HL 𝐈𝐝) -HL +[ #L0 #HL10 #HL02 + lapply (sex_sdj … HL02 f1 ?) /2 width=1 by sdj_isid_sn/ #H + /3 width=5 by (* 2x *) ex2_intro/ +|*: /2 width=1 by ext2_refl, sdj_isid_dx/ + #g #I #K #n #HLK #Hg @H2R /width=7 by/ (**) (* no auto with H2R *) +] +qed-. + +(* Forward lemmas with generic extension of a context sensitive relation **) + +lemma rex_fwd_lex_req (R): c_reflexive … R → rex_fsge_compatible R → ∀L1,L2,T. L1 ⪤[R,T] L2 → ∃∃L. L1 ⪤[R] L & L ≡[T] L2. #R #H1R #H2R #L1 #L2 #T * #f1 #Hf1 #HL -elim (sex_sdj_split … ceq_ext … HL 𝐈𝐝 ?) -HL +elim (sex_sdj_split_sn … ceq_ext … HL 𝐈𝐝 ?) -HL [ #L0 #HL10 #HL02 |*: /2 width=1 by ext2_refl, sdj_isid_dx/ ] -H1R lapply (sex_sdj … HL10 f1 ?) /2 width=1 by sdj_isid_sn/ #H elim (frees_sex_conf_fsge … Hf1 … H) // -H2R -H #f0 #Hf0 #Hf01 diff --git a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl index bce1a4376..31f151da1 100644 --- a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl @@ -36,7 +36,7 @@ table { } ] [ { "syntactic equivalence" * } { - [ [ "for lenvs on referred entries" ] "req" + "( ? ≡[?] ? )" "req_drops" + "req_fqup" + "req_fsle" * ] + [ [ "for lenvs on referred entries" ] "req" + "( ? ≡[?] ? )" "req_length" + "req_drops" + "req_fqup" + "req_fsle" * ] } ] [ { "generic extension of a context-sensitive relation" * } {