Thomas Letan

PhD Student in Computer Science

Coq Ltac 101

I’ve been using Coq for more than two years now. So far, it has been a very interesting journey. The least I can say is that I’ve learnt a lot, from dependent types to generalized rewriting. However, until very recently there has been one thing I’ve been avoiding as much as possible: Ltac, the “tactic language” of Coq. You can write your own tactics to be used later in your proof scripts. The main reason behind my reluctance was how poorly it has been described to me by several developers. Also, I find the reference manual quite unhelpful.

Fortunately, you don’t need to know how to write a tactic to prove most of your lemmas. SpecCert1 has some custom intros-like tactics, but they are nothing more than aliases.

Sometimes, even if you could do without Ltac, the automation power it grants you is just too appealing. For the past few months, I have been working on a new project in Coq that introduces a relatively verbose proof framework. For toy examples, the “do it yourself” way was enough, but very quickly the proof goals become insane. I needed Ltac.

Turns out, it is not that hard.

This article is a quick overview of my findings. If you never wrote a tactic in Coq and are curious about the subject, it might be a good starting point.

Tactics Aliases

The first thing you will probably want to do with Ltac is define aliases for recurring (sequences of) tactics.

For instance, in SpecCert, I had a lot of similar lemmas to prove. They have exactly the same “shape”: forall h1 ev h2, P h -> R h1 ev h2 -> P h2. h1, h2, ev were records I had to destruct and P and R were a composition of sub predicates. As a consequence, most of my proofs started with something like intros [x1 [y1 z1]] [a b] [x2 [y2 z2]] [HP1 [HP2 [HP3 HP4]]] [R1|R2]. Nothing copy/past cannot solve at first, of course, but as soon as the definitions change, you have to change every single intros and it is quite boring, to say the least.

The solution is simple: define a new tactic to use in place of your “raw” intros:

Ltac my_intros_1 := intros [x1 [y1 z1]] [a b] [x2 [y2 z2]] [HP1 [HP2 [HP3 HP4]]] [R1|R2].

It is as simple as that. If your alias uses two tactics instead of one (eg, you always use cbn after you intro), you have to use ; 2:

Ltac my_intros_2 := intros [x1 [y1 z1]] [a b] [x2 [y2 z2]] [HP1 [HP2 [HP3 HP4]]] [R1|R2].

That being said, there is an issue with these definitions. What if you want to use them twice? The name x1 would already be used and the tactic would fail. To solve this issue, Ltac provided fresh, a keyword to get an unused name.

Ltac and_intro :=
let Hl := fresh "Hl" in
let Hr := fresh "Hr" in
intros [Hl Hr].

It is straightforward to use:

Goal (forall P Q, P /\ Q -> P).
  intros P Q.
  and_intro.
  exact Hl.
Qed.

Here, fresh “H” means Coq will try to use H as a name. If it already exists, it will try H0, then H1 etc. In your Ltac definition, you can just use H.

Tactics can be recursive too! For instance, we can write and_intros pretty easily:

Ltac and_intros :=
  let Hl := fresh "Hl" in
  let Hr := fresh "Hr" in
  intros [Hl Hr]; try and_intros.

So, for instance, if we consider the following (incomplete) proof script:

Goal (forall P Q, Q /\ P -> P /\ Q -> P).
  intros P Q.
  and_intros.

Here is what we get after and_intros:

1 subgoal, subgoal 1 (ID 15)

  P, Q : Prop
  Hl : Q
  Hr, Hl0 : P
  Hr0 : Q
  ============================
  P

Finally, tactics can take a set of arguments:

Ltac destruct_and H :=
  let Hl := fresh "Hl" in
  let Hr := fresh "Hr" in
  destruct H as [Hl Hr].

With that, you can already write some very useful “aliases.” It can save you quite some time when refactoring your definitions, but Ltac is capable of much more.

Printing Messages

One thing that can be useful while writing/debugging a tactic is the ability to print a message. You have to strategies available in Ltac as far as I know: idtac and fail, where idtac does not stop the proof script on an error whereas fail does.

It Is Just Pattern Matching, Really

