Tutorial: Chaining Tactics

Main contributors

• Thomas Lamiaux

Summary

In this tutorial, we explain how to chain tactics together to write more concise code.

Table of content

• 1. Introduction to Chaining
• 2. Chaining Selectively on Subgoals
  • 2.1 Basics
  • 2.2 Ignoring Subgoals when Chaining
  • 2.3 Chaining on a Range of Sugoals
• 3. Chaining is actually backtracking
• 4. Repeating Tactics and Chaining

Prerequisites

Needed:

• No Prerequisites

Not Needed:

• No Prerequisites

Installation:

• Available by default with coq

1. Introduction to Chaining

In Coq, we prove theorems interactively, applying at each step a tactic that transform the goal, and basically corresponds to applying a logical resonning. Yet, in practice, it often happens that some of the primitive tactics are too low-level, and that a higher-level resoning step we would like to do gets decomposed into a sequence of tactics, and hence of interactive steps. This is not very practical, as it hinders understanding when stepping through a proof. It introduces extra interactive steps that we do not care about and can be tedious to run, but also makes the logical structure of the proof harder to recognize and understand. For instance, consider the second subgoal of the proof below. Knowing a : A and b : B, we have to prove (A × B) + (A × C) + (A × D), and hence would like to bring ourselves back to proving A × B. While this corresponds to one simple logical step, it actually gets decomposed into two tactics applied in a row left. left..

To recover the correspondence between the interactive steps and the logical steps we have in mind, we would like to be able to chain tactics, so that in the example left and right are excuted together, one after the other. This is possible using the notation tac1 ; tac2 that is going to execute the tactic tac1, and then tac2 on all the subgoals created by tac1. In our case, it enables us to write left; left. rather than left. left. to get one logical step:

The real strength of chaining tactics appears when different subgoals are created by a tactic, e.g tac1, that requires the same kind of proofs, e.g. tac2. Indeed, in such cases, by chaining tactics tac1 to tac2, we can apply tac2 on all subgoals created by tac1 at once, and do not have to repeat tac2 for each subgoal. In general, this enables to greatly factorise redundant code, while flattening the code that is needing less sub-proofs / bullets. Typically, in the example above, in all the cases created by constructor, we want to apply assumption to conclude the proof. We can hence share the code by writing constructor; assumption rather than dealing with each subgoal independently, and in total to remove 6 subproofs. This greatly simplifies the proof structure, while better reflecting the logical structure.

2 Chaining Selectively on Subgoals

2.1 Basics

Chaining tactics with tac1 ; tac2 applies the tactic tac2 to all the subgoals created by tac1. Yet, it is not always subtle enough as different subgoals can require slightly different kind of reasoning. For instance, consider the example below where we need to apply different functions to each subgoal, namely applying fAC in one case and fBD in the other case:

Yet, we would still like to be able to chain tactics together to factorise code and make it clear. It is possible by using the notation tac; [tac1 | ... | tacn] that takes exactly a tactic per subgoal created by tac, and apply taci on the i-th subgoal This enables us to chain constructor with the apply by writing constructor; [apply fAC | apply fBD] .

This is particularly practical when the subgoals created require a slightly different logical step, before resuming the same proof script. In which case, we can use goal selection to do a differentiated reasoning step before resuming regular chaining. For instance, in the proof above, in both case, we conclude the proof with assumption after applying fAC or fBC. We can hence further chain [apply fAC | apply fBD] with assumption to provide a significantly shorter proof:

2.2 Ignoring Subgoals when Chaining

The construction tac ; [tac1 | ... | tacn] requires a tactic per subgoal. Yet, in some cases, before continuing the common proof, an action is needed for only one subgoal. For instance, consider a ternary version of the example above. Using constructor creates a subgoal where we need to use constructor again, before continuing the same usual proof. We hence, would like to apply constructor once more, but only on the first branch.

This is possible by either:

• 1. leaving the tactic spot empty
• 2. using the idtac tactic that does nothing

This enables to flatten the code removing the number of nested subgoals to prove, while better reflecting the natural structure of the proof:

If wished, it is then possible to further factorise the structure by chaining the apply and assumption as before.

However, as you can see it does not necessarily make the proof clearer. Chaining is great but be careful not to overuse as it can create long and unreadable proof, that no longer reflect logical steps. This construction is also particularly practical to get rid of trivial subgoals that are generated by a tactic. For instance, consider, the proof below where a trivial subgoal is generated by constructor:

Chaining with [assumption |] enables to get rid of the trivial goal, making the proof flatter and letting us focus on the main goal:

Note, that it is also possible with the notation only n: tac that applies a tactic only to the n-th goal.

2.3 Chaining on a Range of Sugoals

It often happens that we have several subgoals, for which we want to apply the same tactic, or do nothing. For instance, in the following context, applying up to prove ∀ a : A, D creates a bunch of goals that all get solved by assumption but one:

Consequently, we would like to apply assumption on the first three subgoals to get rid of the trivial goals before tackling the last one. There are basically three facilities to do that, we can:

