Mercurial > cpdt > repo

comparison src/Tactics.v @ 99:8c7d9b82a4a4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
crush' pursues trivial inversions
author Adam Chlipala <adamc@hcoop.net>
date Wed, 08 Oct 2008 09:41:50 -0400
parents cde1351d18bb
children ee676bf3d681
comparison
equal deleted inserted replaced
98:696726af9530 99:8c7d9b82a4a4
40 | (_, _) => fail 1 40 | (_, _) => fail 1
41 | _ => f ls 41 | _ => f ls
42 end. 42 end.
43 43
44 Ltac simplHyp invOne := 44 Ltac simplHyp invOne :=
45 let invert H F :=
46 inList F invOne; (inversion H; fail)
47 || (inversion H; [idtac]; clear H; try subst) in
45 match goal with 48 match goal with
46 | [ H : ex _ |- _ ] => destruct H 49 | [ H : ex _ |- _ ] => destruct H
47 50
48 | [ H : ?F _ = ?F _ |- _ ] => injection H; 51 | [ H : ?F _ = ?F _ |- _ ] => injection H;
49 match goal with 52 match goal with
52 | [ H : ?F _ _ = ?F _ _ |- _ ] => injection H; 55 | [ H : ?F _ _ = ?F _ _ |- _ ] => injection H;
53 match goal with 56 match goal with
54 | [ |- _ = _ -> _ = _ -> _ ] => try clear H; intros; try subst 57 | [ |- _ = _ -> _ = _ -> _ ] => try clear H; intros; try subst
55 end 58 end
56 59
57 | [ H : ?F _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst 60 | [ H : ?F _ |- _ ] => invert H F
58 | [ H : ?F _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst 61 | [ H : ?F _ _ |- _ ] => invert H F
59 | [ H : ?F _ _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst 62 | [ H : ?F _ _ _ |- _ ] => invert H F
60 | [ H : ?F _ _ _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst 63 | [ H : ?F _ _ _ _ |- _ ] => invert H F
61 | [ H : ?F _ _ _ _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst 64 | [ H : ?F _ _ _ _ _ |- _ ] => invert H F
62 end. 65 end.
63 66
64 Ltac rewriteHyp := 67 Ltac rewriteHyp :=
65 match goal with 68 match goal with
66 | [ H : _ |- _ ] => rewrite H 69 | [ H : _ |- _ ] => rewrite H