From c28e3d93b588796bfbbfd6b2ec9dd86f405b2b00 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 6 Oct 2013 11:47:25 +0000 Subject: [PATCH] - big-tree reduction is now based on extended reduction - some renaming --- .../lambdadelta/basic_2/computation/cpre.ma | 6 +- .../lambdadelta/basic_2/computation/cpxe.ma | 6 +- .../basic_2/computation/{csn.ma => csx.ma} | 50 +++++------ .../computation/{csn_aaa.ma => csx_aaa.ma} | 6 +- .../computation/{csn_alt.ma => csx_alt.ma} | 38 ++++---- .../computation/{csn_lift.ma => csx_lift.ma} | 38 ++++---- .../computation/{csn_lpx.ma => csx_lpx.ma} | 80 ++++++++--------- ...{csn_tstc_vector.ma => csx_tstc_vector.ma} | 76 ++++++++-------- .../{csn_vector.ma => csx_vector.ma} | 16 ++-- .../lambdadelta/basic_2/computation/fpbg.ma | 90 +++++++++++++++++++ .../computation/{ygt_ygt.ma => fpbg_fpbg.ma} | 6 +- .../computation/{ygt_lift.ma => fpbg_lift.ma} | 12 +-- .../lambdadelta/basic_2/computation/fpbs.ma | 29 +++--- .../basic_2/computation/fpbs_fpbs.ma | 2 +- .../basic_2/computation/fpbs_lift.ma | 8 +- .../lambdadelta/basic_2/computation/ygt.ma | 86 ------------------ .../lambdadelta/basic_2/dynamic/snv_aaa.ma | 4 +- .../lambdadelta/basic_2/dynamic/snv_cpcs.ma | 10 +-- .../lambdadelta/basic_2/dynamic/snv_da_lpr.ma | 26 +++--- .../lambdadelta/basic_2/dynamic/snv_lpr.ma | 64 ++++++------- .../lambdadelta/basic_2/dynamic/snv_lsstas.ma | 10 +-- .../basic_2/dynamic/snv_lsstas_lpr.ma | 46 +++++----- .../contribs/lambdadelta/basic_2/names.txt | 7 +- .../lambdadelta/basic_2/reduction/fpb.ma | 18 ++-- .../lambdadelta/basic_2/reduction/fpb_lift.ma | 25 ++++++ .../basic_2/reduction/{ysc.ma => fpbc.ma} | 25 +++--- .../basic_2/reduction/fpbc_lift.ma | 28 ++++++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 11 +-- 28 files changed, 450 insertions(+), 373 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/computation/{csn.ma => csx.ma} (78%) rename matita/matita/contribs/lambdadelta/basic_2/computation/{csn_aaa.ma => csx_aaa.ma} (88%) rename matita/matita/contribs/lambdadelta/basic_2/computation/{csn_alt.ma => csx_alt.ma} (80%) rename matita/matita/contribs/lambdadelta/basic_2/computation/{csn_lift.ma => csx_lift.ma} (80%) rename matita/matita/contribs/lambdadelta/basic_2/computation/{csn_lpx.ma => csx_lpx.ma} (70%) rename matita/matita/contribs/lambdadelta/basic_2/computation/{csn_tstc_vector.ma => csx_tstc_vector.ma} (66%) rename matita/matita/contribs/lambdadelta/basic_2/computation/{csn_vector.ma => csx_vector.ma} (80%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma rename matita/matita/contribs/lambdadelta/basic_2/computation/{ygt_ygt.ma => fpbg_fpbg.ma} (88%) rename matita/matita/contribs/lambdadelta/basic_2/computation/{ygt_lift.ma => fpbg_lift.ma} (78%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/ygt.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_lift.ma rename matita/matita/contribs/lambdadelta/basic_2/reduction/{ysc.ma => fpbc.ma} (64%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc_lift.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma index aeb5c6046..61dadbcde 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma @@ -14,7 +14,7 @@ include "basic_2/notation/relations/peval_4.ma". include "basic_2/computation/cprs.ma". -include "basic_2/computation/csn.ma". +include "basic_2/computation/csx.ma". (* CONTEXT-SENSITIVE PARALLEL EVALUATION ON TERMS **************************) @@ -27,8 +27,8 @@ interpretation "context-sensitive parallel evaluation (term)" (* Basic_properties *********************************************************) (* Basic_1: was just: nf2_sn3 *) -lemma csn_cpre: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → ∃T2. ⦃G, L⦄ ⊢ T1 ➡* 𝐍⦃T2⦄. -#h #g #G #L #T1 #H @(csn_ind … H) -T1 +lemma csx_cpre: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → ∃T2. ⦃G, L⦄ ⊢ T1 ➡* 𝐍⦃T2⦄. +#h #g #G #L #T1 #H @(csx_ind … H) -T1 #T1 #_ #IHT1 elim (cnr_dec G L T1) /3 width=3/ * #T #H1T1 #H2T1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxe.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxe.ma index e0d59bb52..3d67c002c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxe.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxe.ma @@ -14,7 +14,7 @@ include "basic_2/notation/relations/peval_6.ma". include "basic_2/computation/cpxs.ma". -include "basic_2/computation/csn.ma". +include "basic_2/computation/csx.ma". (* CONTEXT-SENSITIVE EXTENDED PARALLEL EVALUATION ON TERMS ******************) @@ -26,8 +26,8 @@ interpretation "context-sensitive extended parallel evaluation (term)" (* Basic_properties *********************************************************) -lemma csn_cpxe: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → ∃T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] 𝐍⦃T2⦄. -#h #g #G #L #T1 #H @(csn_ind … H) -T1 +lemma csx_cpxe: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → ∃T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] 𝐍⦃T2⦄. +#h #g #G #L #T1 #H @(csx_ind … H) -T1 #T1 #_ #IHT1 elim (cnx_dec h g G L T1) /3 width=3/ * #T #H1T1 #H2T1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma similarity index 78% rename from matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma index 93d49b4fe..61174c0ff 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma @@ -17,16 +17,16 @@ include "basic_2/reduction/cnx.ma". (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) -definition csn: ∀h. sd h → relation3 genv lenv term ≝ +definition csx: ∀h. sd h → relation3 genv lenv term ≝ λh,g,G,L. SN … (cpx h g G L) (eq …). interpretation "context-sensitive extended strong normalization (term)" - 'SN h g G L T = (csn h g G L T). + 'SN h g G L T = (csx h g G L T). (* Basic eliminators ********************************************************) -lemma csn_ind: ∀h,g,G,L. ∀R:predicate term. +lemma csx_ind: ∀h,g,G,L. ∀R:predicate term. (∀T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → (∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → (T1 = T2 → ⊥) → R T2) → R T1 @@ -39,83 +39,83 @@ qed-. (* Basic properties *********************************************************) (* Basic_1: was just: sn3_pr2_intro *) -lemma csn_intro: ∀h,g,G,L,T1. +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. -lemma csn_cpx_trans: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → +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 -@csn_intro #T #HLT2 #HT2 +@csx_intro #T #HLT2 #HT2 elim (term_eq_dec T1 T2) #HT12 [ -IHT1 -HLT12 destruct /3 width=1/ | -HT1 -HT2 /3 width=4/ qed-. (* Basic_1: was just: sn3_nf2 *) -lemma cnx_csn: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ ⬊*[h, g] T. +lemma cnx_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ ⬊*[h, g] T. /2 width=1/ qed. lemma cnx_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 #IHl #k #Hkl lapply (deg_next_SO … Hkl) -Hkl -#Hkl @csn_intro #X #H #HX elim (cpx_inv_sort1 … H) -H +#Hkl @csx_intro #X #H #HX elim (cpx_inv_sort1 … H) -H [ #H destruct elim HX // | -HX * #l0 #_ #H destruct -l0 /2 width=1/ ] qed. (* Basic_1: was just: sn3_cast *) -lemma csn_cast: ∀h,g,G,L,W. ⦃G, L⦄ ⊢ ⬊*[h, g] W → +lemma csx_cast: ∀h,g,G,L,W. ⦃G, L⦄ ⊢ ⬊*[h, g] W → ∀T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓝW.T. -#h #g #G #L #W #HW @(csn_ind … HW) -W #W #HW #IHW #T #HT @(csn_ind … HT) -T #T #HT #IHT -@csn_intro #X #H1 #H2 +#h #g #G #L #W #HW @(csx_ind … HW) -W #W #HW #IHW #T #HT @(csx_ind … HT) -T #T #HT #IHT +@csx_intro #X #H1 #H2 elim (cpx_inv_cast1 … H1) -H1 [ * #W0 #T0 #HLW0 #HLT0 #H destruct elim (eq_false_inv_tpair_sn … H2) -H2 - [ /3 width=3 by csn_cpx_trans/ + [ /3 width=3 by csx_cpx_trans/ | -HLW0 * #H destruct /3 width=1/ ] -|2,3: /3 width=3 by csn_cpx_trans/ +|2,3: /3 width=3 by csx_cpx_trans/ ] qed. (* Basic forward lemmas *****************************************************) -fact csn_fwd_pair_sn_aux: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ ⬊*[h, g] U → +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 -@csn_intro #V2 #HLV2 #HV2 +@csx_intro #V2 #HLV2 #HV2 @(IH (②{I}V2.T)) -IH // /2 width=1/ -HLV2 #H destruct /2 width=1/ qed-. (* Basic_1: was just: sn3_gen_head *) -lemma csn_fwd_pair_sn: ∀h,g,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ②{I}V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] V. -/2 width=5 by csn_fwd_pair_sn_aux/ qed-. +lemma csx_fwd_pair_sn: ∀h,g,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ②{I}V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] V. +/2 width=5 by csx_fwd_pair_sn_aux/ qed-. -fact csn_fwd_bind_dx_aux: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ ⬊*[h, g] U → +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 -@csn_intro #T2 #HLT2 #HT2 +@csx_intro #T2 #HLT2 #HT2 @(IH (ⓑ{a,I}V.T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/ qed-. (* Basic_1: was just: sn3_gen_bind *) -lemma csn_fwd_bind_dx: ∀h,g,a,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓑ{a,I}V.T → ⦃G, L.ⓑ{I}V⦄ ⊢ ⬊*[h, g] T. -/2 width=4 by csn_fwd_bind_dx_aux/ qed-. +lemma csx_fwd_bind_dx: ∀h,g,a,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓑ{a,I}V.T → ⦃G, L.ⓑ{I}V⦄ ⊢ ⬊*[h, g] T. +/2 width=4 by csx_fwd_bind_dx_aux/ qed-. -fact csn_fwd_flat_dx_aux: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ ⬊*[h, g] U → +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 -@csn_intro #T2 #HLT2 #HT2 +@csx_intro #T2 #HLT2 #HT2 @(IH (ⓕ{I}V.T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/ qed-. (* Basic_1: was just: sn3_gen_flat *) -lemma csn_fwd_flat_dx: ∀h,g,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓕ{I}V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] T. -/2 width=5 by csn_fwd_flat_dx_aux/ qed-. +lemma csx_fwd_flat_dx: ∀h,g,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓕ{I}V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] T. +/2 width=5 by csx_fwd_flat_dx_aux/ qed-. (* Basic_1: removed theorems 14: sn3_cdelta diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma similarity index 88% rename from matita/matita/contribs/lambdadelta/basic_2/computation/csn_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma index e8b3ffb88..d951e4154 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma @@ -13,13 +13,13 @@ (**************************************************************************) include "basic_2/computation/acp_aaa.ma". -include "basic_2/computation/csn_tstc_vector.ma". +include "basic_2/computation/csx_tstc_vector.ma". (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) (* Main properties concerning atomic arity assignment ***********************) -theorem aaa_csn: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⬊*[h, g] T. +theorem aaa_csx: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⬊*[h, g] T. #h #g #G #L #T #A #H -@(acp_aaa … (csn_acp h g) (csn_acr h g) … H) +@(acp_aaa … (csx_acp h g) (csx_acr h g) … H) qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_alt.ma similarity index 80% rename from matita/matita/contribs/lambdadelta/basic_2/computation/csn_alt.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/csx_alt.ma index 5985f9548..7c95fed6e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_alt.ma @@ -14,21 +14,21 @@ include "basic_2/notation/relations/snalt_5.ma". include "basic_2/computation/cpxs.ma". -include "basic_2/computation/csn.ma". +include "basic_2/computation/csx.ma". (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) -(* alternative definition of csn *) -definition csna: ∀h. sd h → relation3 genv lenv term ≝ +(* alternative definition of csx *) +definition csxa: ∀h. sd h → relation3 genv lenv term ≝ λh,g,G,L. SN … (cpxs h g G L) (eq …). interpretation "context-sensitive extended strong normalization (term) alternative" - 'SNAlt h g G L T = (csna h g G L T). + 'SNAlt h g G L T = (csxa h g G L T). (* Basic eliminators ********************************************************) -lemma csna_ind: ∀h,g,G,L. ∀R:predicate term. +lemma csxa_ind: ∀h,g,G,L. ∀R:predicate term. (∀T1. ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T1 → (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → R T2) → R T1 ) → @@ -40,32 +40,32 @@ qed-. (* Basic properties *********************************************************) (* Basic_1: was just: sn3_intro *) -lemma csna_intro: ∀h,g,G,L,T1. +lemma csxa_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. -fact csna_intro_aux: ∀h,g,G,L,T1. ( +fact csxa_intro_aux: ∀h,g,G,L,T1. ( ∀T,T2. ⦃G, L⦄ ⊢ T ➡*[h, g] T2 → T1 = T → (T1 = T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T2 ) → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T1. /4 width=3/ qed-. (* Basic_1: was just: sn3_pr3_trans (old version) *) -lemma csna_cpxs_trans: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T1 → +lemma csxa_cpxs_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 -@csna_intro #T #HLT2 #HT2 +@csxa_intro #T #HLT2 #HT2 elim (term_eq_dec T1 T2) #HT12 [ -IHT1 -HLT12 destruct /3 width=1/ | -HT1 -HT2 /3 width=4/ qed. (* Basic_1: was just: sn3_pr2_intro (old version) *) -lemma csna_intro_cpx: ∀h,g,G,L,T1. ( +lemma csxa_intro_cpx: ∀h,g,G,L,T1. ( ∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → (T1 = T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T2 ) → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T1. #h #g #G #L #T1 #H -@csna_intro_aux #T #T2 #H @(cpxs_ind_dx … H) -T +@csxa_intro_aux #T #T2 #H @(cpxs_ind_dx … H) -T [ -H #H destruct #H elim H // | #T0 #T #HLT1 #HLT2 #IHT #HT10 #HT12 destruct @@ -78,27 +78,27 @@ qed. (* Main properties **********************************************************) -theorem csn_csna: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T. -#h #g #G #L #T #H @(csn_ind … H) -T /4 width=1/ +theorem csx_csxa: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T. +#h #g #G #L #T #H @(csx_ind … H) -T /4 width=1/ qed. -theorem csna_csn: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] T. -#h #g #G #L #T #H @(csna_ind … H) -T /4 width=1/ +theorem csxa_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] T. +#h #g #G #L #T #H @(csxa_ind … H) -T /4 width=1/ qed. (* Basic_1: was just: sn3_pr3_trans *) -lemma csn_cpxs_trans: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → +lemma csx_cpxs_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 #HT1 #T2 #H @(cpxs_ind … H) -T2 // /2 width=3 by csn_cpx_trans/ +#h #g #G #L #T1 #HT1 #T2 #H @(cpxs_ind … H) -T2 // /2 width=3 by csx_cpx_trans/ qed-. (* Main eliminators *********************************************************) -lemma csn_ind_alt: ∀h,g,G,L. ∀R:predicate term. +lemma csx_ind_alt: ∀h,g,G,L. ∀R:predicate term. (∀T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → R T2) → R T1 ) → ∀T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → R T. -#h #g #G #L #R #H0 #T1 #H @(csna_ind … (csn_csna … H)) -T1 #T1 #HT1 #IHT1 +#h #g #G #L #R #H0 #T1 #H @(csxa_ind … (csx_csxa … H)) -T1 #T1 #HT1 #IHT1 @H0 -H0 /2 width=1/ -HT1 /3 width=1/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma similarity index 80% rename from matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma index 6b52e5b00..c431c349b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma @@ -14,27 +14,27 @@ include "basic_2/reduction/cnx_lift.ma". include "basic_2/computation/acp.ma". -include "basic_2/computation/csn.ma". +include "basic_2/computation/csx.ma". (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) (* Relocation properties ****************************************************) (* Basic_1: was just: sn3_lift *) -lemma csn_lift: ∀h,g,G,L2,L1,T1,d,e. ⦃G, L1⦄ ⊢ ⬊*[h, g] T1 → +lemma csx_lift: ∀h,g,G,L2,L1,T1,d,e. ⦃G, L1⦄ ⊢ ⬊*[h, g] T1 → ∀T2. ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → ⦃G, L2⦄ ⊢ ⬊*[h, g] T2. #h #g #G #L2 #L1 #T1 #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL21 #HT12 -@csn_intro #T #HLT2 #HT2 +@csx_intro #T #HLT2 #HT2 elim (cpx_inv_lift1 … HLT2 … HL21 … HT12) -HLT2 #T0 #HT0 #HLT10 @(IHT1 … HLT10) // -L1 -L2 #H destruct >(lift_mono … HT0 … HT12) in HT2; -T1 /2 width=1/ qed. (* Basic_1: was just: sn3_gen_lift *) -lemma csn_inv_lift: ∀h,g,G,L2,L1,T1,d,e. ⦃G, L1⦄ ⊢ ⬊*[h, g] T1 → +lemma csx_inv_lift: ∀h,g,G,L2,L1,T1,d,e. ⦃G, L1⦄ ⊢ ⬊*[h, g] T1 → ∀T2. ⇩[d, e] L1 ≡ L2 → ⇧[d, e] T2 ≡ T1 → ⦃G, L2⦄ ⊢ ⬊*[h, g] T2. #h #g #G #L2 #L1 #T1 #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL12 #HT21 -@csn_intro #T #HLT2 #HT2 +@csx_intro #T #HLT2 #HT2 elim (lift_total T d e) #T0 #HT0 lapply (cpx_lift … HLT2 … HL12 … HT21 … HT0) -HLT2 #HLT10 @(IHT1 … HLT10) // -L1 -L2 #H destruct @@ -44,34 +44,34 @@ qed. (* Advanced properties ******************************************************) (* Basic_1: was just: sn3_abbr *) -lemma csn_lref_bind: ∀h,g,I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ ⬊*[h, g] V → ⦃G, L⦄ ⊢ ⬊*[h, g] #i. +lemma csx_lref_bind: ∀h,g,I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ ⬊*[h, g] V → ⦃G, L⦄ ⊢ ⬊*[h, g] #i. #h #g #I #G #L #K #V #i #HLK #HV -@csn_intro #X #H #Hi +@csx_intro #X #H #Hi elim (cpx_inv_lref1 … H) -H [ #H destruct elim Hi // | -Hi * #I0 #K0 #V0 #V1 #HLK0 #HV01 #HV1 lapply (ldrop_mono … HLK0 … HLK) -HLK #H destruct lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #HLK - @(csn_lift … HLK HV1) -HLK -HV1 - @(csn_cpx_trans … HV) -HV // + @(csx_lift … HLK HV1) -HLK -HV1 + @(csx_cpx_trans … HV) -HV // ] qed. -lemma csn_appl_simple: ∀h,g,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → ∀T1. +lemma csx_appl_simple: ∀h,g,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → ∀T1. (∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → (T1 = T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T2) → 𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T1. -#h #g #G #L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #IHT1 #HT1 -@csn_intro #X #H1 #H2 +#h #g #G #L #V #H @(csx_ind … H) -V #V #_ #IHV #T1 #IHT1 #HT1 +@csx_intro #X #H1 #H2 elim (cpx_inv_appl1_simple … H1) // -H1 #V0 #T0 #HLV0 #HLT10 #H destruct elim (eq_false_inv_tpair_dx … H2) -H2 [ -IHV -HT1 #HT10 - @(csn_cpx_trans … (ⓐV.T0)) /2 width=1/ -HLV0 + @(csx_cpx_trans … (ⓐV.T0)) /2 width=1/ -HLV0 @IHT1 -IHT1 // /2 width=1/ | -HLT10 * #H #HV0 destruct @IHV -IHV // -HT1 /2 width=1/ -HV0 #T2 #HLT02 #HT02 - @(csn_cpx_trans … (ⓐV.T2)) /2 width=1/ -HLV0 + @(csx_cpx_trans … (ⓐV.T2)) /2 width=1/ -HLV0 @IHT1 -IHT1 // -HLT02 /2 width=1/ ] qed. @@ -79,23 +79,23 @@ qed. (* Advanced inversion lemmas ************************************************) (* Basic_1: was: sn3_gen_def *) -lemma csn_inv_lref_bind: ∀h,g,I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → +lemma csx_inv_lref_bind: ∀h,g,I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ ⊢ ⬊*[h, g] #i → ⦃G, K⦄ ⊢ ⬊*[h, g] V. #h #g #I #G #L #K #V #i #HLK #Hi elim (lift_total V 0 (i+1)) #V0 #HV0 lapply (ldrop_fwd_ldrop2 … HLK) #H0LK -@(csn_inv_lift … H0LK … HV0) -H0LK -@(csn_cpx_trans … Hi) -Hi /2 width=7/ +@(csx_inv_lift … H0LK … HV0) -H0LK +@(csx_cpx_trans … Hi) -Hi /2 width=7/ qed-. (* Main properties **********************************************************) -theorem csn_acp: ∀h,g. acp (cpx h g) (eq …) (csn h g). +theorem csx_acp: ∀h,g. acp (cpx h g) (eq …) (csx h g). #h #g @mk_acp [ #G #L elim (deg_total h g 0) #l #Hl lapply (cnx_sort_iter … L … Hl) /2 width=2/ | @cnx_lift -| /2 width=3 by csn_fwd_flat_dx/ +| /2 width=3 by csx_fwd_flat_dx/ | /2 width=1/ ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma similarity index 70% rename from matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpx.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma index 0fbc4c66f..a365b4310 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma @@ -14,55 +14,55 @@ include "basic_2/grammar/tstc_tstc.ma". include "basic_2/computation/cpxs_cpxs.ma". -include "basic_2/computation/csn_alt.ma". -include "basic_2/computation/csn_lift.ma". +include "basic_2/computation/csx_alt.ma". +include "basic_2/computation/csx_lift.ma". (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) (* Advanced properties ******************************************************) -lemma csn_lpx_conf: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → +lemma csx_lpx_conf: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → ∀T. ⦃G, L1⦄ ⊢ ⬊*[h, g] T → ⦃G, L2⦄ ⊢ ⬊*[h, g] T. -#h #g #G #L1 #L2 #HL12 #T #H @(csn_ind_alt … H) -T #T #_ #IHT -@csn_intro #T0 #HLT0 #HT0 +#h #g #G #L1 #L2 #HL12 #T #H @(csx_ind_alt … H) -T #T #_ #IHT +@csx_intro #T0 #HLT0 #HT0 @IHT /2 width=2/ -IHT -HT0 /2 width=3 by lpx_cpx_trans/ qed. -lemma csn_abst: ∀h,g,a,G,L,W. ⦃G, L⦄ ⊢ ⬊*[h, g] W → +lemma csx_abst: ∀h,g,a,G,L,W. ⦃G, L⦄ ⊢ ⬊*[h, g] W → ∀T. ⦃G, L.ⓛW⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓛ{a}W.T. -#h #g #a #G #L #W #HW @(csn_ind … HW) -W #W #_ #IHW #T #HT @(csn_ind … HT) -T #T #HT #IHT -@csn_intro #X #H1 #H2 +#h #g #a #G #L #W #HW @(csx_ind … HW) -W #W #_ #IHW #T #HT @(csx_ind … HT) -T #T #HT #IHT +@csx_intro #X #H1 #H2 elim (cpx_inv_abst1 … H1) -H1 #W0 #T0 #HLW0 #HLT0 #H destruct elim (eq_false_inv_tpair_sn … H2) -H2 -[ -IHT #H lapply (csn_cpx_trans … HLT0) // -HT - #HT0 lapply (csn_lpx_conf … (L.ⓛW0) … HT0) -HT0 /2 width=1/ /3 width=1/ +[ -IHT #H lapply (csx_cpx_trans … HLT0) // -HT + #HT0 lapply (csx_lpx_conf … (L.ⓛW0) … HT0) -HT0 /2 width=1/ /3 width=1/ | -IHW -HLW0 -HT * #H destruct /3 width=1/ ] qed. -lemma csn_abbr: ∀h,g,a,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → +lemma csx_abbr: ∀h,g,a,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → ∀T. ⦃G, L.ⓓV⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V. T. -#h #g #a #G #L #V #HV elim HV -V #V #_ #IHV #T #HT @(csn_ind_alt … HT) -T #T #HT #IHT -@csn_intro #X #H1 #H2 +#h #g #a #G #L #V #HV elim HV -V #V #_ #IHV #T #HT @(csx_ind_alt … HT) -T #T #HT #IHT +@csx_intro #X #H1 #H2 elim (cpx_inv_abbr1 … H1) -H1 * [ #V1 #T1 #HLV1 #HLT1 #H destruct elim (eq_false_inv_tpair_sn … H2) -H2 [ #HV1 @IHV // /2 width=1/ -HV1 - @(csn_lpx_conf … (L.ⓓV)) /2 width=1/ -HLV1 /2 width=3 by csn_cpx_trans/ + @(csx_lpx_conf … (L.ⓓV)) /2 width=1/ -HLV1 /2 width=3 by csx_cpx_trans/ | -IHV -HLV1 * #H destruct /3 width=1/ ] | -IHV -IHT -H2 #T0 #HLT0 #HT0 - lapply (csn_cpx_trans … HT … HLT0) -T #HLT0 - lapply (csn_inv_lift … HLT0 … HT0) -T0 /2 width=3/ + lapply (csx_cpx_trans … HT … HLT0) -T #HLT0 + lapply (csx_inv_lift … HLT0 … HT0) -T0 /2 width=3/ ] qed. -fact csn_appl_beta_aux: ∀h,g,a,G,L,U1. ⦃G, L⦄ ⊢ ⬊*[h, g] U1 → +fact csx_appl_beta_aux: ∀h,g,a,G,L,U1. ⦃G, L⦄ ⊢ ⬊*[h, g] U1 → ∀V,W,T1. U1 = ⓓ{a}ⓝW.V.T1 → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.ⓛ{a}W.T1. -#h #g #a #G #L #X #H @(csn_ind … H) -X +#h #g #a #G #L #X #H @(csx_ind … H) -X #X #HT1 #IHT1 #V #W #T1 #H1 destruct -@csn_intro #X #H1 #H2 +@csx_intro #X #H1 #H2 elim (cpx_inv_appl1 … H1) -H1 * [ -HT1 #V0 #Y #HLV0 #H #H0 destruct elim (cpx_inv_abst1 … H) -H #W0 #T0 #HLW0 #HLT0 #H destruct @@ -70,21 +70,21 @@ elim (cpx_inv_appl1 … H1) -H1 * lapply (lsubr_cpx_trans … HLT0 (L.ⓓⓝW.V) ?) -HLT0 [ /2 width=1/ ] /3 width=1/ | -IHT1 -H2 #b #V0 #W0 #W2 #T0 #T2 #HLV0 #HLW02 #HLT02 #H1 #H3 destruct lapply (lsubr_cpx_trans … HLT02 (L.ⓓⓝW0.V) ?) -HLT02 [ /2 width=1/ ] #HT02 - @(csn_cpx_trans … HT1) -HT1 /3 width=1/ + @(csx_cpx_trans … HT1) -HT1 /3 width=1/ | -HT1 -IHT1 -H2 #b #V0 #V1 #W0 #W1 #T0 #T3 #_ #_ #_ #_ #H destruct ] qed-. (* Basic_1: was just: sn3_beta *) -lemma csn_appl_beta: ∀h,g,a,G,L,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}ⓝW.V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.ⓛ{a}W.T. -/2 width=3 by csn_appl_beta_aux/ qed. +lemma csx_appl_beta: ∀h,g,a,G,L,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}ⓝW.V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.ⓛ{a}W.T. +/2 width=3 by csx_appl_beta_aux/ qed. -fact csn_appl_theta_aux: ∀h,g,a,G,L,U. ⦃G, L⦄ ⊢ ⬊*[h, g] U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 → +fact csx_appl_theta_aux: ∀h,g,a,G,L,U. ⦃G, L⦄ ⊢ ⬊*[h, g] U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 → ∀V,T. U = ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV1.ⓓ{a}V.T. -#h #g #a #G #L #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct -lapply (csn_fwd_pair_sn … HVT) #HV -lapply (csn_fwd_bind_dx … HVT) -HVT #HVT -@csn_intro #X #HL #H +#h #g #a #G #L #X #H @(csx_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct +lapply (csx_fwd_pair_sn … HVT) #HV +lapply (csx_fwd_bind_dx … HVT) -HVT #HVT +@csx_intro #X #HL #H elim (cpx_inv_appl1 … HL) -HL * [ -HV #V0 #Y #HLV10 #HL #H0 destruct elim (cpx_inv_abbr1 … HL) -HL * @@ -103,37 +103,37 @@ elim (cpx_inv_appl1 … HL) -HL * @(IHVT … H … HV04) -IHVT // -H -HV04 /4 width=1/ ] | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct - lapply (csn_cpx_trans … HVT (ⓐV2.T0) ?) /2 width=1/ -T #HVT0 - lapply (csn_inv_lift … L … 1 HVT0 ? ? ?) -HVT0 [ /2 width=4/ |2,3: skip | /2 width=1/ ] -V2 -T0 #HVY - @(csn_cpx_trans … HVY) /2 width=1/ + lapply (csx_cpx_trans … HVT (ⓐV2.T0) ?) /2 width=1/ -T #HVT0 + lapply (csx_inv_lift … L … 1 HVT0 ? ? ?) -HVT0 [ /2 width=4/ |2,3: skip | /2 width=1/ ] -V2 -T0 #HVY + @(csx_cpx_trans … HVY) /2 width=1/ ] | -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #W1 #T0 #T1 #_ #_ #_ #H destruct | -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HV03 #HLW01 #HLT01 #H1 #H2 destruct lapply (cpx_lift … HLV10 (L. ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /2 width=1/ #HLV23 - @csn_abbr /2 width=3 by csn_cpx_trans/ -HV - @(csn_lpx_conf … (L. ⓓW0)) /2 width=1/ -W1 - @(csn_cpxs_trans … HVT) -HVT /3 width=1/ + @csx_abbr /2 width=3 by csx_cpx_trans/ -HV + @(csx_lpx_conf … (L. ⓓW0)) /2 width=1/ -W1 + @(csx_cpxs_trans … HVT) -HVT /3 width=1/ ] qed-. -lemma csn_appl_theta: ∀h,g,a,V1,V2. ⇧[0, 1] V1 ≡ V2 → +lemma csx_appl_theta: ∀h,g,a,V1,V2. ⇧[0, 1] V1 ≡ V2 → ∀G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV1.ⓓ{a}V.T. -/2 width=5 by csn_appl_theta_aux/ qed. +/2 width=5 by csx_appl_theta_aux/ qed. (* Basic_1: was just: sn3_appl_appl *) -lemma csn_appl_simple_tstc: ∀h,g,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → ∀T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → +lemma csx_appl_simple_tstc: ∀h,g,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → ∀T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 ≃ T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T2) → 𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T1. -#h #g #G #L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #H @(csn_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1 -@csn_intro #X #HL #H +#h #g #G #L #V #H @(csx_ind … H) -V #V #_ #IHV #T1 #H @(csx_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1 +@csx_intro #X #HL #H elim (cpx_inv_appl1_simple … HL) -HL // #V0 #T0 #HLV0 #HLT10 #H0 destruct elim (eq_false_inv_tpair_sn … H) -H [ -IHT1 #HV0 - @(csn_cpx_trans … (ⓐV0.T1)) /2 width=1/ -HLT10 + @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1/ -HLT10 @IHV -IHV // -H1T1 -H3T1 /2 width=1/ -HV0 #T2 #HLT12 #HT12 - @(csn_cpx_trans … (ⓐV.T2)) /2 width=1/ -HLV0 + @(csx_cpx_trans … (ⓐV.T2)) /2 width=1/ -HLV0 @H2T1 -H2T1 // -HLT12 /2 width=1/ | -IHV -H1T1 -HLV0 * #H #H1T10 destruct elim (tstc_dec T1 T0) #H2T10 diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma similarity index 66% rename from matita/matita/contribs/lambdadelta/basic_2/computation/csn_tstc_vector.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma index 1eee44b51..f32a267c9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_tstc_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma @@ -14,76 +14,76 @@ include "basic_2/computation/acp_cr.ma". include "basic_2/computation/cpxs_tstc_vector.ma". -include "basic_2/computation/csn_lpx.ma". -include "basic_2/computation/csn_vector.ma". +include "basic_2/computation/csx_lpx.ma". +include "basic_2/computation/csx_vector.ma". (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERM VECTORS *************) (* Advanced properties ******************************************************) (* Basic_1: was just: sn3_appls_lref *) -lemma csn_applv_cnx: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → +lemma csx_applv_cnx: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T. -#h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(cnx_csn … H2T) ] (**) (* /2 width=1/ does not work *) +#h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(cnx_csx … H2T) ] (**) (* /2 width=1/ does not work *) #V #Vs #IHV #H -elim (csnv_inv_cons … H) -H #HV #HVs -@csn_appl_simple_tstc // -HV /2 width=1/ -IHV -HVs +elim (csxv_inv_cons … H) -H #HV #HVs +@csx_appl_simple_tstc // -HV /2 width=1/ -IHV -HVs #X #H #H0 lapply (cpxs_fwd_cnx_vector … H) -H // -H1T -H2T #H elim (H0) -H0 // qed. -lemma csn_applv_sort: ∀h,g,G,L,k,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.⋆k. +lemma csx_applv_sort: ∀h,g,G,L,k,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.⋆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 #IHl #k #Hkl lapply (deg_next_SO … Hkl) -Hkl #Hkl #Vs elim Vs -Vs /2 width=1/ #V #Vs #IHVs #HVVs -elim (csnv_inv_cons … HVVs) #HV #HVs -@csn_appl_simple_tstc // -HV /2 width=1/ -IHVs -HVs +elim (csxv_inv_cons … HVVs) #HV #HVs +@csx_appl_simple_tstc // -HV /2 width=1/ -IHVs -HVs #X #H #H0 elim (cpxs_fwd_sort_vector … H) -H #H [ elim H0 -H0 // -| -H0 @(csn_cpxs_trans … (Ⓐ(V@Vs).⋆(next h k))) /2 width=1/ +| -H0 @(csx_cpxs_trans … (Ⓐ(V@Vs).⋆(next h k))) /2 width=1/ ] qed. (* Basic_1: was just: sn3_appls_beta *) -lemma csn_applv_beta: ∀h,g,a,G,L,Vs,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓓ{a}ⓝW.V.T → +lemma csx_applv_beta: ∀h,g,a,G,L,Vs,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓓ{a}ⓝW.V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs. ⓐV.ⓛ{a}W.T. #h #g #a #G #L #Vs elim Vs -Vs /2 width=1/ #V0 #Vs #IHV #V #W #T #H1T -lapply (csn_fwd_pair_sn … H1T) #HV0 -lapply (csn_fwd_flat_dx … H1T) #H2T -@csn_appl_simple_tstc // -HV0 /2 width=1/ -IHV -H2T +lapply (csx_fwd_pair_sn … H1T) #HV0 +lapply (csx_fwd_flat_dx … H1T) #H2T +@csx_appl_simple_tstc // -HV0 /2 width=1/ -IHV -H2T #X #H #H0 elim (cpxs_fwd_beta_vector … H) -H #H [ -H1T elim H0 -H0 // -| -H0 @(csn_cpxs_trans … H1T) -H1T /2 width=1/ +| -H0 @(csx_cpxs_trans … H1T) -H1T /2 width=1/ ] qed. -lemma csn_applv_delta: ∀h,g,I,G,L,K,V1,i. ⇩[0, i] L ≡ K.ⓑ{I}V1 → +lemma csx_applv_delta: ∀h,g,I,G,L,K,V1,i. ⇩[0, i] L ≡ K.ⓑ{I}V1 → ∀V2. ⇧[0, i + 1] V1 ≡ V2 → ∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.V2) → ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.#i). #h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs [ #H lapply (ldrop_fwd_ldrop2 … HLK) #HLK0 - lapply (csn_inv_lift … H … HLK0 HV12) -V2 -HLK0 /2 width=5/ + lapply (csx_inv_lift … H … HLK0 HV12) -V2 -HLK0 /2 width=5/ | #V #Vs #IHV #H1T - lapply (csn_fwd_pair_sn … H1T) #HV - lapply (csn_fwd_flat_dx … H1T) #H2T - @csn_appl_simple_tstc // -HV /2 width=1/ -IHV -H2T + lapply (csx_fwd_pair_sn … H1T) #HV + lapply (csx_fwd_flat_dx … H1T) #H2T + @csx_appl_simple_tstc // -HV /2 width=1/ -IHV -H2T #X #H #H0 elim (cpxs_fwd_delta_vector … HLK … HV12 … H) -HLK -HV12 -H #H [ -H1T elim H0 -H0 // - | -H0 @(csn_cpxs_trans … H1T) -H1T /2 width=1/ + | -H0 @(csx_cpxs_trans … H1T) -H1T /2 width=1/ ] ] qed. (* Basic_1: was just: sn3_appls_abbr *) -lemma csn_applv_theta: ∀h,g,a,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → +lemma csx_applv_theta: ∀h,g,a,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → ∀V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V.ⒶV2s.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶV1s.ⓓ{a}V.T. #h #g #a #G #L #V1s #V2s * -V1s -V2s /2 width=1/ @@ -91,41 +91,41 @@ lemma csn_applv_theta: ∀h,g,a,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → generalize in match HV12; -HV12 generalize in match V2; -V2 generalize in match V1; -V1 elim H -V1s -V2s /2 width=3/ #V1s #V2s #V1 #V2 #HV12 #HV12s #IHV12s #W1 #W2 #HW12 #V #T #H -lapply (csn_appl_theta … HW12 … H) -H -HW12 #H -lapply (csn_fwd_pair_sn … H) #HW1 -lapply (csn_fwd_flat_dx … H) #H1 -@csn_appl_simple_tstc // -HW1 /2 width=3/ -IHV12s -H1 #X #H1 #H2 +lapply (csx_appl_theta … HW12 … H) -H -HW12 #H +lapply (csx_fwd_pair_sn … H) #HW1 +lapply (csx_fwd_flat_dx … H) #H1 +@csx_appl_simple_tstc // -HW1 /2 width=3/ -IHV12s -H1 #X #H1 #H2 elim (cpxs_fwd_theta_vector … (V2@V2s) … H1) -H1 /2 width=1/ -HV12s -HV12 [ -H #H elim H2 -H2 // -| -H2 #H1 @(csn_cpxs_trans … H) -H /2 width=1/ +| -H2 #H1 @(csx_cpxs_trans … H) -H /2 width=1/ ] qed. (* Basic_1: was just: sn3_appls_cast *) -lemma csn_applv_cast: ∀h,g,G,L,Vs,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.W → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T → +lemma csx_applv_cast: ∀h,g,G,L,Vs,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.W → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓝW.T. #h #g #G #L #Vs elim Vs -Vs /2 width=1/ #V #Vs #IHV #W #T #H1W #H1T -lapply (csn_fwd_pair_sn … H1W) #HV -lapply (csn_fwd_flat_dx … H1W) #H2W -lapply (csn_fwd_flat_dx … H1T) #H2T -@csn_appl_simple_tstc // -HV /2 width=1/ -IHV -H2W -H2T +lapply (csx_fwd_pair_sn … H1W) #HV +lapply (csx_fwd_flat_dx … H1W) #H2W +lapply (csx_fwd_flat_dx … H1T) #H2T +@csx_appl_simple_tstc // -HV /2 width=1/ -IHV -H2W -H2T #X #H #H0 elim (cpxs_fwd_cast_vector … H) -H #H [ -H1W -H1T elim H0 -H0 // -| -H1W -H0 @(csn_cpxs_trans … H1T) -H1T /2 width=1/ -| -H1T -H0 @(csn_cpxs_trans … H1W) -H1W /2 width=1/ +| -H1W -H0 @(csx_cpxs_trans … H1T) -H1T /2 width=1/ +| -H1T -H0 @(csx_cpxs_trans … H1W) -H1W /2 width=1/ ] qed. -theorem csn_acr: ∀h,g. acr (cpx h g) (eq …) (csn h g) (λG,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T). +theorem csx_acr: ∀h,g. acr (cpx h g) (eq …) (csx h g) (λG,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T). #h #g @mk_acr // [ /3 width=1/ |2,3,6: /2 width=1/ | /2 width=7/ | #G #L #V1s #V2s #HV12s #a #V #T #H #HV - @(csn_applv_theta … HV12s) -HV12s - @(csn_abbr) // -| @csn_lift + @(csx_applv_theta … HV12s) -HV12s + @(csx_abbr) // +| @csx_lift ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_vector.ma similarity index 80% rename from matita/matita/contribs/lambdadelta/basic_2/computation/csn_vector.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/csx_vector.ma index 73019d053..733666659 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_vector.ma @@ -13,30 +13,30 @@ (**************************************************************************) include "basic_2/grammar/term_vector.ma". -include "basic_2/computation/csn.ma". +include "basic_2/computation/csx.ma". (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERM VECTORS *************) -definition csnv: ∀h. sd h → relation3 genv lenv (list term) ≝ - λh,g,G,L. all … (csn h g G L). +definition csxv: ∀h. sd h → relation3 genv lenv (list term) ≝ + λh,g,G,L. all … (csx h g G L). interpretation "context-sensitive strong normalization (term vector)" - 'SN h g G L Ts = (csnv h g G L Ts). + 'SN h g G L Ts = (csxv h g G L Ts). (* Basic inversion lemmas ***************************************************) -lemma csnv_inv_cons: ∀h,g,G,L,T,Ts. ⦃G, L⦄ ⊢ ⬊*[h, g] T @ Ts → +lemma csxv_inv_cons: ∀h,g,G,L,T,Ts. ⦃G, L⦄ ⊢ ⬊*[h, g] T @ Ts → ⦃G, L⦄ ⊢ ⬊*[h, g] T ∧ ⦃G, L⦄ ⊢ ⬊*[h, g] Ts. normalize // qed-. (* Basic forward lemmas *****************************************************) -lemma csn_fwd_applv: ∀h,g,G,L,T,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Ⓐ Vs.T → +lemma csx_fwd_applv: ∀h,g,G,L,T,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Ⓐ Vs.T → ⦃G, L⦄ ⊢ ⬊*[h, g] Vs ∧ ⦃G, L⦄ ⊢ ⬊*[h, g] T. #h #g #G #L #T #Vs elim Vs -Vs /2 width=1/ #V #Vs #IHVs #HVs -lapply (csn_fwd_pair_sn … HVs) #HV -lapply (csn_fwd_flat_dx … HVs) -HVs #HVs +lapply (csx_fwd_pair_sn … HVs) #HV +lapply (csx_fwd_flat_dx … HVs) -HVs #HVs elim (IHVs HVs) -IHVs -HVs /3 width=1/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma new file mode 100644 index 000000000..98a890ffe --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma @@ -0,0 +1,90 @@ +(**************************************************************************) +(* ___ *) +(* ||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/btpredstarproper_8.ma". +include "basic_2/reduction/fpbc.ma". +include "basic_2/computation/fpbs.ma". + +(* "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **********************) + +inductive fpbg (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ +| fpbg_inj : ∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≻[h, g] ⦃G2, L2, T2⦄ → + fpbg h g G1 L1 T1 G2 L2 T2 +| fpbg_step: ∀G,L,L2,T. fpbg h g G1 L1 T1 G L T → ⦃G, L⦄ ⊢ ➡[h, g] L2 → fpbg h g G1 L1 T1 G L2 T +. + +interpretation "'big tree' proper parallel computation (closure)" + 'BTPRedStarProper h g G1 L1 T1 G2 L2 T2 = (fpbg h g G1 L1 T1 G2 L2 T2). + +(* Basic forvard lemmas *****************************************************) + +lemma fpbg_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G2 -L2 -T2 +/3 width=5 by fpbs_strap1, fpbc_fpb, fpb_lpx/ +qed-. + +(* Basic properties *********************************************************) + +lemma fpbc_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. +/3 width=5 by fpbg_inj, fpbg_step/ qed. + +lemma fpbg_strap1: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G, L, T⦄ → + ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 +lapply (fpbg_fwd_fpbs … H1) #H0 +elim (fpb_inv_fpbc … H2) -H2 [| * #HG2 #HL2 #HT2 destruct ] +/2 width=5 by fpbg_inj, fpbg_step/ +qed-. + +lemma fpbg_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ → + ⦃G, L, T⦄ >[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 elim H2 -G2 -L2 -T2 +/3 width=5 by fpbg_step, fpbg_inj, fpbs_strap2/ +qed-. + +lemma fpbg_fpbs_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G, L, T⦄ → + ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #HT1 #HT2 @(fpbs_ind … HT2) -G2 -L2 -T2 +/2 width=5 by fpbg_strap1/ +qed-. + +lemma fpbs_fpbg_trans: ∀h,g,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → + ∀G2,L2,T2. ⦃G, L, T⦄ >[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G #L1 #L #T1 #T #HT1 @(fpbs_ind … HT1) -G -L -T +/3 width=5 by fpbg_strap2/ +qed-. + +lemma fsupp_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsupp_ind … L2 T2 H) -G2 -L2 -T2 +/3 width=5 by fsupp_fpbs, fpbc_fsup, fpbc_fpbg, fpbg_inj/ +qed. + +lemma cpxs_fpbg: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → + ⦃G, L, T1⦄ >[h, g] ⦃G, L, T2⦄. +#h #g #G #L #T1 #T2 #H @(cpxs_ind … H) -T2 +[ #H elim H // +| #T #T2 #_ #HT2 #IHT1 #HT12 + elim (term_eq_dec T1 T) #H destruct + [ -IHT1 /4 width=1/ + | lapply (IHT1 … H) -IHT1 -H -HT12 #HT1 + @(fpbg_strap1 … HT1) -HT1 /2 width=1 by fpb_cpx/ + ] +] +qed. + +lemma cprs_fpbg: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → + ⦃G, L, T1⦄ >[h, g] ⦃G, L, T2⦄. +/3 width=1 by cprs_cpxs, cpxs_fpbg/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_ygt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma similarity index 88% rename from matita/matita/contribs/lambdadelta/basic_2/computation/ygt_ygt.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma index 98fd435a3..4f092111a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_ygt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma @@ -12,11 +12,11 @@ (* *) (**************************************************************************) -include "basic_2/computation/ygt.ma". +include "basic_2/computation/fpbg.ma". (* "BIG TREE" ORDER FOR CLOSURES ********************************************) (* Main properties **********************************************************) -theorem ygt_trans: ∀h,g. tri_transitive … (ygt h g). -/3 width=5 by ygt_fwd_fpbs, ygt_fpbs_trans/ qed-. +theorem fpbg_trans: ∀h,g. tri_transitive … (fpbg h g). +/3 width=5 by fpbg_fwd_fpbs, fpbg_fpbs_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma similarity index 78% rename from matita/matita/contribs/lambdadelta/basic_2/computation/ygt_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma index 1c75c8e3d..9afc2523b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma @@ -13,25 +13,27 @@ (**************************************************************************) include "basic_2/unfold/lsstas_lift.ma". -include "basic_2/computation/ygt.ma". +include "basic_2/reduction/fpb_lift.ma". +include "basic_2/reduction/fpbc_lift.ma". +include "basic_2/computation/fpbg.ma". (* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) (* Advanced properties ******************************************************) -lemma lsstas_ygt: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 → (T1 = T2 → ⊥) → - ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ >[h, g] ⦃G, L, T2⦄. +lemma lsstas_fpbg: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 → (T1 = T2 → ⊥) → + ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ >[h, g] ⦃G, L, T2⦄. #h #g #G #L #T1 #T2 #l2 #H @(lsstas_ind_dx … H) -l2 -T2 [ #H elim H // | #l2 #T #T2 #HT1 #HT2 #IHT1 #HT12 #l1 #Hl21 elim (term_eq_dec T1 T) #H destruct [ -IHT1 |] [ elim (le_inv_plus_l … Hl21) -Hl21 #_ #Hl1 - >(plus_minus_m_m … Hl1) -Hl1 /3 width=5 by ysc_ssta, ygt_inj/ + >(plus_minus_m_m … Hl1) -Hl1 /3 width=5 by ssta_fpbc, fpbg_inj/ | #Hl1 >commutative_plus in Hl21; #Hl21 elim (le_inv_plus_l … Hl21) -Hl21 #Hl12 #Hl21 lapply (lsstas_da_conf … HT1 … Hl1) -HT1 >(plus_minus_m_m … Hl12) -Hl12 - /4 width=5 by fpb_ssta, ygt_strap1/ + /4 width=5 by ssta_fpb, fpbg_strap1/ ] ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma index 361642dd1..dc8e8f185 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma @@ -15,8 +15,8 @@ include "basic_2/notation/relations/btpredstar_8.ma". include "basic_2/substitution/fsupp.ma". include "basic_2/reduction/fpb.ma". -include "basic_2/computation/cprs.ma". -include "basic_2/computation/lprs.ma". +include "basic_2/computation/cpxs.ma". +include "basic_2/computation/lpxs.ma". (* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) @@ -62,21 +62,22 @@ lemma fsupp_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2 /3 width=5 by fpb_fsup, tri_step, fpb_fpbs/ qed. -lemma cprs_fpbs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄. -#h #g #G #L #T1 #T2 #H @(cprs_ind … H) -T2 -/3 width=5 by fpb_cpr, fpbs_strap1/ +lemma cpxs_fpbs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄. +#h #g #G #L #T1 #T2 #H @(cpxs_ind … H) -T2 +/3 width=5 by fpb_cpx, fpbs_strap1/ qed. -lemma lprs_fpbs: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1, T⦄ ≥[h, g] ⦃G, L2, T⦄. -#h #g #G #L1 #L2 #T #H @(lprs_ind … H) -L2 -/3 width=5 by fpb_lpr, fpbs_strap1/ +lemma lpxs_fpbs: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L1, T⦄ ≥[h, g] ⦃G, L2, T⦄. +#h #g #G #L1 #L2 #T #H @(lpxs_ind … H) -L2 +/3 width=5 by fpb_lpx, fpbs_strap1/ qed. +lemma cprs_fpbs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄. +/3 width=1 by cprs_cpxs, cpxs_fpbs/ qed. + +lemma lprs_fpbs: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1, T⦄ ≥[h, g] ⦃G, L2, T⦄. +/3 width=1 by lprs_lpxs, lpxs_fpbs/ qed. + lemma cpr_lpr_fpbs: ∀h,g,G,L1,L2,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, T2⦄. -/4 width=5 by fpbs_strap1, fpb_lpr, fpb_cpr/ qed. - -lemma ssta_fpbs: ∀h,g,G,L,T,U,l. - ⦃G, L⦄ ⊢ T ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T •[h, g] U → - ⦃G, L, T⦄ ≥[h, g] ⦃G, L, U⦄. -/3 width=2 by fpb_fpbs, fpb_ssta/ qed. +/4 width=5 by fpbs_strap1, lpr_fpb, cpr_fpb/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma index 1978f2ce6..86cbe3ee3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/computation/fpbs.ma". +include "basic_2/computation/fpbs_lift.ma". (* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma index 809bd3358..19136df6f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma @@ -13,12 +13,18 @@ (**************************************************************************) include "basic_2/unfold/lsstas_lift.ma". +include "basic_2/reduction/fpb_lift.ma". include "basic_2/computation/fpbs.ma". (* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) (* Advanced properties ******************************************************) +lemma ssta_fpbs: ∀h,g,G,L,T,U,l. + ⦃G, L⦄ ⊢ T ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T •[h, g] U → + ⦃G, L, T⦄ ≥[h, g] ⦃G, L, U⦄. +/3 width=2 by fpb_fpbs, ssta_fpb/ qed. + lemma lsstas_fpbs: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 → ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄. #h #g #G #L #T1 #T2 #l2 #H @(lsstas_ind_dx … H) -l2 -T2 // @@ -26,5 +32,5 @@ lemma lsstas_fpbs: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 → elim (le_inv_plus_l … Hl21) -Hl21 #Hl12 #Hl21 lapply (lsstas_da_conf … HT1 … Hl1) -HT1 >(plus_minus_m_m … Hl12) -Hl12 -/3 width=5 by fpb_ssta, fpbs_strap1/ +/3 width=5 by ssta_fpb, fpbs_strap1/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/ygt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ygt.ma deleted file mode 100644 index f6b0f6a5f..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/ygt.ma +++ /dev/null @@ -1,86 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/notation/relations/btpredstarproper_8.ma". -include "basic_2/reduction/ysc.ma". -include "basic_2/computation/fpbs.ma". - -(* "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **********************) - -inductive ygt (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ -| ygt_inj : ∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≻[h, g] ⦃G2, L2, T2⦄ → - ygt h g G1 L1 T1 G2 L2 T2 -| ygt_step: ∀G,L,L2,T. ygt h g G1 L1 T1 G L T → ⦃G, L⦄ ⊢ ➡ L2 → ygt h g G1 L1 T1 G L2 T -. - -interpretation "'big tree' proper parallel computation (closure)" - 'BTPRedStarProper h g G1 L1 T1 G2 L2 T2 = (ygt h g G1 L1 T1 G2 L2 T2). - -(* Basic forvard lemmas *****************************************************) - -lemma ygt_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G2 -L2 -T2 -/3 width=5 by fpbs_strap1, ysc_fpb, fpb_lpr/ -qed-. - -(* Basic properties *********************************************************) - -lemma ysc_ygt: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. -/3 width=5 by ygt_inj, ygt_step/ qed. - -lemma ygt_strap1: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G, L, T⦄ → - ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 -lapply (ygt_fwd_fpbs … H1) #H0 -elim (fpb_inv_ysc … H2) -H2 [| * #HG2 #HL2 #HT2 destruct ] -/2 width=5 by ygt_inj, ygt_step/ -qed-. - -lemma ygt_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ → - ⦃G, L, T⦄ >[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 elim H2 -G2 -L2 -T2 -/3 width=5 by ygt_step, ygt_inj, fpbs_strap2/ -qed-. - -lemma ygt_fpbs_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G, L, T⦄ → - ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #HT1 #HT2 @(fpbs_ind … HT2) -G2 -L2 -T2 -/2 width=5 by ygt_strap1/ -qed-. - -lemma fpbs_ygt_trans: ∀h,g,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → - ∀G2,L2,T2. ⦃G, L, T⦄ >[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G #L1 #L #T1 #T #HT1 @(fpbs_ind … HT1) -G -L -T -/3 width=5 by ygt_strap2/ -qed-. - -lemma fsupp_ygt: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsupp_ind … L2 T2 H) -G2 -L2 -T2 -/3 width=5 by fsupp_fpbs, ysc_fsup, ysc_ygt, ygt_inj/ -qed. - -lemma cprs_ygt: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → - ⦃G, L, T1⦄ >[h, g] ⦃G, L, T2⦄. -#h #g #G #L #T1 #T2 #H @(cprs_ind … H) -T2 -[ #H elim H // -| #T #T2 #_ #HT2 #IHT1 #HT12 - elim (term_eq_dec T1 T) #H destruct - [ -IHT1 /4 width=1/ - | lapply (IHT1 … H) -IHT1 -H -HT12 #HT1 - @(ygt_strap1 … HT1) -HT1 /2 width=1 by fpb_cpr/ - ] -] -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma index e55dd6888..20d72ef3e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/computation/csn_aaa.ma". +include "basic_2/computation/csx_aaa.ma". include "basic_2/computation/cpds_aaa.ma". include "basic_2/equivalence/cpcs_aaa.ma". include "basic_2/dynamic/snv.ma". @@ -37,7 +37,7 @@ lemma snv_fwd_aaa: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ∃A. ⦃G, L⦄ ] qed-. -lemma snv_fwd_csn: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ⦃G, L⦄ ⊢ ⬊*[h, g] T. +lemma snv_fwd_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ⦃G, L⦄ ⊢ ⬊*[h, g] T. #h #g #G #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma index 3679610d9..086cf114b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma @@ -14,7 +14,7 @@ include "basic_2/unfold/lsstas_lsstas.ma". include "basic_2/computation/fpbs_lift.ma". -include "basic_2/computation/ygt.ma". +include "basic_2/computation/fpbg.ma". include "basic_2/equivalence/cpes_cpds.ma". include "basic_2/dynamic/snv.ma". @@ -51,7 +51,7 @@ fact snv_cprs_lpr_aux: ∀h,g,G0,L0,T0. ∀G,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g]. #h #g #G0 #L0 #T0 #IH #G #L1 #T1 #HLT0 #HT1 #T2 #H -@(cprs_ind … H) -T2 /4 width=6 by ygt_fpbs_trans, cprs_fpbs/ +@(cprs_ind … H) -T2 /4 width=6 by fpbg_fpbs_trans, cprs_fpbs/ qed-. fact da_cprs_lpr_aux: ∀h,g,G0,L0,T0. @@ -61,7 +61,7 @@ fact da_cprs_lpr_aux: ∀h,g,G0,L0,T0. ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l → ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] l. #h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #l #Hl #T2 #H -@(cprs_ind … H) -T2 /4 width=10 by snv_cprs_lpr_aux, ygt_fpbs_trans, cprs_fpbs/ +@(cprs_ind … H) -T2 /4 width=10 by snv_cprs_lpr_aux, fpbg_fpbs_trans, cprs_fpbs/ qed-. fact da_cpcs_aux: ∀h,g,G0,L0,T0. @@ -103,7 +103,7 @@ elim (IHT1 L1) // -IHT1 #U #HTU #HU1 elim (IH1 … Hl21 … HTU … HTT2 … HL12) -IH1 -HTU -HTT2 [2: /3 width=12 by da_cprs_lpr_aux/ |3: /3 width=10 by snv_cprs_lpr_aux/ -|4: /3 width=5 by ygt_fpbs_trans, cprs_fpbs/ +|4: /3 width=5 by fpbg_fpbs_trans, cprs_fpbs/ ] -G0 -L0 -T0 -T1 -T -l1 #U2 #HTU2 #HU2 /4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/ qed-. @@ -149,7 +149,7 @@ elim (le_or_ge l2 l) #Hl2 | lapply (lsstas_da_conf … HT1T … Hl1) #Hl1l lapply (lsstas_conf_le … HT1T … HTU1) -HTU1 // #HTU1 elim (lsstas_cprs_lpr_aux … IH3 IH2 IH1 … Hl1l … HTU1 … HTT2 L) - /3 width=8 by ygt_fpbs_trans, lsstas_fpbs, monotonic_le_minus_l/ -T #U2 #HTU2 #HU12 + /3 width=8 by fpbg_fpbs_trans, lsstas_fpbs, monotonic_le_minus_l/ -T #U2 #HTU2 #HU12 /3 width=5 by cpcs_cpes, ex3_2_intro/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma index f65229f06..71c688c21 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma @@ -39,14 +39,14 @@ fact da_cpr_lpr_aux: ∀h,g,G0,L0,T0. lapply (fsupp_lref … G1 … HLK1) elim (lpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2 elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct - /4 width=10 by da_ldef, da_ldec, fsupp_ygt/ + /4 width=10 by da_ldef, da_ldec, fsupp_fpbg/ |2,4: * #K0 #V0 #W0 #H #HVW0 #HW0 lapply (ldrop_mono … H … HLK1) -H #H destruct lapply (fsupp_lref … G1 … HLK1) elim (lpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2 elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #_ #H destruct lapply (ldrop_fwd_ldrop2 … HLK2) -V2 - /4 width=7 by da_lift, fsupp_ygt/ + /4 width=7 by da_lift, fsupp_fpbg/ ] | #p #_ #_ #HT0 #H1 destruct -IH3 -IH2 -IH1 elim (snv_inv_gref … H1) @@ -55,15 +55,15 @@ fact da_cpr_lpr_aux: ∀h,g,G0,L0,T0. lapply (da_inv_bind … H2) -H2 elim (cpr_inv_bind1 … H3) -H3 * [ #V2 #T2 #HV12 #HT12 #H destruct - /4 width=9 by da_bind, fsupp_ygt, lpr_pair/ + /4 width=9 by da_bind, fsupp_fpbg, lpr_pair/ | #T2 #HT12 #HT2 #H1 #H2 destruct - /4 width=11 by da_inv_lift, fsupp_ygt, lpr_pair, ldrop_ldrop/ + /4 width=11 by da_inv_lift, fsupp_fpbg, lpr_pair, ldrop_ldrop/ ] | #V1 #T1 #HG0 #HL0 #HT0 #H1 #l #H2 #X3 #H3 #L2 #HL12 destruct elim (snv_inv_appl … H1) -H1 #b0 #W1 #W0 #T0 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HT10 lapply (da_inv_flat … H2) -H2 #Hl elim (cpr_inv_appl1 … H3) -H3 * - [ #V2 #T2 #HV12 #HT12 #H destruct -IH3 -IH2 /4 width=7 by da_flat, fsupp_ygt/ + [ #V2 #T2 #HV12 #HT12 #H destruct -IH3 -IH2 /4 width=7 by da_flat, fsupp_fpbg/ | #b #V2 #W #W2 #U1 #U2 #HV12 #HW2 #HU12 #H1 #H2 destruct elim (snv_inv_bind … HT1) -HT1 #HW #HU1 lapply (da_inv_bind … Hl) -Hl #Hl @@ -71,24 +71,24 @@ fact da_cpr_lpr_aux: ∀h,g,G0,L0,T0. lapply (cprs_div … HW3 … HW10) -W3 #HWW1 lapply (ssta_da_conf … HVW1 … Hl0) [?,?] ⦃?,?,?⦄ )" "ygt_lift" + "ygt_ygt" * ] - [ "fpbs ( ? ⊢ ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fpbs" * ] + [ "fpbg ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fpbg" * ] + [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fpbs" * ] } ] [ { "decomposed extended computation" * } { @@ -116,7 +116,8 @@ table { class "water" [ { "reduction" * } { [ { "\"big tree\" parallel reduction" * } { - [ "fpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "ysc ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" * ] + [ "fpbc ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpbc_lift" * ] + [ "fpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "fpb_lift" * ] } ] [ { "context-sensitive extended normal forms" * } { -- 2.39.2