• 1. Use the notation only m-n,..., p-q: tac, that applies tac to the ranges of subgoals n-m, ..., and p-q
• 2. Use the .. notation to apply a tactic to all the subgoal until the next one specified like in [tac1 | tac2 .. | tack | tac n ].
• 3. Use the combinator try tac that tries to apply tac to all the subgoals, and it succeeds if no progress is possible

Note that in this very particular case, we could have used first left; left on the last goal then applied assumption everywhere, but it is not a good idea in the facing case, we can hardly predict how difficult will be the last goal.

3 Chaining is actually backtracking

A subtility with chaining tactics is that tac1 ; tac2 does not only chain tactics together, applying tac2 on the subgoals created by tac1, but also does backtracking. If the tactic tac1 makes choice out of several possible ones, e.g. which constructor to apply, and tac2 fails with this choice, then tac1; tac2 will backtrack to tac1, make the next possible choice and try tac2 again. This until a choice makes tac1 ; tac2 succeed, or that all the possible choice for tac1 are exhausted, in which case tac1 ; tac2 fails. This is the case of the tactic constructor that tries to apply the first constructor of an inductive type by default, and will backtrack to try the second constructor and so on if the rest of the proof failed. This enables to write more concise proofs as we can write the same script whatever the constructor we need to apply to keep going and complete the proof. Consider, the following proof where we have to choose between proving the left side A × B or the right side A × C depending on which subgoals we are trying to prove and our hypothesis:

Using constructor, we can replace left and right to get the same proof script for the first and second goal, as:

• for the first goal, it will try left, continue with assumption and solve the goal
• for the second goal, it will try left, continue with assumption and fail, hence backtrack and try right, continue the proof and succded

It can be a bit confusing at first, but once we got used to it, it is very practical to write one proof script to deal with a bunch of barely different subgoals. For instance, we can then further simplify the proof by factorising the left and right of the first and third subgoal. Then by using only 1-2: for the extra constructor, of the first two subgoals, we can get one single proof script to solve all the goals:

Using the backtracking ability of ; to make the right choice out of several possible choices is a simple but very powerful method that enables us to write short but versatile proof scripts.

4. Repeating Tactics

In the previous section, we have explained how to chain tactics linearly so that they execute one after the other, on respectively created subgoals. While this is already very practical, in some cases, we need a bit more freedom like to be able to repeat tactics, or to try a set of tactics. This is what we discuss in this section. Consider the following example of section 1, that has ~25 interactive steps, 6 sub-proofs and is 10 lines long, even though it is a fairly simple proof.

Chaining tactics linearly, we have managed to bring down the proofs to only three interactive steps corresponding to the three logical steps of the proof, and to only two lines.

That is already nice, but the proof is still convoluted. Not only do we have to repeat constructor three times, but we have to think by ourselves when writing the proof that for the third case we only need constructor once and not twice, and hence write only 1-2: constructor. This, even though, the proof is conceptually simple: depending on our case select the appropriate subtype to prove, e.g. A × C, and prove it with constructor; assumption. This is particular annoying as it does not scale very well. Consider, this small variant with only two more types to distribute on. The proof and its overhead then gets much greater, even though it is conceptually as simple as before.

Instead, we would like to be able to apply constructor as much as needed using the backtracking to choose the good subtype to prove; then concludes with constructor; assumption. This is possible with the repeat tac combinator, that given a tactic will apply it repeatedly until it can no longer be applied, or fails if it can not be applied at all. This enables us to refactor the proof by simply writing repeat constructor; assumption, getting a proof that now fully correspond to the logical steps we wanted to take. It further scales much better, as it works exactly the same for the variant with two more types.

However, repeat can be a bit subtle, so be careful not to fall into this two pitfalls:

• 1. repeat will stop if it succeeds, but it may not be what you expect especially when backtracking is involved
  Consider the example above. repeat constructor; assumption manages to solve the subgoals because it tries to apply constructor as much as it can, then to solve the subgoals created by assumption and if it fails backtracks to make other choices. If you stop linking them, then repeat constructor will just apply contructor as much as it can; getting us to prove A × B then A and B in each case, getting us stuck. In other words repeat constructor; assumption is not the same as repeat constructor. all: assumption:

• 2. repeat will apply a tactic as much as possible, it can be more than what you expect
  Consider proving the same goal as before but with A instantiated to nat. You would expect that in both cases, repeat constructor gets you into proving nat × B then nat and B just like explained before. However, running it will actually create only two goals B and B The reason is that constructor applies to nat, and solve the goals using 0 even though you would wanted to solve it using n.

Such issues can be particularly annoying getting you stuck in an unprovable goal, providing the wrong witness or wrongly unifying a metavariable, impact the rest of the proof and getting you stuck latter on. Once should hence be careful when it comes to using tactics combinator like repeat. The repeat combinator also comes as a variant named do n tac that enables to apply tac exactly n times, and if it cannot do it exactly n times fails: