Mercurial > cpdt > repo

comparison src/Firstorder.v @ 248:8bd90fe41acd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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.