comparison src/Firstorder.v @ 249:0f45421cae21

Prose for LocallyNameless
author Adam Chlipala <adamc@hcoop.net>
date Fri, 11 Dec 2009 16:07:27 -0500
parents 8bd90fe41acd
children 76043a960a38
comparison
equal deleted inserted replaced
248:8bd90fe41acd 249:0f45421cae21
570 End DeBruijn. 570 End DeBruijn.
571 571
572 572
573 (** * Locally Nameless Syntax *) 573 (** * Locally Nameless Syntax *)
574 574
575 (** The most popular Coq syntax encoding today is the %\textit{%#<i>#locally nameless#</i>#%}% style, which has been around for a while but was popularized recently by Aydemir et al., following a methodology summarized in their paper "Engineering Formal Metatheory." #<a href="http://www.cis.upenn.edu/~plclub/oregon08/">#A specialized tutorial by that group#</a>#%\footnote{\url{http://www.cis.upenn.edu/~plclub/oregon08/}}% explains the approach, based on a library. In this section, we will build up all of the necessary ingredients from scratch.
576
577 The one-sentence summary of locally nameless encoding is that we represent free variables as concrete syntax does, and we represent bound variables with de Bruijn indices. Many proofs involve reasoning about terms transplanted into different free variable contexts; concrete encoding of free variables means that, to perform such a transplanting, we need no fix-up operation to adjust de Bruijn indices. At the same time, use of de Bruijn indices for local variables gives us canonical representations of expressions, with respect to the usual convention of alpha-equivalence. This makes many operations, including substitution of open terms in open terms, easier to implement.
578
579 The "Engineering Formal Metatheory" methodology involves a number of subtle design decisions, which we will describe as they appear in the latest version of our running example. *)
580
575 Module LocallyNameless. 581 Module LocallyNameless.
576 582
577 Definition free_var := string. 583 Definition free_var := string.
578 Definition bound_var := nat. 584 Definition bound_var := nat.
579 585
582 | FreeVar : free_var -> exp 588 | FreeVar : free_var -> exp
583 | BoundVar : bound_var -> exp 589 | BoundVar : bound_var -> exp
584 | App : exp -> exp -> exp 590 | App : exp -> exp -> exp
585 | Abs : exp -> exp. 591 | Abs : exp -> exp.
586 592
593 (** Note the different constructors for free vs. bound variables, and note that the lack of a variable annotation on [Abs] nodes is inherited from the de Bruijn convention. *)
594
587 Inductive type : Set := 595 Inductive type : Set :=
588 | Bool : type 596 | Bool : type
589 | Arrow : type -> type -> type. 597 | Arrow : type -> type -> type.
590 598
591 Infix "-->" := Arrow (right associativity, at level 60). 599 Infix "-->" := Arrow (right associativity, at level 60).
592 600
601 (** As typing only depends on types of free variables, our contexts borrow their form from the concrete binding example. *)
602
593 Definition ctx := list (free_var * type). 603 Definition ctx := list (free_var * type).
594
595 Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level).
596 604
597 Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level). 605 Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level).
598 606
599 Inductive lookup : ctx -> free_var -> type -> Prop := 607 Inductive lookup : ctx -> free_var -> type -> Prop :=
600 | First : forall x t G, 608 | First : forall x t G,
606 614
607 where "G |-v x : t" := (lookup G x t). 615 where "G |-v x : t" := (lookup G x t).
608 616
609 Hint Constructors lookup. 617 Hint Constructors lookup.
610 618
611 Reserved Notation "G |-e e : t" (no associativity, at level 90, e at next level). 619 (** The first unusual operation we need is %\textit{%#<i>#opening#</i>#%}%, where we replace a particular bound variable with a particular free variable. Whenever we "go under a binder," in the typing judgment or elsewhere, we choose a new free variable to replace the old bound variable of the binder. Opening implements the replacement of one by the other. It is like a specialized version of the substitution function we used for pure de Bruijn terms. *)
612 620
613 Section open. 621 Section open.
614 Variable x : free_var. 622 Variable x : free_var.
615 623
616 Fixpoint open (n : bound_var) (e : exp) : exp := 624 Fixpoint open (n : bound_var) (e : exp) : exp :=
626 | App e1 e2 => App (open n e1) (open n e2) 634 | App e1 e2 => App (open n e1) (open n e2)
627 | Abs e1 => Abs (open (S n) e1) 635 | Abs e1 => Abs (open (S n) e1)
628 end. 636 end.
629 End open. 637 End open.
630 638
639 (** We will also need to reason about an expression's set of free variables. To keep things simple, we represent sets as lists that may contain duplicates. Note how much easier this operation is to implement than over pure de Bruijn terms, since we do not need to maintain a separate numeric argument that keeps track of how deeply we have descended into the input expression. *)
640
631 Fixpoint freeVars (e : exp) : list free_var := 641 Fixpoint freeVars (e : exp) : list free_var :=
632 match e with 642 match e with
633 | Const _ => nil 643 | Const _ => nil
634 | FreeVar x => x :: nil 644 | FreeVar x => x :: nil
635 | BoundVar _ => nil 645 | BoundVar _ => nil
636 | App e1 e2 => freeVars e1 ++ freeVars e2 646 | App e1 e2 => freeVars e1 ++ freeVars e2
637 | Abs e1 => freeVars e1 647 | Abs e1 => freeVars e1
638 end. 648 end.
649
650 (** It will be useful to have a well-formedness judgment for our terms. This notion is called %\textit{%#<i>#local closure#</i>#%}%. An expression may be declared to be closed, up to a particular maximum de Bruijn index. *)
651
652 Inductive lclosed : nat -> exp -> Prop :=
653 | CConst : forall n b, lclosed n (Const b)
654 | CFreeVar : forall n v, lclosed n (FreeVar v)
655 | CBoundVar : forall n v, v < n -> lclosed n (BoundVar v)
656 | CApp : forall n e1 e2, lclosed n e1 -> lclosed n e2 -> lclosed n (App e1 e2)
657 | CAbs : forall n e1, lclosed (S n) e1 -> lclosed n (Abs e1).
658
659 Hint Constructors lclosed.
660
661 (** Now we are ready to define the typing judgment. *)
662
663 Reserved Notation "G |-e e : t" (no associativity, at level 90, e at next level).
639 664
640 Inductive hasType : ctx -> exp -> type -> Prop := 665 Inductive hasType : ctx -> exp -> type -> Prop :=
641 | TConst : forall G b, 666 | TConst : forall G b,
642 G |-e Const b : Bool 667 G |-e Const b : Bool
643 | TFreeVar : forall G v t, 668 | TFreeVar : forall G v t,
646 | TApp : forall G e1 e2 dom ran, 671 | TApp : forall G e1 e2 dom ran,
647 G |-e e1 : dom --> ran 672 G |-e e1 : dom --> ran
648 -> G |-e e2 : dom 673 -> G |-e e2 : dom
649 -> G |-e App e1 e2 : ran 674 -> G |-e App e1 e2 : ran
650 | TAbs : forall G e' dom ran L, 675 | TAbs : forall G e' dom ran L,
651 (forall x, ~In x L -> (x, dom) :: G |-e open x O e' : ran) 676 (forall x, ~ In x L -> (x, dom) :: G |-e open x O e' : ran)
652 -> G |-e Abs e' : dom --> ran 677 -> G |-e Abs e' : dom --> ran
653 678
654 where "G |-e e : t" := (hasType G e t). 679 where "G |-e e : t" := (hasType G e t).
655 680
681 (** Compared to the previous versions, only the [TAbs] rule is surprising. The rule uses %\textit{%#<i>#co-finite quantiifcation#</i>#%}%. That is, the premise of the rule quantifies over all [x] values that are not members of a finite set [L]. A proof may choose any value of [L] when applying [TAbs]. An alternate, more intuitive version of the rule would fix [L] to be [freeVars e']. It turns out that the greater flexibility of the rule above simplifies many proofs significantly. This typing judgment may be proved equivalent to the more intuitive version, though we will not carry out the proof here.
682
683 Specifially, what our version of [TAbs] says is that, to prove that [Abs e'] has a function type, we must prove that any opening of [e'] with a variable not in [L] has the proper type. For each [x] choice, we extend the context [G] in the usual way. *)
684
656 Hint Constructors hasType. 685 Hint Constructors hasType.
686
687 (** We prove a standard weakening theorem for typing, adopting a more general form than in the previous sections. *)
657 688
658 Lemma lookup_push : forall G G' x t x' t', 689 Lemma lookup_push : forall G G' x t x' t',
659 (forall x t, G |-v x : t -> G' |-v x : t) 690 (forall x t, G |-v x : t -> G' |-v x : t)
660 -> (x, t) :: G |-v x' : t' 691 -> (x, t) :: G |-v x' : t'
661 -> (x, t) :: G' |-v x' : t'. 692 -> (x, t) :: G' |-v x' : t'.
671 induction 1; crush; eauto. 702 induction 1; crush; eauto.
672 Qed. 703 Qed.
673 704
674 Hint Resolve weaken_hasType. 705 Hint Resolve weaken_hasType.
675 706
676 Inductive lclosed : nat -> exp -> Prop := 707 (** We define a simple extension of [crush] to apply in many of the lemmas that follow. *)
677 | CConst : forall n b, lclosed n (Const b)
678 | CFreeVar : forall n v, lclosed n (FreeVar v)
679 | CBoundVar : forall n v, v < n -> lclosed n (BoundVar v)
680 | CApp : forall n e1 e2, lclosed n e1 -> lclosed n e2 -> lclosed n (App e1 e2)
681 | CAbs : forall n e1, lclosed (S n) e1 -> lclosed n (Abs e1).
682
683 Hint Constructors lclosed.
684 708
685 Ltac ln := crush; 709 Ltac ln := crush;
686 repeat (match goal with 710 repeat (match goal with
687 | [ |- context[if ?E then _ else _] ] => destruct E 711 | [ |- context[if ?E then _ else _] ] => destruct E
688 | [ _ : context[if ?E then _ else _] |- _ ] => destruct E 712 | [ _ : context[if ?E then _ else _] |- _ ] => destruct E
689 end; crush); eauto. 713 end; crush); eauto.
714
715 (** Two basic properties of local closure will be useful later. *)
690 716
691 Lemma lclosed_S : forall x e n, 717 Lemma lclosed_S : forall x e n,
692 lclosed n (open x n e) 718 lclosed n (open x n e)
693 -> lclosed (S n) e. 719 -> lclosed (S n) e.
694 induction e; inversion 1; ln. 720 induction e; inversion 1; ln.
703 induction 1; crush. 729 induction 1; crush.
704 Qed. 730 Qed.
705 731
706 Hint Resolve lclosed_weaken. 732 Hint Resolve lclosed_weaken.
707 Hint Extern 1 (_ >= _) => omega. 733 Hint Extern 1 (_ >= _) => omega.
734
735 (** To prove some further properties, we need the ability to choose a variable that is disjoint from a particular finite set. We implement a specific choice function [fresh]; its details do not matter, as all we need is the final theorem about it, [freshOk]. Concretely, to choose a variable disjoint from set [L], we sum the lengths of the variable names in [L] and choose a new variable name that is one longer than that sum. This variable can be the string ["x"], followed by a number of primes equal to the sum. *)
708 736
709 Open Scope string_scope. 737 Open Scope string_scope.
710 738
711 Fixpoint primes (n : nat) : string := 739 Fixpoint primes (n : nat) : string :=
712 match n with 740 match n with
720 | x :: L' => String.length x + sumLengths L' 748 | x :: L' => String.length x + sumLengths L'
721 end. 749 end.
722 750
723 Definition fresh (L : list free_var) := primes (sumLengths L). 751 Definition fresh (L : list free_var) := primes (sumLengths L).
724 752
753 (** A few lemmas suffice to establish the correctness theorem [freshOk] for [fresh]. *)
754
725 Theorem freshOk' : forall x L, String.length x > sumLengths L 755 Theorem freshOk' : forall x L, String.length x > sumLengths L
726 -> ~In x L. 756 -> ~ In x L.
727 induction L; crush. 757 induction L; crush.
728 Qed. 758 Qed.
729 759
730 Lemma length_app : forall s2 s1, String.length (s1 ++ s2) = String.length s1 + String.length s2. 760 Lemma length_app : forall s2 s1,
761 String.length (s1 ++ s2) = String.length s1 + String.length s2.
731 induction s1; crush. 762 induction s1; crush.
732 Qed. 763 Qed.
733 764
734 Hint Rewrite length_app : cpdt. 765 Hint Rewrite length_app : cpdt.
735 766
737 induction n; crush. 768 induction n; crush.
738 Qed. 769 Qed.
739 770
740 Hint Rewrite length_primes : cpdt. 771 Hint Rewrite length_primes : cpdt.
741 772
742 Theorem freshOk : forall L, ~In (fresh L) L. 773 Theorem freshOk : forall L, ~ In (fresh L) L.
743 intros; apply freshOk'; unfold fresh; crush. 774 intros; apply freshOk'; unfold fresh; crush.
744 Qed. 775 Qed.
745 776
746 Hint Resolve freshOk. 777 Hint Resolve freshOk.
778
779 (** Now we can prove that well-typedness implies local closure. [fresh] will be used for us automatically by [eauto] in the [Abs] case, driven by the presence of [freshOk] as a hint. *)
747 780
748 Lemma hasType_lclosed : forall G e t, 781 Lemma hasType_lclosed : forall G e t,
749 G |-e e : t 782 G |-e e : t
750 -> lclosed O e. 783 -> lclosed O e.
751 induction 1; eauto. 784 induction 1; eauto.
752 Qed. 785 Qed.
753 786
787 (** An important consequence of local closure is that certain openings are idempotent. *)
788
754 Lemma lclosed_open : forall n e, lclosed n e 789 Lemma lclosed_open : forall n e, lclosed n e
755 -> forall x, open x n e = e. 790 -> forall x, open x n e = e.
756 induction 1; ln. 791 induction 1; ln.
757 Qed. 792 Qed.
758 793
759 Hint Resolve lclosed_open hasType_lclosed. 794 Hint Resolve lclosed_open hasType_lclosed.
760 795
761 Open Scope list_scope. 796 Open Scope list_scope.
797
798 (** We are now almost ready to get down to the details of substitution. First, we prove six lemmas related to treating lists as sets. *)
762 799
763 Lemma In_cons1 : forall T (x x' : T) ls, 800 Lemma In_cons1 : forall T (x x' : T) ls,
764 x = x' 801 x = x'
765 -> In x (x' :: ls). 802 -> In x (x' :: ls).
766 crush. 803 crush.
793 ~ In (fresh (L1 ++ L2)) L2. 830 ~ In (fresh (L1 ++ L2)) L2.
794 intros; generalize (freshOk (L1 ++ L2)); crush. 831 intros; generalize (freshOk (L1 ++ L2)); crush.
795 Qed. 832 Qed.
796 833
797 Hint Resolve In_cons1 In_cons2 In_app1 In_app2. 834 Hint Resolve In_cons1 In_cons2 In_app1 In_app2.
835
836 (** Now we can define our simplest substitution function yet, thanks to the fact that we only subsitute for free variables, which are distinguished syntactically from bound variables. *)
798 837
799 Section subst. 838 Section subst.
800 Hint Resolve freshOk_app1 freshOk_app2. 839 Hint Resolve freshOk_app1 freshOk_app2.
801 840
802 Variable x : free_var. 841 Variable x : free_var.
811 | Abs e' => Abs (subst e') 850 | Abs e' => Abs (subst e')
812 end. 851 end.
813 852
814 Variable xt : type. 853 Variable xt : type.
815 854
855 (** It comes in handy to define disjointness of a variable and a context differently than in previous examples. We use the standard list function [map], as well as the function [fst] for projecting the first element of a pair. We write [@fst _ _] rather than just [fst] to ask that [fst]'s implicit arguments be instantiated with inferred values. *)
856
816 Definition disj x (G : ctx) := In x (map (@fst _ _) G) -> False. 857 Definition disj x (G : ctx) := In x (map (@fst _ _) G) -> False.
817 Infix "#" := disj (no associativity, at level 90). 858 Infix "#" := disj (no associativity, at level 90).
818 859
819 Ltac disj := crush; 860 Ltac disj := crush;
820 match goal with 861 match goal with
821 | [ _ : _ :: _ = ?G0 ++ _ |- _ ] => destruct G0 862 | [ _ : _ :: _ = ?G0 ++ _ |- _ ] => destruct G0
822 end; crush; eauto. 863 end; crush; eauto.
864
865 (** Some basic properties of variable lookup will be needed on the road to our usual theorem connecting substitution and typing. *)
823 866
824 Lemma lookup_disj' : forall t G1, 867 Lemma lookup_disj' : forall t G1,
825 G1 |-v x : t 868 G1 |-v x : t
826 -> forall G, x # G 869 -> forall G, x # G
827 -> G1 = G ++ (x, xt) :: nil 870 -> G1 = G ++ (x, xt) :: nil
836 intros; eapply lookup_disj'; eauto. 879 intros; eapply lookup_disj'; eauto.
837 Qed. 880 Qed.
838 881
839 Lemma lookup_ne' : forall G1 v t, 882 Lemma lookup_ne' : forall G1 v t,
840 G1 |-v v : t 883 G1 |-v v : t
841 -> forall G, G1 = G ++ (x, xt) :: nil 884 -> forall G, G1 = G ++ (x, xt) :: nil
842 -> v <> x 885 -> v <> x
843 -> G |-v v : t. 886 -> G |-v v : t.
844 induction 1; disj. 887 induction 1; disj.
845 Qed. 888 Qed.
846 889
847 Lemma lookup_ne : forall G v t, 890 Lemma lookup_ne : forall G v t,
848 G ++ (x, xt) :: nil |-v v : t 891 G ++ (x, xt) :: nil |-v v : t
857 end. 900 end.
858 Hint Resolve lookup_ne. 901 Hint Resolve lookup_ne.
859 902
860 Hint Extern 1 (@eq exp _ _) => f_equal. 903 Hint Extern 1 (@eq exp _ _) => f_equal.
861 904
905 (** We need to know that substitution and opening commute under appropriate circumstances. *)
906
862 Lemma open_subst : forall x0 e' n, 907 Lemma open_subst : forall x0 e' n,
863 lclosed n e1 908 lclosed n e1
864 -> x <> x0 909 -> x <> x0
865 -> open x0 n (subst e') = subst (open x0 n e'). 910 -> open x0 n (subst e') = subst (open x0 n e').
866 induction e'; ln. 911 induction e'; ln.
867 Qed. 912 Qed.
913
914 (** We state a corollary of the last result which will work more smoothly with [eauto]. *)
868 915
869 Lemma hasType_open_subst : forall G x0 e t, 916 Lemma hasType_open_subst : forall G x0 e t,
870 G |-e subst (open x0 0 e) : t 917 G |-e subst (open x0 0 e) : t
871 -> x <> x0 918 -> x <> x0
872 -> lclosed 0 e1 919 -> lclosed 0 e1
874 intros; rewrite open_subst; eauto. 921 intros; rewrite open_subst; eauto.
875 Qed. 922 Qed.
876 923
877 Hint Resolve hasType_open_subst. 924 Hint Resolve hasType_open_subst.
878 925
926 (** Another lemma establishes the validity of weakening variable lookup judgments with fresh variables. *)
927
879 Lemma disj_push : forall x0 (t : type) G, 928 Lemma disj_push : forall x0 (t : type) G,
880 x # G 929 x # G
881 -> x <> x0 930 -> x <> x0
882 -> x # (x0, t) :: G. 931 -> x # (x0, t) :: G.
883 unfold disj; crush. 932 unfold disj; crush.
885 934
886 Hint Resolve disj_push. 935 Hint Resolve disj_push.
887 936
888 Lemma lookup_cons : forall x0 dom G x1 t, 937 Lemma lookup_cons : forall x0 dom G x1 t,
889 G |-v x1 : t 938 G |-v x1 : t
890 -> ~In x0 (map (@fst _ _) G) 939 -> ~ In x0 (map (@fst _ _) G)
891 -> (x0, dom) :: G |-v x1 : t. 940 -> (x0, dom) :: G |-v x1 : t.
892 induction 1; crush; 941 induction 1; crush;
893 match goal with 942 match goal with
894 | [ H : _ |-v _ : _ |- _ ] => inversion H 943 | [ H : _ |-v _ : _ |- _ ] => inversion H
895 end; crush. 944 end; crush.
896 Qed. 945 Qed.
897 946
898 Hint Resolve lookup_cons. 947 Hint Resolve lookup_cons.
899 Hint Unfold disj. 948 Hint Unfold disj.
900 949
950 (** Finally, it is useful to state a version of the [TAbs] rule specialized to the choice of [L] that is useful in our main substitution proof. *)
951
901 Lemma TAbs_specialized : forall G e' dom ran L x1, 952 Lemma TAbs_specialized : forall G e' dom ran L x1,
902 (forall x, ~In x (x1 :: L ++ map (@fst _ _) G) -> (x, dom) :: G |-e open x O e' : ran) 953 (forall x, ~ In x (x1 :: L ++ map (@fst _ _) G) -> (x, dom) :: G |-e open x O e' : ran)
903 -> G |-e Abs e' : dom --> ran. 954 -> G |-e Abs e' : dom --> ran.
904 eauto. 955 eauto.
905 Qed. 956 Qed.
957
958 (** Now we can prove the main inductive lemma in a manner similar to what worked for concrete binding. *)
906 959
907 Lemma hasType_subst' : forall G1 e t, 960 Lemma hasType_subst' : forall G1 e t,
908 G1 |-e e : t 961 G1 |-e e : t
909 -> forall G, G1 = G ++ (x, xt) :: nil 962 -> forall G, G1 = G ++ (x, xt) :: nil
910 -> x # G 963 -> x # G
914 match goal with 967 match goal with
915 | [ L : list free_var, _ : ?x # _ |- _ ] => 968 | [ L : list free_var, _ : ?x # _ |- _ ] =>
916 apply TAbs_specialized with L x; eauto 20 969 apply TAbs_specialized with L x; eauto 20
917 end. 970 end.
918 Qed. 971 Qed.
919 972
973 (** The main theorem about substitution of closed expressions follows easily. *)
974
920 Theorem hasType_subst : forall e t, 975 Theorem hasType_subst : forall e t,
921 (x, xt) :: nil |-e e : t 976 (x, xt) :: nil |-e e : t
922 -> nil |-e e1 : xt 977 -> nil |-e e1 : xt
923 -> nil |-e subst e : t. 978 -> nil |-e subst e : t.
924 intros; eapply hasType_subst'; eauto. 979 intros; eapply hasType_subst'; eauto.
925 Qed. 980 Qed.
926 End subst. 981 End subst.
927 982
928 Hint Resolve hasType_subst. 983 Hint Resolve hasType_subst.
929 984
985 (** We can define the operational semantics in almost the same way as in previous examples. *)
986
930 Notation "[ x ~> e1 ] e2" := (subst x e1 e2) (no associativity, at level 60). 987 Notation "[ x ~> e1 ] e2" := (subst x e1 e2) (no associativity, at level 60).
931
932 Lemma alpha_open : forall x1 x2 e1 e2 n,
933 ~In x1 (freeVars e2)
934 -> ~In x2 (freeVars e2)
935 -> [x1 ~> e1](open x1 n e2) = [x2 ~> e1](open x2 n e2).
936 induction e2; crush;
937 repeat (match goal with
938 | [ |- context[if ?E then _ else _] ] => destruct E
939 end; crush).
940 Qed.
941 988
942 Inductive val : exp -> Prop := 989 Inductive val : exp -> Prop :=
943 | VConst : forall b, val (Const b) 990 | VConst : forall b, val (Const b)
944 | VAbs : forall e, val (Abs e). 991 | VAbs : forall e, val (Abs e).
945 992
948 Reserved Notation "e1 ==> e2" (no associativity, at level 90). 995 Reserved Notation "e1 ==> e2" (no associativity, at level 90).
949 996
950 Inductive step : exp -> exp -> Prop := 997 Inductive step : exp -> exp -> Prop :=
951 | Beta : forall e1 e2 x, 998 | Beta : forall e1 e2 x,
952 val e2 999 val e2
953 -> ~In x (freeVars e1) 1000 -> ~ In x (freeVars e1)
954 -> App (Abs e1) e2 ==> [x ~> e2] (open x O e1) 1001 -> App (Abs e1) e2 ==> [x ~> e2] (open x O e1)
955 | Cong1 : forall e1 e2 e1', 1002 | Cong1 : forall e1 e2 e1',
956 e1 ==> e1' 1003 e1 ==> e1'
957 -> App e1 e2 ==> App e1' e2 1004 -> App e1 e2 ==> App e1' e2
958 | Cong2 : forall e1 e2 e2', 1005 | Cong2 : forall e1 e2 e2',
961 -> App e1 e2 ==> App e1 e2' 1008 -> App e1 e2 ==> App e1 e2'
962 1009
963 where "e1 ==> e2" := (step e1 e2). 1010 where "e1 ==> e2" := (step e1 e2).
964 1011
965 Hint Constructors step. 1012 Hint Constructors step.
1013
1014 (** The only interesting change is that the [Beta] rule requires identifying a fresh variable [x] to use in opening the abstraction body. We could have avoided this by implementing a more general [open] that allows substituting expressions for variables, not just variables for variables, but it simplifies the proofs to have just one general substitution function.
1015
1016 Now we are ready to prove progress and preservation. The same proof script from the last examples suffices to prove progress, though significantly different lemmas are applied for us by [eauto]. *)
966 1017
967 Lemma progress' : forall G e t, G |-e e : t 1018 Lemma progress' : forall G e t, G |-e e : t
968 -> G = nil 1019 -> G = nil
969 -> val e \/ exists e', e ==> e'. 1020 -> val e \/ exists e', e ==> e'.
970 induction 1; crush; eauto; 1021 induction 1; crush; eauto;
979 Theorem progress : forall e t, nil |-e e : t 1030 Theorem progress : forall e t, nil |-e e : t
980 -> val e \/ exists e', e ==> e'. 1031 -> val e \/ exists e', e ==> e'.
981 intros; eapply progress'; eauto. 1032 intros; eapply progress'; eauto.
982 Qed. 1033 Qed.
983 1034
1035 (** To establish preservation, it is useful to formalize a principle of sound alpha-variation. In particular, when we open an expression with a particular variable and then immediately substitute for the same variable, we can replace that variable with any other that is not free in the body of the opened expression. *)
1036
1037 Lemma alpha_open : forall x1 x2 e1 e2 n,
1038 ~ In x1 (freeVars e2)
1039 -> ~ In x2 (freeVars e2)
1040 -> [x1 ~> e1](open x1 n e2) = [x2 ~> e1](open x2 n e2).
1041 induction e2; ln.
1042 Qed.
1043
984 Hint Resolve freshOk_app1 freshOk_app2. 1044 Hint Resolve freshOk_app1 freshOk_app2.
1045
1046 (** Again it is useful to state a direct corollary which is easier to apply in proof search. *)
985 1047
986 Lemma hasType_alpha_open : forall G L e0 e2 x t, 1048 Lemma hasType_alpha_open : forall G L e0 e2 x t,
987 ~ In x (freeVars e0) 1049 ~ In x (freeVars e0)
988 -> G |-e [fresh (L ++ freeVars e0) ~> e2](open (fresh (L ++ freeVars e0)) 0 e0) : t 1050 -> G |-e [fresh (L ++ freeVars e0) ~> e2](open (fresh (L ++ freeVars e0)) 0 e0) : t
989 -> G |-e [x ~> e2](open x 0 e0) : t. 1051 -> G |-e [x ~> e2](open x 0 e0) : t.
990 intros; rewrite (alpha_open x (fresh (L ++ freeVars e0))); auto. 1052 intros; rewrite (alpha_open x (fresh (L ++ freeVars e0))); auto.
991 Qed. 1053 Qed.
992 1054
993 Hint Resolve hasType_alpha_open. 1055 Hint Resolve hasType_alpha_open.
1056
1057 (** Now the previous sections' preservation proof scripts finish the job. *)
994 1058
995 Lemma preservation' : forall G e t, G |-e e : t 1059 Lemma preservation' : forall G e t, G |-e e : t
996 -> G = nil 1060 -> G = nil
997 -> forall e', e ==> e' 1061 -> forall e', e ==> e'
998 -> nil |-e e' : t. 1062 -> nil |-e e' : t.