The Lean Language Reference

17.7. Algebraic Solver (Commutative Rings, Fields)🔗

The ring solver in grind is inspired by Gröbner basis computation procedures and term rewriting completion. It views multivariate polynomials as rewriting rules. For example, the polynomial equality x * y + x - 2 = 0 is treated as a rewriting rule x * y ↦ -x + 2. It uses superposition to ensure the rewriting system is confluent.

The following examples demonstrate goals that can be decided by the ring solver. In these examples, the Lean and Lean.Grind namespaces are open:

open Lean Grind
Commutative Rings
example [CommRing α] (x : α) : (x + 1) * (x - 1) = x ^ 2 - 1 := α:Type u_1inst✝:CommRing αx:α⊢ (x + 1) * (x - 1) = x ^ 2 - 1 All goals completed! 🐙
Ring Characteristics

The solver “knows” that 16*16 = 0 because the ring characteristic (that is, the minimum number of copies of the multiplicative identity that sum to the additive identity) is 256, which is provided by the IsCharP instance.

example [CommRing α] [IsCharP α 256] (x : α) : (x + 16)*(x - 16) = x^2 := α:Type u_1inst✝¹:CommRing αinst✝:IsCharP α 256x:α⊢ (x + 16) * (x - 16) = x ^ 2 All goals completed! 🐙
Standard Library Types

Types in the standard library are supported by the solver out of the box. UInt8 is a commutative ring with characteristic 256, and thus has instances of CommRing UInt8 and IsCharP UInt8 256.

example (x : UInt8) : (x + 16) * (x - 16) = x ^ 2 := x:UInt8⊢ (x + 16) * (x - 16) = x ^ 2 All goals completed! 🐙
More Commutative Ring Proofs

The axioms of a commutative ring are sufficient to prove these statements.

example [CommRing α] (a b c : α) : a + b + c = 3 → a ^ 2 + b ^ 2 + c ^ 2 = 5 → a ^ 3 + b ^ 3 + c ^ 3 = 7 → a ^ 4 + b ^ 4 = 9 - c ^ 4 := α:Type u_1inst✝:CommRing αa:αb:αc:α⊢ a + b + c = 3 → a ^ 2 + b ^ 2 + c ^ 2 = 5 → a ^ 3 + b ^ 3 + c ^ 3 = 7 → a ^ 4 + b ^ 4 = 9 - c ^ 4 All goals completed! 🐙 example [CommRing α] (x y : α) : x ^ 2 * y = 1 → x * y ^ 2 = y → y * x = 1 := α:Type u_1inst✝:CommRing αx:αy:α⊢ x ^ 2 * y = 1 → x * y ^ 2 = y → y * x = 1 All goals completed! 🐙
Characteristic Zero

ring proves that a + 1 = 2 + a is unsatisfiable because the characteristic is known to be 0.

example [CommRing α] [IsCharP α 0] (a : α) : a + 1 = 2 + a → False := α:Type u_1inst✝¹:CommRing αinst✝:IsCharP α 0a:α⊢ a + 1 = 2 + a → False All goals completed! 🐙
Inferred Characteristic

Even when the characteristic is not initially known, when grind discovers that n = 0 for some numeral n, it makes inferences about the characteristic:

example [CommRing α] (a b c : α) (h₁ : a + 6 = a) (h₂ : c = c + 9) (h : b + 3*c = 0) : 27*a + b = 0 := α:Type u_1inst✝:CommRing αa:αb:αc:αh₁:a + 6 = ah₂:c = c + 9h:b + 3 * c = 0⊢ 27 * a + b = 0 All goals completed! 🐙

17.7.1. Solver Type Classes🔗

Users can enable the ring solver for their own types by providing instances of the following type classes, all in the Lean.Grind namespace:

The algebraic solvers will self-configure depending on the availability of these instances, so not all need to be provided. The capabilities of the algebraic solvers will, of course, degrade when some are not available.

The Lean standard library contains the applicable instances for the types defined in the standard library. By providing these instances, other libraries can also enable grind's ring solver. For example, the Mathlib CommRing type class implements Lean.Grind.CommRing to ensure the ring solver works out-of-the-box.

17.7.1.1. Algebraic Structures

To enable the algebraic solver, a type should have an instance of the most specific possible algebraic structure that the solver supports. In order of increasing specificity, that is Semiring, Ring, CommSemiring, CommRing, and Field.

🔗type class
Lean.Grind.Semiring.{u} (α : Type u) : Type u
Lean.Grind.Semiring.{u} (α : Type u) :
  Type u

