Lean 语言参考

16.8. 代数工作室（交换环、域）🔗

grind 中的 ring 求解器受到 Gröbner 基础计算过程和术语重写完成的启发。 它将多元多项式视为重写规则。 例如，多项式等式x * y + x - 2 = 0被视为重写规则x * y ↦ -x + 2。 它使用叠加来确保重写系统是汇合的。

以下示例演示了可由 ring 求解器决定的目标。 在这些示例中，Lean 和 Lean.Grind 命名空间处于打开状态：

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! 🐙
Live ↪
Ring Characteristics

求解器“知道”16*16 = 0，因为环特征（即，乘法恒等式与加法恒等式之和的最小副本数）是 256，它由 IsCharP 实例提供。

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! 🐙
Live ↪
Standard Library Types

解算器开箱即用地支持标准库中的类型。 UInt8 是具有特征 256 的交换环，因此具有 CommRing UInt8 和 IsCharP UInt8 256 的实例。

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

交换环的公理足以证明这些陈述。

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! 🐙
Live ↪
Characteristic Zero

ring 证明 a + 1 = 2 + a 不可满足，因为已知特性为 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! 🐙
Live ↪
Inferred Characteristic

即使最初不知道该特征，当 grind 发现 n = 0 对于某些数字 n 时，它也会对该特征做出推断：

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! 🐙
Live ↪

16.8.1. 解算器 Type 类🔗

用户可以通过提供以下 类型类 的实例（全部位于 Lean.Grind 命名空间中）来为自己的类型启用 ring 求解器：

代数求解器将根据这些实例的可用性进行自我配置，因此不需要提供所有实例。 当然，当某些代数求解器不可用时，代数求解器的功能将会降低。

Lean 标准库包含标准库中定义的类型的适用实例。 通过提供这些实例，其他库也可以启用 grind 的 ring 求解器。 例如，Mathlib CommRing 类型类实现 Lean.Grind.CommRing 以确保 ring 解算器开箱即用。

16.8.1.1. 代数结构🔗

为了启用代数求解器，类型应该具有求解器支持的最具体的可能代数结构的实例。 按照特异性递增的顺序，即 Semiring、Ring、CommSemiring、CommRing 和 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 : SMul 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

Multiplying by a numeral is consistently defined with respect to the canonical map from natural numbers.

🔗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 : SMul 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 : SMul 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 : SMul 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 : SMul 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 : SMul 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.

16.8.1.1.1. 领域🔗

ring 解算器还支持 Field。 如果 Field 实例可用，则求解器会将项 a / b 预处理为 a * b⁻¹。 它还将每个不等式 p ≠ 0 重写为等式 p * p⁻¹ = 1。

Fields and grind

此示例需要其 Field 实例：

example [Field α] (a : α) : a ^ 2 = 0 → a = 0 := α:Type u_1inst✝:Field αa:α⊢ a ^ 2 = 0 → a = 0 All goals completed! 🐙
Live ↪
🔗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 : SMul 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 : SMul 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 α

An exponentiation operator.

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.

16.8.1.2. 环特性🔗

🔗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.

16.8.1.3. 自然数零因数🔗

NoNatZeroDivisors 类用于控制系数增长。 例如，多项式 2 * x * y + 4 * z = 0 被简化为 x * y + 2 * z = 0。 在处理不平等时也使用它。

Using NoNatZeroDivisors

在此示例中，grind 依赖 NoNatZeroDivisors 实例来简化目标：

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! 🐙

