+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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-.
(**************************************************************************)
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 *********************************************************)
⦃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 ********************************************************)
(* *)
(**************************************************************************)
-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 ******************************)
| /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-.
(* *)
(**************************************************************************)
-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 ************************************************)
[ #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-.
⦃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 ******************************************************)
(* *)
(**************************************************************************)
-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.
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 ********************************************************)
⦃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⦄.
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 **************************)
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 ≝
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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-.
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 *******************************)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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-.
include "basic_2/computation/fpbs.ma".
-(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************)
+(* "QRST" PARALLEL COMPUTATION FOR CLOSURES *********************************)
(* Main properties **********************************************************)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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-.
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 ******************************************************)
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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-.
(**************************************************************************)
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. (
.
interpretation
- "'big tree' strong normalization (closure)"
+ "'qrst' strong normalization (closure)"
'BTSN h g G L T = (fsb h g G L T).
(* Basic eliminators ********************************************************)
(* 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-.
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.
#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.
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 ≝
(* *)
(**************************************************************************)
-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 *)
]
]
]
(* *)
(**************************************************************************)
+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".
/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.
(**************************************************************************)
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".
(* *)
(**************************************************************************)
-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".
(* 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 ]
+(**************************************************************************)
+(* ___ *)
+(* ||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 *****************************************************************)
include "basic_2/multiple/lleq_drop.ma".
+(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
+
(* Main properties **********************************************************)
theorem lleq_trans: ∀d,T. Transitive … (lleq d T).
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-.
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
.
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 *********************************************************)
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 **************************)
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 ******************************************************)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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-.
class "wine"
[ { "examples" * } {
[ { "terms with special features" * } {
- [ "ex_sta_ldec" + "ex_cpr_omega" * ]
+ [ "ex_sta_ldec" + "ex_cpr_omega" + "ex_fpbg_refl" * ]
}
]
}
[ "cpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )" "cpre_cpre" * ]
}
]
- [ { "strongly normalizing \"big tree\" computation" * } {
+ [ { "strongly normalizing qrst-computation" * } {
[ "fsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? )" "fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? )" "fsb_aaa" + "fsb_csx" * ]
}
]
[ "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" * } {
]
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" * ]
}
]
projects / helm.git / commitdiff