The Coq mailing list

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

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