Module 5 · Lesson 2

ring

Automatically solve polynomial ring equations. The ring tactic handles algebraic manipulations that would otherwise require many manual steps.

❗

ring requires Mathlib. Add import Mathlib.Tactic.Ring to use this tactic.

Basic Usage

lean

1import Mathlib.Tactic.Ring
2
3-- ring solves polynomial equalities
4example (x y : Int) : (x + y) * (x - y) = x^2 - y^2 := by ring
5
6example (a b c : Int) : (a + b + c)^2 = a^2 + b^2 + c^2 + 2*a*b + 2*b*c + 2*a*c := by ring
7
8example (x : Int) : (x + 1)^3 = x^3 + 3*x^2 + 3*x + 1 := by ring

Key Takeaway

ring proves equalities that follow from ring axioms: associativity, commutativity, distributivity, and the properties of 0 and 1.

What ring Handles

lean

1import Mathlib.Tactic.Ring
2
3-- Expansion
4example (x : Int) : (x + 1) * (x + 2) = x^2 + 3*x + 2 := by ring
5
6-- Factoring (via equality)
7example (x : Int) : x^2 - 1 = (x + 1) * (x - 1) := by ring
8
9-- Combining like terms
10example (a b : Int) : 3*a + 2*b + a - b = 4*a + b := by ring
11
12-- Nested expressions
13example (x y z : Int) : (x + y) * z + x * (y + z) = x*y + 2*x*z + y*z := by ring

Works on Different Types

lean

1import Mathlib.Tactic.Ring
2
3-- Natural numbers
4example (n m : Nat) : (n + m) * (n + m) = n^2 + 2*n*m + m^2 := by ring
5
6-- Integers
7example (x : Int) : x * (-1) = -x := by ring
8
9-- Rationals
10example (p q : Rat) : (p + q) / 2 + (p - q) / 2 = p := by ring
11
12-- Reals (with Mathlib)
13-- example (r s : ℝ) : (r + s)^2 - (r - s)^2 = 4*r*s := by ring

ring_nf for Normalization

lean

1import Mathlib.Tactic.Ring
2
3-- ring_nf normalizes expressions without closing the goal
4example (x y : Int) (h : x^2 + 2*x*y + y^2 = 0) : (x + y)^2 = 0 := by
5  ring_nf  -- Transforms goal to: x^2 + 2*x*y + y^2 = 0
6  exact h
7
8-- Useful for rewriting to a canonical form
9example (a b : Int) : (a - b) * (a - b) = (b - a) * (b - a) := by ring

Deep Dive: How ring Works

The ring tactic works by:

Converting both sides to a canonical polynomial form
Expanding all multiplications and powers
Collecting like terms
Comparing the resulting normal forms

If the normal forms are identical, the equality holds by ring axioms. This makes it a decision procedure for polynomial ring equations.

Limitations

lean

1import Mathlib.Tactic.Ring
2
3-- ring doesn't handle:
4
5-- Division (use field_simp first)
6-- example (x : Rat) (h : x ≠ 0) : x / x = 1 := by ring  -- Fails!
7
8-- Inequalities (use linarith or nlinarith)
9-- example (x : Int) : x^2 ≥ 0 := by ring  -- Fails!
10
11-- Functions or predicates
12-- example (f : Int → Int) : f (x + y) = f (x + y) := by ring  -- Fails!
13
14-- ring only handles polynomial expressions

💡

For expressions with division, use field_simpfirst to clear denominators, then ring.

Real-World Examples

Proving Algebraic Identities

lean

1import Mathlib.Tactic.Ring
2
3-- Sophie Germain identity
4theorem sophie_germain (a b : Int) : 
5    a^4 + 4*b^4 = (a^2 + 2*b^2 + 2*a*b) * (a^2 + 2*b^2 - 2*a*b) := by
6  ring
7
8-- Difference of cubes
9theorem diff_cubes (x y : Int) :
10    x^3 - y^3 = (x - y) * (x^2 + x*y + y^2) := by
11  ring

Simplifying in Proofs

lean

1import Mathlib.Tactic.Ring
2
3-- Using ring as part of a larger proof
4theorem sum_of_squares_formula (n : Nat) (h : 6 * s = n * (n + 1) * (2*n + 1)) :
5    6 * s = 2*n^3 + 3*n^2 + n := by
6  rw [h]
7  ring

Common Patterns

lean

1import Mathlib.Tactic.Ring
2
3-- Completing the square
4example (x : Int) : x^2 + 6*x + 9 = (x + 3)^2 := by ring
5
6-- Difference of squares
7example (a b : Int) : a^2 - b^2 = (a + b) * (a - b) := by ring
8
9-- Binomial theorem cases
10example (x : Int) : (1 + x)^4 = 1 + 4*x + 6*x^2 + 4*x^3 + x^4 := by ring

Mathlib Introduction Next: field_simp