编辑“︁Lean归纳定义”︁

{{DISPLAYTITLE:Lean归纳定义}}

'''Lean归纳定义'''是[[Lean定理证明器]]中用于定义递归数据结构和递归函数的核心机制。它基于[[数学归纳法]]和[[类型论]]，允许用户通过指定基本情况和归纳步骤来构造自引用的数据类型或算法。

== 基本概念 ==

在[[类型论]]中，归纳定义用于构造[[归纳类型]]（Inductive Types），这些类型通过一组构造子（constructors）来定义。每个构造子可以看作是该类型的"生成规则"。

归纳定义的一般形式如下：

<syntaxhighlight lang="lean">
inductive TypeName where
| constructor₁ : ArgumentTypes → TypeName
| constructor₂ : ArgumentTypes → TypeName
...
| constructorₙ : ArgumentTypes → TypeName
</syntaxhighlight>

=== 简单示例：自然数 ===

最经典的归纳类型是自然数的定义：

<syntaxhighlight lang="lean">
inductive Nat where
| zero : Nat
| succ (n : Nat) : Nat
</syntaxhighlight>

这个定义说明：
* '''zero''' 是一个自然数（基本情况）
* 如果 '''n''' 是一个自然数，那么 '''succ n'''（n的后继）也是一个自然数（归纳步骤）

== 递归函数定义 ==

与归纳类型配套使用的是递归函数，通过'''pattern matching'''和递归调用来定义：

<syntaxhighlight lang="lean">
def add : Nat → Nat → Nat
| m, Nat.zero   => m
| m, Nat.succ n => Nat.succ (add m n)
</syntaxhighlight>

这个加法函数的定义展示了：
1. 基本情况：任何数加零等于它本身
2. 归纳步骤：m + succ n = succ (m + n)

== 结构归纳法 ==

Lean支持对归纳类型的结构进行归纳证明。例如证明加法交换律：

<syntaxhighlight lang="lean">
theorem add_comm (m n : Nat) : add m n = add n m := by
  induction n with
  | zero => simp [add]
  | succ n ih => 
    rw [add, ih]
    simp [add, Nat.succ_add]
</syntaxhighlight>

证明分为：
1. 基本情况：m + 0 = 0 + m
2. 归纳步骤：假设m + n = n + m（归纳假设），证明m + succ n = succ n + m

== 复杂归纳类型 ==

=== 列表类型 ===

列表是另一个常见的归纳类型：

<syntaxhighlight lang="lean">
inductive List (α : Type) where
| nil : List α
| cons (head : α) (tail : List α) : List α
</syntaxhighlight>

对应的递归函数示例（长度计算）：

<syntaxhighlight lang="lean">
def length {α : Type} : List α → Nat
| List.nil => 0
| List.cons _ xs => 1 + length xs
</syntaxhighlight>

=== 二叉树 ===

更复杂的例子是二叉树：

<syntaxhighlight lang="lean">
inductive BinaryTree (α : Type) where
| leaf : BinaryTree α
| node (left : BinaryTree α) (val : α) (right : BinaryTree α) : BinaryTree α
</syntaxhighlight>

对应的递归函数（计算高度）：

<syntaxhighlight lang="lean">
def height {α : Type} : BinaryTree α → Nat
| BinaryTree.leaf => 0
| BinaryTree.node l _ r => 1 + max (height l) (height r)
</syntaxhighlight>

== 归纳定义的原理 ==

Lean中的归纳定义基于以下理论原则：
1. '''形成规则'''：如何构造该类型的项
2. '''消去规则'''：如何使用该类型的项（模式匹配）
3. '''计算规则'''：模式匹配如何化简

这些规则对应[[Gentzen的自然演绎]]中的引入规则和消去规则。

== 互归纳定义 ==

Lean还支持'''互归纳定义'''(Mutual Inductive)，即多个相互依赖的归纳类型：

