## Stream: general

### Topic: ring bug?

#### Heather Macbeth (Jan 30 2022 at 14:57):

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 (Jan 30 2022 at 14:57):

Is it a bug in ring1?

#### Mario Carneiro (Jan 30 2022 at 20:16):

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

#### Patrick Massot (Jan 30 2022 at 20:18):

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

#### Heather Macbeth (Jan 30 2022 at 20:19):

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 (Jan 30 2022 at 20:20):

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 (Jan 30 2022 at 20:20):

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

#### Mario Carneiro (Jan 30 2022 at 20:21):

ring will do the normalization stuff if it fails

#### Mario Carneiro (Jan 30 2022 at 20:21):

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

#### Heather Macbeth (Jan 30 2022 at 20:21):

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 (Jan 30 2022 at 20:23):

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

#### Mario Carneiro (Jan 30 2022 at 20:23):

I don't see a abel_nf though

#### Patrick Massot (Jan 30 2022 at 20:25):

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

#### Mario Carneiro (Jan 30 2022 at 20:28):

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

#### Patrick Massot (Jan 30 2022 at 20:29):

I know, I checked before posting

Last updated: Dec 20 2023 at 11:08 UTC