From f82a900182012664dd58eb1d8ab012c2a6f541ab Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 16 Jan 2017 11:24:12 +0000 Subject: [PATCH] advances towards confluence of reduction in local environments ... --- .../basic_2/relocation/lexs_lexs.ma | 2 - .../basic_2/relocation/lreq_lreq.ma | 1 - .../basic_2/rt_transition/lfpr_lfpr.ma | 2 +- .../basic_2/rt_transition/lfpr_main.ma | 21 +++ .../basic_2/rt_transition/lfpx_frees.ma | 39 +++-- .../lambdadelta/basic_2/static/lfeq_lfeq.ma | 1 - .../lambdadelta/basic_2/static/lfxs.ma | 11 ++ .../lambdadelta/basic_2/static/lfxs_lfxs.ma | 23 +++ .../lambdadelta/basic_2/static/lfxs_main.ma | 50 ------ .../lambdadelta/basic_2/static/lsubf.ma | 153 ++++++------------ .../lambdadelta/basic_2/static/lsubf_frees.ma | 50 +++--- .../lambdadelta/basic_2/static/lsubr.ma | 43 ++--- .../lambdadelta/basic_2/web/basic_2_src.tbl | 12 +- .../ground_2/relocation/rtmap_sle.ma | 11 ++ .../ground_2/relocation/rtmap_sor.ma | 2 + 15 files changed, 205 insertions(+), 216 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_main.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/lfxs_main.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma index cd7e64c51..c0d7c6a12 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma @@ -13,8 +13,6 @@ (**************************************************************************) include "ground_2/relocation/rtmap_sand.ma". -include "ground_2/relocation/rtmap_sor.ma". -include "basic_2/relocation/lexs.ma". include "basic_2/relocation/drops.ma". (* GENERIC ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_lreq.ma index c823270ec..42aaf3eea 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_lreq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_lreq.ma @@ -13,7 +13,6 @@ (**************************************************************************) include "basic_2/relocation/lexs_lexs.ma". -include "basic_2/relocation/lreq.ma". (* RANGED EQUIVALENCE FOR LOCAL ENVIRONMENTS ********************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma index a78a84a89..80310acaf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma @@ -298,7 +298,7 @@ lapply (lifts_mono … HX … HVU) -HX #H destruct /4 width=7 by cpm_bind, cpr_flat, ex2_intro/ (**) (* full auto not tried *) qed-. -theorem cpr_conf_lfpr: ∀h,G. R_confluent_lfxs (cpm 0 h G) (cpm 0 h G) (cpm 0 h G) (cpm 0 h G). +theorem cpr_conf_lfpr: ∀h,G. R_confluent2_lfxs (cpm 0 h G) (cpm 0 h G) (cpm 0 h G) (cpm 0 h G). #h #G #L0 #T0 @(fqup_wf_ind_eq … G L0 T0) -G -L0 -T0 #G #L #T #IH #G0 #L0 * [| * ] [ #I0 #HG #HL #HT #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct elim (cpr_inv_atom1_drops … H1) -H1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_main.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_main.ma new file mode 100644 index 000000000..de8e8a719 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_main.ma @@ -0,0 +1,21 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lfxs_lfxs.ma". +include "basic_2/rt_transition/lfpr_lfpr.ma". + +theorem lfpr_conf: ∀h,G,T. confluent … (lfpr h G T). +#h #G @lfxs_conf [ | @cpr_conf_lfpr ] +qed-. + diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_frees.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_frees.ma index 935109f90..7e184e1a4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_frees.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_frees.ma @@ -15,6 +15,8 @@ include "basic_2/relocation/drops_lexs.ma". include "basic_2/s_computation/fqup_weight.ma". include "basic_2/static/frees_drops.ma". +include "basic_2/static/lsubf_frees.ma". +include "basic_2/static/lfxs.ma". include "basic_2/rt_transition/cpx_drops.ma". (* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****) @@ -40,10 +42,10 @@ axiom frees_pair_flat: ∀L,T,f1,I1,V1. L.ⓑ{I1}V1 ⊢ 𝐅*⦃T⦄ ≡ f1 → ∀I0,I. L.ⓑ{I0}ⓕ{I}V1.V2 ⊢ 𝐅*⦃T⦄ ≡ f0. (* Basic_2A1: was: lpx_cpx_frees_trans *) -lemma cpx_frees_trans_lexs: ∀h,G,L1,T1,f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 → - ∀L2. L1 ⦻*[cpx h G, cfull, f1] L2 → - ∀T2. ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 → - ∃∃f2. L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 & f2 ⊆ f1. +lemma cpx_frees_conf_lfpx: ∀h,G,L1,T1,f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 → + ∀L2. L1 ⦻*[cpx h G, cfull, f1] L2 → + ∀T2. ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 → + ∃∃f2. L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 & f2 ⊆ f1. #h #G #L1 #T1 @(fqup_wf_ind_eq … G L1 T1) -G -L1 -T1 #G0 #L0 #U0 #IH #G #L1 * * [ -IH #s #HG #HL #HU #g1 #H1 #L2 #_ #U2 #H0 destruct @@ -121,13 +123,26 @@ lemma cpx_frees_trans_lexs: ∀h,G,L1,T1,f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 → lapply (sle_lexs_trans … H2 gW1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12W lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T lapply (lexs_inv_tl … Abst … HL12T … HW12 ?) // -HL12T #HL12T + elim (sor_isfin_ex gV1 gW1) /2 width=3 by frees_fwd_isfin/ #g0 #Hg0 #_ + lapply (sor_trans2 … Hg1 … HgT0 … Hg0) -Hg1 -HgT0 #Hg1 + lapply (sor_sym … Hg0) -Hg0 #Hg0 elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21 elim (IH … HgW1 … HL12W … HW12) // -HgW1 -HL12W -HW12 #gW2 #HgW2 #HgW21 elim (IH … HgT1 … HL12T … HT12) // -IH -HgT1 -HL12T -HT12 #gT2 #HgT2 #HgT21 + elim (sor_isfin_ex gV2 (⫱gT2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #gVT2 #HgVT2 #_ + elim (lsubf_frees_trans … HgT2 (⫯gVT2) … (L2.ⓓⓝW2.V2)) + [2: /4 width=3 by lsubf_refl, lsubf_beta, sor_inv_sle_dx, sle_inv_tl_sn/ ] -HgT2 + #gT0 #HgT0 #HgT20 elim (sor_isfin_ex gW2 gV2) /2 width=3 by frees_fwd_isfin/ #gV0 #HgV0 #H - elim (sor_isfin_ex gV0 (⫱gT2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ -H #g2 #Hg2 #_ + elim (sor_isfin_ex gV0 (⫱gT0)) /3 width=3 by frees_fwd_isfin, isfin_tl/ -H #g2 #Hg2 #_ @(ex2_intro … g2) - [ @(frees_bind … Hg2) /2 width=5 by frees_flat/ ] + [ @(frees_bind … Hg2) /2 width=5 by frees_flat/ + | -L2 @(sor_inv_sle … Hg2) -Hg2 + [ /3 width=11 by sor_inv_sle_sn_trans, monotonic_sle_sor/ + | @sle_xn_tl [2:|*: // ] @(sle_trans … HgT20) -HgT20 + /4 width=8 by monotonic_sle_sor, sor_inv_sle_dx_trans, sle_tl, sle_next/ + ] (**) (* full auto too slow *) + ] | #p #V2 #V #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #H0 #H1 #H destruct elim (frees_inv_bind … HgT0) -HgT0 #gW1 #gT1 #HgW1 #HgT1 #HgT0 lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V @@ -149,10 +164,12 @@ lemma cpx_frees_trans_lexs: ∀h,G,L1,T1,f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 → /4 width=10 by frees_flat, frees_bind, monotonic_sle_sor, sle_tl, ex2_intro/ ] ] +qed-. -lemma cpx_frees_trans: ∀h,o,G. frees_trans (cpx h o G). -/2 width=8 by lpx_cpx_frees_trans/ qed-. +(* Basic_2A1: was: cpx_frees_trans *) +lemma cpx_frees_conf: ∀h,G. R_frees_confluent (cpx h G). +/3 width=7 by cpx_frees_conf_lfpx, lexs_refl/ qed-. -lemma lpx_frees_trans: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, o] L2 → - ∀U,i. L2 ⊢ i ϵ 𝐅*[0]⦃U⦄ → L1 ⊢ i ϵ 𝐅*[0]⦃U⦄. -/2 width=8 by lpx_cpx_frees_trans/ qed-. +(* Basic_2A1: was: lpx_frees_trans *) +lemma lfpx_frees_conf: ∀h,G. lexs_frees_confluent (cpx h G) cfull. +/2 width=7 by cpx_frees_conf_lfpx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lfeq.ma index 602c58685..677f53973 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lfeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lfeq.ma @@ -13,7 +13,6 @@ (**************************************************************************) include "basic_2/relocation/lreq_lreq.ma". -include "basic_2/static/frees_frees.ma". include "basic_2/static/lfxs_lfxs.ma". include "basic_2/static/lfeq_lreq.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma index 605af05ce..2064f1217 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma @@ -26,6 +26,17 @@ definition lfxs (R) (T): relation lenv ≝ interpretation "generic extension on referred entries (local environment)" 'RelationStar R T L1 L2 = (lfxs R T L1 L2). +definition R_frees_confluent: predicate (relation3 lenv term term) ≝ + λRN. + ∀f1,L,T1. L ⊢ 𝐅*⦃T1⦄ ≡ f1 → ∀T2. RN L T1 T2 → + ∃∃f2. L ⊢ 𝐅*⦃T2⦄ ≡ f2 & f2 ⊆ f1. + +definition lexs_frees_confluent: relation (relation3 lenv term term) ≝ + λRN,RP. + ∀f1,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f1 → + ∀L2. L1 ⦻*[RN, RP, f1] L2 → + ∃∃f2. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 & f2 ⊆ f1. + definition R_confluent2_lfxs: relation4 (relation3 lenv term term) (relation3 lenv term term) … ≝ λR1,R2,RP1,RP2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma index 5360aeddc..26289760b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma @@ -13,6 +13,8 @@ (**************************************************************************) include "basic_2/relocation/lexs_lexs.ma". +include "basic_2/static/frees_fqup.ma". +include "basic_2/static/frees_frees.ma". include "basic_2/static/lfxs.ma". (* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) @@ -33,3 +35,24 @@ theorem lfxs_flat: ∀R,I,L1,L2,V,T. #R #I #L1 #L2 #V #T * #f1 #HV #Hf1 * #f2 #HT #Hf2 elim (sor_isfin_ex f1 f2) /3 width=7 by frees_fwd_isfin, frees_flat, lexs_join, ex2_intro/ qed. + +theorem lfxs_conf: ∀R. lexs_frees_confluent R cfull → + R_confluent2_lfxs R R R R → + ∀T. confluent … (lfxs R T). +#R #H1R #H2R #T #L0 #L1 * #f1 #Hf1 #HL01 #L2 * #f #Hf #HL02 +lapply (frees_mono … Hf1 … Hf) -Hf1 #Hf12 +lapply (lexs_eq_repl_back … HL01 … Hf12) -f1 #HL01 +elim (lexs_conf … HL01 … HL02) /2 width=3 by ex2_intro/ [ | -HL01 -HL02 ] +[ #L #HL1 #HL2 + elim (H1R … Hf … HL01) -HL01 #f1 #Hf1 #H1 + elim (H1R … Hf … HL02) -HL02 #f2 #Hf2 #H2 + lapply (sle_lexs_trans … HL1 … H1) // -HL1 -H1 #HL1 + lapply (sle_lexs_trans … HL2 … H2) // -HL2 -H2 #HL2 + /3 width=5 by ex2_intro/ +| #g #I #K0 #V0 #n #HLK0 #Hgf #V1 #HV01 #V2 #HV02 #K1 #HK01 #K2 #HK02 + elim (frees_drops_next … Hf … HLK0 … Hgf) -Hf -HLK0 -Hgf #g0 #Hg0 #H0 + lapply (sle_lexs_trans … HK01 … H0) // -HK01 #HK01 + lapply (sle_lexs_trans … HK02 … H0) // -HK02 #HK02 + elim (H2R … HV01 … HV02 K1 … K2) /2 width=3 by ex2_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_main.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_main.ma deleted file mode 100644 index 444d413ef..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_main.ma +++ /dev/null @@ -1,50 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/static/lfxs_lfxs.ma". -include "basic_2/static/frees_fqup.ma". -include "basic_2/static/frees_frees.ma". - -(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) - -axiom frees_lexs_conf_sle: ∀RN,RP,f1,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f1 → - ∀L2. L1 ⦻*[RN, RP, f1] L2 → - ∃∃f2. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 & f2 ⊆ f1. - -theorem lfxs_conf: ∀R. R_confluent2_lfxs R R R R → - ∀T. confluent … (lfxs R T). -#R #H1R #T #L0 #L1 * #f1 #Hf1 #HL01 #L2 * #f #Hf #HL02 -lapply (frees_mono … Hf1 … Hf) -Hf1 #Hf12 -lapply (lexs_eq_repl_back … HL01 … Hf12) -f1 #HL01 -elim (lexs_conf … HL01 … HL02) /2 width=3 by ex2_intro/ [ | -HL01 -HL02 ] -[ #L #HL1 #HL2 - elim (frees_lexs_conf_sle … Hf … HL01) -HL01 #f1 #Hf1 #H1 - elim (frees_lexs_conf_sle … Hf … HL02) -HL02 #f2 #Hf2 #H2 - lapply (sle_lexs_trans … HL1 … H1) // -HL1 -H1 #HL1 - lapply (sle_lexs_trans … HL2 … H2) // -HL2 -H2 #HL2 - /3 width=5 by ex2_intro/ -| #g #I #K0 #V0 #n #HLK0 #Hgf #V1 #HV01 #V2 #HV02 #K1 #HK01 #K2 #HK02 - elim (frees_drops_next … Hf … HLK0 … Hgf) -Hf -HLK0 -Hgf #g0 #Hg0 #H0 - lapply (sle_lexs_trans … HK01 … H0) // -HK01 #HK01 - lapply (sle_lexs_trans … HK02 … H0) // -HK02 #HK02 - elim (H1R … HV01 … HV02 K1 … K2) /2 width=3 by ex2_intro/ -] -qed-. - -(* -lemma pippo: ∀R1,R2,RP1,RP2. R_confluent_lfxs R1 R2 RP1 RP2 → - lexs_confluent R1 R2 RP1 cfull RP2 cfull. -#R1 #R2 #RP1 #RP2 #HR #f #L0 #T0 #T1 #HT01 #T2 #HT02 #L1 #HL01 #L2 -#HL02 -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma index d5ad21f9d..3e6e63b07 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma @@ -18,15 +18,11 @@ include "basic_2/static/frees.ma". (* RESTRICTED REFINEMENT FOR CONTEXT-SENSITIVE FREE VARIABLES ***************) inductive lsubf: relation4 lenv rtmap lenv rtmap ≝ -| lsubf_atom: ∀f. lsubf (⋆) f (⋆) f -| lsubf_push: ∀f1,f2,I,L1,L2,V. lsubf L1 f1 L2 f2 → - lsubf (L1.ⓑ{I}V) (↑f1) (L2.ⓑ{I}V) (↑f2) -| lsubf_next: ∀f1,f2,I,L1,L2,V. lsubf L1 f1 L2 f2 → - lsubf (L1.ⓑ{I}V) (⫯f1) (L2.ⓑ{I}V) (⫯f2) -| lsubf_peta: ∀f1,f,f2,L1,L2,W,V. L1 ⊢ 𝐅*⦃V⦄ ≡ f → f2 ⋓ f ≡ f1 → - lsubf L1 f1 L2 f2 → lsubf (L1.ⓓⓝW.V) (↑f1) (L2.ⓛW) (↑f2) -| lsubf_neta: ∀f1,f,f2,L1,L2,W,V. L1 ⊢ 𝐅*⦃V⦄ ≡ f → f2 ⋓ f ≡ f1 → - lsubf L1 f1 L2 f2 → lsubf (L1.ⓓⓝW.V) (⫯f1) (L2.ⓛW) (⫯f2) +| lsubf_atom: ∀f1,f2. f2 ⊆ f1 → lsubf (⋆) f1 (⋆) f2 +| lsubf_pair: ∀f1,f2,I,L1,L2,V. lsubf L1 (⫱f1) L2 (⫱f2) → f2 ⊆ f1 → + lsubf (L1.ⓑ{I}V) f1 (L2.ⓑ{I}V) f2 +| lsubf_beta: ∀f,f1,f2,L1,L2,W,V. L1 ⊢ 𝐅*⦃V⦄ ≡ f → f ⋓ ⫱f2 ≡ ⫱f1 → f2 ⊆ f1 → + lsubf L1 (⫱f1) L2 (⫱f2) → lsubf (L1.ⓓⓝW.V) f1 (L2.ⓛW) f2 . interpretation @@ -36,126 +32,77 @@ interpretation (* Basic inversion lemmas ***************************************************) fact lsubf_inv_atom1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → L1 = ⋆ → - L2 = ⋆ ∧ f1 = f2. + L2 = ⋆ ∧ f2 ⊆ f1. #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2 [ /2 width=1 by conj/ -| #f1 #f2 #I #L1 #L2 #V #_ #H destruct -| #f1 #f2 #I #L1 #L2 #V #_ #H destruct -| #f1 #f #f2 #L1 #L2 #W #V #_ #_ #_ #H destruct -| #f1 #f #f2 #L1 #L2 #W #V #_ #_ #_ #H destruct +| #f1 #f2 #I #L1 #L2 #V #_ #_ #H destruct +| #f #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #_ #H destruct ] qed-. -lemma lsubf_inv_atom1: ∀f1,f2,L2. ⦃⋆, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → - L2 = ⋆ ∧ f1 = f2. +lemma lsubf_inv_atom1: ∀f1,f2,L2. ⦃⋆, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → L2 = ⋆ ∧ f2 ⊆ f1. /2 width=3 by lsubf_inv_atom1_aux/ qed-. -fact lsubf_inv_push1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → - ∀g1,I,K1,X. f1 = ↑g1 → L1 = K1.ⓑ{I}X → - (∃∃g2,K2. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f2 = ↑g2 & L2 = K2.ⓑ{I}X) ∨ - ∃∃g,g2,K2,W,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 & - ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abbr & f2 = ↑g2 & L2 = K2.ⓛW & X = ⓝW.V. +fact lsubf_inv_pair1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → + ∀I,K1,X. L1 = K1.ⓑ{I}X → + (∃∃K2. f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & L2 = K2.ⓑ{I}X) ∨ + ∃∃f,K2,W,V. K1 ⊢ 𝐅*⦃V⦄ ≡ f & f ⋓ ⫱f2 ≡ ⫱f1 & + f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & I = Abbr & L2 = K2.ⓛW & X = ⓝW.V. #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2 -[ #f #g1 #J #K1 #X #_ #H destruct -| #f1 #f2 #I #L1 #L2 #V #HL12 #g1 #J #K1 #X #H1 #H2 destruct - /3 width=5 by injective_push, ex3_2_intro, or_introl/ -| #f1 #f2 #I #L1 #L2 #V #_ #g1 #J #K1 #X #H elim (discr_next_push … H) -| #f1 #f2 #f #L1 #L2 #W #V #Hf2 #Hf1 #HL12 #g1 #J #K1 #X #H1 #H2 destruct - /3 width=11 by injective_push, ex7_5_intro, or_intror/ -| #f1 #f2 #f #L1 #L2 #W #V #_ #_ #_ #g1 #J #K1 #X #H elim (discr_next_push … H) +[ #f1 #f2 #_ #J #K1 #X #H destruct +| #f1 #f2 #I #L1 #L2 #V #HL12 #H21 #J #K1 #X #H destruct + /3 width=3 by ex3_intro, or_introl/ +| #f #f1 #f2 #L1 #L2 #W #V #Hf #Hf1 #H21 #HL12 #J #K1 #X #H destruct + /3 width=11 by ex7_4_intro, or_intror/ ] qed-. -lemma lsubf_inv_push1: ∀g1,f2,I,K1,L2,X. ⦃K1.ⓑ{I}X, ↑g1⦄ ⫃𝐅* ⦃L2, f2⦄ → - (∃∃g2,K2. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f2 = ↑g2 & L2 = K2.ⓑ{I}X) ∨ - ∃∃g,g2,K2,W,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 & - ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abbr & f2 = ↑g2 & L2 = K2.ⓛW & X = ⓝW.V. -/2 width=5 by lsubf_inv_push1_aux/ qed-. - -fact lsubf_inv_next1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → - ∀g1,I,K1,X. f1 = ⫯g1 → L1 = K1.ⓑ{I}X → - (∃∃g2,K2. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f2 = ⫯g2 & L2 = K2.ⓑ{I}X) ∨ - ∃∃g,g2,K2,W,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 & - ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abbr & f2 = ⫯g2 & L2 = K2.ⓛW & X = ⓝW.V. -#f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2 -[ #f #g1 #J #K1 #X #_ #H destruct -| #f1 #f2 #I #L1 #L2 #V #_ #g1 #J #K1 #X #H elim (discr_push_next … H) -| #f1 #f2 #I #L1 #L2 #V #HL12 #g1 #J #K1 #X #H1 #H2 destruct - /3 width=5 by injective_next, ex3_2_intro, or_introl/ -| #f1 #f2 #f #L1 #L2 #W #V #_ #_ #_ #g1 #J #K1 #X #H elim (discr_push_next … H) -| #f1 #f2 #f #L1 #L2 #W #V #Hf2 #Hf1 #HL12 #g1 #J #K1 #X #H1 #H2 destruct - /3 width=11 by injective_next, ex7_5_intro, or_intror/ -] -qed-. - -lemma lsubf_inv_next1: ∀g1,f2,I,K1,L2,X. ⦃K1.ⓑ{I}X, ⫯g1⦄ ⫃𝐅* ⦃L2, f2⦄ → - (∃∃g2,K2. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f2 = ⫯g2 & L2 = K2.ⓑ{I}X) ∨ - ∃∃g,g2,K2,W,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 & - ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abbr & f2 = ⫯g2 & L2 = K2.ⓛW & X = ⓝW.V. -/2 width=5 by lsubf_inv_next1_aux/ qed-. +lemma lsubf_inv_pair1: ∀f1,f2,I,K1,L2,X. ⦃K1.ⓑ{I}X, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → + (∃∃K2. f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & L2 = K2.ⓑ{I}X) ∨ + ∃∃f,K2,W,V. K1 ⊢ 𝐅*⦃V⦄ ≡ f & f ⋓ ⫱f2 ≡ ⫱f1 & + f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & I = Abbr & L2 = K2.ⓛW & X = ⓝW.V. +/2 width=3 by lsubf_inv_pair1_aux/ qed-. fact lsubf_inv_atom2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → L2 = ⋆ → - L1 = ⋆ ∧ f1 = f2. + L1 = ⋆ ∧ f2 ⊆ f1. #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2 [ /2 width=1 by conj/ -| #f1 #f2 #I #L1 #L2 #V #_ #H destruct -| #f1 #f2 #I #L1 #L2 #V #_ #H destruct -| #f1 #f #f2 #L1 #L2 #W #V #_ #_ #_ #H destruct -| #f1 #f #f2 #L1 #L2 #W #V #_ #_ #_ #H destruct +| #f1 #f2 #I #L1 #L2 #V #_ #_ #H destruct +| #f #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #_ #H destruct ] qed-. -lemma lsubf_inv_atom2: ∀f1,f2,L1. ⦃L1, f1⦄ ⫃𝐅* ⦃⋆, f2⦄ → - L1 = ⋆ ∧ f1 = f2. +lemma lsubf_inv_atom2: ∀f1,f2,L1. ⦃L1, f1⦄ ⫃𝐅* ⦃⋆, f2⦄ → L1 = ⋆ ∧ f2 ⊆ f1. /2 width=3 by lsubf_inv_atom2_aux/ qed-. -fact lsubf_inv_push2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → - ∀g2,I,K2,W. f2 = ↑g2 → L2 = K2.ⓑ{I}W → - (∃∃g1,K1. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f1 = ↑g1 & L1 = K1.ⓑ{I}W) ∨ - ∃∃g,g1,K1,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 & - ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abst & f1 = ↑g1 & L1 = K1.ⓓⓝW.V. +fact lsubf_inv_pair2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → + ∀I,K2,W. L2 = K2.ⓑ{I}W → + (∃∃K1.f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & L1 = K1.ⓑ{I}W) ∨ + ∃∃f,K1,V. K1 ⊢ 𝐅*⦃V⦄ ≡ f & f ⋓ ⫱f2 ≡ ⫱f1 & + f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & I = Abst & L1 = K1.ⓓⓝW.V. #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2 -[ #f #g2 #J #K2 #X #_ #H destruct -| #f1 #f2 #I #L1 #L2 #V #HL12 #g2 #J #K2 #X #H1 #H2 destruct - /3 width=5 by injective_push, ex3_2_intro, or_introl/ -| #f1 #f2 #I #L1 #L2 #V #_ #g2 #J #K2 #X #H elim (discr_next_push … H) -| #f1 #f2 #f #L1 #L2 #W #V #Hf2 #Hf1 #HL12 #g2 #J #K2 #X #H1 #H2 destruct - /3 width=9 by injective_push, ex6_4_intro, or_intror/ -| #f1 #f2 #f #L1 #L2 #W #V #_ #_ #_ #g2 #J #K2 #X #H elim (discr_next_push … H) +[ #f1 #f2 #_ #J #K2 #X #H destruct +| #f1 #f2 #I #L1 #L2 #V #HL12 #H21 #J #K2 #X #H destruct + /3 width=3 by ex3_intro, or_introl/ +| #f #f1 #f2 #L1 #L2 #W #V #Hf #Hf1 #H21 #HL12 #J #K2 #X #H destruct + /3 width=7 by ex6_3_intro, or_intror/ ] qed-. -lemma lsubf_inv_push2: ∀f1,g2,I,L1,K2,W. ⦃L1, f1⦄ ⫃𝐅* ⦃K2.ⓑ{I}W, ↑g2⦄ → - (∃∃g1,K1. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f1 = ↑g1 & L1 = K1.ⓑ{I}W) ∨ - ∃∃g,g1,K1,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 & - ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abst & f1 = ↑g1 & L1 = K1.ⓓⓝW.V. -/2 width=5 by lsubf_inv_push2_aux/ qed-. - -fact lsubf_inv_next2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → - ∀g2,I,K2,W. f2 = ⫯g2 → L2 = K2.ⓑ{I}W → - (∃∃g1,K1. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f1 = ⫯g1 & L1 = K1.ⓑ{I}W) ∨ - ∃∃g,g1,K1,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 & - ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abst & f1 = ⫯g1 & L1 = K1.ⓓⓝW.V. -#f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2 -[ #f #g2 #J #K2 #X #_ #H destruct -| #f1 #f2 #I #L1 #L2 #V #_ #g2 #J #K2 #X #H elim (discr_push_next … H) -| #f1 #f2 #I #L1 #L2 #V #HL12 #g2 #J #K2 #X #H1 #H2 destruct - /3 width=5 by injective_next, ex3_2_intro, or_introl/ -| #f1 #f2 #f #L1 #L2 #W #V #_ #_ #_ #g2 #J #K2 #X #H elim (discr_push_next … H) -| #f1 #f2 #f #L1 #L2 #W #V #Hf2 #Hf1 #HL12 #g2 #J #K2 #X #H1 #H2 destruct - /3 width=9 by injective_next, ex6_4_intro, or_intror/ -] -qed-. +lemma lsubf_inv_pair2: ∀f1,f2,I,L1,K2,W. ⦃L1, f1⦄ ⫃𝐅* ⦃K2.ⓑ{I}W, f2⦄ → + (∃∃K1.f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & L1 = K1.ⓑ{I}W) ∨ + ∃∃f,K1,V. K1 ⊢ 𝐅*⦃V⦄ ≡ f & f ⋓ ⫱f2 ≡ ⫱f1 & + f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & I = Abst & L1 = K1.ⓓⓝW.V. +/2 width=5 by lsubf_inv_pair2_aux/ qed-. -lemma lsubf_inv_next2: ∀f1,g2,I,L1,K2,W. ⦃L1, f1⦄ ⫃𝐅* ⦃K2.ⓑ{I}W, ⫯g2⦄ → - (∃∃g1,K1. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f1 = ⫯g1 & L1 = K1.ⓑ{I}W) ∨ - ∃∃g,g1,K1,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 & - ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abst & f1 = ⫯g1 & L1 = K1.ⓓⓝW.V. -/2 width=5 by lsubf_inv_next2_aux/ qed-. +(* Basic forward lemmas *****************************************************) + +lemma lsubf_fwd_sle: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → f2 ⊆ f1. +#f1 #f2 #L1 #L2 * // +qed-. (* Basic properties *********************************************************) -lemma lsubf_refl: bi_reflexive … lsubf. -#L elim L -L // -#L #I #V #IH #f elim (pn_split f) * /2 width=1 by lsubf_push, lsubf_next/ +lemma lsubf_refl: ∀L,f1,f2. f2 ⊆ f1 → ⦃L, f1⦄ ⫃𝐅* ⦃L, f2⦄. +#L elim L -L /4 width=1 by lsubf_atom, lsubf_pair, sle_tl/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma index 65de4cfae..47fc2f75e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma @@ -18,34 +18,34 @@ include "basic_2/static/lsubf.ma". (* Properties with context-sensitive free variables *************************) -lemma lsubf_free_trans: ∀f2,L2,T. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 → ∀f,L1. ⦃L1, f⦄ ⫃𝐅* ⦃L2, f2⦄ → - ∃∃f1. L1 ⊢ 𝐅*⦃T⦄ ≡ f1 & f1 ⊆ f. +axiom lsubf_frees_trans: ∀f2,L2,T. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 → ∀f,L1. ⦃L1, f⦄ ⫃𝐅* ⦃L2, f2⦄ → + ∃∃f1. L1 ⊢ 𝐅*⦃T⦄ ≡ f1 & f1 ⊆ f. +(* #f2 #L2 #T #H elim H -f2 -L2 -T [ #f2 #I #Hf2 #f #L1 #H elim (lsubf_inv_atom2 … H) -H - #H1 #H2 destruct /3 width=3 by frees_atom, sle_refl, ex2_intro/ -| #f2 #I #K2 #W #s #_ #IH #f #L1 #H elim (lsubf_inv_push2 … H) -H * - [ #g1 #K1 #H12 #H1 #H2 - | #g #g1 #K1 #V #Hg #Hg1 #H12 #H1 #H2 #H3 - ] destruct elim (IH … H12) -f2 -K2 - /3 width=7 by frees_sort, sle_push, ex2_intro/ -| #f2 #I #K2 #W #_ #IH #f #L1 #H elim (lsubf_inv_next2 … H) -H * - [ #g1 #K1 #H12 #H1 #H2 destruct elim (IH … H12) -f2 -K2 + #H #_ destruct /3 width=3 by frees_atom, sle_isid_sn, ex2_intro/ +| #f2 #I #K2 #W #s #_ #IH #f #L1 #H elim (lsubf_inv_pair2 … H) -H * + [ #K1 #_ #H12 #H | #g #K1 #V #Hg #Hf #_ #H12 #H1 #H2 ] + destruct elim (IH … H12) -K2 + /3 width=3 by frees_sort, sle_inv_tl_dx, ex2_intro/ +| #f2 #I #K2 #W #_ #IH #f #L1 #H elim (lsubf_inv_pair2 … H) -H * + [ #K1 #H elim (sle_inv_nx … H ??) -H [