Zulip Chat Archive

Stream: maths

Topic: ring confusion


view this post on Zulip 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:

view this post on Zulip Kevin Buzzard (Mar 01 2019 at 13:03):

Try simp?

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Mar 01 2019 at 20:49):

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

view this post on Zulip Kevin Buzzard (Mar 01 2019 at 20:51):

Is there more than one x?

view this post on Zulip Johan Commelin (Mar 01 2019 at 20:53):

nope

view this post on Zulip Johan Commelin (Mar 01 2019 at 20:53):

simp closes the second goal (but not the first)

view this post on Zulip 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

view this post on Zulip 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