16. `grind` 策略🔗

Tutorials

使用 grind 处理有序映射

grind 策略使用受现代 SMT 求解器启发的技术自动构造证明。它逐步收集事实集，并利用一组相互协作的技术从已有事实推导新事实，以此生成证明。在幕后，所有证明都使用反证法，因此在操作上预期结论与前提并无区别；grind 始终尝试导出矛盾。

想象一块虚拟白板。每当 grind 发现新的等式、不等式或布尔文字时，它都会把该事实写到白板上，将等价的项归入同一组，并让每个引擎从共享白板读取信息、再向其中添加信息。特别地，由于所有真命题都等于 True，所有假命题都等于 False，grind 在跟踪等价类的同时也跟踪一组已知事实。

相互协作的引擎包括：

同余闭包、
约束传播、
E‑匹配、
引导式情形分析，以及
一组卫星理论求解器，包括线性整数算术和交换环求解器。

与其他策略一样，grind 会为它添加的每个事实生成普通的 Lean 证明项。 Lean 标准库已经带有 @[grind] 属性标注，因此常用引理会被自动发现。

grind 并非为搜索空间发生组合爆炸的目标而设计，例如大 n 的鸽巢原理实例、图着色归约、高阶 N 皇后棋盘，或编码为布尔约束的 200 变量数独。这类编码需要成千上万（甚至数百万）次情形拆分，会压垮 grind 的分支搜索。对于位级或纯布尔组合问题，请使用 bv_decide。bv_decide 策略会调用先进的 SAT 求解器（例如 CaDiCaL 或 Kissat），然后返回紧凑且可由机器检查的证书。所有繁重搜索都在 Lean 外部进行；证书会在 Lean 内部重放并验证，因此仍然保持可信（验证时间随证书大小增长）。

同余闭包自动推理

这个证明使用同余闭包立即成功；同余闭包会发现由相等项组成的集合。

example (a b c : Nat) (h₁ : a = b) (h₂ : b = c) :
    a = c := bya:Natb:Natc:Nath₁:a = bh₂:b = c⊢ a = c
  grindAll goals completed! 🐙

在线查看 ↪

代数推理

这个证明使用 grind 的交换环求解器。

example [CommRing α] [NoNatZeroDivisors α] (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 := byα:Type u_1inst✝¹:CommRing αinst✝:NoNatZeroDivisors α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
  grindAll goals completed! 🐙

在线查看 ↪

有限域推理

Fin 上的算术运算会溢出：当结果超出界限时，会回绕到 0。 grind 可以利用这一事实证明如下定理：

example (x y : Fin 11) :
    x ^ 2 * y = 1 →
    x * y ^ 2 = y →
    y * x = 1 := byx:Fin 11y:Fin 11⊢ x ^ 2 * y = 1 → x * y ^ 2 = y → y * x = 1
  grindAll goals completed! 🐙

在线查看 ↪

结合情形分析的线性整数算术

example (x y : Int) :
    27 ≤ 11 * x + 13 * y →
    11 * x + 13 * y ≤ 45 →
    -10 ≤ 7 * x - 9 * y →
    7 * x - 9 * y ≤ 4 →
    False := byx:Inty:Int⊢ 27 ≤ 11 * x + 13 * y → 11 * x + 13 * y ≤ 45 → -10 ≤ 7 * x - 9 * y → 7 * x - 9 * y ≤ 4 → False
  grindAll goals completed! 🐙

在线查看 ↪

16. grind 策略🔗

Tutorials

16. `grind` 策略🔗