编辑“︁Lean战术系统”︁

{{DISPLAYTITLE:Lean战术系统}}
'''Lean战术系统'''是[[Lean定理证明器]]中用于构造形式化证明的核心工具集，它通过一系列自动化或半自动化的策略（tactics）帮助用户逐步完成数学命题的证明。本文将从基础概念到高级应用全面介绍Lean的战术系统，适合从初学者到需要深入理解该系统的程序员。

== 概述 ==
在Lean中，'''战术'''（tactic）是指令式的证明步骤，用于将当前目标分解为更简单的子目标或直接完成证明。战术系统的设计灵感来源于LCF（Logic for Computable Functions）的交互式证明范式，但通过元编程（metaprogramming）机制实现了高度可扩展性。

=== 核心特点 ===
* '''组合性'''：战术可通过运算符（如`<;>`、`>>`）组合成复杂策略。
* '''可逆性'''：部分战术（如`cases`、`induction`）会保留原始目标结构。
* '''元变量'''：允许暂未定义的中间步骤（通过`_`表示）。

== 基础战术 ==
以下是初学者必须掌握的6个核心战术：

=== `intro` ===
用于消除目标中的全称量词或蕴含前提：
<syntaxhighlight lang="lean">
example : ∀ (P Q : Prop), P → Q → P :=
begin
  intro P Q hP hQ,  -- 将命题变量和假设引入上下文
  exact hP          -- 直接使用假设P
end
</syntaxhighlight>

=== `apply` ===
反向应用已知定理：
<syntaxhighlight lang="lean">
lemma modus_ponens (P Q : Prop) (h1 : P → Q) (h2 : P) : Q :=
begin
  apply h1,  -- 目标Q变为证明P
  exact h2
end
</syntaxhighlight>

=== `rw`（重写） ===
基于等式或等价关系进行替换：
<syntaxhighlight lang="lean">
example (a b : ℕ) (h : a = b) : b = a :=
begin
  rw h,  -- 将b替换为a
  -- 目标变为a = a，自动通过refl解决
end
</syntaxhighlight>

== 中级战术 ==

=== `induction` ===
数学归纳法结构：
<syntaxhighlight lang="lean">
theorem add_zero (n : ℕ) : n + 0 = n :=
begin
  induction n with d hd,
  { refl },        -- 基础情况
  { simp [hd] }    -- 归纳步骤
end
</syntaxhighlight>

=== `simp` ===
自动化简化器，可配置规则集：
<syntaxhighlight lang="lean">
@[simp] lemma nil_append (xs : List α) : [] ++ xs = xs := rfl

example : [] ++ [1, 2] = [1, 2] :=
begin
  simp  -- 自动应用注册的simp规则
end
</syntaxhighlight>

== 高级战术组合 ==
通过战术组合实现非平凡证明：

=== 结构化证明 ===
<syntaxhighlight lang="lean">
theorem and_comm (P Q : Prop) : P ∧ Q → Q ∧ P :=
begin
  intro h,
  cases h with hp hq,  -- 分解合取式
  constructor,          -- 构建新的合取式
  { exact hq },         -- 第一个子目标
  { exact hp }          -- 第二个子目标
end
</syntaxhighlight>

=== 战术宏 ===
使用`<;>`进行并行目标处理：
<syntaxhighlight lang="lean">
example (n : ℕ) : 0 + n = n + 0 :=
begin
  induction n <;> simp [add_zero, zero_add]
  -- 自动处理基础情况和归纳步骤
end
</syntaxhighlight>

== 实际案例：斐波那契证明 ==
展示战术系统在具体数学证明中的应用：

<syntaxhighlight lang="lean">
def fib : ℕ → ℕ
| 0     := 0
| 1     := 1
| (n+2) := fib (n+1) + fib n

theorem fib_square (n : ℕ) : fib n * fib (n+1) < fib (n+2) ^ 2 :=
begin
  cases n with d,
  { simp [fib], norm_num },  -- 基础情况
  { induction d with k ih,
    { simp [fib], norm_num }, -- n=1情况
    { simp [fib, nat.succ_eq_add_one],
      rw [←pow_two, add_sq'],
      linarith } }            -- 线性算术战术
end
</syntaxhighlight>

== 战术执行流程 ==
通过Mermaid展示典型证明状态转换：

<mermaid>
graph TD
    A[初始目标] --> B{应用intro}
    B --> C[分解假设]
    C --> D{应用cases}
    D --> E[子目标1]
    D --> F[子目标2]
    E --> G[使用exact]
    F --> H[应用simp]
    G --> I[证毕]
    H --> I
</mermaid>

== 数学公式支持 ==
当需要表达复杂数学概念时：

<math>
\forall (n \in \mathbb{N}), \sum_{i=1}^n i = \frac{n(n+1)}{2}
</math>

对应Lean证明：
<syntaxhighlight lang="lean">
theorem sum_formula (n : ℕ) : ∑ i in finset.range n, i = n*(n-1)/2 :=
begin
  induction n with d hd,
  { simp },
  { rw [finset.sum_range_succ, hd],
    ring }  -- 环代数战术
end
</syntaxhighlight>

== 最佳实践 ==
* 优先使用`simp`而非手动`rw`简化已知结构
* 使用`try { tactic }`处理可选分支
* 通过`suffices`声明中间引理
* 利用`library_search`自动发现证明

== 常见问题 ==
{{Q&A
|question = 为什么`cases`后目标数量会增加？
|answer = 因为该战术会对数据类型的所有构造子进行分情况讨论，每个构造子生成一个独立子目标。
}}

{{Q&A
|question = 如何调试失败的战术应用？
|answer = 使用`show_term { tactic }`查看具体转换过程，或插入`trace_state`检查当前证明状态。
}}

== 扩展阅读 ==
* ''Theorem Proving in Lean'' - 官方教程中的战术章节
* ''Mathematics in Lean'' - 实战数学证明案例集
* ''Tactic Metaprogramming in Lean'' - 高级战术开发指南

[[Category:Lean证明基础]]
[[Category:定理证明]]

[[Category:计算机科学]]
[[Category:Lean]]