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/pts.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 (* Basic inversion lemmas ***************************************************)
50 lemma tpr_inv_sort1_aux: ∀U1,U2. U1 ⇒ U2 → ∀k. U1 = ⋆k → U2 = ⋆k.
52 [ #k0 #k #H destruct -k0 //
54 | #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
55 | #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
56 | #V1 #V2 #W #T1 #T2 #_ #_ #k #H destruct
57 | #V1 #V2 #T1 #T2 #T #_ #_ #_ #k #H destruct
58 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #k #H destruct
59 | #V #T #T1 #T2 #_ #_ #k #H destruct
60 | #V #T1 #T2 #_ #k #H destruct
64 lemma tpr_inv_sort1: ∀k,U2. ⋆k ⇒ U2 → U2 = ⋆k.
67 lemma tpr_inv_lref1_aux: ∀U1,U2. U1 ⇒ U2 → ∀i. U1 = #i → U2 = #i.
70 | #j #i #H destruct -j //
71 | #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
72 | #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
73 | #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct
74 | #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct
75 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
76 | #V #T #T1 #T2 #_ #_ #i #H destruct
77 | #V #T1 #T2 #_ #i #H destruct
81 lemma tpr_inv_lref1: ∀i,U2. #i ⇒ U2 → U2 = #i.
84 lemma tpr_inv_abbr1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Abbr} V1. T1 →
85 ∨∨ ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abbr} V2. T2
86 | ∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
87 ⋆. 𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T &
89 | ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2.
91 [ #k #V #T #H destruct
92 | #i #V #T #H destruct
93 | #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /3 width=5/
94 | #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
95 | #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct
96 | #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #V0 #T0 #H destruct -V1 T1 /3 width=7/
97 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct
98 | #V #T #T1 #T2 #HT1 #HT12 #V0 #T0 #H destruct -V T /3/
99 | #V #T1 #T2 #_ #V0 #T0 #H destruct
103 lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕚{Abbr} V1. T1 ⇒ U2 →
104 ∨∨ ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abbr} V2. T2
105 | ∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
106 ⋆. 𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T &
108 | ∃∃T. ↑[0,1] T ≡ T1 & tpr T U2.
111 lemma tpr_inv_abst1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Abst} V1. T1 →
112 ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abst} V2. T2.
114 [ #k #V #T #H destruct
115 | #i #V #T #H destruct
116 | #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /2 width=5/
117 | #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
118 | #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct
119 | #V1 #V2 #T1 #T2 #T #_ #_ #_ #V0 #T0 #H destruct
120 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct
121 | #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct
122 | #V #T1 #T2 #_ #V0 #T0 #H destruct
126 lemma tpr_inv_abst1: ∀V1,T1,U2. 𝕚{Abst} V1. T1 ⇒ U2 →
127 ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abst} V2. T2.
130 lemma tpr_inv_bind1: ∀V1,T1,U2,I. 𝕓{I} V1. T1 ⇒ U2 →
131 ∨∨ ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕓{I} V2. T2
132 | ∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
133 ⋆. 𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T &
134 U2 = 𝕚{Abbr} V2. T & I = Abbr
135 | ∃∃T. ↑[0,1] T ≡ T1 & tpr T U2 & I = Abbr.
137 [ elim (tpr_inv_abbr1 … H) -H * /3 width=7/
142 lemma tpr_inv_appl1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,U0. U1 = 𝕚{Appl} V1. U0 →
143 ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 &
145 | ∃∃V2,W,T1,T2. V1 ⇒ V2 & T1 ⇒ T2 &
148 | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 &
150 U0 = 𝕚{Abbr} W1. T1 &
151 U2 = 𝕚{Abbr} W2. 𝕚{Appl} V. T2.
153 [ #k #V #T #H destruct
154 | #i #V #T #H destruct
155 | #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
156 | #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /3 width=5/
157 | #V1 #V2 #W #T1 #T2 #HV12 #HT12 #V #T #H destruct -V1 T /3 width=8/
158 | #V1 #V2 #T1 #T2 #T #_ #_ #_ #V0 #T0 #H destruct
159 | #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #V0 #T0 #H
160 destruct -V1 T0 /3 width=12/
161 | #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct
162 | #V #T1 #T2 #_ #V0 #T0 #H destruct
166 lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕚{Appl} V1. U0 ⇒ U2 →
167 ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 &
169 | ∃∃V2,W,T1,T2. V1 ⇒ V2 & T1 ⇒ T2 &
172 | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 &
174 U0 = 𝕚{Abbr} W1. T1 &
175 U2 = 𝕚{Abbr} W2. 𝕚{Appl} V. T2.
178 lemma tpr_inv_cast1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Cast} V1. T1 →
179 (∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Cast} V2. T2)
182 [ #k #V #T #H destruct
183 | #i #V #T #H destruct
184 | #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
185 | #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /3 width=5/
186 | #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct
187 | #V1 #V2 #T1 #T2 #T #_ #_ #_ #V0 #T0 #H destruct
188 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct
189 | #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct
190 | #V #T1 #T2 #HT12 #V0 #T0 #H destruct -V T1 /2/
194 lemma tpr_inv_cast1: ∀V1,T1,U2. 𝕚{Cast} V1. T1 ⇒ U2 →
195 (∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Cast} V2. T2)
199 lemma tpr_inv_flat1: ∀V1,U0,U2,I. 𝕗{I} V1. U0 ⇒ U2 →
200 ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 &
202 | ∃∃V2,W,T1,T2. V1 ⇒ V2 & T1 ⇒ T2 &
204 U2 = 𝕓{Abbr} V2. T2 & I = Appl
205 | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 &
207 U0 = 𝕚{Abbr} W1. T1 &
208 U2 = 𝕚{Abbr} W2. 𝕚{Appl} V. T2 &
210 | (U0 ⇒ U2 ∧ I = Cast).
212 [ elim (tpr_inv_appl1 … H) -H * /3 width=12/
213 | elim (tpr_inv_cast1 … H) -H [1: *] /3 width=5/
217 lemma tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i →
219 | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i &
221 | ∃∃V,T. T ⇒ #i & T1 = 𝕚{Cast} V. T.
225 | #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
226 | #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
227 | #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct
228 | #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct
229 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
230 | #V #T #T1 #T2 #HT1 #HT12 #i #H destruct /3 width=6/
231 | #V #T1 #T2 #HT12 #i #H destruct /3/
235 lemma tpr_inv_lref2: ∀T1,i. T1 ⇒ #i →
237 | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i &
239 | ∃∃V,T. T ⇒ #i & T1 = 𝕗{Cast} V. T.