Comment CpdtTactics.v

src/CpdtTactics.v

-(* 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 @@ Require Omega.
 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 @@ Ltac inList x ls :=
     | (?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 @@ Ltac all f ls :=
     | _ => 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 @@ Ltac simplHyp invOne :=
             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 @@ Ltac un_done :=
 
 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 @@ Ltac dep_destruct E :=
             | [ 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 @@ Ltac guess v H :=
                  (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'.

src/Intro.v

@@ -177,7 +177,7 @@ Previous versions of the book included some suggested exercises at the ends of c
 (**
 To make it possible to start from fancy proof automation, rather than working up to it, I have included with the book source a library of %\emph{%#<i>#tactics#</i>#%}%, or programs that find proofs, since the built-in Coq tactics do not support a high enough level of automation.  I use these tactics even from the first chapter with code examples.
 
-Some readers have asked about the pragmatics of using this tactic library in their own developments.  My position there is that this tactic library was designed with the specific examples of the book in mind; I do not recommend using it in other settings.  Part III should impart the necessary skills to reimplement these tactics and beyond.  One generally deals with undecidable problems in interactive theorem proving, so there can be no tactic that solves all goals, though the %\index{tactics!crush}%[crush] tactic that we will meet soon may sometimes feel like that!  There are still very useful tricks found in the implementations of [crush] and its cousins, so it may be useful to examine the commented source file %\texttt{%#<tt>#CpdtTactics.v#</tt>.#%}.\footnote{It's not actually commented yet. \texttt{;-)}}%  I implement a new tactic library for each new project, since each project involves a different mix of undecidable theories where a different set of heuristics turns out to work well; and that is what I recommend others do, too.
+Some readers have asked about the pragmatics of using this tactic library in their own developments.  My position there is that this tactic library was designed with the specific examples of the book in mind; I do not recommend using it in other settings.  Part III should impart the necessary skills to reimplement these tactics and beyond.  One generally deals with undecidable problems in interactive theorem proving, so there can be no tactic that solves all goals, though the %\index{tactics!crush}%[crush] tactic that we will meet soon may sometimes feel like that!  There are still very useful tricks found in the implementations of [crush] and its cousins, so it may be useful to examine the commented source file %\texttt{%#<tt>#CpdtTactics.v#</tt>.#%}.%  I implement a new tactic library for each new project, since each project involves a different mix of undecidable theories where a different set of heuristics turns out to work well; and that is what I recommend others do, too.
 *)
 
 (** ** Installation and Emacs Set-Up *)