This post describes the new tactic engine designed by Arnaud Spiwack which has replaced the old implementation beginning from Coq 8.5. To replace this work in its context, we first recall the history of tactics in Coq, both from the point of view of the user and the developer. There will be more OCaml code than Coq code, so please bear with me. Hopefully this will clarify things up for people outside of the cénacle of Coq developers, and provide hindsights into the current design choices.

A brief history of Coq tactics

As a Coq user, you know that your favourite proof assistant relies on a tactic language to build up proofs rather than having to write them out by hand. This has not always been the case, though. The very first releases of Coq from the end of the 80's did not feature any kind of tactic language. In those early eons where Coq source code fitted in a mere thousand of lines, Coq users had to spell every part of the proof terms. And yes, there were no implicit arguments, no notations, no coercions, in short, nothing but the kernel.

As far as I can trace it back, tactics were introduced in the 5.x branch, by the beginning of 1990. The system was rudimentary at the time and had virtually no tactic combinators. I can't resist showing you an excerpt from Coq 5.0 example files (remember, there was no stdlib either).

Goal (a:A)(m:list)~(Null (cons a m)).
Red.
Intros.
Do (resolve_unfolds) O_S.
Exact (length m).
Change <nat>(length nil)=(length (cons a m)).
Do (incomplet [3]) (f_equal length).
Assumption.
Save nil_cons.

Although this would definitely not compile on a modern Coq, we can still easily recognize an ancient dialect of today's scripts. Interestingly, tactics were considered at the time as vernacular commands of their own. Moreover, to work around the lack of expressivity of such a system, the user could stuff ML code directly in a tactic, which would then be evaluated dynamically by the toplevel. This is actually the purpose of the above Do command, which has little to do with Ltac do. For instance, Do (resolve_unfolds) O_S passes the Coq term O_S to the ML function resolve_unfolds and evaluates the result.

It would not be until ten years later, in the 7.x branch, that a true tactic language woud be introduced by David Delahaye, at last providing a proper syntax and combinators. As the French version of the CHANGES files states it, Ltac is a new layer of metalanguage to handle small automations. Unluckily, it seems that this remark did not make it into its English translation, resulting in people misusing it for a stunning range of creative hacks. Since then, the language grew organically by successive addition of haphazard primitives. Nonetheless, many of the quicks typical of Ltac can be already found in the code of version 7.0, and the core of Ltac did not really change conceptually much up to Coq 8.5.

A not-so-brief history of Coq tactics, implementationwise

Coq tactics take their roots in Milner's LCF proof assistant, so we'll start there. As a historical side-note, we should remind the unsuspicious reader that, in a surprising rôle-swapping, the ML language was actually designed in order to write LCF, not the other way around. I find this peculiarly amusing. Isn't that a chicken-or-egg issue?

LCF-style tactics

In LCF, tactics were the basic blocks of the prover. To ensure consistency of the proof, LCF simply relied on the abstractness of the type of tactics. That is to say, the user was given an abstract signature of the following form.

type tactic
val intro : tactic (** Apply the λ-abstraction rule *)
val apply : tactic (** Apply the application rule *)
val seq : tactic -> tactic -> tactic (** Compose tactics sequentially *)
(** ... More sound rules in there ... *)

By using them as trusted blackboxes, the user could build up entire scripts that were guaranteed to be valid thanks to the typing system of ML, as long as the interface did not allow unsound rules. As such, those base tactics were no more than a reification of pieces of proof derivations.

Coq architecture is sharply different. Specifically, rather than relying on a trusted set of primitive tactics, it features a full-fledged kernel checking the proof in one go. Even if this is not a desirable goal per se, this allows for unsound tactics messing badly with the proof. But this also gives the user the opportunity to free from the primitive blocks and write its own set of tactics by exposing the tactic type.

As explained before, tactics are pieces of derivations, so they can be naturally represented by the following type.

type tactic = goal -> goal list

Here goal represents the conclusion of a sequent. It may not make sense that this indeed represents pieces of derivations at a first glance, so let me explain it in words. Think for instance of the application rule.

