编辑“︁Lean证明调试”︁（章节）

== 实际案例 ==  

=== 案例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>自动匹配方向。