Lean引理与推论

Lean引理与推论

介绍

在Lean定理证明器中，引理（Lemma）和推论（Corollary）是两种重要的数学陈述形式，用于构建形式化证明。它们本质上是定理（Theorem）的特殊变体，但在使用场景和组织结构上有所不同：

• 引理通常是证明过程中辅助性的中间结果，用于分解复杂证明为更小的步骤
• 推论是从已证明定理中直接得出的次要结论，通常只需少量额外证明步骤

理解这两种结构对于构建良好的Lean证明体系至关重要，它们能帮助开发者：

• 提高证明的可读性和模块化程度
• 减少重复证明工作
• 构建层次化的数学知识体系

基本语法

在Lean中，引理和推论使用与定理相同的声明语法，只是关键字不同：

lemma 名称 (参数列表) : 命题 :=
证明项

corollary 名称 (参数列表) : 命题 :=
证明项

简单示例

考虑自然数加法的交换律证明：

-- 先证明一个引理作为辅助结果
lemma add_zero (n : ℕ) : n + 0 = n :=
by induction n; simp_all

-- 再证明另一个引理
lemma add_succ (m n : ℕ) : m + (n + 1) = (m + n) + 1 :=
by induction n; simp_all

-- 最后将引理组合成主要定理
theorem add_comm (m n : ℕ) : m + n = n + m :=
by induction n;
   simp [add_zero, add_succ, *]

-- 从定理得出一个推论
corollary add_comm_special (n : ℕ) : n + 1 = 1 + n :=
add_comm n 1

引理的深入应用

引理在大型证明中特别有用，可以将复杂证明分解为多个可管理的部分。以下是更复杂的例子：

-- 定义一个偶数的谓词
def even (n : ℕ) : Prop := ∃ k, n = 2 * k

-- 辅助引理1：偶数加偶数仍为偶数
lemma even_add_even {a b : ℕ} (ha : even a) (hb : even b) : even (a + b) :=
match ha, hb with
| ⟨k, hk⟩, ⟨l, hl⟩ => ⟨k + l, by rw [hk, hl]; ring⟩
end

-- 辅助引理2：偶数乘任何数仍为偶数
lemma even_mul {a b : ℕ} (ha : even a) : even (a * b) :=
match ha with
| ⟨k, hk⟩ => ⟨k * b, by rw [hk]; ring⟩
end

-- 主要定理：使用上述引理构建证明
theorem even_square_add_even_square (a b : ℕ) (ha : even a) (hb : even b) :
  even (a^2 + b^2) :=
even_add_even (even_mul ha) (even_mul hb)

推论的使用模式

推论通常用于从现有结果中派生出特殊情形或简化版本：

-- 先证明一个关于列表长度的定理
theorem length_append (l₁ l₂ : List α) :
  (l₁ ++ l₂).length = l₁.length + l₂.length :=
by induction l₁; simp [*, Nat.succ_add]

-- 得出一个特殊情形的推论
corollary length_append_single (l : List α) (a : α) :
  (l ++ [a]).length = l.length + 1 :=
by simp [length_append]

-- 另一个推论：空列表情形
corollary length_append_nil (l : List α) :
  (l ++ []).length = l.length :=
by simp [length_append]

组织结构最佳实践

良好的Lean项目通常会按以下结构组织证明：

graph TD A[基础定义] --> B[关键引理] B --> C[主要定理] C --> D[推论1] C --> E[推论2] B --> F[其他定理]

数学公式示例

当处理数学内容时，可能会用到公式表示。例如关于多项式次数的引理：

$\mathrm{deg}(f\cdot g)=\mathrm{deg}f+\mathrm{deg}g$

对应的Lean形式化：

lemma degree_mul {R : Type} [CommRing R] [NoZeroDivisors R]
  {f g : R[X]} (hf : f ≠ 0) (hg : g ≠ 0) :
  (f * g).degree = f.degree + g.degree := ...

实际应用案例

考虑实现一个安全的加密协议验证系统，我们需要证明某些属性：

-- 定义消息和加密函数
inductive Message
| plain : String → Message
| enc : Key → Message → Message

-- 辅助引理：加密不会改变消息长度
lemma enc_preserves_length (k : Key) (m : Message) :
  (enc k m).length = m.length :=
by cases m; simp [enc, length]

-- 主要安全属性定理
theorem no_length_leakage (k : Key) (m₁ m₂ : Message) :
  m₁.length = m₂.length → (enc k m₁).length = (enc k m₂).length :=
by intro h; simp [enc_preserves_length, h]

-- 实用推论：空消息加密后的长度
corollary enc_empty_length (k : Key) :
  (enc k (Message.plain "")).length = 0 :=
by simp [enc_preserves_length]

常见问题

Q: 何时应该使用引理而不是定理？ A: 当某个结果主要目的是辅助其他证明时使用引理，当它是独立重要结果时使用定理。

Q: 推论可以引用其他推论吗？ A: 可以，但要避免创建过长的依赖链，这会影响代码可维护性。

Q: 这些结构在策略证明和项证明中有区别吗？ A: 语法上无区别，但在项证明中可能更需要引理来构建复杂表达式。

总结

• 引理是证明过程中的构建块，用于分解复杂证明
• 推论是已有结果的直接应用或特例
• 良好的证明结构应该层次分明，使用引理和推论来组织逻辑
• 在Lean中，三者语法相同，区别主要在于使用意图和文档作用
• 合理使用这些结构可以大幅提高证明的可读性和可维护性