1 Require Export pc3_defs.
7 f_inc : (n:?) (lt n (f n))
12 (*#* #caption "typing",
13 "well formed context sort", "well formed context binder",
14 "conversion rule", "typed sort", "typed reference to abbreviation",
15 "typed reference to abstraction", "typed binder", "typed application",
18 Inductive wf0 [g:G] : C -> Prop :=
19 | wf0_sort : (m:?) (wf0 g (CSort m))
20 | wf0_bind : (c:?; u,t:?) (ty0 g c u t) ->
21 (b:?) (wf0 g (CTail c (Bind b) u))
22 with ty0 [g:G] : C -> T -> T -> Prop :=
23 (* structural rules *)
24 | ty0_conv : (c:?; t2,t:?) (ty0 g c t2 t) ->
25 (u,t1:?) (ty0 g c u t1) -> (pc3 c t1 t2) ->
28 | ty0_sort : (c:?) (wf0 g c) ->
29 (m:?) (ty0 g c (TSort m) (TSort (f g m)))
30 | ty0_abbr : (c:?) (wf0 g c) ->
31 (n:?; d:?; u:?) (drop n (0) c (CTail d (Bind Abbr) u)) ->
32 (t:?) (ty0 g d u t) ->
33 (ty0 g c (TLRef n) (lift (S n) (0) t))
34 | ty0_abst : (c:?) (wf0 g c) ->
35 (n:?; d:?; u:?) (drop n (0) c (CTail d (Bind Abst) u)) ->
36 (t:?) (ty0 g d u t) ->
37 (ty0 g c (TLRef n) (lift (S n) (0) u))
38 | ty0_bind : (c:?; u,t:?) (ty0 g c u t) ->
39 (b:?; t1,t2:?) (ty0 g (CTail c (Bind b) u) t1 t2) ->
40 (t0:?) (ty0 g (CTail c (Bind b) u) t2 t0) ->
41 (ty0 g c (TTail (Bind b) u t1) (TTail (Bind b) u t2))
42 | ty0_appl : (c:?; w,u:?) (ty0 g c w u) ->
43 (v,t:?) (ty0 g c v (TTail (Bind Abst) u t)) ->
44 (ty0 g c (TTail (Flat Appl) w v)
45 (TTail (Flat Appl) w (TTail (Bind Abst) u t))
47 | ty0_cast : (c:?; t1,t2:?) (ty0 g c t1 t2) ->
48 (t0:?) (ty0 g c t2 t0) ->
49 (ty0 g c (TTail (Flat Cast) t2 t1) t2).
51 Hint wf0 : ltlc := Constructors wf0.
53 Hint ty0 : ltlc := Constructors ty0.
55 (*#* #caption "generation lemma of typing" #clauses ty0_gen_base *)
57 Section ty0_gen_base. (***************************************************)
59 (*#* #caption "generation lemma for sort" *)
60 (*#* #cap #cap c #alpha x in T, n in h *)
62 Theorem ty0_gen_sort: (g:?; c:?; x:?; n:?)
63 (ty0 g c (TSort n) x) ->
64 (pc3 c (TSort (f g n)) x).
68 Intros until 1; InsertEq H '(TSort n); XElim H; Intros.
69 (* case 1 : ty0_conv *)
71 (* case 2 : ty0_sort *)
73 (* case 3 : ty0_abbr *)
75 (* case 4 : ty0_abst *)
77 (* case 5 : ty0_bind *)
79 (* case 6 : ty0_appl *)
81 (* case 7 : ty0_cast *)
87 (*#* #caption "generation lemma for bound reference" *)
88 (*#* #cap #cap c, e #alpha x in T, t in U, u in V, n in i *)
90 Theorem ty0_gen_lref: (g:?; c:?; x:?; n:?) (ty0 g c (TLRef n) x) ->
91 (EX e u t | (pc3 c (lift (S n) (0) t) x) &
92 (drop n (0) c (CTail e (Bind Abbr) u)) &
95 (EX e u t | (pc3 c (lift (S n) (0) u) x) &
96 (drop n (0) c (CTail e (Bind Abst) u)) &
102 Intros until 1; InsertEq H '(TLRef n); XElim H; Intros.
103 (* case 1 : ty0_conv *)
104 LApply H2; [ Clear H2; Intros H2 | XAuto ].
105 XElim H2; Intros; XElim H2; XEAuto.
106 (* case 2 : ty0_sort *)
108 (* case 3 : ty0_abbr *)
109 Inversion H3 ; Rewrite H5 in H0; XEAuto.
110 (* case 4 : ty0_abst *)
111 Inversion H3; Rewrite H5 in H0; XEAuto.
112 (* case 5 : ty0_bind *)
114 (* case 6 : ty0_appl *)
116 (* case 7 : ty0_cast *)
122 (*#* #caption "generation lemma for binder" *)
123 (*#* #cap #cap c #alpha x in T, t1 in U1, t2 in U2, u in V, t in U, t0 in U3 *)
125 Theorem ty0_gen_bind: (g:?; b:?; c:?; u,t1,x:?) (ty0 g c (TTail (Bind b) u t1) x) ->
126 (EX t2 t t0 | (pc3 c (TTail (Bind b) u t2) x) &
128 (ty0 g (CTail c (Bind b) u) t1 t2) &
129 (ty0 g (CTail c (Bind b) u) t2 t0)
134 Intros until 1; InsertEq H '(TTail (Bind b) u t1); XElim H; Intros.
135 (* case 1 : ty0_conv *)
136 LApply H2; [ Clear H2; Intros H2 | XAuto ].
138 (* case 2 : ty0_sort *)
140 (* case 3 : ty0_abbr *)
142 (* case 4 : ty0_abst *)
144 (* case 5 : ty0_bind *)
146 Rewrite H7 in H1; Rewrite H7 in H3.
147 Rewrite H8 in H; Rewrite H8 in H1; Rewrite H8 in H3.
148 Rewrite H9 in H1; XEAuto.
149 (* case 6 : ty0_appl *)
151 (* case 7 : ty0_cast *)
157 (*#* #caption "generation lemma for application" *)
158 (*#* #cap #cap c #alpha x in T, v in U1, w in V1, u in V2, t in U2 *)
160 Theorem ty0_gen_appl: (g:?; c:?; w,v,x:?) (ty0 g c (TTail (Flat Appl) w v) x) ->
161 (EX u t | (pc3 c (TTail (Flat Appl) w (TTail (Bind Abst) u t)) x) &
162 (ty0 g c v (TTail (Bind Abst) u t)) &
168 Intros until 1; InsertEq H '(TTail (Flat Appl) w v); XElim H; Intros.
169 (* case 1 : ty0_conv *)
170 LApply H2; [ Clear H2; Intros H2 | XAuto ].
172 (* case 2 : ty0_sort *)
174 (* case 3 : ty0_abbr *)
176 (* case 4 : ty0_abst *)
178 (* case 5 : ty0_bind *)
180 (* case 6 : ty0_appl *)
181 Inversion H3; Rewrite H5 in H; Rewrite H6 in H1; XEAuto.
182 (* case 7 : ty0_cast *)
188 (*#* #caption "generation lemma for cast" *)
189 (*#* #cap #cap c #alpha x in T, t2 in V, t1 in U *)
191 Theorem ty0_gen_cast: (g:?; c:?; t1,t2,x:?)
192 (ty0 g c (TTail (Flat Cast) t2 t1) x) ->
193 (pc3 c t2 x) /\ (ty0 g c t1 t2).
197 Intros until 1; InsertEq H '(TTail (Flat Cast) t2 t1); XElim H; Intros.
198 (* case 1 : ty0_conv *)
199 LApply H2; [ Clear H2; Intros H2 | XAuto ].
201 (* case 2 : ty0_sort *)
203 (* case 3 : ty0_abbr *)
205 (* case 4 : ty0_abst *)
207 (* case 5 : ty0_bind *)
209 (* case 6 : ty0_appl *)
211 (* case 7 : ty0_cast *)
212 Inversion H3; Rewrite H5 in H; Rewrite H5 in H1; Rewrite H6 in H; XAuto.
217 Tactic Definition Ty0GenBase :=
219 | [ H: (ty0 ?1 ?2 (TSort ?3) ?4) |- ? ] ->
220 LApply (ty0_gen_sort ?1 ?2 ?4 ?3); [ Clear H; Intros | XAuto ]
221 | [ H: (ty0 ?1 ?2 (TLRef ?3) ?4) |- ? ] ->
222 LApply (ty0_gen_lref ?1 ?2 ?4 ?3); [ Clear H; Intros H | XAuto ];
223 XElim H; Intros H; XElim H; Intros
224 | [ H: (ty0 ?1 ?2 (TTail (Bind ?3) ?4 ?5) ?6) |- ? ] ->
225 LApply (ty0_gen_bind ?1 ?3 ?2 ?4 ?5 ?6); [ Clear H; Intros H | XAuto ];
227 | [ H: (ty0 ?1 ?2 (TTail (Flat Appl) ?3 ?4) ?5) |- ? ] ->
228 LApply (ty0_gen_appl ?1 ?2 ?3 ?4 ?5); [ Clear H; Intros H | XAuto ];
230 | [ H: (ty0 ?1 ?2 (TTail (Flat Cast) ?3 ?4) ?5) |- ? ] ->
231 LApply (ty0_gen_cast ?1 ?2 ?4 ?3 ?5); [ Clear H; Intros H | XAuto ];
234 Section wf0_props. (******************************************************)
236 Theorem wf0_ty0 : (g:?; c:?; u,t:?) (ty0 g c u t) -> (wf0 g c).
237 Intros; XElim H; XAuto.
240 Hints Resolve wf0_ty0 : ltlc.
242 Theorem wf0_drop_O : (c,e:?; h:?) (drop h (0) c e) ->
243 (g:?) (wf0 g c) -> (wf0 g e).
246 Intros; DropGenBase; Rewrite H; XAuto.
247 (* case 2 : CTail k *)
248 Intros c IHc; XElim k; (
249 XElim h; Intros; DropGenBase;
250 [ Rewrite H in H0; XAuto | Inversion H1; XEAuto ] ).
255 Hints Resolve wf0_ty0 wf0_drop_O : ltlc.
257 Tactic Definition Wf0Ty0 :=
259 [ _: (ty0 ?1 ?2 ?3 ?4) |- ? ] ->
260 LApply (wf0_ty0 ?1 ?2 ?3 ?4); [ Intros H_x | XAuto ];
263 Tactic Definition Wf0DropO :=
265 | [ _: (drop ?1 (0) ?2 ?3); _: (wf0 ?4 ?2) |- ? ] ->
266 LApply (wf0_drop_O ?2 ?3 ?1); [ Intros H_x | XAuto ];
267 LApply (H_x ?4); [ Clear H_x; Intros | XAuto ].
269 Section wf0_facilities. (*************************************************)
271 Theorem wf0_drop_wf0 : (g:?; c:?) (wf0 g c) ->
273 (drop h (0) c (CTail e (Bind b) u)) -> (wf0 g e).
275 Wf0DropO; Inversion H1; XEAuto.
278 Theorem ty0_drop_wf0 : (g:?; c:?; t1,t2:?) (ty0 g c t1 t2) ->
280 (drop h (0) c (CTail e (Bind b) u)) -> (wf0 g e).
282 EApply wf0_drop_wf0; [ Idtac | EApply H0 ]; XEAuto.
287 Hints Resolve wf0_drop_wf0 ty0_drop_wf0 : ltlc.
289 Tactic Definition DropWf0 :=
291 | [ _: (ty0 ?1 ?2 ?3 ?4);
292 _: (drop ?5 (0) ?2 (CTail ?6 (Bind ?7) ?8)) |- ? ] ->
293 LApply (ty0_drop_wf0 ?1 ?2 ?3 ?4); [ Intros H_x | XAuto ];
294 LApply (H_x ?7 ?6 ?8 ?5); [ Clear H_x; Intros | XAuto ]
296 _: (drop ?5 (0) ?2 (CTail ?6 (Bind ?7) ?8)) |- ? ] ->
297 LApply (wf0_drop_wf0 ?1 ?2); [ Intros H_x | XAuto ];
298 LApply (H_x ?7 ?6 ?8 ?5); [ Clear H_x; Intros | XAuto ].