Γ ⊢ t : A → B   Γ ⊢ u : A
=========================
      Γ ⊢ t u : B

This rule can be represented in our puzzling tactic type as a function associating to any goal [Γ ⊢ B] the list of two goals made of [Γ ⊢ A → B] and [Γ ⊢ A]. Using the same trick, all basic rules can be represented this way, potentially failing with an exception if they cannot apply. The nice thing about the inhabitants of tactic is that they have a canonical identity and composition functions satisfying the expected equivalence laws.

let id = fun gl -> [gl]
let compose f g = fun gl -> List.concat (List.map g (f gl))

That's no coincidence, and I ought to urge to explain why before the category terrorists amongst our readers start menacing me with blue-haired commutative 3-diagrams. Indeed, this representation is yet-another-instance of the Yoneda lemma, a.k.a. Cayley theorem on steroids. The one idea behind the Yoneda lemma consists in replacing a datum (e.g. group, morphism, etc.) by the interactions it can have with the external world. Here, we're replacing a rule by the transformation it performs on derivations by composition. As usual, this forms a category for free, and thus a programming language for free. End of the category parenthesis, extatic disciples of Mac Lane may return to their sesqui-pullbacks.

Proofs matter!

The LCF-style tactics are perfect to represent the rules of propositional logic, but they start to show their limitations in a dependent setting. For practicality, you want to be able to build terms incrementally just as you do for proofs. And because they appear in types, you need to be able to express partially-defined terms in types. Actually you don't have any choice in Coq, as there is no difference between proofs and terms: you must handle them alike. To this end, we manipulate partial terms with holes. They only make sense in a global state that partially associate another partial term to each hole.

Historically, Coq represented holes by the so-called metas. We will not enter in technical details, but this representation was unsound. Coq switched to evars (short for existential variable) some time ago, and the process of getting rid of legacy meta-using tactics is almost complete as of 8.5. For simplicity, the reader may think of evars as unique identifiers. The global state associating partial proofs to evars is called an evar_map in Coq parlance. It also embeds more information we will not be talking about in this post. Basically, the API of evar maps can be summarized as follows.

type evar_map
val empty : evar_map
val new_evar : evar_map -> context -> types -> evar * evar_map
val define : evar_map -> evar -> constr -> evar_map

The new_evar function creates an evar of type [Γ ⊢ _ : A] where Γ (resp. A) is the provided context (resp. type). The define function fills the evar hole with the provided term. There is also code not shown here to build a term of type A out of an evar of type [Γ ⊢ _ : A] and a set of terms instantiating Γ. Note that this is a idealization of the actual code, so take this with a grain of salt. Have a look at the Evd and Evarutil modules if you want more explicit content.

In any case, we need to account for this global state in the tactic type. This is not really difficult, we just need to stuff a state monad in there, which results in the following definition.

type tactic = goal * evar_map -> goal list * evar_map

Once again, this features nice compositional structure for free, by simply threading the state along in the previous definitions.

Tactics have been represented essentially this way from Coq 5.10 to 8.4 included, with minor variations over this general scheme. This proved to be resilient enough to sustain the passing of age.

Failure is not an option: story of a demise

It is rather miraculous that this implementation lasted so long. We devote this section to the description of the hell of pre-8.5 tactics.

In the description of LCF-style tactics, I hid a serious issue under the carpet by claiming that tactics could fail with an exception if they cannot apply. This first assumes our host language implements exceptions, but that's no big deal as we're using OCaml. The real issue there is that dynamic exceptions are well-known for being hard to manipulate properly, and tend to be caught or escape in an somehow unpredictible fashion.

An enlightening example I like to recall is the following. Coq 8.4 had a fancy bug that could be triggered following the steps below.

  • Launch the eauto tactic (on a precise goal with precise hints).
  • Out of badly designed hints, eauto starts looping.
  • Click on the « interrupt » button of the IDE.
  • And voilà, the tactic magically succeeds!

