7.1. 枚举类型🔗

最简单的归纳类型是一个具有有限的、可枚举的元素列表的类型。

inductive 命令创建了一个新类型 Weekday。构造子都在 Weekday 命名空间中。

Weekday.sunday : Weekday

Weekday.monday : Weekday

Weekday.sunday : Weekday

Weekday.monday : Weekday

在声明 Weekday 归纳类型时，可以省略 : Weekday。

把 sunday、monday、... 、saturday 看作是 Weekday 的不同元素，没有其他有区别的属性。 消去规则 Weekday.rec，与 Weekday 类型及其构造子一起定义。它也被称为 递归器（Recursor）， 它是使该类型“归纳”的原因：它允许我们通过给每个构造子分配相应的值来定义 Weekday 的函数。 直观的说，归纳类型是由构造子详尽地生成的，除了它们构造的元素外，没有其他元素。

我们将使用 match 表达式来定义一个从 Weekday 到自然数的函数：

1

2

3

在使用 Lean 的逻辑时，match 表达式是使用声明归纳类型时生成的 递归器（recursor） Weekday.rec 来编译的。 这确保了结果项在类型论中是良定义的。对于编译后的代码，match 的编译方式与其他函数式编程语言相同。

def numberOfDay : (d : Weekday) → Nat :=
fun (d : Weekday) =>
  numberOfDay.match_1.{1} (fun (d : Weekday) => Nat) d
    (fun (_ : Unit) => @OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))
    (fun (_ : Unit) => @OfNat.ofNat.{0} Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))
    (fun (_ : Unit) => @OfNat.ofNat.{0} Nat (nat_lit 3) (instOfNatNat (nat_lit 3)))
    (fun (_ : Unit) => @OfNat.ofNat.{0} Nat (nat_lit 4) (instOfNatNat (nat_lit 4)))
    (fun (_ : Unit) => @OfNat.ofNat.{0} Nat (nat_lit 5) (instOfNatNat (nat_lit 5)))
    (fun (_ : Unit) => @OfNat.ofNat.{0} Nat (nat_lit 6) (instOfNatNat (nat_lit 6))) fun (_ : Unit) =>
    @OfNat.ofNat.{0} Nat (nat_lit 7) (instOfNatNat (nat_lit 7))

def numberOfDay.match_1.{u_1} : (motive : Weekday → Sort u_1) →
  (d : Weekday) →
    (h_1 : (a : Unit) → motive Weekday.sunday) →
      (h_2 : (a : Unit) → motive Weekday.monday) →
        (h_3 : (a : Unit) → motive Weekday.tuesday) →
          (h_4 : (a : Unit) → motive Weekday.wednesday) →
            (h_5 : (a : Unit) → motive Weekday.thursday) →
              (h_6 : (a : Unit) → motive Weekday.friday) → (h_7 : (a : Unit) → motive Weekday.saturday) → motive d :=
fun (motive : Weekday → Sort u_1) (d : Weekday) (h_1 : (a : Unit) → motive Weekday.sunday)
    (h_2 : (a : Unit) → motive Weekday.monday) (h_3 : (a : Unit) → motive Weekday.tuesday)
    (h_4 : (a : Unit) → motive Weekday.wednesday) (h_5 : (a : Unit) → motive Weekday.thursday)
    (h_6 : (a : Unit) → motive Weekday.friday) (h_7 : (a : Unit) → motive Weekday.saturday) =>
  @Weekday.casesOn.{u_1} (fun (x : Weekday) => motive x) d (h_1 Unit.unit) (h_2 Unit.unit) (h_3 Unit.unit)
    (h_4 Unit.unit) (h_5 Unit.unit) (h_6 Unit.unit) (h_7 Unit.unit)

@[reducible] def Weekday.casesOn.{u} : {motive : (t : Weekday) → Sort u} →
  (t : Weekday) →
    (sunday : motive Weekday.sunday) →
      (monday : motive Weekday.monday) →
        (tuesday : motive Weekday.tuesday) →
          (wednesday : motive Weekday.wednesday) →
            (thursday : motive Weekday.thursday) →
              (friday : motive Weekday.friday) → (saturday : motive Weekday.saturday) → motive t :=
