The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

One thing that could go wrong with a conversion check is that it might
be really expensive in some cases. Another problem is that a fix might
break some existing contribs ;).

In any case, I had a look at the code of omega, and it seems quite
easy indeed to implement this heavy-handed solution.


On Thu, Jul 31, 2014 at 6:48 PM, Xavier Leroy 
<Xavier.Leroy AT inria.fr>
 wrote:
> 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