14 Require ty0_gen_context.
17 (*#* #caption "subject reduction" #clauses *)
21 Section ty0_sred_cpr0_pr0. (**********************************************)
23 Tactic Definition IH H c2 t2 :=
24 LApply (H c2); [ Intros H_x | XEAuto ];
25 LApply H_x; [ Clear H_x; Intros H_x | XAuto ];
26 LApply (H_x t2); [ Clear H_x; Intros | XEAuto ].
28 Tactic Definition IH0 :=
30 [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 ?2 c2)->(t2:T)(pr0 ?3 t2)->(ty0 ?1 c2 t2 ?4);
31 H2: (cpr0 ?2 ?5); H3: (ty0 ?1 ?2 ?3 ?4) |- ? ] ->
34 Tactic Definition IH0c :=
36 [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 ?2 c2)->(t2:T)(pr0 ?3 t2)->(ty0 ?1 c2 t2 ?4);
37 H2: (cpr0 ?2 ?5); H3: (ty0 ?1 ?2 ?3 ?4) |- ? ] ->
38 IH H1 ?5 ?3; Clear H1.
40 Tactic Definition IH0B :=
42 [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 (CTail ?2 (Bind ?6) ?7) c2)->(t2:T)(pr0 ?3 t2)->(ty0 ?1 c2 t2 ?4);
43 H2: (cpr0 ?2 ?5); H3: (ty0 ?1 (CTail ?2 (Bind ?6) ?7) ?3 ?4) |- ? ] ->
44 IH H1 '(CTail ?5 (Bind ?6) ?7) ?3.
46 Tactic Definition IH0Bc :=
48 [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 (CTail ?2 (Bind ?6) ?7) c2)->(t2:T)(pr0 ?3 t2)->(ty0 ?1 c2 t2 ?4);
49 H2: (cpr0 ?2 ?5); H3: (ty0 ?1 (CTail ?2 (Bind ?6) ?7) ?3 ?4) |- ? ] ->
50 IH H1 '(CTail ?5 (Bind ?6) ?7) ?3; Clear H1.
52 Tactic Definition IH1 :=
54 [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 ?2 c2)->(t2:T)(pr0 ?3 t2)->(ty0 ?1 c2 t2 ?4);
55 H2: (cpr0 ?2 ?5); H3: (pr0 ?3 ?6) |- ? ] ->
58 Tactic Definition IH1c :=
60 [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 ?2 c2)->(t2:T)(pr0 ?3 t2)->(ty0 ?1 c2 t2 ?4);
61 H2: (cpr0 ?2 ?5); H3: (pr0 ?3 ?6) |- ? ] ->
62 IH H1 ?5 ?6; Clear H1.
64 Tactic Definition IH1Bc :=
66 [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 (CTail ?2 (Bind ?7) ?8) c2)->(t2:T)(pr0 ?3 t2)->(ty0 ?1 c2 t2 ?4);
67 H2: (cpr0 ?2 ?5); H3: (pr0 ?3 ?6) |- ? ] ->
68 IH H1 '(CTail ?5 (Bind ?7) ?8) ?6; Clear H1.
70 Tactic Definition IH1BLc :=
72 [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 (CTail ?2 (Bind ?7) ?8) c2)->(t2:T)(pr0 (lift ?10 ?11 ?3) t2)->(ty0 ?1 c2 t2 ?4);
73 H2: (cpr0 ?2 ?5); H3: (pr0 ?3 ?6) |- ? ] ->
74 IH H1 '(CTail ?5 (Bind ?7) ?8) '(lift ?10 ?11 ?6); Clear H1.
76 Tactic Definition IH1T :=
78 [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 ?2 c2)->(t2:T)(pr0 (TTail ?7 ?8 ?3) t2)->(ty0 ?1 c2 t2 ?4);
79 H2: (cpr0 ?2 ?5); H3: (pr0 ?3 ?6) |- ? ] ->
80 IH H1 ?5 '(TTail ?7 ?8 ?6).
82 Tactic Definition IH1T2c :=
84 [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 ?2 c2)->(t2:T)(pr0 (TTail ?7 ?8 ?3) t2)->(ty0 ?1 c2 t2 ?4);
85 H2: (cpr0 ?2 ?5); H3: (pr0 ?3 ?6); H4: (pr0 ?8 ?9) |- ? ] ->
86 IH H1 ?5 '(TTail ?7 ?9 ?6); Clear H1.
88 Tactic Definition IH3B :=
90 [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 (CTail ?2 (Bind ?7) ?8) c2)->(t2:T)(pr0 ?3 t2)->(ty0 ?1 c2 t2 ?4);
91 H2: (cpr0 ?2 ?5); H3: (pr0 ?3 ?6); H4: (pr0 ?8 ?9) |- ? ] ->
92 IH H1 '(CTail ?5 (Bind ?7) ?9) ?6.
96 (*#* #caption "base case" *)
97 (*#* #cap #cap c1, c2 #alpha t1 in T, t2 in T1, t in T2 *)
99 Theorem ty0_sred_cpr0_pr0 : (g:?; c1:?; t1,t:?) (ty0 g c1 t1 t) ->
100 (c2:?) (wf0 g c2) -> (cpr0 c1 c2) ->
101 (t2:?) (pr0 t1 t2) -> (ty0 g c2 t2 t).
105 Intros until 1; XElim H; Intros.
106 (* case 1 : ty0_conv *)
107 IH1c; IH0c; EApply ty0_conv; XEAuto.
108 (* case 2 : ty0_sort *)
110 (* case 3 : ty0_abbr *)
111 Inversion H5; Cpr0Drop; IH1c; XEAuto.
112 (* case 4 : ty0_abst *)
113 Intros; Inversion H5; Cpr0Drop; IH0; IH1.
115 [ EApply ty0_lift; [ Idtac | XAuto | XEAuto ]
117 | EApply pc3_lift ]; XEAuto.
118 (* case 5 : ty0_bind *)
119 Intros; Inversion H7; Clear H7.
120 (* case 5.1 : pr0_refl *)
122 EApply ty0_bind; XEAuto.
123 (* case 5.2 : pr0_cont *)
124 IH0; IH0B; Ty0Correct; IH3B; Ty0Correct.
125 EApply ty0_conv; [ EApply ty0_bind | EApply ty0_bind | Idtac ]; XEAuto.
126 (* case 5.3 : pr0_delta *)
127 Rewrite <- H8 in H1; Rewrite <- H8 in H2;
128 Rewrite <- H8 in H3; Rewrite <- H8 in H4; Clear H8 b.
129 IH0; IH0B; Ty0Correct; IH3B; Ty0Correct.
130 EApply ty0_conv; [ EApply ty0_bind | EApply ty0_bind | Idtac ]; XEAuto.
131 (* case 5.4 : pr0_zeta *)
132 Rewrite <- H11 in H1; Rewrite <- H11 in H2; Clear H8 H9 H10 H11 b0 t2 t7 u0.
133 IH0; IH1BLc; Move H3 after H8; IH0Bc; Ty0Correct; Move H8 after H4; Clear H H0 H1 H3 H6 c c1 t t1;
135 (* case 5.4.1 : Abbr *)
136 Ty0GenContext; Subst1Gen; LiftGen; Rewrite H in H1; Clear H x0.
138 [ EApply ty0_bind; XEAuto | XEAuto
140 EApply (pr3_t (TTail (Bind Abbr) u (lift (1) (0) x1))); XEAuto ].
141 (* case 5.4.2 : Abst *)
143 (* case 5.4.3 : Void *)
144 Ty0GenContext; Rewrite H0; Rewrite H0 in H2; Clear H0 t3.
145 LiftGen; Rewrite <- H in H1; Clear H x0.
146 EApply ty0_conv; [ EApply ty0_bind; XEAuto | XEAuto | XAuto ].
147 (* case 6 : ty0_appl *)
148 Intros; Inversion H5; Clear H5.
149 (* case 6.1 : pr0_refl *)
150 IH0c; IH0c; EApply ty0_appl; XEAuto.
151 (* case 6.2 : pr0_cont *)
152 Clear H6 H7 H8 H9 c1 k t t1 t2 t3 u1.
153 IH0; Ty0Correct; Ty0GenBase; IH1c; IH0; IH1c.
155 [ EApply ty0_appl; [ XEAuto | EApply ty0_bind; XEAuto ]
156 | EApply ty0_appl; XEAuto
158 (* case 6.3 : pr0_beta *)
159 Rewrite <- H7 in H1; Rewrite <- H7 in H2; Clear H6 H7 H9 c1 t t1 t2 v v1.
160 IH1T; IH0c; Ty0Correct; Ty0GenBase; IH0; IH1c.
161 Move H5 after H13; Ty0GenBase; Pc3Gen; Repeat CSub0Ty0.
163 [ Apply ty0_appl; [ Idtac | EApply ty0_bind ]
165 | Apply (pc3_t (TTail (Bind Abbr) v2 t0))
167 (* case 6.4 : pr0_delta *)
168 Rewrite <- H7 in H1; Rewrite <- H7 in H2; Clear H6 H7 H11 c1 t t1 t2 v v1.
169 IH1T2c; Clear H1; Ty0Correct; NonLinear; Ty0GenBase; IH1; IH0c.
170 Move H5 after H1; Ty0GenBase; Pc3Gen; Rewrite lift_bind in H0.
171 Move H1 after H0; Ty0Lift b u2; Rewrite lift_bind in H17.
174 [ Apply ty0_appl; [ Idtac | EApply ty0_bind ]; XEAuto
177 | EApply ty0_appl; [ EApply ty0_lift | EApply ty0_conv ]
178 | EApply ty0_appl; [ EApply ty0_lift | EApply ty0_bind ]
181 Rewrite <- lift_bind; Apply pc3_pc1;
182 Apply (pc1_u (TTail (Flat Appl) v2 (TTail (Bind b) u2 (lift (1) (0) (TTail (Bind Abst) u t0))))); XAuto.
183 (* case 7 : ty0_cast *)
184 Intros; Inversion H5; Clear H5.
185 (* case 7.1 : pr0_refl *)
186 IH0c; IH0c; EApply ty0_cast; XEAuto.
187 (* case 7.2 : pr0_cont *)
188 Clear H6 H7 H8 H9 c1 k u1 t t1 t4 t5.
192 | EApply ty0_cast; [ EApply ty0_conv; XEAuto | XEAuto ]
194 (* case 7.3 : pr0_eps *)
198 End ty0_sred_cpr0_pr0.
200 Section ty0_sred_pr3. (**********************************************)
202 Theorem ty0_sred_pr1 : (c:?; t1,t2:?) (pr1 t1 t2) ->
203 (g:?; t:?) (ty0 g c t1 t) ->
205 Intros until 1; XElim H; Intros.
209 EApply H1; EApply ty0_sred_cpr0_pr0; XEAuto.
212 Theorem ty0_sred_pr2 : (c:?; t1,t2:?) (pr2 c t1 t2) ->
213 (g:?; t:?) (ty0 g c t1 t) ->
215 Intros until 1; XElim H; Intros.
216 (* case 1 : pr2_pr0 *)
217 EApply ty0_sred_cpr0_pr0; XEAuto.
224 (*#* #caption "general case" *)
225 (*#* #cap #cap c #alpha t1 in T, t2 in T1, t in T2 *)
227 Theorem ty0_sred_pr3 : (c:?; t1,t2:?) (pr3 c t1 t2) ->
228 (g:?; t:?) (ty0 g c t1 t) ->
233 Intros until 1; XElim H; Intros.
237 EApply H1; EApply ty0_sred_pr2; XEAuto.
242 Tactic Definition Ty0SRed :=
244 | [ H1: (pr3 ?1 ?2 ?3); H2: (ty0 ?4 ?1 ?2 ?5) |- ? ] ->
245 LApply (ty0_sred_pr3 ?1 ?2 ?3); [ Intros H_x | XAuto ];
246 LApply (H_x ?4 ?5); [ Clear H2 H_x; Intros | XAuto ].