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/grammar/term_simple.ma".
16 include "Basic_2/substitution/tps.ma".
18 (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
20 (* Basic_1: includes: pr0_delta1 *)
21 inductive tpr: relation term ≝
22 | tpr_atom : ∀I. tpr (𝕒{I}) (𝕒{I})
23 | tpr_flat : ∀I,V1,V2,T1,T2. tpr V1 V2 → tpr T1 T2 →
24 tpr (𝕗{I} V1. T1) (𝕗{I} V2. T2)
25 | tpr_beta : ∀V1,V2,W,T1,T2.
26 tpr V1 V2 → tpr T1 T2 →
27 tpr (𝕔{Appl} V1. 𝕔{Abst} W. T1) (𝕔{Abbr} V2. T2)
28 | tpr_delta: ∀I,V1,V2,T1,T2,T.
29 tpr V1 V2 → tpr T1 T2 → ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T →
30 tpr (𝕓{I} V1. T1) (𝕓{I} V2. T)
31 | tpr_theta: ∀V,V1,V2,W1,W2,T1,T2.
32 tpr V1 V2 → ↑[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 →
33 tpr (𝕔{Appl} V1. 𝕔{Abbr} W1. T1) (𝕔{Abbr} W2. 𝕔{Appl} V. T2)
34 | tpr_zeta : ∀V,T,T1,T2. ↑[0,1] T1 ≡ T → tpr T1 T2 →
36 | tpr_tau : ∀V,T1,T2. tpr T1 T2 → tpr (𝕔{Cast} V. T1) T2
40 "context-free parallel reduction (term)"
41 'PRed T1 T2 = (tpr T1 T2).
43 (* Basic properties *********************************************************)
45 lemma tpr_bind: ∀I,V1,V2,T1,T2. V1 ⇒ V2 → T1 ⇒ T2 →
46 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2.
49 (* Basic_1: was by definition: pr0_refl *)
50 lemma tpr_refl: ∀T. T ⇒ T.
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 | #V1 #V2 #W #T1 #T2 #_ #_ #k #H destruct
62 | #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #k #H destruct
63 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #k #H destruct
64 | #V #T #T1 #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 → ∀I,V1,T1. U1 = 𝕓{I} V1. T1 →
74 (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
75 ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T &
78 ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr.
80 [ #J #I #V #T #H destruct
81 | #I1 #V1 #V2 #T1 #T2 #_ #_ #I #V #T #H destruct
82 | #V1 #V2 #W #T1 #T2 #_ #_ #I #V #T #H destruct
83 | #I1 #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #I0 #V0 #T0 #H destruct -I1 V1 T1 /3 width=7/
84 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #I0 #V0 #T0 #H destruct
85 | #V #T #T1 #T2 #HT1 #HT12 #I0 #V0 #T0 #H destruct -V T /3/
86 | #V #T1 #T2 #_ #I0 #V0 #T0 #H destruct
90 lemma tpr_inv_bind1: ∀V1,T1,U2,I. 𝕓{I} V1. T1 ⇒ U2 →
91 (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
92 ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T &
95 ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr.
98 (* Basic_1: was pr0_gen_abbr *)
99 lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕓{Abbr} V1. T1 ⇒ U2 →
100 (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
101 ⋆. 𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T &
104 ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2.
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 | ∃∃V2,W,T1,T2. V1 ⇒ V2 & T1 ⇒ T2 &
114 U2 = 𝕔{Abbr} V2. T2 & I = Appl
115 | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 &
117 U0 = 𝕔{Abbr} W1. T1 &
118 U2 = 𝕔{Abbr} W2. 𝕔{Appl} 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 -I V1 T1 /3 width=5/
124 | #V1 #V2 #W #T1 #T2 #HV12 #HT12 #J #V #T #H destruct -J V1 T /3 width=8/
125 | #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #J #V0 #T0 #H destruct
126 | #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #J #V0 #T0 #H
127 destruct -J V1 T0 /3 width=12/
128 | #V #T #T1 #T2 #_ #_ #J #V0 #T0 #H destruct
129 | #V #T1 #T2 #HT12 #J #V0 #T0 #H destruct -J V T1 /3/
133 lemma tpr_inv_flat1: ∀V1,U0,U2,I. 𝕗{I} V1. U0 ⇒ U2 →
134 ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 &
136 | ∃∃V2,W,T1,T2. V1 ⇒ V2 & T1 ⇒ T2 &
138 U2 = 𝕔{Abbr} V2. T2 & I = Appl
139 | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 &
141 U0 = 𝕔{Abbr} W1. T1 &
142 U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 &
144 | (U0 ⇒ U2 ∧ I = Cast).
147 (* Basic_1: was pr0_gen_appl *)
148 lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕔{Appl} V1. U0 ⇒ U2 →
149 ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 &
151 | ∃∃V2,W,T1,T2. V1 ⇒ V2 & T1 ⇒ T2 &
154 | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 &
156 U0 = 𝕔{Abbr} W1. T1 &
157 U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2.
159 elim (tpr_inv_flat1 … H) -H * /3 width=12/ #_ #H destruct
162 (* Note: the main property of simple terms *)
163 lemma tpr_inv_appl1_simple: ∀V1,T1,U. 𝕔{Appl} V1. T1 ⇒ U → 𝕊[T1] →
164 ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 &
167 elim (tpr_inv_appl1 … H) -H *
169 | #V2 #W #W1 #W2 #_ #_ #H #_ destruct -T1;
170 elim (simple_inv_bind … HT1)
171 | #V2 #V #W1 #W2 #U1 #U2 #_ #_ #_ #_ #H #_ destruct -T1;
172 elim (simple_inv_bind … HT1)
176 (* Basic_1: was: pr0_gen_cast *)
177 lemma tpr_inv_cast1: ∀V1,T1,U2. 𝕔{Cast} V1. T1 ⇒ U2 →
178 (∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Cast} V2. T2)
181 elim (tpr_inv_flat1 … H) -H * /3 width=5/
182 [ #V2 #W #W1 #W2 #_ #_ #_ #_ #H destruct
183 | #V2 #W #W1 #W2 #T2 #U1 #_ #_ #_ #_ #_ #_ #H destruct
187 fact tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i →
189 | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i &
191 | ∃∃V,T. T ⇒ #i & T1 = 𝕔{Cast} V. T.
193 [ #I #i #H destruct /2/
194 | #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
195 | #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct
196 | #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct
197 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
198 | #V #T #T1 #T2 #HT1 #HT12 #i #H destruct /3 width=6/
199 | #V #T1 #T2 #HT12 #i #H destruct /3/
203 lemma tpr_inv_lref2: ∀T1,i. T1 ⇒ #i →
205 | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i &
207 | ∃∃V,T. T ⇒ #i & T1 = 𝕔{Cast} V. T.
210 (* Basic_1: removed theorems 3:
211 pr0_subst0_back pr0_subst0_fwd pr0_subst0
212 Basic_1: removed local theorems: 1: pr0_delta_tau