(* Basic eliminators ********************************************************)
lemma xprs_ind: ∀h,g,L,T1. ∀R:predicate term. R T1 →
- (â\88\80T,T2. â¦\83h, Lâ¦\84 â\8a¢ T1 â\9e¸*[g] T â\86\92 â¦\83h, Lâ¦\84 â\8a¢ T â\9e¸[g] T2 → R T → R T2) →
- â\88\80T2. â¦\83h, Lâ¦\84 â\8a¢ T1 â\9e¸*[g] T2 → R T2.
+ (â\88\80T,T2. â¦\83h, Lâ¦\84 â\8a¢ T1 â\80¢â\9e¡*[g] T â\86\92 â¦\83h, Lâ¦\84 â\8a¢ T â\80¢â\9e¡[g] T2 → R T → R T2) →
+ â\88\80T2. â¦\83h, Lâ¦\84 â\8a¢ T1 â\80¢â\9e¡*[g] T2 → R T2.
#h #g #L #T1 #R #HT1 #IHT1 #T2 #HT12
@(TC_star_ind … HT1 IHT1 … HT12) //
qed-.
lemma xprs_ind_dx: ∀h,g,L,T2. ∀R:predicate term. R T2 →
- (â\88\80T1,T. â¦\83h, Lâ¦\84 â\8a¢ T1 â\9e¸[g] T â\86\92 â¦\83h, Lâ¦\84 â\8a¢ T â\9e¸*[g] T2 → R T → R T1) →
- â\88\80T1. â¦\83h, Lâ¦\84 â\8a¢ T1 â\9e¸*[g] T2 → R T1.
+ (â\88\80T1,T. â¦\83h, Lâ¦\84 â\8a¢ T1 â\80¢â\9e¡[g] T â\86\92 â¦\83h, Lâ¦\84 â\8a¢ T â\80¢â\9e¡*[g] T2 → R T → R T1) →
+ â\88\80T1. â¦\83h, Lâ¦\84 â\8a¢ T1 â\80¢â\9e¡*[g] T2 → R T1.
#h #g #L #T2 #R #HT2 #IHT2 #T1 #HT12
@(TC_star_ind_dx … HT2 IHT2 … HT12) //
qed-.
(* Basic properties *********************************************************)
-lemma xprs_refl: ∀h,g,L,T. ⦃h, L⦄ ⊢ T ➸*[g] T.
+lemma xprs_refl: ∀h,g,L. reflexive … (xprs h g L).
/2 width=1/ qed.
lemma xprs_strap1: ∀h,g,L,T1,T,T2.
- â¦\83h, Lâ¦\84 â\8a¢ T1 â\9e¸*[g] T â\86\92 â¦\83h, Lâ¦\84 â\8a¢ T â\9e¸[g] T2 â\86\92 â¦\83h, Lâ¦\84 â\8a¢ T1 â\9e¸*[g] T2.
-/2 width=3 by step/ qed. (**) (* NTypeChecker failure without trace *)
+ â¦\83h, Lâ¦\84 â\8a¢ T1 â\80¢â\9e¡*[g] T â\86\92 â¦\83h, Lâ¦\84 â\8a¢ T â\80¢â\9e¡[g] T2 â\86\92 â¦\83h, Lâ¦\84 â\8a¢ T1 â\80¢â\9e¡*[g] T2.
+/2 width=3/ qed.
lemma xprs_strap2: ∀h,g,L,T1,T,T2.
- â¦\83h, Lâ¦\84 â\8a¢ T1 â\9e¸[g] T â\86\92 â¦\83h, Lâ¦\84 â\8a¢ T â\9e¸*[g] T2 â\86\92 â¦\83h, Lâ¦\84 â\8a¢ T1 â\9e¸*[g] T2.
-/2 width=3 by TC_strap/ qed. (**) (* NTypeChecker failure without trace *)
+ â¦\83h, Lâ¦\84 â\8a¢ T1 â\80¢â\9e¡[g] T â\86\92 â¦\83h, Lâ¦\84 â\8a¢ T â\80¢â\9e¡*[g] T2 â\86\92 â¦\83h, Lâ¦\84 â\8a¢ T1 â\80¢â\9e¡*[g] T2.
+/2 width=3/ qed.
(* Basic inversion lemmas ***************************************************)
(*
(* Properties on atomic arity assignment for terms **************************)
-lemma xprs_aaa: â\88\80h,g,L,T,A. L â\8a¢ T â\81\9d A â\86\92 â\88\80U. â¦\83h, Lâ¦\84 â\8a¢ T â\9e¸*[g] U → L ⊢ U ⁝ A.
+lemma xprs_aaa: â\88\80h,g,L,T,A. L â\8a¢ T â\81\9d A â\86\92 â\88\80U. â¦\83h, Lâ¦\84 â\8a¢ T â\80¢â\9e¡*[g] U → L ⊢ U ⁝ A.
#h #g #L #T #A #HT #U #H @(xprs_ind … H) -U // /2 width=5/
qed.
(* properties on context sensitive parallel computation for terms ***********)
-lemma cprs_xprs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → ⦃h, L⦄ ⊢ T1 ➸*[g] T2.
-#h #g #L #T1 #T2 #H @(cprs_ind … H) -T2 //
-/3 width=3 by xprs_strap1, cpr_xpr/ (**) (* NTypeChecker failure without trace *)
+lemma cprs_xprs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → ⦃h, L⦄ ⊢ T1 •➡*[g] T2.
+#h #g #L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=3/
qed.
(* Advanced forward lemmas **************************************************)
-lemma xprs_fwd_abst1: â\88\80h,g,a,L,V1,T1,U2. â¦\83h, Lâ¦\84 â\8a¢ â\93\9b{a}V1. T1 â\9e¸*[g] U2 →
+lemma xprs_fwd_abst1: â\88\80h,g,a,L,V1,T1,U2. â¦\83h, Lâ¦\84 â\8a¢ â\93\9b{a}V1. T1 â\80¢â\9e¡*[g] U2 →
∃∃V2,T2. L ⊢ V1 ➡* V2 & U2 = ⓛ{a}V2. T2.
#h #g #a #L #V1 #T1 #U2 #H @(xprs_ind … H) -U2 /2 width=4/
#U #U2 #_ #HU2 * #V #T #HV1 #H destruct
(* Relocation properties ****************************************************)
lemma xprs_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K → ∀T1,U1. ⇧[d, e] T1 ≡ U1 →
- â\88\80h,g,T2. â¦\83h, Kâ¦\84 â\8a¢ T1 â\9e¸*[g] T2 → ∀U2. ⇧[d, e] T2 ≡ U2 →
- â¦\83h, Lâ¦\84 â\8a¢ U1 â\9e¸*[g] U2.
+ â\88\80h,g,T2. â¦\83h, Kâ¦\84 â\8a¢ T1 â\80¢â\9e¡*[g] T2 → ∀U2. ⇧[d, e] T2 ≡ U2 →
+ â¦\83h, Lâ¦\84 â\8a¢ U1 â\80¢â\9e¡*[g] U2.
#L #K #d #e #HLK #T1 #U1 #HTU1 #h #g #T2 #HT12 @(xprs_ind … HT12) -T2
[ -HLK #T2 #HT12
<(lift_mono … HTU1 … HT12) -T1 //
| -HTU1 #T #T2 #_ #HT2 #IHT2 #U2 #HTU2
elim (lift_total T d e) #U #HTU
- lapply (xpr_lift … HLK … HTU … HTU2 … HT2) -T2 -HLK (* /3 width=3/ *)
- #H @(step …H) /2 width=1/ (**) (* NTypeChecker failure *)
+ lapply (xpr_lift … HLK … HTU … HTU2 … HT2) -T2 -HLK /3 width=3/
]
qed.
lemma xprs_inv_lift1: ∀L,K,d,e. ⇩[d, e] L ≡ K →
- â\88\80T1,U1. â\87§[d, e] T1 â\89¡ U1 â\86\92 â\88\80h,g,U2. â¦\83h, Lâ¦\84 â\8a¢ U1 â\9e¸*[g] U2 →
- â\88\83â\88\83T2. â\87§[d, e] T2 â\89¡ U2 & â¦\83h, Kâ¦\84 â\8a¢ T1 â\9e¸*[g] T2.
+ â\88\80T1,U1. â\87§[d, e] T1 â\89¡ U1 â\86\92 â\88\80h,g,U2. â¦\83h, Lâ¦\84 â\8a¢ U1 â\80¢â\9e¡*[g] U2 →
+ â\88\83â\88\83T2. â\87§[d, e] T2 â\89¡ U2 & â¦\83h, Kâ¦\84 â\8a¢ T1 â\80¢â\9e¡*[g] T2.
#L #K #d #e #HLK #T1 #U1 #HTU1 #h #g #U2 #HU12 @(xprs_ind … HU12) -U2 /2 width=3/
-HTU1 #U #U2 #_ #HU2 * #T #HTU #HT1
-elim (xpr_inv_lift1 … HLK … HTU … HU2) -U -HLK (* /3 width=5/ *)
-#U #HU2 #HTU @(ex2_1_intro … HU2) @(step … HT1 HTU) (**) (* NTypeChecker failure *)
+elim (xpr_inv_lift1 … HLK … HTU … HU2) -U -HLK /3 width=5/
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/xprs.ma".
+
+(* EXTENDED PARALLEL COMPUTATION ON TERMS ***********************************)
+
+theorem xprs_trans: ∀h,g,L. transitive … (xprs h g L).
+/2 width=3/ 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/reducibility/ypr.ma".
+
+(* HYPER PARALLEL COMPUTATION ON CLOSURES ***********************************)
+
+definition yprs: ∀h. sd h → bi_relation lenv term ≝
+ λh,g. bi_TC … (ypr h g).
+
+interpretation "hyper parallel computation (closure)"
+ 'YPRedStar h g L1 T1 L2 T2 = (yprs h g L1 T1 L2 T2).
+
+(* Basic eliminators ********************************************************)
+
+lemma yprs_ind: ∀h,g,L1,T1. ∀R:relation2 lenv term. R L1 T1 →
+ (∀L,L2,T,T2. h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ •⥸[g] ⦃L2, T2⦄ → R L T → R L2 T2) →
+ ∀L2,T2. h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄ → R L2 T2.
+/3 width=7 by bi_TC_star_ind/ qed-.
+
+lemma yprs_ind_dx: ∀h,g,L2,T2. ∀R:relation2 lenv term. R L2 T2 →
+ (∀L1,L,T1,T. h ⊢ ⦃L1, T1⦄ •⥸[g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ •⥸*[g] ⦃L2, T2⦄ → R L T → R L1 T1) →
+ ∀L1,T1. h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄ → R L1 T1.
+/3 width=7 by bi_TC_star_ind_dx/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma yprs_refl: ∀h,g. bi_reflexive … (yprs h g).
+/2 width=1/ qed.
+
+lemma yprs_strap1: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L, T⦄ →
+ h ⊢ ⦃L, T⦄ •⥸[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+lemma yprs_strap2: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ •⥸[g] ⦃L, T⦄ →
+ h ⊢ ⦃L, T⦄ •⥸*[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄.
+/2 width=4/ 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/csups.ma".
+include "basic_2/computation/yprs.ma".
+
+(* HYPER PARALLEL COMPUTATION ON CLOSURES ***********************************)
+
+(* Properties on iterated supclosure ****************************************)
+
+lemma csups_yprs: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ >* ⦃L2, T2⦄ →
+ h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄.
+#h #g #L1 #L2 #T1 #T2 #H @(csups_ind … H) -L2 -T2 /3 width=1/ /3 width=4/
+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/xprs_cprs.ma".
+include "basic_2/computation/yprs.ma".
+
+(* HYPER PARALLEL COMPUTATION ON CLOSURES ***********************************)
+
+(* Properties on extended parallel computation for terms ********************)
+
+lemma xprs_yprs: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •➡*[g] T2 →
+ h ⊢ ⦃L, T1⦄ •⥸*[g] ⦃L, T2⦄.
+#h #g #L #T1 #T2 #H @(xprs_ind … H) -T2 // /3 width=4/
+qed.
+
+lemma cprs_yprs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → h ⊢ ⦃L, T1⦄ •⥸*[g] ⦃L, T2⦄.
+/3 width=1/ 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/yprs.ma".
+
+(* HYPER PARALLEL COMPUTATION ON TERMS **************************************)
+
+theorem yprs_trans: ∀h,g. bi_transitive … (yprs h g).
+/2 width=4/ 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/substitution/csup.ma".
+include "basic_2/computation/yprs.ma".
+
+(* ITERATED STEP OF HYPER PARALLEL COMPUTATION ON CLOSURES ******************)
+
+inductive ysteps (h) (g) (L1) (T1) (L2) (T2): Prop ≝
+| ysteps_intro: h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄ → (L1 = L2 → T1 = T2 → ⊥) →
+ ysteps h g L1 T1 L2 T2
+.
+
+interpretation "iterated step of hyper parallel computation (closure)"
+ 'YPRedStepStar h g L1 T1 L2 T2 = (ysteps h g L1 T1 L2 T2).
+
+(* Basic properties *********************************************************)
+
+lemma ssta_ysteps: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l + 1] U →
+ h ⊢ ⦃L, T⦄ •⭃*[g] ⦃L, U⦄.
+#h #g #L #T #U #l #HTU
+@ysteps_intro /3 width=2/ #_ #H destruct
+elim (ssta_inv_refl … HTU)
+qed.
+
+lemma csup_ysteps: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ →
+ h ⊢ ⦃L1, T1⦄ •⭃*[g] ⦃L2, T2⦄.
+#h #g #L1 #L2 #T1 #T2 #H
+lapply (csup_fwd_cw … H) #H1
+@ysteps_intro /3 width=1/ -H #H2 #H3 destruct
+elim (lt_refl_false … H1)
+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/yprs_csups.ma".
+include "basic_2/computation/ysteps.ma".
+
+(* ITERATED STEP OF HYPER PARALLEL COMPUTATION ON CLOSURES ******************)
+
+(* Properties on iterated supclosure ****************************************)
+
+lemma csups_ysteps: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ >* ⦃L2, T2⦄ →
+ h ⊢ ⦃L1, T1⦄ •⭃*[g] ⦃L2, T2⦄.
+#h #g #L1 #L2 #T1 #T2 #H
+lapply (csups_fwd_cw … H) #H1
+@ysteps_intro /2 width=1/ -H #H2 #H3 destruct
+elim (lt_refl_false … H1)
+qed.
| snv_bind: ∀a,I,L,V,T. snv h g L V → snv h g (L.ⓑ{I}V) T → snv h g L (ⓑ{a,I}V.T)
| snv_appl: ∀a,L,V,W,W0,T,U,l. snv h g L V → snv h g L T →
⦃h, L⦄ ⊢ V •[g, l + 1] W → L ⊢ W ➡* W0 →
- â¦\83h, Lâ¦\84 â\8a¢ T â\9e¸*[g] ⓛ{a}W0.U → snv h g L (ⓐV.T)
+ â¦\83h, Lâ¦\84 â\8a¢ T â\80¢â\9e¡*[g] ⓛ{a}W0.U → snv h g L (ⓐV.T)
| snv_cast: ∀L,W,T,U,l. snv h g L W → snv h g L T →
⦃h, L⦄ ⊢ T •[g, l + 1] U → L ⊢ W ⬌* U → snv h g L (ⓝW.T)
.
fact snv_inv_appl_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀V,T. X = ⓐV.T →
∃∃a,W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] &
⦃h, L⦄ ⊢ V •[g, l + 1] W & L ⊢ W ➡* W0 &
- â¦\83h, Lâ¦\84 â\8a¢ T â\9e¸*[g] ⓛ{a}W0.U.
+ â¦\83h, Lâ¦\84 â\8a¢ T â\80¢â\9e¡*[g] ⓛ{a}W0.U.
#h #g #L #X * -L -X
[ #L #k #V #T #H destruct
| #I #L #K #V0 #i #_ #_ #V #T #H destruct
lemma snv_inv_appl: ∀h,g,L,V,T. ⦃h, L⦄ ⊩ ⓐV.T :[g] →
∃∃a,W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] &
⦃h, L⦄ ⊢ V •[g, l + 1] W & L ⊢ W ➡* W0 &
- â¦\83h, Lâ¦\84 â\8a¢ T â\9e¸*[g] ⓛ{a}W0.U.
+ â¦\83h, Lâ¦\84 â\8a¢ T â\80¢â\9e¡*[g] ⓛ{a}W0.U.
/2 width=3/ qed-.
fact snv_inv_cast_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀W,T. X = ⓝW.T →
| #I #L #K #V #i #HLK #_ * /3 width=6/
| #a * #L #V #T #_ #_ * #B #HV * #A #HA /3 width=2/
| #a #L #V #W #W0 #T #U #l #_ #_ #HVW #HW0 #HTU * #B #HV * #X #HT
- lapply (xprs_aaa h g … HV W0 ?)
- [ /3 width=3 by xprs_strap2, ssta_xpr, cprs_xprs/ ] -W #HW0 (**) (* NTypeChecker failure without trace *)
+ lapply (xprs_aaa h g … HV W0 ?) [ /3 width=3/ ] -W #HW0
lapply (xprs_aaa … HT … HTU) -HTU #H
elim (aaa_inv_abst … H) -H #B0 #A #H1 #HU #H2 destruct
lapply (aaa_mono … H1 … HW0) -W0 #H destruct /3 width=4/
non associative with precedence 45
for @{ 'RDrop $d $e $L1 $L2 }.
+notation "hvbox( ⦃ L1, break T1 ⦄ > break ⦃ L2 , break T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'SupTerm $L1 $T1 $L2 $T2 }.
+
notation "hvbox( L ⊢ break ⌘ ⦃ T ⦄ ≡ break term 46 k )"
non associative with precedence 45
for @{ 'ICM $L $T $k }.
non associative with precedence 45
for @{ 'RDropStar $e $L1 $L2 }.
+notation "hvbox( ⦃ L1, break T1 ⦄ > * break ⦃ L2 , break T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'SupTermStar $L1 $T1 $L2 $T2 }.
+
notation "hvbox( T1 break ▶ * [ d , break e ] break term 46 T2 )"
non associative with precedence 45
for @{ 'PSubstStar $T1 $d $e $T2 }.
non associative with precedence 45
for @{ 'FocalizedPRedAlt $L1 $L2 }.
-notation "hvbox( â¦\83 h , break L â¦\84 â\8a¢ break term 46 T1 â\9e¸ break [ g ] break term 46 T2 )"
+notation "hvbox( â¦\83 h , break L â¦\84 â\8a¢ break term 46 T1 â\80¢ â\9e¡ break [ g ] break term 46 T2 )"
non associative with precedence 45
for @{ 'XPRed $h $g $L $T1 $T2 }.
+notation "hvbox( h ⊢ break ⦃ L1, break T1 ⦄ • ⥸ break [ g ] break ⦃ L2 , break T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'YPRed $h $g $L1 $T1 $L2 $T2 }.
+
(* Computation **************************************************************)
notation "hvbox( T1 ➡ * break term 46 T2 )"
non associative with precedence 45
for @{ 'CrSubEq $T1 $R $T2 }.
-notation "hvbox( â¦\83 h , break L â¦\84 â\8a¢ break term 46 T1 â\9e¸ * break [ g ] break term 46 T2 )"
+notation "hvbox( â¦\83 h , break L â¦\84 â\8a¢ break term 46 T1 â\80¢ â\9e¡ * break [ g ] break term 46 T2 )"
non associative with precedence 45
for @{ 'XPRedStar $h $g $L $T1 $T2 }.
-notation "hvbox( â¦\83 h , break L â¦\84 â\8a¢ â\9e· * break [ g ] break term 46 T2 )"
+notation "hvbox( â¦\83 h , break L â¦\84 â\8a¢ â\80¢ â¬\8a * break [ g ] break term 46 T2 )"
non associative with precedence 45
for @{ 'XSN $h $g $L $T }.
+notation "hvbox( h ⊢ break ⦃ L1, break T1 ⦄ • ⥸ * break [ g ] break ⦃ L2 , break T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'YPRedStar $h $g $L1 $T1 $L2 $T2 }.
+
+notation "hvbox( h ⊢ break ⦃ L1, break T1 ⦄ • ⭃ * break [ g ] break ⦃ L2 , break T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'YPRedStepStar $h $g $L1 $T1 $L2 $T2 }.
+
(* Conversion ***************************************************************)
notation "hvbox( L ⊢ break term 46 T1 ⬌ break term 46 T2 )"
(* EXTENDED PARALLEL REDUCTION ON TERMS *************************************)
-definition xpr: ∀h. sd h → lenv → relation term ≝
- λh,g,L,T1,T2. L ⊢ T1 ➡ T2 ∨ ∃l. ⦃h, L⦄ ⊢ T1 •[g, l + 1] T2.
+inductive xpr (h) (g) (L) (T1) (T2): Prop ≝
+| xpr_cpr : L ⊢ T1 ➡ T2 → xpr h g L T1 T2
+| xpr_ssta: ∀l. ⦃h, L⦄ ⊢ T1 •[g, l + 1] T2 → xpr h g L T1 T2
+.
interpretation
"extended parallel reduction (term)"
(* Basic properties *********************************************************)
-lemma cpr_xpr: ∀h,g,L,T1,T2. L ⊢ T1 ➡ T2 → ⦃h, L⦄ ⊢ T1 ➸[g] T2.
-/2 width=1/ qed.
-
-lemma ssta_xpr: ∀h,g,L,T1,T2,l. ⦃h, L⦄ ⊢ T1 •[g, l + 1] T2 → ⦃h, L⦄ ⊢ T1 ➸[g] T2.
-/3 width=2/ qed.
-
-lemma xpr_refl: ∀h,g,L,T. ⦃h, L⦄ ⊢ T ➸[g] T.
+lemma xpr_refl: ∀h,g,L. reflexive … (xpr h g L).
/2 width=1/ qed.
(* Properties on atomic arity assignment for terms **************************)
-lemma xpr_aaa: â\88\80h,g,L,T,A. L â\8a¢ T â\81\9d A â\86\92 â\88\80U. â¦\83h, Lâ¦\84 â\8a¢ T â\9e¸[g] U → L ⊢ U ⁝ A.
-#h #g #L #T #A #HT #U * [2: * ] /2 width=3/ /2 width=6/
+lemma xpr_aaa: â\88\80h,g,L,T,A. L â\8a¢ T â\81\9d A â\86\92 â\88\80U. â¦\83h, Lâ¦\84 â\8a¢ T â\80¢â\9e¡[g] U → L ⊢ U ⁝ A.
+#h #g #L #T #A #HT #U * /2 width=3/ /2 width=6/
qed.
(* Advanced inversion lemmas ************************************************)
-lemma xpr_inv_abst1: â\88\80h,g,a,L,V1,T1,U2. â¦\83h, Lâ¦\84 â\8a¢ â\93\9b{a}V1.T1 â\9e¸[g] U2 →
- â\88\83â\88\83V2,T2. L â\8a¢ V1 â\9e¡ V2 & â¦\83h, L. â\93\9bV1â¦\84 â\8a¢ T1 â\9e¸[g] T2 &
+lemma xpr_inv_abst1: â\88\80h,g,a,L,V1,T1,U2. â¦\83h, Lâ¦\84 â\8a¢ â\93\9b{a}V1.T1 â\80¢â\9e¡[g] U2 →
+ â\88\83â\88\83V2,T2. L â\8a¢ V1 â\9e¡ V2 & â¦\83h, L. â\93\9bV1â¦\84 â\8a¢ T1 â\80¢â\9e¡[g] T2 &
U2 = ⓛ{a}V2. T2.
#h #g #a #L #V1 #T1 #U2 *
[ #H elim (cpr_inv_abst1 … H Abst V1) /3 width=5/
-| * #l #H elim (ssta_inv_bind1 … H) /3 width=5/
+| #l #H elim (ssta_inv_bind1 … H) /3 width=5/
]
qed-.
lemma xpr_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K →
∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀T2,U2. ⇧[d, e] T2 ≡ U2 →
- â\88\80h,g. â¦\83h, Kâ¦\84 â\8a¢ T1 â\9e¸[g] T2 â\86\92 â¦\83h, Lâ¦\84 â\8a¢ U1 â\9e¸[g] U2.
-#L #K #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #h #g * [2: * ]
+ â\88\80h,g. â¦\83h, Kâ¦\84 â\8a¢ T1 â\80¢â\9e¡[g] T2 â\86\92 â¦\83h, Lâ¦\84 â\8a¢ U1 â\80¢â\9e¡[g] U2.
+#L #K #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #h #g *
/3 width=9/ /3 width=10/
qed.
lemma xpr_inv_lift1: ∀L,K,d,e. ⇩[d, e] L ≡ K →
- â\88\80T1,U1. â\87§[d, e] T1 â\89¡ U1 â\86\92 â\88\80h,g,U2. â¦\83h, Lâ¦\84 â\8a¢ U1 â\9e¸[g] U2 →
- â\88\83â\88\83T2. â\87§[d, e] T2 â\89¡ U2 & â¦\83h, Kâ¦\84 â\8a¢ T1 â\9e¸[g] T2.
-#L #K #d #e #HLK #T1 #U1 #HTU1 #h #g #U2 * [ #HU12 | * #l #HU12 ]
+ â\88\80T1,U1. â\87§[d, e] T1 â\89¡ U1 â\86\92 â\88\80h,g,U2. â¦\83h, Lâ¦\84 â\8a¢ U1 â\80¢â\9e¡[g] U2 →
+ â\88\83â\88\83T2. â\87§[d, e] T2 â\89¡ U2 & â¦\83h, Kâ¦\84 â\8a¢ T1 â\80¢â\9e¡[g] T2.
+#L #K #d #e #HLK #T1 #U1 #HTU1 #h #g #U2 * [ #HU12 | #l #HU12 ]
[ elim (cpr_inv_lift1 … HLK … HTU1 … HU12) -L -U1 /3 width=3/
| elim (ssta_inv_lift1 … HU12 … HLK … HTU1) -L -U1 /3 width=4/
]
--- /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/substitution/csup.ma".
+include "basic_2/reducibility/xpr.ma".
+
+(* HYPER PARALLEL REDUCTION ON CLOSURES *************************************)
+
+inductive ypr (h) (g) (L1) (T1): relation2 lenv term ≝
+| ypr_cpr : ∀T2. L1 ⊢ T1 ➡ T2 → ypr h g L1 T1 L1 T2
+| ypr_ssta: ∀T2,l. ⦃h, L1⦄ ⊢ T1 •[g, l + 1] T2 → ypr h g L1 T1 L1 T2
+| ypr_csup: ∀L2,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → ypr h g L1 T1 L2 T2
+.
+
+interpretation
+ "hyper parallel reduction (closure)"
+ 'YPRed h g L1 T1 L2 T2 = (ypr h g L1 T1 L2 T2).
+
+(* Basic properties *********************************************************)
+
+lemma ypr_refl: ∀h,g. bi_reflexive … (ypr h g).
+/2 width=1/ qed.
+
+lemma xpr_ypr: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •➡[g] T2 → h ⊢ ⦃L, T1⦄ •⥸[g] ⦃L, T2⦄.
+#h #g #L #T1 #T2 * /2 width=1/ /2 width=2/
+qed.
∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y •[g, l-1] Z1 & ⦃h, L⦄ ⊢ X •[g, l] Z2 &
U = ⓝZ1.Z2.
/2 width=4/ qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+fact ssta_inv_refl_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → T = U → ⊥.
+#h #g #L #T #U #l #H elim H -L -T -U -l
+[ #L #k #l #_ #H
+ lapply (next_lt h k) destruct -H -e0 (**) (* these premises are not erased *)
+ <e1 -e1 #H elim (lt_refl_false … H)
+| #L #K #V #W #U #i #l #_ #_ #HWU #_ #H destruct
+ elim (lift_inv_lref2_be … HWU ? ?) -HWU //
+| #L #K #W #V #U #i #l #_ #_ #HWU #_ #H destruct
+ elim (lift_inv_lref2_be … HWU ? ?) -HWU //
+| #a #I #L #V #T #U #l #_ #IHTU #H destruct /2 width=1/
+| #L #V #T #U #l #_ #IHTU #H destruct /2 width=1/
+| #L #V #W #T #U #l #_ #_ #_ #IHTU #H destruct /2 width=1/
+]
+qed.
+
+lemma ssta_inv_refl: ∀h,g,L,T,l. ⦃h, L⦄ ⊢ T •[g, l] T → ⊥.
+/2 width=8/ 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/substitution/ldrop.ma".
+
+(* SUPCLOSURE ***************************************************************)
+
+inductive csup: bi_relation lenv term ≝
+| csup_lref : ∀I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → csup L (#i) K V
+| csup_bind_sn: ∀a,I,L,V,T. csup L (ⓑ{a,I}V.T) L V
+| csup_bind_dx: ∀a,I,L,V,T. csup L (ⓑ{a,I}V.T) (L.ⓑ{I}V) T
+| csup_flat_sn: ∀I,L,V,T. csup L (ⓕ{I}V.T) L V
+| csup_flat_dx: ∀I,L,V,T. csup L (ⓕ{I}V.T) L T
+.
+
+interpretation
+ "structural predecessor (closure)"
+ 'SupTerm L1 T1 L2 T2 = (csup L1 T1 L2 T2).
+
+(* Basic forward lemmas *****************************************************)
+
+lemma csup_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → #{L2, T2} < #{L1, T1}.
+#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /width=1/ /2 width=4 by ldrop_pair2_fwd_cw/
+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/substitution/csup.ma".
+
+(* ITERATED SUPCLOSURE ******************************************************)
+
+definition csups: bi_relation lenv term ≝ bi_TC … csup.
+
+interpretation "iterated structural predecessor (closure)"
+ 'SupTermStar L1 T1 L2 T2 = (csups L1 T1 L2 T2).
+
+(* Basic eliminators ********************************************************)
+
+lemma csups_ind: ∀L1,T1. ∀R:relation2 lenv term.
+ (∀L2,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → R L2 T2) →
+ (∀L,T,L2,T2. ⦃L1, T1⦄ >* ⦃L, T⦄ → ⦃L, T⦄ > ⦃L2, T2⦄ → R L T → R L2 T2) →
+ ∀L2,T2. ⦃L1, T1⦄ >* ⦃L2, T2⦄ → R L2 T2.
+#L1 #T1 #R #IH1 #IH2 #L2 #T2 #H
+@(bi_TC_ind … IH1 IH2 ? ? H)
+qed-.
+
+lemma csups_ind_dx: ∀L2,T2. ∀R:relation2 lenv term.
+ (∀L1,T1. ⦃L1, T1⦄ > ⦃L2, T2⦄ → R L1 T1) →
+ (∀L1,L,T1,T. ⦃L1, T1⦄ > ⦃L, T⦄ → ⦃L, T⦄ >* ⦃L2, T2⦄ → R L T → R L1 T1) →
+ ∀L1,T1. ⦃L1, T1⦄ >* ⦃L2, T2⦄ → R L1 T1.
+#L2 #T2 #R #IH1 #IH2 #L1 #T1 #H
+@(bi_TC_ind_dx … IH1 IH2 ? ? H)
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma csups_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ >* ⦃L, T⦄ → ⦃L, T⦄ > ⦃L2, T2⦄ →
+ ⦃L1, T1⦄ >* ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+lemma csups_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ > ⦃L, T⦄ → ⦃L, T⦄ >* ⦃L2, T2⦄ →
+ ⦃L1, T1⦄ >* ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma csups_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ >* ⦃L2, T2⦄ → #{L2, T2} < #{L1, T1}.
+#L1 #L2 #T1 #T2 #H @(csups_ind … H) -L2 -T2
+/3 width=3 by csup_fwd_cw, transitive_lt/
+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/csups.ma".
+
+(* ITERATED SUPCLOSURE ******************************************************)
+
+(* Main propertis ***********************************************************)
+
+theorem csups_trans: bi_transitive … csups.
+/2 width=4/ qed.
projects / helm.git / commitdiff