# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1222794699 14400
# Node ID 1a664ff9d2d1a08df61fdf0115b20f6664dbe07e
# Parent  1946586b9da797986f1db196022972efe6469248
Beefed-up crush, with auto-inversion and lemma instantiation

diff -r 1946586b9da7 -r 1a664ff9d2d1 src/Predicates.v
--- 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}% *)
diff -r 1946586b9da7 -r 1a664ff9d2d1 src/Tactics.v
--- 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.