Zulip Chat Archive

Stream: maths

Topic: field_simp fails


view this post on Zulip Yury G. Kudryashov (Dec 19 2019 at 22:14):

Hi, field_simp fails to simplify y = (y - x) / (z - x) * z + (1 - (y - x) / (z - x)) * x. It gives y = (y + -x) * z / (z + -x) + (1 + (x + -y) / (z + -x)) * x. It seems that it lacks a + b / c = (a * c + b) / c rule.

view this post on Zulip Yury G. Kudryashov (Dec 19 2019 at 22:18):

Sorry, adding h : z + -x ≠ 0 did the trick (didn't work with z - x ≠ 0).

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:22):

aah, the dreaded sub_eq_add_neg strikes again!

view this post on Zulip Yury G. Kudryashov (Dec 19 2019 at 22:24):

Possibly field_simp should (partially) simplify its arguments first.

view this post on Zulip Yury G. Kudryashov (Dec 19 2019 at 22:24):

Without sub_eq_add_neg we would need separate lemmas for a - b / c etc.

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 22:25):

Yes, it is somehow a necessary evil sometimes


Last updated: May 06 2021 at 18:20 UTC