8.1. 模式匹配8.1. Pattern Matching🔗

模式图（schematic pattern）的解释是编译过程的第一步。我们已经看到，casesOn 递归子可以根据归纳定义类型（inductive type）中涉及的构造子，按情况用于定义函数和证明定理。但复杂的定义可能使用多个嵌套的 casesOn 应用，并且难以阅读和理解。模式匹配提供了一种更方便的方法，并且为函数式编程语言的用户所熟悉。The interpretation of schematic patterns is the first step of the compilation process. We have seen that the casesOn recursor can be used to define functions and prove theorems by cases, according to the constructors involved in an inductively defined type. But complicated definitions may use several nested casesOn applications, and may be hard to read and understand. Pattern matching provides an approach that is more convenient, and familiar to users of functional programming languages.

考虑自然数的归纳定义类型。每个自然数要么是 zero，要么是 succ x，因此你可以通过指定每种情况下的值来定义从自然数到任意类型的函数：Consider the inductively defined type of natural numbers. Every natural number is either zero or succ x, and so you can define a function from the natural numbers to an arbitrary type by specifying a value in each of those cases:

用于定义这些函数的方程在定义上成立（hold definitionally）：The equations used to define these functions hold definitionally:

除了 zero 和 succ，我们可以使用更熟悉的符号：Instead of zero and succ, we can use more familiar notation:

由于加法和零符号已被赋予 [match_pattern] 属性，它们可以在模式匹配中使用。Lean 只是将这些表达式归一化（normalize），直到构造子 zero 和 succ 被暴露出来。Because addition and the zero notation have been assigned the [match_pattern] attribute, they can be used in pattern matching. Lean simply normalizes these expressions until the constructors zero and succ are exposed.

模式匹配适用于任何归纳类型，例如积类型（product）和选项类型（option type）：Pattern matching works with any inductive type, such as products and option types:

这里我们不仅用它来定义函数，还用来按情况执行证明：Here we use it not only to define a function, but also to carry out a proof by cases:

模式匹配也可以用于析构（destruct）归纳定义的命题（proposition）：Pattern matching can also be used to destruct inductively defined propositions:

这提供了一种紧凑的方式来解包（unpack）使用逻辑连接词（logical connective）的假设。This provides a compact way of unpacking hypotheses that make use of logical connectives.

在所有这些例子中，模式匹配用于执行单个情况区分。更有趣的是，模式可以包含嵌套的构造子，如下面的例子所示。In all these examples, pattern matching was used to carry out a single case distinction. More interestingly, patterns can involve nested constructors, as in the following examples.

方程编译器首先根据输入是 zero 还是形如 succ x 进行情况分割。然后它继续对 x 是 zero 还是 succ x 进行情况分割。它从提供给它的模式中确定必要的情况分割，如果模式未能穷尽所有情况，则引发错误。同样，我们可以使用算术符号，如以下版本所示。无论哪种情况，定义方程都在定义上成立。The equation compiler first splits on cases as to whether the input is zero or of the form succ x. It then does a case split on whether x is of the form zero or succ x. It determines the necessary case splits from the patterns that are presented to it, and raises an error if the patterns fail to exhaust the cases. Once again, we can use arithmetic notation, as in the version below. In either case, the defining equations hold definitionally.

你可以写 def sub2 : Nat → Nat := fun x => match x with | 0 => 0 | 1 => 0 | x.succ.succ => x#print sub2 来看看该函数是如何被编译成递归子的。（Lean 会告诉你 sub2 是根据一个内部辅助函数 sub2.match_1 定义的，但你也可以打印出那个函数。）Lean 使用这些辅助函数来编译 match 表达式。实际上，上面的定义会被展开为You can write def sub2 : Nat → Nat := fun x => match x with | 0 => 0 | 1 => 0 | x.succ.succ => x#print sub2 to see how the function was compiled to recursors. (Lean will tell you that sub2 has been defined in terms of an internal auxiliary function, sub2.match_1, but you can print that out too.) Lean uses these auxiliary functions to compile match expressions. Actually, the definition above is expanded to