fun {motive : (t : Weekday) → Sort u} (t : Weekday) (sunday : motive Weekday.sunday) (monday : motive Weekday.monday)
    (tuesday : motive Weekday.tuesday) (wednesday : motive Weekday.wednesday) (thursday : motive Weekday.thursday)
    (friday : motive Weekday.friday) (saturday : motive Weekday.saturday) =>
  @Weekday.rec.{u} motive sunday monday tuesday wednesday thursday friday saturday t

@Weekday.rec.{u_1} : {motive : (t : Weekday) → Sort u_1} →
  (sunday : motive Weekday.sunday) →
    (monday : motive Weekday.monday) →
      (tuesday : motive Weekday.tuesday) →
        (wednesday : motive Weekday.wednesday) →
          (thursday : motive Weekday.thursday) →
            (friday : motive Weekday.friday) → (saturday : motive Weekday.saturday) → (t : Weekday) → motive t

当声明一个归纳数据类型时，你可以使用 deriving Repr 来指示 Lean 生成一个函数，将 Weekday 对象转换为文本。 这个函数被 #eval 命令用来显示 Weekday 对象。如果不存在 Repr，#eval 会尝试当场派生一个。

Weekday.tuesday

将与某一结构相关的定义和定理归入同名的命名空间通常很有用。例如，我们可以将 numberOfDay 函数放在 Weekday 命名空间中。 然后当我们打开命名空间时，我们就可以使用较短的名称。

我们可以定义从 Weekday 到 Weekday 的函数：

Weekday.thursday

Weekday.tuesday

我们如何证明对于任何 Weekday d，next (previous d) = d 的一般定理？ 你可以使用 match 为每个构造子提供该主张的证明：

使用策略证明，我们可以更简洁：

下面的 归纳类型的策略 将介绍专门设计用于利用归纳类型的其他策略。

注意，在 命题即类型 的对应关系下，我们可以使用 match 来证明定理以及定义函数。 换句话说，在 命题即类型 的对应关系下，按情况证明是一种按情况定义，其中被“定义”的是证明而不是数据。

Lean 库中的 Bool 类型是枚举类型的一个实例。

（为了运行这些例子，我们将它们放在一个名为 Hidden 的命名空间中，这样像 Bool 这样的名字就不会与标准库中的 Bool 冲突。 这是必要的，因为这些类型是 Lean “prelude”的一部分，在系统启动时会自动导入。）

作为一个练习，你应该思考这些类型的引入和消去规则是做什么的。作为进一步的练习，我们建议在 Bool 类型上定义布尔运算 and、or、not， 并验证常见的恒等式。注意，你可以使用 match 定义像 and 这样的二元运算：

同样，大多数恒等式可以通过引入合适的 match，然后使用 rfl 来证明。

7.2. 带参数的构造子🔗

枚举类型是归纳类型的一个非常特殊的情况，其中的构造子完全不接受参数。一般来说，一个“构造”可以依赖于数据， 然后这些数据在构造的参数中表示出来。考虑一下库中乘积类型和和类型的定义：

考虑一下这些例子中发生了什么。乘积类型有一个构造子 Prod.mk，它接受两个参数。 为了定义 Prod α β 上的函数，我们可以假设输入的形式是 Prod.mk a b，并且我们必须根据 a 和 b 指定输出。 我们可以用这个来定义 Prod 的两个投影。请记住，标准库为 Prod α β 定义了符号 α × β， 为 Prod.mk a b 定义了符号 (a, b)。

函数 fst 接受一个对子 p。match 将 p 解释为一个对子 Prod.mk a b。 还记得在 依赖类型理论 中，为了使这些定义尽可能通用，我们允许类型 α 和 β 属于任何宇宙。

这是另一个例子，我们使用递归器 Prod.casesOn 而不是 match。

6

7

参数 motive 用于指定你想要构造的对象的类型，它是一个函数，因为它可能依赖于该对子。 cond 函数是一个布尔条件：如果 b 为真，cond b t1 t2 返回 t1，否则返回 t2。 函数 prod_example 接受一个由布尔值 b 和数字 n 组成的对子， 并根据 b 是真还是假返回 2 * n 或 2 * n + 1。

相比之下，和类型有 两个 构造子，inl 和 inr（代表“左插入”和“右插入”），每个构造子接受 一个（显式）参数。 为了定义 Sum α β 上的函数，我们必须处理两种情况：要么输入的形式是 inl a，在这种情况下我们必须根据 a 指定输出值； 要么输入的形式是 inr b，在这种情况下我们必须根据 b 指定输出值。

