From: Ferruccio Guidi Date: Thu, 2 Oct 2014 15:36:10 +0000 (+0000) Subject: - fpbg can be reflexive (example given) X-Git-Tag: make_still_working~831 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=106b25f0206beedc4e416d223accb1308ca7161b;p=helm.git - fpbg can be reflexive (example given) - so fpbu may use short steps rather than long steps - some refactoring --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma deleted file mode 100644 index f8797e72d..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma +++ /dev/null @@ -1,33 +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/lazybtpredproper_8.ma". -include "basic_2/multiple/fleq.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⦄ ≡[0] ⦃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_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fleq.ma deleted file mode 100644 index af496b60f..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fleq.ma +++ /dev/null @@ -1,34 +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/multiple/fleq_fleq.ma". -include "basic_2/computation/fpbu_fleq.ma". -include "basic_2/computation/fpbc.ma". - -(* SINGLE-STEP "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **********) - -(* Properties on lazy equivalence on closures *******************************) - -lemma fpbc_fleq_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≻≡[h, g] ⦃G, L, T⦄ → - ⦃G, L, T⦄ ≡[0] ⦃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 fleq_trans, ex2_3_intro/ -qed-. - -lemma fleq_fpbc_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≡[0] ⦃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 (fleq_fpbu_trans … H1 … H0) -G -L -T -/3 width=9 by fleq_trans, ex2_3_intro/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpbs.ma deleted file mode 100644 index 2c45646ed..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpbs.ma +++ /dev/null @@ -1,27 +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/fpbs_fleq.ma". -include "basic_2/computation/fpbs_fpbs.ma". -include "basic_2/computation/fpbc.ma". - -(* SINGLE-STEP "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **********) - -(* Forward lemmas on "big tree" parallel computation for closures ***********) - -lemma fpbc_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 * -/3 width=5 by fpbu_fwd_fpbs, fpbs_trans, fleq_fpbs/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma index 5d7ce1cb3..574c35e10 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma @@ -13,14 +13,14 @@ (**************************************************************************) include "basic_2/notation/relations/lazybtpredstarproper_8.ma". -include "basic_2/computation/fpbc.ma". +include "basic_2/reduction/fpbc.ma". -(* GENEARAL "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES *************) +(* "QRST" PROPER PARALLEL COMPUTATION FOR CLOSURES **************************) definition fpbg: ∀h. sd h → tri_relation genv lenv term ≝ λh,g. tri_TC … (fpbc h g). -interpretation "general 'big tree' proper parallel computation (closure)" +interpretation "'qrst' proper parallel computation (closure)" 'LazyBTPRedStarProper h g G1 L1 T1 G2 L2 T2 = (fpbg h g G1 L1 T1 G2 L2 T2). (* Basic properties *********************************************************) @@ -39,9 +39,8 @@ lemma fpbg_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄. /2 width=5 by tri_TC_strap/ qed. -(* Note: this is used in the closure proof *) -lemma fqup_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄. -/4 width=1 by fpbc_fpbg, fpbu_fpbc, fpbu_fqup/ qed. +lemma fpbu_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=1 by fpbu_fpbc, fpbc_fpbg/ qed. (* Basic eliminators ********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fleq.ma index 293e666d5..754811ec2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fleq.ma @@ -12,10 +12,10 @@ (* *) (**************************************************************************) -include "basic_2/computation/fpbc_fleq.ma". +include "basic_2/reduction/fpbc_fleq.ma". include "basic_2/computation/fpbg.ma". -(* GENEARAL "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES *************) +(* "QRST" PROPER PARALLEL COMPUTATION FOR CLOSURES **************************) (* Properties on lazy equivalence for closures ******************************) @@ -34,45 +34,3 @@ lemma fleq_fpbg_trans: ∀h,g,G,G2,L,L2,T,T2. ⦃G, L, T⦄ >≡[h, g] ⦃G2, L2 | /4 width=9 by fpbg_strap2, fleq_fpbc_trans/ ] qed-. - -lemma fpbs_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ≡[0] ⦃G2, L2, T2⦄ ∨ - ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2 -[ /2 width=1 by or_introl/ -| #G #G2 #L #L2 #T #T2 #_ #H2 * #H1 elim (fpb_fpbu … H2) -H2 #H2 - [ /3 width=5 by fleq_trans, or_introl/ - | /5 width=5 by fpbc_fpbg, fleq_fpbc_trans, fpbu_fpbc, or_intror/ - | /3 width=5 by fpbg_fleq_trans, or_intror/ - | /4 width=5 by fpbg_strap1, fpbu_fpbc, or_intror/ - ] -] -qed-. - -(* Advanced properties ******************************************************) - -lemma fpbg_fpb_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 #H2 elim (fpb_fpbu … H2) -H2 -/3 width=5 by fpbg_fleq_trans, fpbg_strap1, fpbu_fpbc/ -qed-. - - -lemma fpb_fpbg_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 elim (fpb_fpbu … H1) -H1 -/3 width=5 by fleq_fpbg_trans, fpbg_strap2, fpbu_fpbc/ -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 #H @(fpbs_ind … H) -G -L -T /3 width=5 by fpb_fpbg_trans/ -qed-. - -(* Note: this is used in the closure proof *) -lemma fpbg_fpbs_trans: ∀h,g,G,G2,L,L2,T,T2. ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → - ∀G1,L1,T1. ⦃G1, L1, T1⦄ >≡[h, g] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄. -#h #g #G #G2 #L #L2 #T #T2 #H @(fpbs_ind_dx … H) -G -L -T /3 width=5 by fpbg_fpb_trans/ -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 index 1f52880ad..57dd5ebb4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma @@ -12,10 +12,12 @@ (* *) (**************************************************************************) -include "basic_2/computation/fpbc_fpbs.ma". -include "basic_2/computation/fpbg_fleq.ma". +include "basic_2/computation/fpbs_fpbu.ma". +include "basic_2/computation/fpbs_fpbc.ma". +include "basic_2/computation/fpbs_fpbs.ma". +include "basic_2/computation/fpbg_fpbs.ma". -(* GENERAL "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************) +(* "QRST" PROPER PARALLEL COMPUTATION FOR CLOSURES **************************) (* Advanced inversion lemmas ************************************************) @@ -25,7 +27,7 @@ lemma fpbg_inv_fpbu_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >≡[h, g] [ #G1 #L1 #T1 * /3 width=5 by fleq_fpbs, ex2_3_intro/ | #G1 #G #L1 #L #T1 #T * #G0 #L0 #T0 #H10 #H0 #_ * - /5 width=9 by fpbu_fwd_fpbs, fpbs_trans, fleq_fpbs, ex2_3_intro/ + /5 width=9 by fpbu_fpbs, fpbs_trans, fleq_fpbs, ex2_3_intro/ ] qed-. @@ -35,7 +37,7 @@ lemma fpbg_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2 ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbg_ind … H) -G2 -L2 -T2 [2: #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 @(fpbs_trans … IH1) -IH1 ] (**) (* full auto fails *) -/2 width=1 by fpbc_fwd_fpbs/ +/2 width=1 by fpbc_fpbs/ qed-. (* Advanced properties ******************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma index 454eaa167..58ecd1200 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma @@ -12,17 +12,13 @@ (* *) (**************************************************************************) -include "basic_2/computation/fpbu_lift.ma". +include "basic_2/reduction/fpbu_lift.ma". include "basic_2/computation/fpbg.ma". -(* GENERAL "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *********************) +(* "QRST" PARALLEL COMPUTATION FOR CLOSURES *********************************) (* Advanced properties ******************************************************) -lemma lstas_fpbg: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, l2] T2 → (T1 = T2 → ⊥) → - ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ >≡[h, g] ⦃G, L, T2⦄. -/5 width=5 by fpbc_fpbg, fpbu_fpbc, lstas_fpbu/ qed. - lemma sta_fpbg: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T1 •*[h, 1] T2 → ⦃G, L, T1⦄ >≡[h, g] ⦃G, L, T2⦄. -/4 width=2 by fpbc_fpbg, fpbu_fpbc, sta_fpbu/ qed. +/4 width=2 by fpbu_fpbg, sta_fpbu/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma index 2daaa8145..0c1568207 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma @@ -18,12 +18,12 @@ include "basic_2/reduction/fpb.ma". include "basic_2/computation/cpxs.ma". include "basic_2/computation/lpxs.ma". -(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) +(* "QRST" PARALLEL COMPUTATION FOR CLOSURES *********************************) definition fpbs: ∀h. sd h → tri_relation genv lenv term ≝ λh,g. tri_TC … (fpb h g). -interpretation "'big tree' parallel computation (closure)" +interpretation "'qrst' parallel computation (closure)" 'BTPRedStar h g G1 L1 T1 G2 L2 T2 = (fpbs h g G1 L1 T1 G2 L2 T2). (* Basic eliminators ********************************************************) @@ -150,6 +150,10 @@ lemma cpxs_fqus_lpxs_fpbs: ∀h,g,G1,G2,L1,L,L2,T1,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡ ⦃G1, L1, T⦄ ⊐* ⦃G2, L, T2⦄ → ⦃G2, L⦄ ⊢ ➡*[h, g] L2 → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. /3 width=5 by cpxs_fqus_fpbs, fpbs_lpxs_trans/ qed. +lemma lpxs_lleq_fpbs: ∀h,g,G,L1,L,L2,T. ⦃G, L1⦄ ⊢ ➡*[h, g] L → + L ≡[T, 0] L2 → ⦃G, L1, T⦄ ≥[h, g] ⦃G, L2, T⦄. +/3 width=3 by lpxs_fpbs_trans, lleq_fpbs/ qed. + (* Note: this is used in the closure proof *) 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⦄. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_aaa.ma index ad075940e..dbefe3bce 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_aaa.ma @@ -15,7 +15,7 @@ include "basic_2/reduction/fpb_aaa.ma". include "basic_2/computation/fpbs.ma". -(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) +(* "QRST" PARALLEL COMPUTATION FOR CLOSURES *********************************) (* Properties on atomic arity assignment for terms **************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma index 254708616..10153c2d1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma @@ -14,12 +14,11 @@ include "basic_2/notation/relations/btpredstaralt_8.ma". include "basic_2/multiple/lleq_fqus.ma". -include "basic_2/multiple/lleq_lleq.ma". include "basic_2/computation/cpxs_lleq.ma". include "basic_2/computation/lpxs_lleq.ma". include "basic_2/computation/fpbs.ma". -(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) +(* "QREST" PARALLEL COMPUTATION FOR CLOSURES ********************************) (* Note: alternative definition of fpbs *) definition fpbsa: ∀h. sd h → tri_relation genv lenv term ≝ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_ext.ma deleted file mode 100644 index 8aedee009..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_ext.ma +++ /dev/null @@ -1,31 +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/fpbs_alt.ma". - -(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) - -(* Properties on extended context-sensitive parallel computation for terms **) - -lemma fpbs_cpxs_trans_neq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → (T2 = U2 → ⊥) → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ≥[h, g] ⦃G2, L2, U2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 #HnTU2 elim (fpbs_inv_alt … H) -H -#L00 #L0 #T0 #HT10 #H10 #HL00 #HL02 lapply (lleq_cpxs_trans … HTU2 … HL02) -HTU2 -#HTU2 lapply (cpxs_lleq_conf_sn … HTU2 … HL02) -HL02 -#HL02 lapply (lpxs_cpxs_trans … HTU2 … HL00) -HTU2 -#HTU2 elim (fqus_cpxs_trans_neq … H10 … HTU2 HnTU2) -H10 -HTU2 -HnTU2 -#U0 #HTU0 #HnTU0 #HU02 elim (eq_term_dec T1 T0) [ -HT10 | -HnTU0 ] -[ #H destruct ] /3 width=10 by fpbs_intro_alt, ex3_intro/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma index 8987fcb57..4761d6097 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma @@ -15,7 +15,7 @@ include "basic_2/multiple/fleq.ma". include "basic_2/computation/fpbs.ma". -(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) +(* "QRST" PARALLEL COMPUTATION FOR CLOSURES *********************************) (* Properties on lazy equivalence on closures *******************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbc.ma new file mode 100644 index 000000000..a88d51925 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbc.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fpbc.ma". +include "basic_2/computation/fpbs_fleq.ma". + +(* "QRST" PARALLEL COMPUTATION FOR CLOSURES *********************************) + +(* Properties on "qrst" proper parallel reduction for closures **************) + +lemma fpbc_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 * +/3 width=5 by fpbu_fwd_fpb, fpbs_strap2, fleq_fpbs/ +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 620bbe4f7..68b07b4d3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma @@ -14,7 +14,7 @@ include "basic_2/computation/fpbs.ma". -(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) +(* "QRST" PARALLEL COMPUTATION FOR CLOSURES *********************************) (* Main properties **********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbu.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbu.ma new file mode 100644 index 000000000..d2e880699 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbu.ma @@ -0,0 +1,68 @@ +(**************************************************************************) +(* ___ *) +(* ||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/multiple/fleq.ma". +include "basic_2/reduction/fpbu.ma". +include "basic_2/computation/fpbs_alt.ma". + +(* "QRST" PARALLEL COMPUTATION FOR CLOSURES *********************************) + +(* Properties on extended context-sensitive parallel computation for terms **) + +lemma fpbs_cpx_trans_neq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 → (T2 = U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ≥[h, g] ⦃G2, L2, U2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 #HnTU2 elim (fpbs_inv_alt … H) -H +#L00 #L0 #T0 #HT10 #H10 #HL00 #HL02 lapply (lleq_cpx_trans … HTU2 … HL02) -HTU2 +#HTU2 lapply (cpx_lleq_conf_sn … HTU2 … HL02) -HL02 +#HL02 lapply (lpxs_cpx_trans … HTU2 … HL00) -HTU2 +#HTU2 elim (fqus_cpxs_trans_neq … H10 … HTU2 HnTU2) -H10 -HTU2 -HnTU2 +#U0 #HTU0 #HnTU0 #HU02 elim (eq_term_dec T1 T0) #HnT10 destruct +[ -HT10 elim (cpxs_neq_inv_step_sn … HTU0 HnTU0) -HTU0 -HnTU0 +| -HnTU0 elim (cpxs_neq_inv_step_sn … HT10 HnT10) -HT10 -HnT10 +] +/4 width=10 by fpbs_intro_alt, cpxs_trans, ex3_intro/ +qed-. + +(* Properties on "rst" proper parallel reduction on closures ****************) + +lemma fpbu_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⦄. +/3 width=1 by fpb_fpbs, fpbu_fwd_fpb/ qed. + +lemma fpbs_fpbu_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ≡[0] ⦃G2, L2, T2⦄ ∨ + ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄. +(* ALTERNATIVE PROOF +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind_dx … H) -G1 -L1 -T1 +[ /2 width=1 by or_introl/ +| #G1 #G #L1 #L #T1 #T #H1 #_ * [ #H2 | * #G0 #L0 #T0 #H0 #H02 ] + elim (fpb_fpbu … H1) -H1 #H1 + [ /3 width=1 by +*) +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim(fpbs_inv_alt … H) -H +#L0 #L #T #HT1 #HT2 #HL0 #HL2 elim (eq_term_dec T1 T) #H destruct +[ -HT1 elim (fqus_inv_gen … HT2) -HT2 + [ #H elim (fqup_inv_step_sn … H) -H + /4 width=11 by fpbs_intro_alt, fpbu_fqu, ex2_3_intro, or_intror/ + | * #HG #HL #HT destruct elim (lleq_dec T2 L0 L 0) #H + [ /4 width=3 by fleq_intro, lleq_trans, or_introl/ + | elim (lpxs_nlleq_inv_step_sn … HL0 H) -HL0 -H + /5 width=7 by lpxs_lleq_fpbs, fpbu_lpx, lleq_trans, ex2_3_intro, or_intror/ + ] + ] +| elim (cpxs_neq_inv_step_sn … HT1 H) -HT1 -H + /5 width=11 by fpbs_intro_alt, fpbu_cpx, ex2_3_intro, or_intror/ +] +qed-. 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 15baaa136..4ea86975a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma @@ -16,7 +16,7 @@ include "basic_2/reduction/fpb_lift.ma". include "basic_2/computation/cpxs_lift.ma". include "basic_2/computation/fpbs.ma". -(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) +(* "QRST" PARALLEL COMPUTATION FOR CLOSURES *********************************) (* Advanced properties ******************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma deleted file mode 100644 index 1525567aa..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma +++ /dev/null @@ -1,46 +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/computation/fpbs.ma". - -(* UNITARY "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************) - -inductive fpbu (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ -| fpbu_fqup: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → fpbu h g G1 L1 T1 G2 L2 T2 -| fpbu_cpxs: ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → fpbu h g G1 L1 T1 G1 L1 T2 -| fpbu_lpxs: ∀L2. ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ≡[T1, 0] L2 → ⊥) → fpbu h g G1 L1 T1 G1 L2 T1 -. - -interpretation - "unitary 'big tree' proper parallel reduction (closure)" - 'BTPRedProper h g G1 L1 T1 G2 L2 T2 = (fpbu h g G1 L1 T1 G2 L2 T2). - -(* Basic properties *********************************************************) - -lemma cprs_fpbu: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → - ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄. -/3 width=1 by fpbu_cpxs, cprs_cpxs/ qed. - -lemma lprs_fpbu: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡* L2 → (L1 ≡[T, 0] L2 → ⊥) → - ⦃G, L1, T⦄ ≻[h, g] ⦃G, L2, T⦄. -/3 width=1 by fpbu_lpxs, lprs_lpxs/ qed. - -(* Basic forward lemmas *****************************************************) - -lemma fpbu_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 * -G2 -L2 -T2 -/3 width=1 by lpxs_fpbs, cpxs_fpbs, fqup_fpbs/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fleq.ma deleted file mode 100644 index 8cf744d4a..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fleq.ma +++ /dev/null @@ -1,69 +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/multiple/fleq.ma". -include "basic_2/computation/fpbs_alt.ma". -include "basic_2/computation/fpbu_lleq.ma". - -(* UNITARY "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************) - -(* Properties on lazy equivalence for closures ******************************) - -lemma fleq_fpbu_trans: ∀h,g,F1,F2,K1,K2,T1,T2. ⦃F1, K1, T1⦄ ≡[0] ⦃F2, K2, T2⦄ → - ∀G2,L2,U2. ⦃F2, K2, T2⦄ ≻[h, g] ⦃G2, L2, U2⦄ → - ∃∃G1,L1,U1. ⦃F1, K1, T1⦄ ≻[h, g] ⦃G1, L1, U1⦄ & ⦃G1, L1, U1⦄ ≡[0] ⦃G2, L2, U2⦄. -#h #g #F1 #F2 #K1 #K2 #T1 #T2 * -F2 -K2 -T2 -#K2 #HK12 #G2 #L2 #U2 #H12 elim (lleq_fpbu_trans … HK12 … H12) -K2 -/3 width=5 by fleq_intro, ex2_3_intro/ -qed-. - -lemma fpb_fpbu: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ≡[0] ⦃G2, L2, T2⦄ ∨ - ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 -[ #G2 #L2 #T2 #H elim (fquq_inv_gen … H) -H - [ /4 width=1 by fpbu_fqup, fqu_fqup, or_intror/ - | * #H1 #H2 #H3 destruct /2 width=1 by or_introl/ - ] -| #T2 #HT12 elim (eq_term_dec T1 T2) - #HnT12 destruct /4 width=1 by fpbu_cpxs, cpx_cpxs, or_intror, or_introl/ -| #L2 #HL12 elim (lleq_dec … T1 L1 L2 0) - /4 width=3 by fpbu_lpxs, fleq_intro, lpx_lpxs, or_intror, or_introl/ -| /3 width=1 by fleq_intro, or_introl/ -] -qed-. - -lemma fpbs_fpbu_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ≡[0] ⦃G2, L2, T2⦄ ∨ - ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄. -(* ALTERNATIVE PROOF -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind_dx … H) -G1 -L1 -T1 -[ /2 width=1 by or_introl/ -| #G1 #G #L1 #L #T1 #T #H1 #_ * [ #H2 | * #G0 #L0 #T0 #H0 #H02 ] - elim (fpb_fpbu … H1) -H1 #H1 - [ /3 width=1 by -*) -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim(fpbs_inv_alt … H) -H -#L0 #L #T #HT1 #HT2 #HL0 #HL2 elim (eq_term_dec T1 T) #H destruct -[ -HT1 elim (fqus_inv_gen … HT2) -HT2 - [ /4 width=11 by fpbs_intro_alt, fpbu_fqup, ex2_3_intro, or_intror/ - | * #HG #HL #HT destruct elim (lleq_dec T2 L0 L 0) #H - [ /4 width=3 by fleq_intro, lleq_trans, or_introl/ - | /5 width=5 by fpbu_lpxs, lleq_fpbs, ex2_3_intro, or_intror/ - ] - ] -| elim (cpxs_neq_inv_step_sn … HT1 H) -HT1 -H - /5 width=11 by fpbs_intro_alt, fpbu_cpxs, cpx_cpxs, ex2_3_intro, or_intror/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lift.ma deleted file mode 100644 index 5d3c40f92..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lift.ma +++ /dev/null @@ -1,32 +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/lstas_da.ma". -include "basic_2/computation/cpxs_lift.ma". -include "basic_2/computation/fpbu.ma". - -(* UNITARY "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************) - -(* Advanced properties ******************************************************) - -lemma lstas_fpbu: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, l2] T2 → (T1 = T2 → ⊥) → - ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄. -/4 width=5 by fpbu_cpxs, lstas_cpxs/ qed. - -lemma sta_fpbu: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → - ⦃G, L⦄ ⊢ T1 •*[h, 1] T2 → ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄. -#h #g #G #L #T1 #T2 #l #HT1 #HT12 elim (eq_term_dec T1 T2) -/3 width=5 by lstas_fpbu/ #H destruct -elim (lstas_inv_refl_pos h G L T2 0) // -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lleq.ma deleted file mode 100644 index 6a9cf9d45..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lleq.ma +++ /dev/null @@ -1,35 +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/multiple/lleq_fqus.ma". -include "basic_2/multiple/lleq_lleq.ma". -include "basic_2/computation/cpxs_lleq.ma". -include "basic_2/computation/lpxs_lleq.ma". -include "basic_2/computation/fpbu.ma". - -(* UNITARY "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************) - -(* Properties on lazy equivalence for local environments ********************) - -lemma lleq_fpbu_trans: ∀h,g,F,K1,K2,T. K1 ≡[T, 0] K2 → - ∀G,L2,U. ⦃F, K2, T⦄ ≻[h, g] ⦃G, L2, U⦄ → - ∃∃L1. ⦃F, K1, T⦄ ≻[h, g] ⦃G, L1, U⦄ & L1 ≡[U, 0] L2. -#h #g #F #K1 #K2 #T #HT #G #L2 #U * -G -L2 -U -[ #G #L2 #U #H2 elim (lleq_fqup_trans … H2 … HT) -K2 - /3 width=3 by fpbu_fqup, ex2_intro/ -| /4 width=10 by fpbu_cpxs, cpxs_lleq_conf_sn, lleq_cpxs_trans, ex2_intro/ -| #L2 #HKL2 #HnKL2 elim (lleq_lpxs_trans … HKL2 … HT) -HKL2 - /6 width=3 by fpbu_lpxs, lleq_canc_sn, ex2_intro/ (* 2 lleq_canc_sn *) -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma index 6aef8f2bd..95548ecf4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma @@ -13,10 +13,10 @@ (**************************************************************************) include "basic_2/notation/relations/btsn_5.ma". -include "basic_2/computation/fpbu.ma". -include "basic_2/computation/csx_alt.ma". +include "basic_2/reduction/fpbu.ma". +include "basic_2/computation/csx.ma". -(* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************) +(* "QRST" STRONGLY NORMALIZING TERMS ****************************************) inductive fsb (h) (g): relation3 genv lenv term ≝ | fsb_intro: ∀G1,L1,T1. ( @@ -25,7 +25,7 @@ inductive fsb (h) (g): relation3 genv lenv term ≝ . interpretation - "'big tree' strong normalization (closure)" + "'qrst' strong normalization (closure)" 'BTSN h g G L T = (fsb h g G L T). (* Basic eliminators ********************************************************) @@ -43,5 +43,5 @@ qed-. (* Basic inversion lemmas ***************************************************) lemma fsb_inv_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⦥[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] T. -#h #g #G #L #T #H elim H -G -L -T /5 width=1 by csx_intro_cpxs, fpbu_cpxs/ +#h #g #G #L #T #H elim H -G -L -T /5 width=1 by csx_intro, fpbu_cpx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma index 271839873..2040a3b35 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma @@ -16,15 +16,15 @@ include "basic_2/computation/fpbs_aaa.ma". include "basic_2/computation/csx_aaa.ma". include "basic_2/computation/fsb_csx.ma". -(* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************) +(* "QRST" STRONGLY NORMALIZING TERMS ****************************************) (* Main properties **********************************************************) -(* Note: this is the "big tree" theorem ("small step" version) *) +(* Note: this is the "big tree" theorem ("RST" version) *) theorem aaa_fsb: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⦥[h, g] T. /3 width=2 by aaa_csx, csx_fsb/ qed. -(* Note: this is the "big tree" theorem ("big step" version) *) +(* Note: this is the "big tree" theorem ("QRST" version) *) theorem aaa_fsba: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⦥⦥[h, g] T. /3 width=2 by fsb_fsba, aaa_fsb/ qed. @@ -39,7 +39,7 @@ fact aaa_ind_fpbu_aux: ∀h,g. ∀R:relation3 genv lenv term. #h #g #R #IH #G #L #T #H @(csx_ind_fpbu … H) -G -L -T #G1 #L1 #T1 #H1 #IH1 #A1 #HTA1 @IH -IH // #G2 #L2 #T2 #H12 elim (fpbs_aaa_conf h g … G2 … L2 … T2 … HTA1) -A1 -/2 width=2 by fpbu_fwd_fpbs/ +/2 width=2 by fpbu_fpbs/ qed-. lemma aaa_ind_fpbu: ∀h,g. ∀R:relation3 genv lenv term. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma index 12df3c22c..0a32134aa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma @@ -16,7 +16,7 @@ include "basic_2/notation/relations/btsnalt_5.ma". include "basic_2/computation/fpbg_fpbg.ma". include "basic_2/computation/fsb.ma". -(* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************) +(* "QRST" STRONGLY NORMALIZING TERMS ****************************************) (* Note: alternative definition of fsb *) inductive fsba (h) (g): relation3 genv lenv term ≝ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma index 5941916f8..ceb783b0b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma @@ -12,34 +12,35 @@ (* *) (**************************************************************************) -include "basic_2/computation/fpbs_ext.ma". include "basic_2/computation/csx_fpbs.ma". include "basic_2/computation/lsx_csx.ma". include "basic_2/computation/fsb_alt.ma". -(* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************) +(* "QRST" STRONGLY NORMALIZING TERMS ****************************************) -(* Advanced propreties on context-sensitive extended normalizing terms *******) +(* Advanced propreties on context-sensitive extended normalizing terms ******) lemma csx_fsb_fpbs: ∀h,g,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G2, L2⦄ ⊢ ⦥[h, g] T2. -#h #g #G1 #L1 #T1 #H @(csx_ind_alt … H) -T1 +#h #g #G1 #L1 #T1 #H @(csx_ind … H) -T1 #T1 #HT1 #IHc #G2 #L2 #T2 @(fqup_wf_ind … G2 L2 T2) -G2 -L2 -T2 #G0 #L0 #T0 #IHu #H10 lapply (csx_fpbs_conf … H10) // -HT1 #HT0 generalize in match IHu; -IHu generalize in match H10; -H10 -@(lsx_ind_alt … (csx_lsx … HT0 0)) -L0 +@(lsx_ind … (csx_lsx … HT0 0)) -L0 #L0 #_ #IHl #H10 #IHu @fsb_intro #G2 #L2 #T2 * -G2 -L2 -T2 [ -IHl -IHc | -IHu -IHl | ] -[ /3 width=5 by fpbs_fqup_trans/ -| #T2 #HT02 #HnT02 elim (fpbs_cpxs_trans_neq … H10 … HT02 HnT02) -T0 +[ /4 width=5 by fpbs_fqup_trans, fqu_fqup/ +| #T2 #HT02 #HnT02 elim (fpbs_cpx_trans_neq … H10 … HT02 HnT02) -T0 /3 width=4 by/ | #L2 #HL02 #HnL02 @(IHl … HL02 HnL02) -IHl -HnL02 [ -IHu -IHc | ] - [ /2 width=3 by fpbs_lpxs_trans/ - | #G3 #L3 #T3 #H03 #_ elim (lpxs_fqup_trans … H03 … HL02) -L2 + [ /3 width=3 by fpbs_lpxs_trans, lpx_lpxs/ + | #G3 #L3 #T3 #H03 #_ elim (lpx_fqup_trans … H03 … HL02) -L2 #L4 #T4 elim (eq_term_dec T0 T4) [ -IHc | -IHu ] - [ #H destruct /4 width=5 by fsb_fpbs_trans, lpxs_fpbs, fpbs_fqup_trans/ - | #HnT04 #HT04 #H04 elim (fpbs_cpxs_trans_neq … H10 … HT04 HnT04) -T0 - /4 width=8 by fpbs_fqup_trans, fpbs_lpxs_trans/ + [ #H destruct /5 width=5 by fsb_fpbs_trans, lpxs_fpbs, fpbs_fqup_trans, lpx_lpxs/ + | #HnT04 #HT04 #H04 #HL43 elim (cpxs_neq_inv_step_sn … HT04 HnT04) -HT04 -HnT04 + #T2 #HT02 #HnT02 #HT24 elim (fpbs_cpx_trans_neq … H10 … HT02 HnT02) -T0 + lapply (fpbs_intro_alt … G3 … L4 … L3 L3 … T3 … HT24 ? ? ?) -HT24 + /3 width=8 by fpbs_trans, lpx_lpxs, fqup_fqus/ (**) (* full auto too slow *) ] ] ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma index 42e34097a..a3ca7a1ac 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/multiple/lleq_lleq.ma". include "basic_2/reduction/lpx_lleq.ma". include "basic_2/computation/cpxs_leq.ma". include "basic_2/computation/lpxs_drop.ma". @@ -30,6 +31,22 @@ lemma lleq_lpxs_trans: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡*[h, g] K2 → /3 width=3 by lpxs_strap1, ex2_intro/ qed-. +lemma lpxs_nlleq_inv_step_sn: ∀h,g,G,L1,L2,T,d. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ≡[T, d] L2 → ⊥) → + ∃∃L,L0. ⦃G, L1⦄ ⊢ ➡[h, g] L & L1 ≡[T, d] L → ⊥ & ⦃G, L⦄ ⊢ ➡*[h, g] L0 & L0 ≡[T, d] L2. +#h #g #G #L1 #L2 #T #d #H @(lpxs_ind_dx … H) -L1 +[ #H elim H -H // +| #L1 #L #H1 #H2 #IH2 #H12 elim (lleq_dec T L1 L d) #H + [ -H1 -H2 elim IH2 -IH2 /3 width=3 by lleq_trans/ -H12 + #L0 #L3 #H1 #H2 #H3 #H4 lapply (lleq_nlleq_trans … H … H2) -H2 + #H2 elim (lleq_lpx_trans … H1 … H) -L + #L #H1 #H lapply (nlleq_lleq_div … H … H2) -H2 + #H2 elim (lleq_lpxs_trans … H3 … H) -L0 + /3 width=8 by lleq_trans, ex4_2_intro/ + | -H12 -IH2 /3 width=6 by ex4_2_intro/ + ] +] +qed-. + lemma lpxs_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ≡[T1, 0] L1 → ∃∃K2. ⦃G1, K1, T1⦄ ⊐ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ≡[T2, 0] L2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_alt.ma index a68fed0c2..48a58442b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_alt.ma @@ -13,7 +13,6 @@ (**************************************************************************) include "basic_2/notation/relations/snalt_6.ma". -include "basic_2/multiple/lleq_lleq.ma". include "basic_2/computation/lpxs_lleq.ma". include "basic_2/computation/lsx.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_scpes.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_scpes.ma index 2c3a1d35c..4895a5105 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_scpes.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_scpes.ma @@ -12,8 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/computation/fpbs_lift.ma". -include "basic_2/computation/fpbg_fleq.ma". +include "basic_2/computation/fpbg_fpbs.ma". include "basic_2/equivalence/scpes_cpcs.ma". include "basic_2/equivalence/scpes_scpes.ma". include "basic_2/dynamic/snv.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/examples/ex_cpr_omega.ma b/matita/matita/contribs/lambdadelta/basic_2/examples/ex_cpr_omega.ma index ef27dfa48..72869603d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/examples/ex_cpr_omega.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/examples/ex_cpr_omega.ma @@ -32,11 +32,11 @@ lemma Delta_lift: ∀W1,W2,d,e. ⬆[d, e] W1 ≡ W2 → (* Main properties **********************************************************) -theorem cpr_Omega_12: ∀W. ⦃⋆, ⋆⦄ ⊢ Omega1 W ➡ Omega2 W. +theorem cpr_Omega_12: ∀G,L,W. ⦃G, L⦄ ⊢ Omega1 W ➡ Omega2 W. /2 width=1 by cpr_beta/ qed. -theorem cpr_Omega_21: ∀W. ⦃⋆, ⋆⦄ ⊢ Omega2 W ➡ Omega1 W. -#W1 elim (lift_total W1 0 1) #W2 #HW12 +theorem cpr_Omega_21: ∀G,L,W. ⦃G, L⦄ ⊢ Omega2 W ➡ Omega1 W. +#G #L #W1 elim (lift_total W1 0 1) #W2 #HW12 @(cpr_zeta … (Omega1 W2)) /3 width=1 by Delta_lift, lift_flat/ @cpr_flat @(cpr_delta … (Delta W1) ? 0) [3,5,8,10: /2 width=2 by Delta_lift/ |4,9: /2 width=1 by cpr_eps/ |*: skip ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/examples/ex_sta_ldec.ma b/matita/matita/contribs/lambdadelta/basic_2/examples/ex_sta_ldec.ma index 376133090..704a913c9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/examples/ex_sta_ldec.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/examples/ex_sta_ldec.ma @@ -1,3 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lstas.ma". (* EXAMPLES *****************************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_lleq.ma index 0458e1da8..d07e13fce 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_lleq.ma @@ -14,6 +14,8 @@ include "basic_2/multiple/lleq_drop.ma". +(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) + (* Main properties **********************************************************) theorem lleq_trans: ∀d,T. Transitive … (lleq d T). @@ -25,8 +27,13 @@ theorem lleq_canc_sn: ∀L,L1,L2,T,d. L ≡[d, T] L1→ L ≡[d, T] L2 → L1 theorem lleq_canc_dx: ∀L1,L2,L,T,d. L1 ≡[d, T] L → L2 ≡[d, T] L → L1 ≡[d, T] L2. /3 width=3 by lleq_trans, lleq_sym/ qed-. -(* Note: lleq_nlleq_trans: ∀d,T,L1,L. L1≡[T, d] L → - ∀L2. (L ≡[T, d] L2 → ⊥) → (L1 ≡[T, d] L2 → ⊥). +(* Advanced properies on negated lazy equivalence *****************************) + +(* Note: for use in auto, works with /4 width=8/ so lleq_canc_sn is preferred *) +lemma lleq_nlleq_trans: ∀d,T,L1,L. L1 ≡[T, d] L → + ∀L2. (L ≡[T, d] L2 → ⊥) → (L1 ≡[T, d] L2 → ⊥). /3 width=3 by lleq_canc_sn/ qed-. -works with /4 width=8/ so lleq_canc_sn is more convenient -*) + +lemma nlleq_lleq_div: ∀d,T,L2,L. L2 ≡[T, d] L → + ∀L1. (L1 ≡[T, d] L → ⊥) → (L1 ≡[T, d] L2 → ⊥). +/3 width=3 by lleq_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma index efe7c5e3d..aaecd70cc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma @@ -17,7 +17,7 @@ include "basic_2/substitution/fquq.ma". include "basic_2/multiple/lleq.ma". include "basic_2/reduction/lpx.ma". -(* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************) +(* "QRST" PARALLEL REDUCTION FOR CLOSURES ***********************************) inductive fpb (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ | fpb_fquq: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → fpb h g G1 L1 T1 G2 L2 T2 @@ -27,7 +27,7 @@ inductive fpb (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ . interpretation - "'big tree' parallel reduction (closure)" + "'qrst' parallel reduction (closure)" 'BTPRed h g G1 L1 T1 G2 L2 T2 = (fpb h g G1 L1 T1 G2 L2 T2). (* Basic properties *********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_aaa.ma index 023e471ff..69a0b1fcf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_aaa.ma @@ -17,7 +17,7 @@ include "basic_2/static/aaa_lleq.ma". include "basic_2/reduction/lpx_aaa.ma". include "basic_2/reduction/fpb.ma". -(* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************) +(* "QRST" PARALLEL REDUCTION FOR CLOSURES ***********************************) (* Properties on atomic arity assignment for terms **************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_lift.ma index 777a944fb..8c9070a44 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_lift.ma @@ -15,7 +15,7 @@ include "basic_2/reduction/cpx_lift.ma". include "basic_2/reduction/fpb.ma". -(* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************) +(* "QRST" PARALLEL REDUCTION FOR CLOSURES ***********************************) (* Advanced properties ******************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma new file mode 100644 index 000000000..9c803f041 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/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/multiple/fleq.ma". +include "basic_2/reduction/fpbu.ma". + +(* "QRST" PROPER PARALLEL REDUCTION 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⦄ ≡[0] ⦃G2, L2, T2⦄. + +interpretation + "'qrst' 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/reduction/fpbc_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc_fleq.ma new file mode 100644 index 000000000..aa5cd7f2b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc_fleq.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/multiple/fleq_fleq.ma". +include "basic_2/reduction/fpbu_fleq.ma". +include "basic_2/reduction/fpbc.ma". + +(* "QRST" PROPER PARALLEL REDUCTION FOR CLOSURES ****************************) + +(* Properties on lazy equivalence on closures *******************************) + +lemma fpbc_fleq_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≻≡[h, g] ⦃G, L, T⦄ → + ⦃G, L, T⦄ ≡[0] ⦃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 fleq_trans, ex2_3_intro/ +qed-. + +lemma fleq_fpbc_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≡[0] ⦃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 (fleq_fpbu_trans … H1 … H0) -G -L -T +/3 width=9 by fleq_trans, ex2_3_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu.ma new file mode 100644 index 000000000..d6d7c9a0a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu.ma @@ -0,0 +1,46 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fpb.ma". + +(* "RST" PROPER PARALLEL COMPUTATION FOR CLOSURES ***************************) + +inductive fpbu (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ +| fpbu_fqu: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → fpbu h g G1 L1 T1 G2 L2 T2 +| fpbu_cpx: ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T2 → (T1 = T2 → ⊥) → fpbu h g G1 L1 T1 G1 L1 T2 +| fpbu_lpx: ∀L2. ⦃G1, L1⦄ ⊢ ➡[h, g] L2 → (L1 ≡[T1, 0] L2 → ⊥) → fpbu h g G1 L1 T1 G1 L2 T1 +. + +interpretation + "'rst' proper parallel reduction (closure)" + 'BTPRedProper h g G1 L1 T1 G2 L2 T2 = (fpbu h g G1 L1 T1 G2 L2 T2). + +(* Basic properties *********************************************************) + +lemma cpr_fpbu: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → + ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄. +/3 width=1 by fpbu_cpx, cpr_cpx/ qed. + +lemma lpr_fpbu: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡ L2 → (L1 ≡[T, 0] L2 → ⊥) → + ⦃G, L1, T⦄ ≻[h, g] ⦃G, L2, T⦄. +/3 width=1 by fpbu_lpx, lpr_lpx/ qed. + +(* Basic forward lemmas *****************************************************) + +lemma fpbu_fwd_fpb: ∀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 +/3 width=1 by fpb_fquq, fpb_cpx, fpb_lpx, fqu_fquq/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu_fleq.ma new file mode 100644 index 000000000..f4a0aed42 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu_fleq.ma @@ -0,0 +1,44 @@ +(**************************************************************************) +(* ___ *) +(* ||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/multiple/fleq.ma". +include "basic_2/reduction/fpbu_lleq.ma". + +(* "RST" PROPER PARALLEL COMPUTATION FOR CLOSURES ***************************) + +(* Properties on lazy equivalence for closures ******************************) + +lemma fleq_fpbu_trans: ∀h,g,F1,F2,K1,K2,T1,T2. ⦃F1, K1, T1⦄ ≡[0] ⦃F2, K2, T2⦄ → + ∀G2,L2,U2. ⦃F2, K2, T2⦄ ≻[h, g] ⦃G2, L2, U2⦄ → + ∃∃G1,L1,U1. ⦃F1, K1, T1⦄ ≻[h, g] ⦃G1, L1, U1⦄ & ⦃G1, L1, U1⦄ ≡[0] ⦃G2, L2, U2⦄. +#h #g #F1 #F2 #K1 #K2 #T1 #T2 * -F2 -K2 -T2 +#K2 #HK12 #G2 #L2 #U2 #H12 elim (lleq_fpbu_trans … HK12 … H12) -K2 +/3 width=5 by fleq_intro, ex2_3_intro/ +qed-. + +lemma fpb_fpbu: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ≡[0] ⦃G2, L2, T2⦄ ∨ + ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 +[ #G2 #L2 #T2 #H elim (fquq_inv_gen … H) -H + [ /3 width=1 by fpbu_fqu, or_intror/ + | * #H1 #H2 #H3 destruct /2 width=1 by or_introl/ + ] +| #T2 #HT12 elim (eq_term_dec T1 T2) + #HnT12 destruct /4 width=1 by fpbu_cpx, or_intror, or_introl/ +| #L2 #HL12 elim (lleq_dec … T1 L1 L2 0) + /4 width=1 by fpbu_lpx, fleq_intro, or_intror, or_introl/ +| /3 width=1 by fleq_intro, or_introl/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu_lift.ma new file mode 100644 index 000000000..a0f28b492 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu_lift.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lstas_da.ma". +include "basic_2/reduction/cpx_lift.ma". +include "basic_2/reduction/fpbu.ma". + +(* "RST" PROPER PARALLEL COMPUTATION FOR CLOSURES ***************************) + +(* Advanced properties ******************************************************) + +lemma sta_fpbu: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → + ⦃G, L⦄ ⊢ T1 •*[h, 1] T2 → ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄. +#h #g #G #L #T1 #T2 #l #HT1 #HT12 elim (eq_term_dec T1 T2) +/3 width=2 by fpbu_cpx, sta_cpx/ #H destruct +elim (lstas_inv_refl_pos h G L T2 0) // +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu_lleq.ma new file mode 100644 index 000000000..9b82c1963 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu_lleq.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/multiple/lleq_fqus.ma". +include "basic_2/multiple/lleq_lleq.ma". +include "basic_2/reduction/lpx_lleq.ma". +include "basic_2/reduction/fpbu.ma". + +(* "RST" PROPER PARALLEL COMPUTATION FOR CLOSURES ***************************) + +(* Properties on lazy equivalence for local environments ********************) + +lemma lleq_fpbu_trans: ∀h,g,F,K1,K2,T. K1 ≡[T, 0] K2 → + ∀G,L2,U. ⦃F, K2, T⦄ ≻[h, g] ⦃G, L2, U⦄ → + ∃∃L1. ⦃F, K1, T⦄ ≻[h, g] ⦃G, L1, U⦄ & L1 ≡[U, 0] L2. +#h #g #F #K1 #K2 #T #HT #G #L2 #U * -G -L2 -U +[ #G #L2 #U #H2 elim (lleq_fqu_trans … H2 … HT) -K2 + /3 width=3 by fpbu_fqu, ex2_intro/ +| /4 width=10 by fpbu_cpx, cpx_lleq_conf_sn, lleq_cpx_trans, ex2_intro/ +| #L2 #HKL2 #HnKL2 elim (lleq_lpx_trans … HKL2 … HT) -HKL2 + /6 width=3 by fpbu_lpx, lleq_canc_sn, ex2_intro/ (* 2 lleq_canc_sn *) +] +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 084720512..0a955cb64 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 @@ -12,7 +12,7 @@ table { class "wine" [ { "examples" * } { [ { "terms with special features" * } { - [ "ex_sta_ldec" + "ex_cpr_omega" * ] + [ "ex_sta_ldec" + "ex_cpr_omega" + "ex_fpbg_refl" * ] } ] } @@ -87,7 +87,7 @@ table { [ "cpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )" "cpre_cpre" * ] } ] - [ { "strongly normalizing \"big tree\" computation" * } { + [ { "strongly normalizing qrst-computation" * } { [ "fsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? )" "fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? )" "fsb_aaa" + "fsb_csx" * ] } ] @@ -98,11 +98,9 @@ table { [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lleq" + "csx_lpx" + "csx_lpxs" + "csx_fpbs" * ] } ] - [ { "\"big tree\" parallel computation" * } { - [ "fpbg ( ⦃?,?,?⦄ >≡[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbg" * ] - [ "fpbc ( ⦃?,?,?⦄ ≻≡[?,?] ⦃?,?,?⦄ )" "fpbc_fleq" + "fpbc_fpbs" * ] - [ "fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpbu_lift" + "fpbu_lleq" + "fpbu_fleq" * ] - [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fleq" + "fpbs_aaa" + "fpbs_fpbs" + "fpbs_ext" * ] + [ { "parallel qrst-computation" * } { + [ "fpbg ( ⦃?,?,?⦄ >≡[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbs" + "fpbg_fpbg" * ] + [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fleq" + "fpbs_aaa" + "fpbs_fpbu" + "fpbs_fpbc" + "fpbs_fpbs" * ] } ] [ { "decomposed extended computation" * } { @@ -131,7 +129,9 @@ table { ] class "water" [ { "reduction" * } { - [ { "\"big tree\" parallel reduction" * } { + [ { "parallel qrst-reduction" * } { + [ "fpbc ( ⦃?,?,?⦄ ≻≡[?,?] ⦃?,?,?⦄ )" "fpbc_fleq" * ] + [ "fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpbu_lift" + "fpbu_lleq" + "fpbu_fleq" * ] [ "fpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "fpb_lift" + "fpb_aaa" * ] } ]