--- a/src/CpdtTactics.v	Thu Apr 12 16:27:28 2012 -0400
+++ b/src/CpdtTactics.v	Thu Apr 12 18:41:32 2012 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2011, Adam Chlipala
+(* Copyright (c) 2008-2012, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -14,13 +14,16 @@
 Set Implicit Arguments.
 
 
+(** A version of [injection] that does some standard simplifications afterward: clear the hypothesis in question, bring the new facts above the double line, and attempt substitution for known variables. *)
 Ltac inject H := injection H; clear H; intros; try subst.
 
+(** Try calling tactic function [f] on all hypotheses, keeping the first application that doesn't fail. *)
 Ltac appHyps f :=
   match goal with
     | [ H : _ |- _ ] => f H
   end.
 
+(** Succeed iff [x] is in the list [ls], represented with left-associated nested tuples. *)
 Ltac inList x ls :=
   match ls with
     | x => idtac
@@ -28,12 +31,14 @@
     | (?LS, _) => inList x LS
   end.
 
+(** Try calling tactic function [f] on every element of tupled list [ls], keeping the first call not to fail. *)
 Ltac app f ls :=
   match ls with
     | (?LS, ?X) => f X || app f LS || fail 1
     | _ => f ls
   end.
 
+(** Run [f] on every element of [ls], not just the first that doesn't fail. *)
 Ltac all f ls :=
   match ls with
     | (?LS, ?X) => f X; all f LS
@@ -41,15 +46,28 @@
     | _ => f ls
   end.
 
+(** Workhorse tactic to simplify hypotheses for a variety of proofs.
+   * Argument [invOne] is a tuple-list of predicates for which we always do inversion automatically. *)
 Ltac simplHyp invOne :=
+  (** Helper function to do inversion on certain hypotheses, where [H] is the hypothesis and [F] its head symbol *)
   let invert H F :=
-    inList F invOne; (inversion H; fail)
-    || (inversion H; [idtac]; clear H; try subst) in
+    (** We only proceed for those predicates in [invOne]. *)
+    inList F invOne;
+    (** This case covers an inversion that succeeds immediately, meaning no constructors of [F] applied. *)
+      (inversion H; fail)
+    (** Otherwise, we only proceed if inversion eliminates all but one constructor case. *)
+      || (inversion H; [idtac]; clear H; try subst) in
+
   match goal with
+    (** Eliminate all existential hypotheses. *)
     | [ H : ex _ |- _ ] => destruct H
 
+    (** Find opportunities to take advantage of injectivity of data constructors, for several different arities. *)
     | [ H : ?F ?X = ?F ?Y |- ?G ] =>
+      (** This first branch of the [||] fails the whole attempt iff the arguments of the constructor applications are already easy to prove equal. *)
       (assert (X = Y); [ assumption | fail 1 ])
+      (** If we pass that filter, then we use injection on [H] and do some simplification as in [inject].
+         * The odd-looking check of the goal form is to avoid cases where [injection] gives a more complex result because of dependent typing, which we aren't equipped to handle here. *)
       || (injection H;
         match goal with
           | [ |- X = Y -> G ] =>
@@ -64,63 +82,84 @@
             try clear H; intros; try subst
         end)
 
+    (** Consider some different arities of a predicate [F] in a hypothesis that we might want to invert. *)
     | [ H : ?F _ |- _ ] => invert H F
     | [ H : ?F _ _ |- _ ] => invert H F
     | [ H : ?F _ _ _ |- _ ] => invert H F
     | [ H : ?F _ _ _ _ |- _ ] => invert H F
     | [ H : ?F _ _ _ _ _ |- _ ] => invert H F
 
+    (** Use an (axiom-dependent!) inversion principle for dependent pairs, from the standard library. *)
     | [ H : existT _ ?T _ = existT _ ?T _ |- _ ] => generalize (inj_pair2 _ _ _ _ _ H); clear H
+
+    (** If we're not ready to use that principle yet, try the standard inversion, which often enables the previous rule. *)
     | [ H : existT _ _ _ = existT _ _ _ |- _ ] => inversion H; clear H
 
+    (** Similar logic to the cases for constructor injectivity above, but specialized to [Some], since the above cases won't deal with polymorphic constructors. *)
     | [ H : Some _ = Some _ |- _ ] => injection H; clear H
   end.
 
+(** Find some hypothesis to rewrite with, ensuring that [auto] proves all of the extra subgoals added by [rewrite]. *)
 Ltac rewriteHyp :=
   match goal with
-    | [ H : _ |- _ ] => rewrite H; auto; [idtac]
+    | [ H : _ |- _ ] => rewrite H by solve [ auto ]
   end.
 
+(** Combine [autorewrite] with automatic hypothesis rewrites. *)
 Ltac rewriterP := repeat (rewriteHyp; autorewrite with core in *).
-
 Ltac rewriter := autorewrite with core in *; rewriterP.
 
+(** This one is just so darned useful, let's add it as a hint here. *)
 Hint Rewrite app_ass.
 
+(** Devious marker predicate to use for encoding state within proof goals *)
 Definition done (T : Type) (x : T) := True.
 
+(** Try a new instantiation of a universally quantified fact, proved by [e].
+   * [trace] is an accumulator recording which instantiations we choose. *)
 Ltac inster e trace :=
+  (** Does [e] have any quantifiers left? *)
   match type of e with
     | forall x : _, _ =>
+      (** Yes, so let's pick the first context variable of the right type. *)
       match goal with
         | [ H : _ |- _ ] =>
           inster (e H) (trace, H)
         | _ => fail 2
       end
     | _ =>
+      (** No more quantifiers, so now we check if the trace we computed was already used. *)
       match trace with
         | (_, _) =>
+          (** We only reach this case if the trace is nonempty, ensuring that [inster] fails if no progress can be made. *)
           match goal with
-            | [ H : done (trace, _) |- _ ] => fail 1
+            | [ H : done (trace, _) |- _ ] =>
+              (** Uh oh, found a record of this trace in the context!  Abort to backtrack to try another trace. *)
+              fail 1
             | _ =>
+              (** What is the type of the proof [e] now? *)
               let T := type of e in
                 match type of T with
                   | Prop =>
+                    (** [e] should be thought of as a proof, so let's add it to the context, and also add a new marker hypothesis recording our choice of trace. *)
                     generalize e; intro;
-                      assert (done (trace, tt)); [constructor | idtac]
+                      assert (done (trace, tt)) by constructor
                   | _ =>
+                    (** [e] is something beside a proof.  Better make sure no element of our current trace was generated by a previous call to [inster], or we might get stuck in an infinite loop!  (We store previous [inster] terms in second positions of tuples used as arguments to [done] in hypotheses.  Proofs instantiated by [inster] merely use [tt] in such positions.) *)
                     all ltac:(fun X =>
                       match goal with
                         | [ H : done (_, X) |- _ ] => fail 1
                         | _ => idtac
                       end) trace;
+                    (** Pick a new name for our new instantiation. *)
                     let i := fresh "i" in (pose (i := e);
-                      assert (done (trace, i)); [constructor | idtac])
+                      assert (done (trace, i)) by constructor)
                 end
           end
       end
   end.
 
+(** After a round of application with the above, we will have a lot of junk [done] markers to clean up; hence this tactic. *)
 Ltac un_done :=
   repeat match goal with
            | [ H : done _ |- _ ] => clear H
@@ -128,29 +167,49 @@
 
 Require Import JMeq.
 
+(** A more parameterized version of the famous [crush].  Extra arguments are:
+   * - A tuple-list of lemmas we try [inster]-ing 
+   * - A tuple-list of predicates we try inversion for *)
 Ltac crush' lemmas invOne :=
-  let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence in
-    let rewriter := autorewrite with core in *;
-      repeat (match goal with
-                | [ H : ?P |- _ ] =>
-                  match P with
-                    | context[JMeq] => fail 1
-                    | _ => (rewrite H; [])
-                      || (rewrite H; [ | solve [ crush' lemmas invOne ] ])
-                        || (rewrite H; [ | solve [ crush' lemmas invOne ] | solve [ crush' lemmas invOne ] ])
-                  end
-              end; autorewrite with core in *)
-    in (sintuition; rewriter;
-        match lemmas with
-          | false => idtac
-          | _ => repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
-            repeat (simplHyp invOne; intuition)); un_done
-        end; sintuition; rewriter; sintuition; try omega; try (elimtype False; omega)).
+  (** A useful combination of standard automation *)
+  let sintuition := simpl in *; intuition; try subst;
+    repeat (simplHyp invOne; intuition; try subst); try congruence in
 
+  (** A fancier version of [rewriter] from above, which uses [crush'] to discharge side conditions *)
+  let rewriter := autorewrite with core in *;
+    repeat (match goal with
+              | [ H : ?P |- _ ] =>
+                match P with
+                  | context[JMeq] => fail 1 (** JMeq is too fancy to deal with here. *)
+                  | _ => rewrite H by crush' lemmas invOne
+                end
+            end; autorewrite with core in *) in
+
+  (** Now the main sequence of heuristics: *)
+    (sintuition; rewriter;
+      match lemmas with
+        | false => idtac (** No lemmas?  Nothing to do here *)
+        | _ =>
+          (** Try a loop of instantiating lemmas... *)
+          repeat ((app ltac:(fun L => inster L L) lemmas
+          (** ...or instantiating hypotheses... *)
+            || appHyps ltac:(fun L => inster L L));
+          (** ...and then simplifying hypotheses. *)
+          repeat (simplHyp invOne; intuition)); un_done
+      end;
+      sintuition; rewriter; sintuition;
+      (** End with a last attempt to prove an arithmetic fact with [omega], or prove any sort of fact in a context that is contradictory by reasoning that [omega] can do. *)
+      try omega; try (elimtype False; omega)).
+
+(** [crush] instantiates [crush'] with the simplest possible parameters. *)
 Ltac crush := crush' false fail.
 
+(** * Wrap Program's [dependent destruction] in a slightly more pleasant form *)
+
 Require Import Program.Equality.
 
+(** Run [dependent destruction] on [E] and look for opportunities to simplify the result.
+   The weird introduction of [x] helps get around limitations of [dependent destruction], in terms of which sorts of arguments it will accept (e.g., variables bound to hypotheses within Ltac [match]es). *)
 Ltac dep_destruct E :=
   let x := fresh "x" in
     remember E as x; simpl in x; dependent destruction x;
@@ -158,11 +217,14 @@
             | [ H : _ = E |- _ ] => rewrite <- H in *; clear H
           end.
 
+(** Nuke all hypotheses that we can get away with, without invalidating the goal statement. *)
 Ltac clear_all :=
   repeat match goal with
            | [ H : _ |- _ ] => clear H
          end.
 
+(** Instantiate a quantifier in a hypothesis [H] with value [v], or, if [v] doesn't have the right type, with a new unification variable.
+   * Also prove the lefthand sides of any implications that this exposes, simplifying [H] to leave out those implications. *)
 Ltac guess v H :=
   repeat match type of H with
            | forall x : ?T, _ =>
@@ -171,17 +233,18 @@
                  (let H' := fresh "H'" in
                    assert (H' : T); [
                      solve [ eauto 6 ]
-                     | generalize (H H'); clear H H'; intro H ])
+                     | specialize (H H'); clear H' ])
                  || fail 1
                | _ =>
-                 (generalize (H v); clear H; intro H)
+                 specialize (H v)
                  || let x := fresh "x" in
                    evar (x : T);
-                   let x' := eval cbv delta [x] in x in
-                     clear x; generalize (H x'); clear H; intro H
+                   let x' := eval unfold x in x in
+                     clear x; specialize (H x')
              end
          end.
 
+(** Version of [guess] that leaves the original [H] intact *)
 Ltac guessKeep v H :=
   let H' := fresh "H'" in
     generalize H; intro H'; guess v H'.