If you need to remember one thing from this blogpost, it is probably this: Ltac is mostly about pattern matching. That is, you will try to find in your goal and hypotheses relevant terms and sub terms you can work with.

You can pattern match a value as you would do in Gallina, but in Ltac, the pattern match is also capable of more. The first case scenario is when you have a hypothesis name and you want to check its type:

Ltac and_or_destruct H :=
let Hl := fresh "Hl" in
let Hr := fresh "Hr" in
match type of H with
| _ /\ _
  => destruct H as [Hl Hr]
| _ \/ _
  => destruct H as [Hl|Hr]
end.

For the following incomplete proof script:

Goal (forall P Q, P /\ Q -> Q \/ P -> True).
  intros P Q H1 H2.
  and_or_destruct H1.
  and_or_destruct H2.

We get two sub goals:

2 subgoals, subgoal 1 (ID 20)

  P, Q : Prop
  Hl : P
  Hr, Hl0 : Q
  ============================
  True

subgoal 2 (ID 21) is:
 True

We are not limited to constructors with the type of keyword, We can also pattern match using our own definitions. For instance:

Ltac and_my_predicate_simpl H :=
  let H_ := fresh "H" in
  match type of H x with
  | my_predicate _ /\ _
    => destruct H as [Hmy_pred H_]; clear H_
  | _ /\ my_predicate x
    => destruct H as [H_ Hmy_pred]; clear H_
  end.

Last but not least, it is possible to introspect the current goal of your proof development:

Ltac rewrite_something :=
  match goal with
  | [ H:  ?x = _ |- context[?x] ]
    => rewrite H
  end.

So once again, as an example, the following proof script:

Goal (forall (x:  nat)
             (H:  x = 2),
       x + 2 = 4).
  intros x Heq.
  rewrite_something.

Gives us the following goal to prove:

1 subgoal, subgoal 1 (ID 6)

  x : nat
  Heq : x = 2
  ============================
  2 + 2 = 4

The rewrite_something tactic will search an equality relation to use to modify your goal. How does it work?

  1. match goal with tells Coq we want to pattern match on the whole proof state, not only a known named hypothesis
  2. [ H: ?x = _ |- _ ] is a pattern to tell coq we are looking for a hypothesis _ = _
  3. ?x is a way to bind the left operand of = to the name x
  4. The right side of |- is dedicated to the current goal
  5. context[?x] is a way to tell Coq we don’t really want to pattern-match the goal as a whole, but rather we are looking for a subterm of the form ?x
  6. rewrite H will be used in case Coq is able to satisfy the constrains specified by the pattern, with H being the hypothesis selected by Coq3

Finally, there is one last thing you really need to know before writing a tactic: the difference between `match` and `lazymatch`. Fortunately, it is pretty simple. One the one hand, with `match`, if one pattern matches, but the branch body fails, Coq will backtrack and try the next branch. On the other hand, `lazymatch` will stop on error.

So, for instance, the two following tactics will print two different messages:

  Ltac match_failure :=
  match goal with
  | [ |- _ ]
    => fail "fail in first branch"
  | _
    => fail "fail in second branch"
  end.

Ltac match_failure' :=
  lazymatch goal with
  | [ |- _ ]
    => fail "fail in first branch"
  | _
    => fail "fail in second branch"
  end.

We can try that quite easily by starting a dumb goal (eg. Goal (True).) and call our tactic. For match_failure, we get:

Ltac call to "match_failure" failed.
Error: Tactic failure: fail in second branch.

On the other hand, for lazymatch_failure, we get:

Ltac call to "match_failure'" failed.
Error: Tactic failure: fail in first branch.

Conclusion

I were able to tackle my automation needs with these Ltac features. As always with Coq, there is more to learn. For instance, I saw that there is a third kind of pattern match (multimatch) I know nothing about.

Footnotes


  1. Yes, SpecCert is on the Nest now. :)

  2. You would do the same in a proof script if you wanted your cbn to be executed right after intros.

  3. I would have preferred ?H over H to be consistent with the rest of the syntax.

Related Threads