以下是一些嵌套模式匹配的更多例子：Here are some more examples of nested pattern matching:

方程编译器可以顺序地处理多个参数。例如，将前面的例子定义为两个参数的函数会更自然：The equation compiler can process multiple arguments sequentially. For example, it would be more natural to define the previous example as a function of two arguments:

这是另一个例子：Here is another example:

注意，模式之间用逗号分隔。Note that the patterns are separated by commas.

在以下每个例子中，即使其他参数也包含在模式列表中，分割也只发生在第一个参数上。In each of the following examples, splitting occurs on only the first argument, even though the others are included among the list of patterns.

还要注意，当某个参数的值在定义中不需要时，你可以使用下划线代替。这个下划线被称为通配符模式（wildcard pattern），或匿名变量（anonymous variable）。与方程编译器外部不同，这里的下划线并不表示隐式参数（implicit argument）。在函数式编程语言中，使用下划线作为通配符是很常见的，因此 Lean 采用了这种符号。关于通配符和重叠模式的部分进一步阐述了通配符的概念，而不可访问模式的描述解释了如何在模式中使用隐式参数。Notice also that, when the value of an argument is not needed in the definition, you can use an underscore instead. This underscore is known as a wildcard pattern, or an anonymous variable. In contrast to usage outside the equation compiler, here the underscore does not indicate an implicit argument. The use of underscores for wildcards is common in functional programming languages, and so Lean adopts that notation. The section on wildcards and overlapping patterns expands on the notion of a wildcard, and the description of inaccessible patterns explains how you can use implicit arguments in patterns as well.

如归纳类型中所述，归纳数据类型可以依赖于参数。下面的例子使用模式匹配定义了 tail 函数。参数 α : Type u 是一个参数，出现在冒号之前，表示它不参与模式匹配。Lean 也允许参数出现在 : 之后，但在它们上进行模式匹配需要显式的 match。As described in Inductive Types, inductive data types can depend on parameters. The following example defines the tail function using pattern matching. The argument α : Type u is a parameter and occurs before the colon to indicate it does not participate in the pattern matching. Lean also allows parameters to occur after the :, but pattern matching on them requires an explicit match.

尽管参数 α 在这两个例子中的位置不同，但在两种情况下它都以相同的方式处理，即不参与情况分割。Despite the different placement of the parameter α in these two examples, in both cases it is treated in the same way, in that it does not participate in a case split.

Lean 还可以处理更复杂的模式匹配形式，其中依赖类型（dependent type）的参数对不同的情况施加了额外的约束。这种依值模式匹配（dependent pattern matching）的例子将在依值模式匹配一节中讨论。Lean can also handle more complex forms of pattern matching, in which arguments to dependent types pose additional constraints on the various cases. Such examples of dependent pattern matching are considered in the section on dependent pattern matching.

8.2. 通配符与重叠模式8.2. Wildcards and Overlapping Patterns🔗

考虑上一节中的一个例子：Consider one of the examples from the last section:

另一种表示方式是：An alternative presentation is:

在第二种表示中，模式是重叠的；例如，参数对 0, 0 匹配所有三种情况。但 Lean 通过使用第一个适用的方程来处理歧义，因此在这个例子中最终结果是一样的。特别地，以下方程在定义上成立：In the second presentation, the patterns overlap; for example, the pair of arguments 0, 0 matches all three cases. But Lean handles the ambiguity by using the first applicable equation, so in this example the net result is the same. In particular, the following equations hold definitionally:

由于 m 和 n 的值不需要，我们完全可以使用通配符模式。Since the values of m and n are not needed, we can just as well use wildcard patterns instead.

你可以验证这个 foo 的定义满足与之前相同的定义恒等式。You can check that this definition of foo satisfies the same definitional identities as before.

