9 (*#* #caption "corollaries of subject reduction" #clauses *)
13 Section ty0_gen. (********************************************************)
15 Tactic Definition IH e :=
17 [ H0: (t:?; d:?) ?1 = (lift ?2 d t) -> ?; H1: ?1 = (lift ?2 ?3 ?4) |- ? ] ->
18 LApply (H0 ?4 ?3); [ Clear H0 H1; Intros H0 | XAuto ];
19 LApply (H0 e); [ Clear H0; Intros H0 | XEAuto ];
20 LApply H0; [ Clear H0; Intros H0 | XAuto ];
25 (*#* #caption "generation lemma for lift" *)
26 (*#* #cap #cap t2 #alpha c in C1, e in C2, t1 in T, x in T1, d in i *)
28 Theorem ty0_gen_lift : (g:?; c:?; t1,x:?; h,d:?)
29 (ty0 g c (lift h d t1) x) ->
30 (e:?) (wf0 g e) -> (drop h d c e) ->
31 (EX t2 | (pc3 c (lift h d t2) x) & (ty0 g e t1 t2)).
35 Intros until 1; InsertEq H '(lift h d t1);
36 UnIntro H d; UnIntro H t1; XElim H; Intros;
37 Rename x0 into t3; Rename x1 into d0.
38 (* case 1 : ty0_conv *)
40 (* case 2 : ty0_sort *)
41 LiftGenBase; Rewrite H0; Clear H0 t.
42 EApply ex2_intro; [ Rewrite lift_sort; XAuto | XAuto ].
43 (* case 3 : ty0_abbr *)
44 Apply (lt_le_e n d0); Intros.
45 (* case 3.1 : n < d0 *)
46 LiftGenBase; DropS; Rewrite H3; Clear H3 t3.
47 Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ].
48 Rewrite (lt_plus_minus n d0) in H5; [ DropDis; IH x1 | XAuto ].
50 [ Rewrite lift_d; [ EApply pc3_lift; XEAuto | XEAuto ]
51 | EApply ty0_abbr; XEAuto ].
52 (* case 3.2 : n >= d0 *)
53 Apply (lt_le_e n (plus d0 h)); Intros.
54 (* case 3.2.1 : n < d0 + h *)
56 (* case 3.2.2 : n >= d0 + h *)
57 Rewrite (le_plus_minus_sym h n) in H3; [ Idtac | XEAuto ].
58 LiftGenBase; DropDis; Rewrite H3; Clear H3 t3.
59 EApply ex2_intro; [ Idtac | EApply ty0_abbr; XEAuto ].
60 Rewrite lift_free; [ Idtac | XEAuto | XAuto ].
61 Rewrite <- plus_n_Sm; Rewrite <- le_plus_minus; XEAuto.
62 (* case 4 : ty0_abst *)
63 Apply (lt_le_e n d0); Intros.
64 (* case 4.1 : n < d0 *)
65 LiftGenBase; Rewrite H3; Clear H3 t3.
66 Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ].
67 Rewrite (lt_plus_minus n d0) in H5; [ DropDis; Rewrite H0; IH x1 | XAuto ].
68 EApply ex2_intro; [ Rewrite lift_d | EApply ty0_abst ]; XEAuto.
69 (* case 4.2 : n >= d0 *)
70 Apply (lt_le_e n (plus d0 h)); Intros.
71 (* case 4.2.1 : n < d0 + h *)
73 (* case 4.2.2 : n >= d0 + h *)
74 Rewrite (le_plus_minus_sym h n) in H3; [ Idtac | XEAuto ].
75 LiftGenBase; DropDis; Rewrite H3; Clear H3 t3.
76 EApply ex2_intro; [ Idtac | EApply ty0_abst; XEAuto ].
77 Rewrite lift_free; [ Idtac | XEAuto | XAuto ].
78 Rewrite <- plus_n_Sm; Rewrite <- le_plus_minus; XEAuto.
79 (* case 5 : ty0_bind *)
80 LiftGenBase; Rewrite H5; Rewrite H8; Rewrite H8 in H2; Clear H5 t3.
81 Move H0 after H2; IH e; IH '(CTail e (Bind b) x0); Ty0Correct.
82 EApply ex2_intro; [ Rewrite lift_bind; XEAuto | XEAuto ].
83 (* case 6 : ty0_appl *)
84 LiftGenBase; Rewrite H3; Rewrite H6; Clear H3 c t3 x y.
85 IH e; IH e; Pc3Gen; Pc3T; Pc3Gen; Pc3T.
86 Move H3 after H12; Ty0Correct; Ty0SRed; Ty0GenBase; Wf0Ty0.
88 [ Rewrite lift_flat; Apply pc3_thin_dx;
89 Rewrite lift_bind; Apply pc3_tail_21; [ EApply pc3_pr3_x | Idtac ]
92 | EApply ty0_conv; [ EApply ty0_bind | Idtac | Idtac ] ]
94 (* case 7 : ty0_cast *)
95 LiftGenBase; Rewrite H3; Rewrite H6; Rewrite H6 in H0.
96 IH e; IH e; Pc3Gen; XEAuto.
101 Tactic Definition Ty0Gen :=
103 | [ H0: (ty0 ?1 ?2 (lift ?3 ?4 ?5) ?6);
104 H1: (drop ?3 ?4 ?2 ?7) |- ? ] ->
105 LApply (ty0_gen_lift ?1 ?2 ?5 ?6 ?3 ?4); [ Clear H0; Intros H0 | XAuto ];
106 LApply (H0 ?7); [ Clear H0; Intros H0 | XEAuto ];
107 LApply H0; [ Clear H0 H1; Intros H0 | XAuto ];
109 | [ H0: (ty0 ?1 ?2 (lift ?3 ?4 ?5) ?6);
110 _ : (wf0 ?1 ?7) |- ? ] ->
111 LApply (ty0_gen_lift ?1 ?2 ?5 ?6 ?3 ?4); [ Clear H0; Intros H0 | XAuto ];
112 LApply (H0 ?7); [ Clear H0; Intros H0 | XAuto ];
113 LApply H0; [ Clear H0; Intros H0 | XAuto ];
115 | _ -> Ty0GenContext.
117 Section ty0_sred_props. (*************************************************)
121 (*#* #caption "drop preserves well-formedness" *)
122 (*#* #cap #alpha c in C1, e in C2, d in i *)
124 Theorem wf0_drop : (c,e:?; d,h:?) (drop h d c e) ->
125 (g:?) (wf0 g c) -> (wf0 g e).
131 Intros; DropGenBase; Rewrite H; XAuto.
132 (* case 2 : CTail k *)
133 Intros c IHc; XElim k; (
136 | Intros d IHd; Intros;
137 DropGenBase; Rewrite H; Rewrite H1 in H0; Clear IHd H H1 e t;
138 Inversion H0; Clear H3 H4 b0 u ]).
139 (* case 2.1 : Bind, d > 0 *)
145 (*#* #caption "type reduction" *)
146 (*#* #cap #cap c, t1, t2 #alpha u in T *)
148 Theorem ty0_tred : (g:?; c:?; u,t1:?) (ty0 g c u t1) ->
149 (t2:?) (pr3 c t1 t2) -> (ty0 g c u t2).
153 Intros; Ty0Correct; Ty0SRed; EApply ty0_conv; XEAuto.
158 (*#* #caption "subject conversion" *)
159 (*#* #cap #cap c, u1, u2, t1, t2 *)
161 Theorem ty0_sconv : (g:?; c:?; u1,t1:?) (ty0 g c u1 t1) ->
162 (u2,t2:?) (ty0 g c u2 t2) ->
163 (pc3 c u1 u2) -> (pc3 c t1 t2).
167 Intros; Pc3Confluence; Repeat Ty0SRed; XEAuto.