16. grind策略
Tutorials
grind策略使用受现代 SMT 求解器启发的技术来自动构建证明。
它通过增量收集事实集、使用一组合作技术从现有事实中推导出新事实来生成证据。
在幕后，所有的证明都是通过反证法，所以预期的结论和前提之间不存在操作上的区别； grind 总是试图推导出矛盾。
想象一个虚拟白板。
每当 grind 发现新的等式、不等式或布尔文字时，它都会将该事实写入黑板上，将等效项合并到存储桶中，并邀请每个引擎从共享白板中读取并添加回共享白板。
特别是，由于所有真命题都等于 True，所有假命题都等于 False，因此 grind 跟踪一组已知事实作为跟踪等价类的一部分。
合作的引擎有：
与其他策略一样，grind 为其添加的每个事实生成普通的 Lean 证明条款。
Lean 的标准库已经用 @[grind] 属性进行了注释，因此会自动发现常见的引理。
grind 不是为搜索空间组合爆炸的目标而设计 - 想想大型 n 鸽子实例、图形着色减少、高阶 N 皇后板或编码为布尔约束的 200 变量数独。
此类编码需要数千（或数百万）次大小写分割，这会压垮 grind 的分支搜索。
对于位级或纯布尔组合问题，请使用 bv_decide。 bv_decide策略调用最先进的 SAT 求解器（例如 CaDiCaL 或 Kissat），然后返回紧凑的机器可检查证书。
所有大量搜索都发生在 Lean 之外；证书在 Lean 内重放和验证，因此保留了信任（验证时间随证书大小而变化）。
Congruence Closure
Algebraic Reasoning
该证明使用 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 := α: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
All goals completed! 🐙