Zulip Chat Archive

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?

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

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: Dec 20 2023 at 11:08 UTC