16.9. 线性算术求解器🔗

grind 策略内置了一个面向任意类型的线性算术求解器 linarith，用于处理 cutsat 不支持的类型。和 ring 求解器一样，只要某个类型拥有若干类型类实例，就可以使用它。它会根据这些类型类实例的可用性自行配置，因此并不需要提供全部实例才能使用该求解器；不过，可用实例越多，它的能力也就越强。这个求解器适合用来推理实数、有序向量空间，以及其他无法嵌入到 Int 中的类型。

linarith 的核心功能，是一个用于处理整数系数线性不等式的基于模型的求解器。它可以用选项 grind -linarith 禁用。

由 linarith 判定的目标

下面这些例子都依赖于下列序关系记号以及 linarith 相关类型类的实例：

variable [LE α] [LT α] [Std.LawfulOrderLT α]  [Std.IsLinearOrder α]
variable [IntModule α] [OrderedAdd α]

整数模（IntModule）是带有零、加法、取负、减法以及整数标量乘法的类型，并满足这些运算应有的性质。线性序（Std.IsLinearOrder）要求任意两个元素都可比较，而 OrderedAdd 表示在不等式两边同时加上一个常量会保持序关系。

example {a b : α} : 2 • a + b ≥ b + a + a := byα:Type u_1inst✝⁵:LE αinst✝⁴:LT αinst✝³:Std.LawfulOrderLT αinst✝²:Std.IsLinearOrder αinst✝¹:IntModule αinst✝:OrderedAdd αa:αb:α⊢ 2 • a + b ≥ b + a + a grindAll goals completed! 🐙

example {a b : α} (h : a ≤ b) : 3 • a + b ≤ 4 • b := byα:Type u_1inst✝⁵:LE αinst✝⁴:LT αinst✝³:Std.LawfulOrderLT αinst✝²:Std.IsLinearOrder αinst✝¹:IntModule αinst✝:OrderedAdd αa:αb:αh:a ≤ b⊢ 3 • a + b ≤ 4 • b grindAll goals completed! 🐙

example {a b c : α} :
    a = b + c →
    2 • b ≤ c →
    2 • a ≤ 3 • c := byα:Type u_1inst✝⁵:LE αinst✝⁴:LT αinst✝³:Std.LawfulOrderLT αinst✝²:Std.IsLinearOrder αinst✝¹:IntModule αinst✝:OrderedAdd αa:αb:αc:α⊢ a = b + c → 2 • b ≤ c → 2 • a ≤ 3 • c
  grindAll goals completed! 🐙

example {a b c d e : α} :
    2 • a + b ≥ 0 →
    b ≥ 0 → c ≥ 0 → d ≥ 0 → e ≥ 0 →
    a ≥ 3 • c → c ≥ 6 • e → d - 5 • e ≥ 0 →
    a + b + 3 • c + d + 2 • e < 0 →
    False := byα:Type u_1inst✝⁵:LE αinst✝⁴:LT αinst✝³:Std.LawfulOrderLT αinst✝²:Std.IsLinearOrder αinst✝¹:IntModule αinst✝:OrderedAdd αa:αb:αc:αd:αe:α⊢ 2 • a + b ≥ 0 →
  b ≥ 0 → c ≥ 0 → d ≥ 0 → e ≥ 0 → a ≥ 3 • c → c ≥ 6 • e → d - 5 • e ≥ 0 → a + b + 3 • c + d + 2 • e < 0 → False
  grindAll goals completed! 🐙

在线查看 ↪

由 linarith 判定的交换环目标

对于带有 CommRing 实例的交换环类型（也就是乘法满足交换律的类型），linarith 具备更强的能力。

variable [LE R] [LT R] [Std.IsLinearOrder R] [Std.LawfulOrderLT R]
variable [CommRing R] [OrderedRing R]

CommRing R 实例允许 linarith 进行基础规范化，例如识别线性原子 a * b 与 b * a，并处理等式或不等式两边的标量乘法。 OrderedRing R 实例则让求解器能够支持常量，因为它可以利用 (0 : R) < 1 这一事实。

example (a b : R) (h : a * b ≤ 1) : b * 3 • a + 1 ≤ 4 := byR:Type u_1inst✝⁵:LE Rinst✝⁴:LT Rinst✝³:Std.IsLinearOrder Rinst✝²:Std.LawfulOrderLT Rinst✝¹:CommRing Rinst✝:OrderedRing Ra:Rb:Rh:a * b ≤ 1⊢ b * 3 • a + 1 ≤ 4 grindAll goals completed! 🐙

example (a b c d e f : R) :
    2 • a + b ≥ 1 →
    b ≥ 0 → c ≥ 0 → d ≥ 0 → e • f ≥ 0 →
    a ≥ 3 • c →
    c ≥ 6 • e • f → d - f * e * 5 ≥ 0 →
    a + b + 3 • c + d + 2 • e • f < 0 →
    False := byR:Type u_1inst✝⁵:LE Rinst✝⁴:LT Rinst✝³:Std.IsLinearOrder Rinst✝²:Std.LawfulOrderLT Rinst✝¹:CommRing Rinst✝:OrderedRing Ra:Rb:Rc:Rd:Re:Rf:R⊢ 2 • a + b ≥ 1 →
  b ≥ 0 →
    c ≥ 0 →
      d ≥ 0 → e • f ≥ 0 → a ≥ 3 • c → c ≥ 6 • e • f → d - f * e * 5 ≥ 0 → a + b + 3 • c + d + 2 • e • f < 0 → False
  grindAll goals completed! 🐙

