Lean证明风格指南

简介

在Lean中编写证明时，良好的风格不仅能提高代码可读性，还能帮助他人（或未来的自己）理解证明结构。Lean证明风格指南涵盖以下核心原则：

• **结构化**：使用缩进和空行划分逻辑块
• **可读性**：选择有意义的命名和注释
• **模块化**：通过小定理组合构建复杂证明
• **一致性**：遵循社区约定（如空格和括号使用）

基础风格规范

缩进与换行

Lean不强制缩进规则，但推荐以下风格：

  
-- 好的风格：使用2空格缩进  
theorem add_comm (a b : Nat) : a + b = b + a := by  
  induction a  
  · simp  
  · simp [add_succ, a_ih]  

-- 差的风格：无缩进  
theorem add_comm_bad (a b : Nat) : a + b = b + a := by  
induction a  
· simp  
· simp [add_succ, a_ih]

命名约定

| 类型 | 示例 | 说明 | |---------------|---------------------|-----------------------------| | 定理/引理 | `add_comm` | 小写加下划线 | | 类型类 | `Monoid` | 大驼峰 | | 假设变量 | `(h : P → Q)` | 使用`h`前缀表示假设 |

高级证明结构

战术块划分

使用`<;>`组合战术时，建议拆分复杂步骤：

  
theorem length_append (xs ys : List α) :  
  (xs ++ ys).length = xs.length + ys.length := by  
  induction xs  
  <;> simp [*, Nat.add_assoc]  -- 简单情况合并  
  -- 复杂情况应单独处理

依赖图可视化

对于大型证明，依赖关系可用Mermaid表示：

graph TD A[add_comm] --> B[add_assoc] A --> C[zero_add] B --> D[Nat.succ_inj]

实际案例

数学证明示例

  
-- 清晰命名的中间引理  
lemma aux_lemma (n : Nat) : 2 * n = n + n := by  
  induction n  
  · simp  
  · simp [Nat.succ_add, *]  

theorem even_double (n : Nat) : Even (2 * n) := by  
  rw [aux_lemma]  -- 显式引用引理  
  use n

编程验证示例

验证列表反转性质：

  
theorem rev_rev_id (xs : List α) :  
  xs.reverse.reverse = xs := by  
  induction xs  
  · simp  
  · simp [List.reverse_cons, *]  -- 保持每行一个主要战术

公式与类型标注

当需要明确类型时，使用完整标注： $⊢\mathrm{\forall }(n:\mathbb{\mathbb{N}}),\text{Even}(n)\to \mathrm{\exists }k,n=2\times k$

  
theorem even_def (n : Nat) : Even n ↔ ∃ k, n = 2 * k :=  
  ⟨fun h => h, fun ⟨k, hk⟩ => ⟨k, hk⟩⟩

常见反模式

• **过度缩写**：避免`by induction a; simp; simp [*]`这样的压缩写法
• **幽灵战术**：删除未实际使用的`have`语句
• **重复代码**：通过抽象共享模式减少冗余

总结

遵循风格指南能显著提升Lean证明的质量。关键要点：

1. 保持一致的缩进和命名
2. 分解大证明为小引理
3. 优先选择自解释的战术组合
4. 使用工具自动化检查（如Lake的格式化功能）