How could interrupting coqtop make it succeed? Easy, the SIGINT signal was raised as an exception while in tactic code, eventually caught by a tactic failure handler of eauto, leading it to believe that the looping hint had actually failed. Then a succeeding branch would be taken, resulting in this surprising behaviour.

This is a particular example, but similar instances of this bug were actually legion. Any seasoned Haskeller knows that this is easy to solve on paper. Just adapt the tactic type with a proper error monad, in the following way.

type tactic = goal * evar_map -> (goal list * evar_map, exn) sum

The sum type indicates whether the tactic succeeded or failed with some exception. Remark that the state is dropped in case of failure (i.e. this is a backtracking state), which is what we want for incremental refinement of terms.

Alas! To add insult to injury, the tactic type has been concrete in the API for ages, so that in Coq 8.4 virtually every tactic in the wild exploited its representation. Most tactics were indeed of the form:

let my_tactic (gl, sigma) =
  (** do some stuff on gl and modify sigma *)
  (gls, sigma')

A nice side-effect of this coding style was that the so-called evar leaks were quite frequent. Because the state was threaded by hand, it was easy to overlook a misuse of a state for another, resulting in proof terms referring to dangling evars. Who never experienced the dreaded Anomaly: Uncaught exception Not_found error?

To be fair, we should remark that there were a tribe of combinators allowing to manipulate tactics more easily, and in particular without having to resort to the type representation. E.g. tclTHEN composes tactics sequentially, tclTRY catches the error raised by its arguments, and so on. The common tcl prefix is a remnant of the past, standing for tactical, I believe. Yet, many parts of the code did exploit the representation, often even while applying those combinators!

Exposing the representation may have sounded easier in the early ages of tactic development, but this choice turned out to be a nightmare in the long run. Every reasonable developer knows the only viable fix to this situation: abstract the tactic type and provide an expressive set of primitives, just as in the good old LCF times.

Unluckily, there was no magic incantation to solve this: one had to put up their sleeves and rewrite the thousands of ML lines of tactics using abstract primitives. Easier said than done. This required a lot of tough work, and as of Coq 8.5 the rewriting process is not entirely finished, as small bits of legacy code are still lurking around.

Tactics in Coq 8.5

In Coq 8.5, the tactic engine has been made much more expressive than what can be achieved by the tactic type of the previous section. Indeed, having an abstract type for tactics allows to change the actual implementation without much fuss. So why stick to the old model if we can get a bunch of killer-features for free?

Note though that in what follows, the exposed implementations are actually not those of Coq. They are here for pedagogical purpose, and I'll probably dedicate another post to the infernal history of the implementation of the new tactic engine. The types are nonetheless very close to the API found in the Proofview module, providing the core functionalities of the tactic engine.

Tactics form a monad

By applying the one design pattern of functional programming, it is immediate to realize that the tactic type forms a monad, by adding a return argument.

type +'a tactic (* morally = goal * state -> (goal list * state * 'a, exn) sum *)

The old tactic type amounts to force the return type to always be unit, which permits to summarize everything we did before. Our monad comes with its standard sequencing operators which are described in the Proofview module.

val tclUNIT : 'a -> 'a tactic
val tclBIND : 'a tactic -> ('a -> 'b tactic) -> 'b tactic

Expectedly, these primitives satisfy the usual equational rules of monads, where >>= is an infix notation for tclBIND.

(tclUNIT x >>= f) ≡ f x
(t >>= tclUNIT) ≡ t
((t >>= f) >>= g) ≡ (t >>= fun x -> f x >>= g)

For usability, we also derive from them a lot of combinators for lists and the like in the API, although we will not describe them here.

I am the State

As in the legacy implementation, there is a notion of global state in the monad called the proofview. It is made of various data, but the most important one is obviously the evar_map representing the current proof term as a bunch of partial terms and pointers between them. You can retrieve the evar_map and modify it using the following primitives.

val tclEVARMAP : evar_map tactic

module Unsafe : sig
  val tclEVARS : evar_map -> unit tactic
end

