4 (*#* #caption "generation lemma of typing" #clauses *)
6 Section ty0_gen_base. (***************************************************)
8 (*#* #caption "generation lemma for sorts" *)
9 (*#* #cap #cap c #alpha x in T, n in h *)
11 Theorem ty0_gen_sort: (g:?; c:?; x:?; n:?)
12 (ty0 g c (TSort n) x) ->
13 (pc3 c (TSort (next g n)) x).
17 Intros until 1; InsertEq H '(TSort n); XElim H; Intros.
18 (* case 1 : ty0_conv *)
20 (* case 2 : ty0_sort *)
22 (* case 3 : ty0_abbr *)
24 (* case 4 : ty0_abst *)
26 (* case 5 : ty0_bind *)
28 (* case 6 : ty0_appl *)
30 (* case 7 : ty0_cast *)
36 (*#* #caption "generation lemma for bound references" *)
37 (*#* #cap #cap c, e #alpha x in T, t in U, u in V, n in i *)
39 Theorem ty0_gen_lref: (g:?; c:?; x:?; n:?) (ty0 g c (TLRef n) x) ->
40 (EX e u t | (pc3 c (lift (S n) (0) t) x) &
41 (drop n (0) c (CTail e (Bind Abbr) u)) &
44 (EX e u t | (pc3 c (lift (S n) (0) u) x) &
45 (drop n (0) c (CTail e (Bind Abst) u)) &
51 Intros until 1; InsertEq H '(TLRef n); XElim H; Intros.
52 (* case 1 : ty0_conv *)
53 LApply H2; [ Clear H2; Intros H2 | XAuto ].
54 XElim H2; Intros; XElim H2; XEAuto.
55 (* case 2 : ty0_sort *)
57 (* case 3 : ty0_abbr *)
58 Inversion H3 ; Rewrite H5 in H0; XEAuto.
59 (* case 4 : ty0_abst *)
60 Inversion H3; Rewrite H5 in H0; XEAuto.
61 (* case 5 : ty0_bind *)
63 (* case 6 : ty0_appl *)
65 (* case 7 : ty0_cast *)
71 (*#* #caption "generation lemma for binders" *)
72 (*#* #cap #cap c #alpha x in T, t1 in U1, t2 in U2, u in V, t in U, t0 in U3 *)
74 Theorem ty0_gen_bind: (g:?; b:?; c:?; u,t1,x:?) (ty0 g c (TTail (Bind b) u t1) x) ->
75 (EX t2 t t0 | (pc3 c (TTail (Bind b) u t2) x) &
77 (ty0 g (CTail c (Bind b) u) t1 t2) &
78 (ty0 g (CTail c (Bind b) u) t2 t0)
83 Intros until 1; InsertEq H '(TTail (Bind b) u t1); XElim H; Intros.
84 (* case 1 : ty0_conv *)
85 LApply H2; [ Clear H2; Intros H2 | XAuto ].
87 (* case 2 : ty0_sort *)
89 (* case 3 : ty0_abbr *)
91 (* case 4 : ty0_abst *)
93 (* case 5 : ty0_bind *)
95 Rewrite H7 in H1; Rewrite H7 in H3.
96 Rewrite H8 in H; Rewrite H8 in H1; Rewrite H8 in H3.
97 Rewrite H9 in H1; XEAuto.
98 (* case 6 : ty0_appl *)
100 (* case 7 : ty0_cast *)
106 (*#* #caption "generation lemma for applications" *)
107 (*#* #cap #cap c #alpha x in T, v in U1, w in V1, u in V2, t in U2 *)
109 Theorem ty0_gen_appl: (g:?; c:?; w,v,x:?) (ty0 g c (TTail (Flat Appl) w v) x) ->
110 (EX u t | (pc3 c (TTail (Flat Appl) w (TTail (Bind Abst) u t)) x) &
111 (ty0 g c v (TTail (Bind Abst) u t)) &
117 Intros until 1; InsertEq H '(TTail (Flat Appl) w v); XElim H; Intros.
118 (* case 1 : ty0_conv *)
119 LApply H2; [ Clear H2; Intros H2 | XAuto ].
121 (* case 2 : ty0_sort *)
123 (* case 3 : ty0_abbr *)
125 (* case 4 : ty0_abst *)
127 (* case 5 : ty0_bind *)
129 (* case 6 : ty0_appl *)
130 Inversion H3; Rewrite H5 in H; Rewrite H6 in H1; XEAuto.
131 (* case 7 : ty0_cast *)
137 (*#* #caption "generation lemma for type casts" *)
138 (*#* #cap #cap c #alpha x in T, t2 in V, t1 in U *)
140 Theorem ty0_gen_cast: (g:?; c:?; t1,t2,x:?)
141 (ty0 g c (TTail (Flat Cast) t2 t1) x) ->
142 (pc3 c t2 x) /\ (ty0 g c t1 t2).
146 Intros until 1; InsertEq H '(TTail (Flat Cast) t2 t1); XElim H; Intros.
147 (* case 1 : ty0_conv *)
148 LApply H2; [ Clear H2; Intros H2 | XAuto ].
150 (* case 2 : ty0_sort *)
152 (* case 3 : ty0_abbr *)
154 (* case 4 : ty0_abst *)
156 (* case 5 : ty0_bind *)
158 (* case 6 : ty0_appl *)
160 (* case 7 : ty0_cast *)
161 Inversion H3; Rewrite H5 in H; Rewrite H5 in H1; Rewrite H6 in H; XAuto.
166 Tactic Definition Ty0GenBase :=
168 | [ H: (ty0 ?1 ?2 (TSort ?3) ?4) |- ? ] ->
169 LApply (ty0_gen_sort ?1 ?2 ?4 ?3); [ Clear H; Intros | XAuto ]
170 | [ H: (ty0 ?1 ?2 (TLRef ?3) ?4) |- ? ] ->
171 LApply (ty0_gen_lref ?1 ?2 ?4 ?3); [ Clear H; Intros H | XAuto ];
172 XElim H; Intros H; XElim H; Intros
173 | [ H: (ty0 ?1 ?2 (TTail (Bind ?3) ?4 ?5) ?6) |- ? ] ->
174 LApply (ty0_gen_bind ?1 ?3 ?2 ?4 ?5 ?6); [ Clear H; Intros H | XAuto ];
176 | [ H: (ty0 ?1 ?2 (TTail (Flat Appl) ?3 ?4) ?5) |- ? ] ->
177 LApply (ty0_gen_appl ?1 ?2 ?3 ?4 ?5); [ Clear H; Intros H | XAuto ];
179 | [ H: (ty0 ?1 ?2 (TTail (Flat Cast) ?3 ?4) ?5) |- ? ] ->
180 LApply (ty0_gen_cast ?1 ?2 ?4 ?3 ?5); [ Clear H; Intros H | XAuto ];