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/substitution/ps_defs.ma".
14 (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
16 inductive tpr: term → term → Prop ≝
17 | tpr_sort : ∀k. tpr (⋆k) (⋆k)
18 | tpr_lref : ∀i. tpr (#i) (#i)
19 | tpr_bind : ∀I,V1,V2,T1,T2. tpr V1 V2 → tpr T1 T2 →
20 tpr (𝕓{I} V1. T1) (𝕓{I} V2. T2)
21 | tpr_flat : ∀I,V1,V2,T1,T2. tpr V1 V2 → tpr T1 T2 →
22 tpr (𝕗{I} V1. T1) (𝕗{I} V2. T2)
23 | tpr_beta : ∀V1,V2,W,T1,T2.
24 tpr V1 V2 → tpr T1 T2 →
25 tpr (𝕚{Appl} V1. 𝕚{Abst} W. T1) (𝕚{Abbr} V2. T2)
26 | tpr_delta: ∀V1,V2,T1,T2,T.
27 tpr V1 V2 → tpr T1 T2 → ⋆. 𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T →
28 tpr (𝕚{Abbr} V1. T1) (𝕚{Abbr} V2. T)
29 | tpr_theta: ∀V,V1,V2,W1,W2,T1,T2.
30 tpr V1 V2 → ↑[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 →
31 tpr (𝕚{Appl} V1. 𝕚{Abbr} W1. T1) (𝕚{Abbr} W2. 𝕚{Appl} V. T2)
32 | tpr_zeta : ∀V,T,T1,T2. ↑[0,1] T1 ≡ T → tpr T1 T2 →
34 | tpr_tau : ∀V,T1,T2. tpr T1 T2 → tpr (𝕚{Cast} V. T1) T2
38 "context-free parallel reduction (term)"
39 'PRed T1 T2 = (tpr T1 T2).
41 (* Basic properties *********************************************************)
43 lemma tpr_refl: ∀T. T ⇒ T.
48 (* The basic inversion lemmas ***********************************************)
50 lemma tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i →
52 | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i &
54 | ∃∃V,T. T ⇒ #i & T1 = 𝕗{Cast} V. T.
55 #T1 #T2 #H elim H -H T1 T2
58 | #I #V1 #V2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
59 | #I #V1 #V2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
60 | #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #i #H destruct
61 | #V1 #V2 #T1 #T2 #T #_ #_ #_ #_ #_ #i #H destruct
62 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #i #H destruct
63 | #V #T #T1 #T2 #HT1 #HT12 #_ #i #H destruct /3 width=6/
64 | #V #T1 #T2 #HT12 #_ #i #H destruct /3/
68 lemma tpr_inv_lref2: ∀T1,i. T1 ⇒ #i →
70 | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i &
72 | ∃∃V,T. T ⇒ #i & T1 = 𝕗{Cast} V. T.