16.7. 线性整数算术🔗

线性整数算术求解器实现了一个针对线性整数算术的基于模型的判定过程。该求解器能够处理四类线性多项式约束（其中 p 是一个线性多项式）：

等式: p = 0
整除性: d ∣ p
不等式: p ≤ 0
不等关系: p ≠ 0

它对于线性整数算术是完备的，并且通过用 Int.ofNat 将自然数转换成整数，也支持自然数。对于其他能够嵌入到 Int 中的类型，可以通过提供 Lean.Grind.ToInt 的实例来增加支持。非线性项（例如 x * x）也是允许的，但会被表示为变量。此外，该求解器还能把信息传播回比喻意义上的 grind 白板，从而触发其他子系统进一步推进证明。默认情况下它是启用的；可以用标志 -lia 将其禁用。

线性整数算术示例

下面这些命题都可以用线性整数算术求解器证明。在第一个例子中，左边必定是 2 的倍数，因此不可能等于 5：

example {x y : Int} : 2 * x + 4 * y ≠ 5 := byx:Inty:Int⊢ 2 * x + 4 * y ≠ 5
  grindAll goals completed! 🐙

求解器支持混合使用等式与不等式：

example {x y : Int} :
    2 * x + 3 * y = 0 →
    1 ≤ x →
    y < 1 := byx:Inty:Int⊢ 2 * x + 3 * y = 0 → 1 ≤ x → y < 1
  grindAll goals completed! 🐙

它也支持线性的整除约束：

example (a b : Int) :
    2 ∣ a + 1 →
    2 ∣ b + a →
    ¬ 2 ∣ b + 2 * a := bya:Intb:Int⊢ 2 ∣ a + 1 → 2 ∣ b + a → ¬2 ∣ b + 2 * a
  grindAll goals completed! 🐙

如果没有 lia，grind 就无法证明该命题：

example (a b : Int) :
    2 ∣ a + 1 →
    2 ∣ b + a →
    ¬ 2 ∣ b + 2 * a := bya:Intb:Int⊢ 2 ∣ a + 1 → 2 ∣ b + a → ¬2 ∣ b + 2 * a
  `grind` failed
