From: Ferruccio Guidi Date: Sun, 16 Feb 2014 18:59:26 +0000 (+0000) Subject: - improved definition of lsx allows more invariants X-Git-Tag: make_still_working~977 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5f1066ffb3c6ed53f9bf17ae2a81a9c9db32dba7;p=helm.git - improved definition of lsx allows more invariants - some additions - we parked some unnecessary planes (cny, cpye) --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpys.ma new file mode 100644 index 000000000..881030572 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpys.ma @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reduction/cpx_cpys.ma". +include "basic_2/computation/cpxs.ma". + +(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) + +(* Properties on local environment refinement for extended substitution *****) + +lemma lsuby_cpxs_trans: ∀h,g,G. lsub_trans … (cpxs h g G) (lsuby 0 (∞)). +/3 width=5 by lsuby_cpx_trans, LTC_lsub_trans/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpye.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpye.ma deleted file mode 100644 index a6f0f86bd..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpye.ma +++ /dev/null @@ -1,36 +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/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 a919045df..2ca1e193d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma @@ -12,32 +12,23 @@ (* *) (**************************************************************************) -include "basic_2/substitution/lleq_ext.ma". +include "basic_2/reduction/lpx_lleq.ma". +include "basic_2/computation/cpxs_cpys.ma". include "basic_2/computation/lpxs_ldrop.ma". include "basic_2/computation/lpxs_cpxs.ma". (* SN EXTENDED PARALLEL COMPUTATION FOR LOCAL ENVIRONMENTS ******************) -(* Advanced properties ******************************************************) +(* Properties on lazy equivalence for local environments ********************) -axiom lleq_lpxs_trans: ∀h,g,G,L1,L2,T,d. L1 ⋕[T, d] L2 → ∀K2. ⦃G, L2⦄ ⊢ ➡*[h, g] K2 → +lemma lleq_lpxs_trans: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡*[h, g] K2 → + ∀L1,T,d. L1 ⋕[T, d] L2 → ∃∃K1. ⦃G, L1⦄ ⊢ ➡*[h, g] K1 & K1 ⋕[T, d] K2. -(* -#h #g #G #L1 #L2 #T #d #H @(lleq_ind_alt … H) -L1 -L2 -T -d -[ -| -| -| -| -| #a #I #L1 #L2 #V #T #d #_ #_ #IHV #IHT #K2 #HLK2 - elim (IHV … HLK2) -IHV #KV #HLKV #HV - elim (IHT (K2.ⓑ{I}V)) -IHT /2 width=1 by lpxs_pair_refl/ -HLK2 #Y #H #HT - elim (lpxs_inv_pair1 … H) -H #KT #VT #HLKT #_ #H destruct - -#h #g #G #L1 #L2 #T #d * #HL12 #IH #K2 #HLK2 -*) - -(* Properties on lazy equivalence for local environments ********************) +#h #g #G #L2 #K2 #H @(lpxs_ind … H) -K2 /2 width=3 by ex2_intro/ +#K #K2 #_ #HK2 #IH #L1 #T #d #HT elim (IH … HT) -L2 +#L #HL1 #HT elim (lleq_lpx_trans … HK2 … HT) -K +/3 width=3 by lpxs_strap1, ex2_intro/ +qed-. lemma lpxs_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 → @@ -101,3 +92,37 @@ elim (fqus_inv_gen … H) -H | * #HG #HL #HT destruct /2 width=4 by ex3_intro/ ] qed-. + +fact lsuby_lpxs_trans_lleq_aux: ∀h,g,G,L1,L0,d,e. L1 ⊑×[d, e] L0 → e = ∞ → + ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, g] L2 → + ∃∃L. L ⊑×[d, e] L2 & ⦃G, L1⦄ ⊢ ➡*[h, g] L & + (∀T. |L1| = |L0| → |L| = |L2| → L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L). +#h #g #G #L1 #L0 #d #e #H elim H -L1 -L0 -d -e +[ #L1 #d #e #_ #L2 #H >(lpxs_inv_atom1 … H) -H + /3 width=5 by ex3_intro, conj/ +| #I1 #I0 #L1 #L0 #V1 #V0 #_ #_ #He destruct +| #I1 #I0 #L1 #L0 #V1 #e #HL10 #IHL10 #He #Y #H + elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct + lapply (ysucc_inv_Y_dx … He) -He #He + elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH + @(ex3_intro … (L.ⓑ{I1}V2)) /3 width=3 by lpxs_pair, lsuby_cpxs_trans, lsuby_pair/ + #T #H1 #H2 lapply (injective_plus_l … H1) lapply (injective_plus_l … H2) -H1 -H2 + #H1 #H2 elim (IH T) // #HL0dx #HL0sn + @conj #H @(lleq_lsuby_repl … H) -H normalize + /3 width=1 by lsuby_sym, lsuby_pair_O_Y/ +| #I1 #I0 #L1 #L0 #V1 #V0 #d #e #HL10 #IHL10 #He #Y #H + elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct + elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH + @(ex3_intro … (L.ⓑ{I1}V1)) /3 width=1 by lpxs_pair, lsuby_succ/ + #T #H1 #H2 lapply (injective_plus_l … H1) lapply (injective_plus_l … H2) -H1 -H2 + #H1 #H2 elim (IH T) // #HL0dx #HL0sn + @conj #H @(lleq_lsuby_repl … H) -H + /3 width=1 by lsuby_sym, lsuby_succ/ normalize // +] +qed-. + +lemma lsuby_lpxs_trans_lleq: ∀h,g,G,L1,L0,d. L1 ⊑×[d, ∞] L0 → + ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, g] L2 → + ∃∃L. L ⊑×[d, ∞] L2 & ⦃G, L1⦄ ⊢ ➡*[h, g] L & + (∀T. |L1| = |L0| → |L| = |L2| → L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L). +/2 width=1 by lsuby_lpxs_trans_lleq_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma index 38e185a86..9661a8839 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma @@ -12,86 +12,86 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/lazysn_5.ma". +include "basic_2/notation/relations/lazysn_6.ma". include "basic_2/substitution/lleq.ma". include "basic_2/computation/lpxs.ma". (* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) -definition lsx: ∀h. sd h → relation3 term genv lenv ≝ - λh,g,T,G. SN … (lpxs h g G) (lleq 0 T). +definition lsx: ∀h. sd h → relation4 ynat term genv lenv ≝ + λh,g,d,T,G. SN … (lpxs h g G) (lleq d T). interpretation "extended strong normalization (local environment)" - 'LazySN h g T G L = (lsx h g T G L). + 'LazySN h g d T G L = (lsx h g T d G L). (* Basic eliminators ********************************************************) -lemma lsx_ind: ∀h,g,T,G. ∀R:predicate lenv. - (∀L1. G ⊢ ⋕⬊*[h, g, T] L1 → - (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T, 0] L2 → ⊥) → R L2) → +lemma lsx_ind: ∀h,g,G,T,d. ∀R:predicate lenv. + (∀L1. G ⊢ ⋕⬊*[h, g, T, d] L1 → + (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T, d] L2 → ⊥) → R L2) → R L1 ) → - ∀L. G ⊢ ⋕⬊*[h, g, T] L → R L. -#h #g #T #G #R #H0 #L1 #H elim H -L1 + ∀L. G ⊢ ⋕⬊*[h, g, T, d] L → R L. +#h #g #G #T #d #R #H0 #L1 #H elim H -L1 /5 width=1 by lleq_sym, SN_intro/ qed-. (* Basic properties *********************************************************) -lemma lsx_intro: ∀h,g,T,G,L1. - (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T, 0] L2 → ⊥) → G ⊢ ⋕⬊*[h, g, T] L2) → - G ⊢ ⋕⬊*[h, g, T] L1. +lemma lsx_intro: ∀h,g,G,L1,T,d. + (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T, d] L2 → ⊥) → G ⊢ ⋕⬊*[h, g, T, d] L2) → + G ⊢ ⋕⬊*[h, g, T, d] L1. /5 width=1 by lleq_sym, SN_intro/ qed. -lemma lsx_atom: ∀h,g,T,G. G ⊢ ⋕⬊*[h, g, T] ⋆. -#h #g #T #G @lsx_intro +lemma lsx_atom: ∀h,g,G,T,d. G ⊢ ⋕⬊*[h, g, T, d] ⋆. +#h #g #G #T #d @lsx_intro #X #H #HT lapply (lpxs_inv_atom1 … H) -H #H destruct elim HT -HT // qed. -lemma lsx_sort: ∀h,g,G,L,k. G ⊢ ⋕⬊*[h, g, ⋆k] L. -#h #g #G #L1 #k @lsx_intro +lemma lsx_sort: ∀h,g,G,L,d,k. G ⊢ ⋕⬊*[h, g, ⋆k, d] L. +#h #g #G #L1 #d #k @lsx_intro #L2 #HL12 #H elim H -H /3 width=4 by lpxs_fwd_length, lleq_sort/ qed. -lemma lsx_gref: ∀h,g,G,L,p. G ⊢ ⋕⬊*[h, g, §p] L. -#h #g #G #L1 #p @lsx_intro +lemma lsx_gref: ∀h,g,G,L,d,p. G ⊢ ⋕⬊*[h, g, §p, d] L. +#h #g #G #L1 #d #p @lsx_intro #L2 #HL12 #H elim H -H /3 width=4 by lpxs_fwd_length, lleq_gref/ qed. (* Basic forward lemmas *****************************************************) -lemma lsx_fwd_bind_sn: ∀h,g,a,I,G,L,V,T. G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V.T] L → - G ⊢ ⋕⬊*[h, g, V] L. -#h #g #a #I #G #L #V #T #H @(lsx_ind … H) -L +lemma lsx_fwd_bind_sn: ∀h,g,a,I,G,L,V,T,d. G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V.T, d] L → + G ⊢ ⋕⬊*[h, g, V, d] L. +#h #g #a #I #G #L #V #T #d #H @(lsx_ind … H) -L #L1 #_ #IHL1 @lsx_intro #L2 #HL12 #HV @IHL1 /3 width=4 by lleq_fwd_bind_sn/ qed-. -lemma lsx_fwd_flat_sn: ∀h,g,I,G,L,V,T. G ⊢ ⋕⬊*[h, g, ⓕ{I}V.T] L → - G ⊢ ⋕⬊*[h, g, V] L. -#h #g #I #G #L #V #T #H @(lsx_ind … H) -L +lemma lsx_fwd_flat_sn: ∀h,g,I,G,L,V,T,d. G ⊢ ⋕⬊*[h, g, ⓕ{I}V.T, d] L → + G ⊢ ⋕⬊*[h, g, V, d] L. +#h #g #I #G #L #V #T #d #H @(lsx_ind … H) -L #L1 #_ #IHL1 @lsx_intro #L2 #HL12 #HV @IHL1 /3 width=3 by lleq_fwd_flat_sn/ qed-. -lemma lsx_fwd_flat_dx: ∀h,g,I,G,L,V,T. G ⊢ ⋕⬊*[h, g, ⓕ{I}V.T] L → - G ⊢ ⋕⬊*[h, g, T] L. -#h #g #I #G #L #V #T #H @(lsx_ind … H) -L +lemma lsx_fwd_flat_dx: ∀h,g,I,G,L,V,T,d. G ⊢ ⋕⬊*[h, g, ⓕ{I}V.T, d] L → + G ⊢ ⋕⬊*[h, g, T, d] L. +#h #g #I #G #L #V #T #d #H @(lsx_ind … H) -L #L1 #_ #IHL1 @lsx_intro #L2 #HL12 #HV @IHL1 /3 width=3 by lleq_fwd_flat_dx/ qed-. -lemma lsx_fwd_pair_sn: ∀h,g,I,G,L,V,T. G ⊢ ⋕⬊*[h, g, ②{I}V.T] L → - G ⊢ ⋕⬊*[h, g, V] L. +lemma lsx_fwd_pair_sn: ∀h,g,I,G,L,V,T,d. G ⊢ ⋕⬊*[h, g, ②{I}V.T, d] L → + G ⊢ ⋕⬊*[h, g, V, d] L. #h #g * /2 width=4 by lsx_fwd_bind_sn, lsx_fwd_flat_sn/ qed-. (* Basic inversion lemmas ***************************************************) -lemma lsx_inv_flat: ∀h,g,I,G,L,V,T. G ⊢ ⋕⬊*[h, g, ⓕ{I}V.T] L → - G ⊢ ⋕⬊*[h, g, V] L ∧ G ⊢ ⋕⬊*[h, g, T] L. +lemma lsx_inv_flat: ∀h,g,I,G,L,V,T,d. G ⊢ ⋕⬊*[h, g, ⓕ{I}V.T, d] L → + G ⊢ ⋕⬊*[h, g, V, d] L ∧ G ⊢ ⋕⬊*[h, g, T, d] L. /3 width=3 by lsx_fwd_flat_sn, lsx_fwd_flat_dx, conj/ qed-. 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 791a0e526..edde17495 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma @@ -12,6 +12,51 @@ (* *) (**************************************************************************) +include "basic_2/reduction/cpx_cpys.ma". +include "basic_2/computation/lpxs_llneq.ma". +include "basic_2/computation/csx_alt.ma". +include "basic_2/computation/lsx_lpxs.ma". + +(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) + +(* Advanced properties ******************************************************) + +lemma lpxs_cpys_csx_lsx: ∀h,g,G,L1,U. ⦃G, L1⦄ ⊢ ⬊*[h, g] U → + ∀T. ⦃G, L1⦄ ⊢ T ▶*[0, ∞] U → + G ⊢ ⋕⬊*[h, g, T] L1. +#h #g #G #L1 #U #H @(csx_ind_alt … H) -U +#U #_ #IHU #T #HTU @lsx_intro +#L2 #HL02 #HnT elim (lpxs_nlleq_fwd_cpxs … HL02 HnT) -HnT +#U0 #U2 #H0 #H2 #HU02 #HnU02 elim (cpys_conf_eq … HTU … H0) +#X #HUX #H0X elim (eq_term_dec U X) #HnUX destruct +[ -HUX +| -HnU02 @(lsx_lpxs_trans … HL02) @(IHU … HnUX) + [ /3 width=3 by cpys_cpx, cpx_cpxs/ + | /2 width=3 by cpys_trans_eq/ + ] +] + +lemma lpxs_cpys_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. +#h #g #G #L1 #U #H @(csx_ind_alt … H) -U +#U #_ #IHU #L0 #HL10 #T #HTU @lsx_intro +#L2 #HL02 #HnT elim (lpxs_nlleq_fwd_cpxs … HL02 HnT) -HnT +#U0 #U2 #H0 #H2 #HU02 #HnU02 elim (cpys_conf_eq … HTU … H0) +#X #HUX #H0X elim (eq_term_dec U X) #HnUX destruct +[ -HUX +| -HnU02 @(IHU … HnUX) + + +-HnT /4 width=9 by lpxs_trans, lpxs_cpxs_trans, cpx_cpye_fwd_lpxs/ +] + + + + + + + include "basic_2/reduction/cpx_cpys.ma". include "basic_2/computation/lpxs_cpye.ma". include "basic_2/computation/csx_alt.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma index 1f1ebc834..2130d8b51 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma @@ -20,35 +20,89 @@ include "basic_2/computation/lsx.ma". (* Advanced properties ******************************************************) -lemma lsx_lleq_trans: ∀h,g,T,G,L1. G ⊢ ⋕⬊*[h, g, T] L1 → - ∀L2. L1 ⋕[T, 0] L2 → G ⊢ ⋕⬊*[h, g, T] L2. -#h #g #T #G #L1 #H @(lsx_ind … H) -L1 +lemma lsx_leqy_conf: ∀h,g,G,L1,T,d. G ⊢ ⋕⬊*[h, g, T, d] L1 → + ∀L2. L1 ⊑×[d, ∞] L2 → |L1| = |L2| → G ⊢ ⋕⬊*[h, g, T, d] L2. +#h #g #G #L1 #T #d #H @(lsx_ind … H) -L1 +#L1 #_ #IHL1 #L2 #H1L12 #H2L12 @lsx_intro +#L3 #H1L23 #HnL23 lapply (lpxs_fwd_length … H1L23) +#H2L23 elim (lsuby_lpxs_trans_lleq … H1L12 … H1L23) -H1L12 -H1L23 +#L0 #H1L03 #H1L10 #H lapply (lpxs_fwd_length … H1L10) +#H2L10 elim (H T) -H // +#_ #H @(IHL1 … H1L10) -IHL1 -H1L10 /3 width=1 by/ +qed-. + +lemma lsx_lleq_trans: ∀h,g,T,G,L1,d. G ⊢ ⋕⬊*[h, g, T, d] L1 → + ∀L2. L1 ⋕[T, d] L2 → G ⊢ ⋕⬊*[h, g, T, d] L2. +#h #g #T #G #L1 #d #H @(lsx_ind … H) -L1 #L1 #_ #IHL1 #L2 #HL12 @lsx_intro -#K2 #HLK2 #HnLK2 elim (lleq_lpxs_trans … HL12 … HLK2) -HLK2 +#K2 #HLK2 #HnLK2 elim (lleq_lpxs_trans … HLK2 … HL12) -HLK2 /5 width=4 by lleq_canc_sn, lleq_trans/ qed-. -lemma lsx_lpxs_trans: ∀h,g,T,G,L1. G ⊢ ⋕⬊*[h, g, T] L1 → - ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → G ⊢ ⋕⬊*[h, g, T] L2. -#h #g #T #G #L1 #H @(lsx_ind … H) -L1 #L1 #HL1 #IHL1 #L2 #HL12 -elim (lleq_dec T L1 L2 0) /3 width=4 by lsx_lleq_trans/ +lemma lsx_lpxs_trans: ∀h,g,T,G,L1,d. G ⊢ ⋕⬊*[h, g, T, d] L1 → + ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → G ⊢ ⋕⬊*[h, g, T, d] L2. +#h #g #T #G #L1 #d #H @(lsx_ind … H) -L1 #L1 #HL1 #IHL1 #L2 #HL12 +elim (lleq_dec T L1 L2 d) /3 width=4 by lsx_lleq_trans/ +qed-. + +fact lsx_bind_lpxs_aux: ∀h,g,a,I,G,L1,V,d. G ⊢ ⋕⬊*[h, g, V, d] L1 → + ∀Y,T. G ⊢ ⋕⬊*[h, g, T, ⫯d] Y → + ∀L2. Y = L2.ⓑ{I}V → ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → + G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V.T, d] L2. +#h #g #a #I #G #L1 #V #d #H @(lsx_ind … H) -L1 +#L1 #HL1 #IHL1 #Y #T #H @(lsx_ind … H) -Y +#Y #HY #IHY #L2 #H #HL12 destruct @lsx_intro +#L0 #HL20 lapply (lpxs_trans … HL12 … HL20) +#HL10 #H elim (nlleq_inv_bind … H) -H [ -HL1 -IHY | -HY -IHL1 ] +[ #HnV elim (lleq_dec V L1 L2 d) + [ #HV @(IHL1 … L0) /3 width=5 by lsx_lpxs_trans, lpxs_pair, lleq_canc_sn/ (**) (* full auto too slow *) + | -HnV -HL10 /4 width=5 by lsx_lpxs_trans, lpxs_pair/ + ] +| /3 width=4 by lpxs_pair/ +] qed-. -lemma lsx_flat_lpxs: ∀h,g,I,G,L1,V. G ⊢ ⋕⬊*[h, g, V] L1 → - ∀L2,T. G ⊢ ⋕⬊*[h, g, T] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → - G ⊢ ⋕⬊*[h, g, ⓕ{I}T.V] L2. -#h #g #I #G #L1 #V #H @(lsx_ind … H) -L1 +lemma lsx_bind: ∀h,g,a,I,G,L,V,d. G ⊢ ⋕⬊*[h, g, V, d] L → + ∀T. G ⊢ ⋕⬊*[h, g, T, ⫯d] L.ⓑ{I}V → + G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V.T, d] L. +/2 width=3 by lsx_bind_lpxs_aux/ qed. + +lemma lsx_flat_lpxs: ∀h,g,I,G,L1,V,d. G ⊢ ⋕⬊*[h, g, V, d] L1 → + ∀L2,T. G ⊢ ⋕⬊*[h, g, T, d] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → + G ⊢ ⋕⬊*[h, g, ⓕ{I}V.T, d] L2. +#h #g #I #G #L1 #V #d #H @(lsx_ind … H) -L1 #L1 #HL1 #IHL1 #L2 #T #H @(lsx_ind … H) -L2 #L2 #HL2 #IHL2 #HL12 @lsx_intro #L0 #HL20 lapply (lpxs_trans … HL12 … HL20) -#HL10 #H elim (nlleq_inv_flat … H) -H [ -HL2 -IHL1 | -HL1 -IHL2 ] -[ /3 width=1 by/ -| #HnV elim (lleq_dec V L1 L2 0) +#HL10 #H elim (nlleq_inv_flat … H) -H [ -HL1 -IHL2 | -HL2 -IHL1 ] +[ #HnV elim (lleq_dec V L1 L2 d) [ #HV @(IHL1 … L0) /3 width=3 by lsx_lpxs_trans, lleq_canc_sn/ (**) (* full auto too slow: 47s *) | -HnV -HL10 /3 width=4 by lsx_lpxs_trans/ + ] +| /3 width=1 by/ ] qed-. -lemma lsx_flat: ∀h,g,I,G,L,V. G ⊢ ⋕⬊*[h, g, V] L → - ∀T. G ⊢ ⋕⬊*[h, g, T] L → G ⊢ ⋕⬊*[h, g, ⓕ{I}T.V] L. +lemma lsx_flat: ∀h,g,I,G,L,V,d. G ⊢ ⋕⬊*[h, g, V, d] L → + ∀T. G ⊢ ⋕⬊*[h, g, T, d] L → G ⊢ ⋕⬊*[h, g, ⓕ{I}V.T, d] L. /2 width=3 by lsx_flat_lpxs/ qed. + +(* Advanced forward lemmas **************************************************) + +lemma lsx_fwd_bind_dx: ∀h,g,a,I,G,L,V,T,d. G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V.T, d] L → + G ⊢ ⋕⬊*[h, g, T, ⫯d] L.ⓑ{I}V. +#h #g #a #I #G #L #V1 #T #d #H @(lsx_ind … H) -L +#L1 #_ #IHL1 @lsx_intro +#Y #H #HT elim (lpxs_inv_pair1 … H) -H +#L2 #V2 #HL12 #_ #H destruct +@(lsx_leqy_conf … (L2.ⓑ{I}V1)) /2 width=1 by lsuby_succ/ +@IHL1 // #H @HT -IHL1 -HL12 -HT +@(lleq_lsuby_trans … (L2.ⓑ{I}V1)) +/2 width=2 by lleq_fwd_bind_dx, lsuby_succ/ +qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma lsx_inv_bind: ∀h,g,a,I,G,L,V,T,d. G ⊢ ⋕⬊*[h, g, ⓑ{a, I}V.T, d] L → + G ⊢ ⋕⬊*[h, g, V, d] L ∧ G ⊢ ⋕⬊*[h, g, T, ⫯d] L.ⓑ{I}V. +/3 width=4 by lsx_fwd_bind_sn, lsx_fwd_bind_dx, conj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cny.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cny.etc new file mode 100644 index 000000000..81919dc4b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cny.etc @@ -0,0 +1,114 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/relations/psubstnormal_5.ma". +include "basic_2/relocation/cpy.ma". + +(* NORMAL TERMS FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION *****************) + +definition cny: ∀d,e. relation3 genv lenv term ≝ + λd,e,G,L. NF … (cpy d e G L) (eq …). + +interpretation + "normality for context-sensitive extended substitution (term)" + 'PSubstNormal G L T d e = (cny d e G L T). + +(* Basic inversion lemmas ***************************************************) + +lemma cny_inv_lref: ∀G,L,d,e,i. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄ → + ∨∨ yinj i < d | d + e ≤ yinj i | |L| ≤ i. +#G #L #d #e #i #H elim (ylt_split i d) /2 width=1 by or3_intro0/ +#Hdi elim (ylt_split i (d+e)) /2 width=1 by or3_intro1/ +#Hide elim (lt_or_ge i (|L|)) /2 width=1 by or3_intro2/ +#Hi elim (ldrop_O1_lt L i) // +#I #K #V #HLK elim (lift_total V 0 (i+1)) +#W #HVW lapply (H W ?) -H /2 width=5 by cpy_subst/ -HLK +#H destruct elim (lift_inv_lref2_be … HVW) -L -d -e // +qed-. + +lemma cny_inv_bind: ∀a,I,G,L,V,T,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓑ{a,I}V.T⦄ → + ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ ▶[⫯d, e] 𝐍⦃T⦄. +#a #I #G #L #V1 #T1 #d #e #HVT1 @conj +[ #V2 #HV2 lapply (HVT1 (ⓑ{a,I}V2.T1) ?) -HVT1 +| #T2 #HT2 lapply (HVT1 (ⓑ{a,I}V1.T2) ?) -HVT1 +] +/2 width=1 by cpy_bind/ #H destruct // +qed-. + +lemma cny_inv_flat: ∀I,G,L,V,T,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓕ{I}V.T⦄ → + ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ ∧ ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃T⦄. +#I #G #L #V1 #T1 #d #e #HVT1 @conj +[ #V2 #HV2 lapply (HVT1 (ⓕ{I}V2.T1) ?) -HVT1 +| #T2 #HT2 lapply (HVT1 (ⓕ{I}V1.T2) ?) -HVT1 +] +/2 width=1 by cpy_flat/ #H destruct // +qed-. + +(* Basic properties *********************************************************) + +lemma lsuby_cny_conf: ∀G,d,e. + ∀L1,T. ⦃G, L1⦄ ⊢ ▶[d, e] 𝐍⦃T⦄ → + ∀L2. L1 ⊑×[d, e] L2 → ⦃G, L2⦄ ⊢ ▶[d, e] 𝐍⦃T⦄. +#G #d #e #L1 #T1 #HT1 #L2 #HL12 #T2 #HT12 +@HT1 /3 width=3 by lsuby_cpy_trans/ +qed-. + +lemma cny_sort: ∀G,L,d,e,k. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃⋆k⦄. +#G #L #d #e #k #X #H elim (cpy_inv_sort1 … H) -H // +qed. + +lemma cny_lref_free: ∀G,L,d,e,i. |L| ≤ i → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄. +#G #L #d #e #i #Hi #X #H elim (cpy_inv_lref1 … H) -H // * +#I #K #V #_ #_ #HLK #_ lapply (ldrop_fwd_length_lt2 … HLK) -HLK +#H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/ +qed. + +lemma cny_lref_atom: ∀G,L,d,e,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄. +#G #L #d #e #i #HL @cny_lref_free >(ldrop_fwd_length … HL) -HL // +qed. + +lemma cny_lref_top: ∀G,L,d,e,i. d+e ≤ yinj i → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄. +#G #L #d #e #i #Hdei #X #H elim (cpy_inv_lref1 … H) -H // * +#I #K #V #_ #H elim (ylt_yle_false … H) // +qed. + +lemma cny_lref_skip: ∀G,L,d,e,i. yinj i < d → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄. +#G #L #d #e #i #Hid #X #H elim (cpy_inv_lref1 … H) -H // * +#I #K #V #H elim (ylt_yle_false … H) // +qed. + +lemma cny_gref: ∀G,L,d,e,p. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃§p⦄. +#G #L #d #e #p #X #H elim (cpy_inv_gref1 … H) -H // +qed. + +lemma cny_bind: ∀G,L,V,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ → + ∀I,T. ⦃G, L.ⓑ{I}V⦄ ⊢ ▶[⫯d, e] 𝐍⦃T⦄ → + ∀a. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓑ{a,I}V.T⦄. +#G #L #V1 #d #e #HV1 #I #T1 #HT1 #a #X #H +elim (cpy_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct +>(HV1 … HV12) -V2 >(HT1 … HT12) -T2 // +qed. + +lemma cny_flat: ∀G,L,V,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ → + ∀T. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃T⦄ → + ∀I. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓕ{I}V.T⦄. +#G #L #V1 #d #e #HV1 #T1 #HT1 #I #X #H +elim (cpy_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct +>(HV1 … HV12) -V2 >(HT1 … HT12) -T2 // +qed. + +lemma cny_narrow: ∀G,L,T,d1,e1. ⦃G, L⦄ ⊢ ▶[d1, e1] 𝐍⦃T⦄ → + ∀d2,e2. d1 ≤ d2 → d2 + e2 ≤ d1 + e1 → ⦃G, L⦄ ⊢ ▶[d2, e2] 𝐍⦃T⦄. +#G #L #T1 #d1 #e1 #HT1 #d2 #e2 #Hd12 #Hde21 #T2 #HT12 +@HT1 /2 width=5 by cpy_weak/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cny_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cny_lift.etc new file mode 100644 index 000000000..213fa6abb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cny_lift.etc @@ -0,0 +1,118 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/cny.ma". + +(* NORMAL TERMS FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION *****************) + +(* Properties on relocation *************************************************) + +lemma cny_lift_le: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, K⦄ ⊢ ▶[dt, et] 𝐍⦃T⦄ → ⇩[s, d, e] L ≡ K → + ⇧[d, e] T ≡ U → dt + et ≤ d → ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄. +#G #L #K #T1 #U1 #s #d #dt #e #et #HT1 #HLK #HTU1 #Hdetd #U2 #HU12 +elim (cpy_inv_lift1_le … HU12 … HLK … HTU1) // -L -Hdetd #T2 #HT12 +>(HT1 … HT12) -K /2 width=5 by lift_mono/ +qed-. + +lemma cny_lift_be: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, K⦄ ⊢ ▶[dt, et] 𝐍⦃T⦄ → ⇩[s, d, e] L ≡ K → + ⇧[d, e] T ≡ U → dt ≤ d → yinj d ≤ dt + et → ⦃G, L⦄ ⊢ ▶[dt, et+e] 𝐍⦃U⦄. +#G #L #K #T1 #U1 #s #d #dt #e #et #HT1 #HLK #HTU1 #Hdtd #Hddet #U2 #HU12 +elim (cpy_inv_lift1_be … HU12 … HLK … HTU1) /2 width=1 by monotonic_yle_plus_dx/ -L -Hdtd -Hddet #T2 +>yplus_minus_inj #HT12 >(HT1 … HT12) -K /2 width=5 by lift_mono/ +qed-. + +lemma cny_lift_ge: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, K⦄ ⊢ ▶[dt, et] 𝐍⦃T⦄ → ⇩[s, d, e] L ≡ K → + ⇧[d, e] T ≡ U → d ≤ dt → ⦃G, L⦄ ⊢ ▶[dt+e, et] 𝐍⦃U⦄. +#G #L #K #T1 #U1 #s #d #dt #e #et #HT1 #HLK #HTU1 #Hddt #U2 #HU12 +elim (cpy_inv_lift1_ge … HU12 … HLK … HTU1) /2 width=1 by monotonic_yle_plus_dx/ -L -Hddt #T2 +>yplus_minus_inj #HT12 >(HT1 … HT12) -K /2 width=5 by lift_mono/ +qed-. + +(* Inversion lemmas on relocation *******************************************) + +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 +lapply (cpy_lift_le … HT12 … HLK … HTU1 … HTU2 ?) // -K -Hdetd #HU12 +lapply (HU1 … HU12) -L /2 width=5 by lift_inj/ +qed-. + +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 +elim (yle_inv_plus_inj2 … Hdedet) -Hdedet #Hddete #Hedet +elim (lift_total T2 d e) #U2 #HTU2 +lapply (cpy_lift_be … HT12 … HLK … HTU1 … HTU2 ? ?) // [ >yplus_minus_assoc_inj // ] -K -Hdtd -Hddete +>ymax_pre_sn // -Heet #HU12 +lapply (HU1 … HU12) -L /2 width=5 by lift_inj/ +qed-. + +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 +elim (lift_total T2 d e) #U2 #HTU2 +lapply (cpy_lift_ge … HT12 … HLK … HTU1 … HTU2 ?) // -K -Hddte +>ymax_pre_sn // -Hedt #HU12 +lapply (HU1 … HU12) -L /2 width=5 by lift_inj/ +qed-. + +(* Advanced inversion lemmas on relocation **********************************) + +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_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_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/ +| >yminus_succ2 // +] +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/etc/cny/cpx_cpzs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpx_cpzs.etc new file mode 100644 index 000000000..6c208d51b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpx_cpzs.etc @@ -0,0 +1,73 @@ +(**************************************************************************) +(* ___ *) +(* ||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/delta_equivalence/cpzs.ma". +include "basic_2/reduction/cpx.ma". + +fact destruct_tsort_tsort: ∀k1,k2. ⋆k1 = ⋆k2 → k1 = k2. +#k1 #k2 #H destruct // +qed-. + +axiom cpzs_inv_subst: ∀I,G,L,K,V1,V2,W2,i. + ⇩[i] L ≡ K.ⓑ{I}V1 → ⇧[O, i+1] V2 ≡ W2 → + ⦃G, L⦄ ⊢ #i ◆*[O, ∞] W2 → ⦃G, K⦄⊢ V1 ◆*[O, ∞] V2. + +axiom cpzs_subst: ∀I,G,L,K,V1,V2,W2,i. + ⇩[i] L ≡ K.ⓑ{I}V1 → ⇧[O, i+1] V2 ≡ W2 → + ⦃G, K⦄⊢ V1 ◆*[O, ∞] V2 → ⦃G, L⦄ ⊢ #i ◆*[O, ∞] W2. + +(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************) + +(* Forward lemmas on delta-equivalence for terms ****************************) + +lemma cpx_fwd_cpys_cpzs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → + ∀d,e. ⦃G, L⦄ ⊢ T1 ◆*[d, e] T2 ↔ ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2. +#h #g #G #L #T1 #T2 #H elim H -G -L -T1 -T2 +[ /2 width=1 by conj/ +| #G #L #k #l #_ #d #e @conj #H lapply (next_lt h k) + [ <(cpzs_inv_sort … H) + | lapply (cpys_inv_sort1 … H) -H #H >(destruct_tsort_tsort … H) + ] -H #H elim (lt_refl_false … H) +| #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #d #e @conj #H +(* + [ @(cpys_subst … HLK … HVW2) // >yminus_Y_inj /3 width=7 by cpzs_inv_subst/ + | elim (cpys_inv_lref1_ldrop … H … HLK … HVW2) -H /3 width=7 by cpzs_subst/ + ] +*) +| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e + elim (IHV12 d e) -IHV12 elim (IHT12 (⫯d) e) -IHT12 + #IHTdx #IHTsn #IHVdx #IHVsn @conj #H + [ elim (cpzs_inv_bind … H) -H /3 width=1 by cpys_bind/ + | elim (cpys_inv_bind1 … H) -H #X1 #X2 #H1 #H2 #H destruct /3 width=1 by cpzs_bind/ + ] +| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e + elim (IHV12 d e) -IHV12 elim (IHT12 (d) e) -IHT12 + #IHTdx #IHTsn #IHVdx #IHVsn @conj #H + [ elim (cpzs_inv_flat … H) -H /3 width=1 by cpys_flat/ + | elim (cpys_inv_flat1 … H) -H #X1 #X2 #H1 #H2 #H destruct /3 width=1 by cpzs_flat/ + ] +| #G #L #V #U1 #U2 #T2 #_ #HTU2 #_ #d #e @conj #H +| #G #L #V1 #T1 #T2 #_ #_ #d #e @conj #H +| #G #L #V1 #V2 #T1 #HV12 #_ #d #e @conj #H +| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #d #e @conj #H + [ elim (cpzs_inv_flat_bind … H) + | elim (cpys_inv_flat1 … H) -H #X1 #X2 #H1 #H2 #H destruct + ] +| #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #d #e @conj #H + [ elim (cpzs_inv_flat_bind … H) + | elim (cpys_inv_flat1 … H) -H #X1 #X2 #H1 #H2 #H destruct + ] +] + + \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpye.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpye.etc new file mode 100644 index 000000000..71e06ea72 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpye.etc @@ -0,0 +1,89 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/relations/psubsteval_6.ma". +include "basic_2/relocation/cny.ma". +include "basic_2/substitution/cpys.ma". + +(* EVALUATION FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION ON TERMS **********) + +definition cpye: ynat → ynat → relation4 genv lenv term term ≝ + λd,e,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 ∧ ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃T2⦄. + +interpretation "evaluation for context-sensitive extended substitution (term)" + 'PSubstEval G L T1 T2 d e = (cpye d e G L T1 T2). + +(* Basic_properties *********************************************************) + +(* Note: this should go in subconversion *) +lemma leqy_cpye_trans: ∀G,L2,T1,T2,d,e. ⦃G, L2⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄ → + ∀L1. L1 ⊑×[d, e] L2 → L2 ⊑×[d, e] L1 → ⦃G, L1⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄. +#G #L2 #T1 #T2 #d #e * +/4 width=8 by lsuby_cpys_trans, lsuby_cny_conf, conj/ +qed-. + +lemma cpye_sort: ∀G,L,d,e,k. ⦃G, L⦄ ⊢ ⋆k ▶*[d, e] 𝐍⦃⋆k⦄. +/3 width=5 by cny_sort, conj/ qed. + +lemma cpye_free: ∀G,L,d,e,i. |L| ≤ i → ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃#i⦄. +/3 width=6 by cny_lref_free, conj/ qed. + +lemma cpye_top: ∀G,L,d,e,i. d + e ≤ yinj i → ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃#i⦄. +/3 width=6 by cny_lref_top, conj/ qed. + +lemma cpye_skip: ∀G,L,d,e,i. yinj i < d → ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃#i⦄. +/3 width=6 by cny_lref_skip, conj/ qed. + +lemma cpye_gref: ∀G,L,d,e,p. ⦃G, L⦄ ⊢ §p ▶*[d, e] 𝐍⦃§p⦄. +/3 width=5 by cny_gref, conj/ qed. + +lemma cpye_bind: ∀G,L,V1,V2,d,e. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ → + ∀I,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*[⫯d, e] 𝐍⦃T2⦄ → + ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*[d, e] 𝐍⦃ⓑ{a,I}V2.T2⦄. +#G #L #V1 #V2 #d #e * #HV12 #HV2 #I #T1 #T2 * +/5 width=8 by cpys_bind, cny_bind, lsuby_cny_conf, lsuby_succ, conj/ +qed. + +lemma cpye_flat: ∀G,L,V1,V2,d,e. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ → + ∀T1,T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄ → + ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ▶*[d, e] 𝐍⦃ⓕ{I}V2.T2⦄. +#G #L #V1 #V2 #d #e * #HV12 #HV2 #T1 #T2 * +/3 width=7 by cpys_flat, cny_flat, conj/ +qed. + +(* Basic inversion lemmas ***************************************************) + +lemma cpye_inv_sort1: ∀G,L,X,d,e,k. ⦃G, L⦄ ⊢ ⋆k ▶*[d, e] 𝐍⦃X⦄ → X = ⋆k. +#G #L #X #d #e #k * /2 width=5 by cpys_inv_sort1/ +qed-. + +lemma cpye_inv_gref1: ∀G,L,X,d,e,p. ⦃G, L⦄ ⊢ §p ▶*[d, e] 𝐍⦃X⦄ → X = §p. +#G #L #X #d #e #p * /2 width=5 by cpys_inv_gref1/ +qed-. + +lemma cpye_inv_bind1: ∀a,I,G,L,V1,T1,X,d,e. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*[d, e] 𝐍⦃X⦄ → + ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*[⫯d, e] 𝐍⦃T2⦄ & + X = ⓑ{a,I}V2.T2. +#a #I #G #L #V1 #T1 #X #d #e * #H1 #H2 elim (cpys_inv_bind1 … H1) -H1 +#V2 #T2 #HV12 #HT12 #H destruct elim (cny_inv_bind … H2) -H2 +/5 width=8 by lsuby_cny_conf, lsuby_succ, ex3_2_intro, conj/ +qed-. + +lemma cpye_inv_flat1: ∀I,G,L,V1,T1,X,d,e. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ▶*[d, e] 𝐍⦃X⦄ → + ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ & ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄ & + X = ⓕ{I}V2.T2. +#I #G #L #V1 #T1 #X #d #e * #H1 #H2 elim (cpys_inv_flat1 … H1) -H1 +#V2 #T2 #HV12 #HT12 #H destruct elim (cny_inv_flat … H2) -H2 +/3 width=5 by ex3_2_intro, conj/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpye_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpye_alt.etc new file mode 100644 index 000000000..a9dc53cf5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpye_alt.etc @@ -0,0 +1,89 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/relations/psubstevalalt_6.ma". +include "basic_2/substitution/cpye_lift.ma". + +(* EVALUATION FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION ON TERMS **********) + +(* Note: alternative definition of cpye *) +inductive cpyea: ynat → ynat → relation4 genv lenv term term ≝ +| cpyea_sort : ∀G,L,d,e,k. cpyea d e G L (⋆k) (⋆k) +| cpyea_free : ∀G,L,d,e,i. |L| ≤ i → cpyea d e G L (#i) (#i) +| cpyea_top : ∀G,L,d,e,i. d + e ≤ yinj i → cpyea d e G L (#i) (#i) +| cpyea_skip : ∀G,L,d,e,i. yinj i < d → cpyea d e G L (#i) (#i) +| cpyea_subst: ∀I,G,L,K,V1,V2,W2,i,d,e. d ≤ yinj i → yinj i < d+e → + ⇩[i] L ≡ K.ⓑ{I}V1 → cpyea (yinj 0) (⫰(d+e-yinj i)) G K V1 V2 → + ⇧[0, i+1] V2 ≡ W2 → cpyea d e G L (#i) W2 +| cpyea_gref : ∀G,L,d,e,p. cpyea d e G L (§p) (§p) +| cpyea_bind : ∀a,I,G,L,V1,V2,T1,T2,d,e. + cpyea d e G L V1 V2 → cpyea (⫯d) e G (L.ⓑ{I}V1) T1 T2 → + cpyea d e G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2) +| cpyea_flat : ∀I,G,L,V1,V2,T1,T2,d,e. + cpyea d e G L V1 V2 → cpyea d e G L T1 T2 → + cpyea d e G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) +. + +interpretation + "evaluation for context-sensitive extended substitution (term) alternative" + 'PSubstEvalAlt G L T1 T2 d e = (cpyea d e G L T1 T2). + +(* Main properties **********************************************************) + +theorem cpye_cpyea: ∀G,L,T1,T2,d,e. ⦃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 #_ #_ #_ #T2 #d #e #H -X -Y -Z >(cpye_inv_sort1 … H) -H // +| #i #HG #HL #HT #T2 #d #e #H destruct + elim (cpye_inv_lref1 … H) -H * + /4 width=7 by cpyea_subst, cpyea_free, cpyea_top, cpyea_skip, fqup_lref/ +| #p #_ #_ #_ #T2 #d #e #H -X -Y -Z >(cpye_inv_gref1 … H) -H // +| #a #I #V1 #T1 #HG #HL #HT #T #d #e #H destruct + elim (cpye_inv_bind1 … H) -H /3 width=1 by cpyea_bind/ +| #I #V1 #T1 #HG #HL #HT #T #d #e #H destruct + elim (cpye_inv_flat1 … H) -H /3 width=1 by cpyea_flat/ +] +qed. + +(* Main inversion properties ************************************************) + +theorem cpyea_inv_cpye: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶▶*[d, e] 𝐍⦃T2⦄ → ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄. +#G #L #T1 #T2 #d #e #H elim H -G -L -T1 -T2 -d -e +/2 width=7 by cpye_subst, cpye_flat, cpye_bind, cpye_skip, cpye_top, cpye_free/ +qed-. + +(* Advanced eliminators *****************************************************) + +lemma cpye_ind_alt: ∀R:ynat→ynat→relation4 genv lenv term term. + (∀G,L,d,e,k. R d e G L (⋆k) (⋆k)) → + (∀G,L,d,e,i. |L| ≤ i → R d e G L (#i) (#i)) → + (∀G,L,d,e,i. d + e ≤ yinj i → R d e G L (#i) (#i)) → + (∀G,L,d,e,i. yinj i < d → R d e G L (#i) (#i)) → + (∀I,G,L,K,V1,V2,W2,i,d,e. d ≤ yinj i → yinj i < d + e → + ⇩[i] L ≡ K.ⓑ{I}V1 → ⦃G, K⦄ ⊢ V1 ▶*[yinj O, ⫰(d+e-yinj i)] 𝐍⦃V2⦄ → + ⇧[O, i+1] V2 ≡ W2 → R (yinj O) (⫰(d+e-yinj i)) G K V1 V2 → R d e G L (#i) W2 + ) → + (∀G,L,d,e,p. R d e G L (§p) (§p)) → + (∀a,I,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ → + ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*[⫯d, e] 𝐍⦃T2⦄ → R d e G L V1 V2 → + R (⫯d) e G (L.ⓑ{I}V1) T1 T2 → R d e G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2) + ) → + (∀I,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ → + ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄ → R d e G L V1 V2 → + R d e G L T1 T2 → R d e G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) + ) → + ∀d,e,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄ → R d e G L T1 T2. +#R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #d #e #G #L #T1 #T2 #H elim (cpye_cpyea … H) -G -L -T1 -T2 -d -e +/3 width=8 by cpyea_inv_cpye/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpye_cpye.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpye_cpye.etc new file mode 100644 index 000000000..42bd19b8e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpye_cpye.etc @@ -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/etc/cny/cpye_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpye_lift.etc new file mode 100644 index 000000000..3c0abe617 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpye_lift.etc @@ -0,0 +1,169 @@ +(**************************************************************************) +(* ___ *) +(* ||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_lift.ma". +include "basic_2/substitution/fqup.ma". +include "basic_2/substitution/cpys_lift.ma". +include "basic_2/substitution/cpye.ma". + +(* EVALUATION FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION ON TERMS **********) + +(* Advanced properties ******************************************************) + +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_lift_subst, ldrop_fwd_drop2, conj/ +qed. + +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/ +| #i #HG #HL #HT #d #e destruct + elim (ylt_split i d) /3 width=2 by cpye_skip, ex_intro/ + elim (ylt_split i (d+e)) /3 width=2 by cpye_top, ex_intro/ + elim (lt_or_ge i (|L|)) /3 width=2 by cpye_free, ex_intro/ + #Hi #Hide #Hdi elim (ldrop_O1_lt L i) // -Hi + #I #K #V1 #HLK elim (IH G K V1 … 0 (⫰(d+e-i))) -IH /2 width=2 by fqup_lref/ + #V2 elim (lift_total V2 0 (i+1)) /3 width=8 by ex_intro, cpye_subst/ +| #p #HG #HL #HT #d #e destruct -IH /2 width=2 by ex_intro/ +| #a #I #V1 #T1 #HG #HL #HT #d #e destruct + elim (IH G L V1 … d e) // elim (IH G (L.ⓑ{I}V1) T1 … (⫯d) e) // + /3 width=2 by cpye_bind, ex_intro/ +| #I #V1 #T1 #HG #HL #HT #d #e destruct + elim (IH G L V1 … d e) // elim (IH G L T1 … d e) // + /3 width=2 by cpye_flat, ex_intro/ +] +qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma cpye_inv_lref1: ∀G,L,T2,d,e,i. ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃T2⦄ → + ∨∨ |L| ≤ i ∧ T2 = #i + | d + e ≤ yinj i ∧ T2 = #i + | yinj i < d ∧ T2 = #i + | ∃∃I,K,V1,V2. d ≤ yinj i & yinj i < d + e & + ⇩[i] L ≡ K.ⓑ{I}V1 & + ⦃G, K⦄ ⊢ V1 ▶*[yinj 0, ⫰(d+e-yinj i)] 𝐍⦃V2⦄ & + ⇧[O, i+1] V2 ≡ T2. +#G #L #T2 #i #d #e * #H1 #H2 elim (cpys_inv_lref1 … H1) -H1 +[ #H destruct elim (cny_inv_lref … H2) -H2 + /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_lift_subst, ldrop_fwd_drop2, conj/ +] +qed-. + +lemma cpye_inv_lref1_free: ∀G,L,T2,d,e,i. ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃T2⦄ → + (∨∨ |L| ≤ i | d + e ≤ yinj i | yinj i < d) → T2 = #i. +#G #L #T2 #d #e #i #H * elim (cpye_inv_lref1 … H) -H * // +#I #K #V1 #V2 #Hdi #Hide #HLK #_ #_ #H +[ elim (lt_refl_false i) -d + @(lt_to_le_to_lt … H) -H /2 width=5 by ldrop_fwd_length_lt2/ (**) (* full auto slow: 19s *) +] +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_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/etc/cny/cpys_cny.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpys_cny.etc new file mode 100644 index 000000000..1499ceea5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpys_cny.etc @@ -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/etc/cny/cpzs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpzs.etc new file mode 100644 index 000000000..0fada97a0 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpzs.etc @@ -0,0 +1,83 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/relations/pdeltaconvstar_6.ma". +include "basic_2/substitution/cpye_lift.ma". + +(* CONTEXT-SENSITIVE EXTENDED DELTA-EQUIVALENCE FOR TERMS *******************) + +definition cpzs: ynat → ynat → relation4 genv lenv term term ≝ + λd,e,G,L,T1,T2. + ∃∃T. ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T⦄ & ⦃G, L⦄ ⊢ T2 ▶*[d, e] 𝐍⦃T⦄. + +interpretation "context-sensitive extended delta-equivalence (term)" + 'PDeltaConvStar G L T1 d e T2 = (cpzs d e G L T1 T2). + +(* Basic properties **********************************************************) + +lemma cpye_div: ∀G,L,T1,T,d,e. ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T⦄ → + ∀T2. ⦃G, L⦄ ⊢ T2 ▶*[d, e] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ T1 ◆*[d, e] T2. +/2 width=3 by ex2_intro/ qed. + +lemma cpzs_refl: ∀G,L,d,e. reflexive … (cpzs d e G L). +#G #L #d #e #T elim (cpye_total G L T d e) /2 width=3 by cpye_div/ +qed. + +lemma cpzs_bind: ∀G,L,V1,V2,d,e. ⦃G, L⦄ ⊢ V1 ◆*[d, e] V2 → + ∀I,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ◆*[⫯d, e] T2 → + ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ◆*[d, e] ⓑ{a,I}V2.T2. +#G #L #V1 #V2 #d #e * #V #HV1 #HV2 #I #T1 #T2 * +/5 width=10 by cpye_div, cpye_bind, leqy_cpye_trans, cny_bind, lsuby_succ/ +qed. + +lemma cpzs_flat: ∀G,L,V1,V2,d,e. ⦃G, L⦄ ⊢ V1 ◆*[d, e] V2 → + ∀T1,T2. ⦃G, L⦄ ⊢ T1 ◆*[d, e] T2 → + ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ◆*[d, e] ⓕ{I}V2.T2. +#G #L #V1 #V2 #d #e * #V #HV1 #HV2 #T1 #T2 * +/3 width=5 by cpye_div, cpye_flat, cny_flat/ +qed. + +(* Basic inversion lemmas ***************************************************) + +lemma cpzs_inv_sort: ∀G,L,d,e,k1,k2. ⦃G, L⦄ ⊢ ⋆k1 ◆*[d, e] ⋆k2 → k1 = k2. +#G #L #d #e #k1 #k2 * #X #H1 #H2 +lapply (cpye_inv_sort1 … H1) -H1 #H1 +lapply (cpye_inv_sort1 … H2) -H2 #H2 +destruct // +qed-. + +lemma cpzs_inv_bind: ∀a1,a2,I1,I2,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ ⓑ{a1,I1}V1.T1 ◆*[d, e] ⓑ{a2,I2}V2.T2 → + ∧∧ a1 = a2 & I1 = I2 + & ⦃G, L⦄ ⊢ V1 ◆*[d, e] V2 & ⦃G, L.ⓑ{I1}V1⦄ ⊢ T1 ◆*[⫯d, e] T2. +#a1 #a2 #I1 #I2 #G #L #V1 #V2 #T1 #T2 #d #e * #X #H1 #H2 +elim (cpye_inv_bind1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H1 +elim (cpye_inv_bind1 … H2) -H2 #W2 #U2 #HW12 #HU12 #H2 +destruct /5 width=8 by cpye_div, leqy_cpye_trans, lsuby_succ, and4_intro/ +qed-. + +lemma cpzs_inv_flat: ∀I1,I2,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ ⓕ{I1}V1.T1 ◆*[d, e] ⓕ{I2}V2.T2 → + ∧∧ I1 = I2 + & ⦃G, L⦄ ⊢ V1 ◆*[d, e] V2 & ⦃G, L⦄ ⊢ T1 ◆*[d, e] T2. +#I1 #I2 #G #L #V1 #V2 #T1 #T2 #d #e * #X #H1 #H2 +elim (cpye_inv_flat1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H1 +elim (cpye_inv_flat1 … H2) -H2 #W2 #U2 #HW12 #HU12 #H2 +destruct /3 width=3 by cpye_div, and3_intro/ +qed-. + +lemma cpzs_inv_flat_bind: ∀a2,I1,I2,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ ⓕ{I1}V1.T1 ◆*[d, e] ⓑ{a2,I2}V2.T2 → ⊥. +#a2 #I1 #I2 #G #L #V1 #V2 #T1 #T2 #d #e * #X #H1 #H2 +elim (cpye_inv_flat1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H1 +elim (cpye_inv_bind1 … H2) -H2 #W2 #U2 #HW12 #HU12 #H2 +destruct +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cny/lleq_cpye.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/lleq_cpye.etc new file mode 100644 index 000000000..e6890e637 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/lleq_cpye.etc @@ -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/etc/cny/lpx_cpye.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/lpx_cpye.etc new file mode 100644 index 000000000..48816c85d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/lpx_cpye.etc @@ -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/etc/cny/lpxs_cpye.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/lpxs_cpye.etc new file mode 100644 index 000000000..a6f0f86bd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/lpxs_cpye.etc @@ -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/etc/cny/pdeltaconvstar_6.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/pdeltaconvstar_6.etc new file mode 100644 index 000000000..b7de5f543 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/pdeltaconvstar_6.etc @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 break ◆ * [ term 46 d , break term 46 e ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'PDeltaConvStar $G $L $T1 $d $e $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cny/psubsteval_6.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/psubsteval_6.etc new file mode 100644 index 000000000..360f43d29 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/psubsteval_6.etc @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ▶ * break [ term 46 d , break term 46 e ] break 𝐍 ⦃ term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'PSubstEval $G $L $T1 $T2 $d $e }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cny/psubstevalalt_6.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/psubstevalalt_6.etc new file mode 100644 index 000000000..18cdf608f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/psubstevalalt_6.etc @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ▶ ▶ * break [ term 46 d , break term 46 e ] break 𝐍 ⦃ term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'PSubstEvalAlt $G $L $T1 $T2 $d $e }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cny/psubstnormal_5.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/psubstnormal_5.etc new file mode 100644 index 000000000..4a7a78afc --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/psubstnormal_5.etc @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ▶ break [ term 46 d , break term 46 e ] 𝐍 break ⦃ term 46 T ⦄ )" + non associative with precedence 45 + for @{ 'PSubstNormal $G $L $T $d $e }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/lazynegatedeq_4.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/lazynegatedeq_4.etc new file mode 100644 index 000000000..6b0cb85e5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/lazynegatedeq_4.etc @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( L1 ⧣ break [ term 46 T , break term 46 d ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'LazyNegatedEq $T $d $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/lazynegatedeqalt_4.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/lazynegatedeqalt_4.etc new file mode 100644 index 000000000..b150f63ff --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/lazynegatedeqalt_4.etc @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( L1 ⧣ ⧣ break [ term 46 T , break term 46 d ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'LazyNegatedEqAlt $T $d $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/llneq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/llneq.etc new file mode 100644 index 000000000..d41a4e83c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/llneq.etc @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/relations/lazynegatedeq_4.ma". +include "basic_2/substitution/lleq.ma". + +(* NEGATED LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **************************) + +definition llneq: relation4 ynat term lenv lenv ≝ + λd,T,L1,L2. |L1| = |L2| ∧ (L1 ⋕[T, d] L2 → ⊥). + +interpretation + "negated lazy equivalence (local environment)" + 'LazyNegatedEq T d L1 L2 = (llneq d T L1 L2). diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/llneq_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/llneq_alt.etc new file mode 100644 index 000000000..00eb2c34e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/llneq_alt.etc @@ -0,0 +1,68 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/relations/lazynegatedeqalt_4.ma". +include "basic_2/substitution/lleq_lleq.ma". +include "basic_2/substitution/llneq.ma". + +(* NEGATED LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **************************) + +(* alternative definition of llneq *) +inductive llneqa: relation4 ynat term lenv lenv ≝ +| llneqa_neq: ∀I1,I2,L1,L2,K1,K2,V1,V2,d,i. d ≤ yinj i → + ⇩[i]L1 ≡ K1.ⓑ{I1}V1 → ⇩[i]L2 ≡ K2.ⓑ{I2}V2 → + |K1| = |K2| → (V1 = V2 → ⊥) → llneqa d (#i) L1 L2 +| llneqa_eq : ∀I1,I2,L1,L2,K1,K2,V,d,i. d ≤ yinj i → + ⇩[i]L1 ≡ K1.ⓑ{I1}V → ⇩[i]L2 ≡ K2.ⓑ{I2}V → + llneqa 0 (V) K1 K2 → llneqa d (#i) L1 L2 +| llneqa_bind_sn: ∀a,I,L1,L2,V,T,d. + llneqa d V L1 L2 → llneqa d (ⓑ{a,I}V.T) L1 L2 +| llneqa_bind_dx: ∀a,I,L1,L2,V,T,d. + llneqa (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → llneqa d (ⓑ{a,I}V.T) L1 L2 +| llneqa_flat_sn: ∀I,L1,L2,V,T,d. + llneqa d V L1 L2 → llneqa d (ⓕ{I}V.T) L1 L2 +| llneqa_flat_dx: ∀I,L1,L2,V,T,d. + llneqa d T L1 L2 → llneqa d (ⓕ{I}V.T) L1 L2 +. + +interpretation + "negated lazy equivalence (local environment) alternative" + 'LazyNegatedEqAlt T d L1 L2 = (llneqa d T L1 L2). + +(* Main properties **********************************************************) + +theorem llneq_llneqa: ∀T,L1,L2,d. L1 ⧣[T, d] L2 → L1 ⧣⧣[T, d] L2. +#T #L1 @(f2_ind … rfw … L1 T) -L1 -T +#n #IH #L1 * * +[ #k #Hn #L2 #d * #HL12 #H elim H /2 width=1 by lleq_sort/ +| #i #Hn #L2 #d * #HL12 #H elim (ylt_split i d) #Hdi + [ elim H /2 width=1 by lleq_skip/ ] + elim (lt_or_ge i (|L1|)) #HiL1 + [2: elim H /3 width=3 by lleq_free, le_repl_sn_aux/ ] + elim (ldrop_O1_lt … HiL1) #I1 #K1 #V1 #HLK1 + elim (ldrop_O1_lt L2 i) /2 width=1 by/ #I2 #K2 #V2 #HLK2 + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) normalize + elim (eq_term_dec V1 V2) #HnV12 destruct + [2: #H @(llneqa_neq … HLK1 … HLK2) /2 width=1 by/ ] (**) (* explicit constructor *) + elim (lleq_dec V2 K1 K2 0) #HnV2 [ elim H /2 width=8 by lleq_lref/ ] + #H @(llneqa_eq … HLK1 … HLK2) /4 width=2 by ldrop_fwd_rfw, conj/ (**) (* explicit constructor *) +| #p #Hn #L2 #d * #HL12 #H elim H /2 width=1 by lleq_gref/ +| #a #I #V #T #Hn #L2 #d * #HL12 #H destruct elim (nlleq_inv_bind … H) -H + [ /5 width=1 by llneqa_bind_sn, conj/ + | #H @llneqa_bind_dx @IH // @conj normalize /2 width=1 by/ + ] +| #I #V #T #Hn #L2 #d * #HL12 #H destruct elim (nlleq_inv_flat … H) -H + /5 width=1 by llneqa_flat_dx, llneqa_flat_sn, conj/ +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/llneq_ext.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/llneq_ext.etc new file mode 100644 index 000000000..235d869c2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/llneq_ext.etc @@ -0,0 +1,33 @@ +(**************************************************************************) +(* ___ *) +(* ||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/llneq_alt.ma". + +(* NEGATED LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **************************) + +(* Advanced inversion lemmas ************************************************) + +lemma llneq_inv_atom1: ∀L1,L2,T,d. L1 ⧣⧣[T, d] L2 → |L1| ≤ d → ⊥. +#L1 #L2 #T #d #H elim H -L1 -L2 -T -d /2 width=1 by/ +[ #I1 #I2 #L1 #L2 #K1 #K2 #V1 #V2 #d #i #Hdi #HLK1 #_ #_ #_ + >(ldrop_fwd_length … HLK1) -HLK1 normalize + #H lapply (yle_trans … H … Hdi) -d + /3 width=4 by yle_inv_inj, le_plus_xySz_x_false/ +| #I1 #I2 #L1 #L2 #K1 #K2 #V #d #i #Hdi #HLK1 #_ #_ #_ + >(ldrop_fwd_length … HLK1) -HLK1 normalize + #H lapply (yle_trans … H … Hdi) -d + /3 width=4 by yle_inv_inj, le_plus_xySz_x_false/ +| #a #I #L1 (length_inv_zero_dx … H) -L1 /3 width=5 by ex3_intro, conj/ +| #I2 #L2 #K2 #V2 #W2 #_ #HVW2 #IHLK2 #Y #H + elim (length_inv_pos_dx … H) -H #I #L1 #V1 #HL12 #H destruct + elim (IHLK2 … HL12) -IHLK2 #K1 #HLK1 #HK12 #IH + elim (eq_term_dec V1 V2) #H destruct + [ @(ex3_intro … (K1.ⓑ{I}W2)) normalize /2 width=1 by / +*) +axiom lleq_lpx_trans: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡[h, g] K2 → + ∀L1,T,d. L1 ⋕[T, d] L2 → + ∃∃K1. ⦃G, L1⦄ ⊢ ➡[h, g] K1 & K1 ⋕[T, d] K2. +(* +#h #g #G #L2 #K2 #H elim H -L2 -K2 +[ #L1 #T #d #H lapply (lleq_fwd_length … H) -H + #H >(length_inv_zero_dx … H) -L1 /2 width=3 by ex2_intro/ +| #I2 #L2 #K2 #V2 #W2 #HLK2 #HVW2 #IHLK2 #Y #T #d #HT + lapply (lleq_fwd_length … HT) #H + elim (length_inv_pos_dx … H) -H #I1 #L1 #V1 #HL12 #H destruct + elim (eq_term_dec V1 V2) #H destruct + [ @ex2_intro … +*) lemma lpx_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cny.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/cny.ma deleted file mode 100644 index 81919dc4b..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cny.ma +++ /dev/null @@ -1,114 +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/notation/relations/psubstnormal_5.ma". -include "basic_2/relocation/cpy.ma". - -(* NORMAL TERMS FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION *****************) - -definition cny: ∀d,e. relation3 genv lenv term ≝ - λd,e,G,L. NF … (cpy d e G L) (eq …). - -interpretation - "normality for context-sensitive extended substitution (term)" - 'PSubstNormal G L T d e = (cny d e G L T). - -(* Basic inversion lemmas ***************************************************) - -lemma cny_inv_lref: ∀G,L,d,e,i. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄ → - ∨∨ yinj i < d | d + e ≤ yinj i | |L| ≤ i. -#G #L #d #e #i #H elim (ylt_split i d) /2 width=1 by or3_intro0/ -#Hdi elim (ylt_split i (d+e)) /2 width=1 by or3_intro1/ -#Hide elim (lt_or_ge i (|L|)) /2 width=1 by or3_intro2/ -#Hi elim (ldrop_O1_lt L i) // -#I #K #V #HLK elim (lift_total V 0 (i+1)) -#W #HVW lapply (H W ?) -H /2 width=5 by cpy_subst/ -HLK -#H destruct elim (lift_inv_lref2_be … HVW) -L -d -e // -qed-. - -lemma cny_inv_bind: ∀a,I,G,L,V,T,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓑ{a,I}V.T⦄ → - ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ ▶[⫯d, e] 𝐍⦃T⦄. -#a #I #G #L #V1 #T1 #d #e #HVT1 @conj -[ #V2 #HV2 lapply (HVT1 (ⓑ{a,I}V2.T1) ?) -HVT1 -| #T2 #HT2 lapply (HVT1 (ⓑ{a,I}V1.T2) ?) -HVT1 -] -/2 width=1 by cpy_bind/ #H destruct // -qed-. - -lemma cny_inv_flat: ∀I,G,L,V,T,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓕ{I}V.T⦄ → - ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ ∧ ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃T⦄. -#I #G #L #V1 #T1 #d #e #HVT1 @conj -[ #V2 #HV2 lapply (HVT1 (ⓕ{I}V2.T1) ?) -HVT1 -| #T2 #HT2 lapply (HVT1 (ⓕ{I}V1.T2) ?) -HVT1 -] -/2 width=1 by cpy_flat/ #H destruct // -qed-. - -(* Basic properties *********************************************************) - -lemma lsuby_cny_conf: ∀G,d,e. - ∀L1,T. ⦃G, L1⦄ ⊢ ▶[d, e] 𝐍⦃T⦄ → - ∀L2. L1 ⊑×[d, e] L2 → ⦃G, L2⦄ ⊢ ▶[d, e] 𝐍⦃T⦄. -#G #d #e #L1 #T1 #HT1 #L2 #HL12 #T2 #HT12 -@HT1 /3 width=3 by lsuby_cpy_trans/ -qed-. - -lemma cny_sort: ∀G,L,d,e,k. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃⋆k⦄. -#G #L #d #e #k #X #H elim (cpy_inv_sort1 … H) -H // -qed. - -lemma cny_lref_free: ∀G,L,d,e,i. |L| ≤ i → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄. -#G #L #d #e #i #Hi #X #H elim (cpy_inv_lref1 … H) -H // * -#I #K #V #_ #_ #HLK #_ lapply (ldrop_fwd_length_lt2 … HLK) -HLK -#H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/ -qed. - -lemma cny_lref_atom: ∀G,L,d,e,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄. -#G #L #d #e #i #HL @cny_lref_free >(ldrop_fwd_length … HL) -HL // -qed. - -lemma cny_lref_top: ∀G,L,d,e,i. d+e ≤ yinj i → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄. -#G #L #d #e #i #Hdei #X #H elim (cpy_inv_lref1 … H) -H // * -#I #K #V #_ #H elim (ylt_yle_false … H) // -qed. - -lemma cny_lref_skip: ∀G,L,d,e,i. yinj i < d → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄. -#G #L #d #e #i #Hid #X #H elim (cpy_inv_lref1 … H) -H // * -#I #K #V #H elim (ylt_yle_false … H) // -qed. - -lemma cny_gref: ∀G,L,d,e,p. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃§p⦄. -#G #L #d #e #p #X #H elim (cpy_inv_gref1 … H) -H // -qed. - -lemma cny_bind: ∀G,L,V,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ → - ∀I,T. ⦃G, L.ⓑ{I}V⦄ ⊢ ▶[⫯d, e] 𝐍⦃T⦄ → - ∀a. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓑ{a,I}V.T⦄. -#G #L #V1 #d #e #HV1 #I #T1 #HT1 #a #X #H -elim (cpy_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct ->(HV1 … HV12) -V2 >(HT1 … HT12) -T2 // -qed. - -lemma cny_flat: ∀G,L,V,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ → - ∀T. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃T⦄ → - ∀I. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓕ{I}V.T⦄. -#G #L #V1 #d #e #HV1 #T1 #HT1 #I #X #H -elim (cpy_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct ->(HV1 … HV12) -V2 >(HT1 … HT12) -T2 // -qed. - -lemma cny_narrow: ∀G,L,T,d1,e1. ⦃G, L⦄ ⊢ ▶[d1, e1] 𝐍⦃T⦄ → - ∀d2,e2. d1 ≤ d2 → d2 + e2 ≤ d1 + e1 → ⦃G, L⦄ ⊢ ▶[d2, e2] 𝐍⦃T⦄. -#G #L #T1 #d1 #e1 #HT1 #d2 #e2 #Hd12 #Hde21 #T2 #HT12 -@HT1 /2 width=5 by cpy_weak/ 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 deleted file mode 100644 index 213fa6abb..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cny_lift.ma +++ /dev/null @@ -1,118 +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/relocation/cpy_lift.ma". -include "basic_2/relocation/cny.ma". - -(* NORMAL TERMS FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION *****************) - -(* Properties on relocation *************************************************) - -lemma cny_lift_le: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, K⦄ ⊢ ▶[dt, et] 𝐍⦃T⦄ → ⇩[s, d, e] L ≡ K → - ⇧[d, e] T ≡ U → dt + et ≤ d → ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄. -#G #L #K #T1 #U1 #s #d #dt #e #et #HT1 #HLK #HTU1 #Hdetd #U2 #HU12 -elim (cpy_inv_lift1_le … HU12 … HLK … HTU1) // -L -Hdetd #T2 #HT12 ->(HT1 … HT12) -K /2 width=5 by lift_mono/ -qed-. - -lemma cny_lift_be: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, K⦄ ⊢ ▶[dt, et] 𝐍⦃T⦄ → ⇩[s, d, e] L ≡ K → - ⇧[d, e] T ≡ U → dt ≤ d → yinj d ≤ dt + et → ⦃G, L⦄ ⊢ ▶[dt, et+e] 𝐍⦃U⦄. -#G #L #K #T1 #U1 #s #d #dt #e #et #HT1 #HLK #HTU1 #Hdtd #Hddet #U2 #HU12 -elim (cpy_inv_lift1_be … HU12 … HLK … HTU1) /2 width=1 by monotonic_yle_plus_dx/ -L -Hdtd -Hddet #T2 ->yplus_minus_inj #HT12 >(HT1 … HT12) -K /2 width=5 by lift_mono/ -qed-. - -lemma cny_lift_ge: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, K⦄ ⊢ ▶[dt, et] 𝐍⦃T⦄ → ⇩[s, d, e] L ≡ K → - ⇧[d, e] T ≡ U → d ≤ dt → ⦃G, L⦄ ⊢ ▶[dt+e, et] 𝐍⦃U⦄. -#G #L #K #T1 #U1 #s #d #dt #e #et #HT1 #HLK #HTU1 #Hddt #U2 #HU12 -elim (cpy_inv_lift1_ge … HU12 … HLK … HTU1) /2 width=1 by monotonic_yle_plus_dx/ -L -Hddt #T2 ->yplus_minus_inj #HT12 >(HT1 … HT12) -K /2 width=5 by lift_mono/ -qed-. - -(* Inversion lemmas on relocation *******************************************) - -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 -lapply (cpy_lift_le … HT12 … HLK … HTU1 … HTU2 ?) // -K -Hdetd #HU12 -lapply (HU1 … HU12) -L /2 width=5 by lift_inj/ -qed-. - -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 -elim (yle_inv_plus_inj2 … Hdedet) -Hdedet #Hddete #Hedet -elim (lift_total T2 d e) #U2 #HTU2 -lapply (cpy_lift_be … HT12 … HLK … HTU1 … HTU2 ? ?) // [ >yplus_minus_assoc_inj // ] -K -Hdtd -Hddete ->ymax_pre_sn // -Heet #HU12 -lapply (HU1 … HU12) -L /2 width=5 by lift_inj/ -qed-. - -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 -elim (lift_total T2 d e) #U2 #HTU2 -lapply (cpy_lift_ge … HT12 … HLK … HTU1 … HTU2 ?) // -K -Hddte ->ymax_pre_sn // -Hedt #HU12 -lapply (HU1 … HU12) -L /2 width=5 by lift_inj/ -qed-. - -(* Advanced inversion lemmas on relocation **********************************) - -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_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_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/ -| >yminus_succ2 // -] -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/lsuby.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma index 123529e05..f6bab12f8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma @@ -44,6 +44,11 @@ lemma lsuby_succ_lt: ∀I1,I2,L1,L2,V1,V2,d,e. L1 ⊑×[⫰d, e] L2 → 0 < d #I1 #I2 #L1 #L2 #V1 #V2 #d #e #HL12 #Hd <(ylt_inv_O1 … Hd) /2 width=1 by lsuby_succ/ qed. +lemma lsuby_pair_O_Y: ∀L1,L2. L1 ⊑×[0, ∞] L2 → + ∀I1,I2,V. L1.ⓑ{I1}V ⊑×[0,∞] L2.ⓑ{I2}V. +#L1 #L2 #HL12 #I1 #I2 #V lapply (lsuby_pair I1 I2 … V … HL12) -HL12 // +qed. + lemma lsuby_refl: ∀L,d,e. L ⊑×[d, e] L. #L elim L -L // #L #I #V #IHL #d elim (ynat_cases … d) [| * #x ] @@ -52,19 +57,19 @@ lemma lsuby_refl: ∀L,d,e. L ⊑×[d, e] L. #He destruct /2 width=1 by lsuby_zero, lsuby_pair/ qed. -lemma lsuby_length: ∀L1,L2. |L2| ≤ |L1| → L1 ⊑×[yinj 0, yinj 0] L2. -#L1 elim L1 -L1 -[ #X #H lapply (le_n_O_to_eq … H) -H - #H lapply (length_inv_zero_sn … H) #H destruct /2 width=1 by lsuby_atom/ -| #L1 #I1 #V1 #IHL1 * normalize - /4 width=2 by lsuby_zero, le_S_S_to_le/ +lemma lsuby_O1: ∀L2,L1,d. |L2| ≤ |L1| → L1 ⊑×[d, yinj 0] L2. +#L2 elim L2 -L2 // #L2 #I2 #V2 #IHL2 * normalize +[ #d #H lapply (le_n_O_to_eq … H) -H (length_inv_zero_dx … H) -L1 // -| /2 width=1 by lsuby_length/ +| /2 width=1 by lsuby_O1/ | #I1 #I2 #L1 #L2 #V #e #_ #IHL12 #H lapply (injective_plus_l … H) /3 width=1 by lsuby_pair/ | #I1 #I2 #L1 #L2 #V1 #V2 #d #e #_ #IHL12 #H lapply (injective_plus_l … H) diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye.ma deleted file mode 100644 index 82a1e3b46..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye.ma +++ /dev/null @@ -1,82 +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/notation/relations/psubsteval_6.ma". -include "basic_2/relocation/cny.ma". -include "basic_2/substitution/cpys.ma". - -(* EVALUATION FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION ON TERMS **********) - -definition cpye: ynat → ynat → relation4 genv lenv term term ≝ - λd,e,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 ∧ ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃T2⦄. - -interpretation "evaluation for context-sensitive extended substitution (term)" - 'PSubstEval G L T1 T2 d e = (cpye d e G L T1 T2). - -(* Basic_properties *********************************************************) - -lemma cpye_sort: ∀G,L,d,e,k. ⦃G, L⦄ ⊢ ⋆k ▶*[d, e] 𝐍⦃⋆k⦄. -/3 width=5 by cny_sort, conj/ qed. - -lemma cpye_free: ∀G,L,d,e,i. |L| ≤ i → ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃#i⦄. -/3 width=6 by cny_lref_free, conj/ qed. - -lemma cpye_top: ∀G,L,d,e,i. d + e ≤ yinj i → ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃#i⦄. -/3 width=6 by cny_lref_top, conj/ qed. - -lemma cpye_skip: ∀G,L,d,e,i. yinj i < d → ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃#i⦄. -/3 width=6 by cny_lref_skip, conj/ qed. - -lemma cpye_gref: ∀G,L,d,e,p. ⦃G, L⦄ ⊢ §p ▶*[d, e] 𝐍⦃§p⦄. -/3 width=5 by cny_gref, conj/ qed. - -lemma cpye_bind: ∀G,L,V1,V2,d,e. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ → - ∀I,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*[⫯d, e] 𝐍⦃T2⦄ → - ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*[d, e] 𝐍⦃ⓑ{a,I}V2.T2⦄. -#G #L #V1 #V2 #d #e * #HV12 #HV2 #I #T1 #T2 * -/5 width=8 by cpys_bind, cny_bind, lsuby_cny_conf, lsuby_succ, conj/ -qed. - -lemma cpye_flat: ∀G,L,V1,V2,d,e. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ → - ∀T1,T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄ → - ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ▶*[d, e] 𝐍⦃ⓕ{I}V2.T2⦄. -#G #L #V1 #V2 #d #e * #HV12 #HV2 #T1 #T2 * -/3 width=7 by cpys_flat, cny_flat, conj/ -qed. - -(* Basic inversion lemmas ***************************************************) - -lemma cpye_inv_sort1: ∀G,L,X,d,e,k. ⦃G, L⦄ ⊢ ⋆k ▶*[d, e] 𝐍⦃X⦄ → X = ⋆k. -#G #L #X #d #e #k * /2 width=5 by cpys_inv_sort1/ -qed-. - -lemma cpye_inv_gref1: ∀G,L,X,d,e,p. ⦃G, L⦄ ⊢ §p ▶*[d, e] 𝐍⦃X⦄ → X = §p. -#G #L #X #d #e #p * /2 width=5 by cpys_inv_gref1/ -qed-. - -lemma cpye_inv_bind1: ∀a,I,G,L,V1,T1,X,d,e. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*[d, e] 𝐍⦃X⦄ → - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*[⫯d, e] 𝐍⦃T2⦄ & - X = ⓑ{a,I}V2.T2. -#a #I #G #L #V1 #T1 #X #d #e * #H1 #H2 elim (cpys_inv_bind1 … H1) -H1 -#V2 #T2 #HV12 #HT12 #H destruct elim (cny_inv_bind … H2) -H2 -/5 width=8 by lsuby_cny_conf, lsuby_succ, ex3_2_intro, conj/ -qed-. - -lemma cpye_inv_flat1: ∀I,G,L,V1,T1,X,d,e. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ▶*[d, e] 𝐍⦃X⦄ → - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ & ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄ & - X = ⓕ{I}V2.T2. -#I #G #L #V1 #T1 #X #d #e * #H1 #H2 elim (cpys_inv_flat1 … H1) -H1 -#V2 #T2 #HV12 #HT12 #H destruct elim (cny_inv_flat … H2) -H2 -/3 width=5 by ex3_2_intro, conj/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye_alt.ma deleted file mode 100644 index a9dc53cf5..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye_alt.ma +++ /dev/null @@ -1,89 +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/notation/relations/psubstevalalt_6.ma". -include "basic_2/substitution/cpye_lift.ma". - -(* EVALUATION FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION ON TERMS **********) - -(* Note: alternative definition of cpye *) -inductive cpyea: ynat → ynat → relation4 genv lenv term term ≝ -| cpyea_sort : ∀G,L,d,e,k. cpyea d e G L (⋆k) (⋆k) -| cpyea_free : ∀G,L,d,e,i. |L| ≤ i → cpyea d e G L (#i) (#i) -| cpyea_top : ∀G,L,d,e,i. d + e ≤ yinj i → cpyea d e G L (#i) (#i) -| cpyea_skip : ∀G,L,d,e,i. yinj i < d → cpyea d e G L (#i) (#i) -| cpyea_subst: ∀I,G,L,K,V1,V2,W2,i,d,e. d ≤ yinj i → yinj i < d+e → - ⇩[i] L ≡ K.ⓑ{I}V1 → cpyea (yinj 0) (⫰(d+e-yinj i)) G K V1 V2 → - ⇧[0, i+1] V2 ≡ W2 → cpyea d e G L (#i) W2 -| cpyea_gref : ∀G,L,d,e,p. cpyea d e G L (§p) (§p) -| cpyea_bind : ∀a,I,G,L,V1,V2,T1,T2,d,e. - cpyea d e G L V1 V2 → cpyea (⫯d) e G (L.ⓑ{I}V1) T1 T2 → - cpyea d e G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2) -| cpyea_flat : ∀I,G,L,V1,V2,T1,T2,d,e. - cpyea d e G L V1 V2 → cpyea d e G L T1 T2 → - cpyea d e G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) -. - -interpretation - "evaluation for context-sensitive extended substitution (term) alternative" - 'PSubstEvalAlt G L T1 T2 d e = (cpyea d e G L T1 T2). - -(* Main properties **********************************************************) - -theorem cpye_cpyea: ∀G,L,T1,T2,d,e. ⦃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 #_ #_ #_ #T2 #d #e #H -X -Y -Z >(cpye_inv_sort1 … H) -H // -| #i #HG #HL #HT #T2 #d #e #H destruct - elim (cpye_inv_lref1 … H) -H * - /4 width=7 by cpyea_subst, cpyea_free, cpyea_top, cpyea_skip, fqup_lref/ -| #p #_ #_ #_ #T2 #d #e #H -X -Y -Z >(cpye_inv_gref1 … H) -H // -| #a #I #V1 #T1 #HG #HL #HT #T #d #e #H destruct - elim (cpye_inv_bind1 … H) -H /3 width=1 by cpyea_bind/ -| #I #V1 #T1 #HG #HL #HT #T #d #e #H destruct - elim (cpye_inv_flat1 … H) -H /3 width=1 by cpyea_flat/ -] -qed. - -(* Main inversion properties ************************************************) - -theorem cpyea_inv_cpye: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶▶*[d, e] 𝐍⦃T2⦄ → ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄. -#G #L #T1 #T2 #d #e #H elim H -G -L -T1 -T2 -d -e -/2 width=7 by cpye_subst, cpye_flat, cpye_bind, cpye_skip, cpye_top, cpye_free/ -qed-. - -(* Advanced eliminators *****************************************************) - -lemma cpye_ind_alt: ∀R:ynat→ynat→relation4 genv lenv term term. - (∀G,L,d,e,k. R d e G L (⋆k) (⋆k)) → - (∀G,L,d,e,i. |L| ≤ i → R d e G L (#i) (#i)) → - (∀G,L,d,e,i. d + e ≤ yinj i → R d e G L (#i) (#i)) → - (∀G,L,d,e,i. yinj i < d → R d e G L (#i) (#i)) → - (∀I,G,L,K,V1,V2,W2,i,d,e. d ≤ yinj i → yinj i < d + e → - ⇩[i] L ≡ K.ⓑ{I}V1 → ⦃G, K⦄ ⊢ V1 ▶*[yinj O, ⫰(d+e-yinj i)] 𝐍⦃V2⦄ → - ⇧[O, i+1] V2 ≡ W2 → R (yinj O) (⫰(d+e-yinj i)) G K V1 V2 → R d e G L (#i) W2 - ) → - (∀G,L,d,e,p. R d e G L (§p) (§p)) → - (∀a,I,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ → - ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*[⫯d, e] 𝐍⦃T2⦄ → R d e G L V1 V2 → - R (⫯d) e G (L.ⓑ{I}V1) T1 T2 → R d e G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2) - ) → - (∀I,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ → - ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄ → R d e G L V1 V2 → - R d e G L T1 T2 → R d e G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) - ) → - ∀d,e,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄ → R d e G L T1 T2. -#R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #d #e #G #L #T1 #T2 #H elim (cpye_cpyea … H) -G -L -T1 -T2 -d -e -/3 width=8 by cpyea_inv_cpye/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye_cpye.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye_cpye.ma deleted file mode 100644 index 42bd19b8e..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye_cpye.ma +++ /dev/null @@ -1,28 +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/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 deleted file mode 100644 index 3c0abe617..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye_lift.ma +++ /dev/null @@ -1,169 +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/relocation/cny_lift.ma". -include "basic_2/substitution/fqup.ma". -include "basic_2/substitution/cpys_lift.ma". -include "basic_2/substitution/cpye.ma". - -(* EVALUATION FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION ON TERMS **********) - -(* Advanced properties ******************************************************) - -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_lift_subst, ldrop_fwd_drop2, conj/ -qed. - -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/ -| #i #HG #HL #HT #d #e destruct - elim (ylt_split i d) /3 width=2 by cpye_skip, ex_intro/ - elim (ylt_split i (d+e)) /3 width=2 by cpye_top, ex_intro/ - elim (lt_or_ge i (|L|)) /3 width=2 by cpye_free, ex_intro/ - #Hi #Hide #Hdi elim (ldrop_O1_lt L i) // -Hi - #I #K #V1 #HLK elim (IH G K V1 … 0 (⫰(d+e-i))) -IH /2 width=2 by fqup_lref/ - #V2 elim (lift_total V2 0 (i+1)) /3 width=8 by ex_intro, cpye_subst/ -| #p #HG #HL #HT #d #e destruct -IH /2 width=2 by ex_intro/ -| #a #I #V1 #T1 #HG #HL #HT #d #e destruct - elim (IH G L V1 … d e) // elim (IH G (L.ⓑ{I}V1) T1 … (⫯d) e) // - /3 width=2 by cpye_bind, ex_intro/ -| #I #V1 #T1 #HG #HL #HT #d #e destruct - elim (IH G L V1 … d e) // elim (IH G L T1 … d e) // - /3 width=2 by cpye_flat, ex_intro/ -] -qed-. - -(* Advanced inversion lemmas ************************************************) - -lemma cpye_inv_lref1: ∀G,L,T2,d,e,i. ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃T2⦄ → - ∨∨ |L| ≤ i ∧ T2 = #i - | d + e ≤ yinj i ∧ T2 = #i - | yinj i < d ∧ T2 = #i - | ∃∃I,K,V1,V2. d ≤ yinj i & yinj i < d + e & - ⇩[i] L ≡ K.ⓑ{I}V1 & - ⦃G, K⦄ ⊢ V1 ▶*[yinj 0, ⫰(d+e-yinj i)] 𝐍⦃V2⦄ & - ⇧[O, i+1] V2 ≡ T2. -#G #L #T2 #i #d #e * #H1 #H2 elim (cpys_inv_lref1 … H1) -H1 -[ #H destruct elim (cny_inv_lref … H2) -H2 - /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_lift_subst, ldrop_fwd_drop2, conj/ -] -qed-. - -lemma cpye_inv_lref1_free: ∀G,L,T2,d,e,i. ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃T2⦄ → - (∨∨ |L| ≤ i | d + e ≤ yinj i | yinj i < d) → T2 = #i. -#G #L #T2 #d #e #i #H * elim (cpye_inv_lref1 … H) -H * // -#I #K #V1 #V2 #Hdi #Hide #HLK #_ #_ #H -[ elim (lt_refl_false i) -d - @(lt_to_le_to_lt … H) -H /2 width=5 by ldrop_fwd_length_lt2/ (**) (* full auto slow: 19s *) -] -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_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_cny.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cny.ma deleted file mode 100644 index 1499ceea5..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cny.ma +++ /dev/null @@ -1,26 +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/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/lleq_cpye.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_cpye.ma deleted file mode 100644 index e6890e637..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_cpye.ma +++ /dev/null @@ -1,49 +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/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 6d4072800..de9939c00 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 @@ -84,7 +84,7 @@ table { } ] [ { "strongly normalizing extended computation" * } { - [ "lsx ( ? ⊢ ⬊*[?,?,?] ? )" "lsx_cpxs" + "lsx_csx" * ] + [ "lsx ( ? ⊢ ⬊*[?,?,?,?] ? )" "lsx_cpxs" + "lsx_csx" * ] [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tstc_vector" + "csx_aaa" * ] [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lpx" + "csx_fpbs" * ] } @@ -105,8 +105,8 @@ table { } ] [ { "context-sensitive extended computation" * } { - [ "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" * ] + [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? )" "lpxs_ldrop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] + [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_lift" + "cpxs_cpys" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ] } ] [ { "context-sensitive computation" * } { @@ -135,7 +135,7 @@ table { } ] [ { "context-sensitive extended reduction" * } { - [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_cpys" + "lpx_cpye" + "lpx_lleq" + "lpx_aaa" * ] + [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_cpys" + "lpx_lleq" + "lpx_aaa" * ] [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_lift" + "cpx_cpys" + "cpx_lleq" + "cpx_cix" * ] } ] @@ -209,15 +209,11 @@ table { class "yellow" [ { "substitution" * } { [ { "lazy equivalence for local environments" * } { - [ "lleq ( ? ⋕[?,?] ? )" "lleq_alt ( ? ⋕⋕[?,?] ? )" "lleq_ldrop" + "lleq_fqus" + "lleq_cpye" + "lleq_lleq" + "lleq_ext" * ] + [ "lleq ( ? ⋕[?,?] ? )" "lleq_alt ( ? ⋕⋕[?,?] ? )" "lleq_ldrop" + "lleq_fqus" + "lleq_lleq" + "lleq_ext" * ] } ] - [ { "evaluation for contxt-sensitive extended substitution" * } { - [ "cpye ( ⦃?,?⦄ ⊢ ? ▶*[?,?] 𝐍⦃?⦄ )" "cpye_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] 𝐍⦃?⦄ )" "cpye_lift" + "cpye_cpye" * ] - } - ] [ { "contxt-sensitive extended multiple substitution" * } { - [ "cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )" "cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )" "cpys_lift" + "cpys_cny" + "cpys_cpys" * ] + [ "cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )" "cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )" "cpys_lift" + "cpys_cpys" * ] } ] [ { "iterated structural successor for closures" * } { @@ -242,10 +238,6 @@ table { ] class "orange" [ { "relocation" * } { - [ { "normal forms for context-sensitive extended substitution" * } { - [ "cny ( ⦃?,?⦄ ⊢ ▶[?,?] 𝐍⦃?⦄ )" "cny_lift" * ] - } - ] [ { "contxt-sensitive extended ordinary substitution" * } { [ "cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )" "cpy_lift" + "cpy_cpy" * ] }