Mercurial > cpdt > repo

comparison src/Hoas.v @ 167:ef485f86a7b6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Cleaning up BigStep proofs
author Adam Chlipala <adamc@hcoop.net>
date Wed, 05 Nov 2008 09:29:15 -0500
parents 73279a8aac71
children 0c5a41e9e508
comparison
equal deleted inserted replaced
166:73279a8aac71 167:ef485f86a7b6
231 | CAbs : forall dom ran (E1 : Exp1 dom ran), 231 | CAbs : forall dom ran (E1 : Exp1 dom ran),
232 Closed (Abs E1). 232 Closed (Abs E1).
233 233
234 Axiom closed : forall t (E : Exp t), Closed E. 234 Axiom closed : forall t (E : Exp t), Closed E.
235 235
236 Ltac my_subst :=
237 repeat match goal with
238 | [ x : type |- _ ] => subst x
239 end.
240
241 Ltac my_crush' := 236 Ltac my_crush' :=
242 crush; my_subst; 237 crush;
243 repeat (match goal with 238 repeat (match goal with
244 | [ H : _ |- _ ] => generalize (inj_pairT2 _ _ _ _ _ H); clear H 239 | [ H : _ |- _ ] => generalize (inj_pairT2 _ _ _ _ _ H); clear H
245 end; crush; my_subst). 240 end; crush).
241
242 Hint Extern 1 (_ = _ @ _) => simpl.
243
244 Lemma progress' : forall t (E : Exp t),
245 Closed E
246 -> Val E \/ exists E', E ==> E'.
247 induction 1; crush;
248 repeat match goal with
249 | [ H : Val _ |- _ ] => inversion H; []; clear H; my_crush'
250 end; eauto 6.
251 Qed.
252
253 Theorem progress : forall t (E : Exp t),
254 Val E \/ exists E', E ==> E'.
255 intros; apply progress'; apply closed.
256 Qed.
257
258
259 (** * Big-Step Semantics *)
260
261 Reserved Notation "E1 ===> E2" (no associativity, at level 90).
262
263 Inductive BigStep : forall t, Exp t -> Exp t -> Prop :=
264 | SConst : forall n,
265 Const n ===> Const n
266 | SPlus : forall E1 E2 n1 n2,
267 E1 ===> Const n1
268 -> E2 ===> Const n2
269 -> Plus E1 E2 ===> Const (n1 + n2)
270
271 | SApp : forall dom ran (E1 : Exp (dom --> ran)) E2 B V2 V,
272 E1 ===> Abs B
273 -> E2 ===> V2
274 -> Subst V2 B ===> V
275 -> App E1 E2 ===> V
276 | SAbs : forall dom ran (B : Exp1 dom ran),
277 Abs B ===> Abs B
278
279 where "E1 ===> E2" := (BigStep E1 E2).
280
281 Hint Constructors BigStep.
282
283 Reserved Notation "E1 ==>* E2" (no associativity, at level 90).
284
285 Inductive MultiStep : forall t, Exp t -> Exp t -> Prop :=
286 | Done : forall t (E : Exp t), E ==>* E
287 | OneStep : forall t (E E' E'' : Exp t),
288 E ==> E'
289 -> E' ==>* E''
290 -> E ==>* E''
291
292 where "E1 ==>* E2" := (MultiStep E1 E2).
293
294 Hint Constructors MultiStep.
295
296 Theorem MultiStep_trans : forall t (E1 E2 E3 : Exp t),
297 E1 ==>* E2
298 -> E2 ==>* E3
299 -> E1 ==>* E3.
300 induction 1; eauto.
301 Qed.
302
303 Theorem Big_Val : forall t (E V : Exp t),
304 E ===> V
305 -> Val V.
306 induction 1; crush.
307 Qed.
308
309 Theorem Val_Big : forall t (V : Exp t),
310 Val V
311 -> V ===> V.
312 destruct 1; crush.
313 Qed.
314
315 Hint Resolve Big_Val Val_Big.
316
317 Lemma Multi_Cong : forall t t' (C : Ctx t t'),
318 isCtx C
319 -> forall E E', E ==>* E'
320 -> C @ E ==>* C @ E'.
321 induction 2; crush; eauto.
322 Qed.
323
324 Lemma Multi_Cong' : forall t t' (C : Ctx t t') E1 E2 E E',
325 isCtx C
326 -> E1 = C @ E
327 -> E2 = C @ E'
328 -> E ==>* E'
329 -> E1 ==>* E2.
330 crush; apply Multi_Cong; auto.
331 Qed.
332
333 Hint Resolve Multi_Cong'.
334
335 Ltac mtrans E :=
336 match goal with
337 | [ |- E ==>* _ ] => fail 1
338 | _ => apply MultiStep_trans with E; [ solve [ eauto ] | eauto ]
339 end.
340
341 Theorem Big_Multi : forall t (E V : Exp t),
342 E ===> V
343 -> E ==>* V.
344 induction 1; crush; eauto;
345 repeat match goal with
346 | [ n1 : _, E2 : _ |- _ ] => mtrans (Plus (Const n1) E2)
347 | [ n1 : _, n2 : _ |- _ ] => mtrans (Plus (Const n1) (Const n2))
348 | [ B : _, E2 : _ |- _ ] => mtrans (App (Abs B) E2)
349 end.
350 Qed.
351
352 Lemma Big_Val' : forall t (V1 V2 : Exp t),
353 Val V2
354 -> V1 = V2
355 -> V1 ===> V2.
356 crush.
357 Qed.
358
359 Hint Resolve Big_Val'.
246 360
247 Ltac equate_conj F G := 361 Ltac equate_conj F G :=
248 match constr:(F, G) with 362 match constr:(F, G) with
249 | (_ ?x1, _ ?x2) => constr:(x1 = x2) 363 | (_ ?x1, _ ?x2) => constr:(x1 = x2)
250 | (_ ?x1 ?y1, _ ?x2 ?y2) => constr:(x1 = x2 /\ y1 = y2) 364 | (_ ?x1 ?y1, _ ?x2 ?y2) => constr:(x1 = x2 /\ y1 = y2)
280 end); 394 end);
281 clear H 395 clear H
282 end; my_crush'); 396 end; my_crush');
283 my_crush'. 397 my_crush'.
284 398
285 Hint Extern 1 (_ = _ @ _) => simpl.
286
287 Lemma progress' : forall t (E : Exp t),
288 Closed E
289 -> Val E \/ exists E', E ==> E'.
290 induction 1; crush;
291 repeat match goal with
292 | [ H : Val _ |- _ ] => inversion H; []; clear H; my_crush
293 end; eauto 6.
294 Qed.
295
296 Theorem progress : forall t (E : Exp t),
297 Val E \/ exists E', E ==> E'.
298 intros; apply progress'; apply closed.
299 Qed.
300
301
302 (** * Big-Step Semantics *)
303
304 Reserved Notation "E1 ===> E2" (no associativity, at level 90).
305
306 Inductive BigStep : forall t, Exp t -> Exp t -> Prop :=
307 | SConst : forall n,
308 Const n ===> Const n
309 | SPlus : forall E1 E2 n1 n2,
310 E1 ===> Const n1
311 -> E2 ===> Const n2
312 -> Plus E1 E2 ===> Const (n1 + n2)
313
314 | SApp : forall dom ran (E1 : Exp (dom --> ran)) E2 B V2 V,
315 E1 ===> Abs B
316 -> E2 ===> V2
317 -> Subst V2 B ===> V
318 -> App E1 E2 ===> V
319 | SAbs : forall dom ran (B : Exp1 dom ran),
320 Abs B ===> Abs B
321
322 where "E1 ===> E2" := (BigStep E1 E2).
323
324 Hint Constructors BigStep.
325
326 Reserved Notation "E1 ==>* E2" (no associativity, at level 90).
327
328 Inductive MultiStep : forall t, Exp t -> Exp t -> Prop :=
329 | Done : forall t (E : Exp t), E ==>* E
330 | OneStep : forall t (E E' E'' : Exp t),
331 E ==> E'
332 -> E' ==>* E''
333 -> E ==>* E''
334
335 where "E1 ==>* E2" := (MultiStep E1 E2).
336
337 Hint Constructors MultiStep.
338
339 Theorem MultiStep_trans : forall t (E1 E2 E3 : Exp t),
340 E1 ==>* E2
341 -> E2 ==>* E3
342 -> E1 ==>* E3.
343 induction 1; eauto.
344 Qed.
345
346 Theorem Big_Val : forall t (E V : Exp t),
347 E ===> V
348 -> Val V.
349 induction 1; crush.
350 Qed.
351
352 Theorem Val_Big : forall t (V : Exp t),
353 Val V
354 -> V ===> V.
355 destruct 1; crush.
356 Qed.
357
358 Hint Resolve Big_Val Val_Big.
359
360 Lemma Multi_Cong : forall t t' (C : Ctx t t'),
361 isCtx C
362 -> forall E E', E ==>* E'
363 -> C @ E ==>* C @ E'.
364 induction 2; crush; eauto.
365 Qed.
366
367 Lemma Multi_Cong' : forall t t' (C : Ctx t t') E1 E2 E E',
368 isCtx C
369 -> E1 = C @ E
370 -> E2 = C @ E'
371 -> E ==>* E'
372 -> E1 ==>* E2.
373 crush; apply Multi_Cong; auto.
374 Qed.
375
376 Hint Resolve Multi_Cong'.
377
378 Ltac mtrans E :=
379 match goal with
380 | [ |- E ==>* _ ] => fail 1
381 | _ => apply MultiStep_trans with E; [ solve [ eauto ] | eauto ]
382 end.
383
384 Theorem Big_Multi : forall t (E V : Exp t),
385 E ===> V
386 -> E ==>* V.
387 induction 1; crush; eauto;
388 repeat match goal with
389 | [ n1 : _, E2 : _ |- _ ] => mtrans (Plus (Const n1) E2)
390 | [ n1 : _, n2 : _ |- _ ] => mtrans (Plus (Const n1) (Const n2))
391 | [ B : _, E2 : _ |- _ ] => mtrans (App (Abs B) E2)
392 end.
393 Qed.
394
395 Lemma Big_Val' : forall t (V1 V2 : Exp t),
396 Val V2
397 -> V1 = V2
398 -> V1 ===> V2.
399 crush.
400 Qed.
401
402 Hint Resolve Big_Val'.
403
404 Lemma Multi_Big' : forall t (E E' : Exp t), 399 Lemma Multi_Big' : forall t (E E' : Exp t),
405 E ==> E' 400 E ==> E'
406 -> forall E'', E' ===> E'' 401 -> forall E'', E' ===> E''
407 -> E ===> E''. 402 -> E ===> E''.
408 induction 1; crush; eauto; 403 induction 1; crush; eauto;