grinda b:Inth:2 ∣ a + 1h_1:2 ∣ a + bh_2:2 ∣ 2 * a + b⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] 2 ∣ a + 1
[prop] 2 ∣ a + b
[prop] 2 ∣ 2 * a + b
[eqc] True propositions
[prop] 2 ∣ a + b
[prop] 2 ∣ a + 1
[prop] 2 ∣ 2 * a + b
[ematch] E-matching patterns
[thm] Nat.dvd_mul_left_of_dvd: [@Dvd.dvd `[Nat] `[Nat.instDvd] #3 #2, @HMul.hMul `[Nat] `[Nat] `[Nat] `[instHMul] #0 #2]
[thm] Nat.dvd_mul_right_of_dvd: [@Dvd.dvd `[Nat] `[Nat.instDvd] #3 #2, @HMul.hMul `[Nat] `[Nat] `[Nat] `[instHMul] #2 #0]
[linarith] Linarith assignment for `Int`
[assign] a := 0
[assign] b := 0grind -liaAll goals completed! 🐙

`grind` failed
grinda b:Inth:2 ∣ a + 1h_1:2 ∣ a + bh_2:2 ∣ 2 * a + b⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] 2 ∣ a + 1
[prop] 2 ∣ a + b
[prop] 2 ∣ 2 * a + b
[eqc] True propositions
[prop] 2 ∣ a + b
[prop] 2 ∣ a + 1
[prop] 2 ∣ 2 * a + b
[ematch] E-matching patterns
[thm] Nat.dvd_mul_left_of_dvd: [@Dvd.dvd `[Nat] `[Nat.instDvd] #3 #2, @HMul.hMul `[Nat] `[Nat] `[Nat] `[instHMul] #0 #2]
[thm] Nat.dvd_mul_right_of_dvd: [@Dvd.dvd `[Nat] `[Nat.instDvd] #3 #2, @HMul.hMul `[Nat] `[Nat] `[Nat] `[instHMul] #2 #0]
[linarith] Linarith assignment for `Int`
[assign] a := 0
[assign] b := 0

在线查看 ↪

16.7.1. 有理数解🔗

该求解器对线性整数算术是完备的。不过，即使约束很少，搜索空间也可能迅速变得极大，而这个求解器并不是为大规模分类讨论而设计的。 grind 的 qlia 选项通过允许求解器接受有理数解来缩小搜索空间。使用该选项后，求解器通常会更快，但它就不再完备。

有理数解但无整数解

下面这个例子有有理数解，但没有整数解：

example {x y : Int} :
    27 ≤ 13 * x + 11 * y →
    13 * x + 11 * y ≤ 30 →
    -10 ≤ 9 * x - 7 * y →
    9 * x - 7 * y > 4 := byx:Inty:Int⊢ 27 ≤ 13 * x + 11 * y → 13 * x + 11 * y ≤ 30 → -10 ≤ 9 * x - 7 * y → 9 * x - 7 * y > 4
  grindAll goals completed! 🐙

由于它使用的是有理数解，因此在指定 +qlia 时，grind 无法驳倒目标的否定：

example {x y : Int} :
    27 ≤ 13 * x + 11 * y →
    13 * x + 11 * y ≤ 30 →
    -10 ≤ 9 * x - 7 * y →
    9 * x - 7 * y > 4 := byx:Inty:Int⊢ 27 ≤ 13 * x + 11 * y → 13 * x + 11 * y ≤ 30 → -10 ≤ 9 * x - 7 * y → 9 * x - 7 * y > 4
  `grind` failed
grindx y:Inth:-13 * x + -11 * y + 27 ≤ 0h_1:13 * x + 11 * y + -30 ≤ 0h_2:-9 * x + 7 * y + -10 ≤ 0h_3:9 * x + -7 * y + -4 ≤ 0⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] -13 * x + -11 * y + 27 ≤ 0
[prop] 13 * x + 11 * y + -30 ≤ 0
[prop] -9 * x + 7 * y + -10 ≤ 0
[prop] 9 * x + -7 * y + -4 ≤ 0
[eqc] True propositions
[prop] -9 * x + 7 * y + -10 ≤ 0
[prop] -13 * x + -11 * y + 27 ≤ 0
[prop] 9 * x + -7 * y + -4 ≤ 0
[prop] 13 * x + 11 * y + -30 ≤ 0
[cutsat] Assignment satisfying linear constraints
[assign] x := 62/117
[assign] y := 2grind +qliaAll goals completed! 🐙

`grind` failed
grindx y:Inth:-13 * x + -11 * y + 27 ≤ 0h_1:13 * x + 11 * y + -30 ≤ 0h_2:-9 * x + 7 * y + -10 ≤ 0h_3:9 * x + -7 * y + -4 ≤ 0⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] -13 * x + -11 * y + 27 ≤ 0
[prop] 13 * x + 11 * y + -30 ≤ 0
[prop] -9 * x + 7 * y + -10 ≤ 0
[prop] 9 * x + -7 * y + -4 ≤ 0
[eqc] True propositions
[prop] -9 * x + 7 * y + -10 ≤ 0
[prop] -13 * x + -11 * y + 27 ≤ 0
[prop] 9 * x + -7 * y + -4 ≤ 0
[prop] 13 * x + 11 * y + -30 ≤ 0
[cutsat] Assignment satisfying linear constraints
[assign] x := 62/117
[assign] y := 2

求解器构造出的有理模型，出现在目标诊断里的 Assignment satisfying linear constraints 一节中。

在线查看 ↪

16.7.2. 非线性约束🔗

该求解器目前并不真正求解非线性约束，而是把 x * x 这样的非线性项当作变量处理。

非线性项

线性整数算术求解器无法证明这个定理：

example (x : Int) : x * x ≥ 0 := byx:Int⊢ x * x ≥ 0
  `grind` failed
grindx:Inth:x * x + 1 ≤ 0⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] x * x + 1 ≤ 0
[eqc] True propositions
[prop] x * x + 1 ≤ 0
[ematch] E-matching patterns
[thm] Nat.pow_pos: [@HPow.hPow `[Nat] `[Nat] `[Nat] `[instHPow] #2 #1]
[thm] Nat.div_pow_of_pos: [@HPow.hPow `[Nat] `[Nat] `[Nat] `[instHPow] #2 #1]
[cutsat] Assignment satisfying linear constraints
[assign] x := 0
[assign] 「x ^ 2」 := -1grindAll goals completed! 🐙

`grind` failed
grindx:Inth:x * x + 1 ≤ 0⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] x * x + 1 ≤ 0
[eqc] True propositions
[prop] x * x + 1 ≤ 0
[ematch] E-matching patterns
[thm] Nat.pow_pos: [@HPow.hPow `[Nat] `[Nat] `[Nat] `[instHPow] #2 #1]
[thm] Nat.div_pow_of_pos: [@HPow.hPow `[Nat] `[Nat] `[Nat] `[instHPow] #2 #1]
[cutsat] Assignment satisfying linear constraints
[assign] x := 0
[assign] 「x ^ 2」 := -1

从线性整数算术求解器的视角来看，这等价于：

example {y : Int} (x : Int) : y ≥ 0 := byy:Intx:Int⊢ y ≥ 0
  `grind` failed
grindy x:Inth:y + 1 ≤ 0⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] y + 1 ≤ 0
[eqc] True propositions
[prop] y + 1 ≤ 0
[cutsat] Assignment satisfying linear constraints
[assign] y := -1
[assign] x := 2grindAll goals completed! 🐙

`grind` failed
grindx:Inth:x * x + 1 ≤ 0⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] x * x + 1 ≤ 0
[eqc] True propositions
[prop] x * x + 1 ≤ 0
[ematch] E-matching patterns
[thm] Nat.pow_pos: [@HPow.hPow `[Nat] `[Nat] `[Nat] `[instHPow] #2 #1]
[thm] Nat.div_pow_of_pos: [@HPow.hPow `[Nat] `[Nat] `[Nat] `[instHPow] #2 #1]
[cutsat] Assignment satisfying linear constraints
[assign] x := 0
[assign] 「x ^ 2」 := -1

这一点可以通过把选项 trace.grind.lia.assert 设为 true 看出来；这样会追踪求解器处理的所有约束。

example (x : Int) : x*x ≥ 0 := byx:Int⊢ x * x ≥ 0
  set_option trace.grind.lia.assert true in
  [grind.lia.assert] -1*「x ^ 2 + 1」 + 「x ^ 2」 + 1 = 0[grind.lia.assert] 「x ^ 2」 + 1 ≤ 0`grind` failed
grindx:Inth:x * x + 1 ≤ 0⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] x * x + 1 ≤ 0
[eqc] True propositions
[prop] x * x + 1 ≤ 0
[ematch] E-matching patterns
[thm] Nat.pow_pos: [@HPow.hPow `[Nat] `[Nat] `[Nat] `[instHPow] #2 #1]
[thm] Nat.div_pow_of_pos: [@HPow.hPow `[Nat] `[Nat] `[Nat] `[instHPow] #2 #1]
[cutsat] Assignment satisfying linear constraints
[assign] x := 0
[assign] 「x ^ 2」 := -1grindAll goals completed! 🐙

[grind.lia.assert] -1*「x ^ 2 + 1」 + 「x ^ 2」 + 1 = 0[grind.lia.assert] 「x ^ 2」 + 1 ≤ 0

在 「x ^ 2」 + 1 ≤ 0 中，项 x ^ 2 被“加引号”显示，以表明 x ^ 2 被当作一个变量处理。

16.7.3. 除法与模🔗

该求解器支持线性的除法与取模运算。

线性除法与取模

example (x y : Int) :
    x = y / 2 →
    y % 2 = 0 →
    y - 2 * x = 0 := byx:Inty:Int⊢ x = y / 2 → y % 2 = 0 → y - 2 * x = 0
  grindAll goals completed! 🐙

在线查看 ↪

16.7.4. 代数处理🔗

该求解器会对交换（半）环表达式做规范化。

交换（半）环规范化

交换环规范化使得下面这个目标可被证明：

example (a b : Nat)
    (h₁ : a + 1 ≠ a * b * a)
    (h₂ : a * a * b ≤ a + 1) :
    b * a ^ 2 < a + 1 := bya:Natb:Nath₁:a + 1 ≠ a * b * ah₂:a * a * b ≤ a + 1⊢ b * a ^ 2 < a + 1
  grindAll goals completed! 🐙

在线查看 ↪

16.7.5. 传播信息🔗

该求解器还实现了 基于模型的理论组合，这是一种把等式传播回共享白板的机制。这些新增的等式又可能进一步触发新的同余。基于模型的理论组合会扩大搜索空间；可以使用选项 grind -mbtc 将其禁用。

传播等式

在上面的例子里，线性不等式与不等关系蕴含 y = 0：

example (f : Int → Int) (x y : Int) :
    f x = 0 →
    0 ≤ y → y ≤ 1 → y ≠ 1 →
    f (x + y) = 0 := byf:Int → Intx:Inty:Int⊢ f x = 0 → 0 ≤ y → y ≤ 1 → y ≠ 1 → f (x + y) = 0
  grindAll goals completed! 🐙

因此 x = x + y，于是由同余得到 f x = f (x + y)。如果没有基于模型的理论组合，证明就会卡住：

example (f : Int → Int) (x y : Int) :
    f x = 0 →
    0 ≤ y → y ≤ 1 → y ≠ 1 →
    f (x + y) = 0 := byf:Int → Intx:Inty:Int⊢ f x = 0 → 0 ≤ y → y ≤ 1 → y ≠ 1 → f (x + y) = 0
  `grind` failed
grindf:Int → Intx y:Inth:f x = 0h_1:-1 * y ≤ 0h_2:y + -1 ≤ 0h_3:¬y = 1h_4:¬f (x + y) = 0⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] f x = 0
[prop] -1 * y ≤ 0
[prop] y + -1 ≤ 0
[prop] ¬y = 1
[prop] ¬f (x + y) = 0
[eqc] True propositions
[prop] y + -1 ≤ 0
[prop] -1 * y ≤ 0
[eqc] False propositions
[prop] y = 1
[prop] f (x + y) = 0
[eqc] Equivalence classes
[eqc] {f x, 0}
[cutsat] Assignment satisfying linear constraints
[assign] x := 0
[assign] y := 0
[assign] f x := 0
[assign] f (x + y) := 4
[ring] Ring `Int`
[diseqs] Disequalities
[_] ¬y + -1 = 0grind -mbtcAll goals completed! 🐙

`grind` failed
grindf:Int → Intx y:Inth:f x = 0h_1:-1 * y ≤ 0h_2:y + -1 ≤ 0h_3:¬y = 1h_4:¬f (x + y) = 0⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] f x = 0
[prop] -1 * y ≤ 0
[prop] y + -1 ≤ 0
[prop] ¬y = 1
[prop] ¬f (x + y) = 0
[eqc] True propositions
[prop] y + -1 ≤ 0
[prop] -1 * y ≤ 0
[eqc] False propositions
[prop] y = 1
[prop] f (x + y) = 0
[eqc] Equivalence classes
[eqc] {f x, 0}
[cutsat] Assignment satisfying linear constraints
[assign] x := 0
[assign] y := 0
[assign] f x := 0
[assign] f (x + y) := 4
[ring] Ring `Int`
[diseqs] Disequalities
[_] ¬y + -1 = 0

在线查看 ↪

16.7.6. 其他类型🔗

LIA 求解器也可以处理包含自然数的线性约束。它会使用 Int.ofNat 将其转换为整数约束。

作为线性整数算术的自然数

example (x y z : Nat) :
    x < y + z →
    y + 1 < z →
    z + x < 3 * z := byx:Naty:Natz:Nat⊢ x < y + z → y + 1 < z → z + x < 3 * z
  grindAll goals completed! 🐙

在线查看 ↪

通过 Lean.Grind.ToInt 类型类，有一种可扩展机制可以告诉求解器某个类型能够嵌入到整数中。借助这一机制，我们可以求解如下目标：

example (a b c : Fin 11) : a ≤ 2 → b ≤ 3 → c = a + b → c ≤ 5 := bya:Fin 11b:Fin 11c:Fin 11⊢ a ≤ 2 → b ≤ 3 → c = a + b → c ≤ 5
  grindAll goals completed! 🐙

example (a : Fin 2) : a ≠ 0 → a ≠ 1 → False := bya:Fin 2⊢ a ≠ 0 → a ≠ 1 → False
  grindAll goals completed! 🐙

example (a b c : UInt64) : a ≤ 2 → b ≤ 3 → c - a - b = 0 → c ≤ 5 := bya:UInt64b:UInt64c:UInt64⊢ a ≤ 2 → b ≤ 3 → c - a - b = 0 → c ≤ 5
  grindAll goals completed! 🐙

类型类

Lean.Grind.ToInt.{u} (α : Type u)
  (range : outParam Lean.Grind.IntInterval) : Type u
Lean.Grind.ToInt.{u} (α : Type u)
  (range :
    outParam Lean.Grind.IntInterval) :
  Type u

ToInt α I 表示可以将 α 忠实地嵌入整数区间 I。

实例构造子

Lean.Grind.ToInt.mk.{u}

方法

toInt : α → Int

嵌入函数。

toInt_inj : ∀ (x y : α), ↑x = ↑y → x = y

嵌入函数是单射。

toInt_mem : ∀ (x : α), ↑x ∈ range

嵌入函数的值落在指定区间内。

归纳类型

Lean.Grind.IntInterval : Type
Lean.Grind.IntInterval : Type

整数区间，可以是有限、半无限或无限区间。

构造子

Lean.Grind.IntInterval.co (lo hi : Int) :
  Lean.Grind.IntInterval

有限区间 [lo, hi)。

Lean.Grind.IntInterval.ci (lo : Int) :
  Lean.Grind.IntInterval

半无限区间 [lo, ∞)。

Lean.Grind.IntInterval.io (hi : Int) :
  Lean.Grind.IntInterval

半无限区间 (-∞, hi)。

Lean.Grind.IntInterval.ii : Lean.Grind.IntInterval

无限区间 (-∞, ∞)。

16.7.7. 实现说明🔗

线性整数算术求解器的实现受到了 Jovanović and de Moura (2023)Dejan Jovanović and Leonardo de Moura, 2023. “Cutting to the Chase: Solving Linear Integer Arithmetic”. In Automated Deduction: CADE '23. (LNCS 6803) 第 4 节的启发。与论文相比，它还包含若干增强与修改，例如：

扩展了约束支持（等式与不等关系），
对 Cooper-Left 规则进行了优化编码，使用一个“大”析取而不是新鲜变量，以及
对分类讨论中的决策变量进行跟踪（不等关系、Cooper-Left、Cooper-Right）。

该求解过程会逐步构造一个模型（也就是对项中变量的赋值），并通过生成约束来解决冲突。例如，给定部分模型 {x := 1} 和约束 3 ∣ 3 * y + x + 1：

求解器无法把该模型扩展到 y，因为 3 ∣ 3 * y + 2 不可满足。
因此，它会通过生成蕴含约束 3 ∣ x + 1 来消解冲突。
这个新约束迫使求解器为 x 寻找新的赋值。

在为变量 y 赋值时，求解器会考虑：

最佳的上界与下界（不等式）。
一个整除约束。
所有以 y 为最大变量的不等关系约束。

Cooper-Left 与 Cooper-Right 规则负责处理不等式与整除性的组合。对于不可满足的不等关系 p ≠ 0，求解器会生成如下分类讨论：p + 1 ≤ 0 ∨ -p + 1 ≤ 0。