From 7df0a06017b477e10505167e146e9afdc1ce622a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 14 Dec 2013 22:21:10 +0000 Subject: [PATCH] commit is now complete :) --- .../lambdadelta/basic_2/computation/fpbc.ma | 33 ++++++++++++++++++ .../basic_2/computation/fpbc_fpns.ma | 34 +++++++++++++++++++ 2 files changed, 67 insertions(+) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpns.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma new file mode 100644 index 000000000..3fc670868 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma @@ -0,0 +1,33 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/lazybtpredproper_8.ma". +include "basic_2/computation/fpns.ma". +include "basic_2/computation/fpbu.ma". + +(* SINGLE-STEP "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **********) + +definition fpbc: ∀h. sd h → tri_relation genv lenv term ≝ + λh,g,G1,L1,T1,G2,L2,T2. + ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, T2⦄ . + +interpretation + "single-step 'big tree' proper parallel reduction (closure)" + 'LazyBTPRedProper h g G1 L1 T1 G2 L2 T2 = (fpbc h g G1 L1 T1 G2 L2 T2). + +(* Baic properties **********************************************************) + +lemma fpbu_fpbc: ∀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=5 by ex2_3_intro/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpns.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpns.ma new file mode 100644 index 000000000..dd15570ef --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpns.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fpns_fpns.ma". +include "basic_2/computation/fpbu_fpns.ma". +include "basic_2/computation/fpbc.ma". + +(* SINGLE-STEP "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **********) + +(* Properties on parallel computation for "big tree" normal forms ***********) + +lemma fpbc_fpns_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 * +/3 width=9 by fpns_trans, ex2_3_intro/ +qed-. + +lemma fpns_fpbc_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 #H1 * +#G0 #L0 #T0 #H0 #H02 elim (fpns_fpbu_trans … H1 … H0) -G -L -T +/3 width=9 by fpns_trans, ex2_3_intro/ +qed-. -- 2.39.2