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 (**************************************************************************)
16 include "basic_2/unfold/delift_lift.ma".
19 include "basic_2/equivalence/cpcs_cpcs.ma".
20 include "basic_2/unfold/delift_delift.ma".
24 axiom pippo1: ∀T1,V. ∃∃T2. ⓓV.T1 ➡ T2 & ⋆.ⓓV ⊢ T1 ▼*[0, 1] ≡ T2.
26 #T1 #V elim (pippo0 (⋆.ⓓV) 0 1 ? T1)
27 [ #T2 #HT12 @(ex2_1_intro … HT12)
31 axiom pippo: ∀L,V,T1. ∃∃T2. L ⊢ ⓓV.T1 ➡ T2 & L.ⓓV ⊢ T1 ▼*[0, 1] ≡ T2.
33 axiom cprs_inv_appl1_cpcs: ∀L,V1,T1,U2. L ⊢ ⓐV1. T1 ➡* U2 → (
34 ∃∃V2,T2. L ⊢ V1 ➡* V2 & L ⊢ T1 ➡* T2 &
37 ∃∃V2,W,T. L ⊢ V1 ➡* V2 &
38 L ⊢ T1 ➡* ⓛW. T & L ⊢ ⓓV2. T ⬌* U2.
39 #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
41 [ #V0 #T0 #HV10 #HT10 #HUT0
42 elim (cprs_strip … HUT0 … HU2) -U #U #H #HU2
43 elim (cpr_inv_appl1 … H) -H *
44 [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/
45 | #V2 #W2 #T #T2 #HV02 #HT2 #H1 #H2 destruct
46 lapply (cprs_strap1 … HV10 HV02) -V0 #HV12
47 lapply (cprs_div ? (ⓓV2.T) ? ? ? HU2) -HU2 /2 width=1/ /3 width=6/
48 | #V #V2 #W0 #W2 #T #T2 #HV0 #HW02 #HT2 #HV2 #H1 #H2 destruct
49 lapply (cprs_strap1 … HV10 HV0) -V0 #HV1
50 lapply (cprs_trans … HT10 (ⓓW2.T2) ?) -HT10 /2 width=1/ -W0 -T #HT1
51 elim (pippo L W2 T2) #T3 #H1T3 #H2T3
52 elim (pippo L W2 (ⓐV2.T2)) #X #H1X #H
53 elim (delift_inv_flat1 … H) -H #V3 #Y #HV23 #HY #H destruct
56 @or_introl @(ex3_2_intro … HV1 HT1) -HV1 -HT1
64 include "basic_2/computation/cprs_lcprs.ma".
65 include "basic_2/dynamic/nta.ma".
67 axiom cprs_inv_appl_abst: ∀L,V,T,W,U. L ⊢ ⓐV.T ➡* ⓛW.U →
68 ∃∃V0,W0,T0,W1,U1. ⇧[O, 1] W ≡ W1 &
70 L ⊢ V ➡* V0 & L ⊢ T ➡* ⓛW0.T0 &
73 elim (cprs_inv_appl1 … H) -H *
74 [ #V0 #T0 #_ #_ #H destruct
75 | #V0 #W0 #T0 #HV0 #HT0 #H
76 elim (cprs_inv_abbr1 … H) -H *
77 [ #V1 #T1 #_ #_ #H destruct
79 elim (lift_inv_bind1 … H) -H #W1 #U1 #HW1 #HU1 #H destruct /2 width=10/
81 | #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #H
82 elim (cprs_inv_abbr1 … H) -H *
83 [ #V3 #T3 #_ #_ #H destruct
85 elim (lift_inv_bind1 … H) -H #W3 #U3 #HW3 #HU3 #H destruct /2 width=10/
87 axiom pippo: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. L ⊢ T ➡* ⓛX.Y →
89 #h #L #T #U #H elim H -L -T -U
95 | #L #V #W #T #U #HTU #HUW #IHTU #IHUW #X #Y #HTY
96 elim (cprs_inv_appl1 … HTY) -HTY *
97 [ #V0 #T0 #_ #_ #H destruct
98 | #V0 #W0 #T0 #HV0 #HT0 #HTY
99 elim (IHTU … HT0) -IHTU -HT0 #Z #HUZ
100 elim (cprs_inv_abbr1 … HTY) -HTY *
101 [ #V1 #T1 #_ #_ #H destruct #X0
104 include "basic_2/dynamic/nta_ltpss.ma".
105 include "basic_2/dynamic/nta_thin.ma".
106 include "basic_2/dynamic/lsubn_nta.ma".
108 include "basic_2/hod/ntas_lift.ma".
111 elim (nta_inv_pure1 … HUW) -HUW #V0 #U0 #U1 #HV0 #HU0 #HU0W #HU01
116 axiom pippo_aux: ∀h,L,Z,U. ⦃h, L⦄ ⊢ Z : U → ∀Y,X. Z = ⓐY.X →
117 ∀W,T. L ⊢ X ➡* ⓛW.T → ⦃h, L⦄ ⊢ Y : W.
118 #h #L #Z #U #H elim H -L -Z -U
124 | #L #V #W #T #U #HTU #_ #_ #IHUW #Y #X #H #W0 #T0 #HX destruct
125 lapply (IHUW Y U ? ?) -IHUW -W // #T
129 axiom pippo: ∀h,L,V,X,U. ⦃h, L⦄ ⊢ ⓐV.X : U →
130 ∃∃W,T. L ⊢ X ➡* ⓛW.T & ⦃h, L⦄ ⊢ V : W.
134 (* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
136 (* Properties on context-free parallel reduction for local environments ******)
138 axiom nta_ltpr_cprs_conf: ∀h,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → ∀L2. L1 ➡ L2 →
139 ∀T2. L2 ⊢ T1 ➡* T2 → ⦃h, L2⦄ ⊢ T2 : U.
140 #h #L1 #T1 #U #H @(nta_ind_alt … H) -L1 -T1 -U
141 [ #L1 #k #L2 #_ #T2 #H
142 >(cprs_inv_sort1 … H) -H //
147 | #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #HL12 #T2 #H
148 elim (cprs_inv_appl1 … H) -H *
149 [ #V2 #T0 #HV12 #HT10 #H destruct
150 elim (nta_fwd_correct h L2 (ⓐV1.T1) (ⓐV1.U1) ?) [2: /3 width=2/ ] #U
151 @(nta_conv … (ⓐV2.U1)) (* /2 width=1/*) [ /4 width=2/] (**) (* explicit constructor, /5 width=5/ is too slow *)
152 | #V2 #W2 #T0 #HV12 #HT10 #HT02
153 lapply (IHTU1 … HL12 (ⓛW2.T0) ?) -IHTU1 /2 width=1/ -HT10 #H
154 elim (nta_inv_bind1 … H) -H #W #U0 #HW2 #HTU0 #HU01
155 elim (cpcs_inv_abst1 … HU01) -HU01 #W #U #HU1 #HU0
156 lapply (IHUW1 … HL12 (ⓐV2.ⓛW.U) ?) -IHUW1 -HL12 /2 width=1/ -HV12 #H
160 elim (nta_fwd_pure1 … H) -H #W0 #U2 #HVU2 #H #HW01
161 elim (nta_inv_bind1 … H) -H #W3 #U3 #HW3 #HU3 #H
162 elim (cpcs_inv_abst1 … H) -H #W4 #U4
165 axiom nta_ltpr_tpr_conf: ∀h,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → ∀L2. L1 ➡ L2 →
166 ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 : U.
167 #h #L1 #T1 #U #H @(nta_ind_alt … H) -L1 -T1 -U
168 [ #L1 #k #L2 #_ #T2 #H
169 >(tpr_inv_atom1 … H) -H //
170 | #L1 #K1 #V1 #W #U #i #HLK1 #_ #HWU #IHV1 #L2 #HL12 #T2 #H
171 >(tpr_inv_atom1 … H) -T2
172 elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H
173 elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=6/
174 | #L1 #K1 #W1 #V1 #U1 #i #HLK1 #HWV1 #HWU1 #IHWV1 #L2 #HL12 #T2 #H
175 >(tpr_inv_atom1 … H) -T2
176 elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H
177 elim (ltpr_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct
178 lapply (ldrop_fwd_ldrop2 … HLK2) #HLK
179 elim (lift_total V1 0 (i+1)) #W #HW
180 lapply (nta_lift h … HLK … HWU1 … HW) /2 width=1/ -HLK -HW
181 elim (lift_total W2 0 (i+1)) #U2 #HWU2
182 lapply (tpr_lift … HW12 … HWU1 … HWU2) -HWU1 #HU12
183 @(nta_conv … U2) /2 width=1/ /3 width=6/ (**) (* explicit constructor, /3 width=6/ is too slow *)
184 | #I #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #HL12 #X #H
185 elim (tpr_inv_bind1 … H) -H *
186 [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct
187 lapply (IHVW1 … HL12 … HV12) #HV2W1
188 lapply (IHVW1 L2 … V1 ?) // -IHVW1 #HWV1
189 lapply (IHTU1 (L2.ⓑ{I}V2) … HT10) -HT10 /2 width=1/ #HT0U1
190 lapply (IHTU1 (L2.ⓑ{I}V1) ? T1 ?) -IHTU1 // /2 width=1/ -HL12 #H
191 lapply (tps_lsubs_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02
192 lapply (nta_tps_conf … HT0U1 … HT02) -T0 #HT2U1
193 elim (nta_fwd_correct … H) -H #U2 #HU12
194 @(nta_conv … (ⓑ{I}V2.U1)) /2 width=2/ /3 width=1/ (**) (* explicit constructor, /4 width=6/ is too slow *)
195 | #T #HT1 #HTX #H destruct
196 lapply (IHVW1 … HL12 V1 ?) -IHVW1 // #HVW1
197 elim (lift_total X 0 1) #Y #HXY
198 lapply (tpr_lift … HTX … HT1 … HXY) -T #H
199 lapply (IHTU1 (L2.ⓓV1) … H) -T1 /2 width=1/ -L1 #H
200 elim (nta_fwd_correct … H) #T1 #HUT1
201 elim (nta_thin_conf … H L2 0 (0+1) ? ?) -H /2 width=1/ /3 width=1/ #T #U #HTU #H
202 normalize in ⊢ (??%??? → ?); #HU1
203 lapply (delift_inv_lift1_eq … H L2 … HXY) -Y /2 width=1/ #H destruct
204 @(nta_conv … U) // /2 width=2/
206 | #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #HL12 #X #H
207 elim (tpr_inv_appl1 … H) -H *
208 [ #V2 #Y #HV12 #HY #H destruct
209 elim (tpr_inv_abst1 … HY) -HY #W2 #T2 #HW12 #HT12 #H destruct
210 lapply (IHTU1 L2 ? (ⓛW1.T1) ?) // #H
211 elim (nta_fwd_correct … H) -H #X #H
212 elim (nta_inv_bind1 … H) -H #W #U #HW #HU #_
213 @(nta_conv … (ⓐV2.ⓛW1.U1)) /4 width=2/ (**) (* explicit constructor, /5 width=5/ is too slow *)
214 | #V2 #W2 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct
215 lapply (IHVW1 … HL12 … HV12) #HVW2
216 lapply (IHVW1 … HL12 V1 ?) -IHVW1 // #HV1W2
217 lapply (IHTU1 … HL12 (ⓛW2.T2) ?) -IHTU1 -HL12 /2 width=1/ -HT02 #H1
218 elim (nta_fwd_correct … H1) #T #H2
219 elim (nta_inv_bind1 … H1) -H1 #W #U2 #HW2 #HTU2 #H
220 elim (cpcs_inv_abst … H Abst W2) -H #_ #HU21
221 elim (nta_inv_bind1 … H2) -H2 #W0 #U0 #_ #H #_ -T -W0
222 lapply (lsubn_nta_trans … HTU2 (L2.ⓓV2) ?) -HTU2 /2 width=1/ #HTU2
223 @(nta_conv … (ⓓV2.U2)) /2 width=2/ /3 width=2/ (**) (* explicit constructor, /4 width=5/ is too slow *)
224 | #V0 #V2 #W0 #W2 #T0 #T2 #_ #_ #_ #_ #H destruct
226 | #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #HL12 #X #H
227 elim (tpr_inv_appl1 … H) -H *
228 [ #V2 #T2 #HV12 #HT12 #H destruct
229 elim (nta_fwd_correct h L2 (ⓐV1.T1) (ⓐV1.U1) ?) [2: /3 width=2/ ] #U
230 @(nta_conv … (ⓐV2.U1)) /2 width=1/ /4 width=2/ (**) (* explicit constructor, /5 width=5/ is too slow *)
231 | #V2 #W2 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct
232 lapply (IHTU1 … HL12 (ⓛW2.T2) ?) -IHTU1 /2 width=1/ -T0 #H
233 elim (nta_inv_bind1 … H) -H #W #U2 #HW2 #HTU2 #HU21
234 lapply (IHUW1 … HL12 (ⓐV2.U1) ?) -IHUW1 -HL12 /2 width=1/ #H
235 elim (nta_inv_pure1 … H) -H #V0 #U0 #U #HV20 #HU10 #HU0W1 #HU0
236 @(nta_conv … (ⓓV2.U2))
238 @(lsubn_nta_trans … HTU2) @lsubn_abbr //
240 lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HB
241 lapply (IH … HB0 … HL12 W2 ?) -HB0 /width=5/ #HB0
242 lapply (IH … HA0 … (L2.ⓛW2) … HT02) -IH -HA0 -HT02 /width=5/ -T0 /2 width=1/ -L1 -V1 /4 width=7/
246 axiom pippo: ⦃h, L⦄ ⊢ ⓐV.X : Y →
247 ∃∃W,T. L ⊢ X ➡* ⓛW.T & ⦃h, L⦄ ⊢ ⓐV : W.
251 | #L1 #T1 #U1 #W1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL12 #X #H
252 elim (tpss_inv_flat1 … H) -H #U2 #T2 #HU12 #HT12 #H destruct
253 lapply (cpr_tpss … HU12) /4 width=4/
254 | #L1 #T1 #U11 #U12 #U #_ #HU112 #_ #IHTU11 #IHU12 #L2 #d #e #HL12 #T2 #HT12
255 @(nta_conv … U11) /2 width=5/ (**) (* explicot constructor, /3 width=7/ is too slow *)
261 fact nta_ltpr_tpr_conf_aux: ∀h,L,T,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → L = L1 → T = T1 →
262 ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 : U.
265 | #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct
266 elim (nta_inv_abbr … HT1) -HT1 #B0 #HW0 #HT0
267 lapply (IH … HW0 … HL12 … HW02) -HW0 /width=5/ #HW2
268 lapply (IH … HV1 … HL12 … HV10) -HV1 -HV10 /width=5/ #HV0
269 lapply (IH … HT0 … (L2.ⓓW2) … HT02) -IH -HT0 -HT02 /width=5/ -V1 -T0 /2 width=1/ -L1 -W0 #HT2
270 @(nta_abbr … HW2) -HW2
271 @(nta_appl … HT2) -HT2 /3 width=7/ (**) (* explict constructors, /5 width=7/ is too slow *)
273 | #L1 #V1 #T1 #A #HV1 #HT1 #H1 #H2 #L2 #HL12 #X #H destruct
274 elim (tpr_inv_cast1 … H) -H
275 [ * #V2 #T2 #HV12 #HT12 #H destruct
276 lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HV2
277 lapply (IH … HT1 … HL12 … HT12) -IH -HT1 -HL12 -HT12 /width=5/ -L1 -V1 -T1 /2 width=1/
279 lapply (IH … HT1 … HL12 … HT1X) -IH -HT1 -HL12 -HT1X /width=5/
286 axiom nta_ltpr_conf: ∀L1,T,A. L1 ⊢ T : A → ∀L2. L1 ➡ L2 → L2 ⊢ T : A.
289 axiom nta_tpr_conf: ∀L,T1,A. L ⊢ T1 : A → ∀T2. T1 ➡ T2 → L ⊢ T2 : A.