Lean证明重用[编辑 | 编辑源代码]

Lean证明重用是指在Lean定理证明器中通过已有证明构造新证明的技术，它通过复用已验证的逻辑片段提升开发效率。该技术体现了Lean作为交互式定理证明器的核心优势——允许用户构建模块化、可组合的数学证明。

核心概念[编辑 | 编辑源代码]

证明重用基于以下机制：

引理库：已证明的命题可作为新证明的构建块
策略组合：将简单证明策略组合成复杂证明流程
类型多态：通过泛型结构实现证明的通用性
命名空间：通过层次化命名管理可重用组件

基础示例[编辑 | 编辑源代码]

-- 已证明的引理
lemma reverse_reverse {α : Type} (xs : List α) : 
  reverse (reverse xs) = xs := by 
  induction xs <;> simp [*]

-- 重用证明构造新定理
theorem palindrome_reverse {α : Type} (xs : List α) :
  xs = reverse xs → reverse xs = xs := by
  intro h
  rw [← reverse_reverse xs]  -- 重用已有引理
  exact congr_arg reverse h  -- 应用函数一致性

输出推导过程：

假设 h : xs = reverse xs
目标：reverse xs = xs

步骤1：通过 reverse_reverse 得到 reverse (reverse xs) = xs
步骤2：用 h 改写目标 → reverse xs = reverse xs

高级重用技术[编辑 | 编辑源代码]

策略宏[编辑 | 编辑源代码]

创建可重用的证明策略片段：

macro "rew_rev" : tactic => 
  `(tactic| rw [← reverse_reverse _])

theorem reverse_injective {α : Type} (xs ys : List α) :
  reverse xs = reverse ys → xs = ys := by
  intro h
  rew_rev  -- 应用宏
  rew_rev at h
  exact h

类型类复用[编辑 | 编辑源代码]

通过类型类实现结构证明的自动继承：

class Commutative (op : α → α → α) where
  comm : ∀ a b, op a b = op b a

instance : Commutative Nat.add where
  comm := Nat.add_comm

-- 自动重用Commutative实例
example (a b : Nat) : a + b = b + a := 
  Commutative.comm a b

实际应用案例[编辑 | 编辑源代码]

案例：构建交换环证明库

通过分层证明重用： 1. 基础算术引理 → 2. 代数结构引理 → 3. 完整环理论

数学表示[编辑 | 编辑源代码]

证明重用的理论基础是证明项合成。给定两个证明： $p_{1} : ϕ_{1} \to ψ_{1}$
$p_{2} : ϕ_{2} \to ψ_{2}$ 当 $ψ_{1} \equiv ϕ_{2}$ 时可构造组合证明： $p_{2} \circ p_{1} : ϕ_{1} \to ψ_{2}$

最佳实践[编辑 | 编辑源代码]

模块化：将大证明分解为可独立验证的小引理
命名规范：使用描述性的引理名称
文档注释：用`/-- -/`说明引理的复用场景
类型参数化：尽可能使用多态定义

常见错误[编辑 | 编辑源代码]

页面模块:Message box/ambox.css没有内容。

lemma bad_cycle1 : A ↔ B := sorry
lemma bad_cycle2 : B ↔ A := bad_cycle1.symm  -- 逻辑正确但无实质进展

页面模块:Message box/ambox.css没有内容。

lemma length_reverse {α : Type} (L : List α) : 
  L.length = (reverse L).length := by 
  simp  -- 依赖环境中的reverse定义

进阶阅读方向[编辑 | 编辑源代码]

证明项元编程
公理化类型类
范畴论式证明组合
可判定性保持的证明变换