Lean战术组合

介绍[编辑 | 编辑源代码]

Lean战术组合是Lean定理证明器中一种强大的证明构造技术，它允许用户通过组合多个基础战术（tactics）来构建复杂的证明策略。这种方法类似于函数式编程中的高阶函数组合，能够显著提升证明的模块化和复用性。对于初学者而言，理解战术组合是掌握Lean高效证明的关键步骤；对于高级用户，深度组合技巧能实现自动化证明工程。

在Lean中，战术是用于操作证明状态的基本指令（如`rw`、`simp`、`apply`等），而战术组合则是通过符号（如`<;>`、`>>`、`repeat`）或自定义策略将它们连接起来。组合后的战术会按特定顺序执行，并可能共享上下文信息。

基础组合符号[编辑 | 编辑源代码]

顺序组合 (`>>`)[编辑 | 编辑源代码]

`tac1 >> tac2`表示先执行`tac1`，再在当前子目标上执行`tac2`。若`tac1`生成多个子目标，`tac2`仅作用于第一个子目标。

example (h : p ∨ q) : q ∨ p := by
  cases h with
  | inl hp => apply Or.inr; exact hp  -- 顺序组合的隐式使用
  | inr hq => apply Or.inl; exact hq

并行组合 (`<;>`)[编辑 | 编辑源代码]

`tac1 <;> tac2`表示先执行`tac1`，然后对`tac1`生成的所有子目标执行`tac2`。这是全局作用域的战术应用。

example (x y : Nat) (h : x = y) : y = x := by
  rw [h] <;> rfl  -- 对`rw [h]`生成的所有目标（此处为1个）执行`rfl`

重复组合 (`repeat`)[编辑 | 编辑源代码]

`repeat tac`会重复执行`tac`直到失败，常用于批量处理相似子目标。

example (a b c : Nat) (h1 : a = b) (h2 : b = c) : a = c := by
  repeat rw [h1, h2]  -- 连续重写直到无法应用

高级组合技术[编辑 | 编辑源代码]

条件组合 (`try`/`first`)[编辑 | 编辑源代码]

`try tac`：执行`tac`，若失败则跳过而不报错。
`first [tac1, tac2, ...]`：依次尝试列表中的战术，直到有一个成功。

example (n : Nat) : n + 0 = n := by
  first
  | apply Nat.add_zero  -- 尝试第一个战术
  | simp               -- 若失败则尝试简化

自定义组合器[编辑 | 编辑源代码]

通过`tactic`关键字可定义新的组合器。例如，实现一个"深度优先"应用策略：

tactic "deep_apply" e:term : tactic =>
  focus (apply e <;> deep_apply e) <|> skip

实际案例[编辑 | 编辑源代码]

代数结构证明[编辑 | 编辑源代码]

组合战术可简化环论性质的证明：

example (R : Type) [Ring R] (a b : R) : (a + b)^2 = a^2 + 2*a*b + b^2 := by
  simp [pow_two]       -- 展开平方
  rw [mul_add, add_mul]  -- 分配律
  repeat rw [add_assoc]  -- 重组加法结合性
  conv => rhs; rw [← add_assoc, add_comm (a*b) (a*b)]  -- 定向重写

逻辑命题处理[编辑 | 编辑源代码]

自动化处理命题逻辑中的重复模式：

theorem and_comm (p q : Prop) : p ∧ q ↔ q ∧ p := by
  apply Iff.intro
  <;> (intro ⟨hp, hq⟩; exact ⟨hq, hp⟩)  -- 对两个方向并行处理

战术组合的理论基础是sequent calculus的派生规则组合。给定两个战术 $t_{1} ⊢ Γ_{1} \to Δ_{1}$ 和 $t_{2} ⊢ Γ_{2} \to Δ_{2}$ ，其组合 $t_{1} \circ t_{2}$ 的类型派生为： $\frac{t_{1} ⊢ Γ \to Δ t_{2} ⊢ Δ \to Θ}{t_{1} \circ t_{2} ⊢ Γ \to Θ}$

最佳实践[编辑 | 编辑源代码]

1. 优先使用`<;>：当需要对多个子目标统一处理时 2. 限制`repeat`深度：避免无限循环，可配合`try`使用 3. 模块化组合：将常用组合定义为自定义策略 4. 交互式调试：使用`_`占位符逐步构建组合

常见错误[编辑 | 编辑源代码]

过度组合：复杂组合难以调试，建议分步验证
忽略作用域：`>>`和`<;>`的作用目标差异
隐式依赖：组合战术可能共享未声明的假设

通过系统掌握战术组合，Lean用户可以将零散的战术转化为高效的证明管道，大幅提升形式化数学的效率。