Mercurial > cpdt > repo

comparison src/Firstorder.v @ 155:b31ca896f211

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Removed G2 everywhere
author Adam Chlipala <adamc@hcoop.net>
date Sun, 02 Nov 2008 13:25:42 -0500
parents 358dcb6e08f2
children be15ed0a8bae
comparison
equal deleted inserted replaced
154:358dcb6e08f2 155:b31ca896f211
111 -> forall G', G' # G 111 -> forall G', G' # G
112 -> G' ++ G |-v x : t. 112 -> G' ++ G |-v x : t.
113 induction G' as [ | [x' t'] tl ]; crush; eauto 9. 113 induction G' as [ | [x' t'] tl ]; crush; eauto 9.
114 Qed. 114 Qed.
115 115
116 Lemma weaken_lookup : forall G2 x t G', 116 Lemma weaken_lookup : forall x t G' G1,
117 G' # G2 117 G1 |-v x : t
118 -> forall G1, G1 ++ G2 |-v x : t 118 -> G1 ++ G' |-v x : t.
119 -> G1 ++ G' ++ G2 |-v x : t.
120 Hint Resolve weaken_lookup'. 119 Hint Resolve weaken_lookup'.
121 120
122 induction G1 as [ | [x' t'] tl ]; crush; 121 induction G1 as [ | [x' t'] tl ]; crush;
123 match goal with 122 match goal with
124 | [ H : _ |-v _ : _ |- _ ] => inversion H; crush 123 | [ H : _ |-v _ : _ |- _ ] => inversion H; crush
125 end. 124 end.
126 Qed. 125 Qed.
127 126
128 Hint Resolve weaken_lookup. 127 Hint Resolve weaken_lookup.
129 128
130 Lemma hasType_push : forall x t G1 G2 e t',
131 ((x, t) :: G1) ++ G2 |-e e : t'
132 -> (x, t) :: G1 ++ G2 |-e e : t'.
133 trivial.
134 Qed.
135
136 Hint Resolve hasType_push.
137
138 Theorem weaken_hasType' : forall G' G e t, 129 Theorem weaken_hasType' : forall G' G e t,
139 G |-e e : t 130 G |-e e : t
140 -> forall G1 G2, G = G1 ++ G2 131 -> G ++ G' |-e e : t.
141 -> G' # G2
142 -> G1 ++ G' ++ G2 |-e e : t.
143 induction 1; crush; eauto. 132 induction 1; crush; eauto.
144 Qed. 133 Qed.
145 134
146 Theorem weaken_hasType : forall G e t, 135 Theorem weaken_hasType : forall e t,
147 G |-e e : t 136 nil |-e e : t
148 -> forall G', G' # G 137 -> forall G', G' |-e e : t.
149 -> G' ++ G |-e e : t. 138 intros; change G' with (nil ++ G');
150 intros; change (G' ++ G) with (nil ++ G' ++ G);
151 eapply weaken_hasType'; eauto. 139 eapply weaken_hasType'; eauto.
152 Qed. 140 Qed.
153 141
154 Theorem weaken_hasType_closed : forall e t, 142 Theorem weaken_hasType_closed : forall e t,
155 nil |-e e : t 143 nil |-e e : t
156 -> forall G, G |-e e : t. 144 -> forall G, G |-e e : t.
157 intros; rewrite (app_nil_end G); apply weaken_hasType; auto. 145 intros; rewrite (app_nil_end G); apply weaken_hasType; auto.
158 Qed. 146 Qed.
159 147
160 Theorem weaken_hasType1 : forall G e t, 148 Theorem weaken_hasType1 : forall e t,
161 G |-e e : t 149 nil |-e e : t
162 -> forall x t', x ## G 150 -> forall x t', (x, t') :: nil |-e e : t.
163 -> (x, t') :: G |-e e : t. 151 intros; change ((x, t') :: nil) with (((x, t') :: nil) ++ nil);
164 intros; change ((x, t') :: G) with (((x, t') :: nil) ++ G); 152 apply weaken_hasType; crush.
165 apply weaken_hasType; crush;
166 match goal with
167 | [ H : (_, _) = (_, _) |- _ ] => injection H
168 end; crush; eauto.
169 Qed. 153 Qed.
170 154
171 Hint Resolve weaken_hasType_closed weaken_hasType1. 155 Hint Resolve weaken_hasType_closed weaken_hasType1.
172 156
173 Section subst. 157 Section subst.
196 -> (x, xt) :: G2 |-v x' : t 180 -> (x, xt) :: G2 |-v x' : t
197 -> t = xt. 181 -> t = xt.
198 inversion 2; crush; elimtype False; eauto. 182 inversion 2; crush; elimtype False; eauto.
199 Qed. 183 Qed.
200 184
201 Lemma subst_lookup : forall x' t G2, 185 Lemma subst_lookup : forall x' t,
202 x <> x' 186 x <> x'
203 -> forall G1, G1 ++ (x, xt) :: G2 |-v x' : t 187 -> forall G1, G1 ++ (x, xt) :: nil |-v x' : t
204 -> G1 ++ G2 |-v x' : t. 188 -> G1 |-v x' : t.
205 induction G1 as [ | [x'' t'] tl ]; crush; 189 induction G1 as [ | [x'' t'] tl ]; crush;
206 match goal with 190 match goal with
207 | [ H : _ |-v _ : _ |- _ ] => inversion H 191 | [ H : _ |-v _ : _ |- _ ] => inversion H
208 end; crush. 192 end; crush.
209 Qed. 193 Qed.
210 194
211 Hint Resolve subst_lookup. 195 Hint Resolve subst_lookup.
212 196
213 Lemma subst_lookup'' : forall G2 x' t, 197 Lemma subst_lookup'' : forall x' t G1,
214 x' ## G2 198 x' ## G1
215 -> forall G1, x' ## G1 199 -> G1 ++ (x, xt) :: nil |-v x' : t
216 -> G1 ++ (x, xt) :: G2 |-v x' : t 200 -> t = xt.
217 -> t = xt.
218 Hint Resolve subst_lookup'. 201 Hint Resolve subst_lookup'.
219 202
220 induction G1 as [ | [x'' t'] tl ]; crush; eauto; 203 induction G1 as [ | [x'' t'] tl ]; crush; eauto;
221 match goal with 204 match goal with
222 | [ H : _ |-v _ : _ |- _ ] => inversion H 205 | [ H : _ |-v _ : _ |- _ ] => inversion H
223 end; crush; elimtype False; eauto. 206 end; crush; elimtype False; eauto;
224 Qed. 207 match goal with
225 208 | [ H : nil |-v _ : _ |- _ ] => inversion H
226 Implicit Arguments subst_lookup'' [G2 x' t G1]. 209 end.
210 Qed.
211
212 Implicit Arguments subst_lookup'' [x' t G1].
227 213
228 Lemma disjoint_cons : forall x x' t (G : ctx), 214 Lemma disjoint_cons : forall x x' t (G : ctx),
229 x ## G 215 x ## G
230 -> x' <> x 216 -> x' <> x
231 -> x ## (x', t) :: G. 217 -> x ## (x', t) :: G.
235 end; crush. 221 end; crush.
236 Qed. 222 Qed.
237 223
238 Hint Resolve disjoint_cons. 224 Hint Resolve disjoint_cons.
239 225
240 Lemma shadow_lookup : forall G2 v t t' G1, 226 Lemma shadow_lookup : forall v t t' G1,
241 G1 |-v x : t' 227 G1 |-v x : t'
242 -> G1 ++ (x, xt) :: G2 |-v v : t 228 -> G1 ++ (x, xt) :: nil |-v v : t
243 -> G1 ++ G2 |-v v : t. 229 -> G1 |-v v : t.
244 induction G1 as [ | [x'' t''] tl ]; crush; 230 induction G1 as [ | [x'' t''] tl ]; crush;
245 match goal with 231 match goal with
246 | [ H : nil |-v _ : _ |- _ ] => inversion H 232 | [ H : nil |-v _ : _ |- _ ] => inversion H
247 | [ H1 : _ |-v _ : _, H2 : _ |-v _ : _ |- _ ] => 233 | [ H1 : _ |-v _ : _, H2 : _ |-v _ : _ |- _ ] =>
248 inversion H1; crush; inversion H2; crush 234 inversion H1; crush; inversion H2; crush
249 end. 235 end.
250 Qed. 236 Qed.
251 237
252 Lemma shadow_hasType' : forall G2 G e t, 238 Lemma shadow_hasType' : forall G e t,
253 G |-e e : t 239 G |-e e : t
254 -> forall G1, G = G1 ++ (x, xt) :: G2 240 -> forall G1, G = G1 ++ (x, xt) :: nil
255 -> forall t'', G1 |-v x : t'' 241 -> forall t'', G1 |-v x : t''
256 -> G1 ++ G2 |-e e : t. 242 -> G1 |-e e : t.
257 Hint Resolve shadow_lookup. 243 Hint Resolve shadow_lookup.
258 244
259 induction 1; crush; eauto; 245 induction 1; crush; eauto;
260 match goal with 246 match goal with
261 | [ H : (?x0, _) :: _ ++ (x, _) :: _ |-e _ : _ |- _ ] => 247 | [ H : (?x0, _) :: _ ++ (x, _) :: _ |-e _ : _ |- _ ] =>
262 destruct (var_eq x0 x); subst; eauto 248 destruct (var_eq x0 x); subst; eauto
263 end. 249 end.
264 Qed. 250 Qed.
265 251
266 Lemma shadow_hasType : forall G1 G2 e t t'', 252 Lemma shadow_hasType : forall G1 e t t'',
267 G1 ++ (x, xt) :: G2 |-e e : t 253 G1 ++ (x, xt) :: nil |-e e : t
268 -> G1 |-v x : t'' 254 -> G1 |-v x : t''
269 -> G1 ++ G2 |-e e : t. 255 -> G1 |-e e : t.
270 intros; eapply shadow_hasType'; eauto. 256 intros; eapply shadow_hasType'; eauto.
271 Qed. 257 Qed.
272 258
273 Hint Resolve shadow_hasType. 259 Hint Resolve shadow_hasType.
274 260
275 Theorem subst_hasType : forall G e2 t, 261 Theorem subst_hasType : forall G e2 t,
276 G |-e e2 : t 262 G |-e e2 : t
277 -> forall G1 G2, G = G1 ++ (x, xt) :: G2 263 -> forall G1, G = G1 ++ (x, xt) :: nil
278 -> x ## G1 264 -> x ## G1
279 -> x ## G2 265 -> G1 |-e subst e2 : t.
280 -> G1 ++ G2 |-e subst e2 : t.
281 induction 1; crush; 266 induction 1; crush;
282 try match goal with 267 try match goal with
283 | [ |- context[if ?E then _ else _] ] => destruct E 268 | [ |- context[if ?E then _ else _] ] => destruct E
284 end; crush; eauto 6; 269 end; crush; eauto 6;
285 match goal with 270 match goal with
286 | [ H1 : x ## _, H2 : x ## _, H3 : _ |-v x : _ |- _ ] => 271 | [ H1 : x ## _, H2 : _ |-v x : _ |- _ ] =>
287 rewrite (subst_lookup'' H2 H1 H3) 272 rewrite (subst_lookup'' H1 H2)
288 end; crush. 273 end; crush.
289 Qed. 274 Qed.
290 275
291 Theorem subst_hasType_closed : forall e2 t, 276 Theorem subst_hasType_closed : forall e2 t,
292 (x, xt) :: nil |-e e2 : t 277 (x, xt) :: nil |-e e2 : t
293 -> nil |-e subst e2 : t. 278 -> nil |-e subst e2 : t.
294 intros; change (nil ++ nil |-e subst e2 : t); 279 intros; eapply subst_hasType; eauto.
295 eapply subst_hasType; eauto.
296 Qed. 280 Qed.
297 End subst. 281 End subst.
298 282
299 Hint Resolve subst_hasType_closed. 283 Hint Resolve subst_hasType_closed.
300 284
321 305
322 where "e1 ==> e2" := (step e1 e2). 306 where "e1 ==> e2" := (step e1 e2).
323 307
324 Hint Constructors step. 308 Hint Constructors step.
325 309
326 Theorem progress : forall G e t, G |-e e : t 310 Lemma progress' : forall G e t, G |-e e : t
327 -> G = nil 311 -> G = nil
328 -> val e \/ exists e', e ==> e'. 312 -> val e \/ exists e', e ==> e'.
329 induction 1; crush; eauto; 313 induction 1; crush; eauto;
330 try match goal with 314 try match goal with
331 | [ H : _ |-e _ : _ --> _ |- _ ] => inversion H 315 | [ H : _ |-e _ : _ --> _ |- _ ] => inversion H
333 repeat match goal with 317 repeat match goal with
334 | [ H : _ |- _ ] => solve [ inversion H; crush; eauto ] 318 | [ H : _ |- _ ] => solve [ inversion H; crush; eauto ]
335 end. 319 end.
336 Qed. 320 Qed.
337 321
338 Theorem preservation : forall G e t, G |-e e : t 322 Theorem progress : forall e t, nil |-e e : t
323 -> val e \/ exists e', e ==> e'.
324 intros; eapply progress'; eauto.
325 Qed.
326
327 Lemma preservation' : forall G e t, G |-e e : t
339 -> G = nil 328 -> G = nil
340 -> forall e', e ==> e' 329 -> forall e', e ==> e'
341 -> G |-e e' : t. 330 -> nil |-e e' : t.
342 induction 1; inversion 2; crush; eauto; 331 induction 1; inversion 2; crush; eauto;
343 match goal with 332 match goal with
344 | [ H : _ |-e Abs _ _ : _ |- _ ] => inversion H 333 | [ H : _ |-e Abs _ _ : _ |- _ ] => inversion H
345 end; eauto. 334 end; eauto.
346 Qed. 335 Qed.
347 336
337 Theorem preservation : forall e t, nil |-e e : t
338 -> forall e', e ==> e'
339 -> nil |-e e' : t.
340 intros; eapply preservation'; eauto.
341 Qed.
342
348 End Concrete. 343 End Concrete.