7.1. 枚举类型（Enumerated Types）7.1. Enumerated Types🔗

最简单的归纳类型是具有有限枚举元素列表的类型。The simplest kind of inductive type is a type with a finite, enumerated list of elements.

inductive 命令创建一个新类型 Weekday。构造子都位于 Weekday 命名空间中。The inductive command creates a new type, Weekday. The constructors all live in the Weekday namespace.

Weekday.sunday : Weekday

Weekday.monday : Weekday

Weekday.sunday : Weekday

Weekday.monday : Weekday

声明 : Weekday 在声明 Weekday 归纳类型时可以省略。You can omit : Weekday when declaring the Weekday inductive type.

将 sunday、monday、……、saturday 视为 Weekday 的互异元素，没有其他可区分的性质。消去原理 Weekday.rec 是随类型 Weekday 及其构造子一起定义的。它也被称为递归子（recursor），正是它使该类型成为“归纳的”：它允许我们通过为每个构造子分配值来在 Weekday 上定义函数。其直觉是归纳类型由构造子穷尽生成，除此之外没有其他元素。Think of sunday, monday, ... , saturday as being distinct elements of Weekday, with no other distinguishing properties. The elimination principle, Weekday.rec, is defined along with the type Weekday and its constructors. It is also known as a recursor, and it is what makes the type “inductive”: it allows us to define a function on Weekday by assigning values corresponding to each constructor. The intuition is that an inductive type is exhaustively generated by the constructors, and has no elements beyond those they construct.

我们将使用 match 表达式定义一个从 Weekday 到自然数的函数：We will use the match expression to define a function from Weekday to the natural numbers:

1

2

3

当使用 Lean 的逻辑时，match 表达式使用声明归纳类型时生成的递归子 Weekday.rec 进行编译。这确保了结果项在类型论中是有良好定义的。对于编译后的代码，match 像在其他函数式编程语言中一样被编译。When using Lean's logic, the match expression is compiled using the recursor Weekday.rec generated when you declare the inductive type. This ensures that the resulting term is well-defined in the type theory. For compiled code, match is compiled as in other functional programming languages.

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 会尝试当场推导出一个。When declaring an inductive datatype, you can use deriving Repr to instruct Lean to generate a function that converts Weekday objects into text. This function is used by the #eval command to display Weekday objects. If no Repr exists, #eval attempts to derive one on the spot.

Weekday.tuesday

将定义和定理归入具有相同名称的命名空间中通常很有用。例如，我们可以将 numberOfDay 函数放在 Weekday 命名空间中。然后当我们打开该命名空间时，就可以使用较短的名称。It is often useful to group definitions and theorems related to a structure in a namespace with the same name. For example, we can put the numberOfDay function in the Weekday namespace. We are then allowed to use the shorter name when we open the namespace.

我们可以定义从 Weekday 到 Weekday 的函数：We can define functions from Weekday to Weekday:

Weekday.thursday

Weekday.tuesday

我们如何证明对于任意 Weekday d，有一般定理 next(previous d) = d？你可以使用 match 为每个构造子提供该断言的证明：How can we prove the general theorem that next (previous d) = d for any Weekday d? You can use match to provide a proof of the claim for each constructor:

使用策略证明（tactic proof），我们可以更简洁：Using a tactic proof, we can be even more concise:

下面的Tactics for Inductive Types将介绍专门设计用于利用归纳类型的其他策略。Tactics for Inductive Types below will introduce additional tactics that are specifically designed to make use of inductive types.

注意，在命题即类型（propositions-as-types）对应下，我们可以使用 match 来证明定理以及定义函数。换句话说，在命题即类型对应下，按情况证明（proof by cases）是一种按情况定义（definition by cases），其中被“定义”的是证明而不是数据。Notice that, under the propositions-as-types correspondence, we can use match to prove theorems as well as define functions. In other words, under the propositions-as-types correspondence, the proof by cases is a kind of definition by cases, where what is being “defined” is a proof instead of a piece of data.