A semiring, i.e. a type equipped with addition, multiplication, and a map from the natural numbers, satisfying appropriate compatibilities.

Use Ring instead if the type also has negation, CommSemiring if the multiplication is commutative, or CommRing if the type has negation and multiplication is commutative.

Instance Constructor

Lean.Grind.Semiring.mk.{u}

Extends

Methods

add : α → α → α
Inherited from
  1. Add α
  2. Mul α
mul : α → α → α
Inherited from
  1. Add α
  2. Mul α
natCast : NatCast α

In every semiring there is a canonical map from the natural numbers to the semiring, providing the values of 0 and 1. Note that this function need not be injective.

ofNat : (n : Nat) → OfNat α n

Natural number numerals in the semiring. The field ofNat_eq_natCast ensures that these are (propositionally) equal to the values of natCast.

nsmul : HMul Nat α α

Scalar multiplication by natural numbers.

npow : HPow α Nat α

Exponentiation by a natural number.

add_zero : ∀ (a : α), a + 0 = a

Zero is the right identity for addition.

add_comm : ∀ (a b : α), a + b = b + a

Addition is commutative.

add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)

Addition is associative.

mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)

Multiplication is associative.

mul_one : ∀ (a : α), a * 1 = a

One is the right identity for multiplication.

one_mul : ∀ (a : α), 1 * a = a

One is the left identity for multiplication.

left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c

Left distributivity of multiplication over addition.

right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c

Right distributivity of multiplication over addition.

zero_mul : ∀ (a : α), 0 * a = 0

Zero is right absorbing for multiplication.

mul_zero : ∀ (a : α), a * 0 = 0

Zero is left absorbing for multiplication.

pow_zero : ∀ (a : α), a ^ 0 = 1

The zeroth power of any element is one.

pow_succ : ∀ (a : α) (n : Nat), a ^ (n + 1) = a ^ n * a

The successor power law for exponentiation.

ofNat_succ : ∀ (a : Nat), OfNat.ofNat (a + 1) = OfNat.ofNat a + 1

Numerals are consistently defined with respect to addition.

ofNat_eq_natCast : ∀ (n : Nat), OfNat.ofNat n = ↑n

Numerals are consistently defined with respect to the canonical map from natural numbers.

nsmul_eq_natCast_mul : ∀ (n : Nat) (a : α), n * a = ↑n * a
🔗type class
Lean.Grind.CommSemiring.{u} (α : Type u) : Type u
Lean.Grind.CommSemiring.{u} (α : Type u) :
  Type u

A commutative semiring, i.e. a semiring with commutative multiplication.

Use CommRing if the type has negation.

Instance Constructor

Lean.Grind.CommSemiring.mk.{u}

Extends

Methods

add : α → α → α
Inherited from
  1. Lean.Grind.Semiring α
mul : α → α → α
Inherited from
  1. Lean.Grind.Semiring α
natCast : NatCast α
Inherited from
  1. Lean.Grind.Semiring α
ofNat : (n : Nat) → OfNat α n
Inherited from
  1. Lean.Grind.Semiring α
nsmul : HMul Nat α α
Inherited from
  1. Lean.Grind.Semiring α
npow : HPow α Nat α
Inherited from
  1. Lean.Grind.Semiring α
add_zero : ∀ (a : α), a + 0 = a
Inherited from
  1. Lean.Grind.Semiring α
add_comm : ∀ (a b : α), a + b = b + a
Inherited from
  1. Lean.Grind.Semiring α
add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
Inherited from
  1. Lean.Grind.Semiring α
mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
Inherited from
  1. Lean.Grind.Semiring α
mul_one : ∀ (a : α), a * 1 = a
Inherited from
  1. Lean.Grind.Semiring α
one_mul : ∀ (a : α), 1 * a = a
Inherited from
  1. Lean.Grind.Semiring α
left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
Inherited from
  1. Lean.Grind.Semiring α
right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
Inherited from
  1. Lean.Grind.Semiring α
zero_mul : ∀ (a : α), 0 * a = 0
Inherited from
  1. Lean.Grind.Semiring α
mul_zero : ∀ (a : α), a * 0 = 0
Inherited from
  1. Lean.Grind.Semiring α
pow_zero : ∀ (a : α), a ^ 0 = 1
Inherited from
  1. Lean.Grind.Semiring α
pow_succ : ∀ (a : α) (n : Nat), a ^ (n + 1) = a ^ n * a
Inherited from
  1. Lean.Grind.Semiring α
