The ring solver 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. 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 typeclasses, so not all need to be provided.
The capabilities of the algebraic solvers will of course degrade when some are not available.
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.
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.
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.)
The inverse of a non-zero element is a right inverse.
The Lean standard library contains the applicable instances for the types defined in core.
Mathlib is also pre-configured. For example, the Mathlib CommRing type class implements
the Lean.Grind.CommRing α to ensure the ring solver works out-of-the-box.
The following examples demonstrate goals that can be decided by the ring solver.
openLeanGrindexample[CommRingα](x:α):(x+1)*(x-1)=x^2-1:=α:Type u_1inst✝:CommRingαx:α⊢ (x+1)*(x-1)=x^2-1All goals completed! 🐙
-- The solver "knows" that `16*16 = 0` because the
-- ring characteristic is `256`.
example[CommRingα][IsCharPα256](x:α):(x+16)*(x-16)=x^2:=α:Type u_1inst✝¹:CommRingαinst✝:IsCharPα256x:α⊢ (x+16)*(x-16)=x^2All goals completed! 🐙
-- Types in the std library implement the appropriate type classes.
-- `UInt8` is a commutative ring with characteristic `256`.
example(x:UInt8):(x+16)*(x-16)=x^2:=x:UInt8⊢ (x+16)*(x-16)=x^2All goals completed! 🐙example[CommRingα](abc:α):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^4All goals completed! 🐙example[CommRingα](xy:α):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=1All goals completed! 🐙
-- `ring` proves that `a + 1 = 2 + a` is unsatisfiable because
-- the characteristic is known.
example[CommRingα][IsCharPα0](a:α):a+1=2+a→False:=α:Type u_1inst✝¹:CommRingαinst✝:IsCharPα0a:α⊢ a+1=2+a→FalseAll goals completed! 🐙
Even when the characteristic is not initially known, when grind discovers that n = 0 for some numeral n, it makes inferences about the charactistic:
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. In the following example,
if you remove the local instance [NoNatZeroDivisors α], the goal will not be solved.
The ring solver also has support for [Field α]. During preprocessing,
it rewrites the term a/b as a*b⁻¹. It also rewrites every disequality
p ≠ 0 as the equality p * p⁻¹ = 1. This transformation is essential to
prove the following example:
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 haveNoNatZeroDivisors α, 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.
You can disable the ring solver using the option grind -ring.
example[CommRingα](xy:α):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
case grind
α : Type u_1
inst : CommRing α
x y : α
h : x ^ 2 * y = 1
h_1 : x * y ^ 2 = y
h_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
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.
The type Nat is an example of such a commutative semiring implementing AddRightCancel.
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>)
example{α}[CommRingα][IsCharPα0](dtc:α)(d_invPSO3_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
-- This example cannot be solved by performing at most 100 steps
`grind` failed
case grind
α : Type u_1
inst : CommRing α
inst_1 : IsCharP α 0
d t c d_inv PSO3_inv : α
h : d ^ 2 * (d + t - d * t - 2) * (d + t + d * t) = 0
h_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)) =
0
h_2 : d * d_inv = 1
h_3 : (d + t - d * t - 2) * PSO3_inv = 1
h_4 : ¬t ^ 2 = t + 1
⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] IsCharP α 0
[prop] d ^ 2 * (d + t - d * t - 2) * (d + t + d * t) = 0
[prop] -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
[prop] d * d_inv = 1
[prop] (d + t - d * t - 2) * PSO3_inv = 1
[prop] ¬t ^ 2 = t + 1
[eqc] True propositions
[prop] IsCharP α 0
[eqc] False propositions
[prop] t ^ 2 = t + 1
[eqc] Equivalence classes
[eqc] {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)),
d ^ 2 * (d + t - d * t - 2) * (d + t + d * t)}
[eqc] {1, d * d_inv, (d + t - d * t - 2) * PSO3_inv}
[linarith] Linarith assignment for `α`
[assign] d := 4
[assign] t := 0
[assign] c := 33
[assign] d_inv := 34
[assign] PSO3_inv := 35
[assign] 「d ^ 2」 := 3
[assign] 「d ^ 4」 := 16
[assign] 「t ^ 2」 := 27
[assign] 「t ^ 4」 := 29
[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
[_] ¬t ^ 2 + -1 * t + -1 = 0
[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
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.
