Mercurial > cpdt > repo
comparison src/Tactics.v @ 50:a21eb02cc7c6
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. |