Mercurial > cpdt > repo

comparison src/GeneralRec.v @ 375:d1276004eec9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finish pass over LogicProg; change [crush] to take advantage of new [Hint Rewrite] syntax that uses database [core] by default
author Adam Chlipala <adam@chlipala.net>
date Mon, 26 Mar 2012 16:55:59 -0400
parents b01c7b3122cc
children 31fa03bc0f18
comparison
equal deleted inserted replaced
374:f3146d40c2a1 375:d1276004eec9
694 TBind (Answer v) m2 = m2 v. 694 TBind (Answer v) m2 = m2 v.
695 intros; rewrite <- (frob_eq (TBind (Answer v) m2)); 695 intros; rewrite <- (frob_eq (TBind (Answer v) m2));
696 simpl; findDestr; reflexivity. 696 simpl; findDestr; reflexivity.
697 Qed. 697 Qed.
698 698
699 Hint Rewrite TBind_Answer : cpdt. 699 Hint Rewrite TBind_Answer.
700 700
701 (** printing exists $\exists$ *) 701 (** printing exists $\exists$ *)
702 702
703 Theorem tassociativity : forall A B C (m : thunk A) (f : A -> thunk B) (g : B -> thunk C), 703 Theorem tassociativity : forall A B C (m : thunk A) (f : A -> thunk B) (g : B -> thunk C),
704 thunk_eq (TBind (TBind m f) g) (TBind m (fun x => TBind (f x) g)). 704 thunk_eq (TBind (TBind m f) g) (TBind m (fun x => TBind (f x) g)).
721 721
722 Inductive eval A : thunk A -> A -> Prop := 722 Inductive eval A : thunk A -> A -> Prop :=
723 | EvalAnswer : forall x, eval (Answer x) x 723 | EvalAnswer : forall x, eval (Answer x) x
724 | EvalThink : forall m x, eval m x -> eval (Think m) x. 724 | EvalThink : forall m x, eval m x -> eval (Think m) x.
725 725
726 Hint Rewrite frob_eq : cpdt. 726 Hint Rewrite frob_eq.
727 727
728 Lemma eval_frob : forall A (c : thunk A) x, 728 Lemma eval_frob : forall A (c : thunk A) x,
729 eval (frob c) x 729 eval (frob c) x
730 -> eval c x. 730 -> eval c x.
731 crush. 731 crush.