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