Lean归纳类型

Lean归纳类型（Inductive Types）是Lean定理证明器类型系统的核心概念之一，它允许用户通过有限的规则构造复杂的数据结构和逻辑命题。本文将详细介绍归纳类型的定义、语法、应用场景以及与递归类型的关系。

基本概念

归纳类型是通过一组构造子（constructors）定义的类型，每个构造子可以包含参数并递归引用类型自身。数学上，归纳类型 $T$ 的构造过程可描述为：

$T = c_{1} (τ_{11}, \dots, τ_{1 n_{1}}) ∣ \dots ∣ c_{k} (τ_{k 1}, \dots, τ_{k n_{k}})$

其中 $c_{i}$ 是构造子， $τ_{i j}$ 是其参数类型。

关键特性

构造子是唯一的生成方式
支持模式匹配（pattern matching）
允许递归定义（如自然数、链表）

语法与示例

基础定义

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

这个经典定义表示：

zero 是 0 的构造子
succ 接收一个 Nat 返回其后继

模式匹配

定义加法函数：

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

#eval add (Nat.succ Nat.zero) (Nat.succ (Nat.succ Nat.zero))  -- 输出: 3

递归与归纳

归纳类型天然支持结构归纳法。例如证明加法交换律：

theorem add_comm (n m : Nat) : add n m = add m n := by
  induction m with
  | zero => simp [add]
  | succ m ih => rw [add, ih, ← Nat.succ_add]

复杂类型示例

列表类型

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

二叉树

对应定义：

inductive Tree (α : Type) where
  | leaf : Tree α
  | node : Tree α → α → Tree α → Tree α

实际应用

表达式求值

定义算术表达式：

inductive Expr where
  | const : Int → Expr
  | add : Expr → Expr → Expr
  | mul : Expr → Expr → Expr

def eval : Expr → Int
  | Expr.const n => n
  | Expr.add a b => eval a + eval b
  | Expr.mul a b => eval a * eval b

逻辑命题

构造命题逻辑：

inductive PropForm where
  | true : PropForm
  | false : PropForm
  | var : String → PropForm
  | and : PropForm → PropForm → PropForm
  | or : PropForm → PropForm → PropForm

高级主题

互归纳类型

多个相互依赖的类型：

mutual
  inductive Even where
    | zero : Even
    | succOdd : Odd → Even

  inductive Odd where
    | succEven : Even → Odd
end

索引归纳类型

使用参数化构造：

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

参见

模板:类型系统导航