A proposal for native atomic reductions in Coq

When reasoning about complex objects in Coq, the lack of flexibility of the the available tactics is often an issue. In fact, if you take a look at the following papers (TODO links), you will see that it is not uncommon for people to define their own embeddings and deduction rules, where it could be argued that

In this section, we propose a relatively simple solution to this issue: create a tactic allowing to apply individual reduction steps at arbitrary location in terms.

1. Atomic reduction steps in Coq

The following reduction steps are a generating set for evaluation in Coq (more information here):

function application (β-reduction)
definition unfolding (δ-reduction)
let-in reduction (ζ-reduction)
fixpoint unfolding (fix-reduction)
cofixpoint unfolding (cofix-reduction)
pattern matching application (match-reduction)

In addition to these, there is another reduction step which is functionally redundant with the above but can have an impact on performance:

elimination of constant pattern matching

Illustrated hereafter:

match <x> with | <a> => <y> | <b> => <y> | _ => <y> end.

If there is no efficient way of normalizing x to WHNF, then the fact that all branches of the pattern matching can be exploited to reduce the expression to the value y without needing to consider it.

2. The interface

2.1. The tactics

The atomic extension defines tactics of the form atomic <command> at <pos>. I will first focus on the command part before turning towards how the position are given.

Explicit atomic reductions

The atomic extension defines a set of tactics, each of them corresponding to one of the aforementioned basic reduction steps:

atomic fun: function application
atomic def: definition unfolding
atomic let: let-in reduction
atomic fix: fixpoint unfolding
atomic cofix: cofixpoint unfolding
atomic match: pattern matching application

These tactics fail when they can't be applied at the given position.

Automatic atomic reductions

In addition to these, it also defines the atomic auto tactic: it turns out that it is impossible for a position to be compatible with two different kinds of steps, and this is the how we exploit that fact.

So, when should you use explicit atomic reductions then? It may be better for readability as well as for didactic purposes.

Helper tactics

We also provide some helper tactics:

atomic info: show a subterm corresponding to a position
atomic show: preview the effect of atomic auto on a subterm at a given position

What we don't provide

We don't give a way of applying multiple reductions at once as things stands. This proposal is mostly a prototype.

2.2. Positions in a term

The way positions are managed as things stand is by passing a list of integers. This list describes which branch to take at each level of the syntax tree:

atomic auto at [2 0].

This is not exactly user friendly (think about very deep subterms) nor intuitive (think about notations hiding some branches). Extending atomic with support for pattern based selection and such is future work.

3. Backend implementation

3.1. Extending conversions

3.2. Bunched reductions

4. Frontend implementation

5. The code

6. Future work

In its current state, the atomic extension is nothing more than a prototype. It concretely shows how the inclusion of tactics for low-level control of the reduction process can drastically improve the handling of some proofs. However, it is lacking with regards TODO

6.1. Avoid duplicating terms in conversions

As things stand, conversions are given in absolute terms, whereas in some situations, it would dramatically more economical to give something relative to the type of the object of the conversion.