[Coq-Club] How to evaluate reflexive tactics? (in a robust way)

[Armaël Guéneau]

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

[Guillaume Melquiond]

Post by Armaël Guéneau
Dear Coq-club,
I'm writing a reflexive tactic that (roughly speaking) simplifies
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.

A good idea is generally not to store the constants directly as an
argument of the constructor. It is better to store them in a map and use
an index in the constructor. There are two advantages. First, you no
longer care about it being evaluated. Second, your simplification code
can now be made aware that two constants are equal.

Still, you might later on still have some evaluation issues, especially
when inverting the reification process. In that case, I suggest taking a
look at the "Strategy" vernacular.

Best regards,

Guillaume

[Armaël Guéneau]

Post by Guillaume Melquiond
A good idea is generally not to store the constants directly as an
argument of the constructor. It is better to store them in a map and use
an index in the constructor. There are two advantages. First, you no
longer care about it being evaluated. Second, your simplification code
can now be made aware that two constants are equal.

Thanks, that sounds like a better idea indeed. Could you detail a bit
more how it would work, though? The interpretation function would still
have to take this map as argument, if I'm not mistaking? How do you
prevent the map itself (and the constants inside) from being evaluated?

Post by Guillaume Melquiond
Still, you might later on still have some evaluation issues, especially
when inverting the reification process. In that case, I suggest taking a
look at the "Strategy" vernacular.

Thanks again, I didn't know about that one; I will keep that in mind.

[Guillaume Melquiond]

Post by Armaël Guéneau

Post by Guillaume Melquiond
A good idea is generally not to store the constants directly as an
argument of the constructor. It is better to store them in a map and use
an index in the constructor. There are two advantages. First, you no
longer care about it being evaluated. Second, your simplification code
can now be made aware that two constants are equal.

Thanks, that sounds like a better idea indeed. Could you detail a bit
more how it would work, though? The interpretation function would still
have to take this map as argument, if I'm not mistaking? How do you
prevent the map itself (and the constants inside) from being evaluated?

You abstract the map away, at the time you force the reduction. Your
goal should look as follows after applying your main correctness theorem:

|- eval (simplify reified_term) constants

You can turn it into two goals, e.g. by rewriting:

|- simplify reified_term = ?1
|- eval ?1 constants

Then you force the reduction in the first goal. Notice that it does not
mention "constants" anywhere, so you are fine.

Best regards,

Guillaume

[Guillaume Melquiond]

Post by Guillaume Melquiond

Post by Armaël Guéneau
Dear Coq-club,
I'm writing a reflexive tactic that (roughly speaking) simplifies
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.

A good idea is generally not to store the constants directly as an
argument of the constructor. It is better to store them in a map and use
an index in the constructor. There are two advantages. First, you no
longer care about it being evaluated. Second, your simplification code
can now be made aware that two constants are equal.

I guess I should have stated it explicitly, but the above indirection is
used by all the standard reflexive tactics: "ring", "field", "tauto",
"romega", "lia", "lra", and so on.

Best regards,

Guillaume

[Gabriel Scherer]

A fairly generic solution (I don't know if it already exists) would be a
parametrized proxy type, isomorphic to the identity on types, that blocks
reduction/simplification. You could use (block_reduction Z) instead of Z as
the ECst value parameter.

Post by Armaël Guéneau
Dear Coq-club,
I'm writing a reflexive tactic that (roughly speaking) simplifies
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?
- 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

[Sylvain Boulmé]

Hello,

I provide below an other example related to Armaël's question.

By default, ring does not benefit from computations over "constants".
This could be painful (see the proof of "painful_test" in attachment).

But, ring provides a way to overcome this limitation, see:
https://coq.inria.fr/refman/addendum/ring.html#adding-a-ring-structure

In particular, the user can provide a tactic (like dummy_cte in
attachment) to discriminate between "constants" and other terms.

Is there a standard way to do it ?

In order to have a robust tactic (instead of dummy_cte), we could define
a tactic that recognizes closed terms in normal formal form (ie built
from constructors of inductive types). But this might not be sufficient
in practice (e.g. the rational (4#2) would not be considered as a constant).

Any ideas ?

Sylvain.

Post by Armaël Guéneau
Dear Coq-club,
I'm writing a reflexive tactic that (roughly speaking) simplifies
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?
- 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