Note that setting the evar_map using the tclEVARS function is deemed unsafe because you can mess badly with the invariants of the engine using it. In a nutshell, you should only update the evar_map with another one which is more refined that the current state, i.e. where you have solved more holes in the proof term, otherwise you are creating an evar leak. Furthermore, because of the universe polymorphism feature introduced in 8.5, an evar_map also carries a local graph of universes, and dropping constraints nonchalantly by misusing tclEVARS can effectively result in nasty kernel anomalies that are hard to track. This is why some higher-level, safe functions are provided in the API, while tclEVARS is used to implement them.

As usual, these operators satisfy the rules of a state monad, e.g. getting twice yields the same result, setting twice is equivalent to only setting the last one, and so on.

Many errors are better than one

The new engine also features a rich backtracking mechanism. Instead of only being able to succeed or fail, we can now succeed several times. This corresponds implementationwise to replace the sum return value into a full-fledged list, or more precisely an error list.

(** Intuitive implementation of the monad *)
type 'a elist = Node of (exn -> 'a enode)
and 'a enode = Zero of exn | Or of 'a * 'a elist

type +'a tactic = goal * state -> (goal list * state * 'a) elist

The idea is that we want to be able to know with which error we failed, so that we need to enrich our list with a potential exception, resulting in the 'a elist type instead of the plain 'a list type, just as the ('a, exn) sum type is an exception-enriched variant of the 'a option type. In the list case, we need to interleave the constructors with exception reading, otherwise this would not form a monad. Such a requirement is already at work in the correct list monad transformer, whose original naive implementation was not a monad.

This provides us with the error-related primitives below.

val tclZERO : exn -> 'a tactic
val tclOR : 'a tactic -> (exn -> 'a tactic) -> 'a tactic
type 'a case =
  | Fail of exn
  | Next of 'a * (exn -> 'a tactic)
val tclCASE : 'a tactic -> 'a case tactic

The correct mental model is that tclZERO is the empty exception-enriched list, tclOR is the concatenation, and tclCASE is pattern-matching over those lists, i.e. we have the following equations.

(tclZERO e >>= f) ≡ tclZERO e
(tclOR t k >>= f) ≡ tclOR (t >>= f) (fun e -> k e >>= f)

tclOR (tclZERO e) k ≡ k e
tclOR t tclZERO ≡ t
tclOR (tclOR t k₁) k₂ ≡ tclOR t (fun e -> tclOR (k₁ e) k₂)

tclCASE (tclZERO e) ≡ tclUNIT (Fail e)
tclCASE (tclOR (tclUNIT x) k) ≡ tclUNIT (Next (x, k))

The API also provides a handful of derived operators for practicality. It is noteworthy to remark that in the current implementation, the tclCASE is a very costly operation, because it forces the evaluation of the list, and should be avoided in favour of the specialized functions when possible.

We need to explain how the backtracking effect interacts with the state effect. As it may be obvious from the intuitive implementation, the proof state is synchronized with backtrack, i.e. when failing the current state is discarded and restored from the last backtracking point. This is what we want: failing should undo the partial refinement you made in the current branch. We have for instance the equation below when t only modifies the global proof state.

tclOR (t >>= fun () -> tclZERO e) k ≡ k e

Here, all effects t may have done on the proof state are not taken into account by k, which would not be the case if the state was non-backtracking.

Losing focus

Another important feature of the new engine is the possibility to manipulate goals as a whole, instead of always having to be focussed on a goal. This is useful to write tactics that reorder goals or focus on a particular set of goals for example. This also has some drawbacks though, as there is not anymore a notion of the current environment as each goal comes with its own context. This has consequences on the evaluation model of Ltac, I'll get back to this point later. On the positive side, this is not difficult to implement: it is sufficient to embed the list of currently focussed goals into the proof state.

(** Intuitive implementation of the monad *)
type state = goal list * evar_map * more_stuff
type +'a tactic = state -> (state * 'a) elist

Manipulating goals is then fairly easy, as it suffices to use the corresponding state operators. The Proofview module provides some primitives to do this abstractly. Here is a short excerpt of the API.

