--- a/src/Predicates.v	Mon Sep 29 14:38:21 2008 -0400
+++ b/src/Predicates.v	Tue Sep 30 13:11:39 2008 -0400
@@ -875,4 +875,6 @@
     %\item%#<li># [p x -> (forall x, p x -> exists y, q x y) -> (forall x y, q x y -> q y (f y)) -> exists z, q z (f z)]#</li>#
   #</ol> </li>#%\end{enumerate}%
 
+%\item%#<li># Define an inductive predicate capturing when a natural number is an integer multiple of either 6 or 10.  Prove that 13 does not satisfy your predicate, and prove that any number satisfying the predicate is not odd.  It is probably easiest to prove the second theorem by indicating "odd-ness" as equality to [2 * n + 1] for some [n].#</li>#
+
 #</ol>#%\end{enumerate}% *)

--- a/src/Tactics.v	Mon Sep 29 14:38:21 2008 -0400
+++ b/src/Tactics.v	Tue Sep 30 13:11:39 2008 -0400
@@ -11,11 +11,39 @@
 
 Require Omega.
 
+Set Implicit Arguments.
+
 
 Ltac inject H := injection H; clear H; intros; subst.
 
-Ltac simplHyp :=
+Ltac appHyps f :=
   match goal with
+    | [ H : _ |- _ ] => f H
+  end.
+
+Ltac inList x ls :=
+  match ls with
+    | x => idtac
+    | (?LS, _) => inList x LS
+  end.
+
+Ltac app f ls :=
+  match ls with
+    | (?LS, ?X) => f X || app f LS || fail 1
+    | _ => f ls
+  end.
+
+Ltac all f ls :=
+  match ls with
+    | (?LS, ?X) => f X; all f LS
+    | (_, _) => fail 1
+    | _ => f ls
+  end.
+
+Ltac simplHyp invOne :=
+  match goal with
+    | [ H : ex _ |- _ ] => destruct H
+
     | [ H : ?F _ = ?F _ |- _ ] => injection H;
       match goal with
         | [ |- _ = _ -> _ ] => clear H; intros; subst
@@ -24,6 +52,9 @@
       match goal with
         | [ |- _ = _ -> _ = _ -> _ ] => clear H; intros; subst
       end
+
+    | [ H : ?F _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; subst
+    | [ H : ?F _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; subst
   end.
 
 Ltac rewriteHyp :=
@@ -37,6 +68,45 @@
 
 Hint Rewrite app_ass : cpdt.
 
-Ltac sintuition := simpl in *; intuition; try simplHyp; try congruence.
+Definition done (T : Type) (x : T) := True.
 
-Ltac crush := sintuition; rewriter; sintuition; try omega.
+Ltac inster e trace :=
+  match type of e with
+    | forall x : _, _ =>
+      match goal with
+        | [ H : _ |- _ ] =>
+          inster (e H) (trace, H)
+        | _ => fail 2
+      end
+    | _ =>
+      match trace with
+        | (_, _) =>
+          match goal with
+            | [ H : done (trace, _) |- _ ] => fail 1
+            | _ =>
+              let T := type of e in
+                match type of T with
+                  | Prop =>
+                    generalize e; intro;
+                      assert (done (trace, tt)); [constructor | idtac]
+                  | _ =>
+                    all ltac:(fun X =>
+                      match goal with
+                        | [ H : done (_, X) |- _ ] => fail 1
+                        | _ => idtac
+                      end) trace;
+                    let i := fresh "i" in (pose (i := e);
+                      assert (done (trace, i)); [constructor | idtac])
+                end
+          end
+      end
+  end.
+
+Ltac crush' lemmas invOne :=
+  let sintuition := simpl in *; intuition; repeat (simplHyp invOne; intuition); try congruence
+    in (sintuition; rewriter;
+      repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
+        repeat (simplHyp invOne; intuition));
+      sintuition; try omega).
+
+Ltac crush := crush' tt fail.