## Emancipate yourself from LTac: Your first Coq plugin

- December 5, 2012
- Last updated on 2012/12/06

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 _) _).

What does `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 `A`

, `B`

, `C`

, and `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 `A`

and `(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: Term.constr) = fun gl -> (* the type of [c] is [ty] *) let ty = Tacmach.pf_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 = Term.decompose_prod_assum ty in (* We will also need the type of the conclusion of the goal *) let concl = Tacmach.pf_concl gl in

We encounter functions from two modules here:

`coq-v8.4/kernel/term.ml`

contains the definition of Coq terms, the`constr`

data-type, and various operations on it. For instance,`decompose_prod_assum`

takes as arguments a`constr`

and 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`t`

may contain de Bruijn indices that refers to variables bound in the context. Therefore, we shall manipulate`t`

with some care and not forget to, e.g., lift it when needed.`coq-v8.4/proofs/tacmach.ml`

contains the API that I use most often to interact with the proof machinery. For instance,`pf_type_of`

takes 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_concl`

returns 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 = Term.mkApp (Term.mkRel 1, [| Term.mkApp (c, Termops.extended_rel_vect 1 ctx) |])

The term `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 = (Names.Anonymous,None, Term.mkArrow t concl ) :: ctx in let pf_term = Term.it_mkLambda_or_LetIn pf_body ctx in

The function `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.

Tactics.apply 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.

Tactics.apply_term pf_term (List.map (fun _ -> Evarutil.mk_new_meta ()) ctx) gl

The function `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 `exploit`

.

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 `exploit`

):

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 `A`

, `B`

, `C`

and `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.