(** If [n] is positive, [cycle n] puts the [n] first goal last. If [n]
    is negative, then it puts the [n] last goals first.*)
val cycle : int -> unit tactic

(** [swap i j] swaps the position of goals number [i] and [j]. *)
val swap : int -> int -> unit tactic

(** [revgoals] reverses the list of focused goals. *)
val revgoals : unit tactic

(** [numgoals] returns the number of goals under focus. *)
val numgoals : int tactic

The missing feature we really need is the ability to focus on each goal individually to recover the old behaviour where we had a goal at hand. The main primitives are the following.

module Goal :
sig
  type 'a t
  val enter : ([ `LZ ] t -> unit tactic) -> unit tactic
  val nf_enter : ([ `NF ] t -> unit tactic) -> unit tactic
end

The 'a Goal.t type represents focussed goals, where the 'a parameter is a phantom type indicating whether the goal has been evar-normalized (`NF for normal form) or not (`LZ for lazy). Indeed, legacy tactics expect terms appearing in goals to be evar-normal, i.e. all defined evars should be substituted by their body. This is a costly operation not necessary in many cases, so be do our best to avoid doing it, and we statically ensure we do not need it thanks to the phantom type.

The semantic of enter f is straightforward:

  • Retrieve the list of goals currently being proved
  • Apply f on each goal from left to right
  • The new list of goals is the concatenation of the goals returned by each call to f in the same order

The order of application is important, as f may be effectful. The nf_enter function is a variant that normalizes goals beforehand.

Finally, the self-explanatory API for goal manipulation gives access to the contents of goals.

module Goal :
sig
  val concl : [ `NF ] t -> constr
  val hyps : [ `NF ] t -> Context.named_context
  val env : 'a t -> Environ.env
  val sigma : 'a t -> evar_map
end

Remark that functions returning terms expect the goal to be normalized. There is a primitive to get around this limitation when you are sure that you do not depend on being normalized.

In practice, most tactics depend on a given goal, so that the following boilerplate coding style is pervasive in the source code of Coq.

let my_tactic args = Proofview.Goal.nf_enter begin fun gl ->
  let concl = Proofview.Goal.concl gl in
  let hyps = Proofview.Goal.hyps gl in
  let sigma = Proofview.Goal.sigma gl in
  (** Do something useful at last *)
end

Refinement

All the above API is not really useful to make the proof progress, as they are mostly geared towards combination of more primitive tactics or read-only features. The basic feature of Coq 8.5 allowing to write actual proof terms is the refine primitive, that allows to fill the current hole with a user-provided partial proof term.

module Refine : sig
  val refine : (evar_map -> evar_map * constr) -> unit tactic
  (** In [refine t], [t] is a term with holes under some
      [evar_map] context. The term [t] is used as a partial solution
      for the current goal (refine is a goal-dependent tactic), the
      new holes created by [t] become the new subgoals. Exception
      raised during the interpretation of [t] are caught and result in
      tactic failures. *)
end

This is actually easy to use. The user simply has to feed this function with an argument f of type evar_map -> evar_map * constr representing a partial term. The f function is given the current evar map, and may create new evars from it, eventually using them to construct the returned term, which is in turn used to solve the current goal. All such new evars are retrieved at the end of the function invocation and are added as new goals. This tactic enters the current goals before applying f, so that f may be applied several times with distinct arguments.

Note that the type of this function is not fully satisfactory, as you can still mess with the returned evar map. It is expected that f uses a strict state-passing style, otherwise this will surely be the source of evar leaks.

Compatibility layer

For completeness, we should mention that the new engine features a compatibility layer for the old tactics. The main functions are provided by the module Proofview.V82.

module V82 : sig
  type tac = evar * evar_map -> evar list * evar_map
  val tactic : tac -> unit tactic
  val of_tactic : 'a tactic -> tac
end

Those functions are not perfect though, as there may be small discrepancy between the expressivity of both implementations. Most notably, of_tactic loses the backtracking behaviour of the underlying tactic, while tactic may confuse goals solved by global side-effect. The other important compatibility layer is provided by the Tacmach.New module, in particular the of_old function.

