Mercurial > cpdt > repo

comparison src/Intensional.v @ 184:699fd70c04a7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
About to stop using JMeq
author Adam Chlipala <adamc@hcoop.net>
date Sun, 16 Nov 2008 15:04:21 -0500
parents 02569049397b
children 303e9d866597
comparison
equal deleted inserted replaced
183:02569049397b 184:699fd70c04a7
6 * The license text is available at: 6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *) 8 *)
9 9
10 (* begin hide *) 10 (* begin hide *)
11 Require Import Arith Bool String List. 11 Require Import Arith Bool String List Eqdep JMeq.
12 12
13 Require Import Axioms Tactics DepList. 13 Require Import Axioms Tactics DepList.
14 14
15 Set Implicit Arguments. 15 Set Implicit Arguments.
16
17 Infix "==" := JMeq (at level 70, no associativity).
16 (* end hide *) 18 (* end hide *)
19
20
17 21
18 22
19 (** %\chapter{Intensional Transformations}% *) 23 (** %\chapter{Intensional Transformations}% *)
20 24
21 (** TODO: Prose for this chapter *) 25 (** TODO: Prose for this chapter *)
795 Implicit Arguments packExp [var envT]. 799 Implicit Arguments packExp [var envT].
796 Implicit Arguments unpackExp [var t envT fvs]. 800 Implicit Arguments unpackExp [var t envT fvs].
797 801
798 Implicit Arguments ccExp [var t envT]. 802 Implicit Arguments ccExp [var t envT].
799 803
800 Fixpoint map_funcs var result T1 T2 (f : T1 -> T2) (fs : cfuncs var result T1) {struct fs} 804 Fixpoint map_funcs var T1 T2 (f : T1 -> T2) (fs : funcs var T1) {struct fs}
801 : cfuncs var result T2 := 805 : funcs var T2 :=
802 match fs with 806 match fs with
803 | CMain v => CMain (f v) 807 | Main v => Main (f v)
804 | CAbs _ _ e fs' => CAbs e (fun x => map_funcs f (fs' x)) 808 | Abs _ _ _ e fs' => Abs e (fun x => map_funcs f (fs' x))
805 end. 809 end.
806 810
807 Definition CcTerm' result (E : Pterm result) (Hwf : wfTerm (envT := nil) tt (E _)) : Cprog result := 811 Definition CcTerm' t (E : Source.Exp t) (Hwf : wfExp (envT := nil) tt (E _)) : Prog (ccType t) :=
808 fun _ => map_funcs (fun f => f tt) (ccTerm (E _) (envT := nil) tt Hwf). 812 fun _ => map_funcs (fun f => f tt) (ccExp (E _) (envT := nil) tt Hwf).
809 813
810 814
811 (** * Correctness *) 815 (** * Correctness *)
812 816
813 Scheme pterm_equiv_mut := Minimality for pterm_equiv Sort Prop 817 Section spliceFuncs_correct.
814 with pprimop_equiv_mut := Minimality for pprimop_equiv Sort Prop.
815
816 Section splicePrim_correct.
817 Variables result t t' : ptype.
818 Variable ps' : ctypeDenote ([< t >]) -> cprimops ctypeDenote t'.
819
820 Theorem splicePrim_correct : forall (ps : cprimops ctypeDenote t),
821 cprimopsDenote (splicePrim ps ps')
822 = cprimopsDenote (ps' (cprimopsDenote ps)).
823 induction ps; equation.
824 Qed.
825 End splicePrim_correct.
826
827 Section spliceTerm_correct.
828 Variables result t : ptype.
829 Variable e : ctypeDenote ([< t >]) -> cterm ctypeDenote result.
830 Variable k : ptypeDenote result -> bool.
831
832 Theorem spliceTerm_correct : forall (ps : cprimops ctypeDenote t),
833 ctermDenote (spliceTerm ps e) k
834 = ctermDenote (e (cprimopsDenote ps)) k.
835 induction ps; equation.
836 Qed.
837 End spliceTerm_correct.
838
839 Section spliceFuncs'_correct.
840 Variable result : ptype.
841 Variables T1 T2 : Type. 818 Variables T1 T2 : Type.
842 Variable f : T1 -> T2. 819 Variable f : T1 -> funcs typeDenote T2.
843 Variable k : ptypeDenote result -> bool. 820
844 821 Theorem spliceFuncs_correct : forall fs,
845 Theorem spliceFuncs'_correct : forall fs, 822 funcsDenote (spliceFuncs fs f)
846 cfuncsDenote (spliceFuncs' fs f) k 823 = funcsDenote (f (funcsDenote fs)).
847 = f (cfuncsDenote fs k). 824 induction fs; crush.
848 induction fs; equation.
849 Qed.
850 End spliceFuncs'_correct.
851
852 Section spliceFuncs_correct.
853 Variable result : ptype.
854 Variables T1 T2 T3 : Type.
855 Variable fs2 : cfuncs ctypeDenote result T2.
856 Variable f : T1 -> T2 -> T3.
857 Variable k : ptypeDenote result -> bool.
858
859 Hint Rewrite spliceFuncs'_correct : ltamer.
860
861 Theorem spliceFuncs_correct : forall fs1,
862 cfuncsDenote (spliceFuncs fs1 fs2 f) k
863 = f (cfuncsDenote fs1 k) (cfuncsDenote fs2 k).
864 induction fs1; equation.
865 Qed. 825 Qed.
866 End spliceFuncs_correct. 826 End spliceFuncs_correct.
867
868 Section inside_correct.
869 Variable result : ptype.
870 Variables T1 T2 : Type.
871 Variable fs2 : T1 -> cfuncs ctypeDenote result T2.
872 Variable k : ptypeDenote result -> bool.
873
874 Theorem inside_correct : forall fs1,
875 cfuncsDenote (inside fs1 fs2) k
876 = cfuncsDenote (fs2 (cfuncsDenote fs1 k)) k.
877 induction fs1; equation.
878 Qed.
879 End inside_correct.
880 827
881 828
882 Notation "var <| to" := (match to with 829 Notation "var <| to" := (match to with
883 | None => unit 830 | None => unit
884 | Some t => var ([< t >])%cc 831 | Some t => var (ccType t)
885 end) (no associativity, at level 70). 832 end) (no associativity, at level 70).
886 833
887 Section packing_correct. 834 Section packing_correct.
888 Variable result : ptype. 835 Fixpoint makeEnv (envT : list Source.type) : forall (fvs : isfree envT),
889 836 Closed.typeDenote (envType fvs)
890 Hint Rewrite splicePrim_correct spliceTerm_correct : ltamer. 837 -> envOf Closed.typeDenote fvs :=
891
892 Ltac my_matching := matching my_equation default_chooser.
893
894 Fixpoint makeEnv (envT : list ptype) : forall (fvs : isfree envT),
895 ptypeDenote (envType fvs)
896 -> envOf ctypeDenote fvs :=
897 match envT return (forall (fvs : isfree envT), 838 match envT return (forall (fvs : isfree envT),
898 ptypeDenote (envType fvs) 839 Closed.typeDenote (envType fvs)
899 -> envOf ctypeDenote fvs) with 840 -> envOf Closed.typeDenote fvs) with
900 | nil => fun _ _ => tt 841 | nil => fun _ _ => tt
901 | first :: rest => fun fvs => 842 | first :: rest => fun fvs =>
902 match fvs return (ptypeDenote (envType (envT := first :: rest) fvs) 843 match fvs return (Closed.typeDenote (envType (envT := first :: rest) fvs)
903 -> envOf (envT := first :: rest) ctypeDenote fvs) with 844 -> envOf (envT := first :: rest) Closed.typeDenote fvs) with
904 | (false, fvs') => fun env => makeEnv rest fvs' env 845 | (false, fvs') => fun env => makeEnv rest fvs' env
905 | (true, fvs') => fun env => (fst env, makeEnv rest fvs' (snd env)) 846 | (true, fvs') => fun env => (fst env, makeEnv rest fvs' (snd env))
906 end 847 end
907 end. 848 end.
908 849
909 Theorem unpackExp_correct : forall (envT : list ptype) (fvs : isfree envT) 850 Implicit Arguments makeEnv [envT fvs].
910 (ps : cprimops ctypeDenote (envType fvs)) 851
911 (e : envOf ctypeDenote fvs -> cterm ctypeDenote result) k, 852 Theorem unpackExp_correct : forall t (envT : list Source.type) (fvs : isfree envT)
912 ctermDenote (unpackExp ps e) k 853 (e1 : Closed.exp Closed.typeDenote (envType fvs))
913 = ctermDenote (e (makeEnv _ _ (cprimopsDenote ps))) k. 854 (e2 : envOf Closed.typeDenote fvs -> Closed.exp Closed.typeDenote t),
914 induction envT; my_matching. 855 Closed.expDenote (unpackExp e1 e2)
856 = Closed.expDenote (e2 (makeEnv (Closed.expDenote e1))).
857 induction envT; my_crush.
915 Qed. 858 Qed.
916 859
917 Lemma lookup_type_more : forall v2 envT (fvs : isfree envT) t b v, 860 Lemma lookup_type_more : forall v2 envT (fvs : isfree envT) t b v,
918 (v2 = length envT -> False) 861 (v2 = length envT -> False)
919 -> lookup_type v2 (envT := t :: envT) (b, fvs) = v 862 -> lookup_type v2 (envT := t :: envT) (b, fvs) = v
920 -> lookup_type v2 fvs = v. 863 -> lookup_type v2 fvs = v.
921 equation. 864 my_crush.
922 Qed. 865 Qed.
923 866
924 Lemma lookup_type_less : forall v2 t envT (fvs : isfree (t :: envT)) v, 867 Lemma lookup_type_less : forall v2 t envT (fvs : isfree (t :: envT)) v,
925 (v2 = length envT -> False) 868 (v2 = length envT -> False)
926 -> lookup_type v2 (snd fvs) = v 869 -> lookup_type v2 (snd fvs) = v
927 -> lookup_type v2 (envT := t :: envT) fvs = v. 870 -> lookup_type v2 (envT := t :: envT) fvs = v.
928 equation. 871 my_crush.
929 Qed. 872 Qed.
873
874 Hint Resolve lookup_bound_contra.
930 875
931 Lemma lookup_bound_contra_eq : forall t envT (fvs : isfree envT) v, 876 Lemma lookup_bound_contra_eq : forall t envT (fvs : isfree envT) v,
932 lookup_type v fvs = Some t 877 lookup_type v fvs = Some t
933 -> v = length envT 878 -> v = length envT
934 -> False. 879 -> False.
935 simpler; eapply lookup_bound_contra; eauto. 880 my_crush; elimtype False; eauto.
936 Defined. 881 Qed.
937 882
938 Lemma lookup_type_inner : forall result t envT v t' (fvs : isfree envT) e, 883 Lemma lookup_type_inner : forall t t' envT v t'' (fvs : isfree envT) e,
939 wfTerm (envT := t :: envT) (true, fvs) e 884 wfExp (envT := t' :: envT) (true, fvs) e
940 -> lookup_type v (snd (fvsTerm (result := result) e (t :: envT))) = Some t' 885 -> lookup_type v (snd (fvsExp (t := t) e (t' :: envT))) = Some t''
941 -> lookup_type v fvs = Some t'. 886 -> lookup_type v fvs = Some t''.
942 Hint Resolve lookup_bound_contra_eq fvsTerm_minimal 887 Hint Resolve lookup_bound_contra_eq fvsExp_minimal
943 lookup_type_more lookup_type_less. 888 lookup_type_more lookup_type_less.
944 Hint Extern 2 (Some _ = Some _) => contradictory. 889 Hint Extern 2 (Some _ = Some _) => elimtype False.
945 890
946 eauto 6. 891 eauto 6.
947 Qed. 892 Qed.
948 893
949 Lemma cast_irrel : forall T1 T2 x (H1 H2 : T1 = T2), 894 Lemma cast_irrel : forall T1 T2 x (H1 H2 : T1 = T2),
950 (x :? H1) = (x :? H2). 895 match H1 in _ = T return T with
951 equation. 896 | refl_equal => x
897 end
898 = match H2 in _ = T return T with
899 | refl_equal => x
900 end.
901 intros; generalize H1; crush;
902 repeat match goal with
903 | [ |- context[match ?pf with refl_equal => _ end] ] =>
904 rewrite (UIP_refl _ _ pf)
905 end;
906 reflexivity.
952 Qed. 907 Qed.
953 908
954 Hint Immediate cast_irrel. 909 Hint Immediate cast_irrel.
955 910
956 Lemma cast_irrel_unit : forall T1 T2 x y (H1 : T1 = T2) (H2 : unit = T2), 911 Hint Extern 3 (_ == _) =>
957 (x :? H1) = (y :? H2).
958 intros; generalize H1;
959 rewrite <- H2 in H1;
960 equation.
961 Qed.
962
963 Hint Immediate cast_irrel_unit.
964
965 Hint Extern 3 (_ = _) =>
966 match goal with 912 match goal with
967 | [ |- context[False_rect _ ?H] ] => 913 | [ |- context[False_rect _ ?H] ] =>
968 apply False_rect; exact H 914 apply False_rect; exact H
969 end. 915 end.
970 916
971 Theorem packExp_correct : forall v2 t envT (fvs1 fvs2 : isfree envT) 917 Theorem packExp_correct : forall v envT (fvs1 fvs2 : isfree envT)
972 Heq1 (Heq2 : ctypeDenote <| lookup_type v2 fvs2 = ptypeDenote t)
973 Hincl env, 918 Hincl env,
974 (lookup ctypeDenote v2 env :? Heq2) 919 lookup_type v fvs1 <> None
975 = (lookup ctypeDenote v2 920 -> lookup Closed.typeDenote v env
976 (makeEnv envT fvs1 921 == lookup Closed.typeDenote v
977 (cprimopsDenote 922 (makeEnv (Closed.expDenote
978 (packExp fvs1 fvs2 Hincl env))) :? Heq1). 923 (packExp fvs1 fvs2 Hincl env))).
979 induction envT; my_equation. 924 induction envT; my_crush.
980 Qed. 925 Qed.
981 End packing_correct. 926 End packing_correct.
927
928 (*Lemma typeDenote_same : forall t,
929 Closed.typeDenote (ccType t) = Source.typeDenote t.
930 induction t; crush.
931 Qed.*)
932
933 Lemma typeDenote_same : forall t,
934 Source.typeDenote t = Closed.typeDenote (ccType t).
935 induction t; crush.
936 Qed.
937
938 Hint Resolve typeDenote_same.
982 939
983 Lemma look : forall envT n (fvs : isfree envT) t, 940 Lemma look : forall envT n (fvs : isfree envT) t,
984 lookup_type n fvs = Some t 941 lookup_type n fvs = Some t
985 -> ctypeDenote <| lookup_type n fvs = ptypeDenote t. 942 -> Closed.typeDenote <| lookup_type n fvs = Source.typeDenote t.
986 equation. 943 crush.
987 Qed. 944 Qed.
988 945
989 Implicit Arguments look [envT n fvs t]. 946 Implicit Arguments look [envT n fvs t].
990 947
991 948 Lemma cast_jmeq : forall (T1 T2 : Set) (pf : T1 = T2) (T2' : Set) (v1 : T1) (v2 : T2'),
992 Theorem ccTerm_correct : forall result G 949 v1 == v2
993 (e1 : pterm ptypeDenote result) 950 -> T2' = T2
994 (e2 : pterm natvar result), 951 -> match pf in _ = T return T with
995 pterm_equiv G e1 e2 952 | refl_equal => v1
996 -> forall (envT : list ptype) (fvs : isfree envT) 953 end == v2.
997 (env : envOf ctypeDenote fvs) (Hwf : wfTerm fvs e2) k, 954 intros; generalize pf; subst.
998 (forall t (v1 : ptypeDenote t) (v2 : natvar t), 955 intro.
999 In (vars (x := t) (v1, v2)) G 956 rewrite (UIP_refl _ _ pf).
957 auto.
958 Qed.
959
960 Hint Resolve cast_jmeq.
961
962 Theorem ccTerm_correct : forall t G
963 (e1 : Source.exp Source.typeDenote t)
964 (e2 : Source.exp natvar t),
965 exp_equiv G e1 e2
966 -> forall (envT : list Source.type) (fvs : isfree envT)
967 (env : envOf Closed.typeDenote fvs) (wf : wfExp fvs e2),
968 (forall t (v1 : Source.typeDenote t) (v2 : natvar t),
969 In (existT _ _ (v1, v2)) G
1000 -> v2 < length envT) 970 -> v2 < length envT)
1001 -> (forall t (v1 : ptypeDenote t) (v2 : natvar t), 971 -> (forall t (v1 : Source.typeDenote t) (v2 : natvar t),
1002 In (vars (x := t) (v1, v2)) G 972 In (existT _ _ (v1, v2)) G
1003 -> lookup_type v2 fvs = Some t 973 -> lookup_type v2 fvs = Some t
1004 -> forall Heq, (lookup ctypeDenote v2 env :? Heq) = v1) 974 -> lookup Closed.typeDenote v2 env == v1)
1005 -> ptermDenote e1 k 975 -> Closed.expDenote (funcsDenote (ccExp e2 fvs wf) env)
1006 = ctermDenote (cfuncsDenote (ccTerm e2 fvs Hwf) k env) k. 976 == Source.expDenote e1.
1007 977
1008 Hint Rewrite splicePrim_correct spliceTerm_correct 978 Hint Rewrite spliceFuncs_correct unpackExp_correct : cpdt.
1009 spliceFuncs_correct inside_correct : ltamer.
1010
1011 Hint Rewrite unpackExp_correct : ltamer.
1012 Hint Resolve packExp_correct lookup_type_inner. 979 Hint Resolve packExp_correct lookup_type_inner.
1013 980
1014 Hint Extern 1 (_ = _) => push_vars. 981 induction 1.
1015 982
1016 Hint Extern 1 (_ = _) => 983 crush.
1017 match goal with 984 crush.
1018 | [ Hvars : forall t v1 v2, _, 985 crush.
1019 Hin : In _ _ |- _ ] => 986 crush.
1020 rewrite (Hvars _ _ _ Hin) 987
1021 end. 988 Lemma app_jmeq : forall dom1 dom2 ran1 ran2
1022 989 (f1 : dom1 -> ran1) (f2 : dom2 -> ran2)
1023 Hint Extern 1 (wfPrimop _ _) => tauto. 990 (x1 : dom1) (x2 : dom2),
1024 991 ran1 = ran2
1025 Hint Extern 1 (_ < _) => 992 -> f1 == f2
1026 match goal with 993 -> x1 == x2
1027 | [ Hvars : forall t v1 v2, _, 994 -> f1 x1 == f2 x2.
1028 Hin : In _ _ |- _ ] => 995 crush.
1029 exact (Hvars _ _ _ Hin) 996 assert (dom1 = dom2).
1030 end. 997 inversion H1; trivial.
1031 998 crush.
1032 Hint Extern 1 (lookup_type _ _ = _) => tauto. 999 Qed.
1033 1000
1034 Hint Extern 1 (_ = _) => 1001 Lemma app_jmeq : forall dom ran
1035 match goal with 1002 (f1 : Closed.typeDenote (ccType dom) -> Closed.typeDenote (ccType ran))
1036 | [ Hvars : forall t v1 v2, _, 1003 (f2 : Source.typeDenote dom -> Source.typeDenote ran)
1037 Hin : In (vars (_, length ?envT)) _ |- _ ] => 1004 (x1 : dom1) (x2 : dom2),
1038 contradictory; assert (length envT < length envT); [auto | omega] 1005 ran1 = ran2
1039 end. 1006 -> f1 == f2
1040 1007 -> x1 == x2
1041 Hint Extern 5 (_ = _) => symmetry. 1008 -> f1 x1 == f2 x2.
1042 1009 crush.
1043 Hint Extern 1 (_ = _) => 1010 assert (dom1 = dom2).
1044 match goal with 1011 inversion H1; trivial.
1045 | [ H : lookup_type ?v _ = Some ?t, fvs : isfree _ |- (lookup _ _ _ :? _) = _ ] => 1012 crush.
1046 let Hty := fresh "Hty" in 1013 Qed.
1047 (assert (Hty : lookup_type v fvs = Some t); 1014
1048 [eauto 1015 simpl.
1049 | eapply (trans_cast (look Hty))]) 1016 refine (app_jmeq _ _ _).
1050 end. 1017 apply app_jmeq.
1051 1018 dependent rewrite <- IHexp_equiv1.
1052 Hint Extern 3 (ptermDenote _ _ = ctermDenote _ _) =>
1053 match goal with
1054 | [ H : _ |- ptermDenote (_ ?v1) _
1055 = ctermDenote (cfuncsDenote (ccTerm (_ ?v2) (envT := ?envT) ?fvs _) _ _) _ ] =>
1056 apply (H v1 v2 envT fvs); my_simpler
1057 end.
1058
1059 intro.
1060 apply (pterm_equiv_mut
1061 (fun G (e1 : pterm ptypeDenote result) (e2 : pterm natvar result) =>
1062 forall (envT : list ptype) (fvs : isfree envT)
1063 (env : envOf ctypeDenote fvs) (Hwf : wfTerm fvs e2) k,
1064 (forall t (v1 : ptypeDenote t) (v2 : natvar t),
1065 In (vars (x := t) (v1, v2)) G
1066 -> v2 < length envT)
1067 -> (forall t (v1 : ptypeDenote t) (v2 : natvar t),
1068 In (vars (x := t) (v1, v2)) G
1069 -> lookup_type v2 fvs = Some t
1070 -> forall Heq, (lookup ctypeDenote v2 env :? Heq) = v1)
1071 -> ptermDenote e1 k
1072 = ctermDenote (cfuncsDenote (ccTerm e2 fvs Hwf) k env) k)
1073 (fun G t (p1 : pprimop ptypeDenote result t) (p2 : pprimop natvar result t) =>
1074 forall (envT : list ptype) (fvs : isfree envT)
1075 (env : envOf ctypeDenote fvs) (Hwf : wfPrimop fvs p2) Hwf k,
1076 (forall t (v1 : ptypeDenote t) (v2 : natvar t),
1077 In (vars (x := t) (v1, v2)) G
1078 -> v2 < length envT)
1079 -> (forall t (v1 : ptypeDenote t) (v2 : natvar t),
1080 In (vars (x := t) (v1, v2)) G
1081 -> lookup_type v2 fvs = Some t
1082 -> forall Heq, (lookup ctypeDenote v2 env :? Heq) = v1)
1083 -> pprimopDenote p1 k
1084 = cprimopsDenote (cfuncsDenote (ccPrimop p2 fvs Hwf) k env)));
1085 my_simpler; eauto.
1086 Qed. 1019 Qed.
1087 1020
1088 1021
1089 (** * Parametric version *) 1022 (** * Parametric version *)
1090 1023