From: Ferruccio Guidi Date: Sun, 13 Apr 2014 15:03:16 +0000 (+0000) Subject: we restored the strong normalization of extended computation for local X-Git-Tag: make_still_working~937 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c69a33bba2ae2f37953737940fb45149136cf054;p=helm.git we restored the strong normalization of extended computation for local environments with some important updates from the "lazy version" --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx.ma new file mode 100644 index 000000000..a1e27d0b1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx.ma @@ -0,0 +1,77 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cosn_5.ma". +include "basic_2/computation/lsx.ma". + +(* SN EXTENDED STRONGLY CONORMALIZING LOCAL ENVIRONMENTS ********************) + +inductive lcosx (h) (g) (G): relation2 ynat lenv ≝ +| lcosx_sort: ∀d. lcosx h g G d (⋆) +| lcosx_skip: ∀I,L,T. lcosx h g G 0 L → lcosx h g G 0 (L.ⓑ{I}T) +| lcosx_pair: ∀I,L,T,d. G ⊢ ⬊*[h, g, T, d] L → + lcosx h g G d L → lcosx h g G (⫯d) (L.ⓑ{I}T) +. + +interpretation + "sn extended strong conormalization (local environment)" + 'CoSN h g d G L = (lcosx h g G d L). + +(* Basic properties *********************************************************) + +lemma lcosx_O: ∀h,g,G,L. G ⊢ ~⬊*[h, g, 0] L. +#h #g #G #L elim L /2 width=1 by lcosx_skip/ +qed. + +lemma lcosx_ldrop_trans_lt: ∀h,g,G,L,d. G ⊢ ~⬊*[h, g, d] L → + ∀I,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → i < d → + G ⊢ ~⬊*[h, g, ⫰(d-i)] K ∧ G ⊢ ⬊*[h, g, V, ⫰(d-i)] K. +#h #g #G #L #d #H elim H -L -d +[ #d #J #K #V #i #H elim (ldrop_inv_atom1 … H) -H #H destruct +| #I #L #T #_ #_ #J #K #V #i #_ #H elim (ylt_yle_false … H) -H // +| #I #L #T #d #HT #HL #IHL #J #K #V #i #H #Hid + elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK destruct + [ >ypred_succ /2 width=1 by conj/ + | lapply (ylt_pred … Hid ?) -Hid /2 width=1 by ylt_inj/ >ypred_succ #Hid + elim (IHL … HLK ?) -IHL -HLK yminus_SO2 // + <(ypred_succ d) in ⊢ (%→%→?); >yminus_pred /2 width=1 by ylt_inj, conj/ + ] +] +qed-. + +(* Basic inversion lemmas ***************************************************) + +fact lcosx_inv_succ_aux: ∀h,g,G,L,x. G ⊢ ~⬊*[h, g, x] L → ∀d. x = ⫯d → + L = ⋆ ∨ + ∃∃I,K,V. L = K.ⓑ{I}V & G ⊢ ~⬊*[h, g, d] K & + G ⊢ ⬊*[h, g, V, d] K. +#h #g #G #L #d * -L -d /2 width=1 by or_introl/ +[ #I #L #T #_ #x #H elim (ysucc_inv_O_sn … H) +| #I #L #T #d #HT #HL #x #H <(ysucc_inj … H) -x + /3 width=6 by ex3_3_intro, or_intror/ +] +qed-. + +lemma lcosx_inv_succ: ∀h,g,G,L,d. G ⊢ ~⬊*[h, g, ⫯d] L → L = ⋆ ∨ + ∃∃I,K,V. L = K.ⓑ{I}V & G ⊢ ~⬊*[h, g, d] K & + G ⊢ ⬊*[h, g, V, d] K. +/2 width=3 by lcosx_inv_succ_aux/ qed-. + +lemma lcosx_inv_pair: ∀h,g,I,G,L,T,d. G ⊢ ~⬊*[h, g, ⫯d] L.ⓑ{I}T → + G ⊢ ~⬊*[h, g, d] L ∧ G ⊢ ⬊*[h, g, T, d] L. +#h #g #I #G #L #T #d #H elim (lcosx_inv_succ … H) -H +[ #H destruct +| * #Z #Y #X #H destruct /2 width=1 by conj/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx_cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx_cpx.ma new file mode 100644 index 000000000..e78ae1b4f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx_cpx.ma @@ -0,0 +1,67 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground_2/ynat/ynat_max.ma". +include "basic_2/computation/lsx_ldrop.ma". +include "basic_2/computation/lsx_lpx.ma". +include "basic_2/computation/lsx_lpxs.ma". +include "basic_2/computation/lcosx.ma". + +(* SN EXTENDED STRONGLY CONORMALIZING LOCAL ENVIRONMENTS ********************) + +(* Properties on extended context-sensitive parallel reduction for term *****) + +lemma lsx_cpx_trans_lcosx: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → + ∀d. G ⊢ ~⬊*[h, g, d] L → + G ⊢ ⬊*[h, g, T1, d] L → G ⊢ ⬊*[h, g, T2, d] L. +#h #g #G #L #T1 #T2 #H elim H -G -L -T1 -T2 // +[ #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #d #HL #H + elim (ylt_split i d) #Hdi [ -H | -HL ] + [ <(ymax_pre_sn d (⫯i)) /2 width=1 by ylt_fwd_le_succ/ + elim (lcosx_ldrop_trans_lt … HL … HLK) // -HL -Hdi + lapply (ldrop_fwd_drop2 … HLK) -HLK /3 width=7 by lsx_lift_ge/ + | lapply (lsx_fwd_lref_be … H … HLK) // -H -Hdi + lapply (ldrop_fwd_drop2 … HLK) -HLK + /4 width=10 by lsx_ge, lsx_lift_le/ + ] +| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #HL #H + elim (lsx_inv_bind … H) -H #HV1 #HT1 + @lsx_bind /2 width=2 by/ (**) (* explicit constructor *) + @(lsx_leq_conf … (L.ⓑ{I}V1)) /3 width=1 by lcosx_pair, leq_succ/ +| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #HL #H + elim (lsx_inv_flat … H) -H /3 width=1 by lsx_flat/ +| #G #L #V #U1 #U2 #T2 #_ #HTU2 #IHU12 #d #HL #H + elim (lsx_inv_bind … H) -H + /4 width=9 by lcosx_pair, lsx_inv_lift_ge, ldrop_drop/ +| #G #L #V #T1 #T2 #_ #IHT12 #d #HL #H + elim (lsx_inv_flat … H) -H /2 width=1 by/ +| #G #L #V1 #V2 #T #_ #IHV12 #d #HL #H + elim (lsx_inv_flat … H) -H /2 width=1 by/ +| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #d #HL #H + elim (lsx_inv_flat … H) -H #HV1 #H + elim (lsx_inv_bind … H) -H #HW1 #HT1 + @lsx_bind /3 width=1 by lsx_flat/ (**) (* explicit constructor *) + @(lsx_leq_conf … (L.ⓛW1)) /3 width=1 by lcosx_pair, leq_succ/ +| #a #G #L #V1 #V2 #U2 #W1 #W2 #T1 #T2 #_ #HVU2 #_ #_ #IHV12 #IHW12 #IHT12 #d #HL #H + elim (lsx_inv_flat … H) -H #HV1 #H + elim (lsx_inv_bind … H) -H #HW1 #HT1 + @lsx_bind /2 width=1 by/ (**) (* explicit constructor *) + @lsx_flat [ /3 width=7 by lsx_lift_ge, ldrop_drop/ ] + @(lsx_leq_conf … (L.ⓓW1)) /3 width=1 by lcosx_pair, leq_succ/ +] +qed-. + +lemma lsx_cpx_trans_O: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → + G ⊢ ⬊*[h, g, T1, 0] L → G ⊢ ⬊*[h, g, T2, 0] L. +/2 width=3 by lsx_cpx_trans_lcosx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma new file mode 100644 index 000000000..435650bd1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma @@ -0,0 +1,109 @@ +(**************************************************************************) +(* ___ *) +(* ||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/sn_6.ma". +include "basic_2/substitution/lleq.ma". +include "basic_2/reduction/lpx.ma". + +(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) + +definition lsx: ∀h. sd h → relation4 ynat term genv lenv ≝ + λh,g,d,T,G. SN … (lpx h g G) (lleq d T). + +interpretation + "extended strong normalization (local environment)" + 'SN h g d T G L = (lsx h g T d G L). + +(* Basic eliminators ********************************************************) + +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, 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,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,G,T,d. G ⊢ ⬊*[h, g, T, d] ⋆. +#h #g #G #T #d @lsx_intro +#X #H #HT lapply (lpx_inv_atom1 … H) -H +#H destruct elim HT -HT // +qed. + +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 lpx_fwd_length, lleq_sort/ +qed. + +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 lpx_fwd_length, lleq_gref/ +qed. + +lemma lsx_ge_up: ∀h,g,G,L,T,U,dt,d,e. dt ≤ yinj d + yinj e → + ⇧[d, e] T ≡ U → G ⊢ ⬊*[h, g, U, dt] L → G ⊢ ⬊*[h, g, U, d] L. +#h #g #G #L #T #U #dt #d #e #Hdtde #HTU #H @(lsx_ind … H) -L +/5 width=7 by lsx_intro, lleq_ge_up/ +qed-. + +lemma lsx_ge: ∀h,g,G,L,T,d1,d2. d1 ≤ d2 → + G ⊢ ⬊*[h, g, T, d1] L → G ⊢ ⬊*[h, g, T, d2] L. +#h #g #G #L #T #d1 #d2 #Hd12 #H @(lsx_ind … H) -L +/5 width=7 by lsx_intro, lleq_ge/ +qed-. + +(* Basic forward lemmas *****************************************************) + +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,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,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,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,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_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_alt.ma new file mode 100644 index 000000000..cd7c83be9 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_alt.ma @@ -0,0 +1,116 @@ +(**************************************************************************) +(* ___ *) +(* ||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/snalt_6.ma". +include "basic_2/substitution/lleq_lleq.ma". +include "basic_2/computation/lpxs_lleq.ma". +include "basic_2/computation/lsx.ma". + +(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) + +(* alternative definition of lsx *) +definition lsxa: ∀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) alternative" + 'SNAlt h g d T G L = (lsxa h g T d G L). + +(* Basic eliminators ********************************************************) + +lemma lsxa_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, 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 lsxa_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. + +fact lsxa_intro_aux: ∀h,g,G,L1,T,d. + (∀L,L2. ⦃G, L⦄ ⊢ ➡*[h, g] L2 → L1 ⋕[T, d] L → (L1 ⋕[T, d] L2 → ⊥) → G ⊢ ⬊⬊*[h, g, T, d] L2) → + G ⊢ ⬊⬊*[h, g, T, d] L1. +/4 width=3 by lsxa_intro/ qed-. + +lemma lsxa_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 @(lsxa_ind … H) -L1 +#L1 #_ #IHL1 #L2 #HL12 @lsxa_intro +#K2 #HLK2 #HnLK2 elim (lleq_lpxs_trans … HLK2 … HL12) -HLK2 +/5 width=4 by lleq_canc_sn, lleq_trans/ +qed-. + +lemma lsxa_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 @(lsxa_ind … H) -L1 #L1 #HL1 #IHL1 #L2 #HL12 +elim (lleq_dec T L1 L2 d) /3 width=4 by lsxa_lleq_trans/ +qed-. + +lemma lsxa_intro_lpx: ∀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. +#h #g #G #L1 #T #d #IH @lsxa_intro_aux +#L #L2 #H @(lpxs_ind_dx … H) -L +[ #H destruct #H elim H // +| #L0 #L elim (lleq_dec T L1 L d) /3 width=1 by/ + #HnT #HL0 #HL2 #_ #HT #_ elim (lleq_lpx_trans … HL0 … HT) -L0 + #L0 #HL10 #HL0 @(lsxa_lpxs_trans … HL2) -HL2 + /5 width=3 by lsxa_lleq_trans, lleq_trans/ +] +qed-. + +(* Main properties **********************************************************) + +theorem lsx_lsxa: ∀h,g,G,L,T,d. G ⊢ ⬊*[h, g, T, d] L → G ⊢ ⬊⬊*[h, g, T, d] L. +#h #g #G #L #T #d #H @(lsx_ind … H) -L +/4 width=1 by lsxa_intro_lpx/ +qed. + +(* Main inversion lemmas ****************************************************) + +theorem lsxa_inv_lsx: ∀h,g,G,L,T,d. G ⊢ ⬊⬊*[h, g, T, d] L → G ⊢ ⬊*[h, g, T, d] L. +#h #g #G #L #T #d #H @(lsxa_ind … H) -L +/4 width=1 by lsx_intro, lpx_lpxs/ +qed-. + +(* Advanced properties ******************************************************) + +lemma lsx_intro_alt: ∀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. +/6 width=1 by lsxa_inv_lsx, lsx_lsxa, lsxa_intro/ qed. + +lemma lsx_lpxs_trans: ∀h,g,G,L1,T,d. G ⊢ ⬊*[h, g, T, d] L1 → + ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → G ⊢ ⬊*[h, g, T, d] L2. +/4 width=3 by lsxa_inv_lsx, lsx_lsxa, lsxa_lpxs_trans/ qed-. + +(* Advanced eliminators *****************************************************) + +lemma lsx_ind_alt: ∀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, d] L → R L. +#h #g #G #T #d #R #IH #L #H @(lsxa_ind h g G T d … L) +/4 width=1 by lsxa_inv_lsx, lsx_lsxa/ +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 new file mode 100644 index 000000000..7dc0b2a85 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma @@ -0,0 +1,59 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/csx_lpxs.ma". +include "basic_2/computation/lcosx_cpx.ma". + +(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) + +(* Advanced properties ******************************************************) + +lemma lsx_lref_be_lpxs: ∀h,g,I,G,K1,V,i,d. d ≤ yinj i → ⦃G, K1⦄ ⊢ ⬊*[h, g] V → + ∀K2. G ⊢ ⬊*[h, g, V, 0] K2 → ⦃G, K1⦄ ⊢ ➡*[h, g] K2 → + ∀L2. ⇩[i] L2 ≡ K2.ⓑ{I}V → G ⊢ ⬊*[h, g, #i, d] L2. +#h #g #I #G #K1 #V #i #d #Hdi #H @(csx_ind_alt … H) -V +#V0 #_ #IHV0 #K2 #H @(lsx_ind … H) -K2 +#K0 #HK0 #IHK0 #HK10 #L0 #HLK0 @lsx_intro +#L2 #HL02 #HnL02 elim (lpx_ldrop_conf … HLK0 … HL02) -HL02 +#Y #H #HLK2 elim (lpx_inv_pair1 … H) -H +#K2 #V2 #HK02 #HV02 #H destruct +elim (eq_term_dec V0 V2) #HnV02 destruct [ -IHV0 -HV02 -HK0 | -IHK0 -HnL02 -HLK0 ] +[ /4 width=8 by lpxs_strap1, lleq_lref/ +| @(IHV0 … HnV02 … HLK2) -IHV0 -HnV02 -HLK2 + /3 width=4 by lsx_cpx_trans_O, lsx_lpx_trans, lpxs_cpx_trans, lpxs_strap1/ (**) (* full auto too slow *) +] +qed. + +lemma lsx_lref_be: ∀h,g,I,G,K,V,i,d. d ≤ yinj i → ⦃G, K⦄ ⊢ ⬊*[h, g] V → + G ⊢ ⬊*[h, g, V, 0] K → + ∀L. ⇩[i] L ≡ K.ⓑ{I}V → G ⊢ ⬊*[h, g, #i, d] L. +/2 width=8 by lsx_lref_be_lpxs/ qed. + +(* Main properties **********************************************************) + +theorem csx_lsx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ∀d. G ⊢ ⬊*[h, g, T, d] L. +#h #g #G #L #T @(fqup_wf_ind_eq … G L T) -G -L -T +#Z #Y #X #IH #G #L * * // +[ #i #HG #HL #HT #H #d destruct + elim (lt_or_ge i (|L|)) /2 width=1 by lsx_lref_free/ + elim (ylt_split i d) /2 width=1 by lsx_lref_skip/ + #Hdi #Hi elim (ldrop_O1_lt … Hi) -Hi + #I #K #V #HLK lapply (csx_inv_lref_bind … HLK … H) -H + /4 width=6 by lsx_lref_be, fqup_lref/ +| #a #I #V #T #HG #HL #HT #H #d destruct + elim (csx_fwd_bind … H) -H /3 width=1 by lsx_bind/ +| #I #V #T #HG #HL #HT #H #d destruct + elim (csx_fwd_flat … H) -H /3 width=1 by lsx_flat/ +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma new file mode 100644 index 000000000..a520ba376 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma @@ -0,0 +1,96 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lleq_ldrop.ma". +include "basic_2/reduction/lpx_ldrop.ma". +include "basic_2/computation/lsx.ma". + +(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) + +(* Advanced properties ******************************************************) + +lemma lsx_lref_free: ∀h,g,G,L,d,i. |L| ≤ i → G ⊢ ⬊*[h, g, #i, d] L. +#h #g #G #L1 #d #i #HL1 @lsx_intro +#L2 #HL12 #H elim H -H +/4 width=6 by lpx_fwd_length, lleq_free, le_repl_sn_conf_aux/ +qed. + +lemma lsx_lref_skip: ∀h,g,G,L,d,i. yinj i < d → G ⊢ ⬊*[h, g, #i, d] L. +#h #g #G #L1 #d #i #HL1 @lsx_intro +#L2 #HL12 #H elim H -H +/3 width=4 by lpx_fwd_length, lleq_skip/ +qed. + +(* Advanced forward lemmas **************************************************) + +lemma lsx_fwd_lref_be: ∀h,g,I,G,L,d,i. d ≤ yinj i → G ⊢ ⬊*[h, g, #i, d] L → + ∀K,V. ⇩[i] L ≡ K.ⓑ{I}V → G ⊢ ⬊*[h, g, V, 0] K. +#h #g #I #G #L #d #i #Hdi #H @(lsx_ind … H) -L +#L1 #_ #IHL1 #K1 #V #HLK1 @lsx_intro +#K2 #HK12 #HnK12 lapply (ldrop_fwd_drop2 … HLK1) +#H2LK1 elim (ldrop_lpx_trans … H2LK1 … HK12) -H2LK1 -HK12 +#L2 #HL12 #H2LK2 #H elim (leq_ldrop_conf_be … H … HLK1) -H /2 width=1 by ylt_inj/ +#Y #_ #HLK2 lapply (ldrop_fwd_drop2 … HLK2) +#HY lapply (ldrop_mono … HY … H2LK2) -HY -H2LK2 #H destruct +/4 width=10 by lleq_inv_lref_ge/ +qed-. + +(* Properties on relocation *************************************************) + +lemma lsx_lift_le: ∀h,g,G,K,T,U,dt,d,e. dt ≤ yinj d → + ⇧[d, e] T ≡ U → G ⊢ ⬊*[h, g, T, dt] K → + ∀L. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⬊*[h, g, U, dt] L. +#h #g #G #K #T #U #dt #d #e #Hdtd #HTU #H @(lsx_ind … H) -K +#K1 #_ #IHK1 #L1 #HLK1 @lsx_intro +#L2 #HL12 #HnU elim (lpx_ldrop_conf … HLK1 … HL12) -HL12 +/4 width=10 by lleq_lift_le/ +qed-. + +lemma lsx_lift_ge: ∀h,g,G,K,T,U,dt,d,e. yinj d ≤ dt → + ⇧[d, e] T ≡ U → G ⊢ ⬊*[h, g, T, dt] K → + ∀L. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⬊*[h, g, U, dt + e] L. +#h #g #G #K #T #U #dt #d #e #Hddt #HTU #H @(lsx_ind … H) -K +#K1 #_ #IHK1 #L1 #HLK1 @lsx_intro +#L2 #HL12 #HnU elim (lpx_ldrop_conf … HLK1 … HL12) -HL12 +/4 width=9 by lleq_lift_ge/ +qed-. + +(* Inversion lemmas on relocation *******************************************) + +lemma lsx_inv_lift_le: ∀h,g,G,L,T,U,dt,d,e. dt ≤ yinj d → + ⇧[d, e] T ≡ U → G ⊢ ⬊*[h, g, U, dt] L → + ∀K. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⬊*[h, g, T, dt] K. +#h #g #G #L #T #U #dt #d #e #Hdtd #HTU #H @(lsx_ind … H) -L +#L1 #_ #IHL1 #K1 #HLK1 @lsx_intro +#K2 #HK12 #HnT elim (ldrop_lpx_trans … HLK1 … HK12) -HK12 +/4 width=10 by lleq_inv_lift_le/ +qed-. + +lemma lsx_inv_lift_be: ∀h,g,G,L,T,U,dt,d,e. yinj d ≤ dt → dt ≤ d + e → + ⇧[d, e] T ≡ U → G ⊢ ⬊*[h, g, U, dt] L → + ∀K. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⬊*[h, g, T, d] K. +#h #g #G #L #T #U #dt #d #e #Hddt #Hdtde #HTU #H @(lsx_ind … H) -L +#L1 #_ #IHL1 #K1 #HLK1 @lsx_intro +#K2 #HK12 #HnT elim (ldrop_lpx_trans … HLK1 … HK12) -HK12 +/4 width=11 by lleq_inv_lift_be/ +qed-. + +lemma lsx_inv_lift_ge: ∀h,g,G,L,T,U,dt,d,e. yinj d + yinj e ≤ dt → + ⇧[d, e] T ≡ U → G ⊢ ⬊*[h, g, U, dt] L → + ∀K. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⬊*[h, g, T, dt-e] K. +#h #g #G #L #T #U #dt #d #e #Hdedt #HTU #H @(lsx_ind … H) -L +#L1 #_ #IHL1 #K1 #HLK1 @lsx_intro +#K2 #HK12 #HnT elim (ldrop_lpx_trans … HLK1 … HK12) -HK12 +/4 width=9 by lleq_inv_lift_ge/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpx.ma new file mode 100644 index 000000000..37f4edfaf --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpx.ma @@ -0,0 +1,63 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lleq_lleq.ma". +include "basic_2/reduction/lpx_lleq.ma". +include "basic_2/computation/lsx.ma". + +(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) + +(* Advanced properties ******************************************************) + +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_lpx_trans … HLK2 … HL12) -HLK2 +/5 width=4 by lleq_canc_sn, lleq_trans/ +qed-. + +lemma lsx_lpx_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-. + +lemma lsx_leq_conf: ∀h,g,G,L1,T,d. G ⊢ ⬊*[h, g, T, d] L1 → + ∀L2. L1 ≃[d, ∞] L2 → G ⊢ ⬊*[h, g, T, d] L2. +#h #g #G #L1 #T #d #H @(lsx_ind … H) -L1 +#L1 #_ #IHL1 #L2 #HL12 @lsx_intro +#L3 #HL23 #HnL23 elim (leq_lpx_trans_lleq … HL12 … HL23) -HL12 -HL23 +#L0 #HL03 #HL10 #H elim (H T) -H /4 width=4 by/ +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 (lpx_inv_pair1 … H) -H +#L2 #V2 #HL12 #_ #H destruct +@(lsx_leq_conf … (L2.ⓑ{I}V1)) /2 width=1 by leq_succ/ +@IHL1 // #H @HT -IHL1 -HL12 -HT +@(lleq_leq_trans … (L2.ⓑ{I}V1)) +/2 width=2 by lleq_fwd_bind_dx, leq_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/computation/lsx_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma new file mode 100644 index 000000000..0accd974f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma @@ -0,0 +1,62 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/lpxs_lpxs.ma". +include "basic_2/computation/lsx_alt.ma". + +(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) + +(* Advanced properties ******************************************************) + +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_alt … H) -L1 +#L1 #HL1 #IHL1 #Y #T #H @(lsx_ind_alt … H) -Y +#Y #HY #IHY #L2 #H #HL12 destruct @lsx_intro_alt +#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_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_alt … H) -L1 +#L1 #HL1 #IHL1 #L2 #T #H @(lsx_ind_alt … H) -L2 +#L2 #HL2 #IHL2 #HL12 @lsx_intro_alt +#L0 #HL20 lapply (lpxs_trans … HL12 … HL20) +#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,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. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lcosx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lcosx.etc deleted file mode 100644 index f29f9837b..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lcosx.etc +++ /dev/null @@ -1,77 +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/lazycosn_5.ma". -include "basic_2/computation/lsx.ma". - -(* SN EXTENDED STRONGLY CONORMALIZING LOCAL ENVIRONMENTS ********************) - -inductive lcosx (h) (g) (G): relation2 ynat lenv ≝ -| lcosx_sort: ∀d. lcosx h g G d (⋆) -| lcosx_skip: ∀I,L,T. lcosx h g G 0 L → lcosx h g G 0 (L.ⓑ{I}T) -| lcosx_pair: ∀I,L,T,d. G ⊢ ⋕⬊*[h, g, T, d] L → - lcosx h g G d L → lcosx h g G (⫯d) (L.ⓑ{I}T) -. - -interpretation - "sn extended strong conormalization (local environment)" - 'LazyCoSN h g d G L = (lcosx h g G d L). - -(* Basic properties *********************************************************) - -lemma lcosx_O: ∀h,g,G,L. G ⊢ ⧤⬊*[h, g, 0] L. -#h #g #G #L elim L /2 width=1 by lcosx_skip/ -qed. - -lemma lcosx_ldrop_trans_lt: ∀h,g,G,L,d. G ⊢ ⧤⬊*[h, g, d] L → - ∀I,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → i < d → - G ⊢ ⧤⬊*[h, g, ⫰(d-i)] K ∧ G ⊢ ⋕⬊*[h, g, V, ⫰(d-i)] K. -#h #g #G #L #d #H elim H -L -d -[ #d #J #K #V #i #H elim (ldrop_inv_atom1 … H) -H #H destruct -| #I #L #T #_ #_ #J #K #V #i #_ #H elim (ylt_yle_false … H) -H // -| #I #L #T #d #HT #HL #IHL #J #K #V #i #H #Hid - elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK destruct - [ >ypred_succ /2 width=1 by conj/ - | lapply (ylt_pred … Hid ?) -Hid /2 width=1 by ylt_inj/ >ypred_succ #Hid - elim (IHL … HLK ?) -IHL -HLK yminus_SO2 // - <(ypred_succ d) in ⊢ (%→%→?); >yminus_pred /2 width=1 by ylt_inj, conj/ - ] -] -qed-. - -(* Basic inversion lemmas ***************************************************) - -fact lcosx_inv_succ_aux: ∀h,g,G,L,x. G ⊢ ⧤⬊*[h, g, x] L → ∀d. x = ⫯d → - L = ⋆ ∨ - ∃∃I,K,V. L = K.ⓑ{I}V & G ⊢ ⧤⬊*[h, g, d] K & - G ⊢ ⋕⬊*[h, g, V, d] K. -#h #g #G #L #d * -L -d /2 width=1 by or_introl/ -[ #I #L #T #_ #x #H elim (ysucc_inv_O_sn … H) -| #I #L #T #d #HT #HL #x #H <(ysucc_inj … H) -x - /3 width=6 by ex3_3_intro, or_intror/ -] -qed-. - -lemma lcosx_inv_succ: ∀h,g,G,L,d. G ⊢ ⧤⬊*[h, g, ⫯d] L → L = ⋆ ∨ - ∃∃I,K,V. L = K.ⓑ{I}V & G ⊢ ⧤⬊*[h, g, d] K & - G ⊢ ⋕⬊*[h, g, V, d] K. -/2 width=3 by lcosx_inv_succ_aux/ qed-. - -lemma lcosx_inv_pair: ∀h,g,I,G,L,T,d. G ⊢ ⧤⬊*[h, g, ⫯d] L.ⓑ{I}T → - G ⊢ ⧤⬊*[h, g, d] L ∧ G ⊢ ⋕⬊*[h, g, T, d] L. -#h #g #I #G #L #T #d #H elim (lcosx_inv_succ … H) -H -[ #H destruct -| * #Z #Y #X #H destruct /2 width=1 by conj/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lcosx_cpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lcosx_cpxs.etc deleted file mode 100644 index aef5014e7..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lcosx_cpxs.etc +++ /dev/null @@ -1,72 +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 "ground_2/ynat/ynat_max.ma". -include "basic_2/computation/lsx_ldrop.ma". -include "basic_2/computation/lsx_lpxs.ma". -include "basic_2/computation/lcosx.ma". - -(* SN EXTENDED STRONGLY CONORMALIZING LOCAL ENVIRONMENTS ********************) - -(* Properties on extended context-sensitive parallel computation for term ***) - -lemma lsx_cpx_trans_lcosx: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → - ∀d. G ⊢ ⧤⬊*[h, g, d] L → - G ⊢ ⋕⬊*[h, g, T1, d] L → G ⊢ ⋕⬊*[h, g, T2, d] L. -#h #g #G #L #T1 #T2 #H elim H -G -L -T1 -T2 // -[ #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #d #HL #H - elim (ylt_split i d) #Hdi [ -H | -HL ] - [ <(ymax_pre_sn d (⫯i)) /2 width=1 by ylt_fwd_le_succ/ - elim (lcosx_ldrop_trans_lt … HL … HLK) // -HL -Hdi - lapply (ldrop_fwd_drop2 … HLK) -HLK /3 width=7 by lsx_lift_ge/ - | lapply (lsx_fwd_lref_be … H … HLK) // -H -Hdi - lapply (ldrop_fwd_drop2 … HLK) -HLK - /4 width=10 by lsx_ge, lsx_lift_le/ - ] -| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #HL #H - elim (lsx_inv_bind … H) -H #HV1 #HT1 - @lsx_bind /2 width=2 by/ (**) (* explicit constructor *) - @(lsx_leq_conf … (L.ⓑ{I}V1)) /3 width=1 by lcosx_pair, leq_succ/ -| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #HL #H - elim (lsx_inv_flat … H) -H /3 width=1 by lsx_flat/ -| #G #L #V #U1 #U2 #T2 #_ #HTU2 #IHU12 #d #HL #H - elim (lsx_inv_bind … H) -H - /4 width=9 by lcosx_pair, lsx_inv_lift_ge, ldrop_drop/ -| #G #L #V #T1 #T2 #_ #IHT12 #d #HL #H - elim (lsx_inv_flat … H) -H /2 width=1 by/ -| #G #L #V1 #V2 #T #_ #IHV12 #d #HL #H - elim (lsx_inv_flat … H) -H /2 width=1 by/ -| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #d #HL #H - elim (lsx_inv_flat … H) -H #HV1 #H - elim (lsx_inv_bind … H) -H #HW1 #HT1 - @lsx_bind /3 width=1 by lsx_flat/ (**) (* explicit constructor *) - @(lsx_leq_conf … (L.ⓛW1)) /3 width=1 by lcosx_pair, leq_succ/ -| #a #G #L #V1 #V2 #U2 #W1 #W2 #T1 #T2 #_ #HVU2 #_ #_ #IHV12 #IHW12 #IHT12 #d #HL #H - elim (lsx_inv_flat … H) -H #HV1 #H - elim (lsx_inv_bind … H) -H #HW1 #HT1 - @lsx_bind /2 width=1 by/ (**) (* explicit constructor *) - @lsx_flat [ /3 width=7 by lsx_lift_ge, ldrop_drop/ ] - @(lsx_leq_conf … (L.ⓓW1)) /3 width=1 by lcosx_pair, leq_succ/ -] -qed-. - -lemma lsx_cpx_trans_O: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → - G ⊢ ⋕⬊*[h, g, T1, 0] L → G ⊢ ⋕⬊*[h, g, T2, 0] L. -/2 width=3 by lsx_cpx_trans_lcosx/ qed-. - -lemma lsx_cpxs_trans_O: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → - G ⊢ ⋕⬊*[h, g, T1, 0] L → G ⊢ ⋕⬊*[h, g, T2, 0] L. -#h #g #G #L #T1 #T2 #H @(cpxs_ind … H) -T2 -/3 width=3 by lsx_cpx_trans_O, cpxs_strap1/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lsx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lsx.etc deleted file mode 100644 index 59dda4e82..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lsx.etc +++ /dev/null @@ -1,103 +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/lazysn_6.ma". -include "basic_2/relocation/lleq.ma". -include "basic_2/computation/lpxs.ma". - -(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) - -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 d T G L = (lsx h g T d G L). - -(* Basic eliminators ********************************************************) - -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, 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,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,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,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,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. - -lemma lsx_ge_up: ∀h,g,G,L,T,U,dt,d,e. dt ≤ yinj d + yinj e → - ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, U, dt] L → G ⊢ ⋕⬊*[h, g, U, d] L. -#h #g #G #L #T #U #dt #d #e #Hdtde #HTU #H @(lsx_ind … H) -L -/5 width=7 by lsx_intro, lleq_ge_up/ -qed-. - -(* Basic forward lemmas *****************************************************) - -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,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,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,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,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/etc/lpx_sn/lsx_csx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lsx_csx.etc deleted file mode 100644 index 61dca7f92..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lsx_csx.etc +++ /dev/null @@ -1,60 +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/computation/csx_lpxs.ma". -include "basic_2/computation/lcosx_cpxs.ma". - -(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) - -(* Advanced properties ******************************************************) - -lemma lsx_lref_be_lpxs: ∀h,g,I,G,K1,V,i,d. d ≤ yinj i → ⦃G, K1⦄ ⊢ ⬊*[h, g] V → - ∀K2. G ⊢ ⋕⬊*[h, g, V, 0] K2 → ⦃G, K1⦄ ⊢ ➡*[h, g] K2 → - ∀L2. ⇩[i] L2 ≡ K2.ⓑ{I}V → G ⊢ ⋕⬊*[h, g, #i, d] L2. -#h #g #I #G #K1 #V #i #d #Hdi #H @(csx_ind_alt … H) -V -#V0 #_ #IHV0 #K2 #H @(lsx_ind … H) -K2 -#K0 #HK0 #IHK0 #HK10 #L0 #HLK0 @lsx_intro -#L2 #HL02 #HnL02 elim (lpxs_ldrop_conf … HLK0 … HL02) -HL02 -#Y #H #HLK2 elim (lpxs_inv_pair1 … H) -H -#K2 #V2 #HK02 #HV02 #H destruct -lapply (lpxs_trans … HK10 … HK02) #HK12 -elim (eq_term_dec V0 V2) #HnV02 destruct [ -IHV0 -HV02 -HK0 -HK10 | -IHK0 -HnL02 -HLK0 ] -[ /4 width=8 by lleq_lref/ -| @(IHV0 … HnV02 … HK12 … HLK2) -IHV0 -HnV02 -HK12 -HLK2 - /3 width=4 by lsx_cpxs_trans_O, lsx_lpxs_trans, lpxs_cpxs_trans/ (**) (* full auto too slow *) -] -qed. - -lemma lsx_lref_be: ∀h,g,I,G,K,V,i,d. d ≤ yinj i → ⦃G, K⦄ ⊢ ⬊*[h, g] V → - G ⊢ ⋕⬊*[h, g, V, 0] K → - ∀L. ⇩[i] L ≡ K.ⓑ{I}V → G ⊢ ⋕⬊*[h, g, #i, d] L. -/2 width=8 by lsx_lref_be_lpxs/ qed. - -(* Main properties **********************************************************) - -theorem csx_lsx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ∀d. G ⊢ ⋕⬊*[h, g, T, d] L. -#h #g #G #L #T @(fqup_wf_ind_eq … G L T) -G -L -T -#Z #Y #X #IH #G #L * * // -[ #i #HG #HL #HT #H #d destruct - elim (lt_or_ge i (|L|)) /2 width=1 by lsx_lref_free/ - elim (ylt_split i d) /2 width=1 by lsx_lref_skip/ - #Hdi #Hi elim (ldrop_O1_lt … Hi) -Hi - #I #K #V #HLK lapply (csx_inv_lref_bind … HLK … H) -H - /4 width=6 by lsx_lref_be, fqup_lref/ -| #a #I #V #T #HG #HL #HT #H #d destruct - elim (csx_fwd_bind … H) -H /3 width=1 by lsx_bind/ -| #I #V #T #HG #HL #HT #H #d destruct - elim (csx_fwd_flat … H) -H /3 width=1 by lsx_flat/ -] -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lsx_ldrop.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lsx_ldrop.etc deleted file mode 100644 index 9bd29a5f1..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lsx_ldrop.etc +++ /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/relocation/lleq_ldrop.ma". -include "basic_2/computation/lpxs_ldrop.ma". -include "basic_2/computation/lsx.ma". - -(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) - -(* Advanced properties ******************************************************) - -lemma lsx_lref_free: ∀h,g,G,L,d,i. |L| ≤ i → G ⊢ ⋕⬊*[h, g, #i, d] L. -#h #g #G #L1 #d #i #HL1 @lsx_intro -#L2 #HL12 #H elim H -H -/4 width=6 by lpxs_fwd_length, lleq_free, le_repl_sn_conf_aux/ -qed. - -lemma lsx_lref_skip: ∀h,g,G,L,d,i. yinj i < d → G ⊢ ⋕⬊*[h, g, #i, d] L. -#h #g #G #L1 #d #i #HL1 @lsx_intro -#L2 #HL12 #H elim H -H -/3 width=4 by lpxs_fwd_length, lleq_skip/ -qed. - -(* Properties on relocation *************************************************) - -lemma lsx_lift_le: ∀h,g,G,K,T,U,dt,d,e. dt ≤ yinj d → - ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, T, dt] K → - ∀L. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, U, dt] L. -#h #g #G #K #T #U #dt #d #e #Hdtd #HTU #H @(lsx_ind … H) -K -#K1 #_ #IHK1 #L1 #HLK1 @lsx_intro -#L2 #HL12 #HnU elim (lpxs_ldrop_conf … HLK1 … HL12) -HL12 -/4 width=10 by lleq_lift_le/ -qed-. - -lemma lsx_lift_ge: ∀h,g,G,K,T,U,dt,d,e. yinj d ≤ dt → - ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, T, dt] K → - ∀L. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, U, dt + e] L. -#h #g #G #K #T #U #dt #d #e #Hddt #HTU #H @(lsx_ind … H) -K -#K1 #_ #IHK1 #L1 #HLK1 @lsx_intro -#L2 #HL12 #HnU elim (lpxs_ldrop_conf … HLK1 … HL12) -HL12 -/4 width=9 by lleq_lift_ge/ -qed-. - -(* Inversion lemmas on relocation *******************************************) - -lemma lsx_inv_lift_le: ∀h,g,G,L,T,U,dt,d,e. dt ≤ yinj d → - ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, U, dt] L → - ∀K. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, T, dt] K. -#h #g #G #L #T #U #dt #d #e #Hdtd #HTU #H @(lsx_ind … H) -L -#L1 #_ #IHL1 #K1 #HLK1 @lsx_intro -#K2 #HK12 #HnT elim (ldrop_lpxs_trans … HLK1 … HK12) -HK12 -/4 width=10 by lleq_inv_lift_le/ -qed-. - -lemma lsx_inv_lift_be: ∀h,g,G,L,T,U,dt,d,e. yinj d ≤ dt → dt ≤ d + e → - ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, U, dt] L → - ∀K. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, T, d] K. -#h #g #G #L #T #U #dt #d #e #Hddt #Hdtde #HTU #H @(lsx_ind … H) -L -#L1 #_ #IHL1 #K1 #HLK1 @lsx_intro -#K2 #HK12 #HnT elim (ldrop_lpxs_trans … HLK1 … HK12) -HK12 -/4 width=11 by lleq_inv_lift_be/ -qed-. - -lemma lsx_inv_lift_ge: ∀h,g,G,L,T,U,dt,d,e. yinj d + yinj e ≤ dt → - ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, U, dt] L → - ∀K. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, T, dt-e] K. -#h #g #G #L #T #U #dt #d #e #Hdedt #HTU #H @(lsx_ind … H) -L -#L1 #_ #IHL1 #K1 #HLK1 @lsx_intro -#K2 #HK12 #HnT elim (ldrop_lpxs_trans … HLK1 … HK12) -HK12 -/4 width=9 by lleq_inv_lift_ge/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lsx_lpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lsx_lpxs.etc deleted file mode 100644 index 9762de28b..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lsx_lpxs.etc +++ /dev/null @@ -1,124 +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/lleq_lleq.ma". -include "basic_2/computation/lpxs_lleq.ma". -include "basic_2/computation/lpxs_lpxs.ma". -include "basic_2/computation/lsx.ma". - -(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) - -(* Advanced properties ******************************************************) - -lemma lsx_leq_conf: ∀h,g,G,L1,T,d. G ⊢ ⋕⬊*[h, g, T, d] L1 → - ∀L2. L1 ≃[d, ∞] L2 → G ⊢ ⋕⬊*[h, g, T, d] L2. -#h #g #G #L1 #T #d #H @(lsx_ind … H) -L1 -#L1 #_ #IHL1 #L2 #HL12 @lsx_intro -#L3 #HL23 #HnL23 elim (leq_lpxs_trans_lleq … HL12 … HL23) -HL12 -HL23 -#L0 #HL03 #HL10 #H elim (H T) -H /4 width=4 by/ -qed-. - -lemma lsx_ge: ∀h,g,G,L,T,d1,d2. d1 ≤ d2 → - G ⊢ ⋕⬊*[h, g, T, d1] L → G ⊢ ⋕⬊*[h, g, T, d2] L. -#h #g #G #L #T #d1 #d2 #Hd12 #H @(lsx_ind … H) -L -/5 width=7 by lsx_intro, lleq_ge/ -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 … HLK2 … HL12) -HLK2 -/5 width=4 by lleq_canc_sn, lleq_trans/ -qed-. - -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_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 [ -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,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_lref_be: ∀h,g,I,G,L,d,i. d ≤ yinj i → G ⊢ ⋕⬊*[h, g, #i, d] L → - ∀K,V. ⇩[i] L ≡ K.ⓑ{I}V → G ⊢ ⋕⬊*[h, g, V, 0] K. -#h #g #I #G #L #d #i #Hdi #H @(lsx_ind … H) -L -#L1 #_ #IHL1 #K1 #V #HLK1 @lsx_intro -#K2 #HK12 #HnK12 lapply (ldrop_fwd_drop2 … HLK1) -#H2LK1 elim (ldrop_lpxs_trans … H2LK1 … HK12) -H2LK1 -HK12 -#L2 #HL12 #H2LK2 #H elim (leq_ldrop_conf_be … H … HLK1) -H /2 width=1 by ylt_inj/ -#Y #_ #HLK2 lapply (ldrop_fwd_drop2 … HLK2) -#HY lapply (ldrop_mono … HY … H2LK2) -HY -H2LK2 #H destruct -/4 width=10 by lleq_inv_lref_ge/ -qed-. - -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_leq_conf … (L2.ⓑ{I}V1)) /2 width=1 by leq_succ/ -@IHL1 // #H @HT -IHL1 -HL12 -HT -@(lleq_leq_trans … (L2.ⓑ{I}V1)) -/2 width=2 by lleq_fwd_bind_dx, leq_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/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt index 6c685b0bf..9a3e5d490 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/names.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt @@ -80,6 +80,7 @@ q: restricted reduction r: reduction s: substitution u: supclosure +w: reserved for generic pointwise extension x: extended reduction y: extended substitution @@ -93,3 +94,4 @@ q: reflexive closure (question) r: proper multiple step (restricted) (restricted) s: reflexive transitive closure (star) u: proper single step (restricted) (unit) +x: reserved for generic pointwise extension diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/cosn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/cosn_5.ma new file mode 100644 index 000000000..01a9040a6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/cosn_5.ma @@ -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( G ⊢ ~ ⬊ * break [ term 46 h , break term 46 g , break term 46 d ] break term 46 L )" + non associative with precedence 45 + for @{ 'CoSN $h $g $d $G $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazycosn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazycosn_5.ma deleted file mode 100644 index 55c37a8fd..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazycosn_5.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( G ⊢ ⧤ ⬊ * break [ term 46 h , break term 46 g , break term 46 d ] break term 46 L )" - non associative with precedence 45 - for @{ 'LazyCoSN $h $g $d $G $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_6.ma new file mode 100644 index 000000000..95bec1559 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_6.ma @@ -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( G ⊢ ⬊ * break [ term 46 h , break term 46 g , break term 46 T , break term 46 d ] break term 46 L )" + non associative with precedence 45 + for @{ 'SN $h $g $T $d $G $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_6.ma new file mode 100644 index 000000000..f1baa6805 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_6.ma @@ -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( G ⊢ ⬊ ⬊ * break [ term 46 h , break term 46 g , break term 46 T , break term 46 d ] break term 46 L )" + non associative with precedence 45 + for @{ 'SNAlt $h $g $T $d $G $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma index d3f594317..8d3f8d68c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma @@ -12,7 +12,9 @@ (* *) (**************************************************************************) +include "basic_2/substitution/lleq_leq.ma". include "basic_2/substitution/lleq_ldrop.ma". +include "basic_2/reduction/cpx_leq.ma". include "basic_2/reduction/lpx_ldrop.ma". (* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) @@ -85,3 +87,33 @@ elim (fqus_inv_gen … H) -H | * #HG #HL #HT destruct /2 width=4 by ex3_intro/ ] qed-. + +fact leq_lpx_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. L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L). +#h #g #G #L1 #L0 #d #e #H elim H -L1 -L0 -d -e +[ #d #e #_ #L2 #H >(lpx_inv_atom1 … H) -H + /3 width=5 by ex3_intro, conj/ +| #I1 #I0 #L1 #L0 #V1 #V0 #_ #_ #He destruct +| #I #L1 #L0 #V1 #e #HL10 #IHL10 #He #Y #H + elim (lpx_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.ⓑ{I}V2)) /3 width=3 by lpx_pair, leq_cpx_trans, leq_pair/ + #T elim (IH T) #HL0dx #HL0sn + @conj #H @(lleq_leq_repl … H) -H /3 width=1 by leq_sym, leq_pair_O_Y/ +| #I1 #I0 #L1 #L0 #V1 #V0 #d #e #HL10 #IHL10 #He #Y #H + elim (lpx_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 lpx_pair, leq_succ/ + #T elim (IH T) #HL0dx #HL0sn + @conj #H @(lleq_leq_repl … H) -H /3 width=1 by leq_sym, leq_succ/ +] +qed-. + +lemma leq_lpx_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. L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L). +/2 width=1 by leq_lpx_trans_lleq_aux/ 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 0152a3d8a..0fc5b655c 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,8 +84,9 @@ table { } ] [ { "strongly normalizing extended computation" * } { -(* [ "lcosx ( ? ⊢ ⧤⬊*[?,?,?] ? )" "lcosx_cpxs" * ] *) + [ "lcosx ( ? ⊢ ~⬊*[?,?,?] ? )" "lcosx_cpx" * ] [ "llsx ( ? ⊢ ⋕⬊*[?,?,?,?] ? )" "llsx_alt ( ? ⊢ ⋕⬊⬊*[?,?,?,?] ? )" "llsx_ldrop" + "llsx_llpx" + "llsx_llpxs" + "llsx_csx" * ] + [ "lsx ( ? ⊢ ⬊*[?,?,?,?] ? )" "lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? )" "lsx_ldrop" + "lsx_lpx" + "lsx_lpxs" + "llsx_csx" * ] [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tstc_vector" + "csx_aaa" * ] [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lpx" + "csx_llpx" + "csx_lpxs" + "csx_llpxs" + "csx_fpbs" * ] }