val of_old : (evar * evar_map -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a

It allows to port functions using the old representation of goals to the new one.

Ltac wants its focussing back

This section is not really useful for the writing of ML tactics by the user. Yet, it provides the reader with an understanding of the semantical problems faced when transitioning Ltac to this new architecture, so we think it is useful to mention in this post.

The non-focussed nature of the new tactic engine unluckily clashes with the (unspecified) semantics of Ltac. Indeed, we want to be able to have Ltac primitive such as cycle that act on all goals at once, while we also want to enter goals at will, e.g. writing let c := constr:(x) in tac where x is a hypothesis of the current goal, which does not make sense when there is no focussed goal in sight. Therefore, adding global tactics while retaining the old behaviour turned out to be a real can of worms.

We mitigated this issue by adding a new monadic layer, called Ftactic, for focussing tactics (f-tactic for brevity). The idea is the following: we cannot decide when to interpret an Ltac expression in a focus statically, thus we will decide this dynamically. The type 'a Ftactic.t will stand for potentially focussed tactics returning an 'a when the tactic is not focussed, and a list of 'a of the same length of the the list of focussed goals when the tactic is focussed. Once a f-tactic is focussed, there is no turning back: it will remain focussed until the end.

We describe briefly the API of module Ftactic below.

type +'a focus

type +'a t = 'a focus Proofview.tactic
(** The type of f-tactics. A f-tactic is like a normal tactic, except that it is
    able to remember it has entered a goal. Whenever this is the case, each
    subsequent effect of the tactic is dispatched on the focussed goals. *)

val return : 'a -> 'a t
val bind : 'a t -> ('a -> 'b t) -> 'b t

val lift : 'a Proofview.tactic -> 'a t
(** Transform a tactic into a non-focussed f-tactic. *)

val enter : ([ `LZ ] Proofview.Goal.t -> 'a t) -> 'a t
(** Enter a goal. The resulting tactic is focussed. *)

val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic
(** Given a continuation producing a tactic, evaluates the f-tactic. *)

That is pretty much all of the basic primitives. This is a monad, so you have the standard monadic combinators at your disposal. You can turn any tactic into a non-focussed f-tactic using the lift primitive, and you can make a f-tactic focussed by using the enter primitive. The run primitive allows to escape into usual tactics: if the f-tactic passed as an argument is not focussed, then the continuation is evaluated once, otherwise it is called in each of the currently focussed goals.

There is a catch in this API, which is that we partially expose the implementation of this monad by definining the abstract container type 'a focus. Morally, an 'a focus is either a non-focussed, single argument, or a list of arguments of the same length as the currently focussed goals. We could actually write the monad implementation in a dependently language, such as Coq, as follows.

(** If Coq were written in Coq. Sigh! *)
Definition state := list goal * evar_map * more_stuff.

Inductive focus (s : state) A :=
| Global : A -> focus s A
| Focussed : forall l : list A, length (fst s) = length l -> focus s A.

Definition t A :=
  forall s : state, elist { s' : state & focus s' A }.

Unluckily, we do require the access to the implementation, because it is not clear how this monad should interact with the backtracking primitives and the like. By simply exposing that it is a particular case of a tactic, we can rely on the primitives features by the tactic API. As of today, it is still unclear how to solve this.

Conclusion

That is all for this inaugural post. We hope that it has clarified your mind regarding the semantics of the new tactic engine, so that you can use it without fuss in your ML plugins. There is some additional API I did not describe, in particular how to include IO-like effects in the tactic, including non-backtracking state.

I will also probably describe the actual implementation as well as its evolution between Arnaud's first implementation and 8.5 release in a later post, for it had a complicated history. Indeed, the practical design of the new engine pushed OCaml into misknown limitations involving tail-recursivity, the GC and inefficiency of towers of functors that required a careful thinking to work around.

Do not hesitate to ask questions in the comments if some points remain obscure to you!