ring bug?

Stream: general

[Heather Macbeth]

I encountered a messy error message and the failure of the expected simplification when applying ring1 on an example which simplifies to the following:

import tactic.ring

variables {R : Type*} [comm_ring R] {S : Type*} [comm_ring S] [has_coe R S]

example {θ : S} (x : R) :
  θ = x - x :=
begin
  ring1,

end

error:

is_def_eq tactic failed, the following expressions are not definitionally equal (remark: is_def_eq tactic does modify the metavariable assignment)
  tactic.ring.horner 1 θ 1 0 : S
and
  0 : S

[Heather Macbeth]

Is it a bug in ring1?

[Mario Carneiro]

That's the expected error when you try to prove a ring equality that isn't true

[Patrick Massot]

Maybe we could catch this error and turn it into a message suggesting the equality may be false?

[Heather Macbeth]

Mario Carneiro said:

That's the expected error when you try to prove a ring equality that isn't true

But this is ring1, it ought to just normalize the goal to have 0 on the RHS.

[Mario Carneiro]

I think this got lost in the shuffle. ring used to clean up the goal by writing the two sides in sum of products form, but then people started using it deliberately for that purpose so the code got moved to ring_nf

[Mario Carneiro]

ring1 is a oneshot tactic: the goal is a ring equality and it is proved or fails

[Mario Carneiro]

ring will do the normalization stuff if it fails

[Mario Carneiro]

you should only use ring1 if you don't want the overhead of the normalization stuff when you know it's true

[Heather Macbeth]

Oh, sorry, I did mean ring_nf. Isn't abel1 the normalizing version of abel? I think that's why I forgot the syntax.

[Mario Carneiro]

from a cursory glance (I don't think I wrote abel1), it has the same relation to abel as ring1 to ring

[Mario Carneiro]

I don't see a abel_nf though

[Patrick Massot]

https://github.com/leanprover-community/mathlib/blob/master/src/tactic/abel.lean#L2-L4

[Mario Carneiro]

I meant abel1 specifically, but I've just git blamed myself, so...

[Patrick Massot]

I know, I checked before posting