1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 notation "hvbox( T1 ➡ break term 46 T2 )"
16 non associative with precedence 45
17 for @{ 'PRed $T1 $T2 }.
19 include "basic_2/substitution/tps.ma".
21 (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
23 (* Basic_1: includes: pr0_delta1 *)
24 inductive tpr: relation term ≝
25 | tpr_atom : ∀I. tpr (⓪{I}) (⓪{I})
26 | tpr_flat : ∀I,V1,V2,T1,T2. tpr V1 V2 → tpr T1 T2 →
27 tpr (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
28 | tpr_beta : ∀a,V1,V2,W,T1,T2.
29 tpr V1 V2 → tpr T1 T2 → tpr (ⓐV1. ⓛ{a}W. T1) (ⓓ{a}V2. T2)
30 | tpr_delta: ∀a,I,V1,V2,T1,T,T2.
31 tpr V1 V2 → tpr T1 T → ⋆. ⓑ{I} V2 ⊢ T ▶ [0, 1] T2 →
32 tpr (ⓑ{a,I} V1. T1) (ⓑ{a,I} V2. T2)
33 | tpr_theta: ∀a,V,V1,V2,W1,W2,T1,T2.
34 tpr V1 V2 → ⇧[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 →
35 tpr (ⓐV1. ⓓ{a}W1. T1) (ⓓ{a}W2. ⓐV. T2)
36 | tpr_zeta : ∀V,T1,T,T2. tpr T1 T → ⇧[0, 1] T2 ≡ T → tpr (+ⓓV. T1) T2
37 | tpr_tau : ∀V,T1,T2. tpr T1 T2 → tpr (ⓝV. T1) T2
41 "context-free parallel reduction (term)"
42 'PRed T1 T2 = (tpr T1 T2).
44 (* Basic properties *********************************************************)
46 lemma tpr_bind: ∀a,I,V1,V2,T1,T2. V1 ➡ V2 → T1 ➡ T2 → ⓑ{a,I} V1. T1 ➡ ⓑ{a,I} V2. T2.
49 (* Basic_1: was by definition: pr0_refl *)
50 lemma tpr_refl: reflexive … tpr.
52 #I elim I -I /2 width=1/
55 (* Basic inversion lemmas ***************************************************)
57 fact tpr_inv_atom1_aux: ∀U1,U2. U1 ➡ U2 → ∀I. U1 = ⓪{I} → U2 = ⓪{I}.
60 | #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
61 | #a #V1 #V2 #W #T1 #T2 #_ #_ #k #H destruct
62 | #a #I #V1 #V2 #T1 #T #T2 #_ #_ #_ #k #H destruct
63 | #a #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #k #H destruct
64 | #V #T1 #T #T2 #_ #_ #k #H destruct
65 | #V #T1 #T2 #_ #k #H destruct
69 (* Basic_1: was: pr0_gen_sort pr0_gen_lref *)
70 lemma tpr_inv_atom1: ∀I,U2. ⓪{I} ➡ U2 → U2 = ⓪{I}.
73 fact tpr_inv_bind1_aux: ∀U1,U2. U1 ➡ U2 → ∀a,I,V1,T1. U1 = ⓑ{a,I} V1. T1 →
74 (∃∃V2,T,T2. V1 ➡ V2 & T1 ➡ T &
75 ⋆. ⓑ{I} V2 ⊢ T ▶ [0, 1] T2 &
78 ∃∃T. T1 ➡ T & ⇧[0, 1] U2 ≡ T & a = true & I = Abbr.
80 [ #J #a #I #V #T #H destruct
81 | #I1 #V1 #V2 #T1 #T2 #_ #_ #a #I #V #T #H destruct
82 | #b #V1 #V2 #W #T1 #T2 #_ #_ #a #I #V #T #H destruct
83 | #b #I1 #V1 #V2 #T1 #T #T2 #HV12 #HT1 #HT2 #a #I0 #V0 #T0 #H destruct /3 width=7/
84 | #b #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #a #I0 #V0 #T0 #H destruct
85 | #V #T1 #T #T2 #HT1 #HT2 #a #I0 #V0 #T0 #H destruct /3 width=3/
86 | #V #T1 #T2 #_ #a #I0 #V0 #T0 #H destruct
90 lemma tpr_inv_bind1: ∀V1,T1,U2,a,I. ⓑ{a,I} V1. T1 ➡ U2 →
91 (∃∃V2,T,T2. V1 ➡ V2 & T1 ➡ T &
92 ⋆. ⓑ{I} V2 ⊢ T ▶ [0, 1] T2 &
95 ∃∃T. T1 ➡ T & ⇧[0,1] U2 ≡ T & a = true & I = Abbr.
98 (* Basic_1: was pr0_gen_abbr *)
99 lemma tpr_inv_abbr1: ∀a,V1,T1,U2. ⓓ{a}V1. T1 ➡ U2 →
100 (∃∃V2,T,T2. V1 ➡ V2 & T1 ➡ T &
101 ⋆. ⓓV2 ⊢ T ▶ [0, 1] T2 &
104 ∃∃T. T1 ➡ T & ⇧[0, 1] U2 ≡ T & a = true.
106 elim (tpr_inv_bind1 … H) -H * /3 width=7/
109 fact tpr_inv_flat1_aux: ∀U1,U2. U1 ➡ U2 → ∀I,V1,U0. U1 = ⓕ{I} V1. U0 →
110 ∨∨ ∃∃V2,T2. V1 ➡ V2 & U0 ➡ T2 &
112 | ∃∃a,V2,W,T1,T2. V1 ➡ V2 & T1 ➡ T2 &
114 U2 = ⓓ{a}V2. T2 & I = Appl
115 | ∃∃a,V2,V,W1,W2,T1,T2. V1 ➡ V2 & W1 ➡ W2 & T1 ➡ T2 &
118 U2 = ⓓ{a}W2. ⓐV. T2 &
120 | (U0 ➡ U2 ∧ I = Cast).
122 [ #I #J #V #T #H destruct
123 | #I #V1 #V2 #T1 #T2 #HV12 #HT12 #J #V #T #H destruct /3 width=5/
124 | #a #V1 #V2 #W #T1 #T2 #HV12 #HT12 #J #V #T #H destruct /3 width=9/
125 | #a #I #V1 #V2 #T1 #T #T2 #_ #_ #_ #J #V0 #T0 #H destruct
126 | #a #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #J #V0 #T0 #H destruct /3 width=13/
127 | #V #T1 #T #T2 #_ #_ #J #V0 #T0 #H destruct
128 | #V #T1 #T2 #HT12 #J #V0 #T0 #H destruct /3 width=1/
132 lemma tpr_inv_flat1: ∀V1,U0,U2,I. ⓕ{I} V1. U0 ➡ U2 →
133 ∨∨ ∃∃V2,T2. V1 ➡ V2 & U0 ➡ T2 &
135 | ∃∃a,V2,W,T1,T2. V1 ➡ V2 & T1 ➡ T2 &
137 U2 = ⓓ{a}V2. T2 & I = Appl
138 | ∃∃a,V2,V,W1,W2,T1,T2. V1 ➡ V2 & W1 ➡ W2 & T1 ➡ T2 &
141 U2 = ⓓ{a}W2. ⓐV. T2 &
143 | (U0 ➡ U2 ∧ I = Cast).
146 (* Basic_1: was pr0_gen_appl *)
147 lemma tpr_inv_appl1: ∀V1,U0,U2. ⓐV1. U0 ➡ U2 →
148 ∨∨ ∃∃V2,T2. V1 ➡ V2 & U0 ➡ T2 &
150 | ∃∃a,V2,W,T1,T2. V1 ➡ V2 & T1 ➡ T2 &
153 | ∃∃a,V2,V,W1,W2,T1,T2. V1 ➡ V2 & W1 ➡ W2 & T1 ➡ T2 &
158 elim (tpr_inv_flat1 … H) -H *
159 /3 width=5/ /3 width=9/ /3 width=13/
163 (* Note: the main property of simple terms *)
164 lemma tpr_inv_appl1_simple: ∀V1,T1,U. ⓐV1. T1 ➡ U → 𝐒⦃T1⦄ →
165 ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 &
168 elim (tpr_inv_appl1 … H) -H *
170 | #a #V2 #W #W1 #W2 #_ #_ #H #_ destruct
171 elim (simple_inv_bind … HT1)
172 | #a #V2 #V #W1 #W2 #U1 #U2 #_ #_ #_ #_ #H #_ destruct
173 elim (simple_inv_bind … HT1)
177 (* Basic_1: was: pr0_gen_cast *)
178 lemma tpr_inv_cast1: ∀V1,T1,U2. ⓝV1. T1 ➡ U2 →
179 (∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = ⓝV2. T2)
182 elim (tpr_inv_flat1 … H) -H * /3 width=5/ #a #V2 #W #W1 #W2
183 [ #_ #_ #_ #_ #H destruct
184 | #T2 #U1 #_ #_ #_ #_ #_ #_ #H destruct
188 fact tpr_inv_lref2_aux: ∀T1,T2. T1 ➡ T2 → ∀i. T2 = #i →
190 | ∃∃V,T. T ➡ #(i+1) & T1 = +ⓓV. T
191 | ∃∃V,T. T ➡ #i & T1 = ⓝV. T.
193 [ #I #i #H destruct /2 width=1/
194 | #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
195 | #a #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct
196 | #a #I #V1 #V2 #T1 #T #T2 #_ #_ #_ #i #H destruct
197 | #a #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
198 | #V #T1 #T #T2 #HT1 #HT2 #i #H destruct
199 lapply (lift_inv_lref1_ge … HT2 ?) -HT2 // #H destruct /3 width=4/
200 | #V #T1 #T2 #HT12 #i #H destruct /3 width=4/
204 lemma tpr_inv_lref2: ∀T1,i. T1 ➡ #i →
206 | ∃∃V,T. T ➡ #(i+1) & T1 = +ⓓV. T
207 | ∃∃V,T. T ➡ #i & T1 = ⓝV. T.
210 (* Basic forward lemmas *****************************************************)
212 lemma tpr_fwd_bind1_minus: ∀I,V1,T1,T. -ⓑ{I}V1.T1 ➡ T → ∀b.
213 ∃∃V2,T2. ⓑ{b,I}V1.T1 ➡ ⓑ{b,I}V2.T2 &
215 #I #V1 #T1 #T #H #b elim (tpr_inv_bind1 … H) -H *
216 [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct /3 width=4/
217 | #T2 #_ #_ #H destruct
221 lemma tpr_fwd_shift1: ∀L1,T1,T. L1 @@ T1 ➡ T →
222 ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2.
223 #L1 @(lenv_ind_dx … L1) -L1 normalize
225 @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *)
226 | #I #L1 #V1 #IH #T1 #X
227 >shift_append_assoc normalize #H
228 elim (tpr_inv_bind1 … H) -H *
229 [ #V0 #T0 #X0 #_ #HT10 #H0 #H destruct
230 elim (IH … HT10) -IH -T1 #L #T #HL1 #H destruct
231 elim (tps_fwd_shift1 … H0) -T #L2 #T2 #HL2 #H destruct
232 >append_length >HL1 >HL2 -L1 -L
233 @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] // /2 width=3/ (**) (* explicit constructor *)
234 | #T #_ #_ #H destruct
239 (* Basic_1: removed theorems 3:
240 pr0_subst0_back pr0_subst0_fwd pr0_subst0
242 (* Basic_1: removed local theorems: 1: pr0_delta_tau *)