Tactics in Coq

Many of the tactics that Coq offers correspond to expression transformations. This post is about them: I will introduce each of them and present their behavior, before classifying them.

I won't yet discuss how these tactics can be controlled in to much detail (e.g. which mechanisms exist to pick the subterm to which they are applied, or whether or not they take the "Arguments" mechanism into account — don't worry if you don't know what this means at this point); this is reserved for the next post.

1. Adapting the classification

2. Tactics for expression transformation in Coq

Remember what I mentioned back in the introduction: Coq tactics are either rewriting ones, deductive ones or bookkeeping ones, and we are only concerned with the first category here.

If you think that I forgot some tactic is missing, make sure that all it does is replacing an expression with something equivalent. For instance, left is a deductive tactic (it clearly doesn't preserve equivalence), so is reflexivity (this one even destroys the expression!), and clear is a bookkeeping one.

2.1. simpl

simpl (man) simplifies stuff. It doesn't fully reduce terms, as it try to keep them human-readable. The heuristics it uses to this end are the following:

• A constant (in this context, a term defined somewhere else, such as in the hypotheses or through an in-scope Definition) is only unfolded if it allows reducing a match or a fixpoint.
• Some smarts about (co)fixpoints — manage recursivity by unfolding the definition once and replace recursive calls with the constant name (the alternative would be to build a (co)fix object, which is not as pleasant on the eye).

It can be applied in the goal as well as in hypotheses. Furthermore, it is possible to apply this tactic to some targeted subterm(s) only (e.g. only simplify subterms matching pattern x).

2.2. cbn

cbn (man) is closely related to simpl. In fact, "cbn was intended to be a more principled, faster and more predictable replacement for simpl" (emphasis added). It is based on a Krivine abstract machine.

The manual stresses that cbn may unfold constants that are not used in recursive calls, unlike simpl (but it doesn't detail under which conditions this happens). I'd also like to add that it handles non-simplifiable deeply nested expressions better, e.g.:

cbn can be passed flags to restrict the set of reductions steps it applies, and it can also specify to which subterms it should be applied (but not as well as cbn can, e.g. no patterns).

So, are there situations where simpl is better than cbn (besides for targeting subterms, which I don't think would be too hard to add anyways)? I'm not quite sure, but apparently if you don't know what you are doing, you should start by giving simpl a shot. Maybe something to do with overhead. TODO check how simpl is implemented

2.3. cbv/compute

cbv (man) is a total reduction tactic! Well, sort of — a bit like cbn, the set of reductions it is allowed to apply can be restricted, making it partial in those cases. In fact, cbv, stands for "call-by-value", just like the evaluation strategy! This is no coincidence.

cbv can also be applied to some subterm(s) of the goal and/or hypotheses (but not by pattern).

compute is basically a synonym of cbv. Just stick to cbv.

2.4. vm_compute/native_compute

vm_compute (man) and native_compute (man) are a pair of closely related tactics. Think of them as faster but less controllable versions of cbv (as they can't be passed a reduction types blacklist). vm_compute is based on a virtual machine, whereas native_compute generates and executes OCaml code.

native_compute is the faster one (the manual indicates that is usually 2 to 5 times faster than vm_compute). However, it comes with a large overhead. As a rule of thumb, if your term is small and reduces to something small, and if it takes more than five seconds to evaluate through vm_compute, then native_compute is probably faster. The intuition is that small terms are easier to convert to and from OCaml.

native_compute is an optional feature of Coq; if it is not active, the tactic prints a warning and delegates to vm_compute.

These tactics leave a mark in the proof term. This gives some interesting guarantees about the equivalence of the performance of the reduction between the application of the tactic and the validation of the proof at Qed time.

2.5. lazy

lazy (man) is a total evaluation transformation which is functionally identical to cbv, but with laziness. That is, it doesn't evaluate arguments when their values are not required — just like in Haskell! Again, more details in this post.

lazy is the better tool if there is a lot of dead code, but the situation reverts when there is little of it cbv. At least this is what the manual says, but can the difference be noticed in practice? TODO try generating an example where cbv is noticeably faster than lazy.

Note that kernel conversions (those which are done are Qed time except when native/vm_compute is used) follow a lazy strategy.

2.5. red

red (man) unfolds the constant at the head of a term (goal and/or hypotheses) or under a forall binder, and normalizes the result in a way I don't fully understand (and which does not seem to fully correspond to what the manual says):

Note that I mentioned forall binders only: if you were to replace it with an exists, then the second call would already fail.

2.6. unfold

unfold (man) unfolds definitions in the whole term or subterms of the goal and/or hypotheses, and normalizes the result as much as it can without unfolding other definitions (it can unfold other occurrences of itself, though).

2.7. fold

Unlike what its name suggests, fold (man) is not the opposite of unfold.

It is a somewhat barbaric tactic which takes expressions as arguments. It applies red to all its arguments, and replaces occurrences of the resulting expressions with the corresponding argument. At least, that is what the manual states, but I found this to be a bit misleading, as it doesn't look for subterms syntactically equal to the resulting expressions, but for some equivalent ones according to a more generous criterion.

The reason why fold doesn't (always) undo unfold is that unfold normalizes the term, and may in particular (partially) apply the function. E.g.:

The manual gives another, sneakier example:

fold also handles more complex arguments:

2.10. change

change (man) replaces a term or a subterm with an arbitrary term, so long as Coq can attest that both terms are equivalent (by doing something akin to cbv).

To replace the whole term, simply skip the <x> with part.

change_no_check (man) is a variant of change which skips the convertibility test. As it can replace any term with anything, including something not equivalent, it can't really be considered an expression transforming tactic. However, the kernel still typechecks the whole proof term in the end, so this does not allow to validate misformed proofs. It avoids duplicated computations, and it can be a sanity saver performance-wise.

2.11. pattern

pattern (man) generalizes a term over some expression.

pattern can be applied to a list of arguments:

It can also be applied at specified locations:

In fact, this tactic corresponds to β-expansion (undoing function application).

2.13. hnf

hnf (man) is a normalization tactic, like simpl and cbn, but with the difference that it does not recurse into subterms, e.g.:

hnf stands for "head normal formal" but in reality the tactic doesn't quite go that far: it stops at weak head normal form, not simplifying the inside of lambda abstractions (more information about normal forms here, written in the context of Haskell but it applies nonetheless).

2.8. rewrite

rewrite (man) can perform arbitrary replacements of (sub)terms, given a proof that the replacement is equivalent to the replacee.

erewrite (man) is a variant which plays nice with evars. TODO is there ever really a reason to favor rewrite over erewrite? It can also take proofs of the form x -> y = z, in which case it performs the replacement but adds x as a goal.

rewrites are oriented: do you want to replace what is on the left of the = sign or the opposite? Here is how the opposite direction is specified.

Instead of passing a proof of the validity of the replacement explicitly, it is possible to specify a tactic which automatically solves the corresponding goal:

There is also the replace (man) tactic, which takes a candidate replacee in and checks the hypotheses for a proof of equivalence. If doesn't find any, it still performs the replacement in the targeted (sub)term, but it adds a goal justifying it.

TODO: setoid_rewrite

2.9. subst

subst (man) is both a bookkeeping and a rewriting tactic: it looks for all hypotheses of the form x = y where either x or y corresponds to an identifier, and it replaces this identifier with the associated expressions in all hypotheses and in the goal. It also removes the x = y hypothesis.

It is an automated but limited relative of the rewrite tactic which also does some cleanup.

subst handles all hypotheses from top to bottom and it gives priority to the left side of equalities (if both x and y are identifiers, it replaces x with y and not the other way around).

It can also be made to look for some specific identifiers only.

3. Filling the classification

This is how the Coq tactics fit in the classification. Not very enlightening, is it? Many tactics end up in the same category and there's not much to distinguish them. Also, many tactics land in an akward position between two areas. That is because their behavior depends on the arguments and flags they receive.

In the next episode…

We will refine our classification by including information about how the tactics can be controlled.

• <
• >