ofNat_succ : ∀ (a : Nat), OfNat.ofNat (a + 1) = OfNat.ofNat a + 1
Inherited from
  1. Lean.Grind.Semiring α
ofNat_eq_natCast : ∀ (n : Nat), OfNat.ofNat n = ↑n
Inherited from
  1. Lean.Grind.Semiring α
nsmul_eq_natCast_mul : ∀ (n : Nat) (a : α), n * a = ↑n * a
Inherited from
  1. Lean.Grind.Semiring α
mul_comm : ∀ (a b : α), a * b = b * a

Multiplication is commutative.

🔗type class
Lean.Grind.Ring.{u} (α : Type u) : Type u
Lean.Grind.Ring.{u} (α : Type u) : Type u

A ring, i.e. a type equipped with addition, negation, multiplication, and a map from the integers, satisfying appropriate compatibilities.

Use CommRing if the multiplication is commutative.

Instance Constructor

Lean.Grind.Ring.mk.{u}

Extends

Methods

add : α → α → α
Inherited from
  1. Lean.Grind.Semiring α
  2. Neg α
  3. Sub α
mul : α → α → α
Inherited from
  1. Lean.Grind.Semiring α
  2. Neg α
  3. Sub α
natCast : NatCast α
Inherited from
  1. Lean.Grind.Semiring α
  2. Neg α
  3. Sub α
ofNat : (n : Nat) → OfNat α n
Inherited from
  1. Lean.Grind.Semiring α
  2. Neg α
  3. Sub α
nsmul : HMul Nat α α
Inherited from
  1. Lean.Grind.Semiring α
  2. Neg α
  3. Sub α
npow : HPow α Nat α
Inherited from
  1. Lean.Grind.Semiring α
  2. Neg α
  3. Sub α
add_zero : ∀ (a : α), a + 0 = a
Inherited from
  1. Lean.Grind.Semiring α
  2. Neg α
  3. Sub α
add_comm : ∀ (a b : α), a + b = b + a
Inherited from
  1. Lean.Grind.Semiring α
  2. Neg α
  3. Sub α
add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
Inherited from
  1. Lean.Grind.Semiring α
  2. Neg α
  3. Sub α
mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
Inherited from
  1. Lean.Grind.Semiring α
  2. Neg α
  3. Sub α
mul_one : ∀ (a : α), a * 1 = a
Inherited from
  1. Lean.Grind.Semiring α
  2. Neg α
  3. Sub α
one_mul : ∀ (a : α), 1 * a = a
Inherited from
  1. Lean.Grind.Semiring α
  2. Neg α
  3. Sub α
left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
Inherited from
  1. Lean.Grind.Semiring α
  2. Neg α
  3. Sub α
right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
Inherited from
  1. Lean.Grind.Semiring α
  2. Neg α
  3. Sub α
zero_mul : ∀ (a : α), 0 * a = 0
Inherited from
  1. Lean.Grind.Semiring α
  2. Neg α
  3. Sub α
mul_zero : ∀ (a : α), a * 0 = 0
Inherited from
  1. Lean.Grind.Semiring α
  2. Neg α
  3. Sub α
pow_zero : ∀ (a : α), a ^ 0 = 1
Inherited from
  1. Lean.Grind.Semiring α
  2. Neg α
  3. Sub α
pow_succ : ∀ (a : α) (n : Nat), a ^ (n + 1) = a ^ n * a
Inherited from
  1. Lean.Grind.Semiring α
  2. Neg α
  3. Sub α
ofNat_succ : ∀ (a : Nat), OfNat.ofNat (a + 1) = OfNat.ofNat a + 1
Inherited from
  1. Lean.Grind.Semiring α
  2. Neg α
  3. Sub α
ofNat_eq_natCast : ∀ (n : Nat), OfNat.ofNat n = ↑n
Inherited from
  1. Lean.Grind.Semiring α
  2. Neg α
  3. Sub α
nsmul_eq_natCast_mul : ∀ (n : Nat) (a : α), n * a = ↑n * a
Inherited from
  1. Lean.Grind.Semiring α
  2. Neg α
  3. Sub α
neg : α → α
Inherited from
  1. Lean.Grind.Semiring α
  2. Neg α
  3. Sub α
sub : α → α → α
Inherited from
  1. Lean.Grind.Semiring α
  2. Neg α
  3. Sub α
intCast : IntCast α

In every ring there is a canonical map from the integers to the ring.

zsmul : HMul Int α α

Scalar multiplication by integers.

neg_add_cancel : ∀ (a : α), -a + a = 0

