16.7. 线性整数算术🔗

线性整数算术求解器实现了基于模型的线性整数算术决策过程。求解器可以处理四类线性多项式约束（其中 p 是线性多项式）：

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

它对于线性整数运算来说是完整的，并且通过使用Int.ofNat将它们转换为整数来支持自然数。可以通过 Lean.Grind.ToInt 的实例添加对可嵌入到 Int 中的其他类型的支持。允许使用非线性项（例如 x * x），并表示为变量。该求解器还能够将信息传播回隐喻的 grind 白板，这可以触发其他子系统的进一步进展。默认情况下是启用的；可以使用标志 -lia 禁用它

Examples of Linear Integer Arithmetic

所有这些陈述都可以使用线性整数算术求解器来证明。在第一个示例中，左侧必须是 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

Live ↪

16.7.1. 理性解决方案🔗

该求解器对于线性整数运算来说是完整的。然而，搜索可能会在约束很少的情况下变得巨大，但求解器并不是为执行大规模案例分析而设计的。 grind 的 qlia 选项通过指示求解器接受有理解来减少搜索空间。使用此选项，求解器可能会更快，但它并不完整。

Rational Solutions

以下示例有有理解，但没有整数解：

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 部分。

Live ↪

16.7.2. 非线性约束🔗

该求解器目前支持非线性约束，并将诸如 x * x 之类的非线性项视为变量。

Nonlinear Terms

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

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 在 「x ^ 2」 + 1 ≤ 0 中被“引用”，以指示 x ^ 2 被视为变量。

16.7.3. 除法和模数🔗

该求解器支持线性除法和模运算。

Linear Division and Modulo

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

Live ↪

16.7.4. 代数处理🔗

求解器规范交换（半）环表达式。

Commutative (Semi)ring Normalization

交换环归一化可以解决这个目标：

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

Live ↪

16.7.5. 传播信息🔗

该求解器还实现了 基于模型的理论组合，这是一种将等式传播回隐喻共享白板的机制。这些额外的等式反过来可能会引发新的同余。基于模型的理论组合增加了搜索空间的大小；可以使用选项 grind -mbtc 禁用它。

Propagating Equalities

在上面的例子中，线性不等式和不等式意味着 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

Live ↪

16.7.6. 其他类型🔗

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

Natural Numbers as Linear Integer Arithmetic

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

Live ↪

有一个可扩展的机制，通过 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! 🐙

type class

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 asserts that α can be embedded faithfully into an interval I in the integers.

Instance Constructor

Lean.Grind.ToInt.mk.{u}

Methods

toInt : α → Int

The embedding function.

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

The embedding function is injective.

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

The embedding function lands in the interval.

inductive type

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

An interval in the integers (either finite, half-infinite, or infinite).

Constructors

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

The finite interval [lo, hi).

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

The half-infinite interval [lo, ∞).

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

The half-infinite interval (-∞, hi).

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

The infinite interval (-∞, ∞).

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} and constraint 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。