From f4e73c50acfc4ed453edd423c9bbe28af5dc9c4c Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 9 Jun 2016 14:45:23 +0000 Subject: [PATCH] frees_drops completed! --- .../basic_2/etc_new/frees/frees_lift.etc | 96 ------ .../basic_2/grammar/cl_restricted_weight.ma | 2 +- .../lambdadelta/basic_2/grammar/cl_weight.ma | 2 +- .../lambdadelta/basic_2/relocation/drops.ma | 288 +++++++++--------- .../basic_2/rt_transition/cpg_drops.ma | 5 +- .../lambdadelta/basic_2/static/aaa_drops.ma | 5 +- .../lambdadelta/basic_2/static/frees.ma | 3 +- .../lambdadelta/basic_2/static/frees_drops.ma | 112 +++---- .../lambdadelta/ground_2/lib/arith.ma | 3 + .../ground_2/relocation/rtmap_after.ma | 14 +- .../ground_2/relocation/rtmap_at.ma | 24 +- .../ground_2/relocation/rtmap_coafter.ma | 50 ++- .../ground_2/relocation/rtmap_pushs.ma | 2 +- .../ground_2/relocation/rtmap_tls.ma | 14 +- 14 files changed, 312 insertions(+), 308 deletions(-) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_lift.etc index 65b629206..7573f1e5a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_lift.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_lift.etc @@ -72,99 +72,3 @@ lemma frees_bind_dx_O: ∀a,I,L,W,U,i. L.ⓑ{I}W ⊢ ⫯i ϵ 𝐅*[0]⦃U⦄ → #a #I #L #W #U #i #HU elim (frees_dec L W 0 i) /4 width=5 by frees_S, frees_bind_dx, frees_bind_sn/ qed. - -(* Properties on relocation *************************************************) - -lemma frees_lift_ge: ∀K,T,l,i. K ⊢ i ϵ𝐅*[l]⦃T⦄ → - ∀L,s,l0,m0. ⬇[s, l0, m0] L ≡ K → - ∀U. ⬆[l0, m0] T ≡ U → l0 ≤ i → - L ⊢ i+m0 ϵ 𝐅*[l]⦃U⦄. -#K #T #l #i #H elim H -K -T -l -i -[ #K #T #l #i #HnT #L #s #l0 #m0 #_ #U #HTU #Hl0i -K -s - @frees_eq #X #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/ -| #I #K #K0 #T #V #l #i #j #Hlj #Hji #HnT #HK0 #HV #IHV #L #s #l0 #m0 #HLK #U #HTU #Hl0i - elim (ylt_split j l0) #H0 - [ elim (drop_trans_lt … HLK … HK0) // -K #L0 #W #HL0 >yminus_SO2 #HLK0 #HVW - @(frees_be … HL0) -HL0 -HV /3 width=3 by ylt_plus_dx2_trans/ - [ lapply (ylt_fwd_lt_O1 … H0) #H1 - #X #HXU <(ymax_pre_sn l0 1) in HTU; /2 width=1 by ylt_fwd_le_succ1/ #HTU - <(ylt_inv_O1 l0) in H0; // -H1 #H0 - elim (lift_div_le … HXU … HTU ?) -U /2 width=2 by ylt_fwd_succ2/ - | >yplus_minus_comm_inj /2 width=1 by ylt_fwd_le/ - commutative_plus -HLK0 #HLK0 - @(frees_be … HLK0) -HLK0 -IHV - /2 width=1 by monotonic_ylt_plus_dx, yle_plus_dx1_trans/ - [ #X yplus_pred1 /2 width=1 by ylt_to_minus/ - ymax_pre_sn /2 width=2 by/ -| #I #L #K0 #U #W #l #i #j #Hli #Hij #HnU #HLK0 #_ #IHW #K #s #l0 #m0 #HLK #T #HTU #Hlm0i - elim (ylt_split j l0) #H1 - [ elim (drop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW - elim (yle_inv_plus_inj2 … Hlm0i) #H0 #Hm0i - @(frees_be … H) -H - [ /3 width=1 by yle_plus_dx1_trans, monotonic_yle_minus_dx/ - | /2 width=3 by ylt_yle_trans/ - | #X #HXT elim (lift_trans_ge … HXT … HTU) -T /2 width=2 by ylt_fwd_le_succ1/ - | lapply (IHW … HKL0 … HVW ?) // -I -K -K0 -L0 -V -W -T -U -s - >yplus_pred1 /2 width=1 by ylt_to_minus/ - minus_minus_associative /2 width=1 by ylt_inv_inj/ yminus_SO2 >yplus_pred2 /2 width=1 by ylt_fwd_le_pred2/ - ] - | lapply (drop_conf_ge … HLK … HLK0 ?) // -L #HK0 - elim ( yle_inv_plus_inj2 … H2) -H2 #H2 #Hm0j - @(frees_be … HK0) - [ /2 width=1 by monotonic_yle_minus_dx/ - | /2 width=1 by monotonic_ylt_minus_dx/ - | #X #HXT elim (lift_trans_le … HXT … HTU) -T // - ymax_pre_sn /2 width=2 by/ - | yplus_minus_assoc_comm_inj // - >ymax_pre_sn /3 width=5 by yle_trans, ylt_fwd_le/ - ] - ] - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_restricted_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_restricted_weight.ma index fb2bcaf94..fcf56071b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_restricted_weight.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_restricted_weight.ma @@ -25,7 +25,7 @@ interpretation "weight (restricted closure)" 'Weight L T = (rfw L T). (* Basic_1: was: flt_shift *) lemma rfw_shift: ∀p,I,K,V,T. ♯{K.ⓑ{I}V, T} < ♯{K, ⓑ{p,I}V.T}. -normalize // +normalize /2 width=1 by monotonic_le_plus_r/ qed. lemma rfw_tpair_sn: ∀I,L,V,T. ♯{L, V} < ♯{L, ②{I}V.T}. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma index 5fb0671c2..bd837d4df 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma @@ -27,7 +27,7 @@ interpretation "weight (closure)" 'Weight G L T = (fw G L T). (* Basic_1: was: flt_shift *) lemma fw_shift: ∀p,I,G,K,V,T. ♯{G, K.ⓑ{I}V, T} < ♯{G, K, ⓑ{p,I}V.T}. -normalize // +normalize /2 width=1 by monotonic_le_plus_r/ qed. lemma fw_tpair_sn: ∀I,G,L,V,T. ♯{G, L, V} < ♯{G, L, ②{I}V.T}. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma index 9a4cfca83..e2f077575 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma @@ -87,11 +87,6 @@ lemma drops_eq_repl_fwd: ∀b,L1,L2. eq_repl_fwd … (λf. ⬇*[b, f] L1 ≡ L2) #b #L1 #L2 @eq_repl_sym /2 width=3 by drops_eq_repl_back/ (**) (* full auto fails *) qed-. -lemma drops_inv_tls_at: ∀f,i1,i2. @⦃i1,f⦄ ≡ i2 → - ∀b,L1,L2. ⬇*[b,⫱*[i2]f] L1 ≡ L2 → - ⬇*[b,↑⫱*[⫯i2]f] L1 ≡ L2. -/3 width=3 by drops_eq_repl_fwd, at_inv_tls/ qed-. - (* Basic_2A1: includes: drop_FT *) lemma drops_TF: ∀f,L1,L2. ⬇*[Ⓣ, f] L1 ≡ L2 → ⬇*[Ⓕ, f] L1 ≡ L2. #f #L1 #L2 #H elim H -f -L1 -L2 @@ -108,97 +103,6 @@ lemma drops_F: ∀b,f,L1,L2. ⬇*[b, f] L1 ≡ L2 → ⬇*[Ⓕ, f] L1 ≡ L2. * /2 width=1 by drops_TF/ qed-. -(* Basic_2A1: includes: drop_refl *) -lemma drops_refl: ∀b,L,f. 𝐈⦃f⦄ → ⬇*[b, f] L ≡ L. -#b #L elim L -L /2 width=1 by drops_atom/ -#L #I #V #IHL #f #Hf elim (isid_inv_gen … Hf) -Hf -/3 width=1 by drops_skip, lifts_refl/ -qed. - -(* Basic_2A1: includes: drop_split *) -lemma drops_split_trans: ∀b,f,L1,L2. ⬇*[b, f] L1 ≡ L2 → ∀f1,f2. f1 ⊚ f2 ≡ f → 𝐔⦃f1⦄ → - ∃∃L. ⬇*[b, f1] L1 ≡ L & ⬇*[b, f2] L ≡ L2. -#b #f #L1 #L2 #H elim H -f -L1 -L2 -[ #f #H0f #f1 #f2 #Hf #Hf1 @(ex2_intro … (⋆)) @drops_atom - #H lapply (H0f H) -b - #H elim (after_inv_isid3 … Hf H) -f // -| #f #I #L1 #L2 #V #HL12 #IHL12 #f1 #f2 #Hf #Hf1 elim (after_inv_xxn … Hf) -Hf [1,3: * |*: // ] - [ #g1 #g2 #Hf #H1 #H2 destruct - lapply (isuni_inv_push … Hf1 ??) -Hf1 [1,2: // ] #Hg1 - elim (IHL12 … Hf) -f - /4 width=5 by drops_drop, drops_skip, lifts_refl, isuni_isid, ex2_intro/ - | #g1 #Hf #H destruct elim (IHL12 … Hf) -f - /3 width=5 by ex2_intro, drops_drop, isuni_inv_next/ - ] -| #f #I #L1 #L2 #V1 #V2 #_ #HV21 #IHL12 #f1 #f2 #Hf #Hf1 elim (after_inv_xxp … Hf) -Hf [2,3: // ] - #g1 #g2 #Hf #H1 #H2 destruct elim (lifts_split_trans … HV21 … Hf) -HV21 - elim (IHL12 … Hf) -f /3 width=5 by ex2_intro, drops_skip, isuni_fwd_push/ -] -qed-. - -lemma drops_split_div: ∀b,f1,L1,L. ⬇*[b, f1] L1 ≡ L → ∀f2,f. f1 ⊚ f2 ≡ f → 𝐔⦃f2⦄ → - ∃∃L2. ⬇*[Ⓕ, f2] L ≡ L2 & ⬇*[Ⓕ, f] L1 ≡ L2. -#b #f1 #L1 #L #H elim H -f1 -L1 -L -[ #f1 #Hf1 #f2 #f #Hf #Hf2 @(ex2_intro … (⋆)) @drops_atom #H destruct -| #f1 #I #L1 #L #V #HL1 #IH #f2 #f #Hf #Hf2 elim (after_inv_nxx … Hf) -Hf [2,3: // ] - #g #Hg #H destruct elim (IH … Hg) -IH -Hg /3 width=5 by drops_drop, ex2_intro/ -| #f1 #I #L1 #L #V1 #V #HL1 #HV1 #IH #f2 #f #Hf #Hf2 - elim (after_inv_pxx … Hf) -Hf [1,3: * |*: // ] - #g2 #g #Hg #H2 #H0 destruct - [ lapply (isuni_inv_push … Hf2 ??) -Hf2 [1,2: // ] #Hg2 -IH - lapply (after_isid_inv_dx … Hg … Hg2) -Hg #Hg - /5 width=7 by drops_eq_repl_back, drops_F, drops_refl, drops_skip, lifts_eq_repl_back, isid_push, ex2_intro/ - | lapply (isuni_inv_next … Hf2 ??) -Hf2 [1,2: // ] #Hg2 -HL1 -HV1 - elim (IH … Hg) -f1 /3 width=3 by drops_drop, ex2_intro/ - ] -] -qed-. - -(* Basic forward lemmas *****************************************************) - -(* Basic_1: includes: drop_gen_refl *) -(* Basic_2A1: includes: drop_inv_O2 *) -lemma drops_fwd_isid: ∀b,f,L1,L2. ⬇*[b, f] L1 ≡ L2 → 𝐈⦃f⦄ → L1 = L2. -#b #f #L1 #L2 #H elim H -f -L1 -L2 // -[ #f #I #L1 #L2 #V #_ #_ #H elim (isid_inv_next … H) // -| /5 width=5 by isid_inv_push, lifts_fwd_isid, eq_f3, sym_eq/ -] -qed-. - -fact drops_fwd_drop2_aux: ∀b,f2,X,Y. ⬇*[b, f2] X ≡ Y → ∀I,K,V. Y = K.ⓑ{I}V → - ∃∃f1,f. 𝐈⦃f1⦄ & f2 ⊚ ⫯f1 ≡ f & ⬇*[b, f] X ≡ K. -#b #f2 #X #Y #H elim H -f2 -X -Y -[ #f2 #Hf2 #J #K #W #H destruct -| #f2 #I #L1 #L2 #V #_ #IHL #J #K #W #H elim (IHL … H) -IHL - /3 width=7 by after_next, ex3_2_intro, drops_drop/ -| #f2 #I #L1 #L2 #V1 #V2 #HL #_ #_ #J #K #W #H destruct - lapply (after_isid_dx 𝐈𝐝 … f2) /3 width=9 by after_push, ex3_2_intro, drops_drop/ -] -qed-. - -lemma drops_fwd_drop2: ∀b,f2,I,X,K,V. ⬇*[b, f2] X ≡ K.ⓑ{I}V → - ∃∃f1,f. 𝐈⦃f1⦄ & f2 ⊚ ⫯f1 ≡ f & ⬇*[b, f] X ≡ K. -/2 width=5 by drops_fwd_drop2_aux/ qed-. - -lemma drops_after_fwd_drop2: ∀b,f2,I,X,K,V. ⬇*[b, f2] X ≡ K.ⓑ{I}V → - ∀f1,f. 𝐈⦃f1⦄ → f2 ⊚ ⫯f1 ≡ f → ⬇*[b, f] X ≡ K. -#b #f2 #I #X #K #V #H #f1 #f #Hf1 #Hf elim (drops_fwd_drop2 … H) -H -#g1 #g #Hg1 #Hg #HK lapply (after_mono_eq … Hg … Hf ??) -Hg -Hf -/3 width=5 by drops_eq_repl_back, isid_inv_eq_repl, eq_next/ -qed-. - -(* Basic_1: was: drop_S *) -(* Basic_2A1: was: drop_fwd_drop2 *) -lemma drops_isuni_fwd_drop2: ∀b,f,I,X,K,V. 𝐔⦃f⦄ → ⬇*[b, f] X ≡ K.ⓑ{I}V → ⬇*[b, ⫯f] X ≡ K. -/3 width=7 by drops_after_fwd_drop2, after_isid_isuni/ qed-. - -(* Forward lemmas with test for finite colength *****************************) - -lemma drops_fwd_isfin: ∀f,L1,L2. ⬇*[Ⓣ, f] L1 ≡ L2 → 𝐅⦃f⦄. -#f #L1 #L2 #H elim H -f -L1 -L2 -/3 width=1 by isfin_next, isfin_push, isfin_isid/ -qed-. - (* Basic inversion lemmas ***************************************************) fact drops_inv_atom1_aux: ∀b,f,X,Y. ⬇*[b, f] X ≡ Y → X = ⋆ → @@ -261,49 +165,104 @@ lemma drops_inv_skip2: ∀b,f,I,X,K2,V2. ⬇*[b, ↑f] X ≡ K2.ⓑ{I}V2 → ∃∃K1,V1. ⬇*[b, f] K1 ≡ K2 & ⬆*[f] V2 ≡ V1 & X = K1.ⓑ{I}V1. /2 width=5 by drops_inv_skip2_aux/ qed-. -fact drops_inv_TF_aux: ∀f,L1,L2. ⬇*[Ⓕ, f] L1 ≡ L2 → 𝐔⦃f⦄ → - ∀I,K,V. L2 = K.ⓑ{I}V → - ⬇*[Ⓣ, f] L1 ≡ K.ⓑ{I}V. -#f #L1 #L2 #H elim H -f -L1 -L2 -[ #f #_ #_ #J #K #W #H destruct -| #f #I #L1 #L2 #V #_ #IH #Hf #J #K #W #H destruct - /4 width=3 by drops_drop, isuni_inv_next/ -| #f #I #L1 #L2 #V1 #V2 #HL12 #HV21 #_ #Hf #J #K #W #H destruct - lapply (isuni_inv_push … Hf ??) -Hf [1,2: // ] #Hf - <(drops_fwd_isid … HL12) -K // <(lifts_fwd_isid … HV21) -V1 - /3 width=3 by drops_refl, isid_push/ +(* Basic forward lemmas *****************************************************) + +fact drops_fwd_drop2_aux: ∀b,f2,X,Y. ⬇*[b, f2] X ≡ Y → ∀I,K,V. Y = K.ⓑ{I}V → + ∃∃f1,f. 𝐈⦃f1⦄ & f2 ⊚ ⫯f1 ≡ f & ⬇*[b, f] X ≡ K. +#b #f2 #X #Y #H elim H -f2 -X -Y +[ #f2 #Hf2 #J #K #W #H destruct +| #f2 #I #L1 #L2 #V #_ #IHL #J #K #W #H elim (IHL … H) -IHL + /3 width=7 by after_next, ex3_2_intro, drops_drop/ +| #f2 #I #L1 #L2 #V1 #V2 #HL #_ #_ #J #K #W #H destruct + lapply (after_isid_dx 𝐈𝐝 … f2) /3 width=9 by after_push, ex3_2_intro, drops_drop/ ] qed-. -(* Basic_2A1: includes: drop_inv_FT *) -lemma drops_inv_TF: ∀f,I,L,K,V. ⬇*[Ⓕ, f] L ≡ K.ⓑ{I}V → 𝐔⦃f⦄ → - ⬇*[Ⓣ, f] L ≡ K.ⓑ{I}V. -/2 width=3 by drops_inv_TF_aux/ qed-. +lemma drops_fwd_drop2: ∀b,f2,I,X,K,V. ⬇*[b, f2] X ≡ K.ⓑ{I}V → + ∃∃f1,f. 𝐈⦃f1⦄ & f2 ⊚ ⫯f1 ≡ f & ⬇*[b, f] X ≡ K. +/2 width=5 by drops_fwd_drop2_aux/ qed-. -(* Advanced inversion lemmas ************************************************) +(* Properties with test for identity ****************************************) -lemma drops_inv_atom2: ∀b,L,f. ⬇*[b,f] L ≡ ⋆ → - ∃∃n,f1. ⬇*[b,𝐔❴n❵] L ≡ ⋆ & 𝐔❴n❵ ⊚ f1 ≡ f. -#b #L elim L -L -[ /3 width=4 by drops_atom, after_isid_sn, ex2_2_intro/ -| #L #I #V #IH #f #H elim (pn_split f) * #g #H0 destruct - [ elim (drops_inv_skip1 … H) -H #K #W #_ #_ #H destruct - | lapply (drops_inv_drop1 … H) -H #HL - elim (IH … HL) -IH -HL /3 width=8 by drops_drop, after_next, ex2_2_intro/ - ] +(* Basic_2A1: includes: drop_refl *) +lemma drops_refl: ∀b,L,f. 𝐈⦃f⦄ → ⬇*[b, f] L ≡ L. +#b #L elim L -L /2 width=1 by drops_atom/ +#L #I #V #IHL #f #Hf elim (isid_inv_gen … Hf) -Hf +/3 width=1 by drops_skip, lifts_refl/ +qed. + +(* Forward lemmas test for identity *****************************************) + +(* Basic_1: includes: drop_gen_refl *) +(* Basic_2A1: includes: drop_inv_O2 *) +lemma drops_fwd_isid: ∀b,f,L1,L2. ⬇*[b, f] L1 ≡ L2 → 𝐈⦃f⦄ → L1 = L2. +#b #f #L1 #L2 #H elim H -f -L1 -L2 // +[ #f #I #L1 #L2 #V #_ #_ #H elim (isid_inv_next … H) // +| /5 width=5 by isid_inv_push, lifts_fwd_isid, eq_f3, sym_eq/ ] qed-. -(* Basic_2A1: includes: drop_inv_gen *) -lemma drops_inv_gen: ∀b,f,I,L,K,V. ⬇*[b, f] L ≡ K.ⓑ{I}V → 𝐔⦃f⦄ → - ⬇*[Ⓣ, f] L ≡ K.ⓑ{I}V. -* /2 width=1 by drops_inv_TF/ + +lemma drops_after_fwd_drop2: ∀b,f2,I,X,K,V. ⬇*[b, f2] X ≡ K.ⓑ{I}V → + ∀f1,f. 𝐈⦃f1⦄ → f2 ⊚ ⫯f1 ≡ f → ⬇*[b, f] X ≡ K. +#b #f2 #I #X #K #V #H #f1 #f #Hf1 #Hf elim (drops_fwd_drop2 … H) -H +#g1 #g #Hg1 #Hg #HK lapply (after_mono_eq … Hg … Hf ??) -Hg -Hf +/3 width=5 by drops_eq_repl_back, isid_inv_eq_repl, eq_next/ qed-. -(* Basic_2A1: includes: drop_inv_T *) -lemma drops_inv_F: ∀b,f,I,L,K,V. ⬇*[Ⓕ, f] L ≡ K.ⓑ{I}V → 𝐔⦃f⦄ → - ⬇*[b, f] L ≡ K.ⓑ{I}V. -* /2 width=1 by drops_inv_TF/ +(* Forward lemmas with test for finite colength *****************************) + +lemma drops_fwd_isfin: ∀f,L1,L2. ⬇*[Ⓣ, f] L1 ≡ L2 → 𝐅⦃f⦄. +#f #L1 #L2 #H elim H -f -L1 -L2 +/3 width=1 by isfin_next, isfin_push, isfin_isid/ +qed-. + +(* Properties with uniform relocations **************************************) + +lemma drops_uni_ex: ∀L,i. ⬇*[Ⓕ, 𝐔❴i❵] L ≡ ⋆ ∨ ∃∃I,K,V. ⬇*[i] L ≡ K.ⓑ{I}V. +#L elim L -L /2 width=1 by or_introl/ +#L #I #V #IH * /4 width=4 by drops_refl, ex1_3_intro, or_intror/ +#i elim (IH i) -IH /3 width=1 by drops_drop, or_introl/ +* /4 width=4 by drops_drop, ex1_3_intro, or_intror/ +qed-. + +(* Basic_2A1: includes: drop_split *) +lemma drops_split_trans: ∀b,f,L1,L2. ⬇*[b, f] L1 ≡ L2 → ∀f1,f2. f1 ⊚ f2 ≡ f → 𝐔⦃f1⦄ → + ∃∃L. ⬇*[b, f1] L1 ≡ L & ⬇*[b, f2] L ≡ L2. +#b #f #L1 #L2 #H elim H -f -L1 -L2 +[ #f #H0f #f1 #f2 #Hf #Hf1 @(ex2_intro … (⋆)) @drops_atom + #H lapply (H0f H) -b + #H elim (after_inv_isid3 … Hf H) -f // +| #f #I #L1 #L2 #V #HL12 #IHL12 #f1 #f2 #Hf #Hf1 elim (after_inv_xxn … Hf) -Hf [1,3: * |*: // ] + [ #g1 #g2 #Hf #H1 #H2 destruct + lapply (isuni_inv_push … Hf1 ??) -Hf1 [1,2: // ] #Hg1 + elim (IHL12 … Hf) -f + /4 width=5 by drops_drop, drops_skip, lifts_refl, isuni_isid, ex2_intro/ + | #g1 #Hf #H destruct elim (IHL12 … Hf) -f + /3 width=5 by ex2_intro, drops_drop, isuni_inv_next/ + ] +| #f #I #L1 #L2 #V1 #V2 #_ #HV21 #IHL12 #f1 #f2 #Hf #Hf1 elim (after_inv_xxp … Hf) -Hf [2,3: // ] + #g1 #g2 #Hf #H1 #H2 destruct elim (lifts_split_trans … HV21 … Hf) -HV21 + elim (IHL12 … Hf) -f /3 width=5 by ex2_intro, drops_skip, isuni_fwd_push/ +] +qed-. + +lemma drops_split_div: ∀b,f1,L1,L. ⬇*[b, f1] L1 ≡ L → ∀f2,f. f1 ⊚ f2 ≡ f → 𝐔⦃f2⦄ → + ∃∃L2. ⬇*[Ⓕ, f2] L ≡ L2 & ⬇*[Ⓕ, f] L1 ≡ L2. +#b #f1 #L1 #L #H elim H -f1 -L1 -L +[ #f1 #Hf1 #f2 #f #Hf #Hf2 @(ex2_intro … (⋆)) @drops_atom #H destruct +| #f1 #I #L1 #L #V #HL1 #IH #f2 #f #Hf #Hf2 elim (after_inv_nxx … Hf) -Hf [2,3: // ] + #g #Hg #H destruct elim (IH … Hg) -IH -Hg /3 width=5 by drops_drop, ex2_intro/ +| #f1 #I #L1 #L #V1 #V #HL1 #HV1 #IH #f2 #f #Hf #Hf2 + elim (after_inv_pxx … Hf) -Hf [1,3: * |*: // ] + #g2 #g #Hg #H2 #H0 destruct + [ lapply (isuni_inv_push … Hf2 ??) -Hf2 [1,2: // ] #Hg2 -IH + lapply (after_isid_inv_dx … Hg … Hg2) -Hg #Hg + /5 width=7 by drops_eq_repl_back, drops_F, drops_refl, drops_skip, lifts_eq_repl_back, isid_push, ex2_intro/ + | lapply (isuni_inv_next … Hf2 ??) -Hf2 [1,2: // ] #Hg2 -HL1 -HV1 + elim (IH … Hg) -f1 /3 width=3 by drops_drop, ex2_intro/ + ] +] qed-. (* Inversion lemmas with test for uniformity ********************************) @@ -351,8 +310,58 @@ lemma drops_inv_pair2_isuni_next: ∀b,f,I,K,V,L1. 𝐔⦃f⦄ → ⬇*[b, ⫯f] ] qed-. +fact drops_inv_TF_aux: ∀f,L1,L2. ⬇*[Ⓕ, f] L1 ≡ L2 → 𝐔⦃f⦄ → + ∀I,K,V. L2 = K.ⓑ{I}V → + ⬇*[Ⓣ, f] L1 ≡ K.ⓑ{I}V. +#f #L1 #L2 #H elim H -f -L1 -L2 +[ #f #_ #_ #J #K #W #H destruct +| #f #I #L1 #L2 #V #_ #IH #Hf #J #K #W #H destruct + /4 width=3 by drops_drop, isuni_inv_next/ +| #f #I #L1 #L2 #V1 #V2 #HL12 #HV21 #_ #Hf #J #K #W #H destruct + lapply (isuni_inv_push … Hf ??) -Hf [1,2: // ] #Hf + <(drops_fwd_isid … HL12) -K // <(lifts_fwd_isid … HV21) -V1 + /3 width=3 by drops_refl, isid_push/ +] +qed-. + +(* Basic_2A1: includes: drop_inv_FT *) +lemma drops_inv_TF: ∀f,I,L,K,V. ⬇*[Ⓕ, f] L ≡ K.ⓑ{I}V → 𝐔⦃f⦄ → + ⬇*[Ⓣ, f] L ≡ K.ⓑ{I}V. +/2 width=3 by drops_inv_TF_aux/ qed-. + +(* Basic_2A1: includes: drop_inv_gen *) +lemma drops_inv_gen: ∀b,f,I,L,K,V. ⬇*[b, f] L ≡ K.ⓑ{I}V → 𝐔⦃f⦄ → + ⬇*[Ⓣ, f] L ≡ K.ⓑ{I}V. +* /2 width=1 by drops_inv_TF/ +qed-. + +(* Basic_2A1: includes: drop_inv_T *) +lemma drops_inv_F: ∀b,f,I,L,K,V. ⬇*[Ⓕ, f] L ≡ K.ⓑ{I}V → 𝐔⦃f⦄ → + ⬇*[b, f] L ≡ K.ⓑ{I}V. +* /2 width=1 by drops_inv_TF/ +qed-. + +(* Forward lemmas with test for uniformity **********************************) + +(* Basic_1: was: drop_S *) +(* Basic_2A1: was: drop_fwd_drop2 *) +lemma drops_isuni_fwd_drop2: ∀b,f,I,X,K,V. 𝐔⦃f⦄ → ⬇*[b, f] X ≡ K.ⓑ{I}V → ⬇*[b, ⫯f] X ≡ K. +/3 width=7 by drops_after_fwd_drop2, after_isid_isuni/ qed-. + (* Inversion lemmas with uniform relocations ********************************) +lemma drops_inv_atom2: ∀b,L,f. ⬇*[b, f] L ≡ ⋆ → + ∃∃n,f1. ⬇*[b, 𝐔❴n❵] L ≡ ⋆ & 𝐔❴n❵ ⊚ f1 ≡ f. +#b #L elim L -L +[ /3 width=4 by drops_atom, after_isid_sn, ex2_2_intro/ +| #L #I #V #IH #f #H elim (pn_split f) * #g #H0 destruct + [ elim (drops_inv_skip1 … H) -H #K #W #_ #_ #H destruct + | lapply (drops_inv_drop1 … H) -H #HL + elim (IH … HL) -IH -HL /3 width=8 by drops_drop, after_next, ex2_2_intro/ + ] +] +qed-. + lemma drops_inv_succ: ∀l,L1,L2. ⬇*[⫯l] L1 ≡ L2 → ∃∃I,K,V. ⬇*[l] K ≡ L2 & L1 = K.ⓑ{I}V. #l #L1 #L2 #H elim (drops_inv_isuni … H) -H // * @@ -361,14 +370,21 @@ lemma drops_inv_succ: ∀l,L1,L2. ⬇*[⫯l] L1 ≡ L2 → ] qed-. -(* Properties with uniform relocations **************************************) +(* Properties with application **********************************************) -lemma drops_uni_ex: ∀L,i. ⬇*[Ⓕ, 𝐔❴i❵] L ≡ ⋆ ∨ ∃∃I,K,V. ⬇*[i] L ≡ K.ⓑ{I}V. -#L elim L -L /2 width=1 by or_introl/ -#L #I #V #IH * /4 width=4 by drops_refl, ex1_3_intro, or_intror/ -#i elim (IH i) -IH /3 width=1 by drops_drop, or_introl/ -* /4 width=4 by drops_drop, ex1_3_intro, or_intror/ -qed-. +lemma drops_tls_at: ∀f,i1,i2. @⦃i1,f⦄ ≡ i2 → + ∀b,L1,L2. ⬇*[b,⫱*[i2]f] L1 ≡ L2 → + ⬇*[b,↑⫱*[⫯i2]f] L1 ≡ L2. +/3 width=3 by drops_eq_repl_fwd, at_inv_tls/ qed-. + +lemma drops_split_trans_pair2: ∀b,f,I,L,K0,V. ⬇*[b, f] L ≡ K0.ⓑ{I}V → ∀n. @⦃O, f⦄ ≡ n → + ∃∃K,W. ⬇*[n]L ≡ K.ⓑ{I}W & ⬇*[b, ⫱*[⫯n]f] K ≡ K0 & ⬆*[⫱*[⫯n]f] V ≡ W. +#b #f #I #L #K0 #V #H #n #Hf +elim (drops_split_trans … H) -H [ |5: @(after_uni_dx … Hf) |2,3: skip ] /2 width=1 by after_isid_dx/ #Y #HLY #H +lapply (drops_tls_at … Hf … H) -H #H +elim (drops_inv_skip2 … H) -H #K #W #HK0 #HVW #H destruct +/3 width=5 by drops_inv_gen, ex3_2_intro/ +qed-. (* Basic_2A1: removed theorems 12: drops_inv_nil drops_inv_cons d1_liftable_liftables diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma index 779ea690b..7c9c79b70 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma @@ -80,6 +80,7 @@ qed-. (* Properties with generic slicing for local environments *******************) +(* Note: it should use drops_split_trans_pair2 *) lemma cpg_lifts: ∀c,h,G. d_liftable2 (cpg h c G). #c #h #G #K #T generalize in match c; -c @(fqup_wf_ind_eq … G K T) -G -K -T #G0 #K0 #T0 #IH #G #K * * @@ -94,7 +95,7 @@ lemma cpg_lifts: ∀c,h,G. d_liftable2 (cpg h c G). elim (lifts_inv_lref1 … H1) -H1 #i2 #Hf #H destruct lapply (drops_trans … HLK … HK0 ??) -HLK [3,6: |*: // ] #H elim (drops_split_trans … H) -H [1,6: |*: /2 width=6 by after_uni_dx/ ] #Y #HL0 #HY - lapply (drops_inv_tls_at … Hf … HY) -HY #HY + lapply (drops_tls_at … Hf … HY) -HY #HY elim (drops_inv_skip2 … HY) -HY #L0 #W #HLK0 #HVW #H destruct elim (IH … HV2 … HLK0 … HVW) -IH /2 width=2 by fqup_lref/ -K -K0 -V #W2 #HVW2 #HW2 elim (lifts_total W2 (𝐔❴⫯i2❵)) #U2 #HWU2 @@ -166,7 +167,7 @@ lemma cpg_inv_lifts1: ∀c,h,G. d_deliftable2_sn (cpg h c G). elim (lifts_inv_lref2 … H1) -H1 #i1 #Hf #H destruct lapply (drops_split_div … HLK (𝐔❴i1❵) ???) -HLK [4,8: * |*: // ] #Y0 #HK0 #HLY0 lapply (drops_conf … HL0 … HLY0 ??) -HLY0 [3,6: |*: /2 width=6 by after_uni_dx/ ] #HLY0 - lapply (drops_inv_tls_at … Hf … HLY0) -HLY0 #HLY0 + lapply (drops_tls_at … Hf … HLY0) -HLY0 #HLY0 elim (drops_inv_skip1 … HLY0) -HLY0 #K0 #V #HLK0 #HVW #H destruct elim (IH … HW2 … HLK0 … HVW) -IH /2 width=2 by fqup_lref/ -L -L0 -W #V2 #HVW2 #HV2 lapply (lifts_trans … HVW2 … HWU2 ??) -W2 [3,6: |*: // ] #HVU2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_drops.ma index 4255a20c4..57c8790ce 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_drops.ma @@ -46,6 +46,7 @@ qed-. (* Properties with generic slicing for local environments *******************) (* Basic_2A1: includes: aaa_lift *) +(* Note: it should use drops_split_trans_pair2 *) lemma aaa_lifts: ∀G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → ∀b,f,L2. ⬇*[b, f] L2 ≡ L1 → ∀T2. ⬆*[f] T1 ≡ T2 → ⦃G, L2⦄ ⊢ T2 ⁝ A. @fqup_wf_ind_eq #G0 #L0 #T0 #IH #G #L1 * * @@ -57,7 +58,7 @@ lemma aaa_lifts: ∀G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → ∀b,f,L2. ⬇*[b, f elim (lifts_inv_lref1 … HX) -HX #i2 #Hf #H destruct lapply (drops_trans … HL21 … HLK1 ??) -HL21 [1,2: // ] #H elim (drops_split_trans … H) -H [ |*: /2 width=6 by after_uni_dx/ ] #Y #HLK2 #HY - lapply (drops_inv_tls_at … Hf … HY) -HY #HY -Hf + lapply (drops_tls_at … Hf … HY) -HY #HY -Hf elim (drops_inv_skip2 … HY) -HY #K2 #V2 #HK21 #HV12 #H destruct /4 width=12 by aaa_lref_drops, fqup_lref, drops_inv_gen/ | #l #HG #HL #HT #A #H #b #f #L2 #HL21 #X #HX -b -f -IH @@ -95,7 +96,7 @@ lemma aaa_inv_lifts: ∀G,L2,T2,A. ⦃G, L2⦄ ⊢ T2 ⁝ A → ∀b,f,L1. ⬇*[ elim (lifts_inv_lref2 … HX) -HX #i1 #Hf #H destruct lapply (drops_split_div … HL21 (𝐔❴i1❵) ???) -HL21 [4: * |*: // ] #Y #HLK1 #HY lapply (drops_conf … HLK2 … HY ??) -HY [1,2: /2 width=6 by after_uni_dx/ ] #HY - lapply (drops_inv_tls_at … Hf … HY) -HY #HY -Hf + lapply (drops_tls_at … Hf … HY) -HY #HY -Hf elim (drops_inv_skip1 … HY) -HY #K1 #V1 #HK21 #HV12 #H destruct /4 width=12 by aaa_lref_drops, fqup_lref, drops_inv_F/ | #l #HG #HL #HT #A #H #b #f #L1 #HL21 #X #HX -IH -b -f diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees.ma index 31bf511d3..3699063ce 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/frees.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees.ma @@ -185,13 +185,14 @@ lemma frees_gref_gen: ∀f,L,p. 𝐈⦃f⦄ → L ⊢ 𝐅*⦃§p⦄ ≡ f. /4 width=3 by frees_eq_repl_back, frees_gref, frees_atom, eq_push_inv_isid/ qed. -(* Basic_2A1: removed theorems 27: +(* Basic_2A1: removed theorems 30: frees_eq frees_be frees_inv frees_inv_sort frees_inv_gref frees_inv_lref frees_inv_lref_free frees_inv_lref_skip frees_inv_lref_ge frees_inv_lref_lt frees_inv_bind frees_inv_flat frees_inv_bind_O frees_lref_eq frees_lref_be frees_weak frees_bind_sn frees_bind_dx frees_flat_sn frees_flat_dx + frees_lift_ge frees_inv_lift_be frees_inv_lift_ge lreq_frees_trans frees_lreq_conf llor_atom llor_skip llor_total llor_tail_frees llor_tail_cofrees diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma index aa4f34998..681e07d8c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "ground_2/relocation/rtmap_pushs.ma". include "ground_2/relocation/rtmap_coafter.ma". include "basic_2/relocation/drops_drops.ma". include "basic_2/static/frees.ma". @@ -38,6 +37,30 @@ lemma frees_lref_pair: ∀f,K,V. K ⊢ 𝐅*⦃V⦄ ≡ f → ] qed. +lemma frees_sort_pushs: ∀f,K,s. K ⊢ 𝐅*⦃⋆s⦄ ≡ f → + ∀i,L. ⬇*[i] L ≡ K → L ⊢ 𝐅*⦃⋆s⦄ ≡ ↑*[i] f. +#f #K #s #Hf #i elim i -i +[ #L #H lapply (drops_fwd_isid … H ?) -H // +| #i #IH #L #H elim (drops_inv_succ … H) -H /3 width=1 by frees_sort/ +] +qed. + +lemma frees_lref_pushs: ∀f,K,j. K ⊢ 𝐅*⦃#j⦄ ≡ f → + ∀i,L. ⬇*[i] L ≡ K → L ⊢ 𝐅*⦃#(i+j)⦄ ≡ ↑*[i] f. +#f #K #j #Hf #i elim i -i +[ #L #H lapply (drops_fwd_isid … H ?) -H // +| #i #IH #L #H elim (drops_inv_succ … H) -H /3 width=1 by frees_lref/ +] +qed. + +lemma frees_gref_pushs: ∀f,K,l. K ⊢ 𝐅*⦃§l⦄ ≡ f → + ∀i,L. ⬇*[i] L ≡ K → L ⊢ 𝐅*⦃§l⦄ ≡ ↑*[i] f. +#f #K #l #Hf #i elim i -i +[ #L #H lapply (drops_fwd_isid … H ?) -H // +| #i #IH #L #H elim (drops_inv_succ … H) -H /3 width=1 by frees_gref/ +] +qed. + (* Advanced inversion lemmas ************************************************) lemma frees_inv_lref_drops: ∀i,f,L. L ⊢ 𝐅*⦃#i⦄ ≡ f → @@ -58,28 +81,6 @@ qed-. (* Properties with generic slicing for local environments *******************) -axiom coafter_inv_xpx: ∀g2,f1,g. g2 ~⊚ ↑f1 ≡ g → ∀n. @⦃0, g2⦄ ≡ n → - ∃∃f2,f. f2 ~⊚ f1 ≡ f & ⫱*[n]g2 = ↑f2 & ⫱*[n]g = ↑f. -(* -#g2 #g1 #g #Hg #n #Hg2 -lapply (coafter_tls … Hg2 … Hg) -Hg #Hg -lapply (at_pxx_tls … Hg2) -Hg2 #H -elim (at_inv_pxp … H) -H [ |*: // ] #f2 #H2 -elim (coafter_inv_pxx … Hg … H2) -Hg * #f1 #f #Hf #H1 #H0 destruct -plus_S1 /2 width=3 by frees_lref_pushs/ (**) (* full auto fails *) +| #f1 #I #K #V #l #_ #IH #Hf1 #f #L #H1 #U #H2 #f2 #H3 + lapply (isfin_fwd_push … Hf1 ??) -Hf1 [3: |*: // ] #Hf1 + lapply (lifts_inv_gref1 … H2) -H2 #H destruct + elim (drops_split_trans_pair2 … H1) -H1 [ |*: // ] #Y #W #HLY #HYK #_ + elim (coafter_fwd_xpx_pushs … H3) [ |*: // ] #g2 #H2 destruct + lapply (coafter_tls_succ … H3 ??) -H3 [3: |*: // ] #H3 + lapply (IH … HYK … H3) -IH -H3 -HYK [1,3: // | skip ] + /3 width=5 by drops_isuni_fwd_drop2, frees_gref_pushs/ | #f1V #f1T #f1 #p #I #K #V #T #_ #_ #H1f1 #IHV #IHT #H2f1 #f #L #H1 #Y #H2 #f2 #H3 elim (sor_inv_isfin3 … H1f1) // #Hf1V #H lapply (isfin_inv_tl … H) -H @@ -142,6 +141,7 @@ lemma frees_lifts: ∀b,f1,K,T. K ⊢ 𝐅*⦃T⦄ ≡ f1 → elim (coafter_sor … H3 … H1f1) /3 width=5 by coafter_isfin2_fwd, frees_flat/ ] +qed-. (* Inversion lemmas with generic slicing for local environments *************) diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma index f86f7a3bd..8ce8b954c 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma @@ -35,6 +35,9 @@ normalize // qed. lemma pred_S: ∀m. pred (S m) = m. // qed. +lemma plus_S1: ∀x,y. ⫯(x+y) = (⫯x) + y. +// qed. + lemma max_O1: ∀n. n = (0 ∨ n). // qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma index f202aa02b..4ca5caf74 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma @@ -270,8 +270,10 @@ lemma after_mono_eq: ∀f1,f2,f. f1 ⊚ f2 ≡ f → ∀g1,g2,g. g1 ⊚ g2 ≡ g lemma after_tls: ∀n,f1,f2,f. @⦃0, f1⦄ ≡ n → f1 ⊚ f2 ≡ f → ⫱*[n]f1 ⊚ f2 ≡ ⫱*[n]f. #n elim n -n // -#n #IH #f1 #f2 #f #Hf1 #Hf cases (at_inv_pxn … Hf1) -Hf1 [ |*: // ] -#g1 #Hg1 #H1 cases (after_inv_nxx … Hf … H1) -Hf /2 width=1 by/ +#n #IH #f1 #f2 #f #Hf1 #Hf +cases (at_inv_pxn … Hf1) -Hf1 [ |*: // ] #g1 #Hg1 #H1 +cases (after_inv_nxx … Hf … H1) -Hf #g #Hg #H0 destruct +