Negation is the left inverse of addition.

sub_eq_add_neg : ∀ (a b : α), a - b = a + -b

Subtraction is addition of the negative.

neg_zsmul : ∀ (i : Int) (a : α), -i * a = -(i * a)

Scalar multiplication by the negation of an integer is the negation of scalar multiplication by that integer.

zsmul_natCast_eq_nsmul : ∀ (n : Nat) (a : α), ↑n * a = n * a

Scalar multiplication by natural numbers is consistent with scalar multiplication by integers.

intCast_ofNat : ∀ (n : Nat), ↑(OfNat.ofNat n) = OfNat.ofNat n

The canonical map from the integers is consistent with the canonical map from the natural numbers.

intCast_neg : ∀ (i : Int), ↑(-i) = -↑i

The canonical map from the integers is consistent with negation.

🔗type class
Lean.Grind.CommRing.{u} (α : Type u) : Type u
Lean.Grind.CommRing.{u} (α : Type u) :
  Type u

A commutative ring, i.e. a ring with commutative multiplication.

Instance Constructor

Lean.Grind.CommRing.mk.{u}

Extends

Methods

add : α → α → α
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
mul : α → α → α
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
natCast : NatCast α
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
ofNat : (n : Nat) → OfNat α n
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
nsmul : HMul Nat α α
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
npow : HPow α Nat α
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
add_zero : ∀ (a : α), a + 0 = a
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
add_comm : ∀ (a b : α), a + b = b + a
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
mul_one : ∀ (a : α), a * 1 = a
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
one_mul : ∀ (a : α), 1 * a = a
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
zero_mul : ∀ (a : α), 0 * a = 0
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
mul_zero : ∀ (a : α), a * 0 = 0
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
pow_zero : ∀ (a : α), a ^ 0 = 1
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
pow_succ : ∀ (a : α) (n : Nat), a ^ (n + 1) = a ^ n * a
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
ofNat_succ : ∀ (a : Nat), OfNat.ofNat (a + 1) = OfNat.ofNat a + 1
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
ofNat_eq_natCast : ∀ (n : Nat), OfNat.ofNat n = ↑n
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
nsmul_eq_natCast_mul : ∀ (n : Nat) (a : α), n * a = ↑n * a
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
neg : α → α
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
sub : α → α → α
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
intCast : IntCast α
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
zsmul : HMul Int α α
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
neg_add_cancel : ∀ (a : α), -a + a = 0
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
neg_zsmul : ∀ (i : Int) (a : α), -i * a = -(i * a)
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
zsmul_natCast_eq_nsmul : ∀ (n : Nat) (a : α), ↑n * a = n * a
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
intCast_ofNat : ∀ (n : Nat), ↑(OfNat.ofNat n) = OfNat.ofNat n
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
intCast_neg : ∀ (i : Int), ↑(-i) = -↑i
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
mul_comm : ∀ (a b : α), a * b = b * a

Multiplication is commutative.

17.7.1.1.1. Fields🔗

The ring solver also has support for Fields. If a Field instance is available, the solver preprocesses the term a / b into a * b⁻¹. It also rewrites every disequality p ≠ 0 as the equality p * p⁻¹ = 1.

Fields and grind

This example requires its Field instance:

example [Field α] (a : α) : a ^ 2 = 0 → a = 0 := α:Type u_1inst✝:Field αa:α⊢ a ^ 2 = 0 → a = 0 All goals completed! 🐙
🔗type class
Lean.Grind.Field.{u} (α : Type u) : Type u
Lean.Grind.Field.{u} (α : Type u) : Type u

A field is a commutative ring with inverses for all non-zero elements.

Instance Constructor

Lean.Grind.Field.mk.{u}

Extends

Methods

