2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "lambda-delta/reduction/tpr.ma".
14 (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
16 definition cpr: lenv → term → term → Prop ≝
17 λL,T1,T2. ∃∃T. T1 ⇒ T & L ⊢ T [0, |L|] ≫ T2.
20 "context-sensitive parallel reduction (term)"
21 'PRed L T1 T2 = (cpr L T1 T2).
23 (* Basic properties *********************************************************)
25 lemma cpr_pr: ∀T1,T2. T1 ⇒ T2 → ∀L. L ⊢ T1 ⇒ T2.
28 lemma cpr_tps: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → L ⊢ T1 ⇒ T2.
31 lemma cpr_refl: ∀L,T. L ⊢ T ⇒ T.
34 (* NOTE: new property *)
35 lemma cpr_flat: ∀I,L,V1,V2,T1,T2.
36 L ⊢ V1 ⇒ V2 → L ⊢ T1 ⇒ T2 → L ⊢ 𝕗{I} V1. T1 ⇒ 𝕗{I} V2. T2.
37 #I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 * /3 width=5/
40 lemma cpr_delta: ∀L,K,V1,V2,V,i.
41 ↓[0, i] L ≡ K. 𝕓{Abbr} V1 → K ⊢ V1 [0, |L| - i - 1] ≫ V2 →
42 ↑[0, i + 1] V2 ≡ V → L ⊢ #i ⇒ V.
43 #L #K #V1 #V2 #V #i #HLK #HV12 #HV2
44 @ex2_1_intro [2: // | skip ] /3 width=8/ (**) (* /4/ is too slow *)
47 lemma cpr_cast: ∀L,V,T1,T2.
48 L ⊢ T1 ⇒ T2 → L ⊢ 𝕗{Cast} V. T1 ⇒ T2.
52 (* Basic inversion lemmas ***************************************************)