一些函数式编程语言支持不完全模式（incomplete pattern）。在这些语言中，解释器会对不完全的情况产生异常或返回一个任意值。我们可以使用 Inhabited 类型类（type class）来模拟任意值的方法。大致来说，Inhabited α 的一个元素是 α 中存在一个元素的见证；在关于类型类的章节中，我们将看到可以指示 Lean 适当的基本类型是 inhabited 的，并且可以自动推断其他构造的类型是 inhabited 的。在此基础上，标准库为任何 inhabited 的类型提供了一个默认元素 default。Some functional programming languages support incomplete patterns. In these languages, the interpreter produces an exception or returns an arbitrary value for incomplete cases. We can simulate the arbitrary value approach using the Inhabited type class. Roughly, an element of Inhabited α is a witness to the fact that there is an element of α; in the chapter on type classes we will see that Lean can be instructed that suitable base types are inhabited, and can automatically infer that other constructed types are inhabited. On this basis, the standard library provides a default element, default, of any inhabited type.

我们也可以使用 Option α 类型来模拟不完全模式。思路是对提供的模式返回 some a，对不完全的情况使用 none。下面的例子演示了这两种方法。We can also use the type Option α to simulate incomplete patterns. The idea is to return some a for the provided patterns, and use none for the incomplete cases. The following example demonstrates both approaches.

方程编译器很聪明。如果你在下面的定义中遗漏了任何情况，错误信息会告诉你哪些情况没有被覆盖。The equation compiler is clever. If you leave out any of the cases in the following definition, the error message will let you know what has not been covered.

在适当的情况下，它也会使用 if ... then ... else 而不是 casesOn。It will also use an if ... then ... else instead of a casesOn in appropriate situations.

def foo.match_1.{u_1} : (motive : Char → Sort u_1) →
  (x : Char) → (Unit → motive 'A') → (Unit → motive 'B') → ((x : Char) → motive x) → motive x :=
fun motive x h_1 h_2 h_3 =>
  if h_1_1 : x = 'A' then Eq.symm h_1_1 ▸ Eq.symm h_1_1 ▸ h_1 ()
  else
    if h_2_1 : x = 'B' then
      Eq.ndrec (motive := fun x => ¬x = 'A' → motive x) (fun h_1 => Eq.symm h_2_1 ▸ h_2 ()) (Eq.symm h_2_1) h_1_1
    else h_3 x

8.3. 结构递归与归纳8.3. Structural Recursion and Induction🔗

使方程编译器强大的是它还支持递归定义。在接下来的三节中，我们将分别描述：What makes the equation compiler powerful is that it also supports recursive definitions. In the next three sections, we will describe, respectively:

• 结构递归（structurally recursive）定义structurally recursive definitions

• 良基递归（well-founded recursive）定义well-founded recursive definitions

• 互递归（mutually recursive）定义mutually recursive definitions

一般来说，方程编译器处理以下形式的输入：Generally speaking, the equation compiler processes input of the following form:

def foo (a : α) : (b : β) → γ
  | [patterns₁] => t₁
  ...
  | [patternsₙ] => tₙ

这里 (a : α) 是一个参数序列，(b : β) 是执行模式匹配的参数序列，而 γ 是任意类型，可以依赖于 a 和 b。每一行应包含相同数量的模式，每个 β 中的元素对应一个模式。如我们所见，模式要么是一个变量，要么是一个应用于其他模式的构造子，要么是一个归一化为这种形式的表达式（其中非构造子用 [match_pattern] 属性标记）。构造子的出现引发情况分割，构造子的参数由给定的变量表示。在依值模式匹配一节中，我们将看到，模式中的一些显式项被迫采用特定形式以使表达式的类型检查通过，尽管它们在模式匹配中不起作用。由于这个原因，它们被称为"不可访问模式（inaccessible patterns）"。但在介绍依值模式匹配之前，我们不需要使用这样的不可访问模式。Here (a : α) is a sequence of parameters, (b : β) is the sequence of arguments on which pattern matching takes place, and γ is any type, which can depend on a and b. Each line should contain the same number of patterns, one for each element of β. As we have seen, a pattern is either a variable, a constructor applied to other patterns, or an expression that normalizes to something of that form (where the non-constructors are marked with the [match_pattern] attribute). The appearances of constructors prompt case splits, with the arguments to the constructors represented by the given variables. In the section on dependent pattern matching, we will see that some explicit terms in patterns are forced into a particular form in order to make an expression type check, though they do not play a role in pattern matching. These are called “inaccessible patterns” for that reason. But we will not need to use such inaccessible patterns before covering dependent pattern matching.

