Mercurial > cpdt > repo

annotate 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
rev   line source
adamc@2 1 (* Copyright (c) 2008, Adam Chlipala
adamc@2 2 *
adamc@2 3 * This work is licensed under a
adamc@2 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@2 5 * Unported License.
adamc@2 6 * The license text is available at:
adamc@2 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@2 8 *)
adamc@2 9
adamc@2 10 Require Import List.
adamc@2 11
adamc@38 12 Require Omega.
adamc@38 13
adamc@2 14
adamc@51 15 Ltac inject H := injection H; clear H; intros; subst.
adamc@51 16
adamc@50 17 Ltac simplHyp :=
adamc@50 18 match goal with
adamc@51 19 | [ H : ?F _ = ?F _ |- _ ] => injection H;
adamc@51 20 match goal with
adamc@51 21 | [ |- _ = _ -> _ ] => clear H; intros; subst
adamc@51 22 end
adamc@51 23 | [ H : ?F _ _ = ?F _ _ |- _ ] => injection H;
adamc@51 24 match goal with
adamc@51 25 | [ |- _ = _ -> _ = _ -> _ ] => clear H; intros; subst
adamc@51 26 end
adamc@50 27 end.
adamc@50 28
adamc@2 29 Ltac rewriteHyp :=
adamc@2 30 match goal with
adamc@2 31 | [ H : _ |- _ ] => rewrite H
adamc@2 32 end.
adamc@2 33
adamc@2 34 Ltac rewriterP := repeat (rewriteHyp; autorewrite with cpdt in *).
adamc@2 35
adamc@2 36 Ltac rewriter := autorewrite with cpdt in *; rewriterP.
adamc@2 37
adamc@2 38 Hint Rewrite app_ass : cpdt.
adamc@2 39
adamc@51 40 Ltac sintuition := simpl in *; intuition; try simplHyp; try congruence.
adamc@2 41
adamc@38 42 Ltac crush := sintuition; rewriter; sintuition; try omega.