The Coq mailing list

[Armaël Guéneau <armael.gueneau AT ens-lyon.fr>]

Dear Coq-club,

I'm writing a reflexive tactic that (roughly speaking) simplifies
arithmetic expressions. It first reifies the goal into something like:

Inductive expr :=
| EAdd : expr -> expr -> expr
| EMul : expr -> expr -> expr
| ECst : Z -> expr.

ECst is a catch-all case: it may store arbitrary-looking terms, not only
numerical constants. These should be treated as abstract by the tactic.

Then, I implemented a [simplify : expr -> expr] Coq function, and proved
that it is meaning-preserving. Finally, my tactic reifies the goal,
applies the theorem specialized to the reified expression, and reduces
the result to obtain the simplified goal.

The issue I have is with this last part: I want to evaluate [simplify],
but I do not want the reduction tactic to reduce the contents of [ECst
..], since these can contain arbitrary terms that should be treated as
abstract.

How do I evaluate my tactic in a robust way? I feel like this is a
relatively fundamental issue, and for example I wonder how
[ring_simplifies] works around it? Does anyone know?

For the moment I thought about:

- Listing all the functions transitively used by [simplify] and reduce
with a whitelist (cbv [the functions...]). However: 1) there is a lot of
them 2) it's bad from a maintainability perspective 3) it does not quite
work as the whitelist will include stuff like Nat.eqb that might very
well be used in a [ECst ..].

- Introducing local definitions for the terms in [ECst foo] (using [set
(x := foo)]); and blacklisting these local definitions during reduction.
There is a technical issue: the blacklist is discovered dynamically, so
I cannot specify it in Ltac using cbv -[foo bar baz]. I guess I could
write a small plugin to handle dynamically constructing the blacklist,
if that's what it takes...

Any ideas?

— Armaël