Zulip Chat Archive

Stream: general

Topic: Ring tactic


view this post on Zulip Kevin Kappelmann (Aug 06 2019 at 08:50):

Hi, I am writing a tutorial for computations in Lean, and I was surprised that ring fails in this case:

import tactic.ring
variables {α : Type*} {a b : α} [ring α]

example : (a + b) * (a + b) = a * a + b * a + a * b + b * b :=
by ring -- fails

-- this works
example : (a + b) * (a + b) = a * a + b * a + a * b + b * b :=
begin
rw mul_add,
rw add_mul,
rw add_mul,
rw add_assoc
end

Is that something to expect or is that also surprising to someone else?

view this post on Zulip Johan Commelin (Aug 06 2019 at 08:53):

Does it work for comm_ring?

view this post on Zulip Johan Commelin (Aug 06 2019 at 08:53):

I think the ring tactic only works in the commutative case.

view this post on Zulip Kevin Kappelmann (Aug 06 2019 at 08:59):

Yep, it does work for comm_ring. In fact, ring already fails for this example:

example : a + b = b + a := by ring -- fails
example : a + b = b + a := by rw add_comm

So I suppose you are right that tactic.ring is actually more like tactic.comm_ring.

view this post on Zulip Wojciech Nawrocki (Aug 06 2019 at 10:04):

Currently it requires an instance of comm_semiring, which a ring is not.


Last updated: May 08 2021 at 18:17 UTC