Beefed-up crush, with auto-inversion and lemma instantiation

src/Predicates.v

@@ -875,4 +875,6 @@ Qed.
     %\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}% *)

src/Tactics.v

@@ -11,11 +11,39 @@ Require Import List.
 
 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 @@ Ltac simplHyp :=
       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 @@ Ltac rewriter := autorewrite with cpdt in *; rewriterP.
 
 Hint Rewrite app_ass : cpdt.
 
-Ltac sintuition := simpl in *; intuition; try simplHyp; try congruence.
+Definition done (T : Type) (x : T) := True.
+
+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 := sintuition; rewriter; sintuition; try omega.
+Ltac crush := crush' tt fail.