Lean 库中的 Bool 类型是枚举类型的一个实例。The Bool type in the Lean library is an instance of enumerated type.

（为了运行这些示例，我们将它们放入名为 Hidden 的命名空间中，这样像 Bool 这样的名称就不会与标准库中的 Bool 冲突。这是必要的，因为这些类型是 Lean“预导入（prelude）”的一部分，在系统启动时会自动导入。）(To run these examples, we put them in a namespace called Hidden, so that a name like Bool does not conflict with the Bool in the standard library. This is necessary because these types are part of the Lean “prelude” that is automatically imported when the system is started.)

作为练习，你应该思考这些类型的引入规则和消去规则的作用。作为进一步的练习，我们建议在 Bool 类型上定义布尔运算 and、or、not，并验证常见的恒等式。注意，你可以使用 match 来定义像 and 这样的二元运算：As an exercise, you should think about what the introduction and elimination rules for these types do. As a further exercise, we suggest defining boolean operations and, or, not on the Bool type, and verifying common identities. Note that you can define a binary operation like and using match:

类似地，大多数恒等式可以通过引入合适的 match，然后使用 rfl 来证明。Similarly, most identities can be proved by introducing suitable match, and then using rfl.

7.2. 带参数的构造子（Constructors with Arguments）7.2. Constructors with Arguments🔗

枚举类型是归纳类型的一个非常特殊的情况，其中构造子根本不带参数。通常，一个“构造”可以依赖于数据，这些数据随后在构造的参数中体现。考虑库中积类型（product type）和和类型（sum type）的定义：Enumerated types are a very special case of inductive types, in which the constructors take no arguments at all. In general, a “construction” can depend on data, which is then represented in the constructed argument. Consider the definitions of the product type and sum type in the library:

思考这些例子中发生了什么。积类型有一个构造子 Prod.mk，它接受两个参数。要定义 Prod α β 上的函数，我们可以假设输入形式为 Prod.mk a b，并且需要根据 a 和 b 指定输出。我们可以利用这一点为 Prod 定义两个投影。记住，标准库为 Prod α β 定义了记法 α × β，并为 Prod.mk a b 定义了记法 (a, b)。Consider what is going on in these examples. The product type has one constructor, Prod.mk, which takes two arguments. To define a function on Prod α β, we can assume the input is of the form Prod.mk a b, and we have to specify the output, in terms of a and b. We can use this to define the two projections for Prod. Remember that the standard library defines notation α × β for Prod α β and (a, b) for Prod.mk a b.

函数 fst 接受一个序对 p。match 将 p 解释为一个序对 Prod.mk a b。另外从依值类型论中回忆，为了使这些定义具有最大的一般性，我们允许类型 α 和 β 属于任意宇宙。The function fst takes a pair, p. The match interprets p as a pair, Prod.mk a b. Recall also from Dependent Type Theory that to give these definitions the greatest generality possible, we allow the types α and β to belong to any universe.

这里有另一个例子，我们使用递归子 Prod.casesOn 而不是 match。Here is another example where we use the recursor Prod.casesOn instead of match.

6

7

参数 motive 用于指定要构造的对象的类型，并且它是一个函数，因为它可能依赖于序对。cond 函数是一个布尔条件式：cond b t1 t2 在 b 为真时返回 t1，否则返回 t2。函数 prod_example 接受一个由布尔值 b 和数字 n 组成的序对，并根据 b 是真还是假返回 2 * n 或 2 * n + 1。The argument motive is used to specify the type of the object you want to construct, and it is a function because it may depend on the pair. The cond function is a boolean conditional: cond b t1 t2 returns t1 if b is true, and t2 otherwise. The function prod_example takes a pair consisting of a boolean, b, and a number, n, and returns either 2 * n or 2 * n + 1 according to whether b is true or false.