没有它，证明就会失败：

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
All goals completed! 🐙 
`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
Live ↪
🔗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.

ring 模块还针对 a 是否为零执行项 a⁻¹ 的案例分析。 在以下示例中，如果 2*a 为零，则 a 也为零，因为 我们有 NoNatZeroDivisors α，所有项都为零并且等式成立。否则， ring 将等式 a*a⁻¹ = 1 和 2*a*(2*a)⁻¹ = 1 相加，并关闭目标。

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! 🐙

如果没有 NoNatZeroDivisors，grind 将根据需要对为零的数字执行大小写分割：

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

在以下示例中，ring 不需要执行任何大小写拆分，因为 目标包含不等式 y ≠ 0 和 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! 🐙

您可以使用选项 grind -ring 禁用 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}
  • [ematch] E-matching patterns
  • [linarith] Linarith assignment for `α`
    • [assign] x := 2
    • [assign] y := 3
    • [assign] 「x ^ 2」 := 4
    • [assign] 「y ^ 2」 := 6
All goals completed! 🐙 
`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}
  • [ematch] E-matching patterns
  • [linarith] Linarith assignment for `α`
    • [assign] x := 2
    • [assign] y := 3
    • [assign] 「x ^ 2」 := 4
    • [assign] 「y ^ 2」 := 6

16.8.1.3.1. 右抵消加法🔗

ring 解算器自动将 CommSemiring 嵌入到 CommRing 包络中（使用构造 Lean.Grind.Ring.OfSemiring.Q）。 但是，仅当 CommSemiring 实现类型类 AddRightCancel 时，嵌入才是单射的。 Nat 是实现 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.

16.8.2. 资源限制🔗

Gröbner 基础计算可能非常昂贵。您可以使用选项 grind (ringSteps := <num>) 限制 ring 求解器执行的步数

Limiting ring Steps

此示例无法通过最多执行 100 个步骤来解决：

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
  • [ematch] E-matching patterns
  • [ring] Ring `α`
    • [basis] Basis
      • [_] t ^ 2 * d_inv ^ 2 + -2 * (t * d_inv ^ 2) + -1 * t ^ 2 + -2 * d_inv + 1 = 0
      • [_] d * t ^ 2 + -1 * (t ^ 2 * d_inv) + 2 * (t * d_inv) + -1 * d + 2 = 0
      • [_] d * t * PSO3_inv + -1 * (d * PSO3_inv) + -1 * (t * PSO3_inv) + 2 * PSO3_inv + 1 = 0
      • [_] t * d_inv * PSO3_inv + -1 * (t * PSO3_inv) + -2 * (d_inv * PSO3_inv) + -1 * d_inv + PSO3_inv = 0
      • [_] d * d_inv + -1 = 0
    • [diseqs] Disequalities
  • [limits] Thresholds reached
    • [limit] maximum number of ring steps has been reached, threshold: `(ringSteps := 100)`
All goals completed! 🐙 
`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
  • [ematch] E-matching patterns
  • [ring] Ring `α`
    • [basis] Basis
      • [_] t ^ 2 * d_inv ^ 2 + -2 * (t * d_inv ^ 2) + -1 * t ^ 2 + -2 * d_inv + 1 = 0
      • [_] d * t ^ 2 + -1 * (t ^ 2 * d_inv) + 2 * (t * d_inv) + -1 * d + 2 = 0
      • [_] d * t * PSO3_inv + -1 * (d * PSO3_inv) + -1 * (t * PSO3_inv) + 2 * PSO3_inv + 1 = 0
      • [_] t * d_inv * PSO3_inv + -1 * (t * PSO3_inv) + -2 * (d_inv * PSO3_inv) + -1 * d_inv + PSO3_inv = 0
      • [_] d * d_inv + -1 = 0
    • [diseqs] Disequalities
  • [limits] Thresholds reached
    • [limit] maximum number of ring steps has been reached, threshold: `(ringSteps := 100)`
Live ↪

ring 求解器通过使用计算的 Gröbner 基对项进行归一化，将等式传播回 grind内核。 在以下示例中，方程 x ^ 2 * y = 1 和 x * y ^ 2 = y 意味着等式 x = 1 和 y = 1。 因此，术语 x * y 和 1 相等，因此 some (x * y) = some 1 同余。

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! 🐙