2025年5月12日 (一) 00:30的最新版本

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

Lean归纳类型（Inductive Types）是Lean定理证明器中最基础且强大的类型构造方式之一，它允许用户通过归纳的方式定义数据类型和命题。归纳类型在函数式编程和形式化验证中广泛应用，是理解依赖类型理论和证明构造的核心概念。

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

归纳类型是通过一组构造子（constructors）递归定义的类型。每个构造子可以接受零个或多个参数，并返回该归纳类型的实例。在Lean中，归纳类型不仅用于表示数据结构（如列表、树），还能表示逻辑命题（如“真”、“假”或“存在”）。

归纳类型的定义遵循以下形式：

inductive MyType where
  | constructor₁ : Arg₁ → ... → Argₙ → MyType
  | constructor₂ : ... → MyType
  ...

基本示例：自然数[编辑 | 编辑源代码]

自然数的归纳定义是经典的例子：

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

这里：

zero 是自然数0的构造子。
succ 接受一个Nat类型的参数n，返回n + 1。

递归与模式匹配[编辑 | 编辑源代码]

归纳类型通常与递归函数和模式匹配结合使用。例如，计算自然数的加法：

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

输入 add 2 3 会逐步展开为 Nat.succ (Nat.succ (Nat.succ 2))，最终输出 5。

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

归纳类型可分为以下几类： 1. 简单归纳类型：如Nat、Bool。 2. 参数化归纳类型：如List α（泛型列表）。 3. 索引归纳类型：构造子的返回类型依赖参数（如长度索引列表）。 4. 互归纳类型：多个相互依赖的归纳类型。

参数化示例：列表[编辑 | 编辑源代码]

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

nil 表示空列表。
cons 将元素head添加到列表tail前。

实际应用案例[编辑 | 编辑源代码]

二叉树的定义与操作[编辑 | 编辑源代码]

定义二叉树并实现其深度计算：

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

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

命题逻辑的编码[编辑 | 编辑源代码]

归纳类型可编码逻辑命题。例如，定义命题的合取与析取：

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

高级主题：归纳类型的原理[编辑 | 编辑源代码]

Lean中归纳类型的底层实现基于归纳族（Inductive Families）和递归-归纳原则。例如，Nat会自动生成归纳原则： $\forall P : ℕ \to Prop, P (0) \to (\forall n, P (n) \to P (n + 1)) \to \forall n, P (n)$

图表展示[编辑 | 编辑源代码]

常见问题[编辑 | 编辑源代码]

Q: 归纳类型和递归类型的区别？

 A: 归纳类型强调通过构造子定义，递归类型强调自引用（如链表）。在Lean中二者通常统一。

Q: 如何避免非终止递归？

 A: Lean会检查递归函数是否结构递归（即参数在每次调用中严格减小）。

总结[编辑 | 编辑源代码]

归纳类型是Lean中定义数据结构和逻辑的基础工具，支持从简单自然数到复杂命题的编码。通过构造子和模式匹配，用户可以构建类型安全的程序和形式化证明。

