Lean证明模式

Lean证明模式

Lean证明模式是Lean定理证明器中进行数学证明的核心方法论，它通过结构化、可交互的方式将数学推理转化为计算机可验证的步骤。本章节将系统介绍Lean的证明构造范式、常用策略及其底层逻辑。

核心概念

在Lean中，证明被建模为目标导向的交互式过程，其工作流程遵循以下模式：

1. 目标状态（Goal State）：系统显示当前待证明的命题及假设环境 2. 策略应用（Tactic Application）：用户选择适当的证明策略推进证明 3. 状态转换（State Transition）：系统根据策略更新目标状态

graph TD A[初始命题] --> B{目标分解} B -->|应用策略| C[子目标1] B -->|应用策略| D[子目标2] C --> E[解决子目标] D --> F[解决子目标] E --> G[完成证明] F --> G

基础证明策略

直接构造法

通过精确给出证明项完成证明，适用于简单命题：

example : ∀ (P : Prop), P → P :=
fun (P : Prop) (h : P) => h  -- 直接构造蕴含证明

输出验证：

No goals left  -- 证明完成

策略模式证明

通过策略序列逐步构建证明，更接近数学家的思考方式：

theorem and_comm (P Q : Prop) : P ∧ Q → Q ∧ P :=
by
  intro h         -- 假设P ∧ Q成立
  cases h with    -- 分解合取假设
  | intro hp hq =>
    constructor  -- 构建目标合取式
    · exact hq   -- 证明第二个分量
    · exact hp   -- 证明第一个分量

高级证明模式

归纳证明

处理归纳数据类型时的标准模式：

inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

theorem add_zero (n : Nat) : n + Nat.zero = n := by
  induction n with
  | zero => simp
  | succ m ih =>   -- ih为归纳假设
    rw [Nat.add_succ]
    rw [ih]

等式重写

利用等式链进行证明的典型模式：

example (a b c : ℕ) : (a + b) * c = a * c + b * c := by
  rw [mul_add]  -- 应用乘法分配律

实际应用案例

案例：证明列表反转的幂等性

theorem rev_rev_id {α : Type} (l : List α) : l.reverse.reverse = l := by
  induction l with
  | nil => simp
  | cons h t ih =>
    rw [List.reverse_cons]
    rw [List.reverse_cons]
    rw [List.append_reverse]
    rw [ih]
    simp

证明结构分析： 1. 基础情况：空列表显然成立 2. 归纳步骤：

  - 分解列表为头元素和尾列表
  - 利用归纳假设处理尾列表
  - 通过列表操作引理完成重组

策略选择指南

常用策略的适用场景：

策略	适用场景	示例
intro	处理蕴含/全称命题	∀x, P x → Q x
cases	分解归纳类型	h : A ∨ B
induction	归纳数据类型	n : Nat
rw	应用等式重写	h : a = b
simp	自动化简化	算术表达式化简

数学符号表示

当处理复杂命题时，可能需要数学符号：

$⊢\mathrm{\forall }ϵ>0,\mathrm{\exists }N\in \mathbb{\mathbb{N}},\mathrm{\forall }n\ge N,|x_n-L|<ϵ$

对应的Lean编码：

example (x : ℕ → ℝ) (L : ℝ) :
  (∀ ε > 0, ∃ N, ∀ n ≥ N, |x n - L| < ε) → isLimit x L :=
by
  -- 证明内容省略

最佳实践建议

1. 增量证明：使用_占位符逐步构建证明 2. 目标可视化：频繁使用⊢符号检查当前目标 3. 策略组合：通过;组合策略提高效率 4. 模块化：将复杂证明分解为辅助引理

通过系统掌握这些证明模式，用户能够将数学思维有效转化为Lean可验证的证明结构，为形式化数学和程序验证奠定基础。