Lean余归纳法

简介[编辑 | 编辑源代码]

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

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

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

余归纳类型[编辑 | 编辑源代码]

余归纳类型表示可能无限的数据结构。例如，一个无限流可以定义为：

codata Stream (α : Type) where
  head : α
  tail : Stream α

这里，`Stream α` 是一个无限序列，其中每个元素都有一个头部（`head`）和一个尾部（`tail`），后者是另一个 `Stream α`。

余递归函数[编辑 | 编辑源代码]

余递归函数是生成余归纳类型的函数。例如，生成一个无限常数流的函数：

def constStream (a : α) : Stream α :=
  { head := a,
    tail := constStream a }

注意，余递归函数不需要终止条件，因为它们生成的是无限结构。

余归纳原理[编辑 | 编辑源代码]

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

示例与应用[编辑 | 编辑源代码]

示例1：无限流[编辑 | 编辑源代码]

定义一个自然数的无限流：

def nats : Stream Nat :=
  { head := 0,
    tail := Stream.map (fun n => n + 1) nats }

这个流生成 `0, 1, 2, 3, ...`。

示例2：双模拟证明[编辑 | 编辑源代码]

证明两个流 `s1` 和 `s2` 相等，如果它们的头部相同且尾部满足双模拟关系：

theorem stream_eq (s1 s2 : Stream α)
  (hhead : s1.head = s2.head)
  (htail : stream_eq s1.tail s2.tail) :
  s1 = s2 :=
by coinduction; assumption

实际应用：进程代数[编辑 | 编辑源代码]

余归纳法常用于形式化验证中，例如验证并发系统的行为等价性。例如，定义两个进程 `P` 和 `Q` 的行为等价：

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