Mercurial > cpdt > repo
comparison src/Firstorder.v @ 248:8bd90fe41acd
Automated LocallyNameless
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Fri, 11 Dec 2009 15:00:42 -0500 |
parents | ecfa8eec3852 |
children | 0f45421cae21 |
comparison
equal
deleted
inserted
replaced
247:ecfa8eec3852 | 248:8bd90fe41acd |
---|---|
680 | CApp : forall n e1 e2, lclosed n e1 -> lclosed n e2 -> lclosed n (App e1 e2) | 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). | 681 | CAbs : forall n e1, lclosed (S n) e1 -> lclosed n (Abs e1). |
682 | 682 |
683 Hint Constructors lclosed. | 683 Hint Constructors lclosed. |
684 | 684 |
685 Ltac ln := crush; | |
686 repeat (match goal with | |
687 | [ |- context[if ?E then _ else _] ] => destruct E | |
688 | [ _ : context[if ?E then _ else _] |- _ ] => destruct E | |
689 end; crush); eauto. | |
690 | |
685 Lemma lclosed_S : forall x e n, | 691 Lemma lclosed_S : forall x e n, |
686 lclosed n (open x n e) | 692 lclosed n (open x n e) |
687 -> lclosed (S n) e. | 693 -> lclosed (S n) e. |
688 induction e; inversion 1; crush; | 694 induction e; inversion 1; ln. |
689 repeat (match goal with | |
690 | [ _ : context[if ?E then _ else _] |- _ ] => destruct E | |
691 end; crush). | |
692 Qed. | 695 Qed. |
693 | 696 |
694 Hint Resolve lclosed_S. | 697 Hint Resolve lclosed_S. |
695 | 698 |
696 Lemma lclosed_weaken : forall n e, | 699 Lemma lclosed_weaken : forall n e, |
709 match n with | 712 match n with |
710 | O => "x" | 713 | O => "x" |
711 | S n' => primes n' ++ "'" | 714 | S n' => primes n' ++ "'" |
712 end. | 715 end. |
713 | 716 |
714 Check fold_left. | |
715 | |
716 Fixpoint sumLengths (L : list free_var) : nat := | 717 Fixpoint sumLengths (L : list free_var) : nat := |
717 match L with | 718 match L with |
718 | nil => O | 719 | nil => O |
719 | x :: L' => String.length x + sumLengths L' | 720 | x :: L' => String.length x + sumLengths L' |
720 end. | 721 end. |
722 | |
721 Definition fresh (L : list free_var) := primes (sumLengths L). | 723 Definition fresh (L : list free_var) := primes (sumLengths L). |
722 | 724 |
723 Theorem freshOk' : forall x L, String.length x > sumLengths L | 725 Theorem freshOk' : forall x L, String.length x > sumLengths L |
724 -> ~In x L. | 726 -> ~In x L. |
725 induction L; crush. | 727 induction L; crush. |
749 induction 1; eauto. | 751 induction 1; eauto. |
750 Qed. | 752 Qed. |
751 | 753 |
752 Lemma lclosed_open : forall n e, lclosed n e | 754 Lemma lclosed_open : forall n e, lclosed n e |
753 -> forall x, open x n e = e. | 755 -> forall x, open x n e = e. |
754 induction 1; crush; | 756 induction 1; ln. |
755 repeat (match goal with | |
756 | [ |- context[if ?E then _ else _] ] => destruct E | |
757 end; crush). | |
758 Qed. | 757 Qed. |
759 | 758 |
760 Hint Resolve lclosed_open hasType_lclosed. | 759 Hint Resolve lclosed_open hasType_lclosed. |
761 | 760 |
762 Open Scope list_scope. | 761 Open Scope list_scope. |
762 | |
763 Lemma In_cons1 : forall T (x x' : T) ls, | |
764 x = x' | |
765 -> In x (x' :: ls). | |
766 crush. | |
767 Qed. | |
768 | |
769 Lemma In_cons2 : forall T (x x' : T) ls, | |
770 In x ls | |
771 -> In x (x' :: ls). | |
772 crush. | |
773 Qed. | |
763 | 774 |
764 Lemma In_app1 : forall T (x : T) ls2 ls1, | 775 Lemma In_app1 : forall T (x : T) ls2 ls1, |
765 In x ls1 | 776 In x ls1 |
766 -> In x (ls1 ++ ls2). | 777 -> In x (ls1 ++ ls2). |
767 induction ls1; crush. | 778 induction ls1; crush. |
771 In x ls2 | 782 In x ls2 |
772 -> In x (ls1 ++ ls2). | 783 -> In x (ls1 ++ ls2). |
773 induction ls1; crush. | 784 induction ls1; crush. |
774 Qed. | 785 Qed. |
775 | 786 |
776 Hint Resolve In_app1 In_app2. | 787 Lemma freshOk_app1 : forall L1 L2, |
788 ~ In (fresh (L1 ++ L2)) L1. | |
789 intros; generalize (freshOk (L1 ++ L2)); crush. | |
790 Qed. | |
791 | |
792 Lemma freshOk_app2 : forall L1 L2, | |
793 ~ In (fresh (L1 ++ L2)) L2. | |
794 intros; generalize (freshOk (L1 ++ L2)); crush. | |
795 Qed. | |
796 | |
797 Hint Resolve In_cons1 In_cons2 In_app1 In_app2. | |
777 | 798 |
778 Section subst. | 799 Section subst. |
800 Hint Resolve freshOk_app1 freshOk_app2. | |
801 | |
779 Variable x : free_var. | 802 Variable x : free_var. |
780 Variable e1 : exp. | 803 Variable e1 : exp. |
781 | 804 |
782 Fixpoint subst (e2 : exp) : exp := | 805 Fixpoint subst (e2 : exp) : exp := |
783 match e2 with | 806 match e2 with |
791 Variable xt : type. | 814 Variable xt : type. |
792 | 815 |
793 Definition disj x (G : ctx) := In x (map (@fst _ _) G) -> False. | 816 Definition disj x (G : ctx) := In x (map (@fst _ _) G) -> False. |
794 Infix "#" := disj (no associativity, at level 90). | 817 Infix "#" := disj (no associativity, at level 90). |
795 | 818 |
819 Ltac disj := crush; | |
820 match goal with | |
821 | [ _ : _ :: _ = ?G0 ++ _ |- _ ] => destruct G0 | |
822 end; crush; eauto. | |
823 | |
796 Lemma lookup_disj' : forall t G1, | 824 Lemma lookup_disj' : forall t G1, |
797 G1 |-v x : t | 825 G1 |-v x : t |
798 -> forall G, x # G | 826 -> forall G, x # G |
799 -> G1 = G ++ (x, xt) :: nil | 827 -> G1 = G ++ (x, xt) :: nil |
800 -> t = xt. | 828 -> t = xt. |
801 unfold disj; induction 1; crush; | 829 unfold disj; induction 1; disj. |
802 match goal with | |
803 | [ _ : _ :: _ = ?G0 ++ _ |- _ ] => destruct G0 | |
804 end; crush; eauto. | |
805 Qed. | 830 Qed. |
806 | 831 |
807 Lemma lookup_disj : forall t G, | 832 Lemma lookup_disj : forall t G, |
808 x # G | 833 x # G |
809 -> G ++ (x, xt) :: nil |-v x : t | 834 -> G ++ (x, xt) :: nil |-v x : t |
814 Lemma lookup_ne' : forall G1 v t, | 839 Lemma lookup_ne' : forall G1 v t, |
815 G1 |-v v : t | 840 G1 |-v v : t |
816 -> forall G, G1 = G ++ (x, xt) :: nil | 841 -> forall G, G1 = G ++ (x, xt) :: nil |
817 -> v <> x | 842 -> v <> x |
818 -> G |-v v : t. | 843 -> G |-v v : t. |
819 induction 1; crush; | 844 induction 1; disj. |
820 match goal with | |
821 | [ _ : _ :: _ = ?G0 ++ _ |- _ ] => destruct G0 | |
822 end; crush. | |
823 Qed. | 845 Qed. |
824 | 846 |
825 Lemma lookup_ne : forall G v t, | 847 Lemma lookup_ne : forall G v t, |
826 G ++ (x, xt) :: nil |-v v : t | 848 G ++ (x, xt) :: nil |-v v : t |
827 -> v <> x | 849 -> v <> x |
839 | 861 |
840 Lemma open_subst : forall x0 e' n, | 862 Lemma open_subst : forall x0 e' n, |
841 lclosed n e1 | 863 lclosed n e1 |
842 -> x <> x0 | 864 -> x <> x0 |
843 -> open x0 n (subst e') = subst (open x0 n e'). | 865 -> open x0 n (subst e') = subst (open x0 n e'). |
844 induction e'; crush; | 866 induction e'; ln. |
845 repeat (match goal with | 867 Qed. |
846 | [ |- context[if ?E then _ else _] ] => destruct E | 868 |
847 end; crush); eauto 6. | 869 Lemma hasType_open_subst : forall G x0 e t, |
848 Qed. | 870 G |-e subst (open x0 0 e) : t |
849 | 871 -> x <> x0 |
850 Hint Rewrite open_subst : cpdt. | 872 -> lclosed 0 e1 |
873 -> G |-e open x0 0 (subst e) : t. | |
874 intros; rewrite open_subst; eauto. | |
875 Qed. | |
876 | |
877 Hint Resolve hasType_open_subst. | |
851 | 878 |
852 Lemma disj_push : forall x0 (t : type) G, | 879 Lemma disj_push : forall x0 (t : type) G, |
853 x # G | 880 x # G |
854 -> x <> x0 | 881 -> x <> x0 |
855 -> x # (x0, t) :: G. | 882 -> x # (x0, t) :: G. |
856 unfold disj; crush. | 883 unfold disj; crush. |
857 Qed. | 884 Qed. |
858 | 885 |
859 Hint Immediate disj_push. | 886 Hint Resolve disj_push. |
860 | 887 |
861 Lemma lookup_cons : forall x0 dom G x1 t, | 888 Lemma lookup_cons : forall x0 dom G x1 t, |
862 G |-v x1 : t | 889 G |-v x1 : t |
863 -> x0 # G | 890 -> ~In x0 (map (@fst _ _) G) |
864 -> (x0, dom) :: G |-v x1 : t. | 891 -> (x0, dom) :: G |-v x1 : t. |
865 unfold disj; induction 1; crush; | 892 induction 1; crush; |
866 match goal with | 893 match goal with |
867 | [ H : _ |-v _ : _ |- _ ] => inversion H | 894 | [ H : _ |-v _ : _ |- _ ] => inversion H |
868 end; crush. | 895 end; crush. |
869 Qed. | 896 Qed. |
870 | 897 |
871 Hint Resolve lookup_cons. | 898 Hint Resolve lookup_cons. |
872 Hint Unfold disj. | 899 Hint Unfold disj. |
900 | |
901 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) | |
903 -> G |-e Abs e' : dom --> ran. | |
904 eauto. | |
905 Qed. | |
873 | 906 |
874 Lemma hasType_subst' : forall G1 e t, | 907 Lemma hasType_subst' : forall G1 e t, |
875 G1 |-e e : t | 908 G1 |-e e : t |
876 -> forall G, G1 = G ++ (x, xt) :: nil | 909 -> forall G, G1 = G ++ (x, xt) :: nil |
877 -> x # G | 910 -> x # G |
878 -> G |-e e1 : xt | 911 -> G |-e e1 : xt |
879 -> G |-e subst e : t. | 912 -> G |-e subst e : t. |
880 induction 1; crush; eauto. | 913 induction 1; ln; |
881 | 914 match goal with |
882 destruct (string_dec v x); crush. | 915 | [ L : list free_var, _ : ?x # _ |- _ ] => |
883 | 916 apply TAbs_specialized with L x; eauto 20 |
884 apply TAbs with (x :: L ++ map (@fst _ _) G0); crush; eauto 7. | 917 end. |
885 apply H0; eauto 6. | |
886 Qed. | 918 Qed. |
887 | 919 |
888 Theorem hasType_subst : forall e t, | 920 Theorem hasType_subst : forall e t, |
889 (x, xt) :: nil |-e e : t | 921 (x, xt) :: nil |-e e : t |
890 -> nil |-e e1 : xt | 922 -> nil |-e e1 : xt |
894 End subst. | 926 End subst. |
895 | 927 |
896 Hint Resolve hasType_subst. | 928 Hint Resolve hasType_subst. |
897 | 929 |
898 Notation "[ x ~> e1 ] e2" := (subst x e1 e2) (no associativity, at level 60). | 930 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. | |
899 | 941 |
900 Inductive val : exp -> Prop := | 942 Inductive val : exp -> Prop := |
901 | VConst : forall b, val (Const b) | 943 | VConst : forall b, val (Const b) |
902 | VAbs : forall e, val (Abs e). | 944 | VAbs : forall e, val (Abs e). |
903 | 945 |
937 Theorem progress : forall e t, nil |-e e : t | 979 Theorem progress : forall e t, nil |-e e : t |
938 -> val e \/ exists e', e ==> e'. | 980 -> val e \/ exists e', e ==> e'. |
939 intros; eapply progress'; eauto. | 981 intros; eapply progress'; eauto. |
940 Qed. | 982 Qed. |
941 | 983 |
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. | 984 Hint Resolve freshOk_app1 freshOk_app2. |
985 | |
986 Lemma hasType_alpha_open : forall G L e0 e2 x t, | |
987 ~ In x (freeVars e0) | |
988 -> 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. | |
990 intros; rewrite (alpha_open x (fresh (L ++ freeVars e0))); auto. | |
991 Qed. | |
992 | |
993 Hint Resolve hasType_alpha_open. | |
963 | 994 |
964 Lemma preservation' : forall G e t, G |-e e : t | 995 Lemma preservation' : forall G e t, G |-e e : t |
965 -> G = nil | 996 -> G = nil |
966 -> forall e', e ==> e' | 997 -> forall e', e ==> e' |
967 -> nil |-e e' : t. | 998 -> nil |-e e' : t. |
968 induction 1; inversion 2; crush; eauto; | 999 induction 1; inversion 2; crush; eauto; |
969 match goal with | 1000 match goal with |
970 | [ H : _ |-e Abs _ : _ |- _ ] => inversion H | 1001 | [ H : _ |-e Abs _ : _ |- _ ] => inversion H |
971 end; eauto. | 1002 end; eauto. |
972 | |
973 rewrite (alpha_open x (fresh (L ++ freeVars e0))); eauto. | |
974 Qed. | 1003 Qed. |
975 | 1004 |
976 Theorem preservation : forall e t, nil |-e e : t | 1005 Theorem preservation : forall e t, nil |-e e : t |
977 -> forall e', e ==> e' | 1006 -> forall e', e ==> e' |
978 -> nil |-e e' : t. | 1007 -> nil |-e e' : t. |