Mercurial > cpdt > repo
annotate src/Tactics.v @ 51:9ceee967b1fc
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. |