Lean简单证明示例[编辑 | 编辑源代码]

介绍[编辑 | 编辑源代码]

Lean简单证明示例是初学者理解Lean定理证明器核心逻辑的重要起点。本节将展示如何用Lean4进行基础数学命题的构造性证明，包括命题逻辑、等式推理和自然数运算。通过交互式证明（Tactic模式）和函数式证明（Term模式）两种风格，读者将掌握Lean证明的基本结构。

命题逻辑证明[编辑 | 编辑源代码]

合取（AND）的证明[编辑 | 编辑源代码]

证明命题 $P \land Q$ 需要同时提供 $P$ 和 $Q$ 的证明：

example : 2 + 2 = 4 ∧ 3 + 1 = 4 := by
  apply And.intro
  · rfl  -- 证明第一个命题
  · rfl  -- 证明第二个命题

输出效果：目标状态依次分解为两个子目标并自动验证。

析取（OR）的证明[编辑 | 编辑源代码]

证明 $P \lor Q$ 只需选择其中一侧：

example : 1 = 1 ∨ 2 = 3 := by
  apply Or.inl  -- 选择左侧分支
  rfl

等式推理[编辑 | 编辑源代码]

Lean使用等式编译器（Eq）进行链式证明：

example (a b : Nat) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by
  calc
    (a + b) ^ 2 = (a + b) * (a + b)       := by rw [pow_two]
              _ = a*(a+b) + b*(a+b)       := by rw [mul_add]
              _ = a^2 + a*b + (b*a + b^2) := by repeat rw [add_mul, mul_comm]
              _ = a^2 + 2*a*b + b^2       := by ring

关键步骤说明：

rw [thm] 用定理重写表达式
ring 自动处理环运算

自然数归纳法[编辑 | 编辑源代码]

通过递归实现数学归纳：

def sum_to_n (n : Nat) : Nat :=
  match n with
  | 0 => 0
  | k + 1 => (k + 1) + sum_to_n k

theorem gauss_sum (n : Nat) : 2 * sum_to_n n = n * (n + 1) := by
  induction n with
  | zero => simp [sum_to_n]
  | succ k ih =>
      rw [sum_to_n, mul_add, ih]
      ring

结构解析： 1. 基础情况（zero）：直接计算 2. 归纳步骤（succ）：假设命题对k成立（ih），证明对k+1成立

实际案例：列表反转[编辑 | 编辑源代码]

证明列表反转操作的特性：

theorem rev_rev_eq_self {α : Type} (L : List α) : L.reverse.reverse = L := by
  induction L with
  | nil => rfl
  | cons h t ih =>
      simp [List.reverse]
      rw [List.reverse_append, ih]
      simp [List.reverse]

战术分析：

simp 自动简化定义展开
rw 使用引理 reverse_append

可视化证明流程[编辑 | 编辑源代码]

用Mermaid展示归纳法证明结构：

进阶技巧[编辑 | 编辑源代码]

存在量词证明[编辑 | 编辑源代码]

构造存在性证据：

example : ∃ x : Nat, x + 2 = 5 := by
  use 3  -- 提供见证者
  rfl

否定命题证明[编辑 | 编辑源代码]

通过矛盾推导：

example (n : Nat) (h : n + 1 = 0) : False := by
  cases n
  · simp at h  -- 0 + 1 ≠ 0
  · simp at h  -- n.succ + 1 ≠ 0

常见问题[编辑 | 编辑源代码]

Q: 为什么rfl能解决简单等式？

 A: 它检查两边是否定义等价（syntactic equality）

Q: 如何选择归纳变量？

 A: 对递归定义的量（如Nat, List）进行归纳

总结[编辑 | 编辑源代码]

通过本文案例，我们观察到Lean证明的典型模式： 1. 分解目标：使用apply或intro 2. 逐步验证：通过rw/simp等战术 3. 结构归纳：处理递归数据类型 4. 自动化：利用ring/linarith等决策过程

掌握这些模式后，读者可进一步学习更复杂的依赖类型证明。