From: Ferruccio Guidi Date: Tue, 11 Feb 2014 21:08:30 +0000 (+0000) Subject: some advances on reduction X-Git-Tag: make_still_working~979 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d95bd78c09617ad212fa9e96837a15fc907dcfca;p=helm.git some advances on reduction --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpye.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpye.ma new file mode 100644 index 000000000..a6f0f86bd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpye.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 "basic_2/substitution/cpye_lift.ma". +include "basic_2/reduction/lpx_cpye.ma". +include "basic_2/computation/cpxs_cpxs.ma". +include "basic_2/computation/lpxs.ma". + +(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) + +(* Forward lemmas on evaluation for extended substitution *******************) + +lemma cpx_cpye_fwd_lpxs: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → + ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 → + ∀U1,d,e. ⦃G, L1⦄ ⊢ T1 ▶*[d, e] 𝐍⦃U1⦄ → + ∀U2. ⦃G, L2⦄ ⊢ T2 ▶*[d, e] 𝐍⦃U2⦄ → + ⦃G, L1⦄ ⊢ U1 ➡*[h, g] U2. +#h #g #G #L1 #L2 #H @(lpxs_ind_dx … H) -L1 +[ /3 width=9 by cpx_cpxs, cpx_cpye_fwd_lpx/ +| #L1 #L #HL1 #_ #IHL2 #T1 #T2 #HT12 #U1 #d #e #HTU1 #U2 #HTU2 + elim (cpye_total G L T2 d e) #X2 #HTX2 + lapply (cpx_cpye_fwd_lpx … HT12 … HL1 … HTU1 … HTX2) -T1 + /4 width=9 by lpx_cpxs_trans, cpxs_strap2/ (**) (* full auto too long: 41s *) +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma index 522d36f97..a919045df 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma @@ -20,75 +20,6 @@ include "basic_2/computation/lpxs_cpxs.ma". (* Advanced properties ******************************************************) -fact le_repl_sn_aux: ∀x,y,z:nat. x ≤ z → x = y → y ≤ z. -// qed-. - -axiom cpxs_cpys_conf_lpxs: ∀h,g,G,d,e. - ∀L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡*[h, g] T1 → - ∀T2. ⦃G, L0⦄ ⊢ T0 ▶*[d, e] T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡*[h, g] L1 → - ∃∃T. ⦃G, L1⦄ ⊢ T1 ▶*[d, e] T & ⦃G, L0⦄ ⊢ T2 ➡*[h, g] T. - -axiom cpxs_conf_lpxs_lpys: ∀h,g,G,d,e. - ∀I,L0,V0,T0,T1. ⦃G, L0.ⓑ{I}V0⦄ ⊢ T0 ➡*[h, g] T1 → - ∀L1. ⦃G, L0⦄ ⊢ ➡*[h, g] L1 → ∀V2. ⦃G, L0⦄ ⊢ V0 ▶*[d, e] V2 → - ∃∃T. ⦃G, L1.ⓑ{I}V0⦄ ⊢ T1 ▶*[⫯d, e] T & ⦃G, L0.ⓑ{I}V2⦄ ⊢ T0 ➡*[h, g] T. - - -include "basic_2/reduction/cpx_cpys.ma". - -fact pippo_aux: ∀h,g,G,L1,T,T1,d,e. ⦃G, L1⦄ ⊢ T ▶*[d, e] T1 → e = ∞ → - ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → - ∃∃T2. ⦃G, L2⦄ ⊢ T ▶*[d, e] T2 & ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2 & - L1 ⋕[T, d] L2 ↔ T1 = T2. -#h #g #G #L1 #T #T1 #d #e #H @(cpys_ind_alt … H) -G -L1 -T -T1 -d -e [ * ] -[ /5 width=5 by lpxs_fwd_length, lleq_sort, ex3_intro, conj/ -| #i #G #L1 elim (lt_or_ge i (|L1|)) [2: /6 width=6 by lpxs_fwd_length, lleq_free, le_repl_sn_aux, ex3_intro, conj/ ] - #Hi #d elim (ylt_split i d) [ /5 width=5 by lpxs_fwd_length, lleq_skip, ex3_intro, conj/ ] - #Hdi #e #He #L2 elim (lleq_dec (#i) L1 L2 d) [ /4 width=5 by lpxs_fwd_length, ex3_intro, conj/ ] - #HnL12 #HL12 elim (ldrop_O1_lt L1 i) // -Hi #I #K1 #V1 #HLK1 - elim (lpxs_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 - elim (lpxs_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct - elim (lift_total V2 0 (i+1)) #W2 #HVW2 - @(ex3_intro … W2) /2 width=7 by cpxs_delta, cpys_subst/ -I -K1 -V1 -Hdi - @conj #H [ elim HnL12 // | destruct elim (lift_inv_lref2_be … HVW2) // ] -| /5 width=5 by lpxs_fwd_length, lleq_gref, ex3_intro, conj/ -| #I #G #L1 #K1 #V #V1 #T1 #i #d #e #Hdi #Hide #HLK1 #HV1 #HVT1 #_ #He #L2 #HL12 destruct - elim (lpxs_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 - elim (lpxs_inv_pair1 … H) -H #K2 #W #HK12 #HVW #H destruct - elim (cpxs_cpys_conf_lpxs … HVW … HV1 … HK12) -HVW -HV1 -HK12 #W1 #HW1 #VW1 - elim (lift_total W1 0 (i+1)) #U1 #HWU1 - lapply (ldrop_fwd_drop2 … HLK1) -HLK1 #HLK1 - @(ex3_intro … U1) /2 width=10 by cpxs_lift, cpys_subst/ -| #a #I #G #L #V #V1 #T #T1 #d #e #HV1 #_ #IHV1 #IHT1 #He #L2 #HL12 - elim (IHV1 … HL12) // -IHV1 #V2 #HV2 #HV12 * #H1V #H2V - elim (IHT1 … (L2.ⓑ{I}V2)) /4 width=3 by lpxs_cpx_trans, lpxs_pair, cpys_cpx/ -IHT1 -He #T2 #HT2 #HT12 * #H1T #H2T - elim (cpxs_conf_lpxs_lpys … HT12 … HL12 … HV1) -HT12 -HL12 -HV1 #T0 #HT20 #HT10 - @(ex3_intro … (ⓑ{a,I}V2.T0)) - [ @cpys_bind // @(cpys_trans_eq … T2) /3 width=5 by lsuby_cpys_trans, lsuby_succ/ - | /2 width=1 by cpxs_bind/ - | @conj #H destruct - [ elim (lleq_inv_bind … H) -H #HV #HT >H1V -H1V // - | @lleq_bind /2 width=1/ - - - /3 width=5 by lsuby_cpys_trans, lsuby_succ/ -| #I #G #L #V #V1 #T #T1 #d #e #HV1 #HT1 #IHV1 #IHT1 #He #L2 #HL12 - elim (IHV1 … HL12) // -IHV1 #V2 #HV2 #HV12 * #H1V #H2V - elim (IHT1 … HL12) // -IHT1 #T2 #HT2 #HT12 * #H1T #H2T -He -HL12 - @(ex3_intro … (ⓕ{I}V2.T2)) /2 width=1 by cpxs_flat, cpys_flat/ - @conj #H destruct [2: /3 width=1 by lleq_flat/ ] - elim (lleq_inv_flat … H) -H /3 width=1 by eq_f2/ -] - - - - [ - | @cpxs_bind // - @(lpx_cpxs_trans … HT12) -| -] - axiom lleq_lpxs_trans: ∀h,g,G,L1,L2,T,d. L1 ⋕[T, d] L2 → ∀K2. ⦃G, L2⦄ ⊢ ➡*[h, g] K2 → ∃∃K1. ⦃G, L1⦄ ⊢ ➡*[h, g] K1 & K1 ⋕[T, d] K2. (* diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma index 883e32d0b..791a0e526 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma @@ -12,85 +12,31 @@ (* *) (**************************************************************************) -include "basic_2/computation/lpxs_lleq.ma". +include "basic_2/reduction/cpx_cpys.ma". +include "basic_2/computation/lpxs_cpye.ma". include "basic_2/computation/csx_alt.ma". include "basic_2/computation/lsx_lpxs.ma". (* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) -(* Advanced forward lemmas **************************************************) - -include "basic_2/computation/cpxs_lleq.ma". +(* Advanced properties ******************************************************) +axiom lpxs_cpye_csx_lsx: ∀h,g,G,L1,U. ⦃G, L1⦄ ⊢ ⬊*[h, g] U → + ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ∀T. ⦃G, L2⦄ ⊢ T ▶*[0, ∞] 𝐍⦃U⦄ → + G ⊢ ⋕⬊*[h, g, T] L2. (* -lemma lsx_cpxs_conf: ∀h,g,G,L1,T1,T2. G ⊢ ⋕⬊*[h, g, T1] L1 → - ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2 → - G ⊢ ⋕⬊*[h, g, T2] L2. -#h #g #G #L1 #T1 #T2 #H @(lsx_ind … H) -L1 -#L1 #HL1 #IHL1 #L2 #HL12 #HT12 @lsx_intro -#L3 #HL23 #HnL23 elim (lleq_dec T2 L1 L2 0) [| -HnL23 ] -[ #HT2 @(IHL1 L3) /2 width=3 by lpxs_trans/ - - @(lsx_lpxs_trans … HL23) -| #HnT2 @(lsx_lpxs_trans … HL23) @(IHL1 … L2) // - #HT1 @HnT2 @(lleq_cpxs_conf_dx … HT12) // +#h #g #G #L1 #U #H @(csx_ind_alt … H) -U +#U0 #_ #IHU0 #L0 #HL10 #T #H0 @lsx_intro +#L2 #HL02 #HnT elim (cpye_total G L2 T 0 (∞)) +#U2 #H2 elim (eq_term_dec U0 U2) #H destruct +[ -IHU0 +| -HnT /4 width=9 by lpxs_trans, lpxs_cpxs_trans, cpx_cpye_fwd_lpxs/ ] *) - -lemma lsx_fwd_bind_dx_lpxs: ∀h,g,a,I,G,L1,V1. ⦃G, L1⦄ ⊢ ⬊*[h, g] V1 → - ∀L2,T. G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V1.T] L2 → - ∀V2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L2⦄ ⊢ V1 ➡*[h, g] V2 → - G ⊢ ⋕⬊*[h, g, T] L2.ⓑ{I}V2. -#h #g #a #I #G #L1 #V1 #H @(csx_ind_alt … H) -V1 -#V1 #_ #IHV1 #L2 #T #H @(lsx_ind … H) -L2 -#L2 #HL2 #IHL2 #V2 #HL12 #HV12 @lsx_intro -#Y #H #HnT elim (lpxs_inv_pair1 … H) -H -#L3 #V3 #HL23 #HV23 #H destruct -lapply (lpxs_trans … HL12 … HL23) #HL13 -elim (eq_term_dec V2 V3) -[ (* -HV13 -HL2 -IHV1 -HL12 *) #H destruct - @IHL2 -IHL2 // -HL23 -HL13 /3 width=2 by lleq_fwd_bind_O/ -| -IHL2 -HnT #HnV23 elim (eq_term_dec V1 V2) - [ #H -HV12 destruct - (* @(lsx_lpxs_trans … (L2.ⓑ{I}V2)) /2 width=1 by lpxs_pair/ *) - @(IHV1 … HnV23) -IHV1 -HnV23 /2 width=3 by lpxs_cpxs_trans/ -HL12 -HL13 - @(lsx_lpxs_trans … HL23) - - -lemma lsx_fwd_bind_dx_lpxs: ∀h,g,a,I,G,L1,V. ⦃G, L1⦄ ⊢ ⬊*[h, g] V → - ∀L2,T. G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V.T] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → - G ⊢ ⋕⬊*[h, g, T] L2.ⓑ{I}V. -#h #g #a #I #G #L1 #V #H @(csx_ind_alt … H) -V -#V1 #_ #IHV1 #L2 #T #H @(lsx_ind … H) -L2 -#L2 #HL2 #IHL2 #HL12 @lsx_intro -#Y #H #HnT elim (lpxs_inv_pair1 … H) -H -#L3 #V3 #HL23 #HV13 #H destruct -lapply (lpxs_trans … HL12 … HL23) #HL13 -elim (eq_term_dec V1 V3) -[ -HV13 -HL2 -IHV1 -HL12 #H destruct - @IHL2 -IHL2 // -HL23 -HL13 /3 width=2 by lleq_fwd_bind_O/ -| -IHL2 -HnT #HnV13 - @(IHV1 … HnV13) -IHV1 -HnV13 /2 width=3 by lpxs_cpxs_trans/ -HL12 -HL13 - @(lsx_lpxs_trans … HL23) - - -(* Advanced inversion lemmas ************************************************) - - - (* Main properties **********************************************************) -axiom csx_lsx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → G ⊢ ⋕⬊*[h, g, T] L. -(* -#h #g #G #L #T @(fqup_wf_ind_eq … G L T) -G -L -T -#G1 #L1 #T1 #IH #G2 #L2 * * -[ #k #HG #HL #HT destruct // -| #i #HG #HL #HT destruct - #H -| #p #HG #HL #HT destruct // -| #a #I #V2 #T2 #HG #HL #HT #H destruct - elim (csx_fwd_bind … H) -H - #HV2 #HT2 -| #I #V2 #T2 #HG #HL #HT #H destruct - elim (csx_fwd_flat … H) -H /3 width=1 by lsx_flat/ -*) +lemma csx_lsx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → G ⊢ ⋕⬊*[h, g, T] L. +#h #g #G #L #T #HT elim (cpye_total G L T 0 (∞)) +#U #HTU elim HTU +/4 width=5 by lpxs_cpye_csx_lsx, csx_cpx_trans, cpys_cpx/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpx_cpys.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpx_cpys.etc new file mode 100644 index 000000000..46abd5464 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpx_cpys.etc @@ -0,0 +1,70 @@ +(**************************************************************************) +(* ___ *) +(* ||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/substitution/cpys_alt.ma". +include "basic_2/reduction/cpx.ma". + +(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************) + +(* Properties on context-sensitive extended multiple substitution for terms *) + +lemma cpys_cpx: ∀h,g,G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2. +#h #g #G #L #T1 #T2 #d #e #H @(cpys_ind_alt … H) -G -L -T1 -T2 -d -e +/2 width=7 by cpx_delta, cpx_bind, cpx_flat/ +qed. + +lemma cpy_cpx: ∀h,g,G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2. +/3 width=3 by cpy_cpys, cpys_cpx/ qed. + +lemma cpx_cpy_trans: ∀h,g,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡[h, g] T → + ∀T2,d,e. ⦃G, L⦄ ⊢ T ▶[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2. +#h #g #G #L #T1 #T #H elim H -G -L -T1 -T +[ #I #G #L #X #d #e #H elim (cpy_inv_atom1 … H) // + * /2 width=3 by cpy_cpx/ +| #G #L #k #l #Hkl #X #d #e #H >(cpy_inv_sort1 … H) -X /2 width=2 by cpx_sort/ +| #I #G #L #K #V1 #V #W #i #HLK #_ #HVW #IHV1 #X #d #e #H + lapply (ldrop_fwd_drop2 … HLK) #H0 + lapply (cpy_weak … H 0 (∞) ? ?) -H // #H + elim (cpy_inv_lift1_be … H … H0 … HVW) -H -H0 -HVW + /3 width=7 by cpx_delta/ +| #a #I #G #L #V1 #V #T1 #T #_ #_ #IHV1 #IHT1 #X #d #e #H elim (cpy_inv_bind1 … H) -H + #V2 #T2 #HV2 #HT2 #H destruct + /5 width=7 by cpx_bind, lsuby_cpy_trans, lsuby_succ/ +| #I #G #L #V1 #V #T1 #T #_ #_ #IHV1 #IHT1 #X #d #e #H elim (cpy_inv_flat1 … H) -H + #V2 #T2 #HV2 #HT2 #H destruct /3 width=3 by cpx_flat/ +| #G #L #V1 #U1 #U #T #_ #HTU #IHU1 #T2 #d #e #HT2 + lapply (cpy_weak … HT2 0 (∞) ? ?) -HT2 // #HT2 + elim (lift_total T2 0 1) #U2 #HTU2 + lapply (cpy_lift_be … HT2 (L.ⓓV1) … (Ⓕ) … HTU … HTU2 ? ?) -T + /3 width=3 by cpx_zeta, ldrop_drop/ +| /3 width=3 by cpx_tau/ +| /3 width=3 by cpx_ti/ +| #a #G #L #V1 #V #W1 #W #T1 #T #_ #_ #_ #IHV1 #IHW1 #IHT1 #X #d #e #HX + elim (cpy_inv_bind1 … HX) -HX #Y #T2 #HY #HT2 #H destruct + elim (cpy_inv_flat1 … HY) -HY #W2 #V2 #HW2 #HV2 #H destruct + /5 width=7 by cpx_beta, lsuby_cpy_trans, lsuby_succ/ +| #a #G #L #V1 #V #U #W1 #W #T1 #T #_ #HVU #_ #_ #IHV1 #IHW1 #IHT1 #X #d #e #HX + elim (cpy_inv_bind1 … HX) -HX #W2 #Y #HW2 #HY #H destruct + elim (cpy_inv_flat1 … HY) -HY #U2 #T2 #HU2 #HT2 #H destruct + lapply (cpy_weak … HU2 0 (∞) ? ?) -HU2 // #HU2 + elim (cpy_inv_lift1_be … HU2 L … HVU) -U + /5 width=7 by cpx_theta, lsuby_cpy_trans, lsuby_succ, ldrop_drop/ +] +qed-. + +lemma cpx_cpys_trans: ∀h,g,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡[h, g] T → + ∀T2,d,e. ⦃G, L⦄ ⊢ T ▶*[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2. +#h #g #G #L #T1 #T #HT1 #T2 #d #e #H @(cpys_ind … H) -T2 +/2 width=5 by cpx_cpy_trans/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_cpye.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_cpye.ma new file mode 100644 index 000000000..48816c85d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_cpye.ma @@ -0,0 +1,44 @@ +(**************************************************************************) +(* ___ *) +(* ||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/substitution/cpye_cpye.ma". +include "basic_2/reduction/lpx_cpys.ma". + +axiom cpx_cpys_conf_lpx: ∀h,g,G,d,e. + ∀L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡[h, g] T1 → ∀L1. ⦃G, L0⦄ ⊢ ➡[h, g] L1 → + ∀T2. ⦃G, L0⦄ ⊢ T0 ▶*[d, e] T2 → + ∃∃T. ⦃G, L1⦄ ⊢ T1 ▶*[d, e] T & ⦃G, L0⦄ ⊢ T2 ➡[h, g] T. + +(* SN EXTENDED PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *********************) + +(* Forward lemmas on evaluation for extended substitution *******************) + +lemma cpx_cpys_cpye_fwd_lpx: ∀h,g,G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 → + ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → + ∀U1,d,e. ⦃G, L1⦄ ⊢ T1 ▶*[d, e] U1 → + ∀U2. ⦃G, L2⦄ ⊢ T2 ▶*[d, e] 𝐍⦃U2⦄ → + ⦃G, L1⦄ ⊢ U1 ➡[h, g] U2. +#h #g #G #L1 #T1 #T2 #HT12 #L2 #HL12 #U1 #d #e #HTU1 +elim (cpx_cpys_conf_lpx … HT12 … HL12 … HTU1) -T1 +/3 width=9 by cpx_cpys_trans_lpx, cpye_cpys_conf/ +qed-. + +lemma cpx_cpye_fwd_lpx: ∀h,g,G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 → + ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → + ∀U1,d,e. ⦃G, L1⦄ ⊢ T1 ▶*[d, e] 𝐍⦃U1⦄ → + ∀U2. ⦃G, L2⦄ ⊢ T2 ▶*[d, e] 𝐍⦃U2⦄ → + ⦃G, L1⦄ ⊢ U1 ➡[h, g] U2. +#h #g #G #L1 #T1 #T2 #HT12 #L2 #HL12 #U1 #d #e * +/2 width=9 by cpx_cpys_cpye_fwd_lpx/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_cpys.ma new file mode 100644 index 000000000..d3c490a89 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_cpys.ma @@ -0,0 +1,69 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/cpy_lift.ma". +include "basic_2/substitution/cpys.ma". +include "basic_2/reduction/lpx_ldrop.ma". + +(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) + +(* Properties on context-sensitive extended substitution for terms **********) + +lemma cpx_cpy_trans_lpx: ∀h,g,G,L1,T1,T. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T → + ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → + ∀T2,d,e. ⦃G, L2⦄ ⊢ T ▶[d, e] T2 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2. +#h #g #G #L1 #T1 #T #H elim H -G -L1 -T1 -T +[ #J #G #L1 #L2 #HL12 #T2 #d #e #H elim (cpy_inv_atom1 … H) -H // + * #I #K2 #V2 #i #_ #_ #HLK2 #HVT2 #H destruct + elim (lpx_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H + elim (lpx_inv_pair2 … H) -H #K1 #V1 #_ #HV12 #H destruct + /2 width=7 by cpx_delta/ +| #G #L1 #k #l #Hkl #L2 #_ #X #d #e #H >(cpy_inv_sort1 … H) -X /2 width=2 by cpx_sort/ +| #I #G #L1 #K1 #V1 #V #T #i #HLK1 #_ #HVT #IHV1 #L2 #HL12 #T2 #d #e #HT2 + elim (lpx_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 + elim (lpx_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct + lapply (ldrop_fwd_drop2 … HLK2) -V0 #HLK2 + lapply (cpy_weak … HT2 0 (∞) ? ?) -HT2 // #HT2 + elim (cpy_inv_lift1_be … HT2 … HLK2 … HVT) -HT2 -HLK2 -HVT + /3 width=7 by cpx_delta/ +| #a #I #G #L1 #V1 #V #T1 #T #HV1 #_ #IHV1 #IHT1 #L2 #HL12 #X #d #e #H elim (cpy_inv_bind1 … H) -H + #V2 #T2 #HV2 #HT2 #H destruct /4 width=5 by lpx_pair, cpx_bind/ +| #I #G #L1 #V1 #V #T1 #T #_ #_ #IHV1 #IHT1 #L2 #HL12 #X #d #e #H elim (cpy_inv_flat1 … H) -H + #V2 #T2 #HV2 #HT2 #H destruct /3 width=5 by cpx_flat/ +| #G #L1 #V1 #U1 #U #T #_ #HTU #IHU1 #L2 #HL12 #T2 #d #e #HT2 + lapply (cpy_weak … HT2 0 (∞) ? ?) -HT2 // #HT2 + elim (lift_total T2 0 1) #U2 #HTU2 + lapply (cpy_lift_be … HT2 (L2.ⓓV1) … (Ⓕ) … HTU … HTU2 ? ?) -T + /4 width=5 by cpx_zeta, lpx_pair, ldrop_drop/ +| /3 width=5 by cpx_tau/ +| /3 width=5 by cpx_ti/ +| #a #G #L1 #V1 #V #W1 #W #T1 #T #HV1 #HW1 #_ #IHV1 #IHW1 #IHT1 #L2 #HL12 #X #d #e #HX + elim (cpy_inv_bind1 … HX) -HX #Y #T2 #HY #HT2 #H destruct + elim (cpy_inv_flat1 … HY) -HY #W2 #V2 #HW2 #HV2 #H destruct + /5 width=11 by lpx_pair, cpx_beta, lsuby_cpy_trans, lsuby_succ/ +| #a #G #L1 #V1 #V #U #W1 #W #T1 #T #_ #HVU #HW1 #_ #IHV1 #IHW1 #IHT1 #L2 #HL12 #X #d #e #HX + elim (cpy_inv_bind1 … HX) -HX #W2 #Y #HW2 #HY #H destruct + elim (cpy_inv_flat1 … HY) -HY #U2 #T2 #HU2 #HT2 #H destruct + lapply (cpy_weak … HU2 0 (∞) ? ?) -HU2 // #HU2 + elim (cpy_inv_lift1_be … HU2 L2 … HVU) -U + /4 width=7 by lpx_pair, cpx_theta, ldrop_drop/ +] +qed-. + +lemma cpx_cpys_trans_lpx: ∀h,g,G,L1,T1,T. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T → + ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → + ∀T2,d,e. ⦃G, L2⦄ ⊢ T ▶*[d, e] T2 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2. +#h #g #G #L1 #T1 #T #HT1 #L2 #HL12 #T2 #d #e #H @(cpys_ind … H) -T2 +/2 width=7 by cpx_cpy_trans_lpx/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cny_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/cny_lift.ma index 2d9b36856..213fa6abb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cny_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cny_lift.ma @@ -42,7 +42,7 @@ qed-. (* Inversion lemmas on relocation *******************************************) -lemma cny_lift_inv_le: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄ → ⇩[s, d, e] L ≡ K → +lemma cny_inv_lift_le: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄ → ⇩[s, d, e] L ≡ K → ⇧[d, e] T ≡ U → dt + et ≤ d → ⦃G, K⦄ ⊢ ▶[dt, et] 𝐍⦃T⦄. #G #L #K #T1 #U1 #s #d #dt #e #et #HU1 #HLK #HTU1 #Hdetd #T2 #HT12 elim (lift_total T2 d e) #U2 #HTU2 @@ -50,7 +50,7 @@ lapply (cpy_lift_le … HT12 … HLK … HTU1 … HTU2 ?) // -K -Hdetd #HU12 lapply (HU1 … HU12) -L /2 width=5 by lift_inj/ qed-. -lemma cny_lift_inv_be: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄ → ⇩[s, d, e] L ≡ K → +lemma cny_inv_lift_be: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄ → ⇩[s, d, e] L ≡ K → ⇧[d, e] T ≡ U → dt ≤ d → yinj d + e ≤ dt + et → ⦃G, K⦄ ⊢ ▶[dt, et-e] 𝐍⦃T⦄. #G #L #K #T1 #U1 #s #d #dt #e #et #HU1 #HLK #HTU1 #Hdtd #Hdedet #T2 #HT12 lapply (yle_fwd_plus_ge_inj … Hdedet) // #Heet @@ -61,7 +61,7 @@ lapply (cpy_lift_be … HT12 … HLK … HTU1 … HTU2 ? ?) // [ >yplus_minus_as lapply (HU1 … HU12) -L /2 width=5 by lift_inj/ qed-. -lemma cny_lift_inv_ge: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄ → ⇩[s, d, e] L ≡ K → +lemma cny_inv_lift_ge: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄ → ⇩[s, d, e] L ≡ K → ⇧[d, e] T ≡ U → yinj d + e ≤ dt → ⦃G, K⦄ ⊢ ▶[dt-e, et] 𝐍⦃T⦄. #G #L #K #T1 #U1 #s #d #dt #e #et #HU1 #HLK #HTU1 #Hdedt #T2 #HT12 elim (yle_inv_plus_inj2 … Hdedt) -Hdedt #Hddte #Hedt @@ -71,39 +71,48 @@ lapply (cpy_lift_ge … HT12 … HLK … HTU1 … HTU2 ?) // -K -Hddte lapply (HU1 … HU12) -L /2 width=5 by lift_inj/ qed-. -(* Advanced properties ******************************************************) +(* Advanced inversion lemmas on relocation **********************************) -fact cny_subst_aux: ∀G,L,K,V,W,i,d,e. d ≤ yinj i → i < d + e → - ⇩[i+1] L ≡ K → ⦃G, K⦄ ⊢ ▶[O, ⫰(d+e-i)] 𝐍⦃V⦄ → - ⇧[O, i+1] V ≡ W → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃W⦄. -#G #L #K #V #W #i #d #e #Hdi #Hide #HLK #HV #HVW -lapply (cny_lift_be … HV … HLK … HVW ? ?) // -HV -HLK -HVW -#HW @(cny_narrow … HW) -HW // +lemma cny_inv_lift_ge_up: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄ → ⇩[s, d, e] L ≡ K → + ⇧[d, e] T ≡ U → d ≤ dt → dt ≤ yinj d + e → yinj d + e ≤ dt + et → + ⦃G, K⦄ ⊢ ▶[d, dt + et - (yinj d + e)] 𝐍⦃T⦄. +#G #L #K #T1 #U1 #s #d #dt #e #et #HU1 #HLK #HTU1 #Hddt #Hdtde #Hdedet +lapply (cny_narrow … HU1 (d+e) (dt+et-(d+e)) ? ?) -HU1 [ >ymax_pre_sn_comm ] // #HU1 +lapply (cny_inv_lift_ge … HU1 … HLK … HTU1 ?) // -L -U1 +>yplus_minus_inj // qed-. -lemma cny_subst: ∀I,G,L,K,V,W,i,d,e. d ≤ yinj i → i < d + e → - ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ ▶[O, ⫰(d+e-i)] 𝐍⦃V⦄ → - ⇧[O, i+1] V ≡ W → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃W⦄. -/3 width=13 by cny_subst_aux, ldrop_fwd_drop2/ qed-. - -(* Advanced inversion lemmas ************************************************) - -fact cny_inv_subst_aux: ∀G,L,K,V,W,i,d,e. d ≤ yinj i → i < d + e → - ⇩[i+1] L ≡ K → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃W⦄ → - ⇧[O, i+1] V ≡ W → ⦃G, K⦄ ⊢ ▶[O, ⫰(d+e-i)] 𝐍⦃V⦄. +lemma cny_inv_lift_subst: ∀G,L,K,V,W,i,d,e. d ≤ yinj i → i < d + e → + ⇩[i+1] L ≡ K → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃W⦄ → + ⇧[O, i+1] V ≡ W → ⦃G, K⦄ ⊢ ▶[O, ⫰(d+e-i)] 𝐍⦃V⦄. #G #L #K #V #W #i #d #e #Hdi #Hide #HLK #HW #HVW -lapply (cny_narrow … HW (i+1) (⫰(d+e-i)) ? ?) -HW -[ >yplus_SO2 ylt_inv_O1 - [ >ymax_pre_sn_comm /2 width=2 by ylt_fwd_le/ - | lapply (monotonic_ylt_minus_dx … Hide i ?) // - ] +lapply (cny_inv_lift_ge_up … HW … HLK … HVW ? ? ?) // +>yplus_O1 yplus_SO2 +[ /2 width=1 by ylt_fwd_le_succ1/ | /2 width=3 by yle_trans/ -| #HW lapply (cny_lift_inv_ge … HW … HLK … HVW ?) // -L -W - >yplus_inj >yminus_refl // +| >yminus_succ2 // ] qed-. -lemma cny_inv_subst: ∀I,G,L,K,V,W,i,d,e. d ≤ yinj i → i < d + e → - ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃W⦄ → - ⇧[O, i+1] V ≡ W → ⦃G, K⦄ ⊢ ▶[O, ⫰(d+e-i)] 𝐍⦃V⦄. -/3 width=13 by cny_inv_subst_aux, ldrop_fwd_drop2/ qed-. +(* Advanced properties ******************************************************) + +(* Note: this should be applicable in a forward manner *) +lemma cny_lift_ge_up: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, K⦄ ⊢ ▶[yinj d, dt + et - (yinj d + yinj e)] 𝐍⦃T⦄ → + ⇩[s, d, e] L ≡ K → ⇧[d, e] T ≡ U → + yinj d ≤ dt → dt ≤ yinj d + yinj e → yinj d + yinj e ≤ dt + et → + ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄. +#G #L #K #T1 #U1 #s #d #dt #e #et #HT1 #HLK #HTU1 #Hddt #Hdtde #Hdedet +lapply (cny_lift_be … HT1 … HLK … HTU1 ? ?) // -K -T1 +#HU1 @(cny_narrow … HU1) -HU1 // (**) (* auto fails *) +qed-. + +lemma cny_lift_subst: ∀G,L,K,V,W,i,d,e. d ≤ yinj i → i < d + e → + ⇩[i+1] L ≡ K → ⦃G, K⦄ ⊢ ▶[O, ⫰(d+e-i)] 𝐍⦃V⦄ → + ⇧[O, i+1] V ≡ W → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃W⦄. +#G #L #K #V #W #i #d #e #Hdi #Hide #HLK #HV #HVW +@(cny_lift_ge_up … HLK … HVW) // >yplus_O1 yplus_SO2 +[ >yminus_succ2 // +| /2 width=3 by yle_trans/ +| /2 width=1 by ylt_fwd_le_succ1/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma index 06e4a43c9..66852c667 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma @@ -15,8 +15,6 @@ include "ground_2/ynat/ynat_max.ma". include "basic_2/notation/relations/psubst_6.ma". include "basic_2/grammar/genv.ma". -include "basic_2/grammar/cl_shift.ma". -include "basic_2/relocation/ldrop_append.ma". include "basic_2/relocation/lsuby.ma". (* CONTEXT-SENSITIVE EXTENDED ORDINARY SUBSTITUTION FOR TERMS ***************) @@ -104,37 +102,6 @@ lapply (cpy_weak … HT12 0 (d + e) ? ?) -HT12 /2 width=2 by cpy_weak_top/ qed-. -lemma cpy_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶[dt, et] U2 → - ∀T1,d,e. ⇧[d, e] T1 ≡ U1 → - d ≤ dt → d + e ≤ dt + et → - ∃∃T2. ⦃G, L⦄ ⊢ U1 ▶[d+e, dt+et-(d+e)] U2 & ⇧[d, e] T2 ≡ U2. -#G #L #U1 #U2 #dt #et #H elim H -G -L -U1 -U2 -dt -et -[ * #i #G #L #dt #et #T1 #d #e #H #_ - [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/ - | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by lift_lref_ge_minus, lift_lref_lt, ex2_intro/ - | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by ex2_intro/ - ] -| #I #G #L #K #V #W #i #dt #et #Hdti #Hidet #HLK #HVW #T1 #d #e #H #Hddt #Hdedet - elim (lift_inv_lref2 … H) -H * #Hid #H destruct [ -V -Hidet -Hdedet | -Hdti -Hddt ] - [ elim (ylt_yle_false … Hddt) -Hddt /3 width=3 by yle_ylt_trans, ylt_inj/ - | elim (le_inv_plus_l … Hid) #Hdie #Hei - elim (lift_split … HVW d (i-e+1) ? ? ?) [2,3,4: /2 width=1 by le_S_S, le_S/ ] -Hdie - #T2 #_ >plus_minus // ymax_pre_sn_comm // (**) (* explicit constructor *) - ] -| #a #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #X #d #e #H #Hddt #Hdedet - elim (lift_inv_bind2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct - elim (IHW12 … HVW1) -V1 -IHW12 // - elim (IHU12 … HTU1) -T1 -IHU12 /2 width=1 by yle_succ/ - yplus_SO2 >yplus_succ1 >yplus_succ1 - /3 width=2 by cpy_bind, lift_bind, ex2_intro/ -| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #X #d #e #H #Hddt #Hdedet - elim (lift_inv_flat2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct - elim (IHW12 … HVW1) -V1 -IHW12 // elim (IHU12 … HTU1) -T1 -IHU12 - /3 width=2 by cpy_flat, lift_flat, ex2_intro/ -] -qed-. - lemma cpy_split_up: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶[d, e] T2 → ∀i. i ≤ d + e → ∃∃T. ⦃G, L⦄ ⊢ T1 ▶[d, i-d] T & ⦃G, L⦄ ⊢ T ▶[i, d+e-i] T2. #G #L #T1 #T2 #d #e #H elim H -G -L -T1 -T2 -d -e @@ -173,13 +140,42 @@ lemma cpy_split_down: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶[d, e] T2 → ∀i. ] qed-. -lemma cpy_append: ∀G,d,e. l_appendable_sn … (cpy d e G). -#G #d #e #K #T1 #T2 #H elim H -G -K -T1 -T2 -d -e -/2 width=1 by cpy_atom, cpy_bind, cpy_flat/ -#I #G #K #K0 #V #W #i #d #e #Hdi #Hide #HK0 #HVW #L -lapply (ldrop_fwd_length_lt2 … HK0) #H -@(cpy_subst I … (L@@K0) … HVW) // (**) (* /4/ does not work *) -@(ldrop_O1_append_sn_le … HK0) /2 width=2 by lt_to_le/ +(* Basic forward lemmas *****************************************************) + +lemma cpy_fwd_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶[dt, et] U2 → + ∀T1,d,e. ⇧[d, e] T1 ≡ U1 → + d ≤ dt → d + e ≤ dt + et → + ∃∃T2. ⦃G, L⦄ ⊢ U1 ▶[d+e, dt+et-(d+e)] U2 & ⇧[d, e] T2 ≡ U2. +#G #L #U1 #U2 #dt #et #H elim H -G -L -U1 -U2 -dt -et +[ * #i #G #L #dt #et #T1 #d #e #H #_ + [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/ + | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by lift_lref_ge_minus, lift_lref_lt, ex2_intro/ + | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by ex2_intro/ + ] +| #I #G #L #K #V #W #i #dt #et #Hdti #Hidet #HLK #HVW #T1 #d #e #H #Hddt #Hdedet + elim (lift_inv_lref2 … H) -H * #Hid #H destruct [ -V -Hidet -Hdedet | -Hdti -Hddt ] + [ elim (ylt_yle_false … Hddt) -Hddt /3 width=3 by yle_ylt_trans, ylt_inj/ + | elim (le_inv_plus_l … Hid) #Hdie #Hei + elim (lift_split … HVW d (i-e+1) ? ? ?) [2,3,4: /2 width=1 by le_S_S, le_S/ ] -Hdie + #T2 #_ >plus_minus // ymax_pre_sn_comm // (**) (* explicit constructor *) + ] +| #a #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #X #d #e #H #Hddt #Hdedet + elim (lift_inv_bind2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct + elim (IHW12 … HVW1) -V1 -IHW12 // + elim (IHU12 … HTU1) -T1 -IHU12 /2 width=1 by yle_succ/ + yplus_SO2 >yplus_succ1 >yplus_succ1 + /3 width=2 by cpy_bind, lift_bind, ex2_intro/ +| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #X #d #e #H #Hddt #Hdedet + elim (lift_inv_flat2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct + elim (IHW12 … HVW1) -V1 -IHW12 // elim (IHU12 … HTU1) -T1 -IHU12 + /3 width=2 by cpy_flat, lift_flat, ex2_intro/ +] +qed-. + +lemma cpy_fwd_tw: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶[d, e] T2 → ♯{T1} ≤ ♯{T2}. +#G #L #T1 #T2 #d #e #H elim H -G -L -T1 -T2 -d -e normalize +/3 width=1 by monotonic_le_plus_l, le_plus/ qed-. (* Basic inversion lemmas ***************************************************) @@ -285,33 +281,10 @@ lemma cpy_inv_refl_O2: ∀G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 ▶[d, 0] T2 → T1 = T (* Basic_1: was: subst1_gen_lift_eq *) lemma cpy_inv_lift1_eq: ∀G,T1,U1,d,e. ⇧[d, e] T1 ≡ U1 → ∀L,U2. ⦃G, L⦄ ⊢ U1 ▶[d, e] U2 → U1 = U2. -#G #T1 #U1 #d #e #HTU1 #L #U2 #HU12 elim (cpy_up … HU12 … HTU1) -HU12 -HTU1 +#G #T1 #U1 #d #e #HTU1 #L #U2 #HU12 elim (cpy_fwd_up … HU12 … HTU1) -HU12 -HTU1 /2 width=4 by cpy_inv_refl_O2/ qed-. -(* Basic forward lemmas *****************************************************) - -lemma cpy_fwd_tw: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶[d, e] T2 → ♯{T1} ≤ ♯{T2}. -#G #L #T1 #T2 #d #e #H elim H -G -L -T1 -T2 -d -e normalize -/3 width=1 by monotonic_le_plus_l, le_plus/ -qed-. - -lemma cpy_fwd_shift1: ∀G,L1,L,T1,T,d,e. ⦃G, L⦄ ⊢ L1 @@ T1 ▶[d, e] T → - ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2. -#G #L1 @(lenv_ind_dx … L1) -L1 normalize -[ #L #T1 #T #d #e #HT1 - @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *) -| #I #L1 #V1 #IH #L #T1 #X #d #e - >shift_append_assoc normalize #H - elim (cpy_inv_bind1 … H) -H - #V0 #T0 #_ #HT10 #H destruct - elim (IH … HT10) -IH -HT10 #L2 #T2 #HL12 #H destruct - >append_length >HL12 -HL12 - @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] (**) (* explicit constructor *) - /2 width=3 by trans_eq/ -] -qed-. - (* Basic_1: removed theorems 25: subst0_gen_sort subst0_gen_lref subst0_gen_head subst0_gen_lift_lt subst0_gen_lift_false subst0_gen_lift_ge subst0_refl subst0_trans diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye_cpye.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye_cpye.ma new file mode 100644 index 000000000..42bd19b8e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye_cpye.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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/substitution/cpys_cny.ma". +include "basic_2/substitution/cpys_cpys.ma". +include "basic_2/substitution/cpye.ma". + +(* EVALUATION FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION ON TERMS **********) + +(* Advanced properties ******************************************************) + +lemma cpye_cpys_conf: ∀G,L,T,T2,d,e. ⦃G, L⦄ ⊢ T ▶*[d, e] 𝐍⦃T2⦄ → + ∀T1. ⦃G, L⦄ ⊢ T ▶*[d, e] T1 → ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2. +#G #L #T #T2 #d #e * #H2 #HT2 #T1 #H1 elim (cpys_conf_eq … H1 … H2) -T +#T0 #HT10 #HT20 >(cpys_inv_cny1 … HT2 … HT20) -T2 // +qed-. + \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye_lift.ma index 1d494871c..3c0abe617 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye_lift.ma @@ -25,10 +25,10 @@ lemma cpye_subst: ∀I,G,L,K,V1,V2,W2,i,d,e. d ≤ yinj i → i < d + e → ⇩[i] L ≡ K.ⓑ{I}V1 → ⦃G, K⦄ ⊢ V1 ▶*[O, ⫰(d+e-i)] 𝐍⦃V2⦄ → ⇧[O, i+1] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃W2⦄. #I #G #L #K #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK * -/4 width=13 by cpys_subst, cny_subst_aux, ldrop_fwd_drop2, conj/ +/4 width=13 by cpys_subst, cny_lift_subst, ldrop_fwd_drop2, conj/ qed. -lemma cpys_total: ∀G,L,T1,d,e. ∃T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄. +lemma cpye_total: ∀G,L,T1,d,e. ∃T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄. #G #L #T1 @(fqup_wf_ind_eq … G L T1) -G -L -T1 #Z #Y #X #IH #G #L * * [ #k #HG #HL #HT #d #e destruct -IH /2 width=2 by ex_intro/ @@ -64,7 +64,7 @@ lemma cpye_inv_lref1: ∀G,L,T2,d,e,i. ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃T2⦄ /3 width=1 by or4_intro0, or4_intro1, or4_intro2, conj/ | * #I #K #V1 #V2 #Hdi #Hide #HLK #HV12 #HVT2 @or4_intro3 @(ex5_4_intro … HLK … HVT2) (**) (* explicit constructor *) - /4 width=13 by cny_inv_subst_aux, ldrop_fwd_drop2, conj/ + /4 width=13 by cny_inv_lift_subst, ldrop_fwd_drop2, conj/ ] qed-. @@ -78,16 +78,92 @@ lemma cpye_inv_lref1_free: ∀G,L,T2,d,e,i. ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃ elim (ylt_yle_false … H) // qed-. +lemma cpye_inv_lref1_lget: ∀G,L,T2,d,e,i. ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃T2⦄ → + ∀I,K,V1. ⇩[i] L ≡ K.ⓑ{I}V1 → + ∨∨ d + e ≤ yinj i ∧ T2 = #i + | yinj i < d ∧ T2 = #i + | ∃∃V2. d ≤ yinj i & yinj i < d + e & + ⦃G, K⦄ ⊢ V1 ▶*[yinj 0, ⫰(d+e-yinj i)] 𝐍⦃V2⦄ & + ⇧[O, i+1] V2 ≡ T2. +#G #L #T2 #d #e #i #H #I #K #V1 #HLK elim (cpye_inv_lref1 … H) -H * +[ #H elim (lt_refl_false i) -T2 -d + @(lt_to_le_to_lt … H) -H /2 width=5 by ldrop_fwd_length_lt2/ +| /3 width=1 by or3_intro0, conj/ +| /3 width=1 by or3_intro1, conj/ +| #Z #Y #X1 #X2 #Hdi #Hide #HLY #HX12 #HXT2 + lapply (ldrop_mono … HLY … HLK) -HLY -HLK #H destruct + /3 width=3 by or3_intro2, ex4_intro/ +] +qed-. + +lemma cpye_inv_lref1_subst_ex: ∀G,L,T2,d,e,i. ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃T2⦄ → + ∀I,K,V1. d ≤ yinj i → yinj i < d + e → + ⇩[i] L ≡ K.ⓑ{I}V1 → + ∃∃V2. ⦃G, K⦄ ⊢ V1 ▶*[yinj 0, ⫰(d+e-yinj i)] 𝐍⦃V2⦄ & + ⇧[O, i+1] V2 ≡ T2. +#G #L #T2 #d #e #i #H #I #K #V1 #Hdi #Hide #HLK +elim (cpye_inv_lref1_lget … H … HLK) -H * /2 width=3 by ex2_intro/ +#H elim (ylt_yle_false … H) // +qed-. + lemma cpye_inv_lref1_subst: ∀G,L,T2,d,e,i. ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃T2⦄ → ∀I,K,V1,V2. d ≤ yinj i → yinj i < d + e → ⇩[i] L ≡ K.ⓑ{I}V1 → ⇧[O, i+1] V2 ≡ T2 → ⦃G, K⦄ ⊢ V1 ▶*[yinj 0, ⫰(d+e-yinj i)] 𝐍⦃V2⦄. -#G #L #T2 #d #e #i #H #I #K #V1 #V2 #Hdi #Hide #HLK #HVT2 elim (cpye_inv_lref1 … H) -H * -[ #H elim (lt_refl_false i) -V2 -T2 -d - @(lt_to_le_to_lt … H) -H /2 width=5 by ldrop_fwd_length_lt2/ -|2,3: #H elim (ylt_yle_false … H) // -| #Z #Y #X1 #X2 #_ #_ #HLY #HX12 #HXT2 - lapply (ldrop_mono … HLY … HLK) -HLY -HLK #H destruct - lapply (lift_inj … HXT2 … HVT2) -HXT2 -HVT2 #H destruct // -] +#G #L #T2 #d #e #i #H #I #K #V1 #V2 #Hdi #Hide #HLK #HVT2 +elim (cpye_inv_lref1_subst_ex … H … HLK) -H -HLK // +#X2 #H0 #HXT2 lapply (lift_inj … HXT2 … HVT2) -HXT2 -HVT2 #H destruct // +qed-. + +(* Inversion lemmas on relocation *******************************************) + +lemma cpye_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] 𝐍⦃U2⦄ → + ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → + dt + et ≤ d → + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt, et] 𝐍⦃T2⦄ & ⇧[d, e] T2 ≡ U2. +#G #L #U1 #U2 #dt #et * #HU12 #HU2 #K #s #d #e #HLK #T1 #HTU1 #Hdetd +elim (cpys_inv_lift1_le … HU12 … HLK … HTU1) -U1 // #T2 #HT12 #HTU2 +lapply (cny_inv_lift_le … HU2 … HLK … HTU2 ?) -L +/3 width=3 by ex2_intro, conj/ +qed-. + +lemma cpye_inv_lift1_be: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] 𝐍⦃U2⦄ → + ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → + dt ≤ d → yinj d + e ≤ dt + et → + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt, et - e] 𝐍⦃T2⦄ & ⇧[d, e] T2 ≡ U2. +#G #L #U1 #U2 #dt #et * #HU12 #HU2 #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hdedet +elim (cpys_inv_lift1_be … HU12 … HLK … HTU1) -U1 // #T2 #HT12 #HTU2 +lapply (cny_inv_lift_be … HU2 … HLK … HTU2 ? ?) -L +/3 width=3 by ex2_intro, conj/ +qed-. + +lemma cpye_inv_lift1_ge: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] 𝐍⦃U2⦄ → + ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → + yinj d + e ≤ dt → + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt - e, et] 𝐍⦃T2⦄ & ⇧[d, e] T2 ≡ U2. +#G #L #U1 #U2 #dt #et * #HU12 #HU2 #K #s #d #e #HLK #T1 #HTU1 #Hdedt +elim (cpys_inv_lift1_ge … HU12 … HLK … HTU1) -U1 // #T2 #HT12 #HTU2 +lapply (cny_inv_lift_ge … HU2 … HLK … HTU2 ?) -L +/3 width=3 by ex2_intro, conj/ +qed-. + +lemma cpye_inv_lift1_ge_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] 𝐍⦃U2⦄ → + ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → + d ≤ dt → dt ≤ yinj d + e → yinj d + e ≤ dt + et → + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[d, dt + et - (yinj d + e)] 𝐍⦃T2⦄ & + ⇧[d, e] T2 ≡ U2. +#G #L #U1 #U2 #dt #et * #HU12 #HU2 #K #s #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet +elim (cpys_inv_lift1_ge_up … HU12 … HLK … HTU1) -U1 // #T2 #HT12 #HTU2 +lapply (cny_inv_lift_ge_up … HU2 … HLK … HTU2 ? ? ?) -L +/3 width=3 by ex2_intro, conj/ +qed-. + +lemma cpye_inv_lift1_subst: ∀G,L,W1,W2,d,e. ⦃G, L⦄ ⊢ W1 ▶*[d, e] 𝐍⦃W2⦄ → + ∀K,V1,i. ⇩[i+1] L ≡ K → ⇧[O, i+1] V1 ≡ W1 → + d ≤ yinj i → i < d + e → + ∃∃V2. ⦃G, K⦄ ⊢ V1 ▶*[O, ⫰(d+e-i)] 𝐍⦃V2⦄ & ⇧[O, i+1] V2 ≡ W2. +#G #L #W1 #W2 #d #e * #HW12 #HW2 #K #V1 #i #HLK #HVW1 #Hdi #Hide +elim (cpys_inv_lift1_subst … HW12 … HLK … HVW1) -W1 // #V2 #HV12 #HVW2 +lapply (cny_inv_lift_subst … HLK HW2 HVW2) -L +/3 width=3 by ex2_intro, conj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma index 422c56878..10c59120d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma @@ -95,20 +95,23 @@ lemma cpys_weak_full: ∀G,L,T1,T2,d,e. /3 width=5 by cpys_strap1, cpy_weak_full/ qed-. -lemma cpys_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 → - ∀T1,d,e. ⇧[d, e] T1 ≡ U1 → - d ≤ dt → d + e ≤ dt + et → - ∃∃T2. ⦃G, L⦄ ⊢ U1 ▶*[d+e, dt+et-(d+e)] U2 & ⇧[d, e] T2 ≡ U2. +(* Basic forward lemmas *****************************************************) + +lemma cpys_fwd_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 → + ∀T1,d,e. ⇧[d, e] T1 ≡ U1 → + d ≤ dt → d + e ≤ dt + et → + ∃∃T2. ⦃G, L⦄ ⊢ U1 ▶*[d+e, dt+et-(d+e)] U2 & ⇧[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #H #T1 #d #e #HTU1 #Hddt #Hdedet @(cpys_ind … H) -U2 [ /2 width=3 by ex2_intro/ | -HTU1 #U #U2 #_ #HU2 * #T #HU1 #HTU - elim (cpy_up … HU2 … HTU) -HU2 -HTU /3 width=3 by cpys_strap1, ex2_intro/ + elim (cpy_fwd_up … HU2 … HTU) -HU2 -HTU /3 width=3 by cpys_strap1, ex2_intro/ ] qed-. -lemma cpys_append: ∀G,d,e. l_appendable_sn … (cpys d e G). -#G #d #e #K #T1 #T2 #H @(cpys_ind … H) -T2 -/3 width=3 by cpys_strap1, cpy_append/ +lemma cpys_fwd_tw: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 → ♯{T1} ≤ ♯{T2}. +#G #L #T1 #T2 #d #e #H @(cpys_ind … H) -T2 // +#T #T2 #_ #HT2 #IHT1 lapply (cpy_fwd_tw … HT2) -HT2 +/2 width=3 by transitive_le/ qed-. (* Basic inversion lemmas ***************************************************) @@ -161,21 +164,3 @@ lemma cpys_inv_lift1_eq: ∀G,L,U1,U2. ∀d,e:nat. #G #L #U1 #U2 #d #e #H #T1 #HTU1 @(cpys_ind … H) -U2 /2 width=7 by cpy_inv_lift1_eq/ qed-. - -(* Basic forward lemmas *****************************************************) - -lemma cpys_fwd_tw: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 → ♯{T1} ≤ ♯{T2}. -#G #L #T1 #T2 #d #e #H @(cpys_ind … H) -T2 // -#T #T2 #_ #HT2 #IHT1 lapply (cpy_fwd_tw … HT2) -HT2 -/2 width=3 by transitive_le/ -qed-. - -lemma cpys_fwd_shift1: ∀G,L,L1,T1,T,d,e. ⦃G, L⦄ ⊢ L1 @@ T1 ▶*[d, e] T → - ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2. -#G #L #L1 #T1 #T #d #e #H @(cpys_ind … H) -T -[ /2 width=4 by ex2_2_intro/ -| #T #X #_ #HX * #L0 #T0 #HL10 #H destruct - elim (cpy_fwd_shift1 … HX) -HX #L2 #T2 #HL02 #H destruct - /2 width=4 by ex2_2_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cny.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cny.ma new file mode 100644 index 000000000..1499ceea5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cny.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/cny.ma". +include "basic_2/substitution/cpys.ma". + +(* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************) + +(* Inversion lemmas on normality for extended substitution ******************) + +lemma cpys_inv_cny1: ∀G,L,T1,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃T1⦄ → + ∀T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 → T1 = T2. +#G #L #T1 #d #e #HT1 #T2 #H @(cpys_ind … H) -T2 // +#T #T2 #_ #HT2 #IHT1 destruct <(HT1 … HT2) -T // +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma index eaccf49f7..b6d9e45a1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma @@ -203,3 +203,16 @@ lemma cpys_inv_lift1_le_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U elim (cpy_inv_lift1_le_up … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/ ] qed-. + +lemma cpys_inv_lift1_subst: ∀G,L,W1,W2,d,e. ⦃G, L⦄ ⊢ W1 ▶*[d, e] W2 → + ∀K,V1,i. ⇩[i+1] L ≡ K → ⇧[O, i+1] V1 ≡ W1 → + d ≤ yinj i → i < d + e → + ∃∃V2. ⦃G, K⦄ ⊢ V1 ▶*[O, ⫰(d+e-i)] V2 & ⇧[O, i+1] V2 ≡ W2. +#G #L #W1 #W2 #d #e #HW12 #K #V1 #i #HLK #HVW1 #Hdi #Hide +elim (cpys_inv_lift1_ge_up … HW12 … HLK … HVW1 ? ? ?) // +>yplus_O1 yplus_SO2 +[ >yminus_succ2 /2 width=3 by ex2_intro/ +| /2 width=1 by ylt_fwd_le_succ1/ +| /2 width=3 by yle_trans/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma index 6bce82987..72a5346ce 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma @@ -66,7 +66,7 @@ lemma lleq_be: ∀L1,L2,U,dt. L1 ⋕[U, dt] L2 → ∀T,d,e. ⇧[d, e] T ≡ U d ≤ dt → dt ≤ d + e → L1 ⋕[U, d] L2. #L1 #L2 #U #dt * #HL12 #IH #T #d #e #HTU #Hddt #Hdtde @conj // -HL12 #U0 elim (IH U0) -IH #H12 #H21 @conj -#HU0 elim (cpys_up … HU0 … HTU) // -HU0 /4 width=5 by cpys_weak/ +#HU0 elim (cpys_fwd_up … HU0 … HTU) // -HU0 /4 width=5 by cpys_weak/ qed-. lemma lsuby_lleq_trans: ∀L2,L,T,d. L2 ⋕[T, d] L → diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_cpye.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_cpye.ma new file mode 100644 index 000000000..e6890e637 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_cpye.ma @@ -0,0 +1,49 @@ +(**************************************************************************) +(* ___ *) +(* ||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/substitution/cpye_lift.ma". +include "basic_2/substitution/lleq_alt.ma". + +(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) + +(* Forward lemmas on evaluation for extended substitution *******************) + +lemma lleq_fwd_cpye: ∀L1,L2,T,d. L1 ⋕[T, d] L2 → ∀G,T1. ⦃G, L1⦄ ⊢ T ▶*[d, ∞] 𝐍⦃T1⦄ → + ∀T2. ⦃G, L2⦄ ⊢ T ▶*[d, ∞] 𝐍⦃T2⦄ → T1 = T2. +#L1 #L2 #T #d #H @(lleq_ind_alt … H) -L1 -L2 -T -d +[ #L1 #L2 #d #k #_ #G #T1 #H1 #T2 #H2 + >(cpye_inv_sort1 … H1) -H1 >(cpye_inv_sort1 … H2) -H2 // +| #L1 #L2 #d #i #_ #Hid #G #T1 #H1 #T2 #H2 + >(cpye_inv_lref1_free … H1) -H1 [ >(cpye_inv_lref1_free … H2) -H2 ] + /2 width=1 by or3_intro2/ +| #I1 #I2 #L1 #L2 #K1 #K2 #V #d #i #Hdi #HLK1 #HLK2 #_ #IHV #G #T1 #H1 #T2 #H2 + elim (cpye_inv_lref1_subst_ex … H1 … HLK1) -H1 -HLK1 // + elim (cpye_inv_lref1_subst_ex … H2 … HLK2) -H2 -HLK2 // + >yminus_Y_inj #V2 #HV2 #HVT2 #V1 #HV1 #HVT1 + lapply (IHV … HV1 … HV2) -IHV -HV1 -HV2 #H destruct /2 width=5 by lift_mono/ +| #L1 #L2 #d #i #_ #HL1 #HL2 #G #T1 #H1 #T2 #H2 + >(cpye_inv_lref1_free … H1) -H1 [ >(cpye_inv_lref1_free … H2) -H2 ] + /2 width=1 by or3_intro0/ +| #L1 #L2 #d #p #_ #G #T1 #H1 #T2 #H2 + >(cpye_inv_gref1 … H1) -H1 >(cpye_inv_gref1 … H2) -H2 // +| #a #I #L1 #L2 #V #T #d #_ #_ #IHV #IHT #G #X1 #H1 #X2 #H2 + elim (cpye_inv_bind1 … H1) -H1 #V1 #T1 #HV1 #HT1 #H destruct + elim (cpye_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct + /3 width=3 by eq_f2/ +| #I #L1 #L2 #V #T #d #_ #_ #IHV #IHT #G #X1 #H1 #X2 #H2 + elim (cpye_inv_flat1 … H1) -H1 #V1 #T1 #HV1 #HT1 #H destruct + elim (cpye_inv_flat1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct + /3 width=3 by eq_f2/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 7dccdcc14..6d4072800 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -105,7 +105,7 @@ table { } ] [ { "context-sensitive extended computation" * } { - [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? )" "lpxs_ldrop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] + [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? )" "lpxs_ldrop" + "lpxs_cpye" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ] } ] @@ -135,7 +135,7 @@ table { } ] [ { "context-sensitive extended reduction" * } { - [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_lleq" + "lpx_aaa" * ] + [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_cpys" + "lpx_cpye" + "lpx_lleq" + "lpx_aaa" * ] [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_lift" + "cpx_cpys" + "cpx_lleq" + "cpx_cix" * ] } ] @@ -209,15 +209,15 @@ table { class "yellow" [ { "substitution" * } { [ { "lazy equivalence for local environments" * } { - [ "lleq ( ? ⋕[?,?] ? )" "lleq_alt ( ? ⋕⋕[?,?] ? )" "lleq_ldrop" + "lleq_fqus" + "lleq_lleq" + "lleq_ext" * ] + [ "lleq ( ? ⋕[?,?] ? )" "lleq_alt ( ? ⋕⋕[?,?] ? )" "lleq_ldrop" + "lleq_fqus" + "lleq_cpye" + "lleq_lleq" + "lleq_ext" * ] } ] [ { "evaluation for contxt-sensitive extended substitution" * } { - [ "cpye ( ⦃?,?⦄ ⊢ ? ▶*[?,?] 𝐍⦃?⦄ )" "cpye_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] 𝐍⦃?⦄ )" "cpye_lift" * ] + [ "cpye ( ⦃?,?⦄ ⊢ ? ▶*[?,?] 𝐍⦃?⦄ )" "cpye_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] 𝐍⦃?⦄ )" "cpye_lift" + "cpye_cpye" * ] } ] [ { "contxt-sensitive extended multiple substitution" * } { - [ "cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )" "cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )" "cpys_lift" + "cpys_cpys" * ] + [ "cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )" "cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )" "cpys_lift" + "cpys_cny" + "cpys_cpys" * ] } ] [ { "iterated structural successor for closures" * } { diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma index 0cbcff85e..832195fe9 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma @@ -52,6 +52,9 @@ lemma arith_i: ∀x,y,z. y < x → x+z-y-1 = x-y-1+z. (* Properties ***************************************************************) +fact le_repl_sn_aux: ∀x,y,z:nat. x ≤ z → x = y → y ≤ z. +// qed-. + lemma monotonic_le_minus_l2: ∀x1,x2,y,z. x1 ≤ x2 → x1 - y - z ≤ x2 - y - z. /3 width=1 by monotonic_le_minus_l/ qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma index d30d6229d..a306b5756 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma @@ -98,8 +98,12 @@ lemma ylt_fwd_succ2: ∀m,n. m < ⫯n → m ≤ n. (* inversion and forward lemmas on yle **************************************) +lemma ylt_fwd_le_succ1: ∀m,n. m < n → ⫯m ≤ n. +#m #n * -m -n /2 width=1 by yle_inj/ +qed-. + lemma ylt_fwd_le: ∀m:ynat. ∀n:ynat. m < n → m ≤ n. -#m #n * -m -n /3 width=1 by yle_pred_sn, yle_inj, yle_Y/ +#m #n * -m -n /3 width=1 by lt_to_le, yle_inj/ qed-. lemma ylt_yle_false: ∀m:ynat. ∀n:ynat. m < n → n ≤ m → ⊥. @@ -125,7 +129,7 @@ lemma ylt_O_succ: ∀n. 0 < ⫯n. qed. lemma ylt_succ: ∀m,n. m < n → ⫯m < ⫯n. -#m #n #H elim H -m -n /3 width=1 by ylt_inj, le_S_S/ +#m #n #H elim H -m -n /3 width=1 by ylt_inj, le_S_S/ qed. (* Properties on order ******************************************************)