编辑“︁Lean证明调试”︁

{{DISPLAYTITLE:Lean证明调试}}  
'''Lean证明调试'''是使用Lean定理证明器进行形式化验证时的重要技能。它涉及识别、诊断和修复证明过程中的错误，确保数学陈述或程序规范的逻辑正确性。本文将从基础概念到高级技巧，系统讲解Lean证明调试的核心方法。

== 概述 ==  
在Lean中，证明是一系列逻辑步骤的集合，由策略（tactics）构建。当证明失败时，系统会返回错误信息或无法关闭目标（goal）。调试过程通常包含以下阶段：  
# 理解错误信息  
# 检查当前证明状态（goal state）  
# 定位逻辑漏洞或策略误用  
# 修正策略序列或补充引理  

== 基础调试技巧 ==  

=== 1. 查看证明状态 ===  
使用<code>show_term</code>或<code>show_goal</code>命令查看当前目标：  
<syntaxhighlight lang="lean">  
example : ∀ n : ℕ, n + 0 = n :=  
by  
  intro n  
  show_goal  -- 显示当前目标：⊢ n + 0 = n  
  sorry  
</syntaxhighlight>  

输出会显示未解决的子目标及其上下文。

=== 2. 使用假设检查 ===  
<code>assumption</code>策略失败时，用<code>print_assumptions</code>查看可用假设：  
<syntaxhighlight lang="lean">  
example (h : p → q) (hp : p) : q :=  
by  
  apply h  
  print_assumptions  -- 显示可用的假设：[hp : p]  
  exact hp  
</syntaxhighlight>  

=== 3. 分步执行策略 ===  
通过<code>·</code>或<code>{}</code>分隔策略步骤，定位失败点：  
<syntaxhighlight lang="lean">  
example (x y : ℕ) : x + y = y + x :=  
by  
  · rw [add_comm]  -- 若失败，说明缺少导入或定义错误  
  · sorry  
</syntaxhighlight>  

== 高级调试方法 ==  

=== 1. 最小化复现代码 ===  
当遇到复杂错误时，尝试构建最小复现案例：  
<syntaxhighlight lang="lean">  
-- 原始错误证明  
example (h : ∀ n, n > 0 → prime n) : prime 2 :=  
by  
  apply h  -- 错误：未能合成足够参数  
  norm_num  

-- 最小复现  
example : 2 > 0 := by norm_num  -- 验证子目标是否可独立证明  
</syntaxhighlight>  

=== 2. 策略组合调试 ===  
使用<code>try</code>和<code>repeat</code>测试策略组合：  
<syntaxhighlight lang="lean">  
example : ¬ (∃ x, false) :=  
by  
  repeat (try contradiction)  -- 尝试多次应用策略  
</syntaxhighlight>  

=== 3. 元编程检查 ===  
通过<code>#check</code>和<code>#eval</code>验证表达式类型：  
<syntaxhighlight lang="lean">  
#check @add_comm  -- 检查定理类型：∀ {α} [add_comm_monoid α] (a b : α), a + b = b + a  
</syntaxhighlight>  

== 实际案例 ==  

=== 案例1：归纳证明失败 ===  
以下归纳证明因缺少基础情形而失败：  
<syntaxhighlight lang="lean">  
theorem wrong_induction (n : ℕ) : n = 0 :=  
by  
  induction n  
  · rfl  -- 基础情形正确  
  · /- 失败：未处理归纳步骤 -/  
</syntaxhighlight>  

'''调试步骤''':  
1. 观察错误提示"unsolved goals"  
2. 添加<code>show_goal</code>发现缺失的归纳假设  
3. 修正为完整证明：  
<syntaxhighlight lang="lean">  
theorem correct_induction (n : ℕ) : n = 0 :=  
by  
  cases n  -- 改用cases处理所有情形  
  · rfl  
  · contradiction  
</syntaxhighlight>  

=== 案例2：重写方向错误 ===  
<syntaxhighlight lang="lean">  
example (a b : ℕ) (h : a = b) : b + 1 = a + 1 :=  
by  
  rw [h]  -- 错误：重写方向与目标不匹配  
</syntaxhighlight>  

'''修正方法''':  
使用<code>rw [←h]</code>反向重写或<code>simp_rw</code>自动匹配方向。

== 可视化调试辅助 ==  
使用Mermaid展示证明状态流转：  
<mermaid>  
graph LR  
  A[初始目标] --> B[应用策略1]  
  B --> C{策略成功?}  
  C -->|是| D[新子目标]  
  C -->|否| E[回溯并尝试策略2]  
</mermaid>  

== 数学公式支持 ==  
当调试涉及代数结构时，可能需要验证公式推导。例如环论中的分配律：  
<math>(a + b) \cdot c = a \cdot c + b \cdot c</math>  
在Lean中对应的定理是<code>mul_add</code>，可通过<code>#check @mul_add</code>验证。

== 总结 ==  
Lean证明调试的核心在于：  
* 系统性分解问题  
* 利用交互式工具检查中间状态  
* 通过最小案例验证猜想  
* 理解策略的精确语义  

掌握这些技能将显著提升形式化验证的效率和可靠性。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean证明基础]]