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 include "basic_2/substitution/tps.ma".
17 (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
19 (* Basic_1: includes: pr0_delta1 *)
20 inductive tpr: relation term ≝
21 | tpr_atom : ∀I. tpr (⓪{I}) (⓪{I})
22 | tpr_flat : ∀I,V1,V2,T1,T2. tpr V1 V2 → tpr T1 T2 →
23 tpr (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
24 | tpr_beta : ∀V1,V2,W,T1,T2.
25 tpr V1 V2 → tpr T1 T2 → tpr (ⓐV1. ⓛW. T1) (ⓓV2. T2)
26 | tpr_delta: ∀I,V1,V2,T1,T2,T.
27 tpr V1 V2 → tpr T1 T2 → ⋆. ⓑ{I} V2 ⊢ T2 ▶ [0, 1] T →
28 tpr (ⓑ{I} V1. T1) (ⓑ{I} 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 (ⓐV1. ⓓW1. T1) (ⓓW2. ⓐV. T2)
32 | tpr_zeta : ∀V,T,T1,T2. ⇧[0,1] T1 ≡ T → tpr T1 T2 → tpr (ⓓV. T) T2
33 | tpr_tau : ∀V,T1,T2. tpr T1 T2 → tpr (ⓝV. T1) T2
37 "context-free parallel reduction (term)"
38 'PRed T1 T2 = (tpr T1 T2).
40 (* Basic properties *********************************************************)
42 lemma tpr_bind: ∀I,V1,V2,T1,T2. V1 ➡ V2 → T1 ➡ T2 → ⓑ{I} V1. T1 ➡ ⓑ{I} V2. T2.
45 (* Basic_1: was by definition: pr0_refl *)
46 lemma tpr_refl: ∀T. T ➡ T.
48 #I elim I -I /2 width=1/
51 (* Basic inversion lemmas ***************************************************)
53 fact tpr_inv_atom1_aux: ∀U1,U2. U1 ➡ U2 → ∀I. U1 = ⓪{I} → U2 = ⓪{I}.
56 | #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
57 | #V1 #V2 #W #T1 #T2 #_ #_ #k #H destruct
58 | #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #k #H destruct
59 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #k #H destruct
60 | #V #T #T1 #T2 #_ #_ #k #H destruct
61 | #V #T1 #T2 #_ #k #H destruct
65 (* Basic_1: was: pr0_gen_sort pr0_gen_lref *)
66 lemma tpr_inv_atom1: ∀I,U2. ⓪{I} ➡ U2 → U2 = ⓪{I}.
69 fact tpr_inv_bind1_aux: ∀U1,U2. U1 ➡ U2 → ∀I,V1,T1. U1 = ⓑ{I} V1. T1 →
70 (∃∃V2,T2,T. V1 ➡ V2 & T1 ➡ T2 &
71 ⋆. ⓑ{I} V2 ⊢ T2 ▶ [0, 1] T &
74 ∃∃T. ⇧[0,1] T ≡ T1 & T ➡ U2 & I = Abbr.
76 [ #J #I #V #T #H destruct
77 | #I1 #V1 #V2 #T1 #T2 #_ #_ #I #V #T #H destruct
78 | #V1 #V2 #W #T1 #T2 #_ #_ #I #V #T #H destruct
79 | #I1 #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #I0 #V0 #T0 #H destruct /3 width=7/
80 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #I0 #V0 #T0 #H destruct
81 | #V #T #T1 #T2 #HT1 #HT12 #I0 #V0 #T0 #H destruct /3 width=3/
82 | #V #T1 #T2 #_ #I0 #V0 #T0 #H destruct
86 lemma tpr_inv_bind1: ∀V1,T1,U2,I. ⓑ{I} V1. T1 ➡ U2 →
87 (∃∃V2,T2,T. V1 ➡ V2 & T1 ➡ T2 &
88 ⋆. ⓑ{I} V2 ⊢ T2 ▶ [0, 1] T &
91 ∃∃T. ⇧[0,1] T ≡ T1 & T ➡ U2 & I = Abbr.
94 (* Basic_1: was pr0_gen_abbr *)
95 lemma tpr_inv_abbr1: ∀V1,T1,U2. ⓓV1. T1 ➡ U2 →
96 (∃∃V2,T2,T. V1 ➡ V2 & T1 ➡ T2 &
97 ⋆. ⓓV2 ⊢ T2 ▶ [0, 1] T &
100 ∃∃T. ⇧[0,1] T ≡ T1 & T ➡ U2.
102 elim (tpr_inv_bind1 … H) -H * /3 width=7/
105 fact tpr_inv_flat1_aux: ∀U1,U2. U1 ➡ U2 → ∀I,V1,U0. U1 = ⓕ{I} V1. U0 →
106 ∨∨ ∃∃V2,T2. V1 ➡ V2 & U0 ➡ T2 &
108 | ∃∃V2,W,T1,T2. V1 ➡ V2 & T1 ➡ T2 &
110 U2 = ⓓV2. T2 & I = Appl
111 | ∃∃V2,V,W1,W2,T1,T2. V1 ➡ V2 & W1 ➡ W2 & T1 ➡ T2 &
116 | (U0 ➡ U2 ∧ I = Cast).
118 [ #I #J #V #T #H destruct
119 | #I #V1 #V2 #T1 #T2 #HV12 #HT12 #J #V #T #H destruct /3 width=5/
120 | #V1 #V2 #W #T1 #T2 #HV12 #HT12 #J #V #T #H destruct /3 width=8/
121 | #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #J #V0 #T0 #H destruct
122 | #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #J #V0 #T0 #H destruct /3 width=12/
123 | #V #T #T1 #T2 #_ #_ #J #V0 #T0 #H destruct
124 | #V #T1 #T2 #HT12 #J #V0 #T0 #H destruct /3 width=1/
128 lemma tpr_inv_flat1: ∀V1,U0,U2,I. ⓕ{I} V1. U0 ➡ U2 →
129 ∨∨ ∃∃V2,T2. V1 ➡ V2 & U0 ➡ T2 &
131 | ∃∃V2,W,T1,T2. V1 ➡ V2 & T1 ➡ T2 &
133 U2 = ⓓV2. T2 & I = Appl
134 | ∃∃V2,V,W1,W2,T1,T2. V1 ➡ V2 & W1 ➡ W2 & T1 ➡ T2 &
139 | (U0 ➡ U2 ∧ I = Cast).
142 (* Basic_1: was pr0_gen_appl *)
143 lemma tpr_inv_appl1: ∀V1,U0,U2. ⓐV1. U0 ➡ U2 →
144 ∨∨ ∃∃V2,T2. V1 ➡ V2 & U0 ➡ T2 &
146 | ∃∃V2,W,T1,T2. V1 ➡ V2 & T1 ➡ T2 &
149 | ∃∃V2,V,W1,W2,T1,T2. V1 ➡ V2 & W1 ➡ W2 & T1 ➡ T2 &
154 elim (tpr_inv_flat1 … H) -H * /3 width=12/ #_ #H destruct
157 (* Note: the main property of simple terms *)
158 lemma tpr_inv_appl1_simple: ∀V1,T1,U. ⓐV1. T1 ➡ U → 𝐒⦃T1⦄ →
159 ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 &
162 elim (tpr_inv_appl1 … H) -H *
164 | #V2 #W #W1 #W2 #_ #_ #H #_ destruct
165 elim (simple_inv_bind … HT1)
166 | #V2 #V #W1 #W2 #U1 #U2 #_ #_ #_ #_ #H #_ destruct
167 elim (simple_inv_bind … HT1)
171 (* Basic_1: was: pr0_gen_cast *)
172 lemma tpr_inv_cast1: ∀V1,T1,U2. ⓝV1. T1 ➡ U2 →
173 (∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = ⓝV2. T2)
176 elim (tpr_inv_flat1 … H) -H * /3 width=5/
177 [ #V2 #W #W1 #W2 #_ #_ #_ #_ #H destruct
178 | #V2 #W #W1 #W2 #T2 #U1 #_ #_ #_ #_ #_ #_ #H destruct
182 fact tpr_inv_lref2_aux: ∀T1,T2. T1 ➡ T2 → ∀i. T2 = #i →
184 | ∃∃V,T,T0. ⇧[O,1] T0 ≡ T & T0 ➡ #i &
186 | ∃∃V,T. T ➡ #i & T1 = ⓝV. T.
188 [ #I #i #H destruct /2 width=1/
189 | #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
190 | #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct
191 | #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct
192 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
193 | #V #T #T1 #T2 #HT1 #HT12 #i #H destruct /3 width=6/
194 | #V #T1 #T2 #HT12 #i #H destruct /3 width=4/
198 lemma tpr_inv_lref2: ∀T1,i. T1 ➡ #i →
200 | ∃∃V,T,T0. ⇧[O,1] T0 ≡ T & T0 ➡ #i &
202 | ∃∃V,T. T ➡ #i & T1 = ⓝV. T.
205 (* Basic_1: removed theorems 3:
206 pr0_subst0_back pr0_subst0_fwd pr0_subst0
207 Basic_1: removed local theorems: 1: pr0_delta_tau