Lean基本战术

Lean基本战术

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

核心概念

在Lean中，战术是指令式的证明步骤，它们通过操作目标状态（由未解决的子目标组成的堆栈）来推进证明过程。每个战术会：

• 分解当前目标
• 修改假设环境
• 或直接解决目标

目标状态结构

目标状态通常表示为： $\mathrm{\Gamma }⊢?T$ 其中：

• $\mathrm{\Gamma }$ 是当前上下文（已知假设的集合）
• $?T$ 是待证明的目标类型

基础战术集

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

1. `intro`

用于分解蕴含（→）或全称量词（∀）目标：

example : ∀ (n : Nat), n = n := by
  intro n  -- 将∀量词引入上下文
  /- 现在目标变为 ⊢ n = n -/
  rfl      -- 通过反射性证明

2. `apply`

反向推理：使用已知定理匹配当前目标：

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

3. `exact`

当表达式完全匹配目标时直接完成证明：

example : 2 + 2 = 4 := by
  exact rfl  -- 2+2与4在定义上相等

4. `rw`（重写）

使用等式重写目标：

axiom double : ∀ n, n + n = 2 * n

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

战术组合

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

分号链式

example (h : P → Q) (hp : P) : Q := by
  apply h; exact hp

战术块

使用`<;>`操作符：

example : (∀ x, P x → Q x) → (∀ x, P x) → ∀ x, Q x := by
  intros h1 h2 x
  apply h1 <;> apply h2

实际案例：自然数证明

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

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]

战术状态图

使用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

高级技巧

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

带条件的重写

example (h : x = y) (f : Nat → Nat) : f x = f y := by
  rw [h]  -- 自动识别f的上下文应用

使用`have`引入中间引理

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]
  /- 继续展开其他步骤 -/

常见错误处理

战术错误对照表

错误类型	现象	解决方案
类型不匹配	`apply`失败	检查定理前提是否与目标一致
未引入变量	`intro`报错	确保目标是∀或→形式
重写方向错误	`rw`不改变目标	尝试`rw [←eq_expression]`反向重写

延伸学习

掌握基础战术后，可以进一步学习：

• 自动化战术（如`simp`、`omega`）
• 自定义战术宏
• 元编程战术组合

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