Lean归纳定义

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

基本概念

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

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

inductive TypeName where
| constructor₁ : ArgumentTypes → TypeName
| constructor₂ : ArgumentTypes → TypeName
...
| constructorₙ : ArgumentTypes → TypeName

简单示例：自然数

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

inductive Nat where
| zero : Nat
| succ (n : Nat) : Nat

这个定义说明：

• zero 是一个自然数（基本情况）
• 如果 n 是一个自然数，那么 succ n（n的后继）也是一个自然数（归纳步骤）

递归函数定义

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

def add : Nat → Nat → Nat
| m, Nat.zero   => m
| m, Nat.succ n => Nat.succ (add m n)

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

结构归纳法

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]

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

复杂归纳类型

列表类型

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

inductive List (α : Type) where
| nil : List α
| cons (head : α) (tail : List α) : List α

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

def length {α : Type} : List α → Nat
| List.nil => 0
| List.cons _ xs => 1 + length xs

二叉树

更复杂的例子是二叉树：

inductive BinaryTree (α : Type) where
| leaf : BinaryTree α
| node (left : BinaryTree α) (val : α) (right : BinaryTree α) : BinaryTree α

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

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

归纳定义的原理

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

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

互归纳定义

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

mutual
inductive Even where
| zero : Even
| succ_odd (n : Odd) : Even

inductive Odd where
| succ_even (n : Even) : Odd
end

归纳谓词

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

inductive Even : Nat → Prop where
| zero : Even 0
| add_two (n : Nat) : Even n → Even (n + 2)

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

实际应用案例

编程语言语法

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

inductive Expr where
| const : Int → Expr
| var : String → Expr
| plus : Expr → Expr → Expr
| times : Expr → Expr → Expr

对应的求值函数：

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

系统建模

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

inductive SystemState where
| start : SystemState
| running (id : Nat) : SystemState
| paused (id : Nat) : SystemState
| stopped : SystemState

归纳定义的局限性

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

高级主题

嵌套归纳

Lean支持嵌套的归纳定义：

inductive RoseTree (α : Type) where
| node : α → List (RoseTree α) → RoseTree α

归纳族

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

inductive Vec (α : Type) : Nat → Type where
| nil : Vec α 0
| cons {n} : α → Vec α n → Vec α (n + 1)

可视化表示

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

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

数学基础

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

常见错误与调试

1. 非严格正的错误：

   -- 错误的定义
   inductive Bad where
   | mk : (Bad → Bool) → Bad  -- 不允许Bad在负位置出现

2. 无法证明终止的错误：

   -- 需要证明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)

最佳实践

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

总结

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