Mercurial > cpdt > repo

comparison src/Extensional.v @ 179:8f3fc56b90d4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
PatMatch Elaborate_correct
author Adam Chlipala <adamc@hcoop.net>
date Mon, 10 Nov 2008 14:12:22 -0500
parents f41d4e43fd30
children de33d1ed7c63
comparison
equal deleted inserted replaced
178:f41d4e43fd30 179:8f3fc56b90d4
210 Infix "+^" := Plus (left associativity, at level 79) : cps_scope. 210 Infix "+^" := Plus (left associativity, at level 79) : cps_scope.
211 211
212 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : cps_scope. 212 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : cps_scope.
213 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : cps_scope. 213 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : cps_scope.
214 214
215 Notation "[ x1 , x2 ]" := (Pair x1 x2) (at level 73) : cps_scope. 215 Notation "[ x1 , x2 ]" := (Pair x1 x2) : cps_scope.
216 Notation "#1 x" := (Fst x) (at level 72) : cps_scope. 216 Notation "#1 x" := (Fst x) (at level 72) : cps_scope.
217 Notation "#2 x" := (Snd x) (at level 72) : cps_scope. 217 Notation "#2 x" := (Snd x) (at level 72) : cps_scope.
218 218
219 Bind Scope cps_scope with prog primop. 219 Bind Scope cps_scope with prog primop.
220 220
408 Implicit Arguments PVar [t]. 408 Implicit Arguments PVar [t].
409 Implicit Arguments PInl [t1 t2 ts]. 409 Implicit Arguments PInl [t1 t2 ts].
410 Implicit Arguments PInr [t1 t2 ts]. 410 Implicit Arguments PInr [t1 t2 ts].
411 411
412 Notation "##" := PVar (at level 70) : pat_scope. 412 Notation "##" := PVar (at level 70) : pat_scope.
413 Notation "[ p1 , p2 ]" := (PPair p1 p2) (at level 72) : pat_scope. 413 Notation "[ p1 , p2 ]" := (PPair p1 p2) : pat_scope.
414 Notation "'Inl' p" := (PInl p) (at level 71) : pat_scope. 414 Notation "'Inl' p" := (PInl p) (at level 71) : pat_scope.
415 Notation "'Inr' p" := (PInr p) (at level 71) : pat_scope. 415 Notation "'Inr' p" := (PInr p) (at level 71) : pat_scope.
416 416
417 Bind Scope pat_scope with pat. 417 Bind Scope pat_scope with pat.
418 Delimit Scope pat_scope with pat. 418 Delimit Scope pat_scope with pat.
471 Notation "()" := EUnit : source_scope. 471 Notation "()" := EUnit : source_scope.
472 472
473 Infix "@" := App (left associativity, at level 77) : source_scope. 473 Infix "@" := App (left associativity, at level 77) : source_scope.
474 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope. 474 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope.
475 475
476 Notation "[ x , y ]" := (Pair x y) (at level 72) : source_scope. 476 Notation "[ x , y ]" := (Pair x y) : source_scope.
477 477
478 Notation "'Inl' e" := (EInl e) (at level 71) : source_scope. 478 Notation "'Inl' e" := (EInl e) (at level 71) : source_scope.
479 Notation "'Inr' e" := (EInr e) (at level 71) : source_scope. 479 Notation "'Inr' e" := (EInr e) (at level 71) : source_scope.
480 480
481 Delimit Scope source_scope with source. 481 Delimit Scope source_scope with source.
625 625
626 Infix "@" := App (left associativity, at level 77) : elab_scope. 626 Infix "@" := App (left associativity, at level 77) : elab_scope.
627 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : elab_scope. 627 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : elab_scope.
628 Notation "\ ? , e" := (Abs (fun _ => e)) (at level 78) : elab_scope. 628 Notation "\ ? , e" := (Abs (fun _ => e)) (at level 78) : elab_scope.
629 629
630 Notation "[ x , y ]" := (Pair x y) (at level 72) : elab_scope. 630 Notation "[ x , y ]" := (Pair x y) : elab_scope.
631 Notation "#1 e" := (Fst e) (at level 72) : elab_scope. 631 Notation "#1 e" := (Fst e) (at level 72) : elab_scope.
632 Notation "#2 e" := (Snd e) (at level 72) : elab_scope. 632 Notation "#2 e" := (Snd e) (at level 72) : elab_scope.
633 633
634 Notation "'Inl' e" := (EInl e) (at level 71) : elab_scope. 634 Notation "'Inl' e" := (EInl e) (at level 71) : elab_scope.
635 Notation "'Inr' e" := (EInr e) (at level 71) : elab_scope. 635 Notation "'Inr' e" := (EInr e) (at level 71) : elab_scope.
842 End elaborate. 842 End elaborate.
843 843
844 Definition Elaborate t (E : Source.Exp t) : Elab.Exp t := 844 Definition Elaborate t (E : Source.Exp t) : Elab.Exp t :=
845 fun _ => elaborate (E _). 845 fun _ => elaborate (E _).
846 846
847 Fixpoint grab t result : choice_tree typeDenote t result -> typeDenote t -> result :=
848 match t return (choice_tree typeDenote t result -> typeDenote t -> result) with
849 | t1 ** t2 => fun ct v =>
850 grab t2 _ (grab t1 _ ct (fst v)) (snd v)
851 | t1 ++ t2 => fun ct v =>
852 match v with
853 | inl v' => grab t1 _ (fst ct) v'
854 | inr v' => grab t2 _ (snd ct) v'
855 end
856 | t => fun ct v => ct (#v)%elab
857 end%source%type.
858
859 Implicit Arguments grab [t result].
860
861 Ltac my_crush :=
862 crush;
863 repeat (match goal with
864 | [ |- context[match ?E with inl _ => _ | inr _ => _ end] ] =>
865 destruct E
866 end; crush).
867
868 Lemma expand_grab : forall t2 t1 result
869 (out : result -> Elab.exp typeDenote t2)
870 (ct : choice_tree typeDenote t1 result)
871 (disc : Elab.exp typeDenote t1),
872 Elab.expDenote (expand out ct disc) = Elab.expDenote (out (grab ct (Elab.expDenote disc))).
873 induction t1; my_crush.
874 Qed.
875
876 Lemma recreate_pair : forall t1 t2
877 (x : Elab.exp typeDenote t1)
878 (x0 : Elab.exp typeDenote t2)
879 (v : typeDenote (t1 ** t2)),
880 expDenote x = fst v
881 -> expDenote x0 = snd v
882 -> @eq (typeDenote t1 * typeDenote t2) (expDenote [x, x0]) v.
883 destruct v; crush.
884 Qed.
885
886 Lemma everywhere_correct : forall t1 result
887 (succ : Elab.exp typeDenote t1 -> result) disc,
888 exists disc', grab (everywhere succ) (Elab.expDenote disc) = succ disc'
889 /\ Elab.expDenote disc' = Elab.expDenote disc.
890 Hint Resolve recreate_pair.
891
892 induction t1; my_crush; eauto; fold choice_tree;
893 repeat (fold typeDenote in *; crush;
894 match goal with
895 | [ IH : forall result succ, _ |- context[grab (everywhere ?S) _] ] =>
896 generalize (IH _ S); clear IH
897 | [ e : exp typeDenote (?T ** _), IH : forall _ : exp typeDenote ?T, _ |- _ ] =>
898 generalize (IH (#1 e)); clear IH
899 | [ e : exp typeDenote (_ ** ?T), IH : forall _ : exp typeDenote ?T, _ |- _ ] =>
900 generalize (IH (#2 e)); clear IH
901 | [ e : typeDenote ?T, IH : forall _ : exp typeDenote ?T, _ |- _ ] =>
902 generalize (IH (#e)); clear IH
903 end; crush); eauto.
904 Qed.
905
906 Lemma merge_correct : forall t result
907 (ct1 ct2 : choice_tree typeDenote t result)
908 (mr : result -> result -> result) v,
909 grab (merge mr ct1 ct2) v = mr (grab ct1 v) (grab ct2 v).
910 induction t; crush.
911 Qed.
912
913 Lemma everywhere_fail : forall t result
914 (fail : result) v,
915 grab (everywhere (fun _ : Elab.exp typeDenote t => fail)) v = fail.
916 induction t; crush.
917 Qed.
918
919 Lemma elaboratePat_correct : forall t1 ts (p : pat t1 ts)
920 result (succ : hlist (Elab.exp typeDenote) ts -> result)
921 (fail : result) v env,
922 patDenote p v = Some env
923 -> exists env', grab (elaboratePat typeDenote p succ fail) v = succ env'
924 /\ env = hmap Elab.expDenote env'.
925 Hint Resolve hmap_happ.
926
927 induction p; crush; fold choice_tree;
928 repeat (match goal with
929 | [ |- context[grab (everywhere ?succ) ?v] ] =>
930 generalize (everywhere_correct succ (#v)%elab)
931
932 | [ H : forall result sudc fail, _ |- context[grab (elaboratePat _ _ ?S ?F) ?V] ] =>
933 generalize (H _ S F V); clear H
934 | [ H1 : context[match ?E with Some _ => _ | None => _ end],
935 H2 : forall env, ?E = Some env -> _ |- _ ] =>
936 destruct E
937 | [ H : forall env, Some ?E = Some env -> _ |- _ ] =>
938 generalize (H _ (refl_equal _)); clear H
939 end; crush); eauto.
940 Qed.
941
942 Lemma elaboratePat_fails : forall t1 ts (p : pat t1 ts)
943 result (succ : hlist (Elab.exp typeDenote) ts -> result)
944 (fail : result) v,
945 patDenote p v = None
946 -> grab (elaboratePat typeDenote p succ fail) v = fail.
947 Hint Resolve everywhere_fail.
948
949 induction p; try solve [ crush ];
950 simpl; fold choice_tree; intuition; simpl in *;
951 repeat match goal with
952 | [ IH : forall result succ fail v, patDenote ?P v = _ -> _
953 |- context[grab (elaboratePat _ ?P ?S ?F) ?V] ] =>
954 generalize (IH _ S F V); clear IH; intro IH;
955 generalize (elaboratePat_correct P S F V); intros;
956 destruct (patDenote P V); try discriminate
957 | [ H : forall env, Some _ = Some env -> _ |- _ ] =>
958 destruct (H _ (refl_equal _)); clear H; intuition
959 | [ H : _ |- _ ] => rewrite H; intuition
960 end.
961 Qed.
962
963 Implicit Arguments letify [var t ts].
964
965 Lemma letify_correct : forall t ts (f : hlist typeDenote ts -> Elab.exp typeDenote t)
966 (env : hlist (Elab.exp typeDenote) ts),
967 Elab.expDenote (letify f env)
968 = Elab.expDenote (f (hmap Elab.expDenote env)).
969 induction ts; crush.
970 Qed.
971
972 Theorem elaborate_correct : forall t (e : Source.exp typeDenote t),
973 Elab.expDenote (elaborate e) = Source.expDenote e.
974 Hint Rewrite expand_grab merge_correct letify_correct : cpdt.
975 Hint Rewrite everywhere_fail elaboratePat_fails using assumption : cpdt.
976
977 induction e; crush; try (ext_eq; crush);
978 match goal with
979 | [ tss : list (list type) |- _ ] =>
980 induction tss; crush;
981 match goal with
982 | [ |- context[grab (elaboratePat _ ?P ?S ?F) ?V] ] =>
983 case_eq (patDenote P V); [intros env Heq;
984 destruct (elaboratePat_correct P S F _ Heq); crush;
985 match goal with
986 | [ H : _ |- _ ] => rewrite <- H; crush
987 end
988 | crush ]
989 end
990 end.
991 Qed.
992
993 Theorem Elaborate_correct : forall t (E : Source.Exp t),
994 Elab.ExpDenote (Elaborate E) = Source.ExpDenote E.
995 unfold Elab.ExpDenote, Elaborate, Source.ExpDenote;
996 intros; apply elaborate_correct.
997 Qed.
998
847 End PatMatch. 999 End PatMatch.