changeset 59:1a664ff9d2d1

Beefed-up crush, with auto-inversion and lemma instantiation
author Adam Chlipala <adamc@hcoop.net>
date Tue, 30 Sep 2008 13:11:39 -0400
parents 1946586b9da7
children 41ee8f8c9d17
files src/Predicates.v src/Tactics.v
diffstat 2 files changed, 75 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- 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.