编辑“︁Lean基本战术”︁（章节）

= Lean基本战术 =

'''Lean基本战术'''是Lean定理证明器中最核心的工具集，它允许用户通过逐步转换目标状态来完成数学证明。这些战术（tactics）构成了交互式证明构建的基础框架，特别适用于函数式编程和依赖类型理论环境下的形式化验证。

== 核心概念 ==

在Lean中，'''战术'''是指令式的证明步骤，它们通过操作'''目标状态'''（由未解决的子目标组成的堆栈）来推进证明过程。每个战术会：
* 分解当前目标
* 修改假设环境
* 或直接解决目标

=== 目标状态结构 ===
目标状态通常表示为：
<math>
\Gamma \vdash ?T
</math>
其中：
* <math>\Gamma</math> 是当前上下文（已知假设的集合）
* <math>?T</math> 是待证明的目标类型

== 基础战术集 ==

以下是Lean 4中最常用的基础战术：

=== 1. `intro` ===
用于分解蕴含（→）或全称量词（∀）目标：
<syntaxhighlight lang="lean">
example : ∀ (n : Nat), n = n := by
  intro n  -- 将∀量词引入上下文
  /- 现在目标变为 ⊢ n = n -/
  rfl      -- 通过反射性证明
</syntaxhighlight>

=== 2. `apply` ===
反向推理：使用已知定理匹配当前目标：
<syntaxhighlight lang="lean">
theorem succ_inj : ∀ {a b : Nat}, Nat.succ a = Nat.succ b → a = b := sorry

example : Nat.succ 1 = Nat.succ 2 → 1 = 2 := by
  apply succ_inj  -- 将目标转换为 ⊢ Nat.succ 1 = Nat.succ 2
</syntaxhighlight>

=== 3. `exact` ===
当表达式完全匹配目标时直接完成证明：
<syntaxhighlight lang="lean">
example : 2 + 2 = 4 := by
  exact rfl  -- 2+2与4在定义上相等
</syntaxhighlight>

=== 4. `rw`（重写） ===
使用等式重写目标：
<syntaxhighlight lang="lean">
axiom double : ∀ n, n + n = 2 * n

example : 5 + 5 = 2 * 5 := by
  rw [double]  -- 将目标中的5+5替换为2*5
</syntaxhighlight>

== 战术组合 ==

战术可以通过多种方式组合：

=== 分号链式 ===
<syntaxhighlight lang="lean">
example (h : P → Q) (hp : P) : Q := by
  apply h; exact hp
</syntaxhighlight>

=== 战术块 ===
使用`<;>`操作符：
<syntaxhighlight lang="lean">
example : (∀ x, P x → Q x) → (∀ x, P x) → ∀ x, Q x := by
  intros h1 h2 x
  apply h1 <;> apply h2
</syntaxhighlight>

== 实际案例：自然数证明 ==

以下展示如何用基础战术证明自然数的简单性质：

<syntaxhighlight lang="lean">
theorem add_comm : ∀ (n m : Nat), n + m = m + n := by
  intro n m          -- 引入变量
  induction n        -- 对n进行归纳
  · rw [Nat.zero_add] -- 基本情况
    rw [Nat.add_zero]
  · rw [Nat.succ_add] -- 归纳步骤
    rw [n_ih]
    rw [Nat.add_succ]
</syntaxhighlight>

== 战术状态图 ==

使用mermaid展示典型证明流程：

<mermaid>
graph TD
    A[初始目标] --> B{是否可分解?}
    B -->|是| C[应用intro/induction]
    B -->|否| D{是否可应用定理?}
    D -->|是| E[apply]
    D -->|否| F{是否可重写?}
    F -->|是| G[rw]
    F -->|否| H[尝试其他策略]
    C --> I[新子目标]
    E --> I
    G --> I
    H --> I
    I --> J{是否解决?}
    J -->|否| B
</mermaid>

== 高级技巧 ==

对于进阶用户，可以组合使用这些基础战术：

=== 带条件的重写 ===
<syntaxhighlight lang="lean">
example (h : x = y) (f : Nat → Nat) : f x = f y := by
  rw [h]  -- 自动识别f的上下文应用
</syntaxhighlight>

=== 使用`have`引入中间引理 ===
<syntaxhighlight lang="lean">
example : (a + b) * (a + b) = a*a + 2*a*b + b*b := by
  have step1 : (a + b) * (a + b) = a*(a+b) + b*(a+b) := by rw [Nat.mul_add]
  rw [step1]
  /- 继续展开其他步骤 -/
</syntaxhighlight>

== 常见错误处理 ==

{| class="wikitable"
|+ 战术错误对照表
|-
! 错误类型 !! 现象 !! 解决方案
|-
| 类型不匹配 || `apply`失败 || 检查定理前提是否与目标一致
|-
| 未引入变量 || `intro`报错 || 确保目标是∀或→形式
|-
| 重写方向错误 || `rw`不改变目标 || 尝试`rw [←eq_expression]`反向重写
|}

== 延伸学习 ==

掌握基础战术后，可以进一步学习：
* 自动化战术（如`simp`、`omega`）
* 自定义战术宏
* 元编程战术组合

这些基础战术构成了Lean证明工程的基石，通过反复练习可以培养出高效的交互式证明思维模式。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean证明基础]]