如上一节所述，项 t₁, ..., tₙ 可以使用任何参数 a，以及相应模式中引入的任何变量。递归和归纳之所以可能，是因为它们还可以涉及对 foo 的递归调用。在本节中，我们将处理结构递归（structural recursion），其中出现在 => 右侧的 foo 的参数是左侧模式的子项。其思想是它们在结构上更小，因此出现在归纳类型的更早阶段。以下是上一章中结构递归的一些例子，现在使用方程编译器定义：As we saw in the last section, the terms t₁, ..., tₙ can make use of any of the parameters a, as well as any of the variables that are introduced in the corresponding patterns. What makes recursion and induction possible is that they can also involve recursive calls to foo. In this section, we will deal with structural recursion, in which the arguments to foo occurring on the right-hand side of the => are subterms of the patterns on the left-hand side. The idea is that they are structurally smaller, and hence appear in the inductive type at an earlier stage. Here are some examples of structural recursion from the last chapter, now defined using the equation compiler:

zero_add 的证明表明，归纳证明（proof by induction）在 Lean 中实际上是一种递归形式。The proof of zero_add makes it clear that proof by induction is really a form of recursion in Lean.

上面的例子表明，add 的定义方程在定义上成立，mul 也是如此。方程编译器尽可能确保这一点成立，就像直接的结构归纳（structural induction）那样。然而，在其他情况下，规约（reduction）只在命题上（propositionally）成立，也就是说，它们是必须显式应用的等式定理。方程编译器在内部生成这样的定理。它们并非供用户直接使用；相反，simp 策略（tactic）被配置为在必要时使用它们。以下 zero_add 的证明就是以这种方式工作的：The example above shows that the defining equations for add hold definitionally, and the same is true of mul. The equation compiler tries to ensure that this holds whenever possible, as is the case with straightforward structural induction. In other situations, however, reductions hold only propositionally, which is to say, they are equational theorems that must be applied explicitly. The equation compiler generates such theorems internally. They are not meant to be used directly by the user; rather, the simp tactic is configured to use them when necessary. The following proof of zero_add works this way:

与通过模式匹配定义一样，结构递归或归纳的参数可以出现在冒号之前。这些参数在处理定义之前被简单地添加到本地上下文中。例如，加法的定义也可以写成如下形式：As with definition by pattern matching, parameters to a structural recursion or induction may appear before the colon. Such parameters are simply added to the local context before the definition is processed. For example, the definition of addition may also be written as follows:

你也可以使用 match 来编写上面的例子。You can also write the example above using match.

结构递归的一个更有趣的例子是斐波那契函数 fib。A more interesting example of structural recursion is given by the Fibonacci function fib.

这里，fib 函数在 n + 2（在定义上等于 succ (succ n)）处的值根据其在 n + 1（在定义上等价于 succ n）和 n 处的值定义。然而，这是一种计算斐波那契函数的众所周知的低效方法，其执行时间相对于 n 是指数级的。以下是一种更好的方法：Here, the value of the fib function at n + 2 (which is definitionally equal to succ (succ n)) is defined in terms of the values at n + 1 (which is definitionally equivalent to succ n) and the value at n. This is a notoriously inefficient way of computing the Fibonacci function, however, with an execution time that is exponential in n. Here is a better way:

573147844013817084101

以下是使用 let rec 而不是 where 的相同定义。Here is the same definition using a let rec instead of a where.

在两种情况下，Lean 都会生成辅助函数 fibFast.loop。In both cases, Lean generates the auxiliary function fibFast.loop.

为了处理结构递归，方程编译器使用值域递归（course-of-values recursion），使用每个归纳定义类型自动生成的常量 below 和 brecOn。你可以通过查看 Nat.below 和 Nat.brecOn 的类型来了解其工作原理：To handle structural recursion, the equation compiler uses course-of-values recursion, using constants below and brecOn that are automatically generated with each inductively defined type. You can get a sense of how it works by looking at the types of Nat.below and Nat.brecOn:

Nat.below : Nat → Type u

Nat.below 3

Nat.brecOn : (t : Nat) → ((t : Nat) → Nat.below t → C t) → C t

类型 @Nat.below C (3 : Nat) 是一个存储 C 0、C 1 和 C 2 的数据结构。值域递归由 Nat.brecOn 实现。它使我们能够根据函数的所有先前值（以 @Nat.below C n 的一个元素的形式呈现），在特定输入 n 处定义类型为 (n : Nat) → C n 的依值函数的值。The type @Nat.below C (3 : Nat) is a data structure that stores elements of C 0, C 1, and C 2. The course-of-values recursion is implemented by Nat.brecOn. It enables us to define the value of a dependent function of type (n : Nat) → C n at a particular input n in terms of all the previous values of the function, presented as an element of @Nat.below C n.

使用值域递归是方程编译器用于向 Lean 内核证明函数终止的技术之一。它不影响代码生成器，该生成器像其他函数式编程语言编译器一样编译递归函数。回想一下，#eval fib <n> 相对于 <n> 是指数级的。另一方面，#reduce fib <n> 是高效的，因为它使用发送给内核的基于 brecOn 结构的定义。The use of course-of-values recursion is one of the techniques the equation compiler uses to justify to the Lean kernel that a function terminates. It does not affect the code generator which compiles recursive functions as other functional programming language compilers. Recall that #eval fib <n> is exponential in <n>. On the other hand, #reduce fib <n> is efficient because it uses the definition sent to the kernel that is based on the brecOn construction.

20365011074

def fib : Nat → Nat :=
fun x =>
  Nat.brecOn x fun x f =>
    (match (motive := (x : Nat) → Nat.below x → Nat) x with
      | 0 => fun x => 1
      | 1 => fun x => 1
      | n.succ.succ => fun x => x.1 + x.2.1)
      f

递归定义的另一个好例子是列表的 append 函数。Another good example of a recursive definition is the list append function.

这是另一个例子：它将第一个列表的元素添加到第二个列表的元素中，直到两个列表中的一个耗尽。Here is another: it adds elements of the first list to elements of the second list, until one of the two lists runs out.

[5, 7, 9]

鼓励你在下面的练习中尝试类似的例子。You are encouraged to experiment with similar examples in the exercises below.

8.4. 局部递归声明8.4. Local recursive declarations🔗

你可以使用 let rec 关键字定义局部递归声明。You can define local recursive declarations using the let rec keyword.

@replicate.loop : {α : Type u_1} → α → Nat → List α → List α

Lean 为每个 let rec 创建一个辅助声明。在上面的例子中，它为 replicate 中出现的 let rec loop 创建了声明 replicate.loop。请注意，Lean 通过将 let rec 声明中出现的任何局部变量作为附加参数添加来"闭合（close）"该声明。例如，局部变量 a 出现在 let rec loop 中。Lean creates an auxiliary declaration for each let rec. In the example above, it created the declaration replicate.loop for the let rec loop occurring at replicate. Note that, Lean “closes” the declaration by adding any local variable occurring in the let rec declaration as additional parameters. For example, the local variable a occurs at let rec loop.

你也可以在策略模式（tactic mode）中使用 let rec，以及用于创建归纳证明。You can also use let rec in tactic mode and for creating proofs by induction.

你也可以在定义后使用 where 子句引入辅助递归声明。Lean 会将它们转换为 let rec。You can also introduce auxiliary recursive declarations using where clause after your definition. Lean converts them into a let rec.

8.5. 良基递归与归纳8.5. Well-Founded Recursion and Induction🔗

当无法使用结构递归时，我们可以使用良基递归（well-founded recursion）来证明终止。我们需要一个良基关系（well-founded relation），以及每个递归应用相对于该关系是递减的证明。依值类型论（dependent type theory）足够强大，可以编码和证明良基递归。让我们从理解其工作原理所需的逻辑背景开始。When structural recursion cannot be used, we can prove termination using well-founded recursion. We need a well-founded relation and a proof that each recursive application is decreasing with respect to this relation. Dependent type theory is powerful enough to encode and justify well-founded recursion. Let us start with the logical background that is needed to understand how it works.

