编辑“︁Lean战术组合”︁

{{DISPLAYTITLE:Lean战术组合}}

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

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

== 基础组合符号 ==
=== 顺序组合 (`>>`) ===
`tac1 >> tac2`表示先执行`tac1`，再在当前子目标上执行`tac2`。若`tac1`生成多个子目标，`tac2`仅作用于第一个子目标。

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

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

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

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

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

== 高级组合技术 ==
=== 条件组合 (`try`/`first`) ===
* `try tac`：执行`tac`，若失败则跳过而不报错。
* `first [tac1, tac2, ...]`：依次尝试列表中的战术，直到有一个成功。

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

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

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

== 实际案例 ==
=== 代数结构证明 ===
组合战术可简化环论性质的证明：

<syntaxhighlight lang="lean">
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)]  -- 定向重写
</syntaxhighlight>

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

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

== 可视化流程 ==
<mermaid>
graph TD
  A[开始证明] --> B[应用初始战术]
  B --> C{生成子目标?}
  C -->|是| D[并行处理子目标]
  C -->|否| E[完成]
  D --> F[组合战术嵌套]
  F --> C
</mermaid>

== 数学原理 ==
战术组合的理论基础是'''sequent calculus'''的派生规则组合。给定两个战术<math>t_1 \vdash \Gamma_1 \rightarrow \Delta_1</math>和<math>t_2 \vdash \Gamma_2 \rightarrow \Delta_2</math>，其组合<math>t_1 \circ t_2</math>的类型派生为：
<math>
\frac{t_1 \vdash \Gamma \rightarrow \Delta \quad t_2 \vdash \Delta \rightarrow \Theta}{t_1 \circ t_2 \vdash \Gamma \rightarrow \Theta}
</math>

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

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

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

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean高级证明技术]]