Nameless tactic programming using HaysTac
If you’ve programmed in Ltac for a while, and unless you’re using a tacticheavy “Adam Chlipala”style of proving, you probably encountered a time where you used a name generated by Coq in your proof script in the past, then changed something, only to see your script failing, because the generated name changed.
This issue is well known to most people in the community (see this blog post, or this ongoing effort to warn users).
For people who still prefer stepping through their script to
automation, the usual solution provided is to use match goal
in your
proof script, to capture just the variables you want based on all or
part of their type:
This makes the tactic more robust, with the assumption that the name it has at this point is more likely to change than the pattern you wrote. However, this is quite tedious to write, so most people will start packaging up recurring patterns. For instance, students at University of Washington have been building the StructTactics library, which defines tactics like:
It left me wondering, was there a way to abstract a little more over this, given the current state of Coq?
Enter the on
tactic
What I would like is a succinct way of identifying a hypothesis by all or part of its type, and to indicate an action to be performed with the targetted hypothesis. I imagined it would look something like:
And would more or less translate to:
I started writing the tactic as such, and entered a small rabbit hole that is worth describing. Let’s be as naïve as I was:
I then tried:
Unfortunately, Coq builtin tactics are not quite firstclass Ltac
functions. One could use on list ltac:(fun x => idtac x).
, but this
is too verbose, and a little alias gets us what we want:
Nice! What next? Well what if we have two lists?
In fact, you don’t even need to mention the full type:
since lb
is the only thing in context whose type mentions bool
.
Unfortunately, this apparent power will become troublesome:
Indeed, while P
’s type looks list
less , an
astute Coq user would remember it stands for @eq (list bool) lb lb
.
This highlights two things:

Our
on
tactic, so far, seems to work its way backwards (trying most recentlyintroduced hypotheses first). This can be what we want most of the times, but there might be times where we’d want the opposite, in the same way thatmultimatch goal
hasmultimatch reverse goal
. 
Most of the time, accessing some data will be hard when we know something about it, since the property’s polymorphic type will be instantiated with the type of the data, thus “shadowing” the data in this traversal.
To solve (1), we can just introduce an operator rev_on
that works
like on
but using said multimatch reverse goal
feature. To solve
(2), I propose a second operator on_head
(and its associate
rev_on_head
), that try to match the given target not anywhere
within the type, but as the head constants of the type.
Unfortunately, I don’t know of a better way to access this head than
an ugly cascade (maybe recent Coq changes made this easier?):
With this, we can write on_head
:
such that:
The on
tactic in practice
After all this is packaged, and aliases are created for most standard tactics, how does a proof in this style look in practice?
Here are two comparative examples, using code from the standard library (not necessarily beautiful to start with).
As it appears in the standard library:
Rewritten following the same logic, using this style:
Using a more positional style, the proof starts by introducing 2
variables, and performing induction on the list
one. subst_all
is
a tactic that performs subst
as much as possible.
Now, in the first case, one wants to instantiate witness l1
as []
,
and witness l2
as the only list around. I’m not quite sure why I
get away with on list exists'
rather than on_head list exists'
though, since IHl
mentions list
in its fullglory type.
The next thing the named proof does is specialize some hypothesis to
destruct its conclusion. To do so, I use another tactic
find_specialize
, not discussed here, which finds a hypothesis that
it can specialize using what’s in context. More specific variants of
find_specialize
can be built if one wants to restrict the type of
the hypothesis to be specialized. Destructing the exists
is
achieved by on @ex destruct'
, which is done twice.
Here comes a challenge for this technique! We want to provide two
lists, (a :: l1)
and l2
. There are two approaches at this point:
either we can let the system figure out what they are, or we’re going
to need to write a match goal
to carefully pick a
, l1
and l2
without naming them. In this proof, we are lucky: the conclusion will
almost entirely determine the witnesses. We only need to nudge Coq
into knowing the first witness will have a cons
cell. eexists (_ ::
_).
lets us proceed, while allowing the necessary reduction that will
allow f_equal
to guess the witnesses by unification!
Let’s now look at an example where we don’t get so lucky:
After the curly braced part where we deal with the base case, we find
ourselves in a pickle: we’d like to do a case analysis given the
hypothesis X : forall x y : A, {x = y} + {x <> y}
, passing in a
and a0
. The context is still simple enough that we could succeed
with on_head A
and rev_on_head A
to pick up each variable, but
this feels a little ugly, and what if this wasn’t the case? In this
case, I’d rather resort to writing a match goal
that relates the
variables I am trying to get a hold on to their role in the
conclusion, as this seems like the most robust thing to do.
HaysTac: a collection of tactics to program in this style
Thinking this might be useful to some people, as a toy first, and maybe as an exercise in changing your own style of proofs, I put all these tactics online and called their collection HaysTac.
I have beefed up the on
tactic some more, as you can see in this
example
for instance. It accepts any tuple of things to find in the target,
and only matches a target that mentions them all. This allows
discriminating between two very similar types by only listing parts
where they differ.
I also added an on'
version of on
that prints out which hypothesis
was chosen as the candidate. It’s sometimes useful when debugging
whether your targetting or your action is wrong.
A bunch of aliases are provided that behave like your usual tactics but can be passed as arguments when not fully applied.
I do not recommend using HaysTac in any critical project, but I’d love some people to try their hand at it, and send me feedback!