Lean 的标准库定义了两个谓词（predicate），Acc r a 和 WellFounded r，其中 r 是类型 α 上的一个二元关系，a 是类型 α 的一个元素。Lean's standard library defines two predicates, Acc r a and WellFounded r, where r is a binary relation on a type α, and a is an element of type α.

Acc r : α → Prop

WellFounded r : Prop

第一个，Acc，是一个归纳定义的谓词。根据其定义，Acc r x 等价于 ∀ y, r y x → Acc r y。如果你将 r y x 视为某种顺序关系 y ≺ x，那么 Acc r x 表示 x 是从下面可访问的，即它的所有前驱都是可访问的。特别地，如果 x 没有前驱，则它是可访问的。给定任意类型 α，我们应该能够递归地给 α 的每个可访问元素赋值，方法是先给它的所有前驱赋值。The first, Acc, is an inductively defined predicate. According to its definition, Acc r x is equivalent to ∀ y, r y x → Acc r y. If you think of r y x as denoting a kind of order relation y ≺ x, then Acc r x says that x is accessible from below, in the sense that all its predecessors are accessible. In particular, if x has no predecessors, it is accessible. Given any type α, we should be able to assign a value to each accessible element of α, recursively, by assigning values to all its predecessors first.

r 是良基的断言，记为 WellFounded r，正是该类型的每个元素都是可访问的。根据上述考虑，如果 r 是类型 α 上的良基关系，那么我们应该有一个在 α 上关于关系 r 的良基递归原理。事实上，我们确实有：标准库定义了 WellFounded.fix，它正是用于这个目的。The statement that r is well-founded, denoted WellFounded r, is exactly the statement that every element of the type is accessible. By the above considerations, if r is a well-founded relation on a type α, we should have a principle of well-founded recursion on α, with respect to the relation r. And, indeed, we do: the standard library defines WellFounded.fix, which serves exactly that purpose.

这里有一长串角色，但第一个块我们已经见过：类型 α、关系 r 以及 r 是良基的假设 h。变量 C 表示递归定义的动机（motive）：对每个元素 x : α，我们希望构造 C x 的一个元素。函数 F 提供了实现这一点的归纳方案：它告诉我们如何在给定 x 的每个前驱 y 的 C y 元素的情况下构造 C x 的一个元素。There is a long cast of characters here, but the first block we have already seen: the type, α, the relation, r, and the assumption, h, that r is well-founded. The variable C represents the motive of the recursive definition: for each element x : α, we would like to construct an element of C x. The function F provides the inductive recipe for doing that: it tells us how to construct an element C x, given elements of C y for each predecessor y of x.

注意，WellFounded.fix 同样可以作为归纳原理使用。它表明，如果 ≺ 是良基的，并且你想要证明 ∀ x, C x，那么只需证明对于任意 x，如果我们有 ∀ y, r y x → C y，那么我们有 C x。Note that WellFounded.fix works equally well as an induction principle. It says that if ≺ is well-founded and you want to prove ∀ x, C x, it suffices to show that for an arbitrary x, if we have ∀ y, r y x → C y, then we have C x.

在上面的例子中，我们使用了修饰符 noncomputable，因为代码生成器目前不支持 WellFounded.fix。函数 WellFounded.fix 是 Lean 用来证明函数终止的另一个工具。In the example above we use the modifier noncomputable because the code generator currently does not support WellFounded.fix. The function WellFounded.fix is another tool Lean uses to justify that a function terminates.

Lean 知道自然数上的通常顺序 < 是良基的。它也知道多种从其他良基序构造新良基序的方法，例如使用字典序（lexicographic order）。Lean knows that the usual order < on the natural numbers is well founded. It also knows a number of ways of constructing new well founded orders from others, for example, using lexicographic order.

以下本质上是标准库中自然数除法的定义。Here is essentially the definition of division on the natural numbers that is found in the standard library.