# A Few of my Favorite Tactics

Having used Coq for a good while now, I’ve slowly begun to accumulate my own set of hand-written tactics. Writing your own tactics can be frustrating at first; Ltac is dynamic and stateful, the polar opposite of the Gallina we all love. But after some time, you’re sure to start writing tactics that you’re surprised you ever lived without.

In this post, I’ll go through some of my personal favorite tactics I’ve written, with the hope that these examples show how Ltac can be used to make your proofs easier, and perhaps inspire you to write your own tactics. They are listed very roughly in accordance to their complexity and inter-dependencies.

A basic understanding of Ltac is assumed. If you are having trouble following along, I suggest you refer to the following documentation:

Documentation may be dry, but there’s not better way to hone your understanding!

Let’s jump in.

# 1. `find`

`find`

is a higher-order tactic which takes a tactic as an argument. It then applies said tactic to the first hypothesis to make progress.

This is useful shorthand when searching for a hypothesis, or when one would prefer not to use a hypothesis’s name. For example, one could re-define the `assumption`

tactic as `find (fun H => exact H)`

.

There are a myriad of reasons one might want to avoid explicitly using an identifier. It can be easier (as is the case with `assumption`

), but it can also be more maintainable. Identifiers within a proof are fragile, especially if introduced implicitly.

Before moving on, let’s note a technical detail in the above definition. The `tac`

argument is given the nonterminal `tactic3`

. Tactic expressions have 6 precedence levels, with 0 representing maximal precedence, and 5 representing minimal precedence. Precedence is necessary to disambiguate tactic expressions such as `a by b; c`

. Should this be interpreted as `a by (b; c)`

, or `(a by b); c`

? This depends on the precedence of the argument `b`

to `a`

. At tactic level 3, which we will use all throughout this post for consistency, it is parsed as `(a by b); c`

.

# 2. `define`

By and large, tactics are used to construct *opaque* terms. With the exception of tactics like `set`

and `pose`

, the definitions of most terms we add to our hypothesis list are completed forgotten; only their type is retained. Most often this is desirable, but occasionally we’d like to actually retain the definition of a term we build tactically.

We introduce a family of such functions called `define`

. The first version behaves much like assert.

Here, `evar`

creates a unification variable of our desired type. Wrapping the tactic in `unshelve`

immediately focuses the newly created unification variable into the first subgoal. Once we clear that goal, the new hypothesis will be available, as in `assert`

, but this time, it will be fully visible, having just been built via unification.

You may notice from the above tactic definitions just how verbose and redundant it is to support the idiomatic optional clauses such as the `as`

and `by`

clauses, since we have to give an instance for each combination of usage. Later in the post, we’ll omit these obvious derivatives when they become to cumbersome.

A common scenario in which we’d like to retain a term’s definition is when we are trying to prove an existential. Therefore, we create a version of define which works specifically on existentials.

Again, we use the `unshelve`

trick, this time with `eexists`

.

# 3. `forward`

Given a functional hypothesis `H : forall a: A, B a`

, or in the nondependent case,
`H : A -> B`

, `forward H`

focuses the new subgoal `A`

, which it then uses to specialize `H`

. The name therefore comes from the concept of “forward reasoning”.

To accomplish our task, we use the previous `define`

tactic to build our term, which we then specialize our hypothesis `H`

with. We then remove the intermediate term from our hypotheses by unfolding its definition in the now specialized hypothesis `H`

, and clear it.

Why do we use `define`

here instead of one of a standard tactic? I.e., why do we want the specializing term to be transparent? In the nondependent case `H : A -> B`

, it won’t make a difference. However, for the dependent case `H : forall a: A, B a`

, the particular term `a: A`

is generally significant, and therefore shouldn’t be obscured.

# 4. `(dependent) inv(c)`

Inversion in Coq can get downright *ugly*. The proof state is often absolutely littered with new hypotheses. There are only so many times one can write `inversion H; subst`

before creating a shorthand. We introduce such a shorthand with the tactic `inv`

