Control mechanisms in Coq

We have seen which tactics can be used to transform expressions in Coq, but I didn't go into as much detail as I could have about how these tactics can be controlled. For instance, many tactics offer ways to select to which subterm(s) they can be applied, and these control mechanisms are usually shared between different tactics.

This post will introduce all these mechanisms. The classification will then be enriched with related information.

1. How transformations are applied

Up to this point I mostly focused on what sort of transformation the tactics do, but not on how they actually reach their results. In other words, I stuck to the functional aspects of these transformations. In this section, we are going to see how tactics sorted in the same category may differ.

1.1. Laziness and eagerness

I already mentioned laziness and eagerness in the first classification I gave as well as in my introductory post about evaluation strategies. Laziness and eagerness decide when an argument is evaluated: when it is first encountered or only when we are sure that its value is required. In some contexts, the latter is much more efficient (albeit it comes with a very small overhead).

These properties are chiefly associated to partial or total evaluation transformations: after all, they are an important characteristic of strategies for picking which reduction steps to choose between the ones available at some point.

Actually, what we showed in the above example was call-by-name, a form of lazy evaluation where the value of inputs can be computed several times, as was the case for (1 + 2 + 3). For functions with complex inputs, this can lead to important performance issues! Therefore, actual lazy strategies are usually based on call-by-need, where the value of each input is computed once if and only if it is actually required. This can be done a bit like this:

Most strategies in Coq are eager. In fact, the only lazy tactic is, well, lazy — but so is the reduction strategy employed by the kernel (not a tactic!).

1.2. Acceleration

Most Coq strategies run "inside of Coq". That is, they directly manipulate Coq terms without stepping through complex intermediate representations.

The two notable exceptions are vm_compute and native_compute. The former works by converting terms to a form which is then executed by a virtual machine written in C (of course, the result also has to be converted back to Coq). The latter converts the term to OCaml code which is then compiled and run.

These tactics are very efficient at computing but come with some overhead (for the conversion between the different forms, and compilation in the case of native_compute). native_compute is the faster of the two, but it also comes with a larger overhead.

1.3. Impact on the proof term

Calls to Coq tactics build a proof term. When Qed is then called, the kernel verifies that this term has the type corresponding to the property being proved, as per Curry-Howard. For instance, a successful call to reflexivity replaces the hole in the proof term which corresponds to the current goal with eq_refl (with the appropriate implicit parameters). But what about expression transformations?

Let's first turn our attention to non evaluation-based tactics. To a first approximation, evaluation based tactics are useless: they take an object to something equivalent to it. Still, they guide the reduction process. The way Coq keeps track of their effect is by inserting an explicit conversion in the proof term. Concretely:

However, I mentioned that vm_compute and native_compute are more efficient than e.g. cbv. This is good, however you should remember that the conversion that these tactics perform are not only performed once, but twice: once during the call to the tactic, and then again during the typechecking of the generated proof term (at Qed time).

Now, if the accelerated tactics were to trigger to non-accelerated conversions in the proof term, then calls to Qed would end up taking a problematic amount of time. Consequently, the kernel also handles accelerated conversions:

native_compute leaves a similar mark, denoted as <<:.

This comes at a cost which is paid in trust: the Coq kernel now contains a compiler and a virtual machine. So much for minimality. The efficiency of these tactics makes the tradeoff acceptable, and it is always possible to use the very restrictive program coqchk to check proofs while avoiding these facilities.

The information left in the proof term is rather limited. Consequently, it may be that you were careful to prove something in a smart way which keeps off performance traps, only for the proof term checker to fall head first into them as not enough information was remembered. Luckily, this should not happen with e.g. your carefully picked cbv flags, due to the way the default conversion used by the kernel works. Read the code below to get a sense of how the reduction process work. In it, we do one proof and then another one which is very close to the first one, yet with a very different performance profile.

I am not 100% certain about the finer details, but my interpretation of what happens is as follows:

• 1. Coq needs to check that the term sc_5_0 (resp. s_0) is equivalent to slow = 0 (resp. slow_comp 5 = 0). The form of the right term is a constructor application (of "=", which is notated in an infix manner). The head of the right terms can't be simplified, but that of the left ones can. Let's do just that.
• 2. We are now comparing slow_comp 5 = 0 (resp. slow = 0) to slow = 0 (resp. slow_comp 5 = 0). The heads are equal, so Coq can focus on the subterms:
  • 2.1. Let's compare slow_comp 5 (resp. slow) to slow (resp. slow_comp 5). Some of those are applications, but function applications this time, which makes the situation quite different: this is not the head of a value. Maybe if we unfolded and simplified slow_comp 5, we would get precisely slow. On the other hand, maybe slow is defined as slow_comp 5. Or maybe neither. It turns out that the second possibility is true here. But how does Coq know that? Well it doesn't, so it defaults to giving priority to applying reductions in the right term, which is at the root of the differences between examples A and B:
    • 2.1.A. The right term (slow) is reduced to slow_comp 5. This is trivially equal to the left term.
    • 2.1.B. The right term (slow_comp 5) keeps getting reduced but never equals the left one (slow). The left term also gets fully reduced, and only once this is done does Coq accept the conversion.
  • 2.2. 0 is syntactically equal to 0, this one is trivial.

Also note how such conversions applied to very large terms can lead to huge proof terms — a very large term and another large term equal to the first one after some simplification both appear in the proof; if there are 50 such passes, then there are 51 large terms (TODO sharing probably mitigates this issue — is it really a problem in practice?).

Not all tactics use conversions to leave a mark in the proof term. For instance, rewrite uses the eq_ind_r, which is a function which takes x to y given a proof of x = y.

In summary, the tactics behave like this:

• traceless tactics: change.
• conversion-based:
  • accelerated: vm_compute, native_compute.
  • non-accelerated: fold, red, cbv, simpl, cbn, hnf, lazy, pattern, unfold.
• eq_ind_r based: rewrite, subst.