6

7

这个例子与前一个类似，但现在 sum_example 的输入隐式地要么是 inl n 的形式，要么是 inr n 的形式。 在第一种情况下，函数返回 2 * n，在第二种情况下，它返回 2 * n + 1。

注意，乘积类型依赖于参数 α β : Type，它们既是构造子的参数，也是 Prod 的参数。 当这些参数可以从构造子的后续参数或返回类型中推断出来时，Lean 会检测到并将它们设为隐式。

在 定义自然数 中，我们将看到当归纳类型的构造子接受来自归纳类型本身的参数时会发生什么。 我们在本节中考虑的例子的特点是，每个构造子只依赖于先前指定的类型。

注意，具有多个构造子的类型是析取的：Sum α β 的元素要么是 inl a 的形式，要么 是 inr b 的形式。 具有多个参数的构造子引入了合取信息：从 Prod α β 的元素 Prod.mk a b 中，我们可以提取 a 和 b。 任意归纳类型可以包含这两个特征，即拥有任意数量的构造子，每个构造子接受任意数量的参数。

与函数定义一样，Lean 的归纳定义语法允许你将构造子的命名参数放在冒号之前：

这些定义的结果本质上与本节前面给出的结果相同。

像 Prod 这样只有一个构造子的类型是纯合取的：构造子只是将参数列表打包成单个数据，本质上是一个元组， 其中后续参数的类型可以依赖于初始参数的类型。我们也可以把这种类型看作是“记录”或“结构”。 在 Lean 中，关键字 structure 可以用来同时定义这种归纳类型及其投影。

这个例子同时引入了归纳类型 Prod、它的构造子 mk、通常的消去器（rec 和 recOn）， 以及如上定义的投影 fst 和 snd。

如果你不命名构造子，Lean 默认使用 mk。例如，下面定义了一个记录，将颜色存储为 RGB 值的元组：

255

yellow 的定义用显示的三个值形成了记录，投影 Color.red 返回红色分量。

structure 命令对于定义代数结构特别有用，Lean 提供了大量的基础设施来支持它们的使用。例如，这里是半群的定义：

我们将在 结构体与记录 一章中看到更多例子。

我们已经讨论了依赖乘积类型 Sigma：

库中还有两个归纳类型的例子：

在依赖类型理论的语义中，没有内置的部分函数的概念。函数类型 α → β 或依赖函数类型 (a : α) → β 的每个元素都被假定在每个输入上都有值。 Option 类型提供了一种表示部分函数的方法。Option β 的元素要么是 none，要么是 some b 的形式，其中 b : β。 因此，我们可以把类型 α → Option β 的元素 f 看作是从 α 到 β 的部分函数： 对于每个 a : α，f a 要么返回 none（表示 f a “未定义”），要么返回 some b。

Inhabited α 的元素只是 α 中存在元素这一事实的见证。稍后，我们将看到 Inhabited 是 Lean 中 类型类 的一个例子： 可以指示 Lean 适当的基本类型是居留的，并在此基础上自动推断其他构造类型也是居留的。

作为练习，我们鼓励你开发从 α 到 β 以及从 β 到 γ 的部分函数的组合概念，并证明它的行为符合预期。 我们还鼓励你证明 Bool 和 Nat 是居留的，两个居留类型的乘积是居留的，以及到居留类型的函数的类型是居留的。

7.3. 归纳定义的命题🔗

归纳定义的类型可以存在于任何类型宇宙中，包括最底层的 Prop。事实上，这正是逻辑连接词的定义方式。

你应该思考这些是如何产生你已经看到的引入和消去规则的。有一些规则管理归纳类型的消去器可以消去 到 什么， 也就是说，什么样的类型可以是递归器的目标。粗略地说，Prop 中归纳类型的特征是，人们只能消去到 Prop 中的其他类型。 这与如果 p : Prop，则元素 hp : p 不携带数据的理解是一致的。 然而，这个规则有一个小的例外，我们将在下面的 归纳族 中讨论。

甚至存在量词也是归纳定义的：

请记住，符号 ∃ x : α, p 是 Exists (fun x : α => p) 的语法糖。

