The Coq mailing list

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

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