## Stream: maths

### Topic: ring confusion

#### Johan Commelin (Mar 01 2019 at 12:19):

Goal before I apply ring:

(x.snd).val * x.fst - x.fst * (x.snd).val = 0


Goal after applying ring:

(-(x.snd).val + (x.snd).val) * x.fst = 0


Me after applying ring: :sad: :cry: :rage:

#### Kevin Buzzard (Mar 01 2019 at 13:03):

Try simp?

#### Kevin Buzzard (Mar 01 2019 at 13:05):

I feel like with linarith I have got to the point where I understand what the tactic is doing so I can use it well. I had thought the same was true with ring but this confuses me. If you generalize x.snd or x.snd.val presumably the problem goes away?

#### Mario Carneiro (Mar 01 2019 at 20:49):

This means it doesn't think the two x.snd.val's are the same

#### Kevin Buzzard (Mar 01 2019 at 20:51):

Is there more than one x?

nope

#### Johan Commelin (Mar 01 2019 at 20:53):

simp closes the second goal (but not the first)

#### Mario Carneiro (Mar 01 2019 at 21:06):

The equality relation used by ring is very restrictive, because it has to totally order the terms

#### Mario Carneiro (Mar 01 2019 at 21:07):

To do something else would require a preprocessing step to merge defeq things or something

Last updated: May 19 2021 at 02:10 UTC