Topic: real examples for ring?
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
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
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.
Joseph Corneli (Mar 27 2019 at 16:28):
Chris Hughes (Mar 27 2019 at 16:28):
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
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
Chris Hughes (Mar 27 2019 at 16:44):
rintro rfl :rolling_eyes:
Last updated: May 14 2021 at 19:21 UTC