Gagallium

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: 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.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 =
  TermmkApp (TermmkRel 1,
              [| TermmkApp (c, Termopsextended_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 = (NamesAnonymous,None, TermmkArrow t concl ) :: ctx in 
let pf_term = Termit_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.

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

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 Require Exploit. to be able to use the exploit tactic, from any coq development.