归纳类型与结构体

inductive 的构造子与递归子、structure 与继承、参数与索引的区别、Nat 与 List 的真实定义。

归纳类型是地基

Lean 里几乎所有数据类型都是 inductive 定义的——包括 Nat、List、Bool，甚至逻辑联结词 And、Or。

inductive Color where
  | red
  | green
  | blue

三个构造子，穷尽了 Color 的所有可能值。

#check Color.red        -- Color.red : Color
#check Color            -- Color : Type

带参数的构造子：

inductive Shape where
  | circle (radius : Float)
  | rect (width height : Float)

def area : Shape → Float
  | .circle r    => 3.14159 * r * r
  | .rect w h    => w * h

.circle 是 Shape.circle 的简写——当类型能被推断时可以省略前缀。这个点记法在模式匹配里用得极多。

Nat 的真实定义

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

自然数不是机器整数，是一个归纳定义的链：

0 = Nat.zero
1 = Nat.succ Nat.zero
2 = Nat.succ (Nat.succ Nat.zero)

这解释了上一章的几件事：为什么 Nat 没有负数（构造子里没有）、为什么减法要截断（0 再减只能是 0）。

性能上 Lean 不真的用一元表示。 编译器对 Nat 有特殊处理，小数用机器整数、大数用 GMP。但在证明层面它就是上面那个归纳定义——归纳法证明依赖的正是这个结构。

这是 Lean 的一个典型模式：语义定义要简洁可推理，运行时实现可以优化，两者由编译器保证一致。

List 的真实定义

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

[1, 2, 3] 是 1 :: 2 :: 3 :: [] 的语法糖，而 :: 就是 cons、[] 就是 nil。

def length : List α → Nat
  | []      => 0
  | _ :: xs => 1 + length xs

结构递归：xs 比 _ :: xs 严格小，所以终止性自动通过。

递归子与归纳法

每定义一个 inductive，Lean 自动生成几个东西：

#check @Nat.rec        -- 递归子（recursor），最基础的消去规则
#check @Nat.casesOn    -- 分情况
#check @Nat.succ.inj   -- 构造子单射性
#check @Nat.noConfusion -- 不同构造子不相等

Nat.rec 的类型（简化后）：

{motive : Nat → Sort u}
→ motive Nat.zero
→ ((n : Nat) → motive n → motive n.succ)
→ (t : Nat) → motive t

读作：「要对所有 Nat 造出 motive n，只需给出：零的情况，以及从 n 的情况造 n+1 的情况。」

这就是数学归纳法。当 motive n 是命题时它是归纳证明，当 motive n 是数据时它是递归定义——同一条规则。

这是「命题即类型」的第一个具体例子，第 2 部分会全面展开。

日常写证明用 induction tactic 而不是直接调 Nat.rec，见归纳证明。

structure

只有一个构造子的归纳类型，用 structure 更方便：

structure Point where
  x : Float
  y : Float

Lean 自动生成：

#check Point.mk         -- Float → Float → Point   构造子
#check Point.x          -- Point → Float           投影
#check Point.y

三种构造写法：

def p1 : Point := ⟨1.0, 2.0⟩                  -- 匿名构造子
def p2 : Point := Point.mk 1.0 2.0            -- 显式
def p3 : Point := { x := 1.0, y := 2.0 }      -- 具名字段

具名字段形式最可读，字段多时尤其如此。

更新语法

def moved : Point := { p1 with x := 5.0 }

「除了 x 改成 5.0，其余同 p1」。函数式语言的标准做法——不修改原值，返回新值。

自定义构造子名与默认值

structure Config where
  mk ::                                -- 自定义构造子名
  host : String := "localhost"         -- 默认值
  port : Nat := 8080

#eval (({} : Config)).port             -- 8080，全用默认值
#eval ({ port := 3000 } : Config).host -- "localhost"

结构体继承

structure Point3D extends Point where
  z : Float

def q : Point3D := { x := 1, y := 2, z := 3 }
#eval q.x          -- 1.0，继承来的字段直接可用
#eval q.toPoint    -- 自动生成的向上转换

extends 生成 toPoint 投影。可以继承多个：

structure A where a : Nat
structure B where b : Nat
structure C extends A, B where c : Nat

这套机制正是类型类层次结构的基础——Mathlib 里 Monoid extends Semigroup, One 之类的代数结构层次全靠它。

参数 vs 索引

这是归纳类型里最需要理解的区别。

-- α 是【参数】：在 : 左边，所有构造子里保持不变
inductive MyList (α : Type) where
  | nil  : MyList α
  | cons : α → MyList α → MyList α

-- n 是【索引】：在 : 右边，不同构造子可以给不同的值
inductive Vec (α : Type) : Nat → Type where
  | nil  : Vec α 0
  | cons : α → Vec α n → Vec α (n + 1)

	参数（parameter）	索引（index）
位置	`:` 左边	`:` 右边
各构造子中	必须相同	可以不同
作用	泛型	让类型携带信息

Vec α n 是长度写进类型的列表：

def v : Vec Nat 3 := .cons 1 (.cons 2 (.cons 3 .nil))
-- def bad : Vec Nat 2 := .cons 1 (.cons 2 (.cons 3 .nil))   ← 类型错误！

类型检查器会拒绝长度不对的向量。这是依值类型的威力——把不变量编码进类型，编译期就排除一整类错误。

它的实际收益：

def head : Vec α (n + 1) → α
  | .cons a _ => a

head 的类型要求输入长度至少为 1，所以不需要处理空列表的情况——空表根本传不进来。对比 List.head 必须返回 Option 或要求一个「非空」的证明。

依值类型那一章会继续展开。

相互递归

mutual
  inductive Tree (α : Type) where
    | node : α → Forest α → Tree α

  inductive Forest (α : Type) where
    | nil  : Forest α
    | cons : Tree α → Forest α → Forest α
end

mutual ... end 包住相互引用的定义。函数也可以：

mutual
  def isEven : Nat → Bool
    | 0     => true
    | n + 1 => isOdd n

  def isOdd : Nat → Bool
    | 0     => false
    | n + 1 => isEven n
end

deriving

inductive Color where
  | red | green | blue
  deriving Repr, DecidableEq, Inhabited

自动派生常用实例：

派生	得到什么
`Repr`	能被 `#eval` 打印
`DecidableEq`	相等性可判定，可用 `==` 与 `if`
`Inhabited`	有默认值（`default`）
`BEq`	布尔相等
`Hashable`	可做哈希表的键

#eval 一个自定义类型报错「no Repr instance」时，加 deriving Repr 即可。 这是最常见的新手卡点之一。

一个综合例子

inductive Expr where
  | lit : Int → Expr
  | add : Expr → Expr → Expr
  | mul : Expr → Expr → Expr
  | neg : Expr → Expr
  deriving Repr

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

def e : Expr := .add (.lit 3) (.mul (.lit 4) (.neg (.lit 2)))

#eval eval e     -- -5

一个表达式求值器，20 行不到，且穷尽性由编译器保证——加一个新构造子，所有 match 都会报错提醒你处理。

而且我们可以对它证明定理：

theorem eval_neg (a : Expr) : eval (.neg a) = -eval a := rfl

这是 Lean 的价值所在：同一段代码既能跑，又能证。

下一篇：类型类。

本页目录