Lean简单证明示例
Lean简单证明示例[编辑 | 编辑源代码]
介绍[编辑 | 编辑源代码]
Lean简单证明示例是初学者理解Lean定理证明器核心逻辑的重要起点。本节将展示如何用Lean4进行基础数学命题的构造性证明，包括命题逻辑、等式推理和自然数运算。通过交互式证明（Tactic模式）和函数式证明（Term模式）两种风格，读者将掌握Lean证明的基本结构。
命题逻辑证明[编辑 | 编辑源代码]
合取（AND）的证明[编辑 | 编辑源代码]
证明命题 需要同时提供 和 的证明：
example : 2 + 2 = 4 ∧ 3 + 1 = 4 := by
apply And.intro
· rfl -- 证明第一个命题
· rfl -- 证明第二个命题
输出效果：目标状态依次分解为两个子目标并自动验证。
析取（OR）的证明[编辑 | 编辑源代码]
证明 只需选择其中一侧：
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等决策过程
掌握这些模式后，读者可进一步学习更复杂的依赖类型证明。