add : α → α → α
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
mul : α → α → α
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
natCast : NatCast α
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
ofNat : (n : Nat) → OfNat α n
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
nsmul : HMul Nat α α
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
npow : HPow α Nat α
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
add_zero : ∀ (a : α), a + 0 = a
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
add_comm : ∀ (a b : α), a + b = b + a
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
mul_one : ∀ (a : α), a * 1 = a
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
one_mul : ∀ (a : α), 1 * a = a
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
zero_mul : ∀ (a : α), 0 * a = 0
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
mul_zero : ∀ (a : α), a * 0 = 0
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
pow_zero : ∀ (a : α), a ^ 0 = 1
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
pow_succ : ∀ (a : α) (n : Nat), a ^ (n + 1) = a ^ n * a
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
ofNat_succ : ∀ (a : Nat), OfNat.ofNat (a + 1) = OfNat.ofNat a + 1
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
ofNat_eq_natCast : ∀ (n : Nat), OfNat.ofNat n = ↑n
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
nsmul_eq_natCast_mul : ∀ (n : Nat) (a : α), n * a = ↑n * a
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
neg : α → α
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
sub : α → α → α
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
intCast : IntCast α
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
zsmul : HMul Int α α
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
neg_add_cancel : ∀ (a : α), -a + a = 0
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
neg_zsmul : ∀ (i : Int) (a : α), -i * a = -(i * a)
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
zsmul_natCast_eq_nsmul : ∀ (n : Nat) (a : α), ↑n * a = n * a
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
intCast_ofNat : ∀ (n : Nat), ↑(OfNat.ofNat n) = OfNat.ofNat n
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
intCast_neg : ∀ (i : Int), ↑(-i) = -↑i
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
mul_comm : ∀ (a b : α), a * b = b * a
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
inv : α → α
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
div : α → α → α
Inherited from
  1. Lean.Grind.CommRing α
  2. Inv α
  3. Div α
zpow : HPow α Int α
div_eq_mul_inv : ∀ (a b : α), a / b = a * b⁻¹

Division is multiplication by the inverse.

zero_ne_one : 0 ≠ 1

Zero is not equal to one: fields are non trivial.

inv_zero : 0⁻¹ = 0

The inverse of zero is zero. This is a "junk value" convention.

mul_inv_cancel : ∀ {a : α}, a ≠ 0 → a * a⁻¹ = 1

The inverse of a non-zero element is a right inverse.

zpow_zero : ∀ (a : α), a ^ 0 = 1

The zeroth power of any element is one.

zpow_succ : ∀ (a : α) (n : Nat), a ^ (↑n + 1) = a ^ ↑n * a

The (n+1)-st power of any element is the element multiplied by the n-th power.

zpow_neg : ∀ (a : α) (n : Int), a ^ (-n) = (a ^ n)⁻¹

Raising to a negative power is the inverse of raising to the positive power.

17.7.1.2. Ring Characteristics

🔗type class
Lean.Grind.IsCharP.{u} (α : Type u) [Lean.Grind.Semiring α]
  (p : outParam Nat) : Prop
Lean.Grind.IsCharP.{u} (α : Type u)
  [Lean.Grind.Semiring α]
  (p : outParam Nat) : Prop

A ring α has characteristic p if OfNat.ofNat x = 0 iff x % p = 0.

Note that for p = 0, we have x % p = x, so this says that OfNat.ofNat is injective from Nat to α.

In the case of a semiring, we take the stronger condition that OfNat.ofNat x = OfNat.ofNat y iff x % p = y % p.

Instance Constructor

Lean.Grind.IsCharP.mk.{u}

Methods

ofNat_ext_iff : ∀ {x y : Nat}, OfNat.ofNat x = OfNat.ofNat y ↔ x % p = y % p

Two numerals in a semiring are equal iff they are congruent module p in the natural numbers.

17.7.1.3. Natural Number Zero Divisors🔗

The class NoNatZeroDivisors is used to control coefficient growth. For example, the polynomial 2 * x * y + 4 * z = 0 is simplified to x * y + 2 * z = 0. It also used when processing disequalities.

Using NoNatZeroDivisors

In this example, grind relies on the NoNatZeroDivisors instance to simplify the goal:

example [CommRing α] [NoNatZeroDivisors α] (a b : α) : 2 * a + 2 * b = 0 → b ≠ -a → False := α:Type u_1inst✝¹:CommRing αinst✝:NoNatZeroDivisors αa:αb:α⊢ 2 * a + 2 * b = 0 → b ≠ -a → False All goals completed! 🐙

Without it, the proof fails:

example [CommRing α] (a b : α) : 2 * a + 2 * b = 0 → b ≠ -a → False := α:Type u_1inst✝:CommRing αa:αb:α⊢ 2 * a + 2 * b = 0 → b ≠ -a → False `grind` failed α:Type u_1inst:CommRing αa b:αh:2 * a + 2 * b = 0h_1:¬b = -a⊢ False
[grind] Goal diagnostics
  • [facts] Asserted facts
  • [eqc] False propositions
    • [prop] b = -a
  • [eqc] Equivalence classes
    • [eqc] {0, 2 * a + 2 * b}
  • [ring] Ring `α`
    • [basis] Basis
      • [_] 2 * a + 2 * b = 0
    • [diseqs] Disequalities
