Armaël Guéneau

2018-11-08 10:24:23 UTC

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

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