However, this is only true when the tactics are applied to a goal! When targeting hypotheses, almost all expression transformation tactics are traceless! In fact, the only exceptions to this are rewrite and subst (I didn't check every single other tactic but I think they are it). This has some nasty consequences:

With rewrite, the changes to hypotheses are dealt with by introducing let bindings overriding the value of the argument that is the Curry-Howard analog to the hypothesis. I don't know why the same isn't done for e.g. conversions — I don't see why it wouldn't work and it would make the performance of Coq much more predictable.

Also, it's perfectly fine for change never to leave a trace in the term, as this tactic searches a proof for the replacement with performance similar to what the kernel does at Qed time (TODO exactly the same? what about laziness?).

2. Where transformations are applied

Most tactics offer a way to target subterms, hypotheses, … In this section, I catalogue the targeting methods available to tactics.

2.1. Occurrences

If you were to design a tactic language for Coq, how would you enable the user to refer to subterms? Asking for an explicit path in the syntax tree works, sure, but this is really not pleasant to deal with, and it gets worse the deeper the targeted subterm is. Coq's answer is based on the notion of occurrences: give a pattern and Coq will associate an identifier to each matching subterm, or apply your tactic to all matches.

Reference occurrences

Some Coq tactics let you refer to occurrences of some definitions:

In this example, the - in the subterm to the left of the = sign was also simplified, but the one in the right subterm was not. This is because vm_compute identified all occurrences of +, and fully evaluated them (including their subterms).

Reference occurrences also understand notations:

Pattern occurrences

Pattern occurrences work by identifying subterms matching a given pattern in a term:

Or even:

And (more complex):

As you can see, unlike reference occurrences, pattern occurrences corresponding to a function only simplify these functions themselves and not the full application. In particular, they leave the subterms being passed to these functions unchanged:

Also note that the universal pattern matches every subterm (and therefore leads to a result no different to a simple call to vm_compute).

The language for expressing patterns include the joker symbol _. This is not sufficient to express all sort of patterns. For instance, you can't express the pattern corresponding to f ?a ?a.

Occurrence numbers

Occurrence numbers are a targeting mechanism where subterms are designated by a number which depends on the position of a match of some query in a term. For instance:

The occurrence number can be computed by considering a depth first search of the syntax tree of the term:

< 1/6 >

This is a representation of the syntactic tree of the expression on the left of the = sign in the previous example.

---

There is already an occurrence at the root!

---

Descending into the left subtree first. We immediately find a new occurrence.

---

This is a depth-first descent, so we keep going down.

---

We reach the bottom, we need to go back up. There were no other sibling trees to go down in at this stage …

---

… But there was one here!

---

We deal with the right subtree similarly. And done!

---

Multiple occurrences in the same term

It is possible to indicate a group of occurrences at once. There are two ways of doing this. First, the positive one:

And then the negative one:

Occurrences in different terms

Up to this point, we only saw occurrences applied to the goal, but they can also target hypotheses:

Multiple hypotheses can be targeted at once:

All hypotheses:

Some hypotheses and goal:

Simple occurrences

For some reason, there are tactics which accept occurrences but not occurrence numbers ("simple occurrences" — that is, you can pass a pattern but you can't focus on occurrence x or y). This is not imposed at the syntactic level: that is, you won't get a parsing error when trying to pass at x arguments to such tactics, but you will get an error message telling you that this tactic doesn't take at clauses.

2.2. Other methods for bunched applications

Besides mundane occurrences, there are some mechanisms for bunched applications that are exclusive to some tactics.

unfold

In fact, unfold takes a list of reference occurrences as arguments, so it also works with notations such as "+".

fold

fold works a bit similarly, but without commas between arguments (life wouldn't be much fun if everything was predictable).

pattern

pattern takes commas:

TODO rewrite/replace

rewrite takes a comma separated list of the form (-> | <-)? (<n>)? (? | !)? <rewrite>. These are called oriented rewriters. Each of them are applied in the order of the list. If one of them fails, then so does the whole tactic. The first component of an oriented rewriter is the orientation — simple enough. Then comes a natural number indicating how many rewrites to perform. The meaning of this number depends on the following component. If it is ? means that the number is an upper bound on the number of rewrites to perform, where 0 is not considered a failure, whereas ! means that it is precisely the number of rewrites to be performed. In the absence of a number, ? simply means try to rewrite and ! means rewrite and fail if you can't (! is the default, no matter if a number is given or not). Finally, Note that only the last of these items is required.

TODO finish. Can't get the natural number to behave like I expect it to. Present rewrite *, impact of occurrences on success

subst

subst doesn't take commas:

2.3. Opacity

There are some situations where you know that unfolding some definition will generally lead to trouble in a context. The thing is, Coq tactics can be complex beasts which do a lot of things implicitly. It would take a lot of care to pass the appropriate flags to ensure that no tactic starts unfolding said defintion. Wouldn't it be nicer to just mark the term as not to be unfolded in the current context? This is precisely what opacity is about.

The Opaque command marks some definitions as not to be unfolded by tactics:

The opposite of Opaque is Transparent.

Some tactics do not respect opacity:

Another context which features opacity is calls to Qed. Closing a proof with Qed makes the proof terminately opaque (it can't be salvaged through Transparent). For most proofs, that is perfectly fine, but in the cases where it's not the proof should be closed with Defined, which keeps everything transparent.

2.4. Strategy

The Strategy command (man) is

2.5. Arguments

The Arguments command (man) comes in handy for controlling when functions are evaluated by tactics. For instance, I often had issues with functions which blow up when Coq tries to evaluate them when e.g. their second argument is not concrete. So, we would like to evaluate these functions when their second argument is concrete but not otherwise. A perfect usecase for Arguments!

Arguments is also used in other contexts (its most common usecase is making some arguments of a function implicit). Here, we focus only on its uses related to the control of the unfolding process. This mechanism is only taken into account by simpl and cbn, however.

Arguments can block the unfolding of a constant, like a worse version of Opaque.

It can also tell when to force the unfolding of a function definition:

In my experience, the most interesting feature of Arguments is its ability to block the evaluation.

!<arg> means "before evaluating the function, make sure that argument <arg> can be evaluated down to a concrete value". It is very useful for avoiding explosions.

Finally, Arguments can be used to block evaluations which lead to new match construct in the head of the simplified subterm.

In this example, it helps us get the exact same behavior as in the previous one which made use of ! instead.

3. Until when transformations are applied — and in which order

3.1. A word on reduction steps

3.2. Restricting the reduction types

3.3. Normal forms

Normal form (NF)

Head normal form (HNF)

Weak head normal form (WHNF)

4. Recap

In the next episode…

We will make a case about the need for the availability of single reduction steps — and propose a solution.

• <
• >