7 Section ty0_correct. (****************************************************)
9 (*#* #caption "correctness of types" *)
10 (*#* #cap #cap c, t1, t2 #alpha t in T3 *)
12 Theorem ty0_correct : (g:?; c:?; t1,t2:?)
13 (ty0 g c t1 t2) -> (EX t | (ty0 g c t2 t)).
17 Intros; 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 *)
29 XElim H0; XElim H2; Intros.
31 (* case 7 : ty0_cast *)
37 Tactic Definition Ty0Correct :=
39 [ _: (ty0 ?1 ?2 ?3 ?4) |- ? ] ->
40 LApply (ty0_correct ?1 ?2 ?3 ?4); [ Intros H_x | XAuto ];
45 Section ty0_shift. (******************************************************)
47 (*#* #caption "shift lemma for types" *)
48 (*#* #cap #cap t1, t2 #alpha c in C1, e in C2 *)
50 Theorem ty0_shift : (h:?; c,e:?) (drop h (0) c e) ->
51 (g:?; t1,t2:?) (ty0 g c t1 t2) -> (wf0 g e) ->
52 (ty0 g e (app c h t1) (app c h t2)).
58 Intros; DropGenBase; Rewrite <- H.
59 Repeat Rewrite app_O; XAuto.
61 Intros h IHh; XElim c.
62 (* case 2.1 : CSort *)
63 Intros; DropGenBase; Rewrite H.
65 (* case 2.2 : CTail k *)
66 Intros c IHc; Clear IHc; XElim k; Intros; Wf0Ty0.
67 DropGenBase; Move H0 after H2; Ty0Correct.
68 Simpl; Apply IHh; [ Idtac | EApply ty0_bind | Idtac ]; XEAuto.
73 Hints Resolve ty0_shift : ltlc.
75 Section ty0_unique. (*****************************************************)
81 (*#* #caption "uniqueness of types" *)
82 (*#* #cap #cap c, t1, t2 #alpha u in T *)
84 Theorem ty0_unique : (g:?; c:?; u,t1:?) (ty0 g c u t1) ->
85 (t2:?) (ty0 g c u t2) -> (pc3 c t1 t2).
89 Intros until 1; XElim H; Intros.
90 (* case 1 : ty0_conv *)
92 (* case 2 : ty0_sort *)
94 (* case 3 : ty0_abbr *)
95 Ty0GenBase; DropDis; Inversion H4.
96 Rewrite H7 in H2; Rewrite H8 in H2; XEAuto.
97 (* case 4 : ty0_abst *)
98 Ty0GenBase; DropDis; Inversion H4.
99 Rewrite H7 in H2; Rewrite H8 in H2; XEAuto.
100 (* case 5 : ty0_bind *)
102 (* case 6 : ty0_appl *)
103 Ty0GenBase; EApply pc3_t; [ Idtac | EApply H3 ]; XEAuto.
104 (* case 7 : ty0_cast *)
110 Hints Resolve ty0_unique : ltlc.