## Stream: general

### Topic: Ring tactic

#### 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
end


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

#### Johan Commelin (Aug 06 2019 at 08:53):

Does it work for comm_ring?

#### Johan Commelin (Aug 06 2019 at 08:53):

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

#### 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.

#### 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