From c69a33bba2ae2f37953737940fb45149136cf054 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 13 Apr 2014 15:03:16 +0000 Subject: [PATCH] we restored the strong normalization of extended computation for local environments with some important updates from the "lazy version" --- .../lpx_sn/lcosx.etc => computation/lcosx.ma} | 28 ++-- .../lcosx_cpx.ma} | 15 +-- .../lpx_sn/lsx.etc => computation/lsx.ma} | 60 +++++---- .../basic_2/computation/lsx_alt.ma | 116 ++++++++++++++++ .../lsx_csx.etc => computation/lsx_csx.ma} | 25 ++-- .../lsx_ldrop.ma} | 56 +++++--- .../basic_2/computation/lsx_lpx.ma | 63 +++++++++ .../basic_2/computation/lsx_lpxs.ma | 62 +++++++++ .../basic_2/etc/lpx_sn/lsx_lpxs.etc | 124 ------------------ .../contribs/lambdadelta/basic_2/names.txt | 2 + .../relations/{lazycosn_5.ma => cosn_5.ma} | 4 +- .../basic_2/notation/relations/sn_6.ma | 19 +++ .../basic_2/notation/relations/snalt_6.ma | 19 +++ .../lambdadelta/basic_2/reduction/lpx_lleq.ma | 32 +++++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 3 +- 15 files changed, 416 insertions(+), 212 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/lcosx.etc => computation/lcosx.ma} (72%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/lcosx_cpxs.etc => computation/lcosx_cpx.ma} (84%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/lsx.etc => computation/lsx.ma} (58%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/lsx_alt.ma rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/lsx_csx.etc => computation/lsx_csx.ma} (75%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/lsx_ldrop.etc => computation/lsx_ldrop.ma} (54%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpx.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lsx_lpxs.etc rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{lazycosn_5.ma => cosn_5.ma} (88%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_6.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_6.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lcosx.etc b/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx.ma similarity index 72% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lcosx.etc rename to matita/matita/contribs/lambdadelta/basic_2/computation/lcosx.ma index f29f9837b..a1e27d0b1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lcosx.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/lazycosn_5.ma". +include "basic_2/notation/relations/cosn_5.ma". include "basic_2/computation/lsx.ma". (* SN EXTENDED STRONGLY CONORMALIZING LOCAL ENVIRONMENTS ********************) @@ -20,23 +20,23 @@ include "basic_2/computation/lsx.ma". 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_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). + '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. +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 → +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. + 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 // @@ -52,10 +52,10 @@ qed-. (* Basic inversion lemmas ***************************************************) -fact lcosx_inv_succ_aux: ∀h,g,G,L,x. G ⊢ ⧤⬊*[h, g, x] L → ∀d. x = ⫯d → +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. + ∃∃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 @@ -63,13 +63,13 @@ fact lcosx_inv_succ_aux: ∀h,g,G,L,x. G ⊢ ⧤⬊*[h, g, x] L → ∀d. x = ] 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. +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. +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/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lcosx_cpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx_cpx.ma similarity index 84% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lcosx_cpxs.etc rename to matita/matita/contribs/lambdadelta/basic_2/computation/lcosx_cpx.ma index aef5014e7..e78ae1b4f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lcosx_cpxs.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx_cpx.ma @@ -14,16 +14,17 @@ 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 computation for term ***) +(* 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. + ∀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 ] @@ -62,11 +63,5 @@ lemma lsx_cpx_trans_lcosx: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → 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. + 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/computation/lsx.ma similarity index 58% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lsx.etc rename to matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma index 59dda4e82..435650bd1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lsx.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma @@ -12,27 +12,27 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/lazysn_6.ma". -include "basic_2/relocation/lleq.ma". -include "basic_2/computation/lpxs.ma". +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 … (lpxs h g G) (lleq d T). + λh,g,d,T,G. SN … (lpx 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). + '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) → + (∀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. + ∀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-. @@ -40,64 +40,70 @@ 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. + (∀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] ⋆. +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 +#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. +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/ +/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. +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/ +/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. + ⇧[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. +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. +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. +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. +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. +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/etc/lpx_sn/lsx_csx.etc b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma similarity index 75% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lsx_csx.etc rename to matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma index 61dca7f92..7dc0b2a85 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lsx_csx.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma @@ -13,37 +13,36 @@ (**************************************************************************) include "basic_2/computation/csx_lpxs.ma". -include "basic_2/computation/lcosx_cpxs.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. + ∀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 +#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 -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 *) +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. + 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. +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 diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lsx_ldrop.etc b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma similarity index 54% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lsx_ldrop.etc rename to matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma index 9bd29a5f1..a520ba376 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lsx_ldrop.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma @@ -12,71 +12,85 @@ (* *) (**************************************************************************) -include "basic_2/relocation/lleq_ldrop.ma". -include "basic_2/computation/lpxs_ldrop.ma". +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. +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/ +/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. +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/ +/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. + ⇧[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 +#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. + ⇧[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 +#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. + ⇧[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 +#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. + ⇧[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 +#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. + ⇧[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 +#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/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/lazycosn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/cosn_5.ma similarity index 88% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazycosn_5.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/cosn_5.ma index 55c37a8fd..01a9040a6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazycosn_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/cosn_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( G ⊢ ⧤ ⬊ * break [ term 46 h , break term 46 g , break term 46 d ] break term 46 L )" +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 }. + for @{ 'CoSN $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" * ] } -- 2.39.2