相比之下，和类型有两个构造子 inl 和 inr（分别表示“insert left”和“insert right”），每个接受一个（显式）参数。要定义 Sum α β 上的函数，我们必须处理两种情况：要么输入的形式是 inl a，此时必须根据 a 指定输出值；要么输入的形式是 inr b，此时必须根据 b 指定输出值。In contrast, the sum type has two constructors, inl and inr (for “insert left” and “insert right”), each of which takes one (explicit) argument. To define a function on Sum α β, we have to handle two cases: either the input is of the form inl a, in which case we have to specify an output value in terms of a, or the input is of the form inr b, in which case we have to specify an output value in terms of b.

6

7

这个例子与上一个类似，但现在 sum_example 的输入隐式地要么是 inl n，要么是 inr n。在第一种情况下，函数返回 2 * n；在第二种情况下，返回 2 * n + 1。This example is similar to the previous one, but now an input to sum_example is implicitly either of the form inl n or inr n. In the first case, the function returns 2 * n, and the second case, it returns 2 * n + 1.

注意，积类型依赖于参数 α β : Type，这些参数也是构造子和 Prod 的参数。当 Lean 检测到这些参数可以从构造子的后续参数或返回类型中推断出来时，就会使它们成为隐式参数。Notice that the product type depends on parameters α β : Type which are arguments to the constructors as well as Prod. Lean detects when these arguments can be inferred from later arguments to a constructor or the return type, and makes them implicit in that case.

在Defining the Natural Numbers中，我们将看到当归纳类型的构造子接受来自该归纳类型本身的参数时会发生什么。我们本节考虑示例的特点是每个构造子仅依赖于先前指定的类型。In Defining the Natural Numbers we will see what happens when the constructor of an inductive type takes arguments from the inductive type itself. What characterizes the examples we consider in this section is that each constructor relies only on previously specified types.

注意，具有多个构造子的类型是析取性的：Sum α β 的元素要么是 inl a 或 inr b。具有多个参数的构造子引入合取性信息：从 Prod.mk a b 这样的 Prod α β 元素中，我们可以提取 a 和 b。任意归纳类型可以通过具有任意数量的构造子（每个构造子接受任意数量的参数）来同时包含这两种特性。Notice that a type with multiple constructors is disjunctive: an element of Sum α β is either of the form inl a or of the form inl b. A constructor with multiple arguments introduces conjunctive information: from an element Prod.mk a b of Prod α β we can extract a and b. An arbitrary inductive type can include both features, by having any number of constructors, each of which takes any number of arguments.

与函数定义类似，Lean 的归纳定义语法允许你在冒号前为构造子命名参数：As with function definitions, Lean's inductive definition syntax will let you put named arguments to the constructors before the colon:

这些定义的结果与本节前面给出的基本相同。The results of these definitions are essentially the same as the ones given earlier in this section.

像 Prod 这样只有一个构造子的类型是纯合取性的：构造子简单地将参数列表打包成单一数据，本质上是一个元组（tuple），其中后续参数的类型可以依赖于初始参数的类型。我们也可以将这样的类型视为“记录（record）”或“结构体（structure）”。在 Lean 中，关键字 structure 可用于同时定义这样的归纳类型及其投影。A type, like Prod, that has only one constructor is purely conjunctive: the constructor simply packs the list of arguments into a single piece of data, essentially a tuple where the type of subsequent arguments can depend on the type of the initial argument. We can also think of such a type as a “record” or a “structure”. In Lean, the keyword structure can be used to define such an inductive type as well as its projections, at the same time.

这个例子同时引入了归纳类型 Prod、其构造子 mk、通常的消去子（rec 和 recOn），以及如上定义的投影 fst 和 snd。This example simultaneously introduces the inductive type, Prod, its constructor, mk, the usual eliminators (rec and recOn), as well as the projections, fst and snd, as defined above.