. Similarly, `invc H`

will perform `inv H`

, then `clear H`

, which I find is desirable more often than not.

(Note: I did not come up with the `inv`

and `invc`

tactics myself. I found them originally in the StructTact library, and modified them to my liking).

Beyond the behavior I described, you can see in these definitions some extra features. For instance, we strengthen `subst`

to clear syntactically reflexive equalities, and we rename to-be-cleared hypotheses to free up identifiers.

Note also in the `invc`

variants that we have to wrap our `clear`

with a `try`

. Some inversions will actually clear the hypothesis automatically (most notably inversions on equalities), and we don’t want `invc`

to fail on such hypotheses.

We can continue making improvements on inversion. One very common issue arises when you invoke inversion on highly dependent terms. You will often end up with hypotheses of type `existT P p x = existT P p y`

. Intuitively, we would expect this to imply `x = y`

, but this is in fact not provable without an additional axiom, so regular inversion does not perform this task. If we were to accept the relevant axiom, we could vastly improve inversion for highly dependent terms.

The axiom we need is any one of the many variants of a class of axioms called “UIP” (Uniqueness of Identity Proofs). Here is one such axiom:

Hopefully this is quite intuitive. Given our inductive definition of `eq`

, it may even be surprising that we can’t derive this proposition. `eq_refl`

is the only constructor of the equality type, so it stands to reason that any proof of `a = a`

must be convertible to `eq_refl a`

. As this post is not about axioms, I won’t dive into *why* this proposition is unprovable. Suffice to say, it is perfectly innocuous (unless combined with more exotic axioms, such as univalence) and extremely helpful.

We can use Coq’s variant of the UIP axiom by exporting `Coq.Logic.EqDep`

(their version of the axiom is called `eq_rect_eq`

. It looks quite different from `uip_refl`

, but the two are in fact logically equivalent).

We then introduce a variant of our inversion tactic called `dependent inv`

to leverage the extra power of this axiom:

# 5. `gen / to`

Sometimes, one’s hypothesis is just too specific, and needs to be weakened. In particular, this issue often arises as we prepare to induct on a hypothesis. The tactic `gen x := y to P in H`

will replace term `y`

in `H`

with the variable `x`

, where `x`

satisfies the predicate `P`

. The definition of `x`

is then discarded. It therefore “generalizes” `y`

up to the predicate.

I define many more variants of `gen / to`

, for example with a `by`

clause, but the implementations are all obvious, following the general idioms followed by the standard tactics.

# 6. `foreach`

, `forsome`

, and other list-based tactics

It would be nice to have some tactics which operate over lists. Specifically, lists of
hypotheses. For instance, a `foreach`

combinator could apply some tactic to every hypothesis in a list (necessarily succeeding on each), and a `forsome`

tactic could do the same, but stop on the first success (and failing if none succeeded).

This immediate issue we run into is that hypotheses will generally have different types, whereas a Gallina list is necessarily homogenous in type. We could certainly overcome this issue with enough force. For instance, we could use a list of type-value pairs (`list {x & x}`

), but this quickly get’s exhausting. We are forced to manually track types, and we must be careful to keep list elements in a canonical form which our Ltac can parse entirely syntactically. Far more convenient is to embrace Ltac’s dynamic typing, and introduce a notion of heterogeneous lists.

Actually, we don’t need to create very many new definitions. Instead, we re-purpose Gallina’s tuples. Recall that the tuple `(a, b, ..., y, z)`

actually de-sugars into the left-nested pairs `((((a, b), ...), y), z)`

. We therefore interpret an arbitrary-length “flat” tuple as a non-empty heterogeneous list, where `(t, h)`

represent the “cons” of `h`

to `t`

.

A non-pair `x`

is therefore interpreted as the single-element list. Of course, a heterogeneous list of pairs is therefore an ambiguous notion which ought to be avoided.

The only thing missing is a notion an empty heterogenous list. We might consider the unit value for this, but as we have enough ambiguity at the moment, we’ll instead introduce a distinguished type and value for this purpose.

