The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

Hi Xavier,

On 30 juil. 2014, at 19:26, Xavier Leroy 
<Xavier.Leroy AT inria.fr>
 wrote:

> 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:

For lia, I had this convertibility thing on my todo list for a (very) long 
time.
just pushed the fix in trunk.

> Definition offset := Z.
> Goal forall x, @eq offset (x + 0) 0.
> Proof. intros; omega.
> (* Error: Omega can’t solve this system *)

Now, lia can prove goals such as
Require Import Lia.

Definition offset := Z.
Goal forall x, @eq offset (x + 0) x.
Proof. intros ; lia. Qed.


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

This is what I have implemented. I would certainly be glad to know if this « 
could possibly go wrong »
Maybe the conversion could run forever ? 
Btw, in the previous Goal, what is the type given by coq to (x+0) or x ? Z or 
offset…

—
Frédéric