编辑“︁Lean证明重用”︁

= Lean证明重用 =

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

== 核心概念 ==
证明重用基于以下机制：
* '''引理库'''：已证明的命题可作为新证明的构建块
* '''策略组合'''：将简单证明策略组合成复杂证明流程
* '''类型多态'''：通过泛型结构实现证明的通用性
* '''命名空间'''：通过层次化命名管理可重用组件

=== 基础示例 ===
<syntaxhighlight lang="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  -- 应用函数一致性
</syntaxhighlight>

输出推导过程：
<pre>
假设 h : xs = reverse xs
目标：reverse xs = xs

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

== 高级重用技术 ==

=== 策略宏 ===
创建可重用的证明策略片段：
<syntaxhighlight lang="lean">
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
</syntaxhighlight>

=== 类型类复用 ===
通过类型类实现结构证明的自动继承：
<syntaxhighlight lang="lean">
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
</syntaxhighlight>

== 实际应用案例 ==

'''案例：构建交换环证明库'''
<mermaid>
graph LR
    A[加法交换律] --> B[乘法分配律]
    C[乘法结合律] --> D[环公理系统]
    B --> D
    A --> D
</mermaid>

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

== 数学表示 ==
证明重用的理论基础是'''证明项合成'''。给定两个证明：
<math>p_1 : \phi_1 \rightarrow \psi_1</math><br>
<math>p_2 : \phi_2 \rightarrow \psi_2</math>
当<math>\psi_1 \equiv \phi_2</math>时可构造组合证明：
<math>p_2 \circ p_1 : \phi_1 \rightarrow \psi_2</math>

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

== 常见错误 ==
{{Warning|1=避免循环重用：}}
<syntaxhighlight lang="lean">
lemma bad_cycle1 : A ↔ B := sorry
lemma bad_cycle2 : B ↔ A := bad_cycle1.symm  -- 逻辑正确但无实质进展
</syntaxhighlight>

{{Warning|2=隐式假设风险：}}
<syntaxhighlight lang="lean">
lemma length_reverse {α : Type} (L : List α) : 
  L.length = (reverse L).length := by 
  simp  -- 依赖环境中的reverse定义
</syntaxhighlight>

== 进阶阅读方向 ==
* 证明项元编程
* 公理化类型类
* 范畴论式证明组合
* 可判定性保持的证明变换

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