The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/30/2014 01:26 PM, Xavier Leroy wrote:
> On 29/07/14 16:28, Enrico Tassi wrote:
> > Let me add that there is no good reason for the tactic to fail here.
> > If "list ..." and "sf" are convertible then they are the very same term.
> Hear, hear!
>
> > In the implementation of the rewrite tactic that is part of ssreflect
> > the conversion relation is taken into account.
> Good to know.  Maybe I should defect to the other side :-)
>
> More seriously, this issue with "rewrite" has been making my life
> miserable since I started working on CompCert 10 years ago, and it is
> still a major trap for beginners.  Could we hope to have it fixed once
> and for all?  To me, that would be about as valuable as all the
> changes planned for Coq 8.5 combined...
>
> While we are at it, "rewrite" is not the only tactic that is dumb
> w.r.t. convertibility of types.  "omega" is also easily confused:
>
> Definition offset := Z.
> Goal forall x, @eq offset (x + 0) 0.
> Proof. intros; omega.
> (* Error: Omega can’t solve this system *)
>
> That makes me sad.
>
> - Xavier

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.

-- Jonathan