Mercurial > cpdt > repo
comparison src/Hoas.v @ 254:e3c3b7ef5901
Done prosifying Hoas
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Wed, 16 Dec 2009 13:16:44 -0500 |
parents | 0d77577e5ac0 |
children | 2c88fc1dbe33 |
comparison
equal
deleted
inserted
replaced
253:0d77577e5ac0 | 254:e3c3b7ef5901 |
---|---|
458 ]] *) | 458 ]] *) |
459 | 459 |
460 | 460 |
461 (** * A Type Soundness Proof *) | 461 (** * A Type Soundness Proof *) |
462 | 462 |
463 Reserved Notation "E1 ==> E2" (no associativity, at level 90). | 463 (** With [Subst] defined, there are few surprises encountered in defining a standard small-step, call-by-value semantics for our object language. We begin by classifying a subset of expressions as values. *) |
464 | 464 |
465 Inductive Val : forall t, Exp t -> Prop := | 465 Inductive Val : forall t, Exp t -> Prop := |
466 | VConst : forall n, Val (Const n) | 466 | VConst : forall n, Val (Const n) |
467 | VAbs : forall dom ran (B : Exp1 dom ran), Val (Abs B). | 467 | VAbs : forall dom ran (B : Exp1 dom ran), Val (Abs B). |
468 | 468 |
469 Hint Constructors Val. | 469 Hint Constructors Val. |
470 | |
471 (** Since this language is more complicated than the one we considered in the chapter on first-order encodings, we will use explicit evaluation contexts to define the semantics. A value of type [Ctx t u] is a context that yields an expression of type [u] when filled by an expression of type [t]. We have one context for each position of the [App] and [Plus] constructors. *) | |
470 | 472 |
471 Inductive Ctx : type -> type -> Type := | 473 Inductive Ctx : type -> type -> Type := |
472 | AppCong1 : forall (dom ran : type), | 474 | AppCong1 : forall (dom ran : type), |
473 Exp dom -> Ctx (dom --> ran) ran | 475 Exp dom -> Ctx (dom --> ran) ran |
474 | AppCong2 : forall (dom ran : type), | 476 | AppCong2 : forall (dom ran : type), |
475 Exp (dom --> ran) -> Ctx dom ran | 477 Exp (dom --> ran) -> Ctx dom ran |
476 | PlusCong1 : Exp Nat -> Ctx Nat Nat | 478 | PlusCong1 : Exp Nat -> Ctx Nat Nat |
477 | PlusCong2 : Exp Nat -> Ctx Nat Nat. | 479 | PlusCong2 : Exp Nat -> Ctx Nat Nat. |
478 | 480 |
481 (** A judgment characterizes when contexts are valid, enforcing the standard call-by-value restriction that certain positions must hold values. *) | |
482 | |
479 Inductive isCtx : forall t1 t2, Ctx t1 t2 -> Prop := | 483 Inductive isCtx : forall t1 t2, Ctx t1 t2 -> Prop := |
480 | IsApp1 : forall dom ran (X : Exp dom), isCtx (AppCong1 ran X) | 484 | IsApp1 : forall dom ran (X : Exp dom), isCtx (AppCong1 ran X) |
481 | IsApp2 : forall dom ran (F : Exp (dom --> ran)), Val F -> isCtx (AppCong2 F) | 485 | IsApp2 : forall dom ran (F : Exp (dom --> ran)), Val F -> isCtx (AppCong2 F) |
482 | IsPlus1 : forall E2, isCtx (PlusCong1 E2) | 486 | IsPlus1 : forall E2, isCtx (PlusCong1 E2) |
483 | IsPlus2 : forall E1, Val E1 -> isCtx (PlusCong2 E1). | 487 | IsPlus2 : forall E1, Val E1 -> isCtx (PlusCong2 E1). |
488 | |
489 (** A simple definition implements plugging a context with a specific expression. *) | |
484 | 490 |
485 Definition plug t1 t2 (C : Ctx t1 t2) : Exp t1 -> Exp t2 := | 491 Definition plug t1 t2 (C : Ctx t1 t2) : Exp t1 -> Exp t2 := |
486 match C with | 492 match C with |
487 | AppCong1 _ _ X => fun F => App F X | 493 | AppCong1 _ _ X => fun F => App F X |
488 | AppCong2 _ _ F => fun X => App F X | 494 | AppCong2 _ _ F => fun X => App F X |
489 | PlusCong1 E2 => fun E1 => Plus E1 E2 | 495 | PlusCong1 E2 => fun E1 => Plus E1 E2 |
490 | PlusCong2 E1 => fun E2 => Plus E1 E2 | 496 | PlusCong2 E1 => fun E2 => Plus E1 E2 |
491 end. | 497 end. |
492 | 498 |
493 Infix "@" := plug (no associativity, at level 60). | 499 Infix "@" := plug (no associativity, at level 60). |
500 | |
501 (** Finally, we have the step relation itself, which combines our ingredients in the standard way. In the congruence rule, we introduce the extra variable [E1] and its associated equality to make the rule easier for [eauto] to apply. *) | |
502 | |
503 Reserved Notation "E1 ==> E2" (no associativity, at level 90). | |
494 | 504 |
495 Inductive Step : forall t, Exp t -> Exp t -> Prop := | 505 Inductive Step : forall t, Exp t -> Exp t -> Prop := |
496 | Beta : forall dom ran (B : Exp1 dom ran) (X : Exp dom), | 506 | Beta : forall dom ran (B : Exp1 dom ran) (X : Exp dom), |
497 Val X | 507 Val X |
498 -> App (Abs B) X ==> Subst X B | 508 -> App (Abs B) X ==> Subst X B |
507 where "E1 ==> E2" := (Step E1 E2). | 517 where "E1 ==> E2" := (Step E1 E2). |
508 | 518 |
509 Hint Constructors isCtx Step. | 519 Hint Constructors isCtx Step. |
510 | 520 |
511 (* EX: Prove type soundness. *) | 521 (* EX: Prove type soundness. *) |
522 | |
523 (** To prove type soundness for this semantics, we need to overcome one crucial obstacle. Standard proofs use induction on the structure of typing derivations. Our encoding mixes typing derivations with expression syntax, so we want to induct over expression structure. Our expressions are represented as functions, which do not, in general, admit induction in Coq. However, because of our use of parametric polymorphism, we know that our expressions do, in fact, have inductive structure. In particular, every closed value of [Exp] type must belong to the following relation. *) | |
512 | 524 |
513 (* begin thide *) | 525 (* begin thide *) |
514 Inductive Closed : forall t, Exp t -> Prop := | 526 Inductive Closed : forall t, Exp t -> Prop := |
515 | CConst : forall n, | 527 | CConst : forall n, |
516 Closed (Const n) | 528 Closed (Const n) |
523 -> Closed E2 | 535 -> Closed E2 |
524 -> Closed (App E1 E2) | 536 -> Closed (App E1 E2) |
525 | CAbs : forall dom ran (E1 : Exp1 dom ran), | 537 | CAbs : forall dom ran (E1 : Exp1 dom ran), |
526 Closed (Abs E1). | 538 Closed (Abs E1). |
527 | 539 |
540 (** How can we prove such a fact? It probably cannot be established in Coq without axioms. Rather, one would have to establish it metatheoretically, reasoning informally outside of Coq. For now, we assert the fact as an axiom. The later chapter on intensional transformations shows one approach to removing the need for an axiom. *) | |
541 | |
528 Axiom closed : forall t (E : Exp t), Closed E. | 542 Axiom closed : forall t (E : Exp t), Closed E. |
543 | |
544 (** The usual progress and preservation theorems are now very easy to prove. In fact, preservation is implicit in our dependently-typed definition of [Step]. This is a huge win, because we avoid completely the theorem about substitution and typing that made up the bulk of each proof in the chapter on first-order encodings. The progress theorem yields to a few lines of automation. | |
545 | |
546 We define a slight variant of [crush] which also looks for chances to use the theorem [inj_pair2] on hypotheses. This theorem deals with an artifact of the way that [inversion] works on dependently-typed hypotheses. *) | |
529 | 547 |
530 Ltac my_crush' := | 548 Ltac my_crush' := |
531 crush; | 549 crush; |
532 repeat (match goal with | 550 repeat (match goal with |
533 | [ H : _ |- _ ] => generalize (inj_pairT2 _ _ _ _ _ H); clear H | 551 | [ H : _ |- _ ] => generalize (inj_pair2 _ _ _ _ _ H); clear H |
534 end; crush). | 552 end; crush). |
535 | 553 |
536 Hint Extern 1 (_ = _ @ _) => simpl. | 554 Hint Extern 1 (_ = _ @ _) => simpl. |
555 | |
556 (** This is the point where we need to do induction over functions, in the form of expressions [E]. The judgment [Closed] provides the perfect framework; we induct over [Closed] derivations. *) | |
537 | 557 |
538 Lemma progress' : forall t (E : Exp t), | 558 Lemma progress' : forall t (E : Exp t), |
539 Closed E | 559 Closed E |
540 -> Val E \/ exists E', E ==> E'. | 560 -> Val E \/ exists E', E ==> E'. |
541 induction 1; crush; | 561 induction 1; crush; |
542 repeat match goal with | 562 repeat match goal with |
543 | [ H : Val _ |- _ ] => inversion H; []; clear H; my_crush' | 563 | [ H : Val _ |- _ ] => inversion H; []; clear H; my_crush' |
544 end; eauto 6. | 564 end; eauto 6. |
545 Qed. | 565 Qed. |
546 | 566 |
567 (** Our final proof of progress makes one top-level use of the axiom [closed] that we asserted above. *) | |
568 | |
547 Theorem progress : forall t (E : Exp t), | 569 Theorem progress : forall t (E : Exp t), |
548 Val E \/ exists E', E ==> E'. | 570 Val E \/ exists E', E ==> E'. |
549 intros; apply progress'; apply closed. | 571 intros; apply progress'; apply closed. |
550 Qed. | 572 Qed. |
551 (* end thide *) | 573 (* end thide *) |
552 | 574 |
553 | 575 |
554 (** * Big-Step Semantics *) | 576 (** * Big-Step Semantics *) |
577 | |
578 (** Another standard exercise in operational semantics is proving the equivalence of small-step and big-step semantics. We can carry out this exercise for our PHOAS lambda calculus. Most of the steps are just as pleasant as in the previous section, but things get complicated near to the end. | |
579 | |
580 We must start by defining the big-step semantics itself. The definition is completely standard. *) | |
555 | 581 |
556 Reserved Notation "E1 ===> E2" (no associativity, at level 90). | 582 Reserved Notation "E1 ===> E2" (no associativity, at level 90). |
557 | 583 |
558 Inductive BigStep : forall t, Exp t -> Exp t -> Prop := | 584 Inductive BigStep : forall t, Exp t -> Exp t -> Prop := |
559 | SConst : forall n, | 585 | SConst : forall n, |
575 | 601 |
576 Hint Constructors BigStep. | 602 Hint Constructors BigStep. |
577 | 603 |
578 (* EX: Prove the equivalence of the small- and big-step semantics. *) | 604 (* EX: Prove the equivalence of the small- and big-step semantics. *) |
579 | 605 |
606 (** To prove a crucial intermediate lemma, we will want to name the transitive-reflexive closure of the small-step relation. *) | |
607 | |
580 (* begin thide *) | 608 (* begin thide *) |
581 Reserved Notation "E1 ==>* E2" (no associativity, at level 90). | 609 Reserved Notation "E1 ==>* E2" (no associativity, at level 90). |
582 | 610 |
583 Inductive MultiStep : forall t, Exp t -> Exp t -> Prop := | 611 Inductive MultiStep : forall t, Exp t -> Exp t -> Prop := |
584 | Done : forall t (E : Exp t), E ==>* E | 612 | Done : forall t (E : Exp t), E ==>* E |
589 | 617 |
590 where "E1 ==>* E2" := (MultiStep E1 E2). | 618 where "E1 ==>* E2" := (MultiStep E1 E2). |
591 | 619 |
592 Hint Constructors MultiStep. | 620 Hint Constructors MultiStep. |
593 | 621 |
622 (** A few basic properties of evaluation and values admit easy proofs. *) | |
623 | |
594 Theorem MultiStep_trans : forall t (E1 E2 E3 : Exp t), | 624 Theorem MultiStep_trans : forall t (E1 E2 E3 : Exp t), |
595 E1 ==>* E2 | 625 E1 ==>* E2 |
596 -> E2 ==>* E3 | 626 -> E2 ==>* E3 |
597 -> E1 ==>* E3. | 627 -> E1 ==>* E3. |
598 induction 1; eauto. | 628 induction 1; eauto. |
609 -> V ===> V. | 639 -> V ===> V. |
610 destruct 1; crush. | 640 destruct 1; crush. |
611 Qed. | 641 Qed. |
612 | 642 |
613 Hint Resolve Big_Val Val_Big. | 643 Hint Resolve Big_Val Val_Big. |
644 | |
645 (** Another useful property deals with pushing multi-step evaluation inside of contexts. *) | |
614 | 646 |
615 Lemma Multi_Cong : forall t t' (C : Ctx t t'), | 647 Lemma Multi_Cong : forall t t' (C : Ctx t t'), |
616 isCtx C | 648 isCtx C |
617 -> forall E E', E ==>* E' | 649 -> forall E E', E ==>* E' |
618 -> C @ E ==>* C @ E'. | 650 -> C @ E ==>* C @ E'. |
628 crush; apply Multi_Cong; auto. | 660 crush; apply Multi_Cong; auto. |
629 Qed. | 661 Qed. |
630 | 662 |
631 Hint Resolve Multi_Cong'. | 663 Hint Resolve Multi_Cong'. |
632 | 664 |
665 (** Unrestricted use of transitivity of [==>*] can lead to very large [eauto] search spaces, which has very inconvenient efficiency consequences. Instead, we define a special tactic [mtrans] that tries applying transitivity with a particular intermediate expression. *) | |
666 | |
633 Ltac mtrans E := | 667 Ltac mtrans E := |
634 match goal with | 668 match goal with |
635 | [ |- E ==>* _ ] => fail 1 | 669 | [ |- E ==>* _ ] => fail 1 |
636 | _ => apply MultiStep_trans with E; [ solve [ eauto ] | eauto ] | 670 | _ => apply MultiStep_trans with E; [ solve [ eauto ] | eauto ] |
637 end. | 671 end. |
672 | |
673 (** With [mtrans], we can give a reasonably short proof of one direction of the equivalence between big-step and small-step semantics. We include proof cases specific to rules of the big-step semantics, since leaving the details to [eauto] would lead to a very slow proof script. The use of [solve] in [mtrans]'s definition keeps us from going down unfruitful paths. *) | |
638 | 674 |
639 Theorem Big_Multi : forall t (E V : Exp t), | 675 Theorem Big_Multi : forall t (E V : Exp t), |
640 E ===> V | 676 E ===> V |
641 -> E ==>* V. | 677 -> E ==>* V. |
642 induction 1; crush; eauto; | 678 induction 1; crush; eauto; |
645 | [ n1 : _, n2 : _ |- _ ] => mtrans (Plus (Const n1) (Const n2)) | 681 | [ n1 : _, n2 : _ |- _ ] => mtrans (Plus (Const n1) (Const n2)) |
646 | [ B : _, E2 : _ |- _ ] => mtrans (App (Abs B) E2) | 682 | [ B : _, E2 : _ |- _ ] => mtrans (App (Abs B) E2) |
647 end. | 683 end. |
648 Qed. | 684 Qed. |
649 | 685 |
686 (** We are almost ready to prove the other direction of the equivalence. First, we wrap an earlier lemma in a form that will work better with [eauto]. *) | |
687 | |
650 Lemma Big_Val' : forall t (V1 V2 : Exp t), | 688 Lemma Big_Val' : forall t (V1 V2 : Exp t), |
651 Val V2 | 689 Val V2 |
652 -> V1 = V2 | 690 -> V1 = V2 |
653 -> V1 ===> V2. | 691 -> V1 ===> V2. |
654 crush. | 692 crush. |
655 Qed. | 693 Qed. |
656 | 694 |
657 Hint Resolve Big_Val'. | 695 Hint Resolve Big_Val'. |
696 | |
697 (** Now we build some quite involved tactic support for reasoning about equalities over PHOAS terms. First, we will call [equate_conj F G] to determine the consequences of an equality [F = G]. When [F = f e_1 ... e_n] and [G = f e'_1 ... e'_n], [equate_conj] will return a conjunction [e_1 = e'_1 /\ ... /\ e_n = e'_n]. We hardcode a pattern for each value of [n] from 1 to 5. *) | |
658 | 698 |
659 Ltac equate_conj F G := | 699 Ltac equate_conj F G := |
660 match constr:(F, G) with | 700 match constr:(F, G) with |
661 | (_ ?x1, _ ?x2) => constr:(x1 = x2) | 701 | (_ ?x1, _ ?x2) => constr:(x1 = x2) |
662 | (_ ?x1 ?y1, _ ?x2 ?y2) => constr:(x1 = x2 /\ y1 = y2) | 702 | (_ ?x1 ?y1, _ ?x2 ?y2) => constr:(x1 = x2 /\ y1 = y2) |
664 | (_ ?x1 ?y1 ?z1 ?u1, _ ?x2 ?y2 ?z2 ?u2) => | 704 | (_ ?x1 ?y1 ?z1 ?u1, _ ?x2 ?y2 ?z2 ?u2) => |
665 constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2) | 705 constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2) |
666 | (_ ?x1 ?y1 ?z1 ?u1 ?v1, _ ?x2 ?y2 ?z2 ?u2 ?v2) => | 706 | (_ ?x1 ?y1 ?z1 ?u1 ?v1, _ ?x2 ?y2 ?z2 ?u2 ?v2) => |
667 constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2 /\ v1 = v2) | 707 constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2 /\ v1 = v2) |
668 end. | 708 end. |
709 | |
710 (** The main tactic is [my_crush], which generalizes our earlier [my_crush'] by performing inversion on hypotheses that equate PHOAS terms. Coq's built-in [inversion] is only designed to be useful on equalities over inductive types. PHOAS terms are functions, so [inversion] is not very helpful on them. To perform the equivalent of [discriminate], we instantiate the terms with [var] as [fun _ => unit] and then appeal to normal [discriminate]. This eliminates some contradictory cases. To perform the equivalent of [injection], we must consider all possible [var] instantiations. Some fairly intricate logic strings together these elements. The details are not worth discussing, since our conclusion will be that one should avoid dealing with proofs of facts like this one. *) | |
669 | 711 |
670 Ltac my_crush := | 712 Ltac my_crush := |
671 my_crush'; | 713 my_crush'; |
672 repeat (match goal with | 714 repeat (match goal with |
673 | [ H : ?F = ?G |- _ ] => | 715 | [ H : ?F = ?G |- _ ] => |
694 end); | 736 end); |
695 clear H | 737 clear H |
696 end; my_crush'); | 738 end; my_crush'); |
697 my_crush'. | 739 my_crush'. |
698 | 740 |
741 (** With that complicated tactic available, the proof of the main lemma is straightforward. *) | |
742 | |
699 Lemma Multi_Big' : forall t (E E' : Exp t), | 743 Lemma Multi_Big' : forall t (E E' : Exp t), |
700 E ==> E' | 744 E ==> E' |
701 -> forall E'', E' ===> E'' | 745 -> forall E'', E' ===> E'' |
702 -> E ===> E''. | 746 -> E ===> E''. |
703 induction 1; crush; eauto; | 747 induction 1; crush; eauto; |
709 end. | 753 end. |
710 Qed. | 754 Qed. |
711 | 755 |
712 Hint Resolve Multi_Big'. | 756 Hint Resolve Multi_Big'. |
713 | 757 |
758 (** The other direction of the overall equivalence follows as an easy corollary. *) | |
759 | |
714 Theorem Multi_Big : forall t (E V : Exp t), | 760 Theorem Multi_Big : forall t (E V : Exp t), |
715 E ==>* V | 761 E ==>* V |
716 -> Val V | 762 -> Val V |
717 -> E ===> V. | 763 -> E ===> V. |
718 induction 1; crush; eauto. | 764 induction 1; crush; eauto. |
719 Qed. | 765 Qed. |
720 (* end thide *) | 766 (* end thide *) |
767 | |
768 (** The lesson here is that working directly with PHOAS terms can easily lead to extremely intricate proofs. It is usually a better idea to stick to inductive proofs about %\textit{%#<i>#instantiated#</i>#%}% PHOAS terms; in the case of this example, that means proofs about [exp] instead of [Exp]. Such results can usually be wrapped into results about [Exp] without further induction. Different theorems demand different variants of this underlying advice, and we will consider several of them in the chapters to come. *) |