@@ 第1行： / 第1行： @@
-{{DISPLAYTITLE:Lean归纳类型}}
+= Lean归纳类型 =
-'''Lean归纳类型'''（Inductive Types）是[[Lean定理证明器]]类型系统的核心概念之一，它允许用户通过有限的规则构造复杂的数据结构和逻辑命题。本文将详细介绍归纳类型的定义、语法、应用场景以及与递归类型的关系。
+'''Lean归纳类型'''（Inductive Types）是Lean定理证明器中最基础且强大的类型构造方式之一，它允许用户通过归纳的方式定义数据类型和命题。归纳类型在函数式编程和形式化验证中广泛应用，是理解依赖类型理论和证明构造的核心概念。
-== 基本概念 ==
+== 简介 ==
-归纳类型是通过一组'''构造子'''（constructors）定义的类型，每个构造子可以包含参数并递归引用类型自身。数学上，归纳类型 <math>T</math> 的构造过程可描述为：
+归纳类型是通过一组构造子（constructors）递归定义的类型。每个构造子可以接受零个或多个参数，并返回该归纳类型的实例。在Lean中，归纳类型不仅用于表示数据结构（如列表、树），还能表示逻辑命题（如“真”、“假”或“存在”）。
-<math>
+归纳类型的定义遵循以下形式：
-T = c_1(\tau_{11}, \ldots, \tau_{1n_1}) \mid \cdots \mid c_k(\tau_{k1}, \ldots, \tau_{kn_k})
+<syntaxhighlight lang="lean">
-</math>
+inductive MyType where
+  | constructor₁ : Arg₁ → ... → Argₙ → MyType
+  | constructor₂ : ... → MyType
+  ...
+</syntaxhighlight>
-其中 <math>c_i</math> 是构造子，<math>\tau_{ij}</math> 是其参数类型。
+=== 基本示例：自然数 ===
+自然数的归纳定义是经典的例子：
-=== 关键特性 ===
-* 构造子是唯一的生成方式
-* 支持模式匹配（pattern matching）
-* 允许递归定义（如自然数、链表）
-== 语法与示例 ==
-=== 基础定义 ===
 <syntaxhighlight lang="lean">
 inductive Nat where
@@ 第26行： / 第22行： @@
    | succ (n : Nat) : Nat
 </syntaxhighlight>
+这里：
+* <code>zero</code> 是自然数0的构造子。
+* <code>succ</code> 接受一个<code>Nat</code>类型的参数<code>n</code>，返回<code>n + 1</code>。
-这个经典定义表示：
+=== 递归与模式匹配 ===
-* <code>zero</code> 是 0 的构造子
+归纳类型通常与递归函数和模式匹配结合使用。例如，计算自然数的加法：
-* <code>succ</code> 接收一个 <code>Nat</code> 返回其后继
-=== 模式匹配 ===
-定义加法函数：
 <syntaxhighlight lang="lean">
 def add : Nat → Nat → Nat
-   | n, Nat.zero => n
+   | m, Nat.zero   => m
-   | n, Nat.succ m => Nat.succ (add n m)
+   | m, Nat.succ n => Nat.succ (add m n)
-#eval add (Nat.succ Nat.zero) (Nat.succ (Nat.succ Nat.zero))  -- 输出: 3
 </syntaxhighlight>
+输入 <code>add 2 3</code> 会逐步展开为 <code>Nat.succ (Nat.succ (Nat.succ 2))</code>，最终输出 <code>5</code>。
-== 递归与归纳 ==
+== 归纳类型的分类 ==
+归纳类型可分为以下几类：
+. '''简单归纳类型'''：如<code>Nat</code>、<code>Bool</code>。
+. '''参数化归纳类型'''：如<code>List α</code>（泛型列表）。
+. '''索引归纳类型'''：构造子的返回类型依赖参数（如长度索引列表）。
+. '''互归纳类型'''：多个相互依赖的归纳类型。
-归纳类型天然支持结构归纳法。例如证明加法交换律：
+=== 参数化示例：列表 ===
-<syntaxhighlight lang="lean">
-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]
-</syntaxhighlight>
-== 复杂类型示例 ==
-=== 列表类型 ===
 <syntaxhighlight lang="lean">
 inductive List (α : Type) where
@@ 第59行： / 第48行： @@
    | cons (head : α) (tail : List α) : List α
 </syntaxhighlight>
+* <code>nil</code> 表示空列表。
+* <code>cons</code> 将元素<code>head</code>添加到列表<code>tail</code>前。
-=== 二叉树 ===
+== 实际应用案例 ==
-<mermaid>
+=== 二叉树的定义与操作 ===
-graph TD
+定义二叉树并实现其深度计算：
-    A[Tree α] --> B[leaf]
-    A --> C[node]
-    C --> D[left: Tree α]
-    C --> E[val: α]
-    C --> F[right: Tree α]
-</mermaid>
-对应定义：
 <syntaxhighlight lang="lean">
