Lean战术系统

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

概述

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

核心特点

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

基础战术

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

`intro`

用于消除目标中的全称量词或蕴含前提：

example : ∀ (P Q : Prop), P → Q → P :=
begin
  intro P Q hP hQ,  -- 将命题变量和假设引入上下文
  exact hP          -- 直接使用假设P
end

`apply`

反向应用已知定理：

lemma modus_ponens (P Q : Prop) (h1 : P → Q) (h2 : P) : Q :=
begin
  apply h1,  -- 目标Q变为证明P
  exact h2
end

`rw`（重写）

基于等式或等价关系进行替换：

example (a b : ℕ) (h : a = b) : b = a :=
begin
  rw h,  -- 将b替换为a
  -- 目标变为a = a，自动通过refl解决
end

中级战术

`induction`

数学归纳法结构：

theorem add_zero (n : ℕ) : n + 0 = n :=
begin
  induction n with d hd,
  { refl },        -- 基础情况
  { simp [hd] }    -- 归纳步骤
end

`simp`

自动化简化器，可配置规则集：

@[simp] lemma nil_append (xs : List α) : [] ++ xs = xs := rfl

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

高级战术组合

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

结构化证明

theorem and_comm (P Q : Prop) : P ∧ Q → Q ∧ P :=
begin
  intro h,
  cases h with hp hq,  -- 分解合取式
  constructor,          -- 构建新的合取式
  { exact hq },         -- 第一个子目标
  { exact hp }          -- 第二个子目标
end

战术宏

使用`<;>`进行并行目标处理：

example (n : ℕ) : 0 + n = n + 0 :=
begin
  induction n <;> simp [add_zero, zero_add]
  -- 自动处理基础情况和归纳步骤
end

实际案例：斐波那契证明

展示战术系统在具体数学证明中的应用：

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

战术执行流程

通过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

数学公式支持

当需要表达复杂数学概念时：

$\mathrm{\forall }(n\in \mathbb{\mathbb{N}}),\sum _{i=1}^{n}i=\frac{n(n+1)}{2}$

对应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

最佳实践

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

扩展阅读

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