The Coq mailing list

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

Le 08/11/2018 à 11:31, Guillaume Melquiond a écrit :
> 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.

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