Mercurial > cpdt > repo

comparison src/Tactics.v @ 50:a21eb02cc7c6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Recursive predicates
author Adam Chlipala <adamc@hcoop.net>
date Sun, 28 Sep 2008 11:57:15 -0400
parents 95e24b629ad9
children 9ceee967b1fc
comparison
equal deleted inserted replaced
49:827d7e8a7d9e 50:a21eb02cc7c6
10 Require Import List. 10 Require Import List.
11 11
12 Require Omega. 12 Require Omega.
13 13
14 14
15 Ltac simplHyp :=
16 match goal with
17 | [ H : S _ = S _ |- _ ] => injection H; clear H; intros; subst
18 end.
19
15 Ltac rewriteHyp := 20 Ltac rewriteHyp :=
16 match goal with 21 match goal with
17 | [ H : _ |- _ ] => rewrite H 22 | [ H : _ |- _ ] => rewrite H
18 end. 23 end.
19 24
21 26
22 Ltac rewriter := autorewrite with cpdt in *; rewriterP. 27 Ltac rewriter := autorewrite with cpdt in *; rewriterP.
23 28
24 Hint Rewrite app_ass : cpdt. 29 Hint Rewrite app_ass : cpdt.
25 30
26 Ltac sintuition := simpl in *; intuition. 31 Ltac sintuition := simpl in *; intuition; try simplHyp.
27 32
28 Ltac crush := sintuition; rewriter; sintuition; try omega. 33 Ltac crush := sintuition; rewriter; sintuition; try omega.