编辑“︁Lean引理与推论”︁

= Lean引理与推论 =

== 介绍 ==

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

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

理解这两种结构对于构建良好的Lean证明体系至关重要，它们能帮助开发者：
* 提高证明的可读性和模块化程度
* 减少重复证明工作
* 构建层次化的数学知识体系

== 基本语法 ==

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

<syntaxhighlight lang="lean">
lemma 名称 (参数列表) : 命题 :=
证明项

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

=== 简单示例 ===

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

<syntaxhighlight lang="lean">
-- 先证明一个引理作为辅助结果
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
</syntaxhighlight>

== 引理的深入应用 ==

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

<syntaxhighlight lang="lean">
-- 定义一个偶数的谓词
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)
</syntaxhighlight>

== 推论的使用模式 ==

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

<syntaxhighlight lang="lean">
-- 先证明一个关于列表长度的定理
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]
</syntaxhighlight>

== 组织结构最佳实践 ==

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

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

== 数学公式示例 ==

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

<math>
\deg(f \cdot g) = \deg f + \deg g
</math>

对应的Lean形式化：

<syntaxhighlight lang="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 := ...
</syntaxhighlight>

== 实际应用案例 ==

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

<syntaxhighlight lang="lean">
-- 定义消息和加密函数
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]
</syntaxhighlight>

== 常见问题 ==

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

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

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

== 总结 ==

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

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