This creates some ambiguity of its own, as there are now two ways to represent singleton lists. Either as `x`

or `(hnil, x)`

.

With our representation decided, we can define some list tactics!

There are a number of interesting aspects of these definitions. First, why do we define both `_foreach`

and `foreach`

? Well, we’d prefer the tactic notation used in the `foreach`

definition, however tactic notations are un-recursive. Therefore, we must first define the recursive tactic `_foreach`

, and then wrap it in the notation defined by `foreach`

.

Second, notice we use `lazymatch`

. This is because there is ambiguity in our cases. Our third match case matches anything. By using `lazymatch`

, we commit to the first two cases if they match, and we only try the third if the first two fail to unify.

Why stop there, let’s create some more list-based tactics!

`in_list`

simply uses `forsome`

to check if an element occurs in a list (up to syntactic equality, not convertibility).

`env`

will create a list of all of the hypotheses in our current environment (i.e. proof state). However, tactics can’t easily “return” values, so we are instead forced into a continuation-passing paradigm in order to use the value built by `env`

. The second argument to `env`

is its continuation, which should be a tactic function expecting a list as an argument. For more information on this strategy, see section 14.3, “Functional Programming in Ltac”, in Chlipala’s *Certified Programming with Dependent Types*.

Now we define `list_minus`

to take the difference of two lists. Again, this is necessarily done in a continuation-passing style.

Putting `env`

and `list_minus`

together, we get `env_delta`

:

Here, we build a list only of the *new* hypotheses introduced into the environment by `tac`

. We do this by grabbing the environment before and after `tac`

is executed, and then calculating their difference.

# 7. `(max) induct(!)`

The standard `induction`

tactic can be surprisingly lacking in a couple of ways. First, it discards information when the arguments to the inductive term are not simple variables.

For instance, consider the proposition `R^* 0 x`

, where `R^*`

is the reflexive-transitive closure of `R`

. We would like to induct over the structure of the proof (a sequence of relation steps). However, if we were to invoke the regular `induction`

tactic, it would replace `0`

with an arbitrary variable, thereby losing that information. We can solve this issue by first replacing the `0`

with a variable ourselves, and creating a separate assumption equating the variable to the value it substitutes before its definition is erased by `induction`

.

To accomplish this task, we are going to need to introduce a number of helpful intermediate tactics.

Our first helper is a refinement of the standard `repeat`

tactic. Just like `repeat`

, it will apply a tactic 0 or more times, stopping at the first failure. `repeat_count`

expands on this functionality by counting the number of successful applications. We will see soon why this might be useful.

Note that this uses the continuation-passing style discussed in our introduction of the list-based tactics.

Knowing that some tactic has been applied `n`

times, we would perhaps like to perform another tactic `n`

times. This is precisely the role of the `do`

tactic. However, the `do`

tactic only accepts Ltac’s internal notion of integers, which is distinct from the Gallina representation of natural numbers as used by the `repeat_count`

tactic. Therefore, we give an alternative definition of `do`

, called `do_g`

which uses Gallina’s naturals.

Finally, we can define our improved induction tactic, called `induct`

.

The first definition, `gen_eq_something`

, simply looks for a non-variable argument in the hypothesis `H`

to generalize up to equality. The second tactic, `intro_try_rew`

, does `intro`

, but simultaneously tries fancier introductions which destructs/rewrites the equality. Finally, `_induct_by`

puts everything together. We `gen_eq_something`

our inductive term as much as possible. Note this will add equality assumptions to our goal. Now, we perform the induction given by `inductStep`

, and on each subgoal, we will introduce each of the equalities we added by `gen_eq_something`

.

If you have ever used `dependent induction`

, `induct`

is trying to do the same thing, sometimes called “inversion-induction”, because it can be seen as simultaneously trying to invert and induct on the hypothesis. If `dependent induction`

does the same thing, why did we just re-create the functionality? Well, `dependent induction`

actually uses the heterogenous equality `JMeq`

, and uses the same UIP axiom we mentioned with `dependent inv`

