10 Section ty0_fsubst0. (****************************************************)
14 Tactic Definition IH H0 v1 v2 v3 v4 v5 :=
15 LApply (H0 v1 v2 v3 v4); [ Intros H_x | XEAuto ];
16 LApply H_x; [ Clear H_x; Intros H_x | XEAuto ];
17 LApply (H_x v5); [ Clear H_x; Intros | XEAuto ].
19 Tactic Definition IHT :=
21 [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 ?1 ?2 c2 t2) ->
23 (e:C) (drop i (0) ?1 (CTail e (Bind Abbr) u0)) -> ?;
24 _: (subst0 ?4 ?5 ?2 ?6);
25 _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
28 Tactic Definition IHTb1 :=
30 [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
32 (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
33 _: (subst0 ?4 ?5 ?10 ?6);
34 _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
35 IH H '(S ?4) ?5 '(CTail ?1 (Bind ?11) ?6) ?2 ?9.
37 Tactic Definition IHTb2 :=
39 [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
41 (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
42 _: (subst0 (s (Bind ?11) ?4) ?5 ?2 ?6);
43 _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
44 IH H '(S ?4) ?5 '(CTail ?1 (Bind ?11) ?10) ?6 ?9.
46 Tactic Definition IHC :=
48 [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 ?1 ?2 c2 t2) ->
50 (e:C) (drop i (0) ?1 (CTail e (Bind Abbr) u0)) -> ?;
51 _: (csubst0 ?4 ?5 ?1 ?6);
52 _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
55 Tactic Definition IHCb :=
57 [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
59 (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
60 _: (csubst0 ?4 ?5 ?1 ?6);
61 _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
62 IH H '(S ?4) ?5 '(CTail ?6 (Bind ?11) ?10) ?2 ?9.
64 Tactic Definition IHTTb :=
66 [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
68 (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
69 _: (subst0 ?4 ?5 ?10 ?6);
70 _: (subst0 (s (Bind ?11) ?4) ?5 ?2 ?7);
71 _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
72 IH H '(S ?4) ?5 '(CTail ?1 (Bind ?11) ?6) ?7 ?9.
74 Tactic Definition IHCT :=
76 [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 ?1 ?2 c2 t2) ->
78 (e:C) (drop i (0) ?1 (CTail e (Bind Abbr) u0)) -> ?;
79 _: (csubst0 ?4 ?5 ?1 ?6);
80 _: (subst0 ?4 ?5 ?2 ?7);
81 _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
84 Tactic Definition IHCTb1 :=
86 [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
88 (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
89 _: (csubst0 ?4 ?5 ?1 ?6);
90 _: (subst0 ?4 ?5 ?10 ?7);
91 _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
92 IH H '(S ?4) ?5 '(CTail ?6 (Bind ?11) ?7) ?2 ?9.
94 Tactic Definition IHCTb2 :=
96 [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
98 (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
99 _: (csubst0 ?4 ?5 ?1 ?6);
100 _: (subst0 (s (Bind ?11) ?4) ?5 ?2 ?7);
101 _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
102 IH H '(S ?4) ?5 '(CTail ?6 (Bind ?11) ?10) ?7 ?9.
104 Tactic Definition IHCTTb :=
106 [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
108 (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
109 _: (csubst0 ?4 ?5 ?1 ?6);
110 _: (subst0 ?4 ?5 ?10 ?7);
111 _: (subst0 (s (Bind ?11) ?4) ?5 ?2 ?8);
112 _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
113 IH H '(S ?4) ?5 '(CTail ?6 (Bind ?11) ?7) ?8 ?9.
117 (*#* #caption "substitution preserves types" *)
118 (*#* #cap #cap c1, c2, e, t1, t2, t #alpha u in V *)
120 (* NOTE: This breaks the mutual recursion between ty0_subst0 and ty0_csubst0 *)
121 Theorem ty0_fsubst0: (g:?; c1:?; t1,t:?) (ty0 g c1 t1 t) ->
122 (i:?; u,c2,t2:?) (fsubst0 i u c1 t1 c2 t2) ->
124 (e:?) (drop i (0) c1 (CTail e (Bind Abbr) u)) ->
129 Intros until 1; XElim H.
130 (* case 1: ty0_conv *)
131 Intros until 6; XElim H4; Intros.
132 (* case 1.1: fsubst0_snd *)
133 IHT; EApply ty0_conv; XEAuto.
134 (* case 1.2: fsubst0_fst *)
135 IHC; EApply ty0_conv; Try EApply pc3_fsubst0; XEAuto.
136 (* case 1.3: fsubst0_both *)
137 IHCT; IHCT; EApply ty0_conv; Try EApply pc3_fsubst0; XEAuto.
138 (* case 2: ty0_sort *)
139 Intros until 2; XElim H0; Intros.
140 (* case 2.1: fsubst0_snd *)
142 (* case 2.2: fsubst0_fst *)
144 (* case 2.3: fsubst0_both *)
146 (* case 3: ty0_abbr *)
147 Intros until 5; XElim H3; Intros; Clear c1 c2 t t1 t2.
148 (* case 3.1: fsubst0_snd *)
149 Subst0GenBase; Rewrite H6; Rewrite <- H3 in H5; Clear H3 H6 i t3.
150 DropDis; Inversion H5; Rewrite <- H6 in H0; Rewrite H7 in H1; XEAuto.
151 (* case 3.2: fsubst0_fst *)
152 Apply (lt_le_e n i); Intros; CSubst0Drop.
153 (* case 3.2.1: n < i, none *)
154 EApply ty0_abbr; XEAuto.
155 (* case 3.2.2: n < i, csubst0_snd *)
156 Inversion H0; CSubst0Drop.
157 Rewrite <- H10 in H7; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H8;
158 Clear H0 H10 H11 H12 x0 x1 x2.
159 DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase | XAuto ].
160 IHT; EApply ty0_abbr; XEAuto.
161 (* case 3.2.3: n < i, csubst0_fst *)
162 Inversion H0; CSubst0Drop.
163 Rewrite <- H10 in H8; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H7;
164 Clear H0 H10 H11 H12 x0 x1 x3.
165 DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase; CSubst0Drop | XAuto ].
166 IHC; EApply ty0_abbr; XEAuto.
167 (* case 3.2.4: n < i, csubst0_both *)
168 Inversion H0; CSubst0Drop.
169 Rewrite <- H11 in H9; Rewrite <- H12 in H7; Rewrite <- H12 in H8; Rewrite <- H12 in H9; Rewrite <- H13 in H8;
170 Clear H0 H11 H12 H13 x0 x1 x3.
171 DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase; CSubst0Drop | XAuto ].
172 IHCT; EApply ty0_abbr; XEAuto.
173 (* case 3.2.5: n >= i *)
174 EApply ty0_abbr; XEAuto.
175 (* case 3.3: fsubst0_both *)
176 Subst0GenBase; Rewrite H7; Rewrite <- H3 in H4; Rewrite <- H3 in H6; Clear H3 H7 i t3.
177 DropDis; Inversion H6; Rewrite <- H7 in H0; Rewrite H8 in H1.
179 (* case 4: ty0_abst *)
180 Intros until 5; XElim H3; Intros; Clear c1 c2 t t1 t2.
181 (* case 4.1: fsubst0_snd *)
182 Subst0GenBase; Rewrite H3 in H0; DropDis; Inversion H0.
183 (* case 4.2: fsubst0_fst *)
184 Apply (lt_le_e n i); Intros; CSubst0Drop.
185 (* case 4.2.1: n < i, none *)
186 EApply ty0_abst; XEAuto.
187 (* case 4.2.2: n < i, csubst0_snd *)
188 Inversion H0; CSubst0Drop.
189 Rewrite <- H10 in H7; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H8; Rewrite <- H12;
190 Clear H0 H10 H11 H12 x0 x1 x2.
191 DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase | XAuto ].
192 IHT; EApply ty0_conv;
193 [ EApply ty0_lift | EApply ty0_abst | EApply pc3_lift ]; XEAuto.
194 (* case 4.2.3: n < i, csubst0_fst *)
195 Inversion H0; CSubst0Drop.
196 Rewrite <- H10 in H8; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H7; Rewrite <- H12;
197 Clear H0 H10 H11 H12 x0 x1 x3.
198 DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase; CSubst0Drop | XAuto ].
199 IHC; EApply ty0_abst; XEAuto.
200 (* case 4.2.4: n < i, csubst0_both *)
201 Inversion H0; CSubst0Drop.
202 Rewrite <- H11 in H9; Rewrite <- H12 in H7; Rewrite <- H12 in H8; Rewrite <- H12 in H9; Rewrite <- H13 in H8; Rewrite <- H13;
203 Clear H0 H11 H12 H13 x0 x1 x3.
204 DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase; CSubst0Drop | XAuto ].
205 IHCT; IHC; EApply ty0_conv;
206 [ EApply ty0_lift | EApply ty0_abst
207 | EApply pc3_lift; Try EApply pc3_fsubst0; Try Apply H0
209 (* case 4.2.4: n >= i *)
210 EApply ty0_abst; XEAuto.
211 (* case 4.3: fsubst0_both *)
212 Subst0GenBase; Rewrite H3 in H0; DropDis; Inversion H0.
213 (* case 5: ty0_bind *)
214 Intros until 7; XElim H5; Intros; Clear H4.
215 (* case 5.1: fsubst0_snd *)
216 Subst0GenBase; Rewrite H4; Clear H4 t6.
217 (* case 5.1.1: subst0 on left argument *)
218 Ty0Correct; IHT; IHTb1; Ty0Correct.
220 [ EApply ty0_bind | EApply ty0_bind | EApply pc3_fsubst0 ]; XEAuto.
221 (* case 5.1.2: subst0 on right argument *)
222 IHTb2; Ty0Correct; EApply ty0_bind; XEAuto.
223 (* case 5.1.3: subst0 on both arguments *)
224 Ty0Correct; IHT; IHTb1; IHTTb; Ty0Correct.
226 [ EApply ty0_bind | EApply ty0_bind | EApply pc3_fsubst0 ]; XEAuto.
227 (* case 5.2: fsubst0_fst *)
228 IHC; IHCb; Ty0Correct; EApply ty0_bind; XEAuto.
229 (* case 5.3: fsubst0_both *)
230 Subst0GenBase; Rewrite H4; Clear H4 t6.
231 (* case 5.3.1: subst0 on left argument *)
232 IHC; IHCb; Ty0Correct; Ty0Correct; IHCT; IHCTb1; Ty0Correct.
234 [ EApply ty0_bind | EApply ty0_bind
235 | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
236 (* case 5.3.2: subst0 on right argument *)
237 IHC; IHCTb2; Ty0Correct; EApply ty0_bind; XEAuto.
238 (* case 5.3.3: subst0 on both arguments *)
239 IHC; IHCb; Ty0Correct; Ty0Correct; IHCT; IHCTTb; Ty0Correct.
241 [ EApply ty0_bind | EApply ty0_bind
242 | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
243 (* case 6: ty0_appl *)
244 Intros until 5; XElim H3; Intros.
245 (* case 6.1: fsubst0_snd *)
246 Subst0GenBase; Rewrite H3; Clear H3 c1 c2 t t1 t2 t3.
247 (* case 6.1.1: subst0 on left argument *)
248 Ty0Correct; Ty0GenBase; IHT; Ty0Correct.
250 [ EApply ty0_appl | EApply ty0_appl | EApply pc3_fsubst0 ]; XEAuto.
251 (* case 6.1.2: subst0 on right argument *)
252 IHT; EApply ty0_appl; XEAuto.
253 (* case 6.1.3: subst0 on both arguments *)
254 Ty0Correct; Ty0GenBase; Move H after H10; Ty0Correct; IHT; Clear H2; IHT.
256 [ EApply ty0_appl | EApply ty0_appl | EApply pc3_fsubst0 ]; XEAuto.
257 (* case 6.2: fsubst0_fst *)
258 IHC; Clear H2; IHC; EApply ty0_appl; XEAuto.
259 (* case 6.3: fsubst0_both *)
260 Subst0GenBase; Rewrite H3; Clear H3 c1 c2 t t1 t2 t3.
261 (* case 6.3.1: subst0 on left argument *)
262 IHC; Ty0Correct; Ty0GenBase; Clear H2; IHC; IHCT.
264 [ EApply ty0_appl | EApply ty0_appl
265 | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
266 (* case 6.3.2: subst0 on right argument *)
267 IHCT; Clear H2; IHC; EApply ty0_appl; XEAuto.
268 (* case 6.3.3: subst0 on both arguments *)
269 IHC; Ty0Correct; Ty0GenBase; IHCT; Clear H2; IHC; Ty0Correct; IHCT.
271 [ EApply ty0_appl | EApply ty0_appl
272 | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
273 (* case 7: ty0_cast *)
274 Clear c1 t t1; Intros until 5; XElim H3; Intros; Clear c2 t3.
275 (* case 7.1: fsubst0_snd *)
276 Subst0GenBase; Rewrite H3; Clear H3 t4.
277 (* case 7.1.1: subst0 on left argument *)
278 IHT; EApply ty0_conv;
281 [ EApply ty0_conv; [ Idtac | Idtac | Apply pc3_s; EApply pc3_fsubst0 ]
283 | EApply pc3_fsubst0 ]; XEAuto.
284 (* case 7.1.2: subst0 on right argument *)
285 IHT; EApply ty0_cast; XEAuto.
286 (* case 7.1.3: subst0 on both arguments *)
291 [ EApply ty0_conv; [ Idtac | Idtac | Apply pc3_s; EApply pc3_fsubst0 ]
293 | EApply pc3_fsubst0 ]; XEAuto.
294 (* case 7.2: fsubst0_fst *)
295 IHC; Clear H2; IHC; EApply ty0_cast; XEAuto.
296 (* case 6.3: fsubst0_both *)
297 Subst0GenBase; Rewrite H3; Clear H3 t4.
298 (* case 7.3.1: subst0 on left argument *)
299 IHC; IHCT; Clear H2; IHC.
303 [ EApply ty0_conv; [ Idtac | Idtac | Apply pc3_s; EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]
305 | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
306 (* case 7.3.2: subst0 on right argument *)
307 IHCT; IHC; EApply ty0_cast; XEAuto.
308 (* case 7.3.3: subst0 on both arguments *)
309 IHC; IHCT; Clear H2; IHCT.
313 [ EApply ty0_conv; [ Idtac | Idtac | Apply pc3_s; EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]
315 | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
318 Theorem ty0_csubst0: (g:?; c1:?; t1,t2:?) (ty0 g c1 t1 t2) ->
319 (e:?; u:?; i:?) (drop i (0) c1 (CTail e (Bind Abbr) u)) ->
320 (c2:?) (wf0 g c2) -> (csubst0 i u c1 c2) ->
322 Intros; EApply ty0_fsubst0; XEAuto.
325 Theorem ty0_subst0: (g:?; c:?; t1,t:?) (ty0 g c t1 t) ->
326 (e:?; u:?; i:?) (drop i (0) c (CTail e (Bind Abbr) u)) ->
327 (t2:?) (subst0 i u t1 t2) -> (ty0 g c t2 t).
328 Intros; EApply ty0_fsubst0; XEAuto.
333 Hints Resolve ty0_subst0 : ltlc.