ring

Summary

The ring tactic proves identities in commutative rings such as (x+y)^2=x^2+2*x*y+y^2. It works on concrete rings such as ℝ and abstract rings, and will also prove some results in “semirings” such as ℕ.

Note that ring does not and cannot look at hypotheses. See the examples for various ways of working around this.

Examples

A basic example is

example (x y : ℝ) : x^3-y^3=(x-y)*(x^2+x*y+y^2) :=
begin
  ring
end

2) Note that ring cannot use hypotheses – the goal has to be an identity. For example faced with

x y : ℝ
h : x = y ^ 2
⊢ x ^ 2 = y ^ 4

the ring tactic will not close the goal, because it does not know about h. The way to solve this goal is rw h, ring.

Sometimes you are in a situation where you cannot rw the hypothesis you want to use. For example if the tactic state is

x y : ℝ
h : x ^ 2 = y ^ 2
⊢ x ^ 4 = y ^ 4

then rw h will fail (of course we know that x^4=(x^2)^2, but rw works up to syntactic equality and it cannot see an x^2 in the goal). In this situation we can use ring to prove an intermediate result and then rewrite our way out of trouble. For example this goal can be solved in the following way.

example (x y : ℝ) (h : x^2 = y^2) : x^4 = y^4 :=
begin
  have h2 : x^4=(x^2)^2, -- introduce a new goal
  { ring }, -- proves ``h2``; note that the `{...}` brackets are good practice
            -- when there is more than one goal
  rw h2, -- goal now ``⊢ (x ^ 2) ^ 2 = y ^ 4``...
  rw h, -- ...so ``rw h`` now works, giving us ``⊢ (y ^ 2) ^ 2 = y ^ 4``
  ring,
end

Further notes

There’s a variant of ring called ring! but I don’t know a concrete example where one works and the other doesn’t.

ring is a “finishing tactic”; this means that it should only be used to close goals. If ring does not close a goal it will issue a warning that you should use the related tactic ring_nf.

ring might not work sometimes with variable exponents like x^n. The variant ring_exp is better at dealing with them.

The algorithm used in the ring tactic is based on the 2005 paper “Proving Equalities in a Commutative Ring Done Right in Coq” by Benjamin Grégoire and Assia Mahboubi.