False、True、And 和 Or 的定义与 Empty、Unit、 Prod 和 Sum 的定义完全类似。区别在于第一组产生 Prop 的元素， 而第二组产生某个 u 的 Type u 的元素。类似地，∃ x : α, p 是 Σ x : α, β 的 Prop 值变体。

这里适合提及另一种归纳类型，记作 {x : α // p}，它是 ∃ x : α, p 和 Σ x : α, β 的一种混合体。

事实上，在 Lean 中，Subtype 是使用 structure 命令定义的：

符号 {x : α // p x} 是 Subtype (fun x : α => p x) 的语法糖。 它模仿了集合论中的子集符号：其思想是 {x : α // p x} 表示 α 中具有属性 p 的元素集合。

7.4. 定义自然数🔗

到目前为止，我们所看到的归纳定义的类型都是“平坦的”：构造子打包数据并将其插入到一个类型中，而相应的递归器则解压数据并对其进行操作。 当构造子作用于被定义的类型中的元素时，事情就变得更加有趣了。一个典型的例子是自然数 Nat 类型：

有两个构造子，我们从 zero : Nat 开始；它不需要参数，所以我们一开始就有了它。相反，构造子 succ 只能应用于先前构造的 Nat。 将其应用于 zero，得到 succ zero : Nat。再次应用它可以得到 succ (succ zero) : Nat，依此类推。 直观地说，Nat 是具有这些构造子的“最小”类型，这意味着它是通过从 zero 开始并重复应用 succ 这样无穷无尽地（并且自由地）生成的。

和以前一样，Nat 的递归器被设计用来定义一个从 Nat 到任何域的依赖函数 f，也就是一个 (n : Nat) → motive n 的元素 f， 其中 motive : Nat → Sort u。它必须处理两种情况：一种是输入为 zero 的情况，另一种是输入为 succ n 的情况，其中 n : Nat。 在第一种情况下，我们只需指定一个适当类型的目标值，就像以前一样。但是在第二种情况下，递归器可以假设在 n 处的 f 的值已经被计算过了。 因此，递归器的下一个参数是以 n 和 f n 来指定 f (succ n) 的值。如果检查递归器的类型，你会得到：

隐参数 motive，是被定义的函数的陪域。在类型论中，通常说 motive 是消去/递归的 目的 ，因为它描述了我们希望构建的对象类型。 接下来的两个参数指定了如何计算零和后继的情况，如上所述。它们也被称为 小前提。 最后，t : Nat 是函数的输入。它也被称为 大前提。

Nat.recOn 与 Nat.rec 类似，但大前提发生在小前提之前。

例如，考虑自然数上的加法函数 add m n。固定 m，我们可以通过递归来定义 n 的加法。在基本情况下，我们将 add m zero 设为 m。 在后续步骤中，假设 add m n 的值已经确定，我们将 add m (succ n) 定义为 succ (add m n)。

Hidden.Nat.succ (Hidden.Nat.succ (Hidden.Nat.succ (Hidden.Nat.zero)))

将这些定义放入一个命名空间 Nat 是很有用的。然后我们可以继续在这个命名空间中定义熟悉的符号。现在加法的两个定义方程是定义上成立的：

我们将在 类型类 一章中解释 instance 命令如何工作。在下面的例子中，我们将使用 Lean 自己的自然数版本。

然而，证明像 0 + n = n 这样的事实，需要用归纳法证明。如上所述，归纳原则只是递归原则的一个特例，其中陪域 motive n 是 Prop 的一个元素。 它代表了熟悉的归纳证明模式：要证明 ∀ n, motive n，首先要证明 motive 0，然后对于任意的 n，假设 ih : motive n 并证明 motive (n + 1)。

请注意，当 Nat.recOn 在证明中使用时，它实际上是变相的归纳原则。rw 和 simp 策略在这样的证明中往往非常有效。 在这种情况下，证明可以化简成：

另一个例子，让我们证明加法结合律，∀ m n k, m + n + k = m + (n + k)。 （我们定义的符号 + 是向左结合的，所以 m + n + k 实际上是 (m + n) + k。） 最难的部分是确定在哪个变量上做归纳。由于加法是由第二个参数的递归定义的，k 是一个很好的猜测，一旦我们做出这个选择，证明几乎是顺理成章的：