Module 5 · Lesson 2

ring — Polynomial Equations

Automatically prove polynomial ring equations. The ring tactic proves identities in commutative rings, such as expanding a product, which would otherwise take many rewriting steps.

❗

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

The Problem ring Solves

Imagine proving (x + y)² = x² + 2xy + y² by hand. You'd need to apply distributivity, commutativity, and associativity multiple times. Thering tactic does all of this automatically:

lean

1import Mathlib.Tactic.Ring
2
3-- Without ring, you'd need many steps:
4-- (x + y) * (x + y)
5-- = x * (x + y) + y * (x + y)     -- distributivity
6-- = x*x + x*y + y*x + y*y         -- distributivity again
7-- = x² + x*y + x*y + y²           -- commutativity
8-- = x² + 2*x*y + y²               -- combining like terms
9
10-- With ring: one tactic, done
11example (x y : Int) : (x + y)^2 = x^2 + 2*x*y + y^2 := by ring

Basic Usage

The ring tactic proves equalities between polynomial expressions by expanding both sides to a canonical form and comparing. It handles the tedious algebraic manipulation automatically.

lean

1import Mathlib.Tactic.Ring
2
3-- Expansion and simplification
4example (x y : Int) : (x + y) * (x - y) = x^2 - y^2 := by ring
5
6-- Multinomial expansion
7example (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
8
9-- Cubes
10example (x : Int) : (x + 1)^3 = x^3 + 3*x^2 + 3*x + 1 := by ring
11
12-- Combining like terms
13example (a b : Int) : 3*a + 2*b + a - b + 5*a = 9*a + b := by ring

Key Takeaway

ring proves equalities that follow from ring axioms: associativity, commutativity, distributivity, and the properties of 0 and 1. It works by reducing both sides to a canonical form.

Understanding Ring Axioms

A ring is an algebraic structure with two operations (+ and ×) satisfying these properties:

Addition is commutative: a + b = b + a
Addition is associative: (a + b) + c = a + (b + c)
Additive identity: a + 0 = a
Additive inverse: a + (-a) = 0
Multiplication is associative: (a × b) × c = a × (b × c)
Multiplicative identity: a × 1 = a
Distributivity: a × (b + c) = a × b + a × c

The ring tactic proves any equality that follows from these axioms. It doesn't need to know specific values—it works purely symbolically.

What ring Handles

ring works with expressions built from:

Addition (+) and subtraction (-)
Multiplication (*)
Exponentiation by natural numbers (^)
Negation (-x)
Numeric constants

lean

1import Mathlib.Tactic.Ring
2
3-- Product expansion
4example (x : Int) : (x + 1) * (x + 2) = x^2 + 3*x + 2 := by ring
5
6-- Factoring (proving the expansion equals the factored form)
7example (x : Int) : x^2 - 1 = (x + 1) * (x - 1) := by ring
8
9-- Collecting 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
14
15-- Powers
16example (x : Int) : x^4 - 1 = (x - 1) * (x + 1) * (x^2 + 1) := by ring

Works on Different Types

ring works on any type that forms a ring (or commutative ring). The standard library provides instances for common numeric 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
8example (a b : Int) : (a - b) * (a + b) = a^2 - b^2 := by ring
9
10-- Rationals
11example (p q : Rat) : (p + q) / 2 + (p - q) / 2 = p := by ring
12
13-- With Mathlib, also works on:
14-- ℝ (reals), ℂ (complex), ℚ (rationals), polynomial rings, etc.

ring_nf: Normalization Without Closing

Sometimes you want to simplify an expression to canonical form without trying to close the goal. Use ring_nf for this:

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-- Normalize at a hypothesis
9example (x y : Int) (h : (x + y)^2 = 9) : x^2 + 2*x*y + y^2 = 9 := by
10  ring_nf at h  -- h becomes: x^2 + 2*x*y + y^2 = 9
11  exact h
12
13-- Useful when ring doesn't quite close the goal
14example (x : Int) (h : x^2 = 4) : (x + 1)^2 - 2*x - 1 = 4 := by
15  ring_nf  -- Simplifies to: x^2 = 4
16  exact h

Famous Algebraic Identities

ring can prove many famous identities from algebra:

Difference of Powers

lean

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

Sophie Germain Identity

lean

1import Mathlib.Tactic.Ring
2
3-- Sophie Germain's identity (discovered in early 1800s)
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

Binomial Expansions

lean

1import Mathlib.Tactic.Ring
2
3-- Binomial theorem cases
4example (x : Int) : (1 + x)^2 = 1 + 2*x + x^2 := by ring
5example (x : Int) : (1 + x)^3 = 1 + 3*x + 3*x^2 + x^3 := by ring
6example (x : Int) : (1 + x)^4 = 1 + 4*x + 6*x^2 + 4*x^3 + x^4 := by ring
7
8-- General pattern
9example (a b : Int) : (a + b)^3 = a^3 + 3*a^2*b + 3*a*b^2 + b^3 := by ring

Limitations

ring only handles polynomial equalities. It doesn't work with:

lean

1import Mathlib.Tactic.Ring
2
3-- ❌ Division (use field_simp first to clear denominators)
4-- example (x : Rat) (h : x ≠ 0) : x / x = 1 := by ring  -- Fails!
5
6-- ✅ With field_simp:
7example (x : Rat) (h : x ≠ 0) : x / x = 1 := by field_simp
8
9-- ❌ Inequalities (use linarith or nlinarith)
10-- example (x : Int) : x^2 ≥ 0 := by ring  -- Fails!
11
12-- ✅ With nlinarith:
13example (x : Int) : x^2 ≥ 0 := by nlinarith [sq_nonneg x]
14
15-- ❌ Functions or predicates
16-- example (f : Int → Int) : f (x + y) = f (x + y) := by ring  -- Fails!
17
18-- ✅ Use rfl instead:
19example (f : Int → Int) (x y : Int) : f (x + y) = f (x + y) := rfl

💡

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

Deep Dive: How ring Works

The ring tactic works by:

Parsing: Convert both sides of the equality to an internal polynomial representation
Normalization: Expand all products, collect like terms, and sort monomials lexicographically
Comparison: Check if the normalized forms are identical
Certificate: If equal, construct a proof term witnessing the equality

This normalization-based approach is why ring is adecision procedure—it always terminates and can definitively say whether a polynomial equality holds.

ring vs Other Tactics

Goal Type	Use
Polynomial equality	`ring`
Equality with division	`field_simp` then `ring`
Linear arithmetic (Nat/Int)	`omega`
Linear inequalities	`linarith`
Non-linear inequalities	`nlinarith`
Simple definitions	`simp`

Common Patterns

Completing the Square

lean

1import Mathlib.Tactic.Ring
2
3-- Standard completing the square
4example (x : Int) : x^2 + 6*x + 9 = (x + 3)^2 := by ring
5
6-- General form
7example (x a : Int) : x^2 + 2*a*x + a^2 = (x + a)^2 := by ring
8
9-- More complex
10example (x : Int) : x^2 + 4*x + 4 = (x + 2)^2 := by ring

Simplifying in Larger Proofs

lean

1import Mathlib.Tactic.Ring
2
3-- Using ring as part of a larger proof
4theorem sum_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
8
9-- Combining with other tactics
10example (x y : Int) (h : x = y + 1) : x^2 = y^2 + 2*y + 1 := by
11  rw [h]
12  ring

Exercise 1: Simple Expansion

Use ring to prove this binomial expansion.

lean

1import Mathlib.Tactic.Ring
2
3example (x y : Int) : (x + y)^2 = x^2 + 2*x*y + y^2 := by
4  ring

Exercise 2: Difference of Squares

Prove the difference of squares formula.

lean

1import Mathlib.Tactic.Ring
2
3example (a b : Int) : (a + b) * (a - b) = a^2 - b^2 := by
4  ring

Exercise 3: Collecting Terms

Simplify this expression to its simplest form.

lean

1import Mathlib.Tactic.Ring
2
3example (x : Int) : (x + 1)^2 - (x - 1)^2 = 4*x := by
4  ring

Mathlib Introduction Next: field_simp