Lean证明调试
Lean证明调试是使用Lean定理证明器进行形式化验证时的重要技能。它涉及识别、诊断和修复证明过程中的错误，确保数学陈述或程序规范的逻辑正确性。本文将从基础概念到高级技巧，系统讲解Lean证明调试的核心方法。
概述[编辑 | 编辑源代码]
在Lean中，证明是一系列逻辑步骤的集合，由策略（tactics）构建。当证明失败时，系统会返回错误信息或无法关闭目标（goal）。调试过程通常包含以下阶段：
- 理解错误信息
- 检查当前证明状态（goal state）
- 定位逻辑漏洞或策略误用
- 修正策略序列或补充引理
基础调试技巧[编辑 | 编辑源代码]
1. 查看证明状态[编辑 | 编辑源代码]
使用show_term或show_goal命令查看当前目标：
example : ∀ n : ℕ, n + 0 = n :=
by
intro n
show_goal -- 显示当前目标：⊢ n + 0 = n
sorry
输出会显示未解决的子目标及其上下文。
2. 使用假设检查[编辑 | 编辑源代码]
assumption策略失败时，用print_assumptions查看可用假设：
example (h : p → q) (hp : p) : q :=
by
apply h
print_assumptions -- 显示可用的假设：[hp : p]
exact hp
3. 分步执行策略[编辑 | 编辑源代码]
通过·或{}分隔策略步骤，定位失败点：
example (x y : ℕ) : x + y = y + x :=
by
· rw [add_comm] -- 若失败，说明缺少导入或定义错误
· sorry
高级调试方法[编辑 | 编辑源代码]
1. 最小化复现代码[编辑 | 编辑源代码]
当遇到复杂错误时，尝试构建最小复现案例：
-- 原始错误证明
example (h : ∀ n, n > 0 → prime n) : prime 2 :=
by
apply h -- 错误：未能合成足够参数
norm_num
-- 最小复现
example : 2 > 0 := by norm_num -- 验证子目标是否可独立证明
2. 策略组合调试[编辑 | 编辑源代码]
使用try和repeat测试策略组合：
example : ¬ (∃ x, false) :=
by
repeat (try contradiction) -- 尝试多次应用策略
3. 元编程检查[编辑 | 编辑源代码]
通过#check和#eval验证表达式类型：
#check @add_comm -- 检查定理类型：∀ {α} [add_comm_monoid α] (a b : α), a + b = b + a
实际案例[编辑 | 编辑源代码]
案例1：归纳证明失败[编辑 | 编辑源代码]
以下归纳证明因缺少基础情形而失败：
theorem wrong_induction (n : ℕ) : n = 0 :=
by
induction n
· rfl -- 基础情形正确
· /- 失败：未处理归纳步骤 -/
调试步骤:
1. 观察错误提示"unsolved goals"
2. 添加show_goal发现缺失的归纳假设
3. 修正为完整证明：
theorem correct_induction (n : ℕ) : n = 0 :=
by
cases n -- 改用cases处理所有情形
· rfl
· contradiction
案例2：重写方向错误[编辑 | 编辑源代码]
example (a b : ℕ) (h : a = b) : b + 1 = a + 1 :=
by
rw [h] -- 错误：重写方向与目标不匹配
修正方法:
使用rw [←h]反向重写或simp_rw自动匹配方向。
可视化调试辅助[编辑 | 编辑源代码]
使用Mermaid展示证明状态流转：
数学公式支持[编辑 | 编辑源代码]
当调试涉及代数结构时，可能需要验证公式推导。例如环论中的分配律：
在Lean中对应的定理是mul_add，可通过#check @mul_add验证。
总结[编辑 | 编辑源代码]
Lean证明调试的核心在于：
- 系统性分解问题
- 利用交互式工具检查中间状态
- 通过最小案例验证猜想
- 理解策略的精确语义
掌握这些技能将显著提升形式化验证的效率和可靠性。