I recently started a post-doc in the Gallium team, and it is past due-time for my first blog post. I will not start with a research oriented blog right now (but stay tuned!); and I will rather talk about one of my hobbies: writing Coq plugins in OCaml to build new tactics. I reckon that this deviates a bit from standard practice, so I will try to make things clear.
First, a Coq proof script is usually a program written in LTac. Executing a proof script builds incrementally a proof-term. The tactics themselves are not trusted: at
Qed time, Coq checks that the proof term that was built is well-typed and that its type is the same as the statement of the theorem. One must remember that LTac tactics can always be understood in terms of manipulations of partial proof terms; and it is often instructive to get an idea of the proof term that is being built, using the
Show Proof vernacular command.
Usually, one build new tactics in LTac. LTac is a powerful domain-specific language with some interesting programming constructs, and it is possible to build powerful new tactics using a few combinators and leveraging the existing automation (builtin tactics, decision procedures and so on). I have read that LTac is vindicated as one of the strong points of Coq, and part of me agree with that statement: there is a lot of use cases in which LTac is a good tool. Yet, writing a LTac tactic is often tedious, the code that needs to be written is hard to debug, and it may be quite inefficient.
The alternative is to write custom tactics in OCaml, the meta-language that is used to implement Coq (and all the primitive tactics). In the following, I will demonstrate how to write such a tactic, and give you a handful of the necessary entry points into Coq's code.
The tactic that we are going to code is the following one, shamefully stolen from Compcert's code.
Lemma modusponens: forall (P Q: Prop), P -> (P -> Q) -> Q. Proof. auto. Qed. Ltac exploit x := refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _) _) || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _) _) (* Lots of lines elided. The actual code handle cases upto 35 arguments *) || refine (modusponens _ _ (x _ _ _) _) || refine (modusponens _ _ (x _ _) _) || refine (modusponens _ _ (x _) _).
exploit do ? Well, the best thing is to give an example. In the following context,
A, B, C, D, G : Prop H : A -> B -> C -> D ============================ G
exploit H will produce four sub-goals in which the user needs to prove
D -> G. That is, the
exploit tactic is a generalized version of the modus-ponens.
This tactic has two drawbacks. First, it is a bit inefficient: it tries to apply the
modusponens theorem to
x applied to a decreasing number of arguments (obviously we do not want to get two subgoals
(B -> C -> D) -> G). Yet, this is a pity, because most of the time, the right application has a low number of arguments, and the execution of
exploit must go through twenty-something failures before reaching a successful of
refine. The second drawback is that one has to repeat by hand the same pattern (
x followed by a given number of holes), to handle all reasonable use-cases of the tactic.
Now, we probably could imagine other (LTac) implementations of exploit, but it is not the point of this article, and you should definitely not try to do that at home! What we will do is implement this tactic as 9 lines long tactic in an OCaml plugin, way shorter than the LTac implementation.
Here we go.
let exploit (c: Termconstr) = fun gl -> (* the type of [c] is [ty] *) let ty = Tacmachpf_type_of gl c in (* In the general case, [ty] can be written as [forall (x1:t1) ... (xn:tn), t]. We decompose this arity in two parts: [ctx] which is [(xn, tn); ...; (x1,t1)] and the conclusion [t] *) let ctx, t = Termdecompose_prod_assum ty in (* We will also need the type of the conclusion of the goal *) let concl = Tacmachpf_concl gl in
We encounter functions from two modules here:
coq-v8.4/kernel/term.mlcontains the definition of Coq terms, the
constrdata-type, and various operations on it. For instance,
decompose_prod_assumtakes as arguments a
constrand decomposes it into two parts: a telescope of products (that is, a context
cxt), and the final type
t. At this point, it is crucial to note that this manipulation of terms is very syntactic: the term
tmay contain de Bruijn indices that refers to variables bound in the context. Therefore, we shall manipulate
twith some care and not forget to, e.g., lift it when needed.
coq-v8.4/proofs/tacmach.mlcontains the API that I use most often to interact with the proof machinery. For instance,
pf_type_oftakes as argument the current proof environment (that is, the goal, the typing context, and so on) and a
constr, and returns its coq type. The function
pf_conclreturns the conclusion of the current goal.
All in all, the above snippet is quite straightforward: get the type of the argument of the tactic, and the conclusion of the current goal. Nothing fancy, but here comes the meaty stuff.
Recall that a tactic builds a partial proof-term, which is a regular Coq term. Here, the proof-term that we want to generate is
(fun (x1:t1) ... (xn:tn) (m : t -> concl) => m (c x1 ... xn))
(intuitively, if we were to
apply this term in Coq, we would get a sub-goal for each of the arguments of the function)
let pf_body = TermmkApp (TermmkRel 1, [| TermmkApp (c, Termopsextended_rel_vect 1 ctx) |])
pf_body corresponds to the internal representation of the above
m (c x1 ... xn). As should be obvious with their names, the function
Term.mkApp builds an application, and
Term.mkRel builds a term that is a de Bruijn index that points to the nearest binder. The function
Termops.extended_rel_vect is slightly more complicated: it builds a vector of de Bruijn indices, lifted by 1.
Now, we need to build the
fun part. We build exactly one
lambda for each product that occurred in the type of the term
c, plus one for the parameter of type
t -> concl. To do so, we simply extend the former context with a new definition. (Note here that the type
t may depend on the context
ctx. Yet, there is no need to lift
t, because it is used in the exact same context as before; and
concl should be a closed term.)
let ctx = (NamesAnonymous,None, TermmkArrow t concl ) :: ctx in let pf_term = Termit_mkLambda_or_LetIn pf_body ctx in
Term.it_mkLambda_or_LetIn iterates the function that creates a lambda, for each of the elements of the context
ctx. Finally, we can call the built-in
apply tactics to finish the job.
Tacticsapply pf_term gl
There is one wrinkle here: with my version of Coq, the sub-goals that are generated are not in the same order as with the LTac version (which is a problem if we have to deal with backward compatibility of proof-scripts). More precisely, the proof obligation that corresponds to
t -> concl comes first. In order to avoid this problem, we will rely on a slightly more arcane piece of code.
Tacticsapply_term pf_term (Listmap (fun _ -> Evarutilmk_new_meta ()) ctx) gl
apply_term seems to be a variant of apply to which we give a term, and a list of arguments to which the term is applied. Here, we provide as arguments a bunch of
_ (in the same fashion as we would have done for
refine). For a reason that I do not fully grasp, this gives us exactly the same sub-goals as the above LTac
The last line of our OCaml plugin enrichs Coq's tactic environments with our new tactic. This declaration is made of three parts: a unique identifier
foobar (that is used internally by Coq), the syntax extension, and the actual OCaml code of the tactic (here, we simply wrap a call to
TACTIC EXTEND foobar | ["exploit" constr(c)] -> [exploit c] END;;
And that's it: mission accomplished.
There is one extra benefit to our brand new implementation of
exploit: the former version was not working properly if it was given a theorem of type, e.g.,
A -> B -> ~C. Let
D be the goal, the sub-goals that were generated were
False -> D. This short-coming is solved with our new implementation.
In the end, our new tactic is 9 lines long, compared to 20 something repetitions of the same pattern in the LTac implementation. (To be honest, we omit on this 9 lines count a few lines of boilerplate that must be written for each new OCaml tactic, like the makefile that is needed to compile the plugin.)
Moving to OCaml, we lost the safety-belt that is provided by LTac: for instance, it is possible to get the de Bruijn indices wrong by one when we build a proof-term. But it gives us the full power of the best programming language ever ;) to build our new tactics.
The plugin that was build in this tutorial is available from the public GitHub repository here. From the root of the repository
make make -f Makefile.coq install
should install the plugin in your Coq plugins directory. Then, it suffices to use the vernacular
exploit tactic, from any coq development.