From: Ferruccio Guidi Date: Fri, 4 Oct 2013 15:02:46 +0000 (+0000) Subject: lenv refinement for native validity removed from big tree reduction X-Git-Tag: make_still_working~1103 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=06d5ff2316426acfb16a9cc9784d40ce19351771;p=helm.git lenv refinement for native validity removed from big tree reduction --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/ygt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ygt.ma new file mode 100644 index 000000000..03678e4a8 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/ygt.ma @@ -0,0 +1,86 @@ +(**************************************************************************) +(* ___ *) +(* ||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/yprs.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_yprs: ∀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 yprs_strap1, ysc_ypr, ypr_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_yprs … H1) #H0 +elim (ypr_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, yprs_strap2/ +qed-. + +lemma ygt_yprs_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 @(yprs_ind … HT2) -G2 -L2 -T2 +/2 width=5 by ygt_strap1/ +qed-. + +lemma yprs_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 @(yprs_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_yprs, 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 ypr_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 new file mode 100644 index 000000000..6b713bc91 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_lift.ma @@ -0,0 +1,37 @@ +(**************************************************************************) +(* ___ *) +(* ||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 ypr_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 new file mode 100644 index 000000000..5910f81ca --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_ygt.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/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_yprs, ygt_yprs_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/yprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/yprs.ma new file mode 100644 index 000000000..d3260bc65 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/yprs.ma @@ -0,0 +1,82 @@ +(**************************************************************************) +(* ___ *) +(* ||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/btpredstar_8.ma". +include "basic_2/substitution/fsupp.ma". +include "basic_2/reduction/ypr.ma". +include "basic_2/computation/cprs.ma". +include "basic_2/computation/lprs.ma". + +(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) + +definition yprs: ∀h. sd h → tri_relation genv lenv term ≝ + λh,g. tri_TC … (ypr h g). + +interpretation "'big tree' parallel computation (closure)" + 'BTPRedStar h g G1 L1 T1 G2 L2 T2 = (yprs h g G1 L1 T1 G2 L2 T2). + +(* Basic eliminators ********************************************************) + +lemma yprs_ind: ∀h,g,G1,L1,T1. ∀R:relation3 genv lenv term. R G1 L1 T1 → + (∀L,G2,G,L2,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) → + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2. +/3 width=8 by tri_TC_star_ind/ qed-. + +lemma yprs_ind_dx: ∀h,g,G2,L2,T2. ∀R:relation3 genv lenv term. R G2 L2 T2 → + (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) → + ∀G1,L1,T1. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → R G1 L1 T1. +/3 width=8 by tri_TC_star_ind_dx/ qed-. + +(* Basic properties *********************************************************) + +lemma yprs_refl: ∀h,g. tri_reflexive … (yprs h g). +/2 width=1 by tri_inj/ qed. + +lemma ypr_yprs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. +/2 width=1 by tri_inj/ qed. + +lemma yprs_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⦄. +/2 width=5 by tri_step/ qed-. + +lemma yprs_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⦄. +/2 width=5 by tri_TC_strap/ qed-. + +(* Note: this is a general property of bi_TC *) +lemma fsupp_yprs: ∀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 ypr_fsup, tri_step, ypr_yprs/ +qed. + +lemma cprs_yprs: ∀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 ypr_cpr, yprs_strap1/ +qed. + +lemma lprs_yprs: ∀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 ypr_lpr, yprs_strap1/ +qed. + +lemma cpr_lpr_yprs: ∀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 yprs_strap1, ypr_lpr, ypr_cpr/ qed. + +lemma ssta_yprs: ∀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 ypr_yprs, ypr_ssta/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/yprs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/yprs_lift.ma new file mode 100644 index 000000000..2743f9c68 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/yprs_lift.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||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/yprs.ma". + +(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) + +(* Advanced properties ******************************************************) + +lemma lsstas_yprs: ∀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 // +#l2 #T #T2 #HT1 #HT2 #IHT1 #l1 >commutative_plus #Hl21 #Hl1 +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 ypr_ssta, yprs_strap1/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/yprs_yprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/yprs_yprs.ma new file mode 100644 index 000000000..f28153053 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/yprs_yprs.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||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/yprs.ma". + +(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) + +(* Main properties **********************************************************) + +theorem yprs_trans: ∀h,g. tri_transitive … (yprs h g). +/2 width=5 by tri_TC_transitive/ qed-. + +(* Advanced properties ******************************************************) + +lemma cpr_lpr_ssta_yprs: ∀h,g,G,L1,L2,T1,T2,U2,l2. + ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡ L2 → + ⦃G, L2⦄ ⊢ T2 ▪[h, g] l2+1 → ⦃G, L2⦄ ⊢ T2 •[h, g] U2 → + ⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, U2⦄. +/3 width=5 by yprs_trans, cpr_lpr_yprs, ssta_yprs/ 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 a49ab5419..28aa4a7a0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma @@ -13,9 +13,10 @@ (**************************************************************************) include "basic_2/unfold/lsstas_lsstas.ma". +include "basic_2/computation/yprs_lift.ma". +include "basic_2/computation/ygt.ma". include "basic_2/equivalence/cpes_cpds.ma". -include "basic_2/dynamic/yprs_lift.ma". -include "basic_2/dynamic/ygt.ma". +include "basic_2/dynamic/snv.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma index e35537937..a69b20043 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma @@ -12,10 +12,10 @@ (* *) (**************************************************************************) +include "basic_2/computation/yprs_yprs.ma". include "basic_2/dynamic/snv_lift.ma". include "basic_2/dynamic/snv_cpcs.ma". include "basic_2/dynamic/lsubsv_snv.ma". -include "basic_2/dynamic/yprs_yprs.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma index d19c92bbf..a9dd6ebd2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma @@ -13,10 +13,10 @@ (**************************************************************************) include "basic_2/computation/cpds_cpds.ma". +include "basic_2/computation/yprs_yprs.ma". include "basic_2/dynamic/snv_aaa.ma". include "basic_2/dynamic/snv_cpcs.ma". include "basic_2/dynamic/lsubsv_lsstas.ma". -include "basic_2/dynamic/yprs_yprs.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma deleted file mode 100644 index 43cc6d055..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma +++ /dev/null @@ -1,88 +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/dynamic/ysc.ma". -include "basic_2/dynamic/yprs.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_yprs: ∀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 yprs_strap1, ysc_ypr, ypr_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/ 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_yprs … H1) #H0 -elim (ypr_inv_ysc … H2) -H2 [| * #HG2 #HL2 #HT2 destruct ] /2 width=5/ -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_inj, yprs_strap2/ | /2 width=3/ ] -qed-. - -lemma ygt_yprs_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 @(yprs_ind … HT2) -G2 -L2 -T2 // -/2 width=5 by ygt_strap1/ -qed-. - -lemma yprs_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 @(yprs_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=1/ /3 width=5/ -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/ - ] -] -qed. - -lemma lsubsv_ygt: ∀h,g,G,L1,L2,T. G ⊢ L2 ¡⊑[h, g] L1 → (L1 = L2 → ⊥) → - ⦃G, L1, T⦄ >[h, g] ⦃G, L2, T⦄. -/4 width=1/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt_lift.ma deleted file mode 100644 index 19c15be07..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/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/dynamic/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 ypr_ssta, ygt_strap1/ - ] -] -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt_ygt.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt_ygt.ma deleted file mode 100644 index 443dbcbf0..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/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/dynamic/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_yprs, ygt_yprs_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma deleted file mode 100644 index c08c984f2..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.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/notation/relations/btpred_8.ma". -include "basic_2/relocation/fsup.ma". -include "basic_2/reduction/lpr.ma". -include "basic_2/dynamic/lsubsv.ma". - -(* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************) - -inductive ypr (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ -| ypr_fsup : ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ypr h g G1 L1 T1 G2 L2 T2 -| ypr_lpr : ∀L2. ⦃G1, L1⦄ ⊢ ➡ L2 → ypr h g G1 L1 T1 G1 L2 T1 -| ypr_cpr : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡ T2 → ypr h g G1 L1 T1 G1 L1 T2 -| ypr_ssta : ∀T2,l. ⦃G1, L1⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G1, L1⦄ ⊢ T1 •[h, g] T2 → ypr h g G1 L1 T1 G1 L1 T2 -| ypr_lsubsv: ∀L2. G1 ⊢ L2 ¡⊑[h, g] L1 → ypr h g G1 L1 T1 G1 L2 T1 -. - -interpretation - "'big tree' parallel reduction (closure)" - 'BTPRed h g G1 L1 T1 G2 L2 T2 = (ypr h g G1 L1 T1 G2 L2 T2). - -(* Basic properties *********************************************************) - -lemma ypr_refl: ∀h,g. tri_reflexive … (ypr h g). -/2 width=1/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma deleted file mode 100644 index c94852540..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma +++ /dev/null @@ -1,81 +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/btpredstar_8.ma". -include "basic_2/substitution/fsupp.ma". -include "basic_2/computation/lprs.ma". -include "basic_2/dynamic/ypr.ma". - -(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) - -definition yprs: ∀h. sd h → tri_relation genv lenv term ≝ - λh,g. tri_TC … (ypr h g). - -interpretation "'big tree' parallel computation (closure)" - 'BTPRedStar h g G1 L1 T1 G2 L2 T2 = (yprs h g G1 L1 T1 G2 L2 T2). - -(* Basic eliminators ********************************************************) - -lemma yprs_ind: ∀h,g,G1,L1,T1. ∀R:relation3 genv lenv term. R G1 L1 T1 → - (∀L,G2,G,L2,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) → - ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2. -/3 width=8 by tri_TC_star_ind/ qed-. - -lemma yprs_ind_dx: ∀h,g,G2,L2,T2. ∀R:relation3 genv lenv term. R G2 L2 T2 → - (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) → - ∀G1,L1,T1. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → R G1 L1 T1. -/3 width=8 by tri_TC_star_ind_dx/ qed-. - -(* Basic properties *********************************************************) - -lemma yprs_refl: ∀h,g. tri_reflexive … (yprs h g). -/2 width=1/ qed. - -lemma ypr_yprs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. -/2 width=1/ qed. - -lemma yprs_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⦄. -/2 width=5/ qed-. - -lemma yprs_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⦄. -/2 width=5/ qed-. - -(* Note: this is a general property of bi_TC *) -lemma fsupp_yprs: ∀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=1/ /3 width=5/ -qed. - -lemma cprs_yprs: ∀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 ypr_cpr, yprs_strap1/ -qed. - -lemma lprs_yprs: ∀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 ypr_lpr, yprs_strap1/ -qed. - -lemma lsubsv_yprs: ∀h,g,G,L1,L2,T. G ⊢ L2 ¡⊑[h, g] L1 → ⦃G, L1, T⦄ ≥[h, g] ⦃G, L2, T⦄. -/3 width=1/ qed. - -lemma cpr_lpr_yprs: ∀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 yprs_strap1, ypr_lpr, ypr_cpr/ qed. - -lemma ssta_yprs: ∀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 ypr_yprs, ypr_ssta/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs_lift.ma deleted file mode 100644 index 60bf07b48..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs_lift.ma +++ /dev/null @@ -1,30 +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/dynamic/yprs.ma". - -(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) - -(* Advanced properties ******************************************************) - -lemma lsstas_yprs: ∀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 // -#l2 #T #T2 #HT1 #HT2 #IHT1 #l1 >commutative_plus #Hl21 #Hl1 -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 ypr_ssta, yprs_strap1/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs_yprs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs_yprs.ma deleted file mode 100644 index d2e994216..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs_yprs.ma +++ /dev/null @@ -1,30 +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/dynamic/yprs.ma". - -(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) - -(* Main properties **********************************************************) - -theorem yprs_trans: ∀h,g. tri_transitive … (yprs h g). -/2 width=5/ qed-. - -(* Advanced properties ******************************************************) - -lemma cpr_lpr_ssta_yprs: ∀h,g,G,L1,L2,T1,T2,U2,l2. - ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡ L2 → - ⦃G, L2⦄ ⊢ T2 ▪[h, g] l2+1 → ⦃G, L2⦄ ⊢ T2 •[h, g] U2 → - ⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, U2⦄. -/3 width=5 by yprs_trans, cpr_lpr_yprs, ssta_yprs/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma deleted file mode 100644 index a531dad1c..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma +++ /dev/null @@ -1,47 +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/btpredproper_8.ma". -include "basic_2/dynamic/ypr.ma". - -(* "BIG TREE" PROPER PARALLEL REDUCTION FOR CLOSURES ************************) - -inductive ysc (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ -| ysc_fsup : ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ysc h g G1 L1 T1 G2 L2 T2 -| ysc_cpr : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → ysc h g G1 L1 T1 G1 L1 T2 -| ysc_ssta : ∀T2,l. ⦃G1, L1⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G1, L1⦄ ⊢ T1 •[h, g] T2 → ysc h g G1 L1 T1 G1 L1 T2 -| ysc_lsubsv: ∀L2. G1 ⊢ L2 ¡⊑[h, g] L1 → (L1 = L2 → ⊥) → ysc h g G1 L1 T1 G1 L2 T1 -. - -interpretation - "'big tree' proper parallel reduction (closure)" - 'BTPRedProper h g G1 L1 T1 G2 L2 T2 = (ysc h g G1 L1 T1 G2 L2 T2). - -(* Basic properties *********************************************************) - -lemma ysc_ypr: ∀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 * -G2 -L2 -T2 /2 width=1/ /2 width=2/ -qed. - -(* Inversion lemmas on "big tree" parallel reduction for closures ***********) - -lemma ypr_inv_ysc: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ ∨ - ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡ L2 & T1 = T2. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /3 width=1/ /3 width=2/ -[ #T2 #HT12 elim (term_eq_dec T1 T2) #H destruct /3 width=1/ /4 width=1/ -| #L2 #HL21 elim (lenv_eq_dec L1 L2) #H destruct /3 width=1/ /4 width=1/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/ypr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/ypr.ma new file mode 100644 index 000000000..308f30095 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/ypr.ma @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||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/btpred_8.ma". +include "basic_2/relocation/fsup.ma". +include "basic_2/static/ssta.ma". +include "basic_2/reduction/lpr.ma". + +(* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************) + +inductive ypr (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ +| ypr_fsup : ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ypr h g G1 L1 T1 G2 L2 T2 +| ypr_lpr : ∀L2. ⦃G1, L1⦄ ⊢ ➡ L2 → ypr h g G1 L1 T1 G1 L2 T1 +| ypr_cpr : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡ T2 → ypr h g G1 L1 T1 G1 L1 T2 +| ypr_ssta : ∀T2,l. ⦃G1, L1⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G1, L1⦄ ⊢ T1 •[h, g] T2 → ypr h g G1 L1 T1 G1 L1 T2 +. + +interpretation + "'big tree' parallel reduction (closure)" + 'BTPRed h g G1 L1 T1 G2 L2 T2 = (ypr h g G1 L1 T1 G2 L2 T2). + +(* Basic properties *********************************************************) + +lemma ypr_refl: ∀h,g. tri_reflexive … (ypr h g). +/2 width=1 by ypr_cpr/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/ysc.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/ysc.ma new file mode 100644 index 000000000..290157d30 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/ysc.ma @@ -0,0 +1,47 @@ +(**************************************************************************) +(* ___ *) +(* ||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/btpredproper_8.ma". +include "basic_2/reduction/ypr.ma". + +(* "BIG TREE" PROPER PARALLEL REDUCTION FOR CLOSURES ************************) + +inductive ysc (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ +| ysc_fsup : ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ysc h g G1 L1 T1 G2 L2 T2 +| ysc_cpr : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → ysc h g G1 L1 T1 G1 L1 T2 +| ysc_ssta : ∀T2,l. ⦃G1, L1⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G1, L1⦄ ⊢ T1 •[h, g] T2 → ysc h g G1 L1 T1 G1 L1 T2 +. + +interpretation + "'big tree' proper parallel reduction (closure)" + 'BTPRedProper h g G1 L1 T1 G2 L2 T2 = (ysc h g G1 L1 T1 G2 L2 T2). + +(* Basic properties *********************************************************) + +lemma ysc_ypr: ∀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 * -G2 -L2 -T2 +/2 width=2 by ypr_fsup, ypr_cpr, ypr_ssta/ +qed. + +(* Inversion lemmas on "big tree" parallel reduction for closures ***********) + +lemma ypr_inv_ysc: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ ∨ + ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡ L2 & T1 = T2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 +/3 width=2 by and3_intro, or_introl, or_intror, ysc_fsup, ysc_ssta/ +#T2 #HT12 elim (term_eq_dec T1 T2) #H destruct +/4 width=1 by and3_intro, or_introl, or_intror, ysc_cpr/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 3b79088f2..571d2e6de 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -39,15 +39,6 @@ table { } ] *) - [ { "\"big tree\" parallel computation" * } { - [ "ygt ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "ygt_lift" + "ygt_ygt" * ] - [ "yprs ( ? ⊢ ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "yprs_lift" + "yprs_yprs" * ] - } - ] - [ { "\"big tree\" parallel reduction" * } { - [ "ypr ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "ysc ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" * ] - } - ] [ { "local env. ref. for stratified native validity" * } { [ "lsubsv ( ? ⊢ ? ¡⊑[?,?] ? )" "lsubsv_ldrop" + "lsubsv_lsubd" + "lsubsv_lsuba" + "lsubsv_lsstas" + "lsubsv_cpds" + "lsubsv_cpcs" + "lsubsv_snv" * ] } @@ -93,6 +84,11 @@ table { [ "csn ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csn_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csn_lift" + "csn_lpx" * ] } ] + [ { "\"big tree\" parallel computation" * } { + [ "ygt ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "ygt_lift" + "ygt_ygt" * ] + [ "yprs ( ? ⊢ ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "yprs_lift" + "yprs_yprs" * ] + } + ] [ { "decomposed extended computation" * } { [ "cpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?] ? )" "cpds_lift" + "cpds_aaa" + "cpds_cpds" * ] } @@ -119,6 +115,10 @@ table { ] class "water" [ { "reduction" * } { + [ { "\"big tree\" parallel reduction" * } { + [ "ypr ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "ysc ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" * ] + } + ] [ { "context-sensitive extended normal forms" * } { [ "cnx ( ⦃?,?⦄ ⊢ 𝐍[?,?]⦃?⦄ )" "cnx_lift" + "cnx_crx" + "cnx_cix" * ] }