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 (
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.
The following reduction steps are a generating set for evaluation in Coq (more information here):
In addition to these, there is another reduction step which is functionally redundant with the above but can have an impact on performance:
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.
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.
The atomic extension defines a set of tactics, each of them corresponding to one of the aforementioned basic reduction steps:
These tactics fail when they can't be applied at the given position.
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.
We also provide some helper tactics:
We don't give a way of applying multiple reductions at once as things stands. This proposal is mostly a prototype.
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:
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.