Mercurial > cpdt > repo

comparison src/Firstorder.v @ 247:ecfa8eec3852

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Proved preservation for LocallyNameless
author Adam Chlipala <adamc@hcoop.net>
date Fri, 11 Dec 2009 14:05:56 -0500
parents cca30734ab40
children 8bd90fe41acd
comparison
equal deleted inserted replaced
246:cca30734ab40 247:ecfa8eec3852
626 | App e1 e2 => App (open n e1) (open n e2) 626 | App e1 e2 => App (open n e1) (open n e2)
627 | Abs e1 => Abs (open (S n) e1) 627 | Abs e1 => Abs (open (S n) e1)
628 end. 628 end.
629 End open. 629 End open.
630 630
631 Inductive notFreeIn (x : free_var) : exp -> Prop := 631 Fixpoint freeVars (e : exp) : list free_var :=
632 | NfConst : forall c, notFreeIn x (Const c) 632 match e with
633 | NfFreeVar : forall y, y <> x -> notFreeIn x (FreeVar y) 633 | Const _ => nil
634 | NfBoundVar : forall y, notFreeIn x (BoundVar y) 634 | FreeVar x => x :: nil
635 | NfApp : forall e1 e2, notFreeIn x e1 -> notFreeIn x e2 -> notFreeIn x (App e1 e2) 635 | BoundVar _ => nil
636 | NfAbs : forall e1, (forall y, y <> x -> notFreeIn x (open y O e1)) -> notFreeIn x (Abs e1). 636 | App e1 e2 => freeVars e1 ++ freeVars e2
637 637 | Abs e1 => freeVars e1
638 Hint Constructors notFreeIn. 638 end.
639 639
640 Inductive hasType : ctx -> exp -> type -> Prop := 640 Inductive hasType : ctx -> exp -> type -> Prop :=
641 | TConst : forall G b, 641 | TConst : forall G b,
642 G |-e Const b : Bool 642 G |-e Const b : Bool
643 | TFreeVar : forall G v t, 643 | TFreeVar : forall G v t,
645 -> G |-e FreeVar v : t 645 -> G |-e FreeVar v : t
646 | TApp : forall G e1 e2 dom ran, 646 | TApp : forall G e1 e2 dom ran,
647 G |-e e1 : dom --> ran 647 G |-e e1 : dom --> ran
648 -> G |-e e2 : dom 648 -> G |-e e2 : dom
649 -> G |-e App e1 e2 : ran 649 -> G |-e App e1 e2 : ran
650 | TAbs : forall G e' dom ran, 650 | TAbs : forall G e' dom ran L,
651 (forall x, notFreeIn x e' -> (x, dom) :: G |-e open x O e' : ran) 651 (forall x, ~In x L -> (x, dom) :: G |-e open x O e' : ran)
652 -> G |-e Abs e' : dom --> ran 652 -> G |-e Abs e' : dom --> ran
653 653
654 where "G |-e e : t" := (hasType G e t). 654 where "G |-e e : t" := (hasType G e t).
655 655
656 Hint Constructors hasType. 656 Hint Constructors hasType.
657 657
658 (** We prove roughly the same weakening theorems as before. *) 658 Lemma lookup_push : forall G G' x t x' t',
659 659 (forall x t, G |-v x : t -> G' |-v x : t)
660 Lemma weaken_lookup : forall G' v t G, 660 -> (x, t) :: G |-v x' : t'
661 G |-v v : t 661 -> (x, t) :: G' |-v x' : t'.
662 -> G ++ G' |-v v : t. 662 inversion 2; crush.
663 Qed.
664
665 Hint Resolve lookup_push.
666
667 Theorem weaken_hasType : forall G e t,
668 G |-e e : t
669 -> forall G', (forall x t, G |-v x : t -> G' |-v x : t)
670 -> G' |-e e : t.
671 induction 1; crush; eauto.
672 Qed.
673
674 Hint Resolve weaken_hasType.
675
676 Inductive lclosed : nat -> exp -> Prop :=
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
685 Lemma lclosed_S : forall x e n,
686 lclosed n (open x n e)
687 -> lclosed (S n) e.
688 induction e; inversion 1; crush;
689 repeat (match goal with
690 | [ _ : context[if ?E then _ else _] |- _ ] => destruct E
691 end; crush).
692 Qed.
693
694 Hint Resolve lclosed_S.
695
696 Lemma lclosed_weaken : forall n e,
697 lclosed n e
698 -> forall n', n' >= n
699 -> lclosed n' e.
663 induction 1; crush. 700 induction 1; crush.
664 Qed. 701 Qed.
665 702
666 Hint Resolve weaken_lookup. 703 Hint Resolve lclosed_weaken.
667 704 Hint Extern 1 (_ >= _) => omega.
668 Theorem weaken_hasType' : forall G' G e t, 705
706 Open Scope string_scope.
707
708 Fixpoint primes (n : nat) : string :=
709 match n with
710 | O => "x"
711 | S n' => primes n' ++ "'"
712 end.
713
714 Check fold_left.
715
716 Fixpoint sumLengths (L : list free_var) : nat :=
717 match L with
718 | nil => O
719 | x :: L' => String.length x + sumLengths L'
720 end.
721 Definition fresh (L : list free_var) := primes (sumLengths L).
722
723 Theorem freshOk' : forall x L, String.length x > sumLengths L
724 -> ~In x L.
725 induction L; crush.
726 Qed.
727
728 Lemma length_app : forall s2 s1, String.length (s1 ++ s2) = String.length s1 + String.length s2.
729 induction s1; crush.
730 Qed.
731
732 Hint Rewrite length_app : cpdt.
733
734 Lemma length_primes : forall n, String.length (primes n) = S n.
735 induction n; crush.
736 Qed.
737
738 Hint Rewrite length_primes : cpdt.
739
740 Theorem freshOk : forall L, ~In (fresh L) L.
741 intros; apply freshOk'; unfold fresh; crush.
742 Qed.
743
744 Hint Resolve freshOk.
745
746 Lemma hasType_lclosed : forall G e t,
669 G |-e e : t 747 G |-e e : t
670 -> G ++ G' |-e e : t. 748 -> lclosed O e.
671 induction 1; crush; eauto. 749 induction 1; eauto.
672 Qed. 750 Qed.
673 751
674 Theorem weaken_hasType : forall e t, 752 Lemma lclosed_open : forall n e, lclosed n e
675 nil |-e e : t 753 -> forall x, open x n e = e.
676 -> forall G', G' |-e e : t. 754 induction 1; crush;
677 intros; change G' with (nil ++ G'); 755 repeat (match goal with
678 eapply weaken_hasType'; eauto. 756 | [ |- context[if ?E then _ else _] ] => destruct E
679 Qed. 757 end; crush).
680 758 Qed.
681 Hint Resolve weaken_hasType. 759
760 Hint Resolve lclosed_open hasType_lclosed.
761
762 Open Scope list_scope.
763
764 Lemma In_app1 : forall T (x : T) ls2 ls1,
765 In x ls1
766 -> In x (ls1 ++ ls2).
767 induction ls1; crush.
768 Qed.
769
770 Lemma In_app2 : forall T (x : T) ls2 ls1,
771 In x ls2
772 -> In x (ls1 ++ ls2).
773 induction ls1; crush.
774 Qed.
775
776 Hint Resolve In_app1 In_app2.
682 777
683 Section subst. 778 Section subst.
684 Variable x : free_var. 779 Variable x : free_var.
685 Variable e1 : exp. 780 Variable e1 : exp.
686 781
690 | FreeVar x' => if string_dec x' x then e1 else e2 785 | FreeVar x' => if string_dec x' x then e1 else e2
691 | BoundVar _ => e2 786 | BoundVar _ => e2
692 | App e1 e2 => App (subst e1) (subst e2) 787 | App e1 e2 => App (subst e1) (subst e2)
693 | Abs e' => Abs (subst e') 788 | Abs e' => Abs (subst e')
694 end. 789 end.
790
791 Variable xt : type.
792
793 Definition disj x (G : ctx) := In x (map (@fst _ _) G) -> False.
794 Infix "#" := disj (no associativity, at level 90).
795
796 Lemma lookup_disj' : forall t G1,
797 G1 |-v x : t
798 -> forall G, x # G
799 -> G1 = G ++ (x, xt) :: nil
800 -> t = xt.
801 unfold disj; induction 1; crush;
802 match goal with
803 | [ _ : _ :: _ = ?G0 ++ _ |- _ ] => destruct G0
804 end; crush; eauto.
805 Qed.
806
807 Lemma lookup_disj : forall t G,
808 x # G
809 -> G ++ (x, xt) :: nil |-v x : t
810 -> t = xt.
811 intros; eapply lookup_disj'; eauto.
812 Qed.
813
814 Lemma lookup_ne' : forall G1 v t,
815 G1 |-v v : t
816 -> forall G, G1 = G ++ (x, xt) :: nil
817 -> v <> x
818 -> G |-v v : t.
819 induction 1; crush;
820 match goal with
821 | [ _ : _ :: _ = ?G0 ++ _ |- _ ] => destruct G0
822 end; crush.
823 Qed.
824
825 Lemma lookup_ne : forall G v t,
826 G ++ (x, xt) :: nil |-v v : t
827 -> v <> x
828 -> G |-v v : t.
829 intros; eapply lookup_ne'; eauto.
830 Qed.
831
832 Hint Extern 1 (_ |-e _ : _) =>
833 match goal with
834 | [ H1 : _, H2 : _ |- _ ] => rewrite (lookup_disj H1 H2)
835 end.
836 Hint Resolve lookup_ne.
837
838 Hint Extern 1 (@eq exp _ _) => f_equal.
839
840 Lemma open_subst : forall x0 e' n,
841 lclosed n e1
842 -> x <> x0
843 -> open x0 n (subst e') = subst (open x0 n e').
844 induction e'; crush;
845 repeat (match goal with
846 | [ |- context[if ?E then _ else _] ] => destruct E
847 end; crush); eauto 6.
848 Qed.
849
850 Hint Rewrite open_subst : cpdt.
851
852 Lemma disj_push : forall x0 (t : type) G,
853 x # G
854 -> x <> x0
855 -> x # (x0, t) :: G.
856 unfold disj; crush.
857 Qed.
858
859 Hint Immediate disj_push.
860
861 Lemma lookup_cons : forall x0 dom G x1 t,
862 G |-v x1 : t
863 -> x0 # G
864 -> (x0, dom) :: G |-v x1 : t.
865 unfold disj; induction 1; crush;
866 match goal with
867 | [ H : _ |-v _ : _ |- _ ] => inversion H
868 end; crush.
869 Qed.
870
871 Hint Resolve lookup_cons.
872 Hint Unfold disj.
873
874 Lemma hasType_subst' : forall G1 e t,
875 G1 |-e e : t
876 -> forall G, G1 = G ++ (x, xt) :: nil
877 -> x # G
878 -> G |-e e1 : xt
879 -> G |-e subst e : t.
880 induction 1; crush; eauto.
881
882 destruct (string_dec v x); crush.
883
884 apply TAbs with (x :: L ++ map (@fst _ _) G0); crush; eauto 7.
885 apply H0; eauto 6.
886 Qed.
887
888 Theorem hasType_subst : forall e t,
889 (x, xt) :: nil |-e e : t
890 -> nil |-e e1 : xt
891 -> nil |-e subst e : t.
892 intros; eapply hasType_subst'; eauto.
893 Qed.
695 End subst. 894 End subst.
696 895
697 896 Hint Resolve hasType_subst.
698 Notation "[ x ~> e1 ] e2" := (subst x e1 e2) (no associativity, at level 80). 897
898 Notation "[ x ~> e1 ] e2" := (subst x e1 e2) (no associativity, at level 60).
699 899
700 Inductive val : exp -> Prop := 900 Inductive val : exp -> Prop :=
701 | VConst : forall b, val (Const b) 901 | VConst : forall b, val (Const b)
702 | VAbs : forall e, val (Abs e). 902 | VAbs : forall e, val (Abs e).
703 903
704 Hint Constructors val. 904 Hint Constructors val.
705 905
706 Reserved Notation "e1 ==> e2" (no associativity, at level 90). 906 Reserved Notation "e1 ==> e2" (no associativity, at level 90).
707 907
708 Inductive step : exp -> exp -> Prop := 908 Inductive step : exp -> exp -> Prop :=
709 | Beta : forall x e1 e2, 909 | Beta : forall e1 e2 x,
710 val e2 910 val e2
711 -> notFreeIn x e1 911 -> ~In x (freeVars e1)
712 -> App (Abs e1) e2 ==> [x ~> e2] (open x O e1) 912 -> App (Abs e1) e2 ==> [x ~> e2] (open x O e1)
713 | Cong1 : forall e1 e2 e1', 913 | Cong1 : forall e1 e2 e1',
714 e1 ==> e1' 914 e1 ==> e1'
715 -> App e1 e2 ==> App e1' e2 915 -> App e1 e2 ==> App e1' e2
716 | Cong2 : forall e1 e2 e2', 916 | Cong2 : forall e1 e2 e2',
719 -> App e1 e2 ==> App e1 e2' 919 -> App e1 e2 ==> App e1 e2'
720 920
721 where "e1 ==> e2" := (step e1 e2). 921 where "e1 ==> e2" := (step e1 e2).
722 922
723 Hint Constructors step. 923 Hint Constructors step.
724
725 Open Scope string_scope.
726
727 Fixpoint vlen (e : exp) : nat :=
728 match e with
729 | Const _ => 0
730 | FreeVar x => String.length x
731 | BoundVar _ => 0
732 | App e1 e2 => vlen e1 + vlen e2
733 | Abs e1 => vlen e1
734 end.
735
736 Opaque le_lt_dec.
737
738 Hint Extern 1 (@eq exp _ _) => f_equal.
739
740 Lemma open_comm : forall x1 x2 e n1 n2,
741 open x1 n1 (open x2 (S n2 + n1) e)
742 = open x2 (n2 + n1) (open x1 n1 e).
743 induction e; crush;
744 repeat (match goal with
745 | [ |- context[if ?E then _ else _] ] => destruct E
746 end; crush).
747
748 replace (S (n2 + n1)) with (n2 + S n1); auto.
749 Qed.
750
751 Hint Rewrite plus_0_r : cpdt.
752
753 Lemma open_comm0 : forall x1 x2 e n,
754 open x1 0 (open x2 (S n) e)
755 = open x2 n (open x1 0 e).
756 intros; generalize (open_comm x1 x2 e 0 n); crush.
757 Qed.
758
759 Hint Extern 1 (notFreeIn _ (open _ 0 (open _ (S _) _))) => rewrite open_comm0.
760
761 Lemma notFreeIn_open : forall x y,
762 x <> y
763 -> forall e,
764 notFreeIn x e
765 -> forall n, notFreeIn x (open y n e).
766 induction 2; crush;
767 repeat (match goal with
768 | [ |- context[if ?E then _ else _] ] => destruct E
769 end; crush).
770 Qed.
771
772 Hint Resolve notFreeIn_open.
773
774 Lemma infVar : forall x y, String.length x > String.length y
775 -> y <> x.
776 intros; destruct (string_dec x y); intros; subst; crush.
777 Qed.
778
779 Hint Resolve infVar.
780
781 Lemma inf' : forall x e, String.length x > vlen e -> notFreeIn x e.
782 induction e; crush; eauto.
783 Qed.
784
785 Fixpoint primes (n : nat) : string :=
786 match n with
787 | O => "x"
788 | S n' => primes n' ++ "'"
789 end.
790
791 Lemma length_app : forall s2 s1, String.length (s1 ++ s2) = String.length s1 + String.length s2.
792 induction s1; crush.
793 Qed.
794
795 Hint Rewrite length_app : cpdt.
796
797 Lemma length_primes : forall n, String.length (primes n) = S n.
798 induction n; crush.
799 Qed.
800
801 Hint Rewrite length_primes : cpdt.
802
803 Lemma inf : forall e, exists x, notFreeIn x e.
804 intro; exists (primes (vlen e)); apply inf'; crush.
805 Qed.
806
807 Lemma progress_Abs : forall e1 e2,
808 val e2
809 -> exists e', App (Abs e1) e2 ==> e'.
810 intros; destruct (inf e1); eauto.
811 Qed.
812
813 Hint Resolve progress_Abs.
814 924
815 Lemma progress' : forall G e t, G |-e e : t 925 Lemma progress' : forall G e t, G |-e e : t
816 -> G = nil 926 -> G = nil
817 -> val e \/ exists e', e ==> e'. 927 -> val e \/ exists e', e ==> e'.
818 induction 1; crush; eauto; 928 induction 1; crush; eauto;
827 Theorem progress : forall e t, nil |-e e : t 937 Theorem progress : forall e t, nil |-e e : t
828 -> val e \/ exists e', e ==> e'. 938 -> val e \/ exists e', e ==> e'.
829 intros; eapply progress'; eauto. 939 intros; eapply progress'; eauto.
830 Qed. 940 Qed.
831 941
832 (*Lemma preservation' : forall G e t, G |-e e : t 942 Lemma alpha_open : forall x1 x2 e1 e2 n,
943 ~In x1 (freeVars e2)
944 -> ~In x2 (freeVars e2)
945 -> [x1 ~> e1](open x1 n e2) = [x2 ~> e1](open x2 n e2).
946 induction e2; crush;
947 repeat (match goal with
948 | [ |- context[if ?E then _ else _] ] => destruct E
949 end; crush).
950 Qed.
951
952 Lemma freshOk_app1 : forall L1 L2,
953 ~ In (fresh (L1 ++ L2)) L1.
954 intros; generalize (freshOk (L1 ++ L2)); crush.
955 Qed.
956
957 Lemma freshOk_app2 : forall L1 L2,
958 ~ In (fresh (L1 ++ L2)) L2.
959 intros; generalize (freshOk (L1 ++ L2)); crush.
960 Qed.
961
962 Hint Resolve freshOk_app1 freshOk_app2.
963
964 Lemma preservation' : forall G e t, G |-e e : t
833 -> G = nil 965 -> G = nil
834 -> forall e', e ==> e' 966 -> forall e', e ==> e'
835 -> nil |-e e' : t. 967 -> nil |-e e' : t.
836 induction 1; inversion 2; crush; eauto; 968 induction 1; inversion 2; crush; eauto;
837 match goal with 969 match goal with
838 | [ H : _ |-e Abs _ : _ |- _ ] => inversion H 970 | [ H : _ |-e Abs _ : _ |- _ ] => inversion H
839 end; eauto. 971 end; eauto.
972
973 rewrite (alpha_open x (fresh (L ++ freeVars e0))); eauto.
840 Qed. 974 Qed.
841 975
842 Theorem preservation : forall e t, nil |-e e : t 976 Theorem preservation : forall e t, nil |-e e : t
843 -> forall e', e ==> e' 977 -> forall e', e ==> e'
844 -> nil |-e e' : t. 978 -> nil |-e e' : t.
845 intros; eapply preservation'; eauto. 979 intros; eapply preservation'; eauto.
846 Qed.*) 980 Qed.
847 981
848 End LocallyNameless. 982 End LocallyNameless.