From 045c74915022181e288d9a950cc485437b08d002 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 29 Sep 2016 15:07:41 +0000 Subject: [PATCH] more on lfpx_frees.ma ... --- .../lambdadelta/basic_2/relocation/lexs.ma | 2 +- .../basic_2/relocation/lexs_lexs.ma | 4 +- .../basic_2/rt_transition/lfpx_frees.ma | 79 +++++++++++++++---- .../lambdadelta/basic_2/static/lfxs.ma | 12 +-- .../lambdadelta/basic_2/static/lfxs_main.ma | 4 +- .../ground_2/relocation/rtmap_coafter.ma | 12 ++- .../ground_2/relocation/rtmap_sle.ma | 13 +++ .../ground_2/relocation/rtmap_sor.ma | 13 +++ 8 files changed, 108 insertions(+), 31 deletions(-) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma index d0dbc7568..9587c2659 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma @@ -32,7 +32,7 @@ inductive lexs (RN,RP:relation3 lenv term term): rtmap → relation lenv ≝ interpretation "generic entrywise extension (local environment)" 'RelationStar RN RP f L1 L2 = (lexs RN RP f L1 L2). -definition lexs_pw_confluent2_R: relation3 lenv term term → relation3 lenv term term → +definition R_pw_confluent2_lexs: relation3 lenv term term → relation3 lenv term term → relation3 lenv term term → relation3 lenv term term → relation3 lenv term term → relation3 lenv term term → relation3 rtmap lenv term ≝ 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 13ec6ca81..cd7e64c51 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma @@ -45,8 +45,8 @@ theorem lexs_trans (RN) (RP) (f): lexs_transitive RN RN RN RN RP → (* Basic_2A1: includes: lpx_sn_conf *) theorem lexs_conf (RN1) (RP1) (RN2) (RP2): ∀L,f. - (∀g,I,K,V,n. ⬇*[n] L ≡ K.ⓑ{I}V → ⫯g = ⫱*[n] f → lexs_pw_confluent2_R RN1 RN2 RN1 RP1 RN2 RP2 g K V) → - (∀g,I,K,V,n. ⬇*[n] L ≡ K.ⓑ{I}V → ↑g = ⫱*[n] f → lexs_pw_confluent2_R RP1 RP2 RN1 RP1 RN2 RP2 g K V) → + (∀g,I,K,V,n. ⬇*[n] L ≡ K.ⓑ{I}V → ⫯g = ⫱*[n] f → R_pw_confluent2_lexs RN1 RN2 RN1 RP1 RN2 RP2 g K V) → + (∀g,I,K,V,n. ⬇*[n] L ≡ K.ⓑ{I}V → ↑g = ⫱*[n] f → R_pw_confluent2_lexs RP1 RP2 RN1 RP1 RN2 RP2 g K V) → pw_confluent2 … (lexs RN1 RP1 f) (lexs RN2 RP2 f) L. #RN1 #RP1 #RN2 #RP2 #L elim L -L [ #f #_ #_ #L1 #H1 #L2 #H2 >(lexs_inv_atom1 … H1) >(lexs_inv_atom1 … H2) -H2 -H1 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 47d35f2e5..935109f90 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 @@ -11,10 +11,7 @@ (* v GNU General Public License Version 2 *) (* *) (**************************************************************************) -(* -include "basic_2/multiple/frees_lreq.ma". -include "basic_2/multiple/frees_lift.ma". -*) + include "basic_2/relocation/drops_lexs.ma". include "basic_2/s_computation/fqup_weight.ma". include "basic_2/static/frees_drops.ma". @@ -32,23 +29,16 @@ axiom pippo: ∀RN,RP,L1,i. ⬇*[Ⓕ, 𝐔❴i❵] L1 ≡ ⋆ → lapply (lexs_co_dropable_sn … H1 … H2) // -HL1 -H2 *) -lemma coafter_uni_sn: ∀i,f. 𝐔❴i❵ ~⊚ f ≡ ↑*[i] f. -#i elim i -i /2 width=5 by coafter_isid_sn, coafter_next/ -qed. - -lemma sle_pushs: ∀f1,f2. f1 ⊆ f2 → ∀i. ↑*[i] f1 ⊆ ↑*[i] f2. -#f1 #f2 #Hf12 #i elim i -i /2 width=5 by sle_push/ -qed. - -axiom monotonic_sle_sor: ∀f1,g1. f1 ⊆ g1 → ∀f2,g2. f2 ⊆ g2 → - ∀f. f1 ⋓ f2 ≡ f → ∀g. g1 ⋓ g2 ≡ g → f ⊆ g. - -axiom sle_tl: ∀f1,f2. f1 ⊆ f2 → ⫱f1 ⊆ ⫱f2. axiom frees_inv_lifts_SO: ∀b,f,L,U. L ⊢ 𝐅*⦃U⦄ ≡ f → ∀K. ⬇*[b, 𝐔❴1❵] L ≡ K → ∀T. ⬆*[1] T ≡ U → K ⊢ 𝐅*⦃T⦄ ≡ ⫱f. +axiom frees_pair_flat: ∀L,T,f1,I1,V1. L.ⓑ{I1}V1 ⊢ 𝐅*⦃T⦄ ≡ f1 → + ∀f2,I2,V2. L.ⓑ{I2}V2 ⊢ 𝐅*⦃T⦄ ≡ f2 → + ∀f0. f1 ⋓ f2 ≡ f0 → + ∀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 → @@ -102,8 +92,63 @@ lemma cpx_frees_trans_lexs: ∀h,G,L1,T1,f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 → | #T2 #HT12 #HUT2 #H0 #H1 destruct -HgV1 lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T lapply (lexs_inv_tl … Abbr … V1 V1 HL12T ??) // -HL12T #HL12T + elim (IH … HgT1 … HL12T … HT12) // -L1 -T1 #gT2 #HgT2 #HgT21 + lapply (frees_inv_lifts_SO (Ⓣ) … HgT2 … L2 … HUT2) [ /3 width=1 by drops_refl, drops_drop/ ] -V1 -T2 + /5 width=6 by sor_inv_sle_dx, sle_trans, sle_tl, ex2_intro/ + ] +| #I #V1 #T0 #HG #HL #HU #g1 #H1 #L2 #H2 #U2 #H0 destruct + elim (frees_inv_flat … H1) -H1 #gV1 #gT0 #HgV1 #HgT0 #Hg1 + elim (cpx_inv_flat1 … H0) -H0 * + [ #V2 #T2 #HV12 #HT12 #H destruct + lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V + lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T + elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21 + elim (IH … HgT0 … HL12T … HT12) // -IH -HgT0 -HL12T -HT12 #gT2 #HgT2 #HgT21 + elim (sor_isfin_ex gV2 gT2) /2 width=3 by frees_fwd_isfin/ + /3 width=10 by frees_flat, monotonic_sle_sor, ex2_intro/ + | #HU2 #H destruct -HgV1 + lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T + elim (IH … HgT0 … HL12T … HU2) // -L1 -T0 -V1 + /4 width=6 by sor_inv_sle_dx, sle_trans, ex2_intro/ + | #HU2 #H destruct -HgT0 + lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ -H2 #HL12V + elim (IH … HgV1 … HL12V … HU2) // -L1 -T0 -V1 + /4 width=6 by sor_inv_sle_sn, sle_trans, ex2_intro/ + | #p #V2 #W1 #W2 #T1 #T2 #HV12 #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 + lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #H2 + 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 (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 - lapply (frees_inv_lifts_SO (Ⓣ) … HgT2 … L2 … HUT2) [ /3 width=1 by drops_refl, drops_drop/ ] + 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 #_ + @(ex2_intro … g2) + [ @(frees_bind … Hg2) /2 width=5 by frees_flat/ ] + | #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 + lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #H2 + 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 … Abbr … 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 + 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_push/ #gV0 #HgV0 #H + elim (sor_isfin_ex gW2 (⫱gV0)) /3 width=3 by frees_fwd_isfin, isfin_tl/ -H #g2 #Hg2 #_ + elim (sor_isfin_ex gW2 gV2) /2 width=3 by frees_fwd_isfin/ #g #Hg #_ + lapply (sor_trans2 … Hg2 … (⫱gT2) … Hg) /2 width=1 by sor_tl/ #Hg2 + lapply (frees_lifts (Ⓣ) … HgV2 … (L2.ⓓW2) … HV2 ??) [4: |*: /3 width=3 by drops_refl, drops_drop/ ] -V2 #HgV + lapply (sor_sym … Hg) -Hg #Hg + /4 width=10 by frees_flat, frees_bind, monotonic_sle_sor, sle_tl, ex2_intro/ + ] +] lemma cpx_frees_trans: ∀h,o,G. frees_trans (cpx h o G). /2 width=8 by lpx_cpx_frees_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma index 5c3a07a2a..605af05ce 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma @@ -26,12 +26,12 @@ 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_confluent_lfxs: relation4 (relation3 lenv term term) - (relation3 lenv term term) … ≝ - λR1,R2,RP1,RP2. - ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 → - ∀L1. L0 ⦻*[RP1, T0] L1 → ∀L2. L0 ⦻*[RP2, T0] L2 → - ∃∃T. R2 L1 T1 T & R1 L2 T2 T. +definition R_confluent2_lfxs: relation4 (relation3 lenv term term) + (relation3 lenv term term) … ≝ + λR1,R2,RP1,RP2. + ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 → + ∀L1. L0 ⦻*[RP1, T0] L1 → ∀L2. L0 ⦻*[RP2, T0] L2 → + ∃∃T. R2 L1 T1 T & R1 L2 T2 T. (* Basic properties ***********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_main.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_main.ma index 3d6a2658e..444d413ef 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_main.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_main.ma @@ -22,7 +22,7 @@ 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_confluent_lfxs R R R R → +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 @@ -47,4 +47,4 @@ 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 -*) \ No newline at end of file +*) diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma index cb5ede22b..56449d838 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma @@ -257,7 +257,7 @@ lemma coafter_inv_tl0: ∀g2,g1,g. g2 ~⊚ g1 ≡ ⫱g → ] qed-. -(* Properties on tls ********************************************************) +(* Properties with iterated tail ********************************************) lemma coafter_tls: ∀n,f1,f2,f. @⦃0, f1⦄ ≡ n → f1 ~⊚ f2 ≡ f → ⫱*[n]f1 ~⊚ f2 ≡ ⫱*[n]f. @@ -304,7 +304,7 @@ elim (coafter_inv_pxx … Hf … H2) -Hf -H2 * #f1 #g #_ #H1 #H0 destruct ] qed-. -(* Properties on isid *******************************************************) +(* Properties with test for identity ****************************************) corec lemma coafter_isid_sn: ∀f1. 𝐈⦃f1⦄ → ∀f2. f1 ~⊚ f2 ≡ f2. #f1 * -f1 #f1 #g1 #Hf1 #H1 #f2 cases (pn_split f2) * #g2 #H2 @@ -318,13 +318,19 @@ corec lemma coafter_isid_dx: ∀f2,f. 𝐈⦃f2⦄ → 𝐈⦃f⦄ → ∀f1. f1 ] qed. -(* Inversion lemmas on isid *************************************************) +(* Inversion lemmas with test for identity **********************************) lemma coafter_isid_inv_sn: ∀f1,f2,f. f1 ~⊚ f2 ≡ f → 𝐈⦃f1⦄ → f2 ≗ f. /3 width=6 by coafter_isid_sn, coafter_mono/ qed-. lemma coafter_isid_inv_dx: ∀f1,f2,f. f1 ~⊚ f2 ≡ f → 𝐈⦃f2⦄ → 𝐈⦃f⦄. /4 width=4 by eq_id_isid, coafter_isid_dx, coafter_mono/ qed-. + +(* Properties with uniform relocations **************************************) + +lemma coafter_uni_sn: ∀i,f. 𝐔❴i❵ ~⊚ f ≡ ↑*[i] f. +#i elim i -i /2 width=5 by coafter_isid_sn, coafter_next/ +qed. (* (* Properties on isuni ******************************************************) diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma index 29614b3dc..2fc90abd1 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma @@ -88,12 +88,25 @@ corec theorem sle_trans: Transitive … sle. /3 width=5 by sle_push, sle_next, sle_weak/ qed-. +(* Properties with iteraded push ********************************************) + +lemma sle_pushs: ∀f1,f2. f1 ⊆ f2 → ∀i. ↑*[i] f1 ⊆ ↑*[i] f2. +#f1 #f2 #Hf12 #i elim i -i /2 width=5 by sle_push/ +qed. + (* Properties with tail *****************************************************) lemma sle_px_tl: ∀g1,g2. g1 ⊆ g2 → ∀f1. ↑f1 = g1 → f1 ⊆ ⫱g2. #g1 #g2 #H #f1 #H1 elim (sle_inv_px … H … H1) -H -H1 * // qed. +lemma sle_tl: ∀f1,f2. f1 ⊆ f2 → ⫱f1 ⊆ ⫱f2. +#f1 elim (pn_split f1) * #g1 #H1 #f2 #H +[ lapply (sle_px_tl … H … H1) -H // +| elim (sle_inv_nx … H … H1) -H // +] +qed. + (* Inversion lemmas with tail ***********************************************) lemma sle_inv_tl_sn: ∀f1,f2. ⫱f1 ⊆ f2 → f1 ⊆ ⫯f2. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma index 839426b9a..f86e7f809 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma @@ -266,6 +266,19 @@ corec lemma sor_sym: ∀f1,f2,f. f1 ⋓ f2 ≡ f → f2 ⋓ f1 ≡ f. [ @sor_pp | @sor_pn | @sor_np | @sor_nn ] /2 width=7 by/ qed-. +(* Main properties **********************************************************) + +axiom monotonic_sle_sor: ∀f1,g1. f1 ⊆ g1 → ∀f2,g2. f2 ⊆ g2 → + ∀f. f1 ⋓ f2 ≡ f → ∀g. g1 ⋓ g2 ≡ g → f ⊆ g. + +axiom sor_trans1: ∀f0,f3,f4. f0 ⋓ f3 ≡ f4 → + ∀f1,f2. f1 ⋓ f2 ≡ f0 → + ∀f. f2 ⋓ f3 ≡ f → f1 ⋓ f ≡ f4. + +axiom sor_trans2: ∀f1,f0,f4. f1 ⋓ f0 ≡ f4 → + ∀f2, f3. f2 ⋓ f3 ≡ f0 → + ∀f. f1 ⋓ f2 ≡ f → f ⋓ f3 ≡ f4. + (* Properties with tail *****************************************************) lemma sor_tl: ∀f1,f2,f. f1 ⋓ f2 ≡ f → ⫱f1 ⋓ ⫱f2 ≡ ⫱f. -- 2.39.2