<syntaxhighlight lang="lean">
mutual
inductive Even where
| zero : Even
| succ_odd (n : Odd) : Even

inductive Odd where
| succ_even (n : Even) : Odd
end
</syntaxhighlight>

== 归纳谓词 ==

归纳定义不仅可用于数据类型，还可用于谓词（命题）：

<syntaxhighlight lang="lean">
inductive Even : Nat → Prop where
| zero : Even 0
| add_two (n : Nat) : Even n → Even (n + 2)
</syntaxhighlight>

这定义了一个判断自然数是否为偶数的谓词。

== 实际应用案例 ==

=== 编程语言语法 ===

定义简单算术表达式的语法：

<syntaxhighlight lang="lean">
inductive Expr where
| const : Int → Expr
| var : String → Expr
| plus : Expr → Expr → Expr
| times : Expr → Expr → Expr
</syntaxhighlight>

对应的求值函数：

<syntaxhighlight lang="lean">
def eval (env : String → Int) : Expr → Int
| Expr.const n => n
| Expr.var x => env x
| Expr.plus a b => eval env a + eval env b
| Expr.times a b => eval env a * eval env b
</syntaxhighlight>

=== 系统建模 ===

建模简单的状态转换系统：

<syntaxhighlight lang="lean">
inductive SystemState where
| start : SystemState
| running (id : Nat) : SystemState
| paused (id : Nat) : SystemState
| stopped : SystemState
</syntaxhighlight>

== 归纳定义的局限性 ==

1. 所有构造子必须是严格正（strictly positive）的
2. 递归必须结构递减（structural recursion）以保证终止性
3. 某些高级形式需要额外证明终止性

== 高级主题 ==

=== 嵌套归纳 ===

Lean支持嵌套的归纳定义：

<syntaxhighlight lang="lean">
inductive RoseTree (α : Type) where
| node : α → List (RoseTree α) → RoseTree α
</syntaxhighlight>

=== 归纳族 ===

更高级的'''归纳族'''(Indexed Inductive Families)允许类型依赖参数：

<syntaxhighlight lang="lean">
inductive Vec (α : Type) : Nat → Type where
| nil : Vec α 0
| cons {n} : α → Vec α n → Vec α (n + 1)
</syntaxhighlight>

== 可视化表示 ==

自然数归纳定义的生成过程：

<mermaid>
graph TD
    Z[zero] --> S1[succ zero]
    S1 --> S2[succ (succ zero)]
    S2 --> S3[succ (succ (succ zero))]
    style Z fill:#f9f
</mermaid>

== 数学基础 ==

归纳定义的理论基础是[[不动点定理]]。对于类型<math>T</math>，其归纳定义可以看作方程<math>T \cong F(T)</math>的最小不动点，其中<math>F</math>是定义中给出的类型构造子。

== 常见错误与调试 ==

1. '''非严格正'''的错误：
   <syntaxhighlight lang="lean">
   -- 错误的定义
   inductive Bad where
   | mk : (Bad → Bool) → Bad  -- 不允许Bad在负位置出现
   </syntaxhighlight>

2. '''无法证明终止'''的错误：
   <syntaxhighlight lang="lean">
   -- 需要证明termination
   partial def ackermann : Nat → Nat → Nat
   | 0, n => n + 1
   | m+1, 0 => ackermann m 1
   | m+1, n+1 => ackermann m (ackermann (m+1) n)
   </syntaxhighlight>

== 最佳实践 ==

1. 保持归纳定义简单直观
2. 使用结构递归确保终止性
3. 为复杂定义添加文档说明
4. 考虑使用派生实例（如DecidableEq, Repr等）

== 总结 ==

Lean的归纳定义提供了强大而安全的方式来定义递归数据结构和算法。通过结合类型论基础和模式匹配，它既适合初学者理解递归概念，又能满足高级用户对形式化验证的需求。掌握归纳定义是学习Lean和定理证明的关键步骤。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean归纳与递归]]