If you’ve programmed in Ltac for a while, and unless you’re using a tactic-heavy “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:

match goal with
| [ H : (* some_pattern *) |- _ ] => (* do something with H *)
end.

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:

Ltac break_exists :=
  repeat match goal with
           | [H : exists _, _ |- _ ] => destruct H
         end.

Ltac break_and :=
  repeat match goal with
           | [H : _ /\ _ |- _ ] => destruct H
         end.

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:

on list induction.

And would more or less translate to:

multimatch goal with
| [ H : context [ list ] |- _ ] => induction H
end.

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:

Ltac on pattern action :=
  multimatch goal with
  | [ H : context [ pattern ] |- _ ] => action H
  end.

I then tried:

Goal forall (l : list bool), False. intros. on list idtac.
(* Ltac call to "on" failed. Error: Illegal tactic application. *)

Unfortunately, Coq built-in tactics are not quite first-class 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:

Ltac idtac' H := idtac H.
Goal forall (l : list bool), False. intros. on list idtac'.
(* l *)

Nice! What next? Well what if we have two lists?

Goal forall (lb : list bool) (ln : list nat), False. intros.
  on (list bool) idtac'. (* lb *)
  on (list nat) idtac'. (* ln *)

In fact, you don’t even need to mention the full type:

Goal forall (lb : list bool) (ln : list nat), False. intros.
  on bool idtac'. (* lb *)
  on nat idtac'. (* ln *)

since lb is the only thing in context whose type mentions bool. Unfortunately, this apparent power will become troublesome:

Goal forall (lb : list bool) (P : lb = lb), False. intros.
  on list idtac'. (* P *)

Indeed, while P’s type looks list-less :upside_down_face: , an astute Coq user would remember it stands for @eq (list bool) lb lb. This highlights two things:

  1. Our on tactic, so far, seems to work its way backwards (trying most recently-introduced 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 that multimatch goal has multimatch reverse goal.

  2. 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?):

Ltac get_head_type T :=
  match T with
  | ?P _ _ _ _ _ _ _ _ _ _ _ _ => constr:(P)
  | ?P _ _ _ _ _ _ _ _ _ _ _   => constr:(P)
  | ?P _ _ _ _ _ _ _ _ _ _     => constr:(P)
  | ?P _ _ _ _ _ _ _ _ _       => constr:(P)
  | ?P _ _ _ _ _ _ _ _         => constr:(P)
  | ?P _ _ _ _ _ _ _           => constr:(P)
  | ?P _ _ _ _ _ _             => constr:(P)
  | ?P _ _ _ _ _               => constr:(P)
  | ?P _ _ _ _                 => constr:(P)
  | ?P _ _ _                   => constr:(P)
  | ?P _ _                     => constr:(P)
  | ?P _                       => constr:(P)
  | ?P                         => constr:(P)
  end.

With this, we can write on_head:

Ltac on_head type tactic :=
  match goal with
  | [ H : ?U |- _ ] =>
    match get_head_type U with
    | type => tactic H
    end
  end.

such that:

Goal forall (lb : list bool) (P : lb = lb), False.
  intros.
  on_head list idtac'. (* lb *)

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:

  Theorem in_split : forall x (l:list A), In x l -> exists l1 l2, l = l1++x::l2.
  Proof.
  induction l; simpl; destruct 1.
  subst a; auto.
  exists [], l; auto.
  destruct (IHl H) as (l1,(l2,H0)).
  exists (a::l1), l2; simpl. apply f_equal. auto.
  Qed.

Rewritten following the same logic, using this style:

  Theorem in_split : forall x (l:list A), In x l -> exists l1 l2, l = l1++x::l2.
  Proof.
    do 2 intro.
    on list induction'; simpl; destruct 1.
    subst_all.
    exists []. on list exists'. auto.
    find_specialize.
    do 2 on @ex destruct'.
    eexists (_ :: _). eexists. simpl. apply f_equal. eauto.
  Qed.

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 full-glory 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:

  Theorem in_dec :
    (forall x y:A, {x = y} + {x <> y}) ->
    forall (a:A) (l:list A), {In a l} + {~ In a l}.
  Proof.
    do 3 intro.
    on list induction'.
    { right; apply in_nil. }
    match goal with
    | [ |- context [In ?a (?b :: _)] ] =>
      on sumbool ltac:(fun H => destruct (H b a))
    end.
    simpl; auto.
    on sumbool destruct'; simpl; auto.
    right; unfold not; intros [? | ?]; auto.
  Defined.

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! :+1: :-1: