11 Section ty0_fsubst0. (****************************************************)
15 Tactic Definition IH H0 v1 v2 v3 v4 v5 :=
16 LApply (H0 v1 v2 v3 v4); [ Intros H_x | XEAuto ];
17 LApply H_x; [ Clear H_x; Intros H_x | XEAuto ];
18 LApply (H_x v5); [ Clear H_x; Intros | XEAuto ].
20 Tactic Definition IHT :=
22 [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 ?1 ?2 c2 t2) ->
24 (e:C) (drop i (0) ?1 (CTail e (Bind Abbr) u0)) -> ?;
25 _: (subst0 ?4 ?5 ?2 ?6);
26 _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
29 Tactic Definition IHTb1 :=
31 [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
33 (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
34 _: (subst0 ?4 ?5 ?10 ?6);
35 _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
36 IH H '(S ?4) ?5 '(CTail ?1 (Bind ?11) ?6) ?2 ?9.
38 Tactic Definition IHTb2 :=
40 [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
42 (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
43 _: (subst0 (s (Bind ?11) ?4) ?5 ?2 ?6);
44 _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
45 IH H '(S ?4) ?5 '(CTail ?1 (Bind ?11) ?10) ?6 ?9.
47 Tactic Definition IHC :=
49 [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 ?1 ?2 c2 t2) ->
51 (e:C) (drop i (0) ?1 (CTail e (Bind Abbr) u0)) -> ?;
52 _: (csubst0 ?4 ?5 ?1 ?6);
53 _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
56 Tactic Definition IHCb :=
58 [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
60 (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
61 _: (csubst0 ?4 ?5 ?1 ?6);
62 _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
63 IH H '(S ?4) ?5 '(CTail ?6 (Bind ?11) ?10) ?2 ?9.
65 Tactic Definition IHTTb :=
67 [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
69 (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
70 _: (subst0 ?4 ?5 ?10 ?6);
71 _: (subst0 (s (Bind ?11) ?4) ?5 ?2 ?7);
72 _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
73 IH H '(S ?4) ?5 '(CTail ?1 (Bind ?11) ?6) ?7 ?9.
75 Tactic Definition IHCT :=
77 [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 ?1 ?2 c2 t2) ->
79 (e:C) (drop i (0) ?1 (CTail e (Bind Abbr) u0)) -> ?;
80 _: (csubst0 ?4 ?5 ?1 ?6);
81 _: (subst0 ?4 ?5 ?2 ?7);
82 _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
85 Tactic Definition IHCTb1 :=
87 [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
89 (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
90 _: (csubst0 ?4 ?5 ?1 ?6);
91 _: (subst0 ?4 ?5 ?10 ?7);
92 _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
93 IH H '(S ?4) ?5 '(CTail ?6 (Bind ?11) ?7) ?2 ?9.
95 Tactic Definition IHCTb2 :=
97 [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
99 (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
100 _: (csubst0 ?4 ?5 ?1 ?6);
101 _: (subst0 (s (Bind ?11) ?4) ?5 ?2 ?7);
102 _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
103 IH H '(S ?4) ?5 '(CTail ?6 (Bind ?11) ?10) ?7 ?9.
105 Tactic Definition IHCTTb :=
107 [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
109 (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
110 _: (csubst0 ?4 ?5 ?1 ?6);
111 _: (subst0 ?4 ?5 ?10 ?7);
112 _: (subst0 (s (Bind ?11) ?4) ?5 ?2 ?8);
113 _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
114 IH H '(S ?4) ?5 '(CTail ?6 (Bind ?11) ?7) ?8 ?9.
118 (*#* #caption "substitution preserves types" *)
119 (*#* #cap #cap c1, c2, e, t1, t2, t #alpha u in V *)
121 (* NOTE: This breaks the mutual recursion between ty0_subst0 and ty0_csubst0 *)
122 Theorem ty0_fsubst0: (g:?; c1:?; t1,t:?) (ty0 g c1 t1 t) ->
123 (i:?; u,c2,t2:?) (fsubst0 i u c1 t1 c2 t2) ->
125 (e:?) (drop i (0) c1 (CTail e (Bind Abbr) u)) ->
130 Intros until 1; XElim H.
131 (* case 1: ty0_conv *)
132 Intros until 6; XElim H4; Intros.
133 (* case 1.1: fsubst0_snd *)
134 IHT; EApply ty0_conv; XEAuto.
135 (* case 1.2: fsubst0_fst *)
136 IHC; EApply ty0_conv; Try EApply pc3_fsubst0; XEAuto.
137 (* case 1.3: fsubst0_both *)
138 IHCT; IHCT; EApply ty0_conv; Try EApply pc3_fsubst0; XEAuto.
139 (* case 2: ty0_sort *)
140 Intros until 2; XElim H0; Intros.
141 (* case 2.1: fsubst0_snd *)
143 (* case 2.2: fsubst0_fst *)
145 (* case 2.3: fsubst0_both *)
147 (* case 3: ty0_abbr *)
148 Intros until 5; XElim H3; Intros; Clear c1 c2 t t1 t2.
149 (* case 3.1: fsubst0_snd *)
150 Subst0GenBase; Rewrite H6; Rewrite <- H3 in H5; Clear H3 H6 i t3.
151 DropDis; Inversion H5; Rewrite <- H6 in H0; Rewrite H7 in H1; XEAuto.
152 (* case 3.2: fsubst0_fst *)
153 Apply (lt_le_e n i); Intros; CSubst0Drop.
154 (* case 3.2.1: n < i, none *)
155 EApply ty0_abbr; XEAuto.
156 (* case 3.2.2: n < i, csubst0_snd *)
157 Inversion H0; CSubst0Drop.
158 Rewrite <- H10 in H7; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H8;
159 Clear H0 H10 H11 H12 x0 x1 x2.
160 DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase | XAuto ].
161 IHT; EApply ty0_abbr; XEAuto.
162 (* case 3.2.3: n < i, csubst0_fst *)
163 Inversion H0; CSubst0Drop.
164 Rewrite <- H10 in H8; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H7;
165 Clear H0 H10 H11 H12 x0 x1 x3.
166 DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase; CSubst0Drop | XAuto ].
167 IHC; EApply ty0_abbr; XEAuto.
168 (* case 3.2.4: n < i, csubst0_both *)
169 Inversion H0; CSubst0Drop.
170 Rewrite <- H11 in H9; Rewrite <- H12 in H7; Rewrite <- H12 in H8; Rewrite <- H12 in H9; Rewrite <- H13 in H8;
171 Clear H0 H11 H12 H13 x0 x1 x3.
172 DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase; CSubst0Drop | XAuto ].
173 IHCT; EApply ty0_abbr; XEAuto.
174 (* case 3.2.5: n >= i *)
175 EApply ty0_abbr; XEAuto.
176 (* case 3.3: fsubst0_both *)
177 Subst0GenBase; Rewrite H7; Rewrite <- H3 in H4; Rewrite <- H3 in H6; Clear H3 H7 i t3.
178 DropDis; Inversion H6; Rewrite <- H7 in H0; Rewrite H8 in H1.
180 (* case 4: ty0_abst *)
181 Intros until 5; XElim H3; Intros; Clear c1 c2 t t1 t2.
182 (* case 4.1: fsubst0_snd *)
183 Subst0GenBase; Rewrite H3 in H0; DropDis; Inversion H0.
184 (* case 4.2: fsubst0_fst *)
185 Apply (lt_le_e n i); Intros; CSubst0Drop.
186 (* case 4.2.1: n < i, none *)
187 EApply ty0_abst; XEAuto.
188 (* case 4.2.2: n < i, csubst0_snd *)
189 Inversion H0; CSubst0Drop.
190 Rewrite <- H10 in H7; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H8; Rewrite <- H12;
191 Clear H0 H10 H11 H12 x0 x1 x2.
192 DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase | XAuto ].
193 IHT; EApply ty0_conv;
194 [ EApply ty0_lift | EApply ty0_abst | EApply pc3_lift ]; XEAuto.
195 (* case 4.2.3: n < i, csubst0_fst *)
196 Inversion H0; CSubst0Drop.
197 Rewrite <- H10 in H8; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H7; Rewrite <- H12;
198 Clear H0 H10 H11 H12 x0 x1 x3.
199 DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase; CSubst0Drop | XAuto ].
200 IHC; EApply ty0_abst; XEAuto.
201 (* case 4.2.4: n < i, csubst0_both *)
202 Inversion H0; CSubst0Drop.
203 Rewrite <- H11 in H9; Rewrite <- H12 in H7; Rewrite <- H12 in H8; Rewrite <- H12 in H9; Rewrite <- H13 in H8; Rewrite <- H13;
204 Clear H0 H11 H12 H13 x0 x1 x3.
205 DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase; CSubst0Drop | XAuto ].
206 IHCT; IHC; EApply ty0_conv;
207 [ EApply ty0_lift | EApply ty0_abst
208 | EApply pc3_lift; Try EApply pc3_fsubst0; Try Apply H0
210 (* case 4.2.4: n >= i *)
211 EApply ty0_abst; XEAuto.
212 (* case 4.3: fsubst0_both *)
213 Subst0GenBase; Rewrite H3 in H0; DropDis; Inversion H0.
214 (* case 5: ty0_bind *)
215 Intros until 7; XElim H5; Intros; Clear H4.
216 (* case 5.1: fsubst0_snd *)
217 Subst0GenBase; Rewrite H4; Clear H4 t6.
218 (* case 5.1.1: subst0 on left argument *)
219 Ty0Correct; IHT; IHTb1; Ty0Correct.
221 [ EApply ty0_bind | EApply ty0_bind | EApply pc3_fsubst0 ]; XEAuto.
222 (* case 5.1.2: subst0 on right argument *)
223 IHTb2; Ty0Correct; EApply ty0_bind; XEAuto.
224 (* case 5.1.3: subst0 on both arguments *)
225 Ty0Correct; IHT; IHTb1; IHTTb; Ty0Correct.
227 [ EApply ty0_bind | EApply ty0_bind | EApply pc3_fsubst0 ]; XEAuto.
228 (* case 5.2: fsubst0_fst *)
229 IHC; IHCb; Ty0Correct; EApply ty0_bind; XEAuto.
230 (* case 5.3: fsubst0_both *)
231 Subst0GenBase; Rewrite H4; Clear H4 t6.
232 (* case 5.3.1: subst0 on left argument *)
233 IHC; IHCb; Ty0Correct; Ty0Correct; IHCT; IHCTb1; Ty0Correct.
235 [ EApply ty0_bind | EApply ty0_bind
236 | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
237 (* case 5.3.2: subst0 on right argument *)
238 IHC; IHCTb2; Ty0Correct; EApply ty0_bind; XEAuto.
239 (* case 5.3.3: subst0 on both arguments *)
240 IHC; IHCb; Ty0Correct; Ty0Correct; IHCT; IHCTTb; Ty0Correct.
242 [ EApply ty0_bind | EApply ty0_bind
243 | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
244 (* case 6: ty0_appl *)
245 Intros until 5; XElim H3; Intros.
246 (* case 6.1: fsubst0_snd *)
247 Subst0GenBase; Rewrite H3; Clear H3 c1 c2 t t1 t2 t3.
248 (* case 6.1.1: subst0 on left argument *)
249 Ty0Correct; Ty0GenBase; IHT; Ty0Correct.
251 [ EApply ty0_appl | EApply ty0_appl | EApply pc3_fsubst0 ]; XEAuto.
252 (* case 6.1.2: subst0 on right argument *)
253 IHT; EApply ty0_appl; XEAuto.
254 (* case 6.1.3: subst0 on both arguments *)
255 Ty0Correct; Ty0GenBase; Move H after H10; Ty0Correct; IHT; Clear H2; IHT.
257 [ EApply ty0_appl | EApply ty0_appl | EApply pc3_fsubst0 ]; XEAuto.
258 (* case 6.2: fsubst0_fst *)
259 IHC; Clear H2; IHC; EApply ty0_appl; XEAuto.
260 (* case 6.3: fsubst0_both *)
261 Subst0GenBase; Rewrite H3; Clear H3 c1 c2 t t1 t2 t3.
262 (* case 6.3.1: subst0 on left argument *)
263 IHC; Ty0Correct; Ty0GenBase; Clear H2; IHC; IHCT.
265 [ EApply ty0_appl | EApply ty0_appl
266 | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
267 (* case 6.3.2: subst0 on right argument *)
268 IHCT; Clear H2; IHC; EApply ty0_appl; XEAuto.
269 (* case 6.3.3: subst0 on both arguments *)
270 IHC; Ty0Correct; Ty0GenBase; IHCT; Clear H2; IHC; Ty0Correct; IHCT.
272 [ EApply ty0_appl | EApply ty0_appl
273 | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
274 (* case 7: ty0_cast *)
275 Clear c1 t t1; Intros until 5; XElim H3; Intros; Clear c2 t3.
276 (* case 7.1: fsubst0_snd *)
277 Subst0GenBase; Rewrite H3; Clear H3 t4.
278 (* case 7.1.1: subst0 on left argument *)
279 IHT; EApply ty0_conv;
282 [ EApply ty0_conv; [ Idtac | Idtac | Apply pc3_s; EApply pc3_fsubst0 ]
284 | EApply pc3_fsubst0 ]; XEAuto.
285 (* case 7.1.2: subst0 on right argument *)
286 IHT; EApply ty0_cast; XEAuto.
287 (* case 7.1.3: subst0 on both arguments *)
292 [ EApply ty0_conv; [ Idtac | Idtac | Apply pc3_s; EApply pc3_fsubst0 ]
294 | EApply pc3_fsubst0 ]; XEAuto.
295 (* case 7.2: fsubst0_fst *)
296 IHC; Clear H2; IHC; EApply ty0_cast; XEAuto.
297 (* case 6.3: fsubst0_both *)
298 Subst0GenBase; Rewrite H3; Clear H3 t4.
299 (* case 7.3.1: subst0 on left argument *)
300 IHC; IHCT; Clear H2; IHC.
304 [ EApply ty0_conv; [ Idtac | Idtac | Apply pc3_s; EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]
306 | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
307 (* case 7.3.2: subst0 on right argument *)
308 IHCT; IHC; EApply ty0_cast; XEAuto.
309 (* case 7.3.3: subst0 on both arguments *)
310 IHC; IHCT; Clear H2; IHCT.
314 [ EApply ty0_conv; [ Idtac | Idtac | Apply pc3_s; EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]
316 | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
319 Theorem ty0_csubst0: (g:?; c1:?; t1,t2:?) (ty0 g c1 t1 t2) ->
320 (e:?; u:?; i:?) (drop i (0) c1 (CTail e (Bind Abbr) u)) ->
321 (c2:?) (wf0 g c2) -> (csubst0 i u c1 c2) ->
323 Intros; EApply ty0_fsubst0; XEAuto.
326 Theorem ty0_subst0: (g:?; c:?; t1,t:?) (ty0 g c t1 t) ->
327 (e:?; u:?; i:?) (drop i (0) c (CTail e (Bind Abbr) u)) ->
328 (t2:?) (subst0 i u t1 t2) -> (ty0 g c t2 t).
329 Intros; EApply ty0_fsubst0; XEAuto.
334 Hints Resolve ty0_subst0 : ltlc.