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@50: Ltac simplHyp :=
adamc@50:   match goal with
adamc@50:     | [ H : S _ = S _ |- _ ] => injection H; clear H; intros; subst
adamc@50:   end.
adamc@50: 
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@50: Ltac sintuition := simpl in *; intuition; try simplHyp.
adamc@2: 
adamc@38: Ltac crush := sintuition; rewriter; sintuition; try omega.