如果你不为构造子命名，Lean 默认使用 mk。例如，以下定义了一个将颜色存储为 RGB 值三元组的记录：If you do not name the constructor, Lean uses mk as a default. For example, the following defines a record to store a color as a triple of RGB values:

255

yellow 的定义使用所示的三个值构成记录，投影 Color.red 返回红色分量。The definition of yellow forms the record with the three values shown, and the projection Color.red returns the red component.

structure 命令对于定义代数结构特别有用，Lean 为此提供了大量的基础设施。例如，以下是半群（semigroup）的定义：The structure command is especially useful for defining algebraic structures, and Lean provides substantial infrastructure to support working with them. Here, for example, is the definition of a semigroup:

我们将在关于结构体与记录（structures and records）的章节中看到更多示例。We will see more examples in the chapter on structures and records.

我们已经讨论过依值积类型（dependent product type）Sigma：We have already discussed the dependent product type Sigma:

库中还有两个归纳类型的例子如下：Two more examples of inductive types in the library are the following:

在依值类型论的语义中，没有内建的偏函数（partial function）概念。函数类型 α → β 或依值函数类型 (a : α) → β 的每个元素都被假定在每个输入处都有一个值。Option 类型提供了一种表示偏函数的方式。Option β 的元素要么是 none，要么是形如 some b（对于某个值 b : β）。因此，我们可以将类型 α → Option β 的一个元素 f 看作从 α 到 β 的偏函数：对于每个 a : α，f a 要么返回 none（表示 f a “未定义”），要么返回 some b。In the semantics of dependent type theory, there is no built-in notion of a partial function. Every element of a function type α → β or a dependent function type (a : α) → β is assumed to have a value at every input. The Option type provides a way of representing partial functions. An element of Option β is either none or of the form some b, for some value b : β. Thus we can think of an element f of the type α → Option β as being a partial function from α to β: for every a : α, f a either returns none, indicating f a is “undefined”, or some b.

Inhabited α 的一个元素只是 α 中存在一个元素的证据。稍后，我们将看到 Inhabited 是 Lean 中类型类（type class）的一个例子：可以指示 Lean 哪些基础类型是 inhabited 的，Lean 可以在此基础上自动推断其他构造的类型是 inhabited 的。An element of Inhabited α is simply a witness to the fact that there is an element of α. Later, we will see that Inhabited is an example of a type class in Lean: Lean can be instructed that suitable base types are inhabited, and can automatically infer that other constructed types are inhabited on that basis.

作为练习，我们鼓励你为从 α 到 β 和从 β 到 γ 的偏函数开发一个复合（composition）概念，并证明其行为符合预期。我们还鼓励你证明 Bool 和 Nat 是 inhabited 的，两个 inhabited 类型的积类型是 inhabited 的，以及到 inhabited 类型的函数类型是 inhabited 的。As exercises, we encourage you to develop a notion of composition for partial functions from α to β and β to γ, and show that it behaves as expected. We also encourage you to show that Bool and Nat are inhabited, that the product of two inhabited types is inhabited, and that the type of functions to an inhabited type is inhabited.

7.3. 归纳定义的命题（Inductively Defined Propositions）7.3. Inductively Defined Propositions🔗

归纳定义的类型可以位于任何类型宇宙中，包括最底层的 Prop。事实上，这正是逻辑连接词的定义方式。Inductively defined types can live in any type universe, including the bottom-most one, Prop. In fact, this is exactly how the logical connectives are defined.

你应该思考这些如何产生你已经见过的引入规则和消去规则。有一些规则规定了归纳类型的消去子可以消去到什么，即，什么类型的类型可以作为递归子的目标。粗略地说，Prop 中的归纳类型的特征在于只能消去到 Prop 中的其他类型。这与以下理解一致：如果 p : Prop，那么元素 hp : p 不携带任何数据。然而，这条规则有一个小例外，我们将在下面的Inductive Families中讨论。You should think about how these give rise to the introduction and elimination rules that you have already seen. There are rules that govern what the eliminator of an inductive type can eliminate to, that is, what kinds of types can be the target of a recursor. Roughly speaking, what characterizes inductive types in Prop is that one can only eliminate to other types in Prop. This is consistent with the understanding that if p : Prop, an element hp : p carries no data. There is a small exception to this rule, however, which we will discuss below, in Inductive Families.

