Dissecting crush
For almost a year and half now I’ve been referencing one particular book on Coq, Certified Programming with Dependent Types. CPDT is a literate program on building practical things with Coq.
One of the main ideas of CPDT is that proofs ought to be fully automated. This means that a proof should be primarily a logic program (Ltac) which constructs some boring and large proof term. To this end, CPDT has a bunch of Ltac “tactics” for constructing such logic programs.
Since CPDT is a program, there’s actual working source for each of these tactics. It occurred to me today that in my 18 months of blinking uncomprehendingly at CPDT, I’ve never read its source for these tactics.
In this post, we’ll dissect how CPDT’s main tactic for automation, crush, actually works. In the process, we’ll get the chance to explore some nice, compositional, ltac engineering as well as a whole host of useful tricks.
The Code
The first step to figuring out of crush works is actually finding where it’s defined.
After downloading the source to CPDT I ran
grep "Ltac crush :=" -r .And found in src/CpdtTactics, line 205
Ltac crush := crush' false fail.Glancing at crush', I’ve noticed that it pulls in almost every tactic in CpdtTactics. Therefore, we’ll start at the top of this file and work our way done, dissecting each tactic as we go.
Incidentally, since CpdtTactics is an independent file, if you’re confused about something firing up your coq dev environment of choice and trying things out with Goal inline works nicely.
Starting from the top, our first tactic is inject.
Ltac inject H := injection H; clear H; intros; try subst.This is just a quick wrapper around injection, which also does the normal operations one wants after calling injection. It clears the original hypothesis and brings our new equalities into our environment so future tactics can use them. It also tries to swap out any variables with our new equalities using subst. Notice the try wrapper since subst is one of those few tactics that will fail if it can’t do anything useful.
Next up is
Ltac appHyps f :=
match goal with
| [ H : _ |- _ ] => f H
end.appHyps makes use of the backtracking nature of match goal with. It’ll apply f to every hypothesis in the current environment and stop once it find a hypothesis f works with.
Now we get to some combinators for working with hypothesis.
Ltac inList x ls :=
match ls with
| x => idtac
| (_, x) => idtac
| (?LS, _) => inList x LS
end.inList takes a faux-list of hypothesis and looks for an occurrence of a particular lemma x. When it finds it we just run idtac which does nothing. In the case were we can’t match x anywhere, inList will just fail with the standard “No matching clause” message.
Next we have the equivalent of appHyps for tupled lists
Ltac app f ls :=
match ls with
| (?LS, ?X) => f X || app f LS || fail 1
| _ => f ls
end.This works exactly like appHyps but instead of looking through the proofs environment, we’re looking through ls. It has the same “keep the first result that works” semantics too. One thing that confused me was the _ => f ls clause of this tactic. Remember that with our tupled lists we don’t have a “nil” member. But rather the equivalent of
A :: B :: C :: Nilis
((A, B), C)So when we don’t have a pair, ls itself is the last hypothesis in our list. As a corollary of this, there is no obvious “empty” tupled list, only one with a useless last hypothesis.
Next we have all, which runs f on every member in f ls.
Ltac all f ls :=
match ls with
| (?LS, ?X) => f X; all f LS
| (_, _) => fail 1
| _ => f ls
end.Careful readers will notice that instead of f X || ... we use ;. Additionally, if the first clause fails and the second clause matches, that means that either f X or all f LS failed. In this case we backtrack all the way back out of this clause. This should mean that this is a “all or nothing” tactic. It will either not fail on all members of ls or nothing at all will happen.
Now we get to the first big tactic
Ltac simplHyp invOne :=
let invert H F :=
inList F invOne;
(inversion H; fail)
|| (inversion H; [idtac]; clear H; try subst) in
match goal with
| [ H : ex _ |- _ ] => destruct H
| [ H : ?F ?X = ?F ?Y |- ?G ] =>
(assert (X = Y); [ assumption | fail 1 ])
|| (injection H;
match goal with
| [ |- X = Y -> G ] =>
try clear H; intros; try subst
end)
| [ H : ?F ?X ?U = ?F ?Y ?V |- ?G ] =>
(assert (X = Y); [ assumption
| assert (U = V); [ assumption | fail 1 ] ])
|| (injection H;
match goal with
| [ |- U = V -> X = Y -> G ] =>
try clear H; intros; try subst
end)
| [ 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
| [ H : existT _ ?T _ = existT _ ?T _ |- _ ] => generalize (inj_pair2 _ _ _ _ _ H); clear H
| [ H : existT _ _ _ = existT _ _ _ |- _ ] => inversion H; clear H
| [ H : Some _ = Some _ |- _ ] => injection H; clear H
end.Wow, just a little bit bigger than what we’ve been working with so far.
The first small chunk of simpleHyp is a tactic for doing clever inversion using the tuple list invOne.
invert H F :=
inList F invOne;
(inversion H; fail)
|| (inversion H; [idtac]; clear H; try subst)Here H is a hypothesis that we’re thinking about inverting on and F is the head symbol of H. First we run the inList predicate, meaning that we don’t invert upon anything that we don’t want to. If the head symbol of H is something worth inverting upon we try two different types of inversion.
In the first case inversion H; fail we’re just looking for an “easy proof” where inverting H immediately dispatches the current goal. In the second case inversion H; [idtac]; clear H; try subst, we invert upon H iff it only generates 1 subgoal. Remember that [t | t' | t''] is a tactic that runs t on the first subgoal, t’ on the second, and so on. If the number of goals don’t match, [] will fail. So [idtac] is just a clever way of saying “there’s only one new subgoal”. Next we get rid of the hypothesis we just inverted on (it’s not useful now, and we don’t want to try inverting it again) and see if any substitutions are applicable.
Alright! Now let’s talk about the massive match goal with going on in simplHyp.
The first branch is
| [ H : ex _ |- _ ] => destruct HThis just looks for a hypothesis with an existential (remember that ex is what exists desugars to). If we find one, we introduce a new variable to our environment and instantiate H with it. The fact that this doesn’t recursively call simplHyp probably means that we want to do something like repeat simplHyp to ensure this is applied everywhere.
Next we look at simplifying hypothesis where injection applies. There are two almost identical branches, one for constructors of two parameters, one for one. Let’s look at the latter since it’s slightly simpler.
| [ H : ?F ?X = ?F ?Y |- ?G ] =>
(assert (X = Y); [ assumption | fail 1 ])
|| (injection H;
match goal with
| [ |- X = Y -> G ] =>
try clear H; intros; try subst
end)This looks for an equality over a constructor F. This branch is looking to prove that X = Y, a fact deducible from the injectiveness of F.
The way that we go about doing this is actually quite a clever ltac trick though. First we assert X = Y, this will generate to subgoals, the first that X = Y (shocker) and the second is the current goal G, with the new hypothesis that X = Y. We attempt to prove that X = Y by assumption. If this works, than we already trivially can deduce X = Y so there’s no point in doing all that injection stuff so we fail 1 and bomb out of the whole branch.
If assumption fails we’ll jump to the other side of the ||s and actually use injection. We only run injection if it generates a proof that X = Y in which case we do the normal cleanup with trying to clear our original fact and do some substitution.
The next part is fairly straightforward, we make use of that invert tactic and run it over facts we have floating around in our environment
| [ H : ?F _ |- _ ] => invert H F
| [ H : ?F _ _ |- _ ] => invert H F
| [ H : ?F _ _ _ |- _ ] => invert H F
| [ H : ?F _ _ _ _ |- _ ] => invert H F
| [ H : ?F _ _ _ _ _ |- _ ] => invert H FNotice that we can now use the match to grab the leading symbol for H so we only invert upon hypothesis that we think will be useful.
Next comes a bit of axiom-fu
| [ H : existT _ ?T _ = existT _ ?T _ |- _ ] =>
generalize (inj_pair2 _ _ _ _ _ H); clear Hinj_pair2 is function that lives in the Coq standard library and has the type
forall (U : Type) (P : U -> Type) (p : U) (x y : P p),
existT P p x = existT P p y -> x = yThis relies on eq_rect_eq so it’s just a little bit dodgy for something like HoTT where we give more rope to = than just refl.
This particular branch of the match is quite straightforward though. Once we see an equality between two witnesses for the same existential type, we just generalize the equality between their proofs into our goal.
If this fails however, we’ll fall back to standard inversion with
| [ H : existT _ _ _ = existT _ _ _ |- _ ] => inversion H; clear HFinally, we have one last special case branch for Some. This is because the branches above will fail when phased with a polymorphic constructor
| [ H : Some _ = Some _ |- _ ] => injection H; clear HNothing exciting going on there.
So that wraps up simplHyp. It’s just a conglomeration of useful stuff to do to constructors in our hypothesis.
Onwards we go! Next is a simple tactic for automatically rewriting with a hypothesis
Ltac rewriteHyp :=
match goal with
| [ H : _ |- _ ] => rewrite H by solve [ auto ]
end.like most of the other tactics we saw earlier, this will hunt for an H where this works and then stop. The by solve [auto] will run solve [auto] against all the hypothesis that the rewrite generates and ensure that auto solves all the new goals. This prevents a rewrite from going and introducing obviously false facts as goals for a rewrite that made no sense.
We can combine this with autorewrite with two simple tactics
Ltac rewriterP := repeat (rewriteHyp; autorewrite with core in *).
Ltac rewriter := autorewrite with core in *; rewriterP.This just repeatedly rewrite with autorewrite and rewriteHyp as long as they can. Worth noticing here how we can use repeat to make these smaller tactics modify all applicable hypothesis rather than just one.
Next up is an innocent looking definition that frightens me a little bit
Definition done (T : Type) (x : T) := True.What frightens me about this is that Adam calls this “devious”.. and when he calls something clever or devious I’m fairly certain I’d never be able to come up with it :)
What this actually appears to do is provide a simple way to “stick” something into an environment. We can trivially prove done T x for any T and x but having this in an environment also gives us a proposition T and a ready made proof of it x! This is useful for tactics since we can do something like
assert (done SomethingUseful usefulPrf) by constructorand viola! Global state without hurting anything.
We use these in the next tactic, instr.
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)) by constructor
| _ =>
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)) by constructor)
end
end
end
end.Another big one!
This match is a little different than the previous ones. It’s not a match goal but a match type of ... with. This is used to examine one particular hypothesis’ type and match over that.
This particular match has two branches. The first deals with the case where we have uninstantiated universally quantified variables.
| forall x : _, _ =>
match goal with
| [ H : _ |- _ ] =>
inster (e H) (trace, H)
| _ => fail 2
endIf our hypothesis does, we randomly grab a hypothesis, instantiate e with it, add H to the trace list, and then recurse.
If there isn’t a hypothesis, then we fail out of the toplevel match and exit the tactic.
Now the next branch is where the real work happens
| _ =>
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)) by constructor
| _ =>
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)) by constructor)
end
end
endWe first chekc to make sure that trace isn’t empty. If this is the case, then we know that we instantiated e with at least something. If we have, we snoop around to see if there’s a done in our environment with the same trace. If this is the case, we know that we’ve done an identical instantiation of e before hand so we backtrack to try another one.
Otherwise, we look to see what e was instantiated too. If it was a simple Prop, we just stick a done record of this instantiation into our environment and add our new instantiated e back in with generalize. If e isn’t a proof, we do the same thing. In this case, however, we must also double check that the things we used to instantiate e with aren’t results of inster as well otherwise our combination of backtracking/instantiating can lead to an infinite loop.
Since this tactic generates a bunch of done’s that are otherwise useless, a tactic to clear them is helpful.
Ltac un_done :=
repeat match goal with
| [ H : done _ |- _ ] => clear H
end.Hopefully by this point this isn’t too confusing. All this tactic does is loop through the environment and clear all dones.
Now, finally, we’ve reached crush'.
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 by crush' lemmas invOne
end
end; autorewrite with core in *) in
(sintuition; rewriter;
match lemmas with
| false => idtac | _ =>
(** 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;
try omega; try (elimtype False; omega)).crush' is really broken into 3 main components.
First is a simple tactic sintuition
sintuition := simpl in *; intuition; try subst;
repeat (simplHyp invOne; intuition; try subst); try congruenceSo this first runs the normal set of “generally useful tactics” and then breaks out some of first custom tactics. This essentially will act like a souped-up version of intuition and solve goals that are trivially solvable with straightforward inversions and reductions.
Next there’s a more powerful version of rewriter
rewriter := autorewrite with core in *;
repeat (match goal with
| [ H : ?P |- _ ] =>
match P with
| context[JMeq] => fail 1
| _ => rewrite H by crush' lemmas invOne
end
end; autorewrite with core in *)This is almost identical to what we have above but instead of solving side conditions with solve [auto], we use crush' to hopefully deal with a larger number of possible rewrites.
Finally, we have the main loop of crush'.
(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)).Here we run the sintuition and rewriter and then get to work with the lemmas we supplied in lemmas.
The first branch is just a match on false, which we use like a nil. Since we have no hypothesis we don’t do anything new.
If we do have lemmas, we try instantiating both them and our hypothesis as many times as necessary and then repeatedly simplify the results. This loop will ensure that we make full use of bot our supplied lemmas and the surrounding environment.
Finally, we make another few passes with rewriter and sintuition attempting to dispatch our goal using our new, instantiated and simplified environment.
As a final bonus, if we still haven’t dispatched our goal, we’ll run omega to attempt to solve a Presburger arithmetic. On the off chance that we have something omega can be contradictory, we also try elimType false; omega to try to exploit such a contradiction.
So all crush does is call this tactic with no lemmas (false) and no suggestions to invert upon (fail). There you have it, and it only took 500 lines to get here.
Wrap Up
So that’s it, hopefully you got a few useful Ltac trick out of reading this. I certainly did writing it :)
If you enjoyed these tactics, there’s a more open-source version of these tactics, on the CPDT website. It might also interest you to read the rest of CpdtTactics.v since it has some useful gems like dep_destruct.
Last but not least, if you haven’t read CPDT itself and you’ve made it this far, go read it! It’s available as either dead-tree or online. I still reference it regularly so I at least find it useful. It’s certainly better written than this post :)
Note, all the code I’ve shown in this post is from CPDT and is licensed under ANCND license. I’ve removed some comments from the code where they wouldn’t render nicely with them.
comments powered by Disqus