Zulip Chat Archive

Stream: maths

Topic: real examples for ring?


view this post on Zulip Joseph Corneli (Mar 27 2019 at 16:24):

The first two examples here are successful but not very interesting; the third fails. Could someone suggest a more interesting working example to illustrate ring?

example (x : ) : x=2  2+x=x+2 := begin intro h, ring, end -- works
example (x : ) : x=2  2*x=x*2 := begin intro h, ring, end -- works
example (x : ) : x=2  2+x=x*2 := begin intro h, ring, end -- fails

view this post on Zulip Johan Commelin (Mar 27 2019 at 16:27):

ring is good at expanding parentheses. So take (x + y)*(3+x^2+y), and put the expanded version on the RHS. Then ring can prove you did it right.

view this post on Zulip Joseph Corneli (Mar 27 2019 at 16:28):

thanks

view this post on Zulip Chris Hughes (Mar 27 2019 at 16:28):

I think ring just doesn't use hypotheses.
A more interesting example is

example (x y : ) : (x - y) ^ 3 = x^3 - 3 * x^2 * y + 3 * x * y^2 - y^3 := by ring

view this post on Zulip Mario Carneiro (Mar 27 2019 at 16:38):

Something less obvious using a combination of ring and substitution:

example (x y : ) : x=2  (x+y)^2=y*(y+x*x)+x*2 := by rintro rfl; ring

view this post on Zulip Chris Hughes (Mar 27 2019 at 16:44):

rintro rfl :rolling_eyes:


Last updated: May 14 2021 at 19:21 UTC