甚至存在量词（existential quantifier）也是归纳定义的：Even the existential quantifier is inductively defined:

请记住，记法 ∃ x : α, p 是 Exists (fun x : α => p) 的语法糖。Keep in mind that the notation ∃ x : α, p is syntactic sugar for Exists (fun x : α => p).

False、True、And 和 Or 的定义与 Empty、Unit、Prod 和 Sum 的定义完全类似。区别在于第一组产生 Prop 的元素，而第二组对某个 u 产生 Type u 的元素。类似地，∃ x : α, p 是 Σ x : α, β 的 Prop 值变体。The definitions of False, True, And, and Or are perfectly analogous to the definitions of Empty, Unit, Prod, and Sum. The difference is that the first group yields elements of Prop, and the second yields elements of Type u for some u. In a similar way, ∃ x : α, p is a Prop-valued variant of Σ x : α, β.

这是一个很好的地方来提及另一个归纳类型，记作 {x : α // p}，它有点像 ∃ x : α, p 和 Σ x : α, β 之间的混合体。This is a good place to mention another inductive type, denoted {x : α // p}, which is sort of a hybrid between ∃ x : α, p and Σ x : α, β.

事实上，在 Lean 中，Subtype 是使用结构体命令定义的：In fact, in Lean, Subtype is defined using the structure command:

记法 {x : α // p x} 是 Subtype (fun x : α => p x) 的语法糖。它仿照集合论中的子集记法：其思想是 {x : α // p x} 表示 α 中具有性质 p 的元素的集合。The notation {x : α // p x} is syntactic sugar for Subtype (fun x : α => p x). It is modeled after subset notation in set theory: the idea is that {x : α // p x} denotes the collection of elements of α that have property p.

7.4. 定义自然数（Defining the Natural Numbers）7.4. Defining the Natural Numbers🔗

到目前为止，我们看到的归纳定义类型都是“平坦的”：构造子包装数据并将其插入类型中，相应的递归子解包数据并对其进行操作。当构造子作用于正在定义的类型本身的元素时，情况就变得有趣得多了。一个典型的例子是自然数类型 Nat：The inductively defined types we have seen so far are “flat”: constructors wrap data and insert it into a type, and the corresponding recursor unpacks the data and acts on it. Things get much more interesting when the constructors act on elements of the very type being defined. A canonical example is the type Nat of natural numbers:

有两个构造子。我们从 zero : Nat 开始；它不接受参数，所以我们从一开始就有了它。相比之下，构造子 succ 只能应用于先前构造的 Nat。将其应用于 zero 得到 succ zero : Nat。再次应用得到 succ (succ zero) : Nat，依此类推。直观上，Nat 是包含这些构造子的“最小”类型，意味着它是由从 zero 开始并重复应用 succ 穷尽地（且自由地）生成的。There are two constructors. We start with zero : Nat; it takes no arguments, so we have it from the start. In contrast, the constructor succ can only be applied to a previously constructed Nat. Applying it to zero yields succ zero : Nat. Applying it again yields succ (succ zero) : Nat, and so on. Intuitively, Nat is the “smallest” type with these constructors, meaning that it is exhaustively (and freely) generated by starting with zero and applying succ repeatedly.

与之前一样，Nat 上的递归子旨在定义从 Nat 到任意值域（domain）的依值函数 f，即对于某个 motive : Nat → Sort u，是 (n : Nat) → motive n 的一个元素。它必须处理两种情况：输入为 zero 的情况，以及对某个 n : Nat 输入形如 succ n 的情况。在第一种情况下，我们像之前一样简单地指定一个具有适当类型的目标值。然而，在第二种情况下，递归子可以假设 f 在 n 处的值已经被计算出来了。因此，递归子的下一个参数根据 n 和 f n 指定 f (succ n) 的值。如果我们检查递归子的类型，会发现以下内容：As before, the recursor for Nat is designed to define a dependent function f from Nat to any domain, that is, an element f of (n : Nat) → motive n for some motive : Nat → Sort u. It has to handle two cases: the case where the input is zero, and the case where the input is of the form succ n for some n : Nat. In the first case, we simply specify a target value with the appropriate type, as before. In the second case, however, the recursor can assume that a value of f at n has already been computed. As a result, the next argument to the recursor specifies a value for f (succ n) in terms of n and f n. If we check the type of the recursor, you find the following:

隐式参数 motive 是所定义函数的余值域（codomain）。在类型论中，通常称 motive 为该消去/递归的动机（motive），因为它描述了我们想要构造的对象种类。接下来的两个参数如上所述指定了如何处理零和后继情况。它们也被称为次要前提（minor premises）。最后，t : Nat 是函数的输入。它也被称为主要前提（major premise）。The implicit argument, motive, is the codomain of the function being defined. In type theory it is common to say motive is the motive for the elimination/recursion, since it describes the kind of object we wish to construct. The next two arguments specify how to compute the zero and successor cases, as described above. They are also known as the minor premises. Finally, the t : Nat is the input to the function. It is also known as the major premise.

Nat.recOn 与 Nat.rec 类似，但主要前提出现在次要前提之前。The Nat.recOn is similar to Nat.rec but the major premise occurs before the minor premises.

考虑，例如，自然数上的加法函数 add m n。固定 m，我们可以通过 n 上的递归来定义加法。在基础情况中，我们设 add m zero 为 m。在后继步骤中，假设值 add m n 已经确定，我们定义 add m (succ n) 为 succ (add m n)。Consider, for example, the addition function add m n on the natural numbers. Fixing m, we can define addition by recursion on n. In the base case, we set add m zero to m. In the successor step, assuming the value add m n is already determined, we define add m (succ n) to be succ (add m n).

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

将这些定义放入命名空间 Nat 中很有用。然后我们可以在该命名空间中定义常用的记法。加法的两个定义方程现在定义性地成立：It is useful to put such definitions into a namespace, Nat. We can then go on to define familiar notation in that namespace. The two defining equations for addition now hold definitionally:

我们将在Type Classes一章中解释 instance 命令是如何工作的。在下面的例子中，我们将使用 Lean 版本的自然数。We will explain how the instance command works in the Type Classes chapter. In the examples below, we will use Lean's version of the natural numbers.

然而，证明像 0 + n = n 这样的事实需要归纳证明。如上所述，归纳原理只是递归原理的一个特例，即余值域 motive n 是 Prop 的一个元素的情况。它代表了归纳证明的熟悉模式：要证明 ∀ n, motive n，首先证明 motive 0，然后对任意 n，假设 ih : motive n 并证明 motive (n + 1)。Proving a fact like 0 + n = n, however, requires a proof by induction. As observed above, the induction principle is just a special case of the recursion principle, when the codomain motive n is an element of Prop. It represents the familiar pattern of an inductive proof: to prove ∀ n, motive n, first prove motive 0, and then, for arbitrary n, assume ih : motive n and prove motive (n + 1).

再次注意，当 Nat.recOn 在证明上下文中使用时，它实际上是伪装下的归纳原理。rw 和 simp 策略在类似的证明中往往非常有效。在这种情况下，每个都可以将证明简化为：Notice that, once again, when Nat.recOn is used in the context of a proof, it is really the induction principle in disguise. The rw and simp tactics tend to be very effective in proofs like these. In this case, each can be used to reduce the proof to: