Mercurial > cpdt > repo

comparison src/Hoas.v @ 165:cf60d8dc57c9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
About to remove Cfold stuff
author Adam Chlipala <adamc@hcoop.net>
date Wed, 05 Nov 2008 08:56:11 -0500
parents 391ccedd0568
children 73279a8aac71
comparison
equal deleted inserted replaced
164:391ccedd0568 165:cf60d8dc57c9
440 | [ xt : type |- _ ] => 440 | [ xt : type |- _ ] =>
441 rewrite (@fold_Subst xt) in * 441 rewrite (@fold_Subst xt) in *
442 end; 442 end;
443 autorewrite with fold in *. 443 autorewrite with fold in *.
444 444
445 Lemma cfold_thorough : forall var t (e : exp var t),
446 cfold (cfold e) = cfold e.
447 induction e; crush; try (f_equal; ext_eq; eauto);
448 match goal with
449 | [ e1 : exp _ Nat, e2 : exp _ Nat |- _ ] =>
450 dep_destruct (cfold e1); crush;
451 dep_destruct (cfold e2); crush
452 end.
453 Qed.
454
455 Lemma Cfold_thorough : forall t (E : Exp t),
456 Cfold (Cfold E) = Cfold E.
457 intros; unfold Cfold, Exp; ext_eq;
458 apply cfold_thorough.
459 Qed.
460
461 Hint Resolve Cfold_thorough.
462
463 Section eq_arg.
464 Variable A : Type.
465 Variable B : A -> Type.
466
467 Variable x : A.
468
469 Variables f g : forall x, B x.
470 Hypothesis Heq : f = g.
471
472 Theorem eq_arg : f x = g x.
473 congruence.
474 Qed.
475 End eq_arg.
476
477 Implicit Arguments eq_arg [A B f g].
478
479 Lemma Cfold_Subst_thorough : forall t1 (V : Exp t1) t2 (B : Exp1 t1 t2),
480 Subst (Cfold V) (Cfold1 B) = Cfold (Subst (Cfold V) (Cfold1 B)).
481
482 Lemma Cfold_Step_thorough' : forall t (E V : Exp t),
483 E ===> V
484 -> forall E', E = Cfold E'
485 -> Cfold V = V.
486 induction 1; crush.
487 apply IHBigStep3 with (Subst V2 B).
488
489 generalize (closed E'); inversion 1; my_crush.
490
491 generalize (eq_arg (fun _ => Set) H2); ssimp.
492 dep_destruct (cfold (E0 (fun _ => Set))); try discriminate;
493 dep_destruct (cfold (E3 (fun _ => Set))); discriminate.
494
495 ssimp; my_crush.
496
497 rewrite <- (IHBigStep2 _ (refl_equal _)).
498 generalize (IHBigStep1 _ (refl_equal _)).
499 my_crush.
500 ssimp.
501 assert (B = Cfold1 B).
502 generalize H2; clear_all; my_crush.
503 unfold Exp1; ext_eq.
504 generalize (eq_arg x H2); injection 1; my_crush.
505
506 rewrite H8.
507
508
509 my_crush.
510
511 Lemma Cfold_thorough : forall t (E V : Exp t),
512 Cfold E ===> V
513 -> V = Cfold V.
514
445 Lemma Cfold_Subst' : forall t (E V : Exp t), 515 Lemma Cfold_Subst' : forall t (E V : Exp t),
446 E ===> V 516 E ===> V
447 -> forall t' B (V' : Exp t') V'', E = Cfold (Subst V' B) 517 -> forall t' B (V' : Exp t') V'', E = Cfold (Subst V' B)
448 -> V = Cfold V'' 518 -> V = Cfold V''
449 -> Closed1 B 519 -> Closed1 B
464 match goal with 534 match goal with
465 | [ |- _ ===> ?F ] => 535 | [ |- _ ===> ?F ] =>
466 replace F with (fun var => cfold (Abs' (fun x : var _ => B var x))) 536 replace F with (fun var => cfold (Abs' (fun x : var _ => B var x)))
467 end. 537 end.
468 apply IHBigStep1; auto. 538 apply IHBigStep1; auto.
539 ssimp.
469 apply cheat. 540 apply cheat.
470 reflexivity. 541 reflexivity.
471 542
472 replace V2 with (Cfold V2). 543 replace V2 with (Cfold V2).
473 unfold Cfold, Subst. 544 unfold Cfold, Subst.
495 Hint Resolve Cfold_Subst. 566 Hint Resolve Cfold_Subst.
496 567
497 Theorem Cfold_correct : forall t (E V : Exp t), 568 Theorem Cfold_correct : forall t (E V : Exp t),
498 E ===> V 569 E ===> V
499 -> Cfold E ===> Cfold V. 570 -> Cfold E ===> Cfold V.
500 induction 1; unfold Cfold in *; crush; ssimp; eauto. 571 induction 1; crush; ssimp; eauto.
501 572
502 change ((fun H1 : type -> Type => 573 change ((fun H1 : type -> Type =>
503 match Cfold E1 H1 with 574 match Cfold E1 H1 with
504 | Const' n3 => 575 | Const' n3 =>
505 match Cfold E2 H1 with 576 match Cfold E2 H1 with