The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

On 30/07/14 20:11, Jonathan wrote:
> How about this stop-gap proposal: define an unfold hint db to which users
> can add their own hints, and which is used by Coq in cases like rewrite and
> omega (and I'm sure plenty of others).  Or, slightly better - have a setting
> like "Add Implicit Autounfolds dbname" so that multiple different hint dbs
> can be used.

Thanks for the suggestion.  It could work pretty well for my uses in
CompCert, because I have relatively few type aliases and they get
reused a lot.  But Coq beginners would still be baffled, first by the
mysterious failures of rewrite et al, then by the need to build an
unfold hint db...

Why just a stop-gap and not a proper fix?  Being curious, I looked at
the implementation of "omega" to undestand why it skips equalities at
types that are aliases of Z.  The algorithm is, as far as I
understand:
- normalize the type part of the equality using "pf_nf"
(i.e. "pf_reduce simpl") (apparently something that doesn't unfold
definitions);
- test for equality with the "Z" type constructor.

Why not just a conversion check instead of "normalize (incompletely)
then test for equality"?  What could possibly go wrong?

Apologies for being probably naive and  definitely heavy-handed with this
issue, but I strongly feel that a number of basic tactics of Coq could
use some love.  That they have been clunky for the last two decades
and that power users learned to work around this clunkiness is no
reason for status quo.

- Xavier