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@59: Set Implicit Arguments.
adamc@59: 
adamc@2: 
adamc@51: Ltac inject H := injection H; clear H; intros; subst.
adamc@51: 
adamc@59: Ltac appHyps f :=
adamc@50:   match goal with
adamc@59:     | [ H : _ |- _ ] => f H
adamc@59:   end.
adamc@59: 
adamc@59: Ltac inList x ls :=
adamc@59:   match ls with
adamc@59:     | x => idtac
adamc@59:     | (?LS, _) => inList x LS
adamc@59:   end.
adamc@59: 
adamc@59: Ltac app f ls :=
adamc@59:   match ls with
adamc@59:     | (?LS, ?X) => f X || app f LS || fail 1
adamc@59:     | _ => f ls
adamc@59:   end.
adamc@59: 
adamc@59: Ltac all f ls :=
adamc@59:   match ls with
adamc@59:     | (?LS, ?X) => f X; all f LS
adamc@59:     | (_, _) => fail 1
adamc@59:     | _ => f ls
adamc@59:   end.
adamc@59: 
adamc@59: Ltac simplHyp invOne :=
adamc@59:   match goal with
adamc@59:     | [ H : ex _ |- _ ] => destruct H
adamc@59: 
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@59: 
adamc@59:     | [ H : ?F _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; subst
adamc@59:     | [ H : ?F _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; 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@59: Definition done (T : Type) (x : T) := True.
adamc@2: 
adamc@59: Ltac inster e trace :=
adamc@59:   match type of e with
adamc@59:     | forall x : _, _ =>
adamc@59:       match goal with
adamc@59:         | [ H : _ |- _ ] =>
adamc@59:           inster (e H) (trace, H)
adamc@59:         | _ => fail 2
adamc@59:       end
adamc@59:     | _ =>
adamc@59:       match trace with
adamc@59:         | (_, _) =>
adamc@59:           match goal with
adamc@59:             | [ H : done (trace, _) |- _ ] => fail 1
adamc@59:             | _ =>
adamc@59:               let T := type of e in
adamc@59:                 match type of T with
adamc@59:                   | Prop =>
adamc@59:                     generalize e; intro;
adamc@59:                       assert (done (trace, tt)); [constructor | idtac]
adamc@59:                   | _ =>
adamc@59:                     all ltac:(fun X =>
adamc@59:                       match goal with
adamc@59:                         | [ H : done (_, X) |- _ ] => fail 1
adamc@59:                         | _ => idtac
adamc@59:                       end) trace;
adamc@59:                     let i := fresh "i" in (pose (i := e);
adamc@59:                       assert (done (trace, i)); [constructor | idtac])
adamc@59:                 end
adamc@59:           end
adamc@59:       end
adamc@59:   end.
adamc@59: 
adamc@59: Ltac crush' lemmas invOne :=
adamc@59:   let sintuition := simpl in *; intuition; repeat (simplHyp invOne; intuition); try congruence
adamc@59:     in (sintuition; rewriter;
adamc@59:       repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
adamc@59:         repeat (simplHyp invOne; intuition));
adamc@59:       sintuition; try omega).
adamc@59: 
adamc@59: Ltac crush := crush' tt fail.