From: Ferruccio Guidi Date: Sun, 6 Oct 2013 11:47:25 +0000 (+0000) Subject: - big-tree reduction is now based on extended reduction X-Git-Tag: make_still_working~1100 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=c28e3d93b588796bfbbfd6b2ec9dd86f405b2b00 - big-tree reduction is now based on extended reduction - some renaming --- 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/csn.ma deleted file mode 100644 index 93d49b4fe..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma +++ /dev/null @@ -1,125 +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/sn_5.ma". -include "basic_2/reduction/cnx.ma". - -(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) - -definition csn: ∀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). - -(* Basic eliminators ********************************************************) - -lemma csn_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 - ) → - ∀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/ -qed-. - -(* Basic properties *********************************************************) - -(* Basic_1: was just: sn3_pr2_intro *) -lemma csn_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 → - ∀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 -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. -/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 -[ #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 → - ∀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 -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/ - | -HLW0 * #H destruct /3 width=1/ - ] -|2,3: /3 width=3 by csn_cpx_trans/ -] -qed. - -(* Basic forward lemmas *****************************************************) - -fact csn_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 -@(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-. - -fact csn_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 -@(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-. - -fact csn_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 -@(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-. - -(* Basic_1: removed theorems 14: - sn3_cdelta - sn3_gen_cflat sn3_cflat sn3_cpr3_trans sn3_shift sn3_change - sn3_appl_cast sn3_appl_beta sn3_appl_lref sn3_appl_abbr - sn3_appl_appls sn3_bind sn3_appl_bind sn3_appls_bind -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_aaa.ma deleted file mode 100644 index e8b3ffb88..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_aaa.ma +++ /dev/null @@ -1,25 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/computation/acp_aaa.ma". -include "basic_2/computation/csn_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. -#h #g #G #L #T #A #H -@(acp_aaa … (csn_acp h g) (csn_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/csn_alt.ma deleted file mode 100644 index 5985f9548..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_alt.ma +++ /dev/null @@ -1,104 +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/snalt_5.ma". -include "basic_2/computation/cpxs.ma". -include "basic_2/computation/csn.ma". - -(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) - -(* alternative definition of csn *) -definition csna: ∀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). - -(* Basic eliminators ********************************************************) - -lemma csna_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 - ) → - ∀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/ -qed-. - -(* Basic properties *********************************************************) - -(* Basic_1: was just: sn3_intro *) -lemma csna_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. ( - ∀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 → - ∀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 -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. ( - ∀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 -[ -H #H destruct #H - elim H // -| #T0 #T #HLT1 #HLT2 #IHT #HT10 #HT12 destruct - elim (term_eq_dec T0 T) #HT0 - [ -HLT1 -HLT2 -H /3 width=1/ - | -IHT -HT12 /4 width=3/ - ] -] -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/ -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/ -qed. - -(* Basic_1: was just: sn3_pr3_trans *) -lemma csn_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/ -qed-. - -(* Main eliminators *********************************************************) - -lemma csn_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 -@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/csn_lift.ma deleted file mode 100644 index 6b52e5b00..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma +++ /dev/null @@ -1,101 +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/reduction/cnx_lift.ma". -include "basic_2/computation/acp.ma". -include "basic_2/computation/csn.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 → - ∀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 -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 → - ∀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 -elim (lift_total T d e) #T0 #HT0 -lapply (cpx_lift … HLT2 … HL12 … HT21 … HT0) -HLT2 #HLT10 -@(IHT1 … HLT10) // -L1 -L2 #H destruct ->(lift_inj … HT0 … HT21) in HT2; -T1 /2 width=1/ -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. -#h #g #I #G #L #K #V #i #HLK #HV -@csn_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 // -] -qed. - -lemma csn_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 -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 - @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 - @IHT1 -IHT1 // -HLT02 /2 width=1/ -] -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 → - ⦃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/ -qed-. - -(* Main properties **********************************************************) - -theorem csn_acp: ∀h,g. acp (cpx h g) (eq …) (csn 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=1/ -] -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpx.ma deleted file mode 100644 index 0fbc4c66f..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpx.ma +++ /dev/null @@ -1,147 +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/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". - -(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) - -(* Advanced properties ******************************************************) - -lemma csn_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 -@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 → - ∀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 -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/ -| -IHW -HLW0 -HT * #H destruct /3 width=1/ -] -qed. - -lemma csn_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 -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/ - | -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/ -] -qed. - -fact csn_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 -#X #HT1 #IHT1 #V #W #T1 #H1 destruct -@csn_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 - @IHT1 -IHT1 [4: // | skip |3: #H destruct /2 width=1/ ] -H2 - 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/ -| -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. - -fact csn_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 -elim (cpx_inv_appl1 … HL) -HL * -[ -HV #V0 #Y #HLV10 #HL #H0 destruct - elim (cpx_inv_abbr1 … HL) -HL * - [ #V3 #T3 #HV3 #HLT3 #H0 destruct - elim (lift_total V0 0 1) #V4 #HV04 - elim (term_eq_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V3.ⓐV4.T3)) - [ -IHVT #H0 destruct - elim (eq_false_inv_tpair_sn … H) -H - [ -HLV10 -HV3 -HLT3 -HVT - >(lift_inj … HV12 … HV04) -V4 - #H elim H // - | * #_ #H elim H // - ] - | -H -HVT #H - lapply (cpx_lift … HLV10 (L. ⓓV) … HV12 … HV04) -HLV10 -HV12 /2 width=1/ #HV24 - @(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/ - ] -| -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/ -] -qed-. - -lemma csn_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. - -(* 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 → - (∀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 -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 - @IHV -IHV // -H1T1 -H3T1 /2 width=1/ -HV0 - #T2 #HLT12 #HT12 - @(csn_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 - [ @IHT1 -IHT1 // /2 width=1/ -H1T10 /2 width=3/ -H3T1 - #T2 #HLT02 #HT02 - @H2T1 -H2T1 /2 width=3/ -HLT10 -HLT02 /3 width=3/ - | -IHT1 -H3T1 -H1T10 - @H2T1 -H2T1 /2 width=1/ - ] -] -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_tstc_vector.ma deleted file mode 100644 index 1eee44b51..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_tstc_vector.ma +++ /dev/null @@ -1,131 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/computation/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". - -(* 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⦄ → - ∀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 *) -#V #Vs #IHV #H -elim (csnv_inv_cons … H) -H #HV #HVs -@csn_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. -#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 -#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/ -] -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 → - ⦃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 -#X #H #H0 -elim (cpxs_fwd_beta_vector … H) -H #H -[ -H1T elim H0 -H0 // -| -H0 @(csn_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 → - ∀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/ -| #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 - #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/ - ] -] -qed. - -(* Basic_1: was just: sn3_appls_abbr *) -lemma csn_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/ -#V1s #V2s #V1 #V2 #HV12 #H -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 -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/ -] -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 → - ⦃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 -#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/ -] -qed. - -theorem csn_acr: ∀h,g. acr (cpx h g) (eq …) (csn 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 -] -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_vector.ma deleted file mode 100644 index 73019d053..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_vector.ma +++ /dev/null @@ -1,42 +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/grammar/term_vector.ma". -include "basic_2/computation/csn.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). - -interpretation - "context-sensitive strong normalization (term vector)" - 'SN h g G L Ts = (csnv h g G L Ts). - -(* Basic inversion lemmas ***************************************************) - -lemma csnv_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 → - ⦃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 -elim (IHVs HVs) -IHVs -HVs /3 width=1/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma new file mode 100644 index 000000000..61174c0ff --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma @@ -0,0 +1,125 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/sn_5.ma". +include "basic_2/reduction/cnx.ma". + +(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) + +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 = (csx h g G L T). + +(* Basic eliminators ********************************************************) + +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 + ) → + ∀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/ +qed-. + +(* Basic properties *********************************************************) + +(* Basic_1: was just: sn3_pr2_intro *) +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 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 (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_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 @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 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 @(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 csx_cpx_trans/ + | -HLW0 * #H destruct /3 width=1/ + ] +|2,3: /3 width=3 by csx_cpx_trans/ +] +qed. + +(* Basic forward lemmas *****************************************************) + +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/ +qed-. + +(* Basic_1: was just: sn3_gen_head *) +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 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/ +qed-. + +(* Basic_1: was just: sn3_gen_bind *) +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 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/ +qed-. + +(* Basic_1: was just: sn3_gen_flat *) +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 + sn3_gen_cflat sn3_cflat sn3_cpr3_trans sn3_shift sn3_change + sn3_appl_cast sn3_appl_beta sn3_appl_lref sn3_appl_abbr + sn3_appl_appls sn3_bind sn3_appl_bind sn3_appls_bind +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma new file mode 100644 index 000000000..d951e4154 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.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/acp_aaa.ma". +include "basic_2/computation/csx_tstc_vector.ma". + +(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) + +(* Main properties concerning atomic arity assignment ***********************) + +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 … (csx_acp h g) (csx_acr h g) … H) +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_alt.ma new file mode 100644 index 000000000..7c95fed6e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_alt.ma @@ -0,0 +1,104 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/snalt_5.ma". +include "basic_2/computation/cpxs.ma". +include "basic_2/computation/csx.ma". + +(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) + +(* 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 = (csxa h g G L T). + +(* Basic eliminators ********************************************************) + +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 + ) → + ∀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/ +qed-. + +(* Basic properties *********************************************************) + +(* Basic_1: was just: sn3_intro *) +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 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 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 +@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 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 +@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 + elim (term_eq_dec T0 T) #HT0 + [ -HLT1 -HLT2 -H /3 width=1/ + | -IHT -HT12 /4 width=3/ + ] +] +qed. + +(* Main properties **********************************************************) + +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 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 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 csx_cpx_trans/ +qed-. + +(* Main eliminators *********************************************************) + +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 @(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/csx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma new file mode 100644 index 000000000..c431c349b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma @@ -0,0 +1,101 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cnx_lift.ma". +include "basic_2/computation/acp.ma". +include "basic_2/computation/csx.ma". + +(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) + +(* Relocation properties ****************************************************) + +(* Basic_1: was just: sn3_lift *) +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 +@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 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 +@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 +>(lift_inj … HT0 … HT21) in HT2; -T1 /2 width=1/ +qed. + +(* Advanced properties ******************************************************) + +(* Basic_1: was just: sn3_abbr *) +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 +@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 + @(csx_lift … HLK HV1) -HLK -HV1 + @(csx_cpx_trans … HV) -HV // +] +qed. + +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 @(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 + @(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 + @(csx_cpx_trans … (ⓐV.T2)) /2 width=1/ -HLV0 + @IHT1 -IHT1 // -HLT02 /2 width=1/ +] +qed. + +(* Advanced inversion lemmas ************************************************) + +(* Basic_1: was: sn3_gen_def *) +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 +@(csx_inv_lift … H0LK … HV0) -H0LK +@(csx_cpx_trans … Hi) -Hi /2 width=7/ +qed-. + +(* Main properties **********************************************************) + +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 csx_fwd_flat_dx/ +| /2 width=1/ +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma new file mode 100644 index 000000000..a365b4310 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma @@ -0,0 +1,147 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/tstc_tstc.ma". +include "basic_2/computation/cpxs_cpxs.ma". +include "basic_2/computation/csx_alt.ma". +include "basic_2/computation/csx_lift.ma". + +(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) + +(* Advanced properties ******************************************************) + +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 @(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 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 @(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 (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 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 @(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 + @(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 (csx_cpx_trans … HT … HLT0) -T #HLT0 + lapply (csx_inv_lift … HLT0 … HT0) -T0 /2 width=3/ +] +qed. + +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 @(csx_ind … H) -X +#X #HT1 #IHT1 #V #W #T1 #H1 destruct +@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 + @IHT1 -IHT1 [4: // | skip |3: #H destruct /2 width=1/ ] -H2 + 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 + @(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 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 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 @(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 * + [ #V3 #T3 #HV3 #HLT3 #H0 destruct + elim (lift_total V0 0 1) #V4 #HV04 + elim (term_eq_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V3.ⓐV4.T3)) + [ -IHVT #H0 destruct + elim (eq_false_inv_tpair_sn … H) -H + [ -HLV10 -HV3 -HLT3 -HVT + >(lift_inj … HV12 … HV04) -V4 + #H elim H // + | * #_ #H elim H // + ] + | -H -HVT #H + lapply (cpx_lift … HLV10 (L. ⓓV) … HV12 … HV04) -HLV10 -HV12 /2 width=1/ #HV24 + @(IHVT … H … HV04) -IHVT // -H -HV04 /4 width=1/ + ] + | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct + 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 + @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 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 csx_appl_theta_aux/ qed. + +(* Basic_1: was just: sn3_appl_appl *) +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 @(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 + @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1/ -HLT10 + @IHV -IHV // -H1T1 -H3T1 /2 width=1/ -HV0 + #T2 #HLT12 #HT12 + @(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 + [ @IHT1 -IHT1 // /2 width=1/ -H1T10 /2 width=3/ -H3T1 + #T2 #HLT02 #HT02 + @H2T1 -H2T1 /2 width=3/ -HLT10 -HLT02 /3 width=3/ + | -IHT1 -H3T1 -H1T10 + @H2T1 -H2T1 /2 width=1/ + ] +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma new file mode 100644 index 000000000..f32a267c9 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma @@ -0,0 +1,131 @@ +(**************************************************************************) +(* ___ *) +(* ||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/acp_cr.ma". +include "basic_2/computation/cpxs_tstc_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 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_csx … H2T) ] (**) (* /2 width=1/ does not work *) +#V #Vs #IHV #H +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 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 (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 @(csx_cpxs_trans … (Ⓐ(V@Vs).⋆(next h k))) /2 width=1/ +] +qed. + +(* Basic_1: was just: sn3_appls_beta *) +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 (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 @(csx_cpxs_trans … H1T) -H1T /2 width=1/ +] +qed. + +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 (csx_inv_lift … H … HLK0 HV12) -V2 -HLK0 /2 width=5/ +| #V #Vs #IHV #H1T + 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 @(csx_cpxs_trans … H1T) -H1T /2 width=1/ + ] +] +qed. + +(* Basic_1: was just: sn3_appls_abbr *) +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/ +#V1s #V2s #V1 #V2 #HV12 #H +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 (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 @(csx_cpxs_trans … H) -H /2 width=1/ +] +qed. + +(* Basic_1: was just: sn3_appls_cast *) +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 (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 @(csx_cpxs_trans … H1T) -H1T /2 width=1/ +| -H1T -H0 @(csx_cpxs_trans … H1W) -H1W /2 width=1/ +] +qed. + +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 + @(csx_applv_theta … HV12s) -HV12s + @(csx_abbr) // +| @csx_lift +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_vector.ma new file mode 100644 index 000000000..733666659 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_vector.ma @@ -0,0 +1,42 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/term_vector.ma". +include "basic_2/computation/csx.ma". + +(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERM VECTORS *************) + +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 = (csxv h g G L Ts). + +(* Basic inversion lemmas ***************************************************) + +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 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 (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/fpbg_fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma new file mode 100644 index 000000000..4f092111a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma @@ -0,0 +1,22 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fpbg.ma". + +(* "BIG TREE" ORDER FOR CLOSURES ********************************************) + +(* Main properties **********************************************************) + +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/fpbg_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma new file mode 100644 index 000000000..9afc2523b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma @@ -0,0 +1,39 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unfold/lsstas_lift.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_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 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 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/computation/ygt_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_lift.ma deleted file mode 100644 index 1c75c8e3d..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_lift.ma +++ /dev/null @@ -1,37 +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/unfold/lsstas_lift.ma". -include "basic_2/computation/ygt.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⦄. -#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/ - | #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/ - ] -] -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_ygt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_ygt.ma deleted file mode 100644 index 98fd435a3..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_ygt.ma +++ /dev/null @@ -1,22 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/computation/ygt.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-. 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" * } {