-inductive Tree (α : Type) where
+inductive BinaryTree (α : Type) where
-   | leaf : Tree α
+   | leaf : BinaryTree α
-   | node : Tree α → α → Tree α → Tree α
+   | node (left : BinaryTree α) (val : α) (right : BinaryTree α) : BinaryTree α
-</syntaxhighlight>
-== 实际应用 ==
-=== 表达式求值 ===
-定义算术表达式：
-<syntaxhighlight lang="lean">
-inductive Expr where
-  | const : Int → Expr
-  | add : Expr → Expr → Expr
-  | mul : Expr → Expr → Expr
-def eval : Expr → Int
+def depth : BinaryTree α → Nat
-   | Expr.const n => n
+   | BinaryTree.leaf => 0
-   | Expr.add a b => eval a + eval b
+   | BinaryTree.node l _ r => 1 + max (depth l) (depth r)
-  | Expr.mul a b => eval a * eval b
 </syntaxhighlight>
-=== 逻辑命题 ===
+=== 命题逻辑的编码 ===
-构造命题逻辑：
+归纳类型可编码逻辑命题。例如，定义命题的合取与析取：
 <syntaxhighlight lang="lean">
 inductive PropForm where
-   | true : PropForm
+   | true  : PropForm
    | false : PropForm
-   | var : String → PropForm
+   | and   : PropForm → PropForm → PropForm
-   | and : PropForm → PropForm → PropForm
+   | or    : PropForm → PropForm → PropForm
-   | or : PropForm → PropForm → PropForm
 </syntaxhighlight>
-== 高级主题 ==
+== 高级主题：归纳类型的原理 ==
+Lean中归纳类型的底层实现基于'''归纳族'''（Inductive Families）和'''递归-归纳原则'''。例如，<code>Nat</code>会自动生成归纳原则：
+<math>
+\forall P : \mathbb{N} \to \text{Prop}, P(0) \to (\forall n, P(n) \to P(n+1)) \to \forall n, P(n)
+</math>
-=== 互归纳类型 ===
+== 图表展示 ==
-多个相互依赖的类型：
+<mermaid>
-<syntaxhighlight lang="lean">
+graph TD
-mutual
+   A[归纳类型] --> B[简单类型]
-   inductive Even where
+  A --> C[参数化类型]
-    | zero : Even
+  A --> D[索引类型]
-    | succOdd : Odd → Even
+   A --> E[互归纳类型]
+  B --> F[Nat, Bool]
-   inductive Odd where
+   C --> G[List α]
-    | succEven : Even → Odd
+   D --> H[Vec n α]
-end
+  E --> I[Even/Odd]
-</syntaxhighlight>
+</mermaid>
-=== 索引归纳类型 ===
-使用参数化构造：
-<syntaxhighlight lang="lean">
-inductive Vec (α : Type) : Nat → Type where
-   | nil : Vec α 0
-   | cons : α → Vec α n → Vec α (n+1)
-</syntaxhighlight>
-== 参见 ==
-* [[依赖类型]]
-* [[递归类型]]
-* [[构造演算]]
-{{类型系统导航}}
+== 常见问题 ==
+* '''Q: 归纳类型和递归类型的区别？'''
+  A: 归纳类型强调通过构造子定义，递归类型强调自引用（如链表）。在Lean中二者通常统一。
+* '''Q: 如何避免非终止递归？'''
+  A: Lean会检查递归函数是否结构递归（即参数在每次调用中严格减小）。
-[[Category:Lean编程]]
+== 总结 ==
-[[Category:类型理论]]
+归纳类型是Lean中定义数据结构和逻辑的基础工具，支持从简单自然数到复杂命题的编码。通过构造子和模式匹配，用户可以构建类型安全的程序和形式化证明。
 [[Category:计算机科学]]
 [[Category:Lean]]
-[[Category:Lean类型系统]]
+[[Category:Lean归纳与递归]]