Ring tactic

Stream: general

[Kevin Kappelmann]

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?

[Johan Commelin]

Does it work for comm_ring?

[Johan Commelin]

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

[Kevin Kappelmann]

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.

[Wojciech Nawrocki]

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