From d1b944b638846d98dfeb21fa6757e89c609be82a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 9 Dec 2013 21:53:19 +0000 Subject: [PATCH] - first results on strongly normalizing local environments - some updates --- .../lambdadelta/basic_2/computation/csx.ma | 32 ++--- .../basic_2/computation/csx_fpbc.ma | 30 ----- .../basic_2/computation/csx_fpbs.ma | 25 ++++ .../basic_2/computation/fpbc_fpns.ma | 10 +- .../basic_2/computation/lpxs_lleq.ma | 21 ++-- .../lambdadelta/basic_2/computation/lsx.ma | 63 ++++++++++ .../basic_2/computation/lsx_cpxs.ma | 32 +++++ .../basic_2/computation/lsx_csx.ma | 33 ++++++ .../basic_2/computation/lsx_fpbc.ma | 111 ++++++++++++++++++ .../basic_2/notation/relations/lazysn_5.ma | 19 +++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 5 +- 11 files changed, 315 insertions(+), 66 deletions(-) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbc.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbs.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/lsx_cpxs.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/lsx_fpbc.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazysn_5.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma index 3ba52668c..c57b04713 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma @@ -32,8 +32,8 @@ lemma csx_ind: ∀h,g,G,L. ∀R:predicate term. R T1 ) → ∀T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → R T. -#h #g #G #L #R #H0 #T1 #H elim H -T1 #T1 #HT1 #IHT1 -@H0 -H0 /3 width=1/ -IHT1 /4 width=1/ +#h #g #G #L #R #H0 #T1 #H elim H -T1 +/5 width=1 by SN_intro/ qed-. (* Basic properties *********************************************************) @@ -42,28 +42,25 @@ qed-. lemma csx_intro: ∀h,g,G,L,T1. (∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → (T1 = T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊*[h, g] T2) → ⦃G, L⦄ ⊢ ⬊*[h, g] T1. -/4 width=1/ qed. +/4 width=1 by SN_intro/ qed. lemma csx_cpx_trans: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → ∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ⦃G, L⦄ ⊢ ⬊*[h, g] T2. -#h #g #G #L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12 -@csx_intro #T #HLT2 #HT2 -elim (eq_term_dec T1 T2) #HT12 -[ -IHT1 -HLT12 destruct /3 width=1/ -| -HT1 -HT2 /3 width=4/ +#h #g #G #L #T1 #H @(csx_ind … H) -T1 #T1 #HT1 #IHT1 #T2 #HLT12 +elim (eq_term_dec T1 T2) #HT12 destruct /3 width=4 by/ qed-. (* Basic_1: was just: sn3_nf2 *) lemma cnx_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ ⬊*[h, g] T. -/2 width=1/ qed. +/2 width=1 by NF_to_SN/ qed. -lemma cnx_sort: ∀h,g,G,L,k. ⦃G, L⦄ ⊢ ⬊*[h, g] ⋆k. +lemma csx_sort: ∀h,g,G,L,k. ⦃G, L⦄ ⊢ ⬊*[h, g] ⋆k. #h #g #G #L #k elim (deg_total h g k) -#l generalize in match k; -k @(nat_ind_plus … l) -l /3 width=1/ +#l generalize in match k; -k @(nat_ind_plus … l) -l /3 width=6 by cnx_csx, cnx_sort/ #l #IHl #k #Hkl lapply (deg_next_SO … Hkl) -Hkl #Hkl @csx_intro #X #H #HX elim (cpx_inv_sort1 … H) -H [ #H destruct elim HX // -| -HX * #l0 #_ #H destruct -l0 /2 width=1/ +| -HX * #l0 #_ #H destruct -l0 /2 width=1 by/ ] qed. @@ -76,7 +73,7 @@ elim (cpx_inv_cast1 … H1) -H1 [ * #W0 #T0 #HLW0 #HLT0 #H destruct elim (eq_false_inv_tpair_sn … H2) -H2 [ /3 width=3 by csx_cpx_trans/ - | -HLW0 * #H destruct /3 width=1/ + | -HLW0 * #H destruct /3 width=1 by/ ] |2,3: /3 width=3 by csx_cpx_trans/ ] @@ -88,7 +85,8 @@ fact csx_fwd_pair_sn_aux: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ ⬊*[h, g] U → ∀I,V,T. U = ②{I}V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] V. #h #g #G #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct @csx_intro #V2 #HLV2 #HV2 -@(IH (②{I}V2.T)) -IH // /2 width=1/ -HLV2 #H destruct /2 width=1/ +@(IH (②{I}V2.T)) -IH /2 width=3 by cpx_pair_sn/ -HLV2 +#H destruct /2 width=1 by/ qed-. (* Basic_1: was just: sn3_gen_head *) @@ -99,7 +97,8 @@ fact csx_fwd_bind_dx_aux: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ ⬊*[h, g] U → ∀a,I,V,T. U = ⓑ{a,I}V.T → ⦃G, L.ⓑ{I}V⦄ ⊢ ⬊*[h, g] T. #h #g #G #L #U #H elim H -H #U0 #_ #IH #a #I #V #T #H destruct @csx_intro #T2 #HLT2 #HT2 -@(IH (ⓑ{a,I}V.T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/ +@(IH (ⓑ{a,I}V.T2)) -IH /2 width=3 by cpx_bind/ -HLT2 +#H destruct /2 width=1 by/ qed-. (* Basic_1: was just: sn3_gen_bind *) @@ -110,7 +109,8 @@ fact csx_fwd_flat_dx_aux: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ ⬊*[h, g] U → ∀I,V,T. U = ⓕ{I}V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] T. #h #g #G #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct @csx_intro #T2 #HLT2 #HT2 -@(IH (ⓕ{I}V.T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/ +@(IH (ⓕ{I}V.T2)) -IH /2 width=3 by cpx_flat/ -HLT2 +#H destruct /2 width=1 by/ qed-. (* Basic_1: was just: sn3_gen_flat *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbc.ma deleted file mode 100644 index b97478371..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbc.ma +++ /dev/null @@ -1,30 +0,0 @@ -include "basic_2/computation/fpbc.ma". - -(* Advanced eliminators *****************************************************) - -fact csx_ind_fpbc_aux: ∀h,g. ∀R:relation3 genv lenv term. - (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → - (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → - R G1 L1 T1 - ) → - ∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → - ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → R G2 L2 T2. -#h #g #R #IH1 #G1 #L1 #T1 #H @(csx_ind … H) -T1 -#T1 @(fqup_wf_ind … G1 L1 T1) -G1 -L1 -T1 -#G1 #L1 #T1 #IH2 #H1 #IH3 #G2 #L2 #T2 #H12 @IH1 -IH1 /2 width=5 by csx_fqus_conf/ -#G #L #T * -[ #G0 #L0 #T0 #H20 lapply (fqus_fqup_trans … H12 H20) -G2 -L2 -T2 - #H10 @(IH2 … H10) -IH2 /2 width=5 by csx_fqup_conf/ - #T2 #HT02 #H #G3 #L3 #T3 #HT23 elim (fqup_cpx_trans_neq … H10 … HT02 H) -T0 - /4 width=8 by fqup_fqus_trans, fqup_fqus/ -| #T0 #HT20 #H elim (fqus_cpxs_trans_neq … H12 … HT20 H) -T2 /3 width=4 by/ -] -qed-. - -lemma csx_ind_fpbc: ∀h,g. ∀R:relation3 genv lenv term. - (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → - (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → - R G1 L1 T1 - ) → - ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → R G L T. -/4 width=8 by csx_ind_fpbc_fqus/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbs.ma new file mode 100644 index 000000000..99f39de1d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbs.ma @@ -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/computation/lpxs.ma". +include "basic_2/computation/csx_lpx.ma". + +(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) + +(* Advanced properties ******************************************************) + +lemma csx_lpxs_conf: ∀h,g,G,L1. ∀T:term. ⦃G, L1⦄ ⊢ ⬊*[h, g] T → + ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L2⦄ ⊢ ⬊*[h, g] T. +#h #g #G #L1 #T #HT #L2 #H @(lpxs_ind … H) -L2 /2 width=3 by csx_lpx_conf/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpns.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpns.ma index fc1a71f5b..672d2d6e4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpns.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpns.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/computation/lpxs_lleq.ma". +include "basic_2/relocation/lleq_lleq.ma". include "basic_2/computation/fpns.ma". include "basic_2/computation/fpbs_alt.ma". include "basic_2/computation/fpbc.ma". @@ -27,13 +27,11 @@ lemma fpbs_fwd_fpbc_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃ #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim(fpbs_fpbsa … H) -H #L #T #HT1 #HT2 #HL2 elim (eq_term_dec T1 T) #H destruct [ -HT1 elim (fqus_inv_gen … HT2) -HT2 - [ #HT2 elim (fqup_inv_step_sn … HT2) -HT2 - #H6 #H7 #H8 #H9 #H10 @or_intror @(ex2_3_intro … H6 H7 H8) - /5 width=9 by fpbsa_inv_fpbs, fpbc_fqup, fqu_fqup, ex3_2_intro, ex2_3_intro, or_intror/ + [ #HT2 @or_intror + /5 width=9 by fpbsa_inv_fpbs, fpbc_fqup, ex3_2_intro, ex2_3_intro, or_intror/ | * #HG #HL #HT destruct elim (lleq_dec T2 L L2 0) #H [ /3 width=1 by fpns_intro, or_introl/ - | elim (lpxs_nlleq_inv_step_sn … HL2 H) -HL2 -H - /5 width=5 by fpbc_lpxs, lpxs_fpbs, ex2_3_intro, or_intror/ + | /5 width=5 by fpbc_lpxs, ex2_3_intro, or_intror/ ] ] | elim (cpxs_neq_inv_step_sn … HT1 H) -HT1 -H 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 a36a267a5..792b639dc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma @@ -18,19 +18,16 @@ include "basic_2/computation/lpxs_cpxs.ma". (* SN EXTENDED PARALLEL COMPUTATION FOR LOCAL ENVIRONMENTS ******************) -(* Inversion lemmas on lazy equivalence for local environments **************) +(* Advanced properties ******************************************************) -lemma lpxs_nlleq_inv_step_sn: ∀h,g,G,L1,L2,T,d. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[d, T] L2 → ⊥) → - ∃∃L. ⦃G, L1⦄ ⊢ ➡*[h, g] L & L1 ⋕[d, T] L → ⊥ & ⦃G, L⦄ ⊢ ➡*[h, g] L2. -#h #g #G #L1 #L2 #T #d #H @(lpxs_ind_dx … H) -L1 -[ #H elim H -H // -| #L1 #L #H1 #H2 #IH2 #H12 elim (lleq_dec T L1 L d) #H - [ -H2 elim IH2 -IH2 - /4 width=4 by lpxs_strap2, lleq_canc_sn, lleq_trans, ex3_intro/ - | -IH2 -H12 /3 width=4 by lpx_lpxs, ex3_intro/ (**) (* auto fails without clear *) - ] -] -qed-. +axiom lleq_lpxs_trans_nlleq: ∀h,g,G,L1s,L1d,T,d. L1s ⋕[d, T] L1d → + ∀L2d. ⦃G, L1d⦄ ⊢ ➡*[h, g] L2d → (L1d ⋕[d, T] L2d → ⊥) → + ∃∃L2s. ⦃G, L1s⦄ ⊢ ➡*[h, g] L2s & L2s ⋕[d, T] L2d & L1s ⋕[d, T] L2s → ⊥. + +(* Advanced inversion lemmas ************************************************) + +axiom lpxs_inv_cpxs_nlleq: ∀h,g,G,L1,L2,T1. ⦃G, L1⦄ ⊢ ➡*[h,g] L2 → (L1 ⋕[O, T1] L2 → ⊥) → + ∃∃T2. ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2 & T1 = T2 → ⊥ & ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2. (* Properties on lazy equivalence for local environments ********************) 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..61363bf9f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.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/notation/relations/lazysn_5.ma". +include "basic_2/relocation/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). + +interpretation + "extended strong normalization (local environment)" + 'LazySN h g T G L = (lsx h g T 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 ⋕[0, T] L2 → ⊥) → R L2) → + R L1 + ) → + ∀L. G ⊢ ⋕⬊*[h, g, T] L → R L. +#h #g #T #G #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 ⋕[0, T] L2 → ⊥) → G ⊢ ⋕⬊*[h, g, T] L2) → + G ⊢ ⋕⬊*[h, g, T] 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 +#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 +#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 +#L2 #HL12 #H elim H -H +/3 width=4 by lpxs_fwd_length, lleq_gref/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_cpxs.ma new file mode 100644 index 000000000..e6bf5d3e4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_cpxs.ma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||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_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. G ⊢ ⋕⬊*[h, g, T] L1 → + ∀L2. L1 ⋕[0, T] L2 → G ⊢ ⋕⬊*[h, g, T] L2. +#h #g #T #G #L1 #H @(lsx_ind … H) -L1 #L1 #HL1 #IHL1 #L2 #HL12 +@lsx_intro #L #HL2 #HnT elim (lleq_lpxs_trans_nlleq … HL12 … HL2 HnT) -L2 /3 width=4 by/ +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/ +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..48786e5e2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma @@ -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/computation/lpxs_lleq.ma". +include "basic_2/computation/csx_alt.ma". +include "basic_2/computation/lsx.ma". + +(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) + +(* Main properties **********************************************************) + +axiom csx_lsx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → G ⊢ ⋕⬊*[h, g, T] L. + +axiom lsx_inv_csx: ∀h,g,G,L,T. G ⊢ ⋕⬊*[h, g, T] L → ⦃G, L⦄ ⊢ ⬊*[h, g] T. + +(* +#h #g #G #L1 #T1 #H @(csx_ind_alt … H) -T1 +#T1 #_ #IHT1 @lsx_intro +#L2 #HL12 #HnT1 elim (lpxs_inv_cpxs_nlleq … HL12 HnT1) -HL12 -HnT1 +#T2 #H1T12 #HnT12 #H2T12 lapply (IHT1 … H1T12 HnT12) -IHT1 -H1T12 -HnT12 +#HT2 +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_fpbc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_fpbc.ma new file mode 100644 index 000000000..2c6418f2a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_fpbc.ma @@ -0,0 +1,111 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fpbs.ma". +include "basic_2/computation/fpbc.ma". +include "basic_2/computation/csx_lift.ma". +include "basic_2/computation/csx_lpxs.ma". +include "basic_2/computation/lsx_csx.ma". + +(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) + +(* Advanced eliminators for context-sensitive ext. strongly norm. terms *****) + +lemma tollens: ∀R1,R2,R3:Prop. (R1 → R2) → (R2 → R3) → R1 → R3. +/3 width=1/ qed-. + +axiom fqus_lpxs_trans_nlleq: ∀h,g,G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ → + ∀L2. ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 → (K2 ⋕[O, T2] L2 →⊥) → + ∃∃L1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 & + K1 ⋕[O, T1] L1 → ⊥ & ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄. + +axiom fpbs_lpxs_trans_nlleq: ∀h,g,G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ≥[h, g] ⦃G2, K2, T2⦄ → + ∀L2. ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 → (K2 ⋕[O, T2] L2 →⊥) → + ∃∃L1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 & + K1 ⋕[O, T1] L1 → ⊥ & ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. + + +lemma csx_ind_fpbc_fpbs: ∀h,g. ∀R:relation3 genv lenv term. + (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → + (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → + R G1 L1 T1 + ) → + ∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → + R G2 L2 T2. +#h #g #R #IH1 #G1 #L1 #T1 #H @(csx_ind_alt … H) -T1 +#T1 #HT1 @(lsx_ind h g T1 G1 … L1) /2 width=1 by csx_lsx/ -L1 +#L1 @(fqup_wf_ind … G1 L1 T1) -G1 -L1 -T1 +#G1 #L1 #T1 #IH2 #H1 #IH3 #IH4 #G2 #L2 #T2 #H12 +@IH1 -IH1 (* /4 width=5 by lsx_inv_csx, csx_lpxs_conf, csx_fqus_conf/ *) +[2: #G #L #T * + [ + | + | #L0 #HL20 #HnT2 elim (fpbs_lpxs_trans_nlleq … H12 … HL20 HnT2) -L2 + #L2 #HL12 #HnT1 #H12 @(IH3 … HL12 HnT1 … H12) -IH3 + #H26 #H27 #H28 #H29 #H30 #H31 #H32 + @(IH4) … H27 H28) + + [ #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 + lapply (fqup_fqus_trans … H15 … H21) -H15 -H21 #H + @(IH3 … H23 H24) + + #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 + @(IH4 … H3 … H10) -IH4 -H10 -H3 // + + + + [ -IH4 | -H1 -IH2 -IH4 | -H1 -H2 -IH2 -IH3 ] +[ #G0 #L0 #T0 #H20 elim (lpxs_lleq_fqup_trans … H20 … HYL2 HT2) -L2 + #L2 #H20 #HL20 lapply (fqus_fqup_trans … H12 H20) -G2 -Y -T2 + #H10 @(IH2 … H10) -IH2 /2 width=5 by csx_fqup_conf/ +(* + #T2 #HT02 #H #G3 #L3 #T3 #HT23 elim (fqup_cpxs_trans_neq … H10 … HT02 H) -T0 + /4 width=8 by fqup_fqus_trans, fqup_fqus/ +*) +| (* #T0 #HT20 #H elim (fqus_cpxs_trans_neq … H12 … HT20 H) -T2 /3 width=4 by/ *) +| #L0 #HL20 #HnT2 @(IH4 L0) /3 width=3 by lpxs_trans, lleq_canc_sn/ + + + + + + | /3 width=3 by / + [ /2 width=3 + + lapply (lpxs_trans … HYL2 … HL20) + #HYL0 lapply (tollens ???? HnT2) [ @(lleq_canc_sn … HT2) | skip ] -L2 + #HnT2 elim (fqus_lpxs_trans_nlleq … H12 … HYL0 HnT2) - + + + lapply (lleq_canc_sn … L0 … HT2) + + + + | + +elim (lpxs_lleq_fqup_trans … H12 … HYL2 HT2) -L2 + + +] +qed-. + +lemma csx_ind_fpbc: ∀h,g. ∀R:relation3 genv lenv term. + (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → + (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → + R G1 L1 T1 + ) → + ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → R G L T. +/4 width=8 by csx_ind_fpbc_fqus/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazysn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazysn_5.ma new file mode 100644 index 000000000..469eecac4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazysn_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 T ] break term 46 L )" + non associative with precedence 45 + for @{ 'LazySN $h $g $T $G $L }. 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 bdd170770..6e021dd88 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" * } { - [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tstc_vector" + "csx_aaa" * ] - [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lpx" * ] + [ "lsx ()" "lsx_cpxs" + "lsx_fpbc" + "lsx_csx" * ] + [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tstc_vector" + "csx_aaa" * ] + [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lpx" + "csx_fpbs" * ] } ] [ { "\"big tree\" parallel computation" * } { -- 2.39.2