Mercurial > cpdt > repo

comparison src/Tactics.v @ 51:9ceee967b1fc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
What could go wrong; some exercises
author Adam Chlipala <adamc@hcoop.net>
date Sun, 28 Sep 2008 12:44:05 -0400
parents a21eb02cc7c6
children 1a664ff9d2d1
comparison
equal deleted inserted replaced
50:a21eb02cc7c6 51:9ceee967b1fc
10 Require Import List. 10 Require Import List.
11 11
12 Require Omega. 12 Require Omega.
13 13
14 14
15 Ltac inject H := injection H; clear H; intros; subst.
16
15 Ltac simplHyp := 17 Ltac simplHyp :=
16 match goal with 18 match goal with
17 | [ H : S _ = S _ |- _ ] => injection H; clear H; intros; subst 19 | [ H : ?F _ = ?F _ |- _ ] => injection H;
20 match goal with
21 | [ |- _ = _ -> _ ] => clear H; intros; subst
22 end
23 | [ H : ?F _ _ = ?F _ _ |- _ ] => injection H;
24 match goal with
25 | [ |- _ = _ -> _ = _ -> _ ] => clear H; intros; subst
26 end
18 end. 27 end.
19 28
20 Ltac rewriteHyp := 29 Ltac rewriteHyp :=
21 match goal with 30 match goal with
22 | [ H : _ |- _ ] => rewrite H 31 | [ H : _ |- _ ] => rewrite H
26 35
27 Ltac rewriter := autorewrite with cpdt in *; rewriterP. 36 Ltac rewriter := autorewrite with cpdt in *; rewriterP.
28 37
29 Hint Rewrite app_ass : cpdt. 38 Hint Rewrite app_ass : cpdt.
30 39
31 Ltac sintuition := simpl in *; intuition; try simplHyp. 40 Ltac sintuition := simpl in *; intuition; try simplHyp; try congruence.
32 41
33 Ltac crush := sintuition; rewriter; sintuition; try omega. 42 Ltac crush := sintuition; rewriter; sintuition; try omega.