编辑“︁Lean余归纳法”︁

{{DISPLAYTITLE:Lean余归纳法}}

== 简介 ==
'''余归纳法'''（Coinduction）是 Lean 证明辅助工具中一种强大的技术，用于处理无限数据结构或行为。与归纳法（Induction）不同，余归纳法关注的是'''最大不动点'''（greatest fixed point）而非最小不动点（least fixed point）。它特别适用于定义和证明关于'''无限流'''（infinite streams）、'''共递归函数'''（corecursive functions）和'''行为等价性'''（behavioral equivalence）的性质。

在 Lean 中，余归纳法通过关键字 `codata` 或 `coinductive` 定义类型，并使用模式匹配和余递归（corecursion）来操作这些类型。

== 核心概念 ==

=== 余归纳类型 ===
余归纳类型表示可能无限的数据结构。例如，一个无限流可以定义为：
<syntaxhighlight lang="lean">
codata Stream (α : Type) where
  head : α
  tail : Stream α
</syntaxhighlight>
这里，`Stream α` 是一个无限序列，其中每个元素都有一个头部（`head`）和一个尾部（`tail`），后者是另一个 `Stream α`。

=== 余递归函数 ===
余递归函数是生成余归纳类型的函数。例如，生成一个无限常数流的函数：
<syntaxhighlight lang="lean">
def constStream (a : α) : Stream α :=
  { head := a,
    tail := constStream a }
</syntaxhighlight>
注意，余递归函数不需要终止条件，因为它们生成的是无限结构。

=== 余归纳原理 ===
余归纳法的证明原理基于'''双模拟'''（bisimulation）。要证明两个余归纳类型的实例相等，通常需要展示它们满足某种双模拟关系。

== 示例与应用 ==

=== 示例1：无限流 ===
定义一个自然数的无限流：
<syntaxhighlight lang="lean">
def nats : Stream Nat :=
  { head := 0,
    tail := Stream.map (fun n => n + 1) nats }
</syntaxhighlight>
这个流生成 `0, 1, 2, 3, ...`。

=== 示例2：双模拟证明 ===
证明两个流 `s1` 和 `s2` 相等，如果它们的头部相同且尾部满足双模拟关系：
<syntaxhighlight lang="lean">
theorem stream_eq (s1 s2 : Stream α)
  (hhead : s1.head = s2.head)
  (htail : stream_eq s1.tail s2.tail) :
  s1 = s2 :=
by coinduction; assumption
</syntaxhighlight>

=== 实际应用：进程代数 ===
余归纳法常用于形式化验证中，例如验证并发系统的行为等价性。例如，定义两个进程 `P` 和 `Q` 的行为等价：
<syntaxhighlight lang="lean">
coinductive Bisimilar (P Q : Process) : Prop where
  | intro :
      (∀ a, P ↓ a → Q ↓ a) →
      (∀ a, Q ↓ a → P ↓ a) →
      (∀ P', P → P' → ∃ Q', Q → Q' ∧ Bisimilar P' Q') →
      (∀ Q', Q → Q' → ∃ P', P → P' ∧ Bisimilar P' Q') →
      Bisimilar P Q
</syntaxhighlight>
这里 `P ↓ a` 表示进程 `P` 可以执行动作 `a`，`P → P'` 表示 `P` 可以转移到 `P'`。

== 图表说明 ==
以下是一个双模拟关系的示意图：
<mermaid>
graph LR
    P1((P)) --a--> P2((P'))
    Q1((Q)) --a--> Q2((Q'))
    P1 -.-> Q1
    P2 -.-> Q2
</mermaid>
图中，`P` 和 `Q` 是双模拟的，如果它们可以匹配彼此的转移动作并保持双模拟关系。

== 数学基础 ==
余归纳法的数学基础是最大不动点理论。给定一个单调函数 `F`，其最大不动点 `νF` 满足：
<math>
\nu F = F(\nu F)
</math>
并且对于任何其他满足 `X ⊆ F(X)` 的集合 `X`，有 `X ⊆ νF`。

== 总结 ==
余归纳法是 Lean 中处理无限结构和行为等价性的重要工具。通过定义余归纳类型、余递归函数和双模拟关系，可以形式化并证明许多复杂的系统性质。初学者可以从简单的无限流开始，逐步掌握余归纳法的核心思想与应用技巧。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean高级证明技术]]