Mercurial > cpdt > repo
comparison src/Intensional.v @ 187:71c076dd5f31
Close to automated ccExp_correct
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Mon, 17 Nov 2008 10:22:40 -0500 |
parents | ecd231ba5c8b |
children | aec05464fedd |
comparison
equal
deleted
inserted
replaced
186:ecd231ba5c8b | 187:71c076dd5f31 |
---|---|
229 Notation "#1 x" := (Fst x) (at level 72) : cc_scope. | 229 Notation "#1 x" := (Fst x) (at level 72) : cc_scope. |
230 Notation "#2 x" := (Snd x) (at level 72) : cc_scope. | 230 Notation "#2 x" := (Snd x) (at level 72) : cc_scope. |
231 | 231 |
232 Notation "f <== \\ x , y , e ; fs" := | 232 Notation "f <== \\ x , y , e ; fs" := |
233 (Abs (fun x y => e) (fun f => fs)) | 233 (Abs (fun x y => e) (fun f => fs)) |
234 (right associativity, at level 80, e at next level) : cc_scope. | |
235 Notation "f <== \\ ! , y , e ; fs" := | |
236 (Abs (fun _ y => e) (fun f => fs)) | |
237 (right associativity, at level 80, e at next level) : cc_scope. | |
238 Notation "f <== \\ x , ! , e ; fs" := | |
239 (Abs (fun x _ => e) (fun f => fs)) | |
240 (right associativity, at level 80, e at next level) : cc_scope. | |
241 Notation "f <== \\ ! , ! , e ; fs" := | |
242 (Abs (fun _ _ => e) (fun f => fs)) | |
234 (right associativity, at level 80, e at next level) : cc_scope. | 243 (right associativity, at level 80, e at next level) : cc_scope. |
235 | 244 |
236 Notation "x <- e1 ; e2" := (Let e1 (fun x => e2)) | 245 Notation "x <- e1 ; e2" := (Let e1 (fun x => e2)) |
237 (right associativity, at level 80, e1 at next level) : cc_scope. | 246 (right associativity, at level 80, e1 at next level) : cc_scope. |
238 | 247 |
322 end; crush). | 331 end; crush). |
323 | 332 |
324 Section isfree. | 333 Section isfree. |
325 Import Source. | 334 Import Source. |
326 Open Local Scope source_scope. | 335 Open Local Scope source_scope. |
327 | |
328 Hint Extern 3 False => omega. | |
329 | 336 |
330 Fixpoint lookup_type (envT : list Source.type) (n : nat) {struct envT} | 337 Fixpoint lookup_type (envT : list Source.type) (n : nat) {struct envT} |
331 : isfree envT -> option Source.type := | 338 : isfree envT -> option Source.type := |
332 match envT return (isfree envT -> _) with | 339 match envT return (isfree envT -> _) with |
333 | nil => fun _ => None | 340 | nil => fun _ => None |
503 Hint Resolve lookup_bound. | 510 Hint Resolve lookup_bound. |
504 | 511 |
505 Lemma lookup_bound_contra : forall t envT (fvs : isfree envT), | 512 Lemma lookup_bound_contra : forall t envT (fvs : isfree envT), |
506 lookup_type (length envT) fvs = Some t | 513 lookup_type (length envT) fvs = Some t |
507 -> False. | 514 -> False. |
508 intros; assert (length envT < length envT); eauto. | 515 intros; assert (length envT < length envT); eauto; crush. |
509 Defined. | 516 Defined. |
510 | 517 |
511 Hint Resolve lookup_bound_contra. | 518 Hint Resolve lookup_bound_contra. |
512 | |
513 Hint Extern 3 (_ = _) => elimtype False; omega. | |
514 | 519 |
515 Lemma lookup_push_drop : forall v t t' envT fvs, | 520 Lemma lookup_push_drop : forall v t t' envT fvs, |
516 v < length envT | 521 v < length envT |
517 -> lookup_type (envT := t :: envT) v (true, fvs) = Some t' | 522 -> lookup_type (envT := t :: envT) v (true, fvs) = Some t' |
518 -> lookup_type (envT := envT) v fvs = Some t'. | 523 -> lookup_type (envT := envT) v fvs = Some t'. |
622 Implicit Arguments envOf [envT]. | 627 Implicit Arguments envOf [envT]. |
623 Implicit Arguments lok [var n t envT fvs]. | 628 Implicit Arguments lok [var n t envT fvs]. |
624 | 629 |
625 Section lookup_hints. | 630 Section lookup_hints. |
626 Hint Resolve lookup_bound_contra. | 631 Hint Resolve lookup_bound_contra. |
627 | |
628 (*Ltac my_chooser T k := | |
629 match T with | |
630 | ptype => | |
631 match goal with | |
632 | [ H : lookup _ _ = Some ?t |- _ ] => k t | |
633 end | |
634 | _ => default_chooser T k | |
635 end. | |
636 | |
637 Ltac my_matching := matching equation my_chooser.*) | |
638 | 632 |
639 Hint Resolve lookup_bound_contra. | 633 Hint Resolve lookup_bound_contra. |
640 | 634 |
641 Lemma lookup_type_push : forall t' envT (fvs1 fvs2 : isfree envT) b1 b2, | 635 Lemma lookup_type_push : forall t' envT (fvs1 fvs2 : isfree envT) b1 b2, |
642 (forall (n : nat) (t : Source.type), | 636 (forall (n : nat) (t : Source.type), |
759 Definition env_prog var t envT (fvs : isfree envT) := | 753 Definition env_prog var t envT (fvs : isfree envT) := |
760 funcs var (envOf var fvs -> Closed.exp var t). | 754 funcs var (envOf var fvs -> Closed.exp var t). |
761 | 755 |
762 Implicit Arguments env_prog [envT]. | 756 Implicit Arguments env_prog [envT]. |
763 | 757 |
764 Axiom cheat : forall T, T. | |
765 | |
766 Import Source. | 758 Import Source. |
767 Open Local Scope cc_scope. | 759 Open Local Scope cc_scope. |
760 | |
761 Definition proj1 A B (pf : A /\ B) : A := | |
762 let (x, _) := pf in x. | |
763 Definition proj2 A B (pf : A /\ B) : B := | |
764 let (_, y) := pf in y. | |
768 | 765 |
769 Fixpoint ccExp var t (e : Source.exp natvar t) | 766 Fixpoint ccExp var t (e : Source.exp natvar t) |
770 (envT : list Source.type) (fvs : isfree envT) | 767 (envT : list Source.type) (fvs : isfree envT) |
771 {struct e} : wfExp fvs e -> env_prog var (ccType t) fvs := | 768 {struct e} : wfExp fvs e -> env_prog var (ccType t) fvs := |
772 match e in (Source.exp _ t) return (wfExp fvs e -> env_prog var (ccType t) fvs) with | 769 match e in (Source.exp _ t) return (wfExp fvs e -> env_prog var (ccType t) fvs) with |
810 | 807 |
811 Definition CcExp' t (E : Source.Exp t) (Hwf : wfExp (envT := nil) tt (E _)) : Prog (ccType t) := | 808 Definition CcExp' t (E : Source.Exp t) (Hwf : wfExp (envT := nil) tt (E _)) : Prog (ccType t) := |
812 fun _ => map_funcs (fun f => f tt) (ccExp (E _) (envT := nil) tt Hwf). | 809 fun _ => map_funcs (fun f => f tt) (ccExp (E _) (envT := nil) tt Hwf). |
813 | 810 |
814 | 811 |
815 (** * Correctness *) | 812 (** ** Examples *) |
813 | |
814 Open Local Scope source_scope. | |
815 | |
816 Definition ident : Source.Exp (Nat --> Nat) := fun _ => \x, #x. | |
817 Theorem ident_ok : wfExp (envT := nil) tt (ident _). | |
818 crush. | |
819 Defined. | |
820 Eval compute in CcExp' ident ident_ok. | |
821 Eval compute in ProgDenote (CcExp' ident ident_ok). | |
822 | |
823 Definition app_ident : Source.Exp Nat := fun _ => ident _ @ ^0. | |
824 Theorem app_ident_ok : wfExp (envT := nil) tt (app_ident _). | |
825 crush. | |
826 Defined. | |
827 Eval compute in CcExp' app_ident app_ident_ok. | |
828 Eval compute in ProgDenote (CcExp' app_ident app_ident_ok). | |
829 | |
830 Definition first : Source.Exp (Nat --> Nat --> Nat) := fun _ => | |
831 \x, \y, #x. | |
832 Theorem first_ok : wfExp (envT := nil) tt (first _). | |
833 crush. | |
834 Defined. | |
835 Eval compute in CcExp' first first_ok. | |
836 Eval compute in ProgDenote (CcExp' first first_ok). | |
837 | |
838 Definition app_first : Source.Exp Nat := fun _ => first _ @ ^1 @ ^0. | |
839 Theorem app_first_ok : wfExp (envT := nil) tt (app_first _). | |
840 crush. | |
841 Defined. | |
842 Eval compute in CcExp' app_first app_first_ok. | |
843 Eval compute in ProgDenote (CcExp' app_first app_first_ok). | |
844 | |
845 | |
846 (** ** Correctness *) | |
816 | 847 |
817 Section spliceFuncs_correct. | 848 Section spliceFuncs_correct. |
818 Variables T1 T2 : Type. | 849 Variables T1 T2 : Type. |
819 Variable f : T1 -> funcs typeDenote T2. | 850 Variable f : T1 -> funcs typeDenote T2. |
820 | 851 |
912 match goal with | 943 match goal with |
913 | [ |- context[False_rect _ ?H] ] => | 944 | [ |- context[False_rect _ ?H] ] => |
914 apply False_rect; exact H | 945 apply False_rect; exact H |
915 end. | 946 end. |
916 | 947 |
917 Theorem packExp_correct : forall v envT (fvs1 fvs2 : isfree envT) | 948 Theorem packExp_correct : forall v t envT (fvs1 fvs2 : isfree envT) |
918 Hincl env, | 949 Hincl env, |
919 lookup_type v fvs1 <> None | 950 lookup_type v fvs1 = Some t |
920 -> lookup Closed.typeDenote v env | 951 -> lookup Closed.typeDenote v env |
921 == lookup Closed.typeDenote v | 952 == lookup Closed.typeDenote v |
922 (makeEnv (Closed.expDenote | 953 (makeEnv (Closed.expDenote |
923 (packExp fvs1 fvs2 Hincl env))). | 954 (packExp fvs1 fvs2 Hincl env))). |
924 induction envT; my_crush. | 955 induction envT; my_crush. |
925 Qed. | 956 Qed. |
926 End packing_correct. | 957 End packing_correct. |
927 | 958 |
928 About packExp_correct. | |
929 Implicit Arguments packExp_correct [v envT fvs1]. | 959 Implicit Arguments packExp_correct [v envT fvs1]. |
930 | 960 Implicit Arguments lookup_type_inner [t t' envT v t'' fvs e]. |
931 Implicit Arguments lookup_type_more [v2 envT fvs t b v]. | 961 Implicit Arguments inclusion [t t' envT fvs e]. |
932 | 962 |
933 Lemma typeDenote_same : forall t, | 963 Lemma typeDenote_same : forall t, |
934 Source.typeDenote t = Closed.typeDenote (ccType t). | 964 Source.typeDenote t = Closed.typeDenote (ccType t). |
935 induction t; crush. | 965 induction t; crush. |
936 Qed. | 966 Qed. |
937 | 967 |
938 Hint Resolve typeDenote_same. | 968 Hint Resolve typeDenote_same. |
939 | |
940 Lemma look : forall envT n (fvs : isfree envT) t, | |
941 lookup_type n fvs = Some t | |
942 -> Closed.typeDenote <| lookup_type n fvs = Source.typeDenote t. | |
943 crush. | |
944 Qed. | |
945 | |
946 Implicit Arguments look [envT n fvs t]. | |
947 | 969 |
948 Fixpoint lr (t : Source.type) : Source.typeDenote t -> Closed.typeDenote (ccType t) -> Prop := | 970 Fixpoint lr (t : Source.type) : Source.typeDenote t -> Closed.typeDenote (ccType t) -> Prop := |
949 match t return Source.typeDenote t -> Closed.typeDenote (ccType t) -> Prop with | 971 match t return Source.typeDenote t -> Closed.typeDenote (ccType t) -> Prop with |
950 | Nat => @eq nat | 972 | Nat => @eq nat |
951 | dom --> ran => fun f1 f2 => | 973 | dom --> ran => fun f1 f2 => |
966 In (existT _ _ (v1, v2)) G | 988 In (existT _ _ (v1, v2)) G |
967 -> forall pf, | 989 -> forall pf, |
968 lr t v1 (match lok pf in _ = T return T with | 990 lr t v1 (match lok pf in _ = T return T with |
969 | refl_equal => lookup Closed.typeDenote v2 env | 991 | refl_equal => lookup Closed.typeDenote v2 env |
970 end)) | 992 end)) |
971 (*-> forall pf : lookup_type v2 fvs = Some t, | |
972 lr t v1 (match pf in _ = T return Closed.typeDenote <| T with | |
973 | refl_equal => lookup Closed.typeDenote v2 env | |
974 end))*) | |
975 -> lr t (Source.expDenote e1) (Closed.expDenote (funcsDenote (ccExp e2 fvs wf) env)). | 993 -> lr t (Source.expDenote e1) (Closed.expDenote (funcsDenote (ccExp e2 fvs wf) env)). |
976 | 994 |
977 Hint Rewrite spliceFuncs_correct unpackExp_correct : cpdt. | 995 Hint Rewrite spliceFuncs_correct unpackExp_correct : cpdt. |
978 Hint Resolve packExp_correct lookup_type_inner. | 996 Hint Resolve packExp_correct lookup_type_inner. |
979 | 997 |
980 induction 1. | 998 induction 1; crush. |
999 | |
1000 match goal with | |
1001 | [ IH : _, Hlr : lr ?T ?X1 ?X2, ENV : list Source.type, F2 : natvar _ -> _ |- _ ] => | |
1002 apply (IH X1 (length ENV) (T :: ENV) (true, snd (fvsExp (F2 (length ENV)) (T :: ENV)))) | |
1003 end. | |
981 | 1004 |
982 crush. | 1005 crush. |
983 crush. | 1006 match goal with |
984 crush. | 1007 | [ Hlt : forall t v1 v2, _ -> _ < _, Hin : In _ _ |- _ ] => |
985 crush. | 1008 generalize (Hlt _ _ _ Hin); crush |
986 | 1009 end. |
987 crush. | 1010 |
988 apply (H0 x1 (length envT) (t1 :: envT) (true, snd (fvsExp (f2 (length envT)) (t1 :: envT)))). | 1011 crush; |
989 clear H0. | |
990 crush. | |
991 eauto. | |
992 generalize (H1 _ _ _ H4). | |
993 crush. | |
994 | |
995 crush. | |
996 generalize H3; clear_all. | |
997 match goal with | 1012 match goal with |
998 | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf | 1013 | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf |
999 end. | 1014 end; simpl; |
1000 simpl. | |
1001 destruct (eq_nat_dec (length envT) (length envT)); crush. | |
1002 rewrite (UIP_refl _ _ e0); assumption. | |
1003 | |
1004 match goal with | 1015 match goal with |
1005 | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf | 1016 | [ |- context[if ?E then _ else _] ] => destruct E |
1006 end; simpl. | 1017 end; intuition; subst; |
1007 destruct (eq_nat_dec v2 (length envT)); crush. | 1018 try match goal with |
1008 generalize (H1 _ _ _ H5). | 1019 | [ |- context[match ?pf with refl_equal => _ end] ] => rewrite (UIP_refl _ _ pf); assumption |
1009 crush. | 1020 | [ Hlt : forall t v1 v2, _ -> _ < _, Hin : In (existT _ _ (_, length _)) _ |- _ ] => |
1010 generalize (H2 _ _ _ H5). | 1021 generalize (Hlt _ _ _ Hin); crush |
1011 clear H2; intro H2. | 1022 end. |
1012 generalize (H2 (lookup_type_inner _ _ _ _ _ wf pf)). | 1023 |
1013 clear H2; intro H2. | 1024 generalize (H2 _ _ _ H5 (lookup_type_inner wf pf)); clear_all. |
1014 generalize H2; clear_all. | |
1015 repeat match goal with | 1025 repeat match goal with |
1016 | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf | 1026 | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf |
1017 end; simpl. | 1027 end; simpl. |
1018 | 1028 generalize (packExp_correct _ fvs (inclusion wf) env pf); simpl. |
1019 match type of pf with | |
1020 | ?X = _ => assert (X <> None) | |
1021 end. | |
1022 congruence. | |
1023 assert (forall (n : nat) (t0 : Source.type), | |
1024 lookup_type (envT:=envT) n (snd (fvsExp (f2 (length envT)) (t1 :: envT))) = Some t0 -> | |
1025 lookup_type (envT:=envT) n fvs = Some t0). | |
1026 eauto. | |
1027 generalize (packExp_correct fvs (inclusion t1 envT fvs (f2 (length envT)) wf) env H). | |
1028 simpl. | |
1029 match goal with | 1029 match goal with |
1030 | [ |- ?X == ?Y -> _ ] => | 1030 | [ |- ?X == ?Y -> _ ] => |
1031 generalize X Y | 1031 generalize X Y |
1032 end. | 1032 end. |
1033 rewrite pf. | 1033 rewrite pf. |
1034 rewrite (lookup_type_inner _ _ _ _ _ wf pf). | 1034 rewrite (lookup_type_inner wf pf). |
1035 crush. | 1035 crush. |
1036 rewrite (UIP_refl _ _ e0). | 1036 repeat match goal with |
1037 rewrite (UIP_refl _ _ e1) in H2. | 1037 | [ H : _ = _ |- _ ] => rewrite (UIP_refl _ _ H) in * |
1038 crush. | 1038 end. |
1039 rewrite <- H1. | 1039 rewrite <- H. |
1040 assumption. | 1040 assumption. |
1041 Qed. | 1041 Qed. |
1042 | 1042 |
1043 | 1043 |
1044 (** * Parametric version *) | 1044 (** * Parametric version *) |