The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le 08/11/2018 à 11:24, Armaël Guéneau a écrit :
> 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.

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