Mercurial > cpdt > repo

comparison src/Generic.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 e0d91bcf70ec
children 3c941750c347
comparison
equal deleted inserted replaced
374:f3146d40c2a1 375:d1276004eec9
584 584
585 (** Using hints, we can redo this proof in a nice automated form. *) 585 (** Using hints, we can redo this proof in a nice automated form. *)
586 586
587 Restart. 587 Restart.
588 588
589 Hint Rewrite hget_hmake : cpdt. 589 Hint Rewrite hget_hmake.
590 Hint Resolve foldr_plus. 590 Hint Resolve foldr_plus.
591 591
592 unfold size; intros; pattern v; apply dok; crush. 592 unfold size; intros; pattern v; apply dok; crush.
593 Qed. 593 Qed.
594 (* end thide *) 594 (* end thide *)
603 (v : T), 603 (v : T),
604 map dd fx (fun x => x) v = v. 604 map dd fx (fun x => x) v = v.
605 (* begin thide *) 605 (* begin thide *)
606 (** Let us begin as we did in the last theorem, after adding another useful library equality as a hint. *) 606 (** Let us begin as we did in the last theorem, after adding another useful library equality as a hint. *)
607 607
608 Hint Rewrite hget_hmap : cpdt. 608 Hint Rewrite hget_hmap.
609 609
610 unfold map; intros; pattern v; apply dok; crush. 610 unfold map; intros; pattern v; apply dok; crush.
611 (** %\vspace{-.15in}%[[ 611 (** %\vspace{-.15in}%[[
612 H : forall i : fin (recursive c), 612 H : forall i : fin (recursive c),
613 fx T 613 fx T