在线查看 ↪

16.9.1. 支持 `linarith`🔗

若要让 linarith 支持一种新类型，第一步是在可能时实现 IntModule，否则实现 NatModule。每个 Ring 都已经是 IntModule，每个 Semiring 都已经是 NatModule，因此实现其中任一实例也已足够。接下来，还应实现某个序类型类（Std.IsPreorder、Std.IsPartialOrder 或 Std.IsLinearOrder）。通常来说，当上下文中已经包含矛盾时，IsPreorder 实例就够用；但若要证明线性不等式目标，则需要 IsLinearOrder 实例。此外，若实现 OrderedAdd（表达模的加法结构与序相容）以及 OrderedRing（改进对常量的支持），还可以启用更多功能。

类型类

Lean.Grind.NatModule.{u} (M : Type u) : Type u
Lean.Grind.NatModule.{u} (M : Type u) :
  Type u

自然数上的模，即配备零、加法和自然数标量乘法，并满足相应相容性条件的类型。

等价地说，它是加法交换幺半群。若该类型带有取负运算，请改用 IntModule。

实例构造子

Lean.Grind.NatModule.mk.{u}

扩展

AddCommMonoid M

方法

zero : M

继承自父结构。

add : M → M → M

继承自父结构。

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

继承自父结构。

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

继承自父结构。

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

继承自父结构。

nsmul : SMul Nat M

自然数标量乘法。

zero_nsmul : ∀ (a : M), 0 • a = 0

零的标量乘法为零。

add_one_nsmul : ∀ (n : Nat) (a : M), (n + 1) • a = n • a + a

后继数的标量乘法。

类型类

Lean.Grind.IntModule.{u} (M : Type u) : Type u
Lean.Grind.IntModule.{u} (M : Type u) :
  Type u

整数上的模，即配备零、加法、取负、减法和整数标量乘法，并满足相应相容性条件的类型。

等价地说，它是加法交换群。

实例构造子

Lean.Grind.IntModule.mk.{u}

扩展

AddCommGroup M

方法

zero : M

继承自父结构。

add : M → M → M

继承自父结构。

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

继承自父结构。

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

继承自父结构。

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

继承自父结构。

neg : M → M

继承自父结构。

sub : M → M → M

继承自父结构。

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

继承自父结构。

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

继承自父结构。

nsmul : SMul Nat M

自然数标量乘法。

zsmul : SMul Int M

整数标量乘法。

zero_zsmul : ∀ (a : M), 0 • a = 0

零的标量乘法为零。

one_zsmul : ∀ (a : M), 1 • a = a

一的标量乘法是恒等映射。

add_zsmul : ∀ (n m : Int) (a : M), (n + m) • a = n • a + m • a

标量乘法对整数加法满足分配律。

zsmul_natCast_eq_nsmul : ∀ (n : Nat) (a : M), ↑n • a = n • a

自然数标量乘法与整数标量乘法相容。

类型类

Lean.Grind.OrderedAdd.{u} (M : Type u) [HAdd M M M] [LE M]
  [Std.IsPreorder M] : Prop
Lean.Grind.OrderedAdd.{u} (M : Type u)
  [HAdd M M M] [LE M] [Std.IsPreorder M] :
  Prop

若 a ≤ b ↔ a + c ≤ b + c，则称加法与预序相容。

实例构造子

Lean.Grind.OrderedAdd.mk.{u}

方法

add_le_left_iff : ∀ {a b : M} (c : M), a ≤ b ↔ a + c ≤ b + c

a + c ≤ b + c 当且仅当 a ≤ b。

类型类

Lean.Grind.OrderedRing.{u} (R : Type u) [Semiring R] [LE R] [LT R]
  [Std.IsPreorder R] : Prop
Lean.Grind.OrderedRing.{u} (R : Type u)
  [Semiring R] [LE R] [LT R]
  [Std.IsPreorder R] : Prop

若一个环还配备预序，加法、取负和乘法均与该预序相容，并且 0 < 1，则称其为严格有序环。

实例构造子

Lean.Grind.OrderedRing.mk.{u}

扩展

OrderedAdd R

方法

add_le_left_iff : ∀ {a b : R} (c : R), a ≤ b ↔ a + c ≤ b + c

继承自父结构。

zero_lt_one : 0 < 1

在严格有序半环中，0 < 1。

mul_lt_mul_of_pos_left : ∀ {a b c : R}, a < b → 0 < c → c * a < c * b

在严格有序半环中，可用正元素 0 < c 从左侧乘不等式 a < b，得到 c * a < c * b。

mul_lt_mul_of_pos_right : ∀ {a b c : R}, a < b → 0 < c → a * c < b * c

在严格有序半环中，可用正元素 0 < c 从右侧乘不等式 a < b，得到 a * c < b * c。

16.9. 线性算术求解器🔗

16.9.1. 支持 linarith🔗

16.9.1. 支持 `linarith`🔗