From 5f1066ffb3c6ed53f9bf17ae2a81a9c9db32dba7 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 16 Feb 2014 18:59:26 +0000 Subject: [PATCH] - improved definition of lsx allows more invariants - some additions - we parked some unnecessary planes (cny, cpye) --- .../basic_2/computation/cpxs_cpys.ma | 24 +++++ .../basic_2/computation/lpxs_lleq.ma | 63 +++++++++---- .../lambdadelta/basic_2/computation/lsx.ma | 62 ++++++------- .../basic_2/computation/lsx_csx.ma | 45 ++++++++++ .../basic_2/computation/lsx_lpxs.ma | 88 +++++++++++++++---- .../{relocation/cny.ma => etc/cny/cny.etc} | 0 .../cny_lift.ma => etc/cny/cny_lift.etc} | 0 .../lambdadelta/basic_2/etc/cny/cpx_cpzs.etc | 73 +++++++++++++++ .../cpye.ma => etc/cny/cpye.etc} | 7 ++ .../cpye_alt.ma => etc/cny/cpye_alt.etc} | 0 .../cpye_cpye.ma => etc/cny/cpye_cpye.etc} | 0 .../cpye_lift.ma => etc/cny/cpye_lift.etc} | 0 .../cpys_cny.ma => etc/cny/cpys_cny.etc} | 0 .../lambdadelta/basic_2/etc/cny/cpzs.etc | 83 +++++++++++++++++ .../lleq_cpye.ma => etc/cny/lleq_cpye.etc} | 0 .../lpx_cpye.ma => etc/cny/lpx_cpye.etc} | 0 .../lpxs_cpye.ma => etc/cny/lpxs_cpye.etc} | 0 .../basic_2/etc/cny/pdeltaconvstar_6.etc | 19 ++++ .../cny/psubsteval_6.etc} | 0 .../cny/psubstevalalt_6.etc} | 0 .../cny/psubstnormal_5.etc} | 0 .../basic_2/etc/llneq/lazynegatedeq_4.etc | 19 ++++ .../basic_2/etc/llneq/lazynegatedeqalt_4.etc | 19 ++++ .../lambdadelta/basic_2/etc/llneq/llneq.etc | 25 ++++++ .../basic_2/etc/llneq/llneq_alt.etc | 68 ++++++++++++++ .../basic_2/etc/llneq/llneq_ext.etc | 33 +++++++ .../basic_2/etc/llneq/lpxs_llneq.etc | 67 ++++++++++++++ .../relations/{lazysn_5.ma => lazysn_6.ma} | 4 +- .../lambdadelta/basic_2/reduction/cpx_cpys.ma | 14 +++ .../lambdadelta/basic_2/reduction/lpx_lleq.ma | 25 ++++++ .../lambdadelta/basic_2/relocation/lsuby.ma | 19 ++-- .../lambdadelta/basic_2/web/basic_2_src.tbl | 20 ++--- 32 files changed, 687 insertions(+), 90 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpys.ma rename matita/matita/contribs/lambdadelta/basic_2/{relocation/cny.ma => etc/cny/cny.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation/cny_lift.ma => etc/cny/cny_lift.etc} (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpx_cpzs.etc rename matita/matita/contribs/lambdadelta/basic_2/{substitution/cpye.ma => etc/cny/cpye.etc} (92%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution/cpye_alt.ma => etc/cny/cpye_alt.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution/cpye_cpye.ma => etc/cny/cpye_cpye.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution/cpye_lift.ma => etc/cny/cpye_lift.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution/cpys_cny.ma => etc/cny/cpys_cny.etc} (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpzs.etc rename matita/matita/contribs/lambdadelta/basic_2/{substitution/lleq_cpye.ma => etc/cny/lleq_cpye.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/lpx_cpye.ma => etc/cny/lpx_cpye.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation/lpxs_cpye.ma => etc/cny/lpxs_cpye.etc} (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cny/pdeltaconvstar_6.etc rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/psubsteval_6.ma => etc/cny/psubsteval_6.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/psubstevalalt_6.ma => etc/cny/psubstevalalt_6.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/psubstnormal_5.ma => etc/cny/psubstnormal_5.etc} (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/llneq/lazynegatedeq_4.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/llneq/lazynegatedeqalt_4.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/llneq/llneq.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/llneq/llneq_alt.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/llneq/llneq_ext.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/llneq/lpxs_llneq.etc rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{lazysn_5.ma => lazysn_6.ma} (92%) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpys.ma new file mode 100644 index 000000000..881030572 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpys.ma @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/reduction/cpx_cpys.ma". +include "basic_2/computation/cpxs.ma". + +(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) + +(* Properties on local environment refinement for extended substitution *****) + +lemma lsuby_cpxs_trans: ∀h,g,G. lsub_trans … (cpxs h g G) (lsuby 0 (∞)). +/3 width=5 by lsuby_cpx_trans, LTC_lsub_trans/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma index a919045df..2ca1e193d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma @@ -12,32 +12,23 @@ (* *) (**************************************************************************) -include "basic_2/substitution/lleq_ext.ma". +include "basic_2/reduction/lpx_lleq.ma". +include "basic_2/computation/cpxs_cpys.ma". include "basic_2/computation/lpxs_ldrop.ma". include "basic_2/computation/lpxs_cpxs.ma". (* SN EXTENDED PARALLEL COMPUTATION FOR LOCAL ENVIRONMENTS ******************) -(* Advanced properties ******************************************************) +(* Properties on lazy equivalence for local environments ********************) -axiom lleq_lpxs_trans: ∀h,g,G,L1,L2,T,d. L1 ⋕[T, d] L2 → ∀K2. ⦃G, L2⦄ ⊢ ➡*[h, g] K2 → +lemma lleq_lpxs_trans: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡*[h, g] K2 → + ∀L1,T,d. L1 ⋕[T, d] L2 → ∃∃K1. ⦃G, L1⦄ ⊢ ➡*[h, g] K1 & K1 ⋕[T, d] K2. -(* -#h #g #G #L1 #L2 #T #d #H @(lleq_ind_alt … H) -L1 -L2 -T -d -[ -| -| -| -| -| #a #I #L1 #L2 #V #T #d #_ #_ #IHV #IHT #K2 #HLK2 - elim (IHV … HLK2) -IHV #KV #HLKV #HV - elim (IHT (K2.ⓑ{I}V)) -IHT /2 width=1 by lpxs_pair_refl/ -HLK2 #Y #H #HT - elim (lpxs_inv_pair1 … H) -H #KT #VT #HLKT #_ #H destruct - -#h #g #G #L1 #L2 #T #d * #HL12 #IH #K2 #HLK2 -*) - -(* Properties on lazy equivalence for local environments ********************) +#h #g #G #L2 #K2 #H @(lpxs_ind … H) -K2 /2 width=3 by ex2_intro/ +#K #K2 #_ #HK2 #IH #L1 #T #d #HT elim (IH … HT) -L2 +#L #HL1 #HT elim (lleq_lpx_trans … HK2 … HT) -K +/3 width=3 by lpxs_strap1, ex2_intro/ +qed-. lemma lpxs_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 → @@ -101,3 +92,37 @@ elim (fqus_inv_gen … H) -H | * #HG #HL #HT destruct /2 width=4 by ex3_intro/ ] qed-. + +fact lsuby_lpxs_trans_lleq_aux: ∀h,g,G,L1,L0,d,e. L1 ⊑×[d, e] L0 → e = ∞ → + ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, g] L2 → + ∃∃L. L ⊑×[d, e] L2 & ⦃G, L1⦄ ⊢ ➡*[h, g] L & + (∀T. |L1| = |L0| → |L| = |L2| → L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L). +#h #g #G #L1 #L0 #d #e #H elim H -L1 -L0 -d -e +[ #L1 #d #e #_ #L2 #H >(lpxs_inv_atom1 … H) -H + /3 width=5 by ex3_intro, conj/ +| #I1 #I0 #L1 #L0 #V1 #V0 #_ #_ #He destruct +| #I1 #I0 #L1 #L0 #V1 #e #HL10 #IHL10 #He #Y #H + elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct + lapply (ysucc_inv_Y_dx … He) -He #He + elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH + @(ex3_intro … (L.ⓑ{I1}V2)) /3 width=3 by lpxs_pair, lsuby_cpxs_trans, lsuby_pair/ + #T #H1 #H2 lapply (injective_plus_l … H1) lapply (injective_plus_l … H2) -H1 -H2 + #H1 #H2 elim (IH T) // #HL0dx #HL0sn + @conj #H @(lleq_lsuby_repl … H) -H normalize + /3 width=1 by lsuby_sym, lsuby_pair_O_Y/ +| #I1 #I0 #L1 #L0 #V1 #V0 #d #e #HL10 #IHL10 #He #Y #H + elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct + elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH + @(ex3_intro … (L.ⓑ{I1}V1)) /3 width=1 by lpxs_pair, lsuby_succ/ + #T #H1 #H2 lapply (injective_plus_l … H1) lapply (injective_plus_l … H2) -H1 -H2 + #H1 #H2 elim (IH T) // #HL0dx #HL0sn + @conj #H @(lleq_lsuby_repl … H) -H + /3 width=1 by lsuby_sym, lsuby_succ/ normalize // +] +qed-. + +lemma lsuby_lpxs_trans_lleq: ∀h,g,G,L1,L0,d. L1 ⊑×[d, ∞] L0 → + ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, g] L2 → + ∃∃L. L ⊑×[d, ∞] L2 & ⦃G, L1⦄ ⊢ ➡*[h, g] L & + (∀T. |L1| = |L0| → |L| = |L2| → L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L). +/2 width=1 by lsuby_lpxs_trans_lleq_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma index 38e185a86..9661a8839 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma @@ -12,86 +12,86 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/lazysn_5.ma". +include "basic_2/notation/relations/lazysn_6.ma". include "basic_2/substitution/lleq.ma". include "basic_2/computation/lpxs.ma". (* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) -definition lsx: ∀h. sd h → relation3 term genv lenv ≝ - λh,g,T,G. SN … (lpxs h g G) (lleq 0 T). +definition lsx: ∀h. sd h → relation4 ynat term genv lenv ≝ + λh,g,d,T,G. SN … (lpxs h g G) (lleq d T). interpretation "extended strong normalization (local environment)" - 'LazySN h g T G L = (lsx h g T G L). + 'LazySN h g d T G L = (lsx h g T d G L). (* Basic eliminators ********************************************************) -lemma lsx_ind: ∀h,g,T,G. ∀R:predicate lenv. - (∀L1. G ⊢ ⋕⬊*[h, g, T] L1 → - (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T, 0] L2 → ⊥) → R L2) → +lemma lsx_ind: ∀h,g,G,T,d. ∀R:predicate lenv. + (∀L1. G ⊢ ⋕⬊*[h, g, T, d] L1 → + (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T, d] L2 → ⊥) → R L2) → R L1 ) → - ∀L. G ⊢ ⋕⬊*[h, g, T] L → R L. -#h #g #T #G #R #H0 #L1 #H elim H -L1 + ∀L. G ⊢ ⋕⬊*[h, g, T, d] L → R L. +#h #g #G #T #d #R #H0 #L1 #H elim H -L1 /5 width=1 by lleq_sym, SN_intro/ qed-. (* Basic properties *********************************************************) -lemma lsx_intro: ∀h,g,T,G,L1. - (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T, 0] L2 → ⊥) → G ⊢ ⋕⬊*[h, g, T] L2) → - G ⊢ ⋕⬊*[h, g, T] L1. +lemma lsx_intro: ∀h,g,G,L1,T,d. + (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T, d] L2 → ⊥) → G ⊢ ⋕⬊*[h, g, T, d] L2) → + G ⊢ ⋕⬊*[h, g, T, d] L1. /5 width=1 by lleq_sym, SN_intro/ qed. -lemma lsx_atom: ∀h,g,T,G. G ⊢ ⋕⬊*[h, g, T] ⋆. -#h #g #T #G @lsx_intro +lemma lsx_atom: ∀h,g,G,T,d. G ⊢ ⋕⬊*[h, g, T, d] ⋆. +#h #g #G #T #d @lsx_intro #X #H #HT lapply (lpxs_inv_atom1 … H) -H #H destruct elim HT -HT // qed. -lemma lsx_sort: ∀h,g,G,L,k. G ⊢ ⋕⬊*[h, g, ⋆k] L. -#h #g #G #L1 #k @lsx_intro +lemma lsx_sort: ∀h,g,G,L,d,k. G ⊢ ⋕⬊*[h, g, ⋆k, d] L. +#h #g #G #L1 #d #k @lsx_intro #L2 #HL12 #H elim H -H /3 width=4 by lpxs_fwd_length, lleq_sort/ qed. -lemma lsx_gref: ∀h,g,G,L,p. G ⊢ ⋕⬊*[h, g, §p] L. -#h #g #G #L1 #p @lsx_intro +lemma lsx_gref: ∀h,g,G,L,d,p. G ⊢ ⋕⬊*[h, g, §p, d] L. +#h #g #G #L1 #d #p @lsx_intro #L2 #HL12 #H elim H -H /3 width=4 by lpxs_fwd_length, lleq_gref/ qed. (* Basic forward lemmas *****************************************************) -lemma lsx_fwd_bind_sn: ∀h,g,a,I,G,L,V,T. G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V.T] L → - G ⊢ ⋕⬊*[h, g, V] L. -#h #g #a #I #G #L #V #T #H @(lsx_ind … H) -L +lemma lsx_fwd_bind_sn: ∀h,g,a,I,G,L,V,T,d. G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V.T, d] L → + G ⊢ ⋕⬊*[h, g, V, d] L. +#h #g #a #I #G #L #V #T #d #H @(lsx_ind … H) -L #L1 #_ #IHL1 @lsx_intro #L2 #HL12 #HV @IHL1 /3 width=4 by lleq_fwd_bind_sn/ qed-. -lemma lsx_fwd_flat_sn: ∀h,g,I,G,L,V,T. G ⊢ ⋕⬊*[h, g, ⓕ{I}V.T] L → - G ⊢ ⋕⬊*[h, g, V] L. -#h #g #I #G #L #V #T #H @(lsx_ind … H) -L +lemma lsx_fwd_flat_sn: ∀h,g,I,G,L,V,T,d. G ⊢ ⋕⬊*[h, g, ⓕ{I}V.T, d] L → + G ⊢ ⋕⬊*[h, g, V, d] L. +#h #g #I #G #L #V #T #d #H @(lsx_ind … H) -L #L1 #_ #IHL1 @lsx_intro #L2 #HL12 #HV @IHL1 /3 width=3 by lleq_fwd_flat_sn/ qed-. -lemma lsx_fwd_flat_dx: ∀h,g,I,G,L,V,T. G ⊢ ⋕⬊*[h, g, ⓕ{I}V.T] L → - G ⊢ ⋕⬊*[h, g, T] L. -#h #g #I #G #L #V #T #H @(lsx_ind … H) -L +lemma lsx_fwd_flat_dx: ∀h,g,I,G,L,V,T,d. G ⊢ ⋕⬊*[h, g, ⓕ{I}V.T, d] L → + G ⊢ ⋕⬊*[h, g, T, d] L. +#h #g #I #G #L #V #T #d #H @(lsx_ind … H) -L #L1 #_ #IHL1 @lsx_intro #L2 #HL12 #HV @IHL1 /3 width=3 by lleq_fwd_flat_dx/ qed-. -lemma lsx_fwd_pair_sn: ∀h,g,I,G,L,V,T. G ⊢ ⋕⬊*[h, g, ②{I}V.T] L → - G ⊢ ⋕⬊*[h, g, V] L. +lemma lsx_fwd_pair_sn: ∀h,g,I,G,L,V,T,d. G ⊢ ⋕⬊*[h, g, ②{I}V.T, d] L → + G ⊢ ⋕⬊*[h, g, V, d] L. #h #g * /2 width=4 by lsx_fwd_bind_sn, lsx_fwd_flat_sn/ qed-. (* Basic inversion lemmas ***************************************************) -lemma lsx_inv_flat: ∀h,g,I,G,L,V,T. G ⊢ ⋕⬊*[h, g, ⓕ{I}V.T] L → - G ⊢ ⋕⬊*[h, g, V] L ∧ G ⊢ ⋕⬊*[h, g, T] L. +lemma lsx_inv_flat: ∀h,g,I,G,L,V,T,d. G ⊢ ⋕⬊*[h, g, ⓕ{I}V.T, d] L → + G ⊢ ⋕⬊*[h, g, V, d] L ∧ G ⊢ ⋕⬊*[h, g, T, d] L. /3 width=3 by lsx_fwd_flat_sn, lsx_fwd_flat_dx, conj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma index 791a0e526..edde17495 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma @@ -12,6 +12,51 @@ (* *) (**************************************************************************) +include "basic_2/reduction/cpx_cpys.ma". +include "basic_2/computation/lpxs_llneq.ma". +include "basic_2/computation/csx_alt.ma". +include "basic_2/computation/lsx_lpxs.ma". + +(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) + +(* Advanced properties ******************************************************) + +lemma lpxs_cpys_csx_lsx: ∀h,g,G,L1,U. ⦃G, L1⦄ ⊢ ⬊*[h, g] U → + ∀T. ⦃G, L1⦄ ⊢ T ▶*[0, ∞] U → + G ⊢ ⋕⬊*[h, g, T] L1. +#h #g #G #L1 #U #H @(csx_ind_alt … H) -U +#U #_ #IHU #T #HTU @lsx_intro +#L2 #HL02 #HnT elim (lpxs_nlleq_fwd_cpxs … HL02 HnT) -HnT +#U0 #U2 #H0 #H2 #HU02 #HnU02 elim (cpys_conf_eq … HTU … H0) +#X #HUX #H0X elim (eq_term_dec U X) #HnUX destruct +[ -HUX +| -HnU02 @(lsx_lpxs_trans … HL02) @(IHU … HnUX) + [ /3 width=3 by cpys_cpx, cpx_cpxs/ + | /2 width=3 by cpys_trans_eq/ + ] +] + +lemma lpxs_cpys_csx_lsx: ∀h,g,G,L1,U. ⦃G, L1⦄ ⊢ ⬊*[h, g] U → + ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ∀T. ⦃G, L2⦄ ⊢ T ▶*[0, ∞] U → + G ⊢ ⋕⬊*[h, g, T] L2. +#h #g #G #L1 #U #H @(csx_ind_alt … H) -U +#U #_ #IHU #L0 #HL10 #T #HTU @lsx_intro +#L2 #HL02 #HnT elim (lpxs_nlleq_fwd_cpxs … HL02 HnT) -HnT +#U0 #U2 #H0 #H2 #HU02 #HnU02 elim (cpys_conf_eq … HTU … H0) +#X #HUX #H0X elim (eq_term_dec U X) #HnUX destruct +[ -HUX +| -HnU02 @(IHU … HnUX) + + +-HnT /4 width=9 by lpxs_trans, lpxs_cpxs_trans, cpx_cpye_fwd_lpxs/ +] + + + + + + + include "basic_2/reduction/cpx_cpys.ma". include "basic_2/computation/lpxs_cpye.ma". include "basic_2/computation/csx_alt.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma index 1f1ebc834..2130d8b51 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma @@ -20,35 +20,89 @@ include "basic_2/computation/lsx.ma". (* Advanced properties ******************************************************) -lemma lsx_lleq_trans: ∀h,g,T,G,L1. G ⊢ ⋕⬊*[h, g, T] L1 → - ∀L2. L1 ⋕[T, 0] L2 → G ⊢ ⋕⬊*[h, g, T] L2. -#h #g #T #G #L1 #H @(lsx_ind … H) -L1 +lemma lsx_leqy_conf: ∀h,g,G,L1,T,d. G ⊢ ⋕⬊*[h, g, T, d] L1 → + ∀L2. L1 ⊑×[d, ∞] L2 → |L1| = |L2| → G ⊢ ⋕⬊*[h, g, T, d] L2. +#h #g #G #L1 #T #d #H @(lsx_ind … H) -L1 +#L1 #_ #IHL1 #L2 #H1L12 #H2L12 @lsx_intro +#L3 #H1L23 #HnL23 lapply (lpxs_fwd_length … H1L23) +#H2L23 elim (lsuby_lpxs_trans_lleq … H1L12 … H1L23) -H1L12 -H1L23 +#L0 #H1L03 #H1L10 #H lapply (lpxs_fwd_length … H1L10) +#H2L10 elim (H T) -H // +#_ #H @(IHL1 … H1L10) -IHL1 -H1L10 /3 width=1 by/ +qed-. + +lemma lsx_lleq_trans: ∀h,g,T,G,L1,d. G ⊢ ⋕⬊*[h, g, T, d] L1 → + ∀L2. L1 ⋕[T, d] L2 → G ⊢ ⋕⬊*[h, g, T, d] L2. +#h #g #T #G #L1 #d #H @(lsx_ind … H) -L1 #L1 #_ #IHL1 #L2 #HL12 @lsx_intro -#K2 #HLK2 #HnLK2 elim (lleq_lpxs_trans … HL12 … HLK2) -HLK2 +#K2 #HLK2 #HnLK2 elim (lleq_lpxs_trans … HLK2 … HL12) -HLK2 /5 width=4 by lleq_canc_sn, lleq_trans/ qed-. -lemma lsx_lpxs_trans: ∀h,g,T,G,L1. G ⊢ ⋕⬊*[h, g, T] L1 → - ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → G ⊢ ⋕⬊*[h, g, T] L2. -#h #g #T #G #L1 #H @(lsx_ind … H) -L1 #L1 #HL1 #IHL1 #L2 #HL12 -elim (lleq_dec T L1 L2 0) /3 width=4 by lsx_lleq_trans/ +lemma lsx_lpxs_trans: ∀h,g,T,G,L1,d. G ⊢ ⋕⬊*[h, g, T, d] L1 → + ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → G ⊢ ⋕⬊*[h, g, T, d] L2. +#h #g #T #G #L1 #d #H @(lsx_ind … H) -L1 #L1 #HL1 #IHL1 #L2 #HL12 +elim (lleq_dec T L1 L2 d) /3 width=4 by lsx_lleq_trans/ +qed-. + +fact lsx_bind_lpxs_aux: ∀h,g,a,I,G,L1,V,d. G ⊢ ⋕⬊*[h, g, V, d] L1 → + ∀Y,T. G ⊢ ⋕⬊*[h, g, T, ⫯d] Y → + ∀L2. Y = L2.ⓑ{I}V → ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → + G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V.T, d] L2. +#h #g #a #I #G #L1 #V #d #H @(lsx_ind … H) -L1 +#L1 #HL1 #IHL1 #Y #T #H @(lsx_ind … H) -Y +#Y #HY #IHY #L2 #H #HL12 destruct @lsx_intro +#L0 #HL20 lapply (lpxs_trans … HL12 … HL20) +#HL10 #H elim (nlleq_inv_bind … H) -H [ -HL1 -IHY | -HY -IHL1 ] +[ #HnV elim (lleq_dec V L1 L2 d) + [ #HV @(IHL1 … L0) /3 width=5 by lsx_lpxs_trans, lpxs_pair, lleq_canc_sn/ (**) (* full auto too slow *) + | -HnV -HL10 /4 width=5 by lsx_lpxs_trans, lpxs_pair/ + ] +| /3 width=4 by lpxs_pair/ +] qed-. -lemma lsx_flat_lpxs: ∀h,g,I,G,L1,V. G ⊢ ⋕⬊*[h, g, V] L1 → - ∀L2,T. G ⊢ ⋕⬊*[h, g, T] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → - G ⊢ ⋕⬊*[h, g, ⓕ{I}T.V] L2. -#h #g #I #G #L1 #V #H @(lsx_ind … H) -L1 +lemma lsx_bind: ∀h,g,a,I,G,L,V,d. G ⊢ ⋕⬊*[h, g, V, d] L → + ∀T. G ⊢ ⋕⬊*[h, g, T, ⫯d] L.ⓑ{I}V → + G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V.T, d] L. +/2 width=3 by lsx_bind_lpxs_aux/ qed. + +lemma lsx_flat_lpxs: ∀h,g,I,G,L1,V,d. G ⊢ ⋕⬊*[h, g, V, d] L1 → + ∀L2,T. G ⊢ ⋕⬊*[h, g, T, d] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → + G ⊢ ⋕⬊*[h, g, ⓕ{I}V.T, d] L2. +#h #g #I #G #L1 #V #d #H @(lsx_ind … H) -L1 #L1 #HL1 #IHL1 #L2 #T #H @(lsx_ind … H) -L2 #L2 #HL2 #IHL2 #HL12 @lsx_intro #L0 #HL20 lapply (lpxs_trans … HL12 … HL20) -#HL10 #H elim (nlleq_inv_flat … H) -H [ -HL2 -IHL1 | -HL1 -IHL2 ] -[ /3 width=1 by/ -| #HnV elim (lleq_dec V L1 L2 0) +#HL10 #H elim (nlleq_inv_flat … H) -H [ -HL1 -IHL2 | -HL2 -IHL1 ] +[ #HnV elim (lleq_dec V L1 L2 d) [ #HV @(IHL1 … L0) /3 width=3 by lsx_lpxs_trans, lleq_canc_sn/ (**) (* full auto too slow: 47s *) | -HnV -HL10 /3 width=4 by lsx_lpxs_trans/ + ] +| /3 width=1 by/ ] qed-. -lemma lsx_flat: ∀h,g,I,G,L,V. G ⊢ ⋕⬊*[h, g, V] L → - ∀T. G ⊢ ⋕⬊*[h, g, T] L → G ⊢ ⋕⬊*[h, g, ⓕ{I}T.V] L. +lemma lsx_flat: ∀h,g,I,G,L,V,d. G ⊢ ⋕⬊*[h, g, V, d] L → + ∀T. G ⊢ ⋕⬊*[h, g, T, d] L → G ⊢ ⋕⬊*[h, g, ⓕ{I}V.T, d] L. /2 width=3 by lsx_flat_lpxs/ qed. + +(* Advanced forward lemmas **************************************************) + +lemma lsx_fwd_bind_dx: ∀h,g,a,I,G,L,V,T,d. G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V.T, d] L → + G ⊢ ⋕⬊*[h, g, T, ⫯d] L.ⓑ{I}V. +#h #g #a #I #G #L #V1 #T #d #H @(lsx_ind … H) -L +#L1 #_ #IHL1 @lsx_intro +#Y #H #HT elim (lpxs_inv_pair1 … H) -H +#L2 #V2 #HL12 #_ #H destruct +@(lsx_leqy_conf … (L2.ⓑ{I}V1)) /2 width=1 by lsuby_succ/ +@IHL1 // #H @HT -IHL1 -HL12 -HT +@(lleq_lsuby_trans … (L2.ⓑ{I}V1)) +/2 width=2 by lleq_fwd_bind_dx, lsuby_succ/ +qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma lsx_inv_bind: ∀h,g,a,I,G,L,V,T,d. G ⊢ ⋕⬊*[h, g, ⓑ{a, I}V.T, d] L → + G ⊢ ⋕⬊*[h, g, V, d] L ∧ G ⊢ ⋕⬊*[h, g, T, ⫯d] L.ⓑ{I}V. +/3 width=4 by lsx_fwd_bind_sn, lsx_fwd_bind_dx, conj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cny.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cny.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/cny.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cny/cny.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cny_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cny_lift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/cny_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cny/cny_lift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpx_cpzs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpx_cpzs.etc new file mode 100644 index 000000000..6c208d51b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpx_cpzs.etc @@ -0,0 +1,73 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/delta_equivalence/cpzs.ma". +include "basic_2/reduction/cpx.ma". + +fact destruct_tsort_tsort: ∀k1,k2. ⋆k1 = ⋆k2 → k1 = k2. +#k1 #k2 #H destruct // +qed-. + +axiom cpzs_inv_subst: ∀I,G,L,K,V1,V2,W2,i. + ⇩[i] L ≡ K.ⓑ{I}V1 → ⇧[O, i+1] V2 ≡ W2 → + ⦃G, L⦄ ⊢ #i ◆*[O, ∞] W2 → ⦃G, K⦄⊢ V1 ◆*[O, ∞] V2. + +axiom cpzs_subst: ∀I,G,L,K,V1,V2,W2,i. + ⇩[i] L ≡ K.ⓑ{I}V1 → ⇧[O, i+1] V2 ≡ W2 → + ⦃G, K⦄⊢ V1 ◆*[O, ∞] V2 → ⦃G, L⦄ ⊢ #i ◆*[O, ∞] W2. + +(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************) + +(* Forward lemmas on delta-equivalence for terms ****************************) + +lemma cpx_fwd_cpys_cpzs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → + ∀d,e. ⦃G, L⦄ ⊢ T1 ◆*[d, e] T2 ↔ ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2. +#h #g #G #L #T1 #T2 #H elim H -G -L -T1 -T2 +[ /2 width=1 by conj/ +| #G #L #k #l #_ #d #e @conj #H lapply (next_lt h k) + [ <(cpzs_inv_sort … H) + | lapply (cpys_inv_sort1 … H) -H #H >(destruct_tsort_tsort … H) + ] -H #H elim (lt_refl_false … H) +| #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #d #e @conj #H +(* + [ @(cpys_subst … HLK … HVW2) // >yminus_Y_inj /3 width=7 by cpzs_inv_subst/ + | elim (cpys_inv_lref1_ldrop … H … HLK … HVW2) -H /3 width=7 by cpzs_subst/ + ] +*) +| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e + elim (IHV12 d e) -IHV12 elim (IHT12 (⫯d) e) -IHT12 + #IHTdx #IHTsn #IHVdx #IHVsn @conj #H + [ elim (cpzs_inv_bind … H) -H /3 width=1 by cpys_bind/ + | elim (cpys_inv_bind1 … H) -H #X1 #X2 #H1 #H2 #H destruct /3 width=1 by cpzs_bind/ + ] +| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e + elim (IHV12 d e) -IHV12 elim (IHT12 (d) e) -IHT12 + #IHTdx #IHTsn #IHVdx #IHVsn @conj #H + [ elim (cpzs_inv_flat … H) -H /3 width=1 by cpys_flat/ + | elim (cpys_inv_flat1 … H) -H #X1 #X2 #H1 #H2 #H destruct /3 width=1 by cpzs_flat/ + ] +| #G #L #V #U1 #U2 #T2 #_ #HTU2 #_ #d #e @conj #H +| #G #L #V1 #T1 #T2 #_ #_ #d #e @conj #H +| #G #L #V1 #V2 #T1 #HV12 #_ #d #e @conj #H +| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #d #e @conj #H + [ elim (cpzs_inv_flat_bind … H) + | elim (cpys_inv_flat1 … H) -H #X1 #X2 #H1 #H2 #H destruct + ] +| #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #d #e @conj #H + [ elim (cpzs_inv_flat_bind … H) + | elim (cpys_inv_flat1 … H) -H #X1 #X2 #H1 #H2 #H destruct + ] +] + + \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpye.etc similarity index 92% rename from matita/matita/contribs/lambdadelta/basic_2/substitution/cpye.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpye.etc index 82a1e3b46..71e06ea72 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpye.etc @@ -26,6 +26,13 @@ interpretation "evaluation for context-sensitive extended substitution (term)" (* Basic_properties *********************************************************) +(* Note: this should go in subconversion *) +lemma leqy_cpye_trans: ∀G,L2,T1,T2,d,e. ⦃G, L2⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄ → + ∀L1. L1 ⊑×[d, e] L2 → L2 ⊑×[d, e] L1 → ⦃G, L1⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄. +#G #L2 #T1 #T2 #d #e * +/4 width=8 by lsuby_cpys_trans, lsuby_cny_conf, conj/ +qed-. + lemma cpye_sort: ∀G,L,d,e,k. ⦃G, L⦄ ⊢ ⋆k ▶*[d, e] 𝐍⦃⋆k⦄. /3 width=5 by cny_sort, conj/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpye_alt.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/substitution/cpye_alt.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpye_alt.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye_cpye.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpye_cpye.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/substitution/cpye_cpye.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpye_cpye.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpye_lift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/substitution/cpye_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpye_lift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cny.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpys_cny.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cny.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpys_cny.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpzs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpzs.etc new file mode 100644 index 000000000..0fada97a0 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/cpzs.etc @@ -0,0 +1,83 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/pdeltaconvstar_6.ma". +include "basic_2/substitution/cpye_lift.ma". + +(* CONTEXT-SENSITIVE EXTENDED DELTA-EQUIVALENCE FOR TERMS *******************) + +definition cpzs: ynat → ynat → relation4 genv lenv term term ≝ + λd,e,G,L,T1,T2. + ∃∃T. ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T⦄ & ⦃G, L⦄ ⊢ T2 ▶*[d, e] 𝐍⦃T⦄. + +interpretation "context-sensitive extended delta-equivalence (term)" + 'PDeltaConvStar G L T1 d e T2 = (cpzs d e G L T1 T2). + +(* Basic properties **********************************************************) + +lemma cpye_div: ∀G,L,T1,T,d,e. ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T⦄ → + ∀T2. ⦃G, L⦄ ⊢ T2 ▶*[d, e] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ T1 ◆*[d, e] T2. +/2 width=3 by ex2_intro/ qed. + +lemma cpzs_refl: ∀G,L,d,e. reflexive … (cpzs d e G L). +#G #L #d #e #T elim (cpye_total G L T d e) /2 width=3 by cpye_div/ +qed. + +lemma cpzs_bind: ∀G,L,V1,V2,d,e. ⦃G, L⦄ ⊢ V1 ◆*[d, e] V2 → + ∀I,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ◆*[⫯d, e] T2 → + ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ◆*[d, e] ⓑ{a,I}V2.T2. +#G #L #V1 #V2 #d #e * #V #HV1 #HV2 #I #T1 #T2 * +/5 width=10 by cpye_div, cpye_bind, leqy_cpye_trans, cny_bind, lsuby_succ/ +qed. + +lemma cpzs_flat: ∀G,L,V1,V2,d,e. ⦃G, L⦄ ⊢ V1 ◆*[d, e] V2 → + ∀T1,T2. ⦃G, L⦄ ⊢ T1 ◆*[d, e] T2 → + ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ◆*[d, e] ⓕ{I}V2.T2. +#G #L #V1 #V2 #d #e * #V #HV1 #HV2 #T1 #T2 * +/3 width=5 by cpye_div, cpye_flat, cny_flat/ +qed. + +(* Basic inversion lemmas ***************************************************) + +lemma cpzs_inv_sort: ∀G,L,d,e,k1,k2. ⦃G, L⦄ ⊢ ⋆k1 ◆*[d, e] ⋆k2 → k1 = k2. +#G #L #d #e #k1 #k2 * #X #H1 #H2 +lapply (cpye_inv_sort1 … H1) -H1 #H1 +lapply (cpye_inv_sort1 … H2) -H2 #H2 +destruct // +qed-. + +lemma cpzs_inv_bind: ∀a1,a2,I1,I2,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ ⓑ{a1,I1}V1.T1 ◆*[d, e] ⓑ{a2,I2}V2.T2 → + ∧∧ a1 = a2 & I1 = I2 + & ⦃G, L⦄ ⊢ V1 ◆*[d, e] V2 & ⦃G, L.ⓑ{I1}V1⦄ ⊢ T1 ◆*[⫯d, e] T2. +#a1 #a2 #I1 #I2 #G #L #V1 #V2 #T1 #T2 #d #e * #X #H1 #H2 +elim (cpye_inv_bind1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H1 +elim (cpye_inv_bind1 … H2) -H2 #W2 #U2 #HW12 #HU12 #H2 +destruct /5 width=8 by cpye_div, leqy_cpye_trans, lsuby_succ, and4_intro/ +qed-. + +lemma cpzs_inv_flat: ∀I1,I2,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ ⓕ{I1}V1.T1 ◆*[d, e] ⓕ{I2}V2.T2 → + ∧∧ I1 = I2 + & ⦃G, L⦄ ⊢ V1 ◆*[d, e] V2 & ⦃G, L⦄ ⊢ T1 ◆*[d, e] T2. +#I1 #I2 #G #L #V1 #V2 #T1 #T2 #d #e * #X #H1 #H2 +elim (cpye_inv_flat1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H1 +elim (cpye_inv_flat1 … H2) -H2 #W2 #U2 #HW12 #HU12 #H2 +destruct /3 width=3 by cpye_div, and3_intro/ +qed-. + +lemma cpzs_inv_flat_bind: ∀a2,I1,I2,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ ⓕ{I1}V1.T1 ◆*[d, e] ⓑ{a2,I2}V2.T2 → ⊥. +#a2 #I1 #I2 #G #L #V1 #V2 #T1 #T2 #d #e * #X #H1 #H2 +elim (cpye_inv_flat1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H1 +elim (cpye_inv_bind1 … H2) -H2 #W2 #U2 #HW12 #HU12 #H2 +destruct +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_cpye.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/lleq_cpye.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_cpye.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cny/lleq_cpye.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_cpye.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/lpx_cpye.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_cpye.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cny/lpx_cpye.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpye.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/lpxs_cpye.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpye.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cny/lpxs_cpye.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cny/pdeltaconvstar_6.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/pdeltaconvstar_6.etc new file mode 100644 index 000000000..b7de5f543 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/pdeltaconvstar_6.etc @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 break ◆ * [ term 46 d , break term 46 e ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'PDeltaConvStar $G $L $T1 $d $e $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubsteval_6.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/psubsteval_6.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubsteval_6.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cny/psubsteval_6.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubstevalalt_6.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/psubstevalalt_6.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubstevalalt_6.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cny/psubstevalalt_6.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubstnormal_5.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cny/psubstnormal_5.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubstnormal_5.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cny/psubstnormal_5.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/lazynegatedeq_4.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/lazynegatedeq_4.etc new file mode 100644 index 000000000..6b0cb85e5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/lazynegatedeq_4.etc @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( L1 ⧣ break [ term 46 T , break term 46 d ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'LazyNegatedEq $T $d $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/lazynegatedeqalt_4.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/lazynegatedeqalt_4.etc new file mode 100644 index 000000000..b150f63ff --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/lazynegatedeqalt_4.etc @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( L1 ⧣ ⧣ break [ term 46 T , break term 46 d ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'LazyNegatedEqAlt $T $d $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/llneq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/llneq.etc new file mode 100644 index 000000000..d41a4e83c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/llneq.etc @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/lazynegatedeq_4.ma". +include "basic_2/substitution/lleq.ma". + +(* NEGATED LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **************************) + +definition llneq: relation4 ynat term lenv lenv ≝ + λd,T,L1,L2. |L1| = |L2| ∧ (L1 ⋕[T, d] L2 → ⊥). + +interpretation + "negated lazy equivalence (local environment)" + 'LazyNegatedEq T d L1 L2 = (llneq d T L1 L2). diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/llneq_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/llneq_alt.etc new file mode 100644 index 000000000..00eb2c34e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/llneq_alt.etc @@ -0,0 +1,68 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/lazynegatedeqalt_4.ma". +include "basic_2/substitution/lleq_lleq.ma". +include "basic_2/substitution/llneq.ma". + +(* NEGATED LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **************************) + +(* alternative definition of llneq *) +inductive llneqa: relation4 ynat term lenv lenv ≝ +| llneqa_neq: ∀I1,I2,L1,L2,K1,K2,V1,V2,d,i. d ≤ yinj i → + ⇩[i]L1 ≡ K1.ⓑ{I1}V1 → ⇩[i]L2 ≡ K2.ⓑ{I2}V2 → + |K1| = |K2| → (V1 = V2 → ⊥) → llneqa d (#i) L1 L2 +| llneqa_eq : ∀I1,I2,L1,L2,K1,K2,V,d,i. d ≤ yinj i → + ⇩[i]L1 ≡ K1.ⓑ{I1}V → ⇩[i]L2 ≡ K2.ⓑ{I2}V → + llneqa 0 (V) K1 K2 → llneqa d (#i) L1 L2 +| llneqa_bind_sn: ∀a,I,L1,L2,V,T,d. + llneqa d V L1 L2 → llneqa d (ⓑ{a,I}V.T) L1 L2 +| llneqa_bind_dx: ∀a,I,L1,L2,V,T,d. + llneqa (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → llneqa d (ⓑ{a,I}V.T) L1 L2 +| llneqa_flat_sn: ∀I,L1,L2,V,T,d. + llneqa d V L1 L2 → llneqa d (ⓕ{I}V.T) L1 L2 +| llneqa_flat_dx: ∀I,L1,L2,V,T,d. + llneqa d T L1 L2 → llneqa d (ⓕ{I}V.T) L1 L2 +. + +interpretation + "negated lazy equivalence (local environment) alternative" + 'LazyNegatedEqAlt T d L1 L2 = (llneqa d T L1 L2). + +(* Main properties **********************************************************) + +theorem llneq_llneqa: ∀T,L1,L2,d. L1 ⧣[T, d] L2 → L1 ⧣⧣[T, d] L2. +#T #L1 @(f2_ind … rfw … L1 T) -L1 -T +#n #IH #L1 * * +[ #k #Hn #L2 #d * #HL12 #H elim H /2 width=1 by lleq_sort/ +| #i #Hn #L2 #d * #HL12 #H elim (ylt_split i d) #Hdi + [ elim H /2 width=1 by lleq_skip/ ] + elim (lt_or_ge i (|L1|)) #HiL1 + [2: elim H /3 width=3 by lleq_free, le_repl_sn_aux/ ] + elim (ldrop_O1_lt … HiL1) #I1 #K1 #V1 #HLK1 + elim (ldrop_O1_lt L2 i) /2 width=1 by/ #I2 #K2 #V2 #HLK2 + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) normalize + elim (eq_term_dec V1 V2) #HnV12 destruct + [2: #H @(llneqa_neq … HLK1 … HLK2) /2 width=1 by/ ] (**) (* explicit constructor *) + elim (lleq_dec V2 K1 K2 0) #HnV2 [ elim H /2 width=8 by lleq_lref/ ] + #H @(llneqa_eq … HLK1 … HLK2) /4 width=2 by ldrop_fwd_rfw, conj/ (**) (* explicit constructor *) +| #p #Hn #L2 #d * #HL12 #H elim H /2 width=1 by lleq_gref/ +| #a #I #V #T #Hn #L2 #d * #HL12 #H destruct elim (nlleq_inv_bind … H) -H + [ /5 width=1 by llneqa_bind_sn, conj/ + | #H @llneqa_bind_dx @IH // @conj normalize /2 width=1 by/ + ] +| #I #V #T #Hn #L2 #d * #HL12 #H destruct elim (nlleq_inv_flat … H) -H + /5 width=1 by llneqa_flat_dx, llneqa_flat_sn, conj/ +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/llneq_ext.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/llneq_ext.etc new file mode 100644 index 000000000..235d869c2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/llneq/llneq_ext.etc @@ -0,0 +1,33 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/substitution/llneq_alt.ma". + +(* NEGATED LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **************************) + +(* Advanced inversion lemmas ************************************************) + +lemma llneq_inv_atom1: ∀L1,L2,T,d. L1 ⧣⧣[T, d] L2 → |L1| ≤ d → ⊥. +#L1 #L2 #T #d #H elim H -L1 -L2 -T -d /2 width=1 by/ +[ #I1 #I2 #L1 #L2 #K1 #K2 #V1 #V2 #d #i #Hdi #HLK1 #_ #_ #_ + >(ldrop_fwd_length … HLK1) -HLK1 normalize + #H lapply (yle_trans … H … Hdi) -d + /3 width=4 by yle_inv_inj, le_plus_xySz_x_false/ +| #I1 #I2 #L1 #L2 #K1 #K2 #V #d #i #Hdi #HLK1 #_ #_ #_ + >(ldrop_fwd_length … HLK1) -HLK1 normalize + #H lapply (yle_trans … H … Hdi) -d + /3 width=4 by yle_inv_inj, le_plus_xySz_x_false/ +| #a #I #L1 (length_inv_zero_dx … H) -L1 /3 width=5 by ex3_intro, conj/ +| #I2 #L2 #K2 #V2 #W2 #_ #HVW2 #IHLK2 #Y #H + elim (length_inv_pos_dx … H) -H #I #L1 #V1 #HL12 #H destruct + elim (IHLK2 … HL12) -IHLK2 #K1 #HLK1 #HK12 #IH + elim (eq_term_dec V1 V2) #H destruct + [ @(ex3_intro … (K1.ⓑ{I}W2)) normalize /2 width=1 by / +*) +axiom lleq_lpx_trans: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡[h, g] K2 → + ∀L1,T,d. L1 ⋕[T, d] L2 → + ∃∃K1. ⦃G, L1⦄ ⊢ ➡[h, g] K1 & K1 ⋕[T, d] K2. +(* +#h #g #G #L2 #K2 #H elim H -L2 -K2 +[ #L1 #T #d #H lapply (lleq_fwd_length … H) -H + #H >(length_inv_zero_dx … H) -L1 /2 width=3 by ex2_intro/ +| #I2 #L2 #K2 #V2 #W2 #HLK2 #HVW2 #IHLK2 #Y #T #d #HT + lapply (lleq_fwd_length … HT) #H + elim (length_inv_pos_dx … H) -H #I1 #L1 #V1 #HL12 #H destruct + elim (eq_term_dec V1 V2) #H destruct + [ @ex2_intro … +*) lemma lpx_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma index 123529e05..f6bab12f8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma @@ -44,6 +44,11 @@ lemma lsuby_succ_lt: ∀I1,I2,L1,L2,V1,V2,d,e. L1 ⊑×[⫰d, e] L2 → 0 < d #I1 #I2 #L1 #L2 #V1 #V2 #d #e #HL12 #Hd <(ylt_inv_O1 … Hd) /2 width=1 by lsuby_succ/ qed. +lemma lsuby_pair_O_Y: ∀L1,L2. L1 ⊑×[0, ∞] L2 → + ∀I1,I2,V. L1.ⓑ{I1}V ⊑×[0,∞] L2.ⓑ{I2}V. +#L1 #L2 #HL12 #I1 #I2 #V lapply (lsuby_pair I1 I2 … V … HL12) -HL12 // +qed. + lemma lsuby_refl: ∀L,d,e. L ⊑×[d, e] L. #L elim L -L // #L #I #V #IHL #d elim (ynat_cases … d) [| * #x ] @@ -52,19 +57,19 @@ lemma lsuby_refl: ∀L,d,e. L ⊑×[d, e] L. #He destruct /2 width=1 by lsuby_zero, lsuby_pair/ qed. -lemma lsuby_length: ∀L1,L2. |L2| ≤ |L1| → L1 ⊑×[yinj 0, yinj 0] L2. -#L1 elim L1 -L1 -[ #X #H lapply (le_n_O_to_eq … H) -H - #H lapply (length_inv_zero_sn … H) #H destruct /2 width=1 by lsuby_atom/ -| #L1 #I1 #V1 #IHL1 * normalize - /4 width=2 by lsuby_zero, le_S_S_to_le/ +lemma lsuby_O1: ∀L2,L1,d. |L2| ≤ |L1| → L1 ⊑×[d, yinj 0] L2. +#L2 elim L2 -L2 // #L2 #I2 #V2 #IHL2 * normalize +[ #d #H lapply (le_n_O_to_eq … H) -H (length_inv_zero_dx … H) -L1 // -| /2 width=1 by lsuby_length/ +| /2 width=1 by lsuby_O1/ | #I1 #I2 #L1 #L2 #V #e #_ #IHL12 #H lapply (injective_plus_l … H) /3 width=1 by lsuby_pair/ | #I1 #I2 #L1 #L2 #V1 #V2 #d #e #_ #IHL12 #H lapply (injective_plus_l … H) diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 6d4072800..de9939c00 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -84,7 +84,7 @@ table { } ] [ { "strongly normalizing extended computation" * } { - [ "lsx ( ? ⊢ ⬊*[?,?,?] ? )" "lsx_cpxs" + "lsx_csx" * ] + [ "lsx ( ? ⊢ ⬊*[?,?,?,?] ? )" "lsx_cpxs" + "lsx_csx" * ] [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tstc_vector" + "csx_aaa" * ] [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lpx" + "csx_fpbs" * ] } @@ -105,8 +105,8 @@ table { } ] [ { "context-sensitive extended computation" * } { - [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? )" "lpxs_ldrop" + "lpxs_cpye" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] - [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ] + [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? )" "lpxs_ldrop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] + [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_lift" + "cpxs_cpys" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ] } ] [ { "context-sensitive computation" * } { @@ -135,7 +135,7 @@ table { } ] [ { "context-sensitive extended reduction" * } { - [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_cpys" + "lpx_cpye" + "lpx_lleq" + "lpx_aaa" * ] + [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_cpys" + "lpx_lleq" + "lpx_aaa" * ] [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_lift" + "cpx_cpys" + "cpx_lleq" + "cpx_cix" * ] } ] @@ -209,15 +209,11 @@ table { class "yellow" [ { "substitution" * } { [ { "lazy equivalence for local environments" * } { - [ "lleq ( ? ⋕[?,?] ? )" "lleq_alt ( ? ⋕⋕[?,?] ? )" "lleq_ldrop" + "lleq_fqus" + "lleq_cpye" + "lleq_lleq" + "lleq_ext" * ] + [ "lleq ( ? ⋕[?,?] ? )" "lleq_alt ( ? ⋕⋕[?,?] ? )" "lleq_ldrop" + "lleq_fqus" + "lleq_lleq" + "lleq_ext" * ] } ] - [ { "evaluation for contxt-sensitive extended substitution" * } { - [ "cpye ( ⦃?,?⦄ ⊢ ? ▶*[?,?] 𝐍⦃?⦄ )" "cpye_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] 𝐍⦃?⦄ )" "cpye_lift" + "cpye_cpye" * ] - } - ] [ { "contxt-sensitive extended multiple substitution" * } { - [ "cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )" "cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )" "cpys_lift" + "cpys_cny" + "cpys_cpys" * ] + [ "cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )" "cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )" "cpys_lift" + "cpys_cpys" * ] } ] [ { "iterated structural successor for closures" * } { @@ -242,10 +238,6 @@ table { ] class "orange" [ { "relocation" * } { - [ { "normal forms for context-sensitive extended substitution" * } { - [ "cny ( ⦃?,?⦄ ⊢ ▶[?,?] 𝐍⦃?⦄ )" "cny_lift" * ] - } - ] [ { "contxt-sensitive extended ordinary substitution" * } { [ "cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )" "cpy_lift" + "cpy_cpy" * ] } -- 2.39.2