α:Type u_1inst✝:CommRing αa:αb:α⊢ 2 * a + 2 * b = 0 → b ≠ -a → False 
`grind` failed
α:Type u_1inst:CommRing αa b:αh:2 * a + 2 * b = 0h_1:¬b = -a⊢ False

[grind] Goal diagnostics
  • [facts] Asserted facts
  • [eqc] False propositions
    • [prop] b = -a
  • [eqc] Equivalence classes
    • [eqc] {0, 2 * a + 2 * b}
  • [ring] Ring `α`
    • [basis] Basis
      • [_] 2 * a + 2 * b = 0
    • [diseqs] Disequalities
🔗type class
Lean.Grind.NoNatZeroDivisors.{u} (α : Type u) [Lean.Grind.NatModule α] :
  Prop
Lean.Grind.NoNatZeroDivisors.{u}
  (α : Type u) [Lean.Grind.NatModule α] :
  Prop

We say a module has no natural number zero divisors if k ≠ 0 and k * a = k * b implies a = b (here k is a natural number and a and b are element of the module).

For a module over the integers this is equivalent to k ≠ 0 and k * a = 0 implies a = 0. (See the alternative constructor NoNatZeroDivisors.mk', and the theorem eq_zero_of_mul_eq_zero.)

Instance Constructor

Lean.Grind.NoNatZeroDivisors.mk.{u}

Methods

no_nat_zero_divisors : ∀ (k : Nat) (a b : α), k ≠ 0 → k * a = k * b → a = b

If k * a ≠ k * b then k ≠ 0 or a ≠ b.

🔗def
Lean.Grind.NoNatZeroDivisors.mk'.{u_1} {α : Type u_1}
  [Lean.Grind.IntModule α]
  (eq_zero_of_mul_eq_zero :
    ∀ (k : Nat) (a : α), k ≠ 0 → k * a = 0 → a = 0) :
  Lean.Grind.NoNatZeroDivisors α
Lean.Grind.NoNatZeroDivisors.mk'.{u_1}
  {α : Type u_1} [Lean.Grind.IntModule α]
  (eq_zero_of_mul_eq_zero :
    ∀ (k : Nat) (a : α),
      k ≠ 0 → k * a = 0 → a = 0) :
  Lean.Grind.NoNatZeroDivisors α

Alternative constructor for NoNatZeroDivisors when we have an IntModule.

The ring module also performs case-analysis for terms a⁻¹ on whether a is zero or not. In the following example, if 2*a is zero, then a is also zero since we have NoNatZeroDivisors α, and all terms are zero and the equality hold. Otherwise, ring adds the equalities a*a⁻¹ = 1 and 2*a*(2*a)⁻¹ = 1, and closes the goal.

example [Field α] [NoNatZeroDivisors α] (a : α) : 1 / a + 1 / (2 * a) = 3 / (2 * a) := α:Type u_1inst✝¹:Field αinst✝:NoNatZeroDivisors αa:α⊢ 1 / a + 1 / (2 * a) = 3 / (2 * a) All goals completed! 🐙

Without NoNatZeroDivisors, grind will perform case splits on numerals being zero as needed:

example [Field α] (a : α) : (2 * a)⁻¹ = a⁻¹ / 2 := α:Type u_1inst✝:Field αa:α⊢ (2 * a)⁻¹ = a⁻¹ / 2 All goals completed! 🐙

In the following example, ring does not need to perform any case split because the goal contains the disequalities y ≠ 0 and w ≠ 0.

example [Field α] {x y z w : α} : x / y = z / w → y ≠ 0 → w ≠ 0 → x * w = z * y := α:Type u_1inst✝:Field αx:αy:αz:αw:α⊢ x / y = z / w → y ≠ 0 → w ≠ 0 → x * w = z * y All goals completed! 🐙

You can disable the ring solver using the option grind -ring.

example [CommRing α] (x y : α) : x ^ 2 * y = 1 → x * y ^ 2 = y → y * x = 1 := α:Type u_1inst✝:CommRing αx:αy:α⊢ x ^ 2 * y = 1 → x * y ^ 2 = y → y * x = 1 `grind` failed α:Type u_1inst:CommRing αx y:αh:x ^ 2 * y = 1h_1:x * y ^ 2 = yh_2:¬y * x = 1⊢ False
[grind] Goal diagnostics
  • [facts] Asserted facts
    • [prop] x ^ 2 * y = 1
    • [prop] x * y ^ 2 = y
    • [prop] ¬y * x = 1
  • [eqc] False propositions
    • [prop] y * x = 1
  • [eqc] Equivalence classes
    • [eqc] {y, x * y ^ 2}
    • [eqc] {1, x ^ 2 * y}
  • [linarith] Linarith assignment for `α`
    • [assign] x := 3
    • [assign] y := 4
    • [assign] 「x ^ 2」 := 2
    • [assign] 「y ^ 2」 := 7
[grind] Issues
  • [issue] `grind linarith` term with unexpected instance y * x
α:Type u_1inst✝:CommRing αx:αy:α⊢ x ^ 2 * y = 1 → x * y ^ 2 = y → y * x = 1 
`grind` failed
α:Type u_1inst:CommRing αx y:αh:x ^ 2 * y = 1h_1:x * y ^ 2 = yh_2:¬y * x = 1⊢ False

[grind] Goal diagnostics
  • [facts] Asserted facts
    • [prop] x ^ 2 * y = 1
    • [prop] x * y ^ 2 = y
    • [prop] ¬y * x = 1
  • [eqc] False propositions
    • [prop] y * x = 1
  • [eqc] Equivalence classes
    • [eqc] {y, x * y ^ 2}
    • [eqc] {1, x ^ 2 * y}
  • [linarith] Linarith assignment for `α`
    • [assign] x := 3
    • [assign] y := 4
    • [assign] 「x ^ 2」 := 2
    • [assign] 「y ^ 2」 := 7


[grind] Issues
  • [issue] `grind linarith` term with unexpected instance
      y * x

17.7.1.3.1. Right-Cancellative Addition🔗

The ring solver automatically embeds CommSemirings into a CommRing envelope (using the construction Lean.Grind.Ring.OfSemiring.Q). However, the embedding is injective only when the CommSemiring implements the type class AddRightCancel. Nat is an example of a commutative semiring that implements AddRightCancel.

example (x y : Nat) : x ^ 2 * y = 1 → x * y ^ 2 = y → y * x = 1 := x:Naty:Nat⊢ x ^ 2 * y = 1 → x * y ^ 2 = y → y * x = 1 All goals completed! 🐙
🔗type class
Lean.Grind.AddRightCancel.{u} (M : Type u) [Add M] : Prop
Lean.Grind.AddRightCancel.{u} (M : Type u)
  [Add M] : Prop

A type where addition is right-cancellative, i.e. a + c = b + c implies a = b.

Instance Constructor

Lean.Grind.AddRightCancel.mk.{u}

Methods

add_right_cancel : ∀ (a b c : M), a + c = b + c → a = b

Addition is right-cancellative.

17.7.2. Resource Limits

Gröbner basis computation can be very expensive. You can limit the number of steps performed by the ring solver using the option grind (ringSteps := <num>)

Limiting ring Steps

This example cannot be solved by performing at most 100 steps:

example [CommRing α] [IsCharP α 0] (d t c : α) (d_inv PSO3_inv : α) : d ^ 2 * (d + t - d * t - 2) * (d + t + d * t) = 0 → -d ^ 4 * (d + t - d * t - 2) * (2 * d + 2 * d * t - 4 * d * t ^ 2 + 2 * d * t^4 + 2 * d^2 * t^4 - c * (d + t + d * t)) = 0 → d * d_inv = 1 → (d + t - d * t - 2) * PSO3_inv = 1 → t^2 = t + 1 := α:Type u_1inst✝¹:CommRing αinst✝:IsCharP α 0d:αt:αc:αd_inv:αPSO3_inv:α⊢ d ^ 2 * (d + t - d * t - 2) * (d + t + d * t) = 0 → -d ^ 4 * (d + t - d * t - 2) * (2 * d + 2 * d * t - 4 * d * t ^ 2 + 2 * d * t ^ 4 + 2 * d ^ 2 * t ^ 4 - c * (d + t + d * t)) = 0 → d * d_inv = 1 → (d + t - d * t - 2) * PSO3_inv = 1 → t ^ 2 = t + 1 `grind` failed α:Type u_1inst:CommRing αinst_1:IsCharP α 0d t c d_inv PSO3_inv:αh:d ^ 2 * (d + t - d * t - 2) * (d + t + d * t) = 0h_1:-d ^ 4 * (d + t - d * t - 2) * (2 * d + 2 * d * t - 4 * d * t ^ 2 + 2 * d * t ^ 4 + 2 * d ^ 2 * t ^ 4 - c * (d + t + d * t)) = 0h_2:d * d_inv = 1h_3:(d + t - d * t - 2) * PSO3_inv = 1h_4:¬t ^ 2 = t + 1⊢ False
[grind] Goal diagnostics
  • [facts] Asserted facts
  • [eqc] True propositions
  • [eqc] False propositions
    • [prop] t ^ 2 = t + 1
  • [eqc] Equivalence classes
  • [ring] Ring `α`
    • [basis] Basis
      • [_] t ^ 2 * d_inv + 2 * (t * d_inv ^ 2) + t ^ 2 + -1 * (d * d_inv) + t * d_inv + 2 * d_inv = 0
      • [_] 2 * (d_inv ^ 2 * PSO3_inv) + d_inv ^ 2 + 2 * (d_inv * PSO3_inv) + d_inv + -2 * PSO3_inv = 0
      • [_] d * t + -1 * (t * d_inv) + d + -1 = 0
      • [_] d * d_inv + -1 = 0
      • [_] t * d_inv + t + 1 = 0
      • [_] 2 * (d * PSO3_inv) + -2 * (d_inv * PSO3_inv) + -1 * d_inv + -2 * PSO3_inv + -1 = 0
      • [_] 2 * (t * PSO3_inv) + 2 * (d_inv * PSO3_inv) + d_inv = 0
    • [diseqs] Disequalities
  • [limits] Thresholds reached
    • [limit] maximum number of ring steps has been reached, threshold: `(ringSteps := 100)`
α:Type u_1inst✝¹:CommRing αinst✝:IsCharP α 0d:αt:αc:αd_inv:αPSO3_inv:α⊢ d ^ 2 * (d + t - d * t - 2) * (d + t + d * t) = 0 → -d ^ 4 * (d + t - d * t - 2) * (2 * d + 2 * d * t - 4 * d * t ^ 2 + 2 * d * t ^ 4 + 2 * d ^ 2 * t ^ 4 - c * (d + t + d * t)) = 0 → d * d_inv = 1 → (d + t - d * t - 2) * PSO3_inv = 1 → t ^ 2 = t + 1 
`grind` failed
α:Type u_1inst:CommRing αinst_1:IsCharP α 0d t c d_inv PSO3_inv:αh:d ^ 2 * (d + t - d * t - 2) * (d + t + d * t) = 0h_1:-d ^ 4 * (d + t - d * t - 2) *
    (2 * d + 2 * d * t - 4 * d * t ^ 2 + 2 * d * t ^ 4 + 2 * d ^ 2 * t ^ 4 - c * (d + t + d * t)) =
  0h_2:d * d_inv = 1h_3:(d + t - d * t - 2) * PSO3_inv = 1h_4:¬t ^ 2 = t + 1⊢ False

[grind] Goal diagnostics
  • [facts] Asserted facts
  • [eqc] True propositions
  • [eqc] False propositions
    • [prop] t ^ 2 = t + 1
  • [eqc] Equivalence classes
  • [ring] Ring `α`
    • [basis] Basis
      • [_] t ^ 2 * d_inv + 2 * (t * d_inv ^ 2) + t ^ 2 + -1 * (d * d_inv) + t * d_inv + 2 * d_inv = 0
      • [_] 2 * (d_inv ^ 2 * PSO3_inv) + d_inv ^ 2 + 2 * (d_inv * PSO3_inv) + d_inv + -2 * PSO3_inv = 0
      • [_] d * t + -1 * (t * d_inv) + d + -1 = 0
      • [_] d * d_inv + -1 = 0
      • [_] t * d_inv + t + 1 = 0
      • [_] 2 * (d * PSO3_inv) + -2 * (d_inv * PSO3_inv) + -1 * d_inv + -2 * PSO3_inv + -1 = 0
      • [_] 2 * (t * PSO3_inv) + 2 * (d_inv * PSO3_inv) + d_inv = 0
    • [diseqs] Disequalities
  • [limits] Thresholds reached
    • [limit] maximum number of ring steps has been reached, threshold: `(ringSteps := 100)`

The ring solver propagates equalities back to the grind core by normalizing terms using the computed Gröbner basis. In the following example, the equations x ^ 2 * y = 1 and x * y ^ 2 = y imply the equalities x = 1 and y = 1. Thus, the terms x * y and 1 are equal, and consequently some (x * y) = some 1 by congruence.

example (x y : Int) : x ^ 2 * y = 1 → x * y ^ 2 = y → some (y * x) = some 1 := x:Inty:Int⊢ x ^ 2 * y = 1 → x * y ^ 2 = y → some (y * x) = some 1 All goals completed! 🐙