adamc@2: (* Copyright (c) 2008, Adam Chlipala adamc@2: * adamc@2: * This work is licensed under a adamc@2: * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 adamc@2: * Unported License. adamc@2: * The license text is available at: adamc@2: * http://creativecommons.org/licenses/by-nc-nd/3.0/ adamc@2: *) adamc@2: adamc@2: Require Import List. adamc@2: adamc@38: Require Omega. adamc@38: adamc@2: adamc@2: Ltac rewriteHyp := adamc@2: match goal with adamc@2: | [ H : _ |- _ ] => rewrite H adamc@2: end. adamc@2: adamc@2: Ltac rewriterP := repeat (rewriteHyp; autorewrite with cpdt in *). adamc@2: adamc@2: Ltac rewriter := autorewrite with cpdt in *; rewriterP. adamc@2: adamc@2: Hint Rewrite app_ass : cpdt. adamc@2: adamc@35: Ltac sintuition := simpl in *; intuition. adamc@2: adamc@38: Ltac crush := sintuition; rewriter; sintuition; try omega.