3 Require Export ty0_defs.
5 Inductive csub0 [g:G] : C -> C -> Prop :=
7 | csub0_sort : (n:?) (csub0 g (CSort n) (CSort n))
8 | csub0_tail : (c1,c2:?) (csub0 g c1 c2) -> (k,u:?)
9 (csub0 g (CTail c1 k u) (CTail c2 k u))
11 | csub0_void : (c1,c2:?) (csub0 g c1 c2) -> (b:?) ~b=Void -> (u1,u2:?)
12 (csub0 g (CTail c1 (Bind Void) u1) (CTail c2 (Bind b) u2))
13 | csub0_abst : (c1,c2:?) (csub0 g c1 c2) -> (u,t:?) (ty0 g c2 u t) ->
14 (csub0 g (CTail c1 (Bind Abst) t) (CTail c2 (Bind Abbr) u)).
16 Hint csub0 : ltlc := Constructors csub0.
18 Section csub0_props. (****************************************************)
20 Theorem csub0_refl : (g:?; c:?) (csub0 g c c).
26 Hints Resolve csub0_refl : ltlc.
28 Section csub0_drop. (*****************************************************)
30 Theorem csub0_drop_abbr : (g:?; n:?; c1,c2:?) (csub0 g c1 c2) -> (d1,u:?)
31 (drop n (0) c1 (CTail d1 (Bind Abbr) u)) ->
32 (EX d2 | (csub0 g d1 d2) &
33 (drop n (0) c2 (CTail d2 (Bind Abbr) u))
37 Intros; DropGenBase; Rewrite H0 in H; Inversion H; XEAuto.
39 Intros until 2; XElim H0.
40 (* case 2.1 : csub0_sort *)
42 (* case 2.2 : csub0_tail *)
43 XElim k; Intros; DropGenBase.
44 (* case 2.2.1 : Bind *)
45 LApply (H c0 c3); [ Clear H; Intros H | XAuto ].
46 LApply (H d1 u0); [ Clear H; Intros H | XAuto ].
48 (* case 2.2.2 : Flat *)
49 LApply (H1 d1 u0); [ Clear H1; Intros H1 | XAuto ].
51 (* case 2.3 : csub0_void *)
53 LApply (H c0 c3); [ Clear H; Intros H | XAuto ].
54 LApply (H d1 u); [ Clear H; Intros H | XAuto ].
56 (* case 2.4 : csub0_abst *)
58 LApply (H c0 c3); [ Clear H; Intros H | XAuto ].
59 LApply (H d1 u0); [ Clear H; Intros H | XAuto ].
63 Theorem csub0_drop_abst : (g:?; n:?; c1,c2:?) (csub0 g c1 c2) -> (d1,t:?)
64 (drop n (0) c1 (CTail d1 (Bind Abst) t)) ->
65 (EX d2 | (csub0 g d1 d2) &
66 (drop n (0) c2 (CTail d2 (Bind Abst) t))
69 (EX d2 u | (csub0 g d1 d2) &
70 (drop n (0) c2 (CTail d2 (Bind Abbr) u)) &
75 Intros; DropGenBase; Rewrite H0 in H; Inversion H; XEAuto.
77 Intros until 2; XElim H0.
78 (* case 2.1 : csub0_sort *)
80 (* case 2.2 : csub0_tail *)
81 XElim k; Intros; DropGenBase.
82 (* case 2.2.1 : Bind *)
83 LApply (H c0 c3); [ Clear H; Intros H | XAuto ].
84 LApply (H d1 t); [ Clear H; Intros H | XAuto ].
85 XElim H; Intros; XElim H; XEAuto.
86 (* case 2.2.2 : Flat *)
87 LApply (H1 d1 t); [ Clear H1; Intros H1 | XAuto ].
88 XElim H1; Intros; XElim H1; XEAuto.
89 (* case 2.3 : csub0_void *)
91 LApply (H c0 c3); [ Clear H; Intros H | XAuto ].
92 LApply (H d1 t); [ Clear H; Intros H | XAuto ].
93 XElim H; Intros; XElim H; XEAuto.
94 (* case 2.4 : csub0_abst *)
96 LApply (H c0 c3); [ Clear H; Intros H | XAuto ].
97 LApply (H d1 t0); [ Clear H; Intros H | XAuto ].
98 XElim H; Intros; XElim H; XEAuto.
103 Tactic Definition CSub0Drop :=
105 | [ H1: (csub0 ?1 ?2 ?3);
106 H2: (drop ?4 (0) ?2 (CTail ?5 (Bind Abbr) ?6)) |- ? ] ->
107 LApply (csub0_drop_abbr ?1 ?4 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
108 LApply (H1 ?5 ?6); [ Clear H1 H2; Intros H1 | XAuto ];
110 | [ H1: (csub0 ?1 ?2 ?3);
111 H2: (drop ?4 (0) ?2 (CTail ?5 (Bind Abst) ?6)) |- ? ] ->
112 LApply (csub0_drop_abst ?1 ?4 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
113 LApply (H1 ?5 ?6); [ Clear H1 H2; Intros H1 | XAuto ];
114 XElim H1; Intros H1; XElim H1; Intros.
116 Section csub0_pc3. (*****************************************************)
118 Theorem csub0_pr2 : (g:?; c1:?; t1,t2:?) (pr2 c1 t1 t2) ->
119 (c2:?) (csub0 g c1 c2) -> (pr2 c2 t1 t2).
120 Intros until 1; XElim H; Intros.
121 (* case 1 : pr2_pr0 *)
123 (* case 2 : pr2_delta *)
127 Theorem csub0_pc2 : (g:?; c1:?; t1,t2:?) (pc2 c1 t1 t2) ->
128 (c2:?) (csub0 g c1 c2) -> (pc2 c2 t1 t2).
129 Intros until 1; XElim H; Intros.
131 Apply pc2_r; EApply csub0_pr2; XEAuto.
133 Apply pc2_x; EApply csub0_pr2; XEAuto.
136 Theorem csub0_pc3 : (g:?; c1:?; t1,t2:?) (pc3 c1 t1 t2) ->
137 (c2:?) (csub0 g c1 c2) -> (pc3 c2 t1 t2).
138 Intros until 1; XElim H; Intros.
142 EApply pc3_u; [ EApply csub0_pc2; XEAuto | XAuto ].
147 Hints Resolve csub0_pc3 : ltlc.
149 Section csub0_ty0. (*****************************************************)
151 Theorem csub0_ty0 : (g:?; c1:?; t1,t2:?) (ty0 g c1 t1 t2) ->
152 (c2:?) (wf0 g c2) -> (csub0 g c1 c2) ->
154 Intros until 1; XElim H; Intros.
155 (* case 1 : ty0_conv *)
156 EApply ty0_conv; XEAuto.
157 (* case 2 : ty0_sort *)
159 (* case 3 : ty0_abbr *)
160 CSub0Drop; EApply ty0_abbr; XEAuto.
161 (* case 4 : ty0_abst *)
162 CSub0Drop; [ EApply ty0_abst | EApply ty0_abbr ]; XEAuto.
163 (* case 5 : ty0_bind *)
164 EApply ty0_bind; XEAuto.
165 (* case 6 : ty0_appl *)
166 EApply ty0_appl; XEAuto.
167 (* case 7 : ty0_cast *)
168 EApply ty0_cast; XAuto.
171 Theorem csub0_ty0_ld : (g:?; c:?; u,v:?) (ty0 g c u v) -> (t1,t2:?)
172 (ty0 g (CTail c (Bind Abst) v) t1 t2) ->
173 (ty0 g (CTail c (Bind Abbr) u) t1 t2).
174 Intros; EApply csub0_ty0; XEAuto.
179 Hints Resolve csub0_ty0 csub0_ty0_ld : ltlc.
181 Tactic Definition CSub0Ty0 :=
183 [ _: (ty0 ?1 ?2 ?4 ?); _: (ty0 ?1 ?2 ?3 ?7); _: (pc3 ?2 ?4 ?7);
184 H: (ty0 ?1 (CTail ?2 (Bind Abst) ?4) ?5 ?6) |- ? ] ->
185 LApply (csub0_ty0_ld ?1 ?2 ?3 ?4); [ Intros H_x | EApply ty0_conv; XEAuto ];
186 LApply (H_x ?5 ?6); [ Clear H_x H; Intros | XAuto ].