. Therefore, `induct`

is something of a simpler variation of `dependent induction`

.

One annoying problem with our `induct`

tactic (and `dependent induction`

, for that matter) is that we often end up with inductive hypotheses of the form `x = x -> y`

(or `forall x, x = y -> z`

), which are trivial but annoying to simplify. To solve these, I include a tactic variant `induct!`

, which is more eager to clean up the hypothesis state.

We create a tactic called `ecut_eq`

which will look for equality assumptions in a hypothesis, and attempt to resolve them automatically, potentially specializing the hypothesis with unification variables to do so, as long as no unification variables remain by the end.

The meat of `induct!`

is performed by the `_induct_excl_by`

tactic which uses `env_delta`

and `foreach`

from our list tactics to apply `ecut_eq`

only to the hypotheses introduced during induction.

You may have noticed the odd-looking backtick tactic notation. Clearly this is just an identity combinator, right? What use is it here?

This bactick combinator highlights a very unfortunate corner of Ltac. Contrary to our expectations, the backtick combinator is *not* referentially transparent. That is, the tactic expression `a`

is *not* necessarily semantically equivalent to ``a`

.

Specifically, adding the backtick can affect when a tactic expression is executed. In the tactic expression `a b`

, where `b`

is a tactic expression being passed to the higher-order tactic combinator `a`

, it is unfortunately not always clear *when* `b`

will execute. Almost always, we’d prefer it to only execute at the point it is invoked by `a`

. For whatever reason, this is ensured in the expression `a `b`

, but not in `a b`

. Thus, the bactick can be interpreted as a way to properly delay execution of a tactic expression.

I wish I could explain when adding the backtick is necessary. The truth is, I don’t know. The broader Coq community seems to be resigned to the fact that the execution semantics of Ltac are unclear, and place their hope in some eventual successor such as the mythical “Ltac2” to save us. (Much like Ltac’s execution semantics, it is quite unclear *when* this will come to pass). Until then, we will have to simply live with this defect and insert a backtick now and again when our tactics are misbehaving.

Finally, we add one more feature to our custom induction. Often, we are tasked with manually reverting variables before inducting in order to maximally generalize our inductive hypothesis. Then, we have to re-`intro`

s them. Since there is no harm “over”-generalizing our inductive hypothesis in this way, we can automatically revert and re-`intro`

s all of our variables.

# 8. `tedious`

/`follows`

I’ll end with a tactic which has been extremely useful to me, but I’d also consider to be quite experimental. I am quite a fan of the `easy`

tactic, and the related `now`

tactic, which automatically solves some simple goals. However, I got frustrated that it was unable to solve certain goals, such as those which would follow from one or two `constructor`

applications, or by `eauto`

.

I originally envisioned `tedious`

/`follows`

as slightly more powerful versions of `easy`

/`now`

, but I quickly found myself adding more and more functionality until these had become quite ambitious tactics. Still, I have tried to retain one important characteristic: that it be relatively quick to fail. Here they are in their current form:

As you can see, `tedious`

is a sort of brute force heuristic tactic to solve “straightforward” goals. It uses `auto; easy`

(or `eauto; easy`

if we expect there to be unificaiton variables) as its immediate solver. If the goal is not immediately solvable, it will try some step and recurse. Of course, we would have no reason to expect this to terminate by itself, so we start `tedious`

with some “gas”. Each time it recurses, it loses gas, and when it gets to 0, it gives up. This “gas” is therefore the maximum search depth. By default, tedious starts with 5 gas. We note that increasing the gas will slow it down exponentially, since *each subgoal* `tedious`

encounters will have more gas, meaning it will be more likely to produce more subgoals/hypotheses.

In practice, I have found this tactic to exhibit suprising strength given its usual speed. However, there are certainly some times where the proof state is too complex and `tedious`

will take too long before giving up. Going forward, I’d like to experiment more with ways `tedious`

can inspect the proof state, either the number of subgoals or the number of hypotheses, and reduce its gas accordingly to get more consistent execution times.