ring confusion

Stream: maths

[Johan Commelin]

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]

Try simp?

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

Is there more than one x?

[Johan Commelin]

nope

[Johan Commelin]

simp closes the second goal (but not the first)

[Mario Carneiro]

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

[Mario Carneiro]

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