Mercurial > cpdt > repo

comparison src/Intensional.v @ 187:71c076dd5f31

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