8.1. 模式匹配🔗

对示意图模式的解释是编译过程的第一步。我们已经看到，casesOn 递归器可以通过分情况讨论来定义函数和证明定理， 根据归纳定义类型所涉及的构造子。但是复杂的定义可能会使用几个嵌套的 casesOn 应用， 而且可能很难阅读和理解。模式匹配提供了一种更方便的方法，并且为函数式编程语言的用户所熟悉。

考虑一下自然数的归纳定义类型。每个自然数要么是 zero，要么是 succ x， 因此你可以通过在每个情况下指定一个值来定义一个从自然数到任意类型的函数：

用来定义这些函数的方程在定义上是成立的：

我们可以用一些更耳熟能详的符号，而不是 zero 和 succ：

因为加法和零符号已经被赋予 [match_pattern] 属性，它们可以被用于模式匹配。Lean 简单地将这些表达式规范化， 直到显示构造子 zero 和 succ。

模式匹配适用于任何归纳类型，如乘积和 Option 类型：

在这里，我们不仅用它来定义一个函数，而且还用它来进行逐情况证明：

模式匹配也可以用来解构归纳定义的命题：

这样解决带逻辑连接词的命题就很紧凑。

在所有这些例子中，模式匹配被用来进行单一情况的区分。更有趣的是，模式可以涉及嵌套的构造子，如下面的例子。

方程编译器首先对输入是 zero 还是 succ x 的形式进行分类讨论，然后对 x 是 zero 还是 succ x 的形式进行分类讨论。 它从提交给它的模式中确定必要的情况拆分，如果模式不能穷尽情况，则会引发错误。同时，我们可以使用算术符号，如下面的版本。 在任何一种情况下，定义方程都是成立的。

你可以写 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 表达式。实际上，上面的定义被扩展为

下面是一些嵌套模式匹配的例子：

方程编译器可以按顺序处理多个参数。例如，将前面的例子定义为两个参数的函数会更自然：

另一例：

这些模式是由逗号分隔的。

在下面的每个例子中，尽管其他参数包括在模式列表中，但只对第一个参数进行了分割。

还要注意的是，当定义中不需要一个参数的值时，你可以用下划线来代替。这个下划线被称为 通配符模式 ，或 匿名变量 。与方程编译器之外的用法不同，这里的下划线 并不 表示一个隐参数。使用下划线表示通配符在函数式编程语言中是很常见的，所以 Lean 采用了这种符号。通配符和重叠模式一节阐述了通配符的概念，而不可访问模式一节解释了你如何在模式中使用隐参数。

正如归纳类型一章中所描述的，归纳数据类型可以依赖于参数。下面的例子使用模式匹配定义了 tail 函数。参数 α : Type u 是一个参数，出现在冒号之前，表示它不参与模式匹配。Lean 也允许参数出现在 : 之后，但需要显式的 match 才能模式匹配。

尽管参数 α 在这两个例子中的位置不同，但在这两种情况下，它的处理方式是一样的，即它不参与情况分割。

Lean 也可以处理更复杂的模式匹配形式，其中从属类型的参数对各种情况构成了额外的约束。 这种 依值模式匹配 的例子在 依值模式匹配一节中考虑。

8.2. 通配符和重叠模式🔗

考虑上节的一个例子：

也可以表述成：

在第二种表述中，模式是重叠的；例如，一对参数 0, 0 符合所有三种情况。但是 Lean 通过使用第一个适用的方程来处理这种模糊性， 所以在这个例子中，最终结果是一样的。特别是，以下方程在定义上是成立的：

由于不需要 m 和 n 的值，我们也可以用通配符模式代替。

你可以检查这个 foo 的定义是否满足与之前相同的定义特性。

一些函数式编程语言支持 不完整的模式 。在这些语言中，解释器对不完整的情况产生一个异常或返回一个任意的值。 我们可以使用 Inhabited （含元素的）类型类来模拟任意值的方法。粗略的说，Inhabited α 的一个元素是对 α 拥有一个元素的见证； 在 类型类一章中，我们将看到 Lean 可以被告知合适的基础类型是含元素的，并且可以自动推断出其他构造类型是含元素的。 在此基础上，标准库提供了一个任意元素 default，任何含元素的类型。

我们还可以使用类型 Option α 来模拟不完整的模式。我们的想法是对所提供的模式返回 some a， 而对不完整的情况使用 none。下面的例子演示了这两种方法。

方程编译器是很智能的。如果你遗漏了以下定义中的任何一种情况，错误信息会告诉你遗漏了哪个。

某些情况也可以用 if ... then ... else 代替 casesOn。

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. 结构化递归和归纳🔗

方程编译器的强大之处在于，它还支持递归定义。在接下来的三节中，我们将分别介绍。

• 结构性递归定义

• 良基的递归定义

• 相互递归的定义

一般来说，方程编译器处理以下形式的输入：

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

这里 (a : α) 是一个参数序列，(b : β) 是进行模式匹配的参数序列，γ 是任何类型， 它可以取决于 a 和 b。每一行应该包含相同数量的模式，对应于 β 的每个元素。 正如我们所看到的，模式要么是一个变量，要么是应用于其他模式的构造子，要么是一个正规化为该形式的表达式 （其中非构造子用 [match_pattern] 属性标记）。构造子的出现会提示情况拆分，构造子的参数由给定的变量表示。 在 依值模式匹配一节中，我们将看到有时有必要在模式中包含明确的项， 这些项需要进行表达式类型检查，尽管它们在模式匹配中没有起到作用。由于这个原因，这些被称为“不可访问的模式”。 但是在 依值模式匹配一节之前，我们将不需要使用这种不可访问的模式。

正如我们在上一节所看到的，项 t₁, ..., tₙ 可以利用任何一个参数 a，以及在相应模式中引入的任何一个变量。 使得递归和归纳成为可能的是，它们也可以涉及对 foo 的递归调用。在本节中，我们将处理 结构性递归 ， 其中 foo 的参数出现在 => 的右侧，是左侧模式的子项。我们的想法是，它们在结构上更小， 因此在归纳类型中出现在更早的阶段。下面是上一章的一些结构递归的例子，现在用方程编译器来定义：

zero_add 的证明清楚地表明，归纳证明实际上是 Lean 中的一种递归形式。

上面的例子表明，add 的定义方程具有定义意义，mul 也是如此。方程编译器试图确保在任何可能的情况下都是这样， 就像直接的结构归纳法一样。然而，在其他情况下，约简只在 命题 上成立，也就是说，它们是必须明确应用的方程定理。 方程编译器在内部生成这样的定理。用户不能直接使用它们；相反，simp 策略被配置为在必要时使用它们。 因此，对 zero_add 的以下两种证明都成立：

与模式匹配定义一样，结构递归或归纳的参数可能出现在冒号之前。在处理定义之前，简单地将这些参数添加到本地上下文中。 例如，加法的定义也可以写成这样：

你也可以用 match 来写上面的例子。

一个更有趣的结构递归的例子是斐波那契函数 fib。

这里，fib 函数在 n + 2 （定义上等于 succ (succ n) ）处的值是根据 n + 1 （定义上等价于 succ n ）和 n 处的值定义的。然而，这是一种众所周知的计算斐波那契函数的低效方法， 其执行时间是 n 的指数级。这里有一个更好的方法：

573147844013817084101

这里是使用 let rec 而不是 where 的相同定义。

在这两种情况下，Lean 都会生成辅助函数 fibFast.loop。

为了处理结构递归，方程编译器使用 值域 递归（course-of-values recursion），使用每个归纳定义类型自动生成的常量 below 和 brecOn。 你可以通过查看 Nat.below 和 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 : Nat) → C n 的依赖函数在特定输入 n 处的值。

使用值域递归是方程编译器用来向 Lean 内核证明函数终止的技术之一。它不影响代码生成器，代码生成器像其他函数式编程语言编译器一样编译递归函数。 回想一下，#eval fib <n> 在 <n> 上是指数级的。 另一方面，#reduce fib <n> 是高效的，因为它使用发送到内核的基于 brecOn 构造的定义。

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 函数。

这里还有另一个例子：它将第一个列表的元素添加到第二个列表的元素中，直到两个列表中的一个用完为止。

[5, 7, 9]

鼓励你在下面的练习中尝试类似的例子。

8.4. 局部递归声明🔗

你可以使用 let rec 关键字定义局部递归声明。

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

Lean 为每个 let rec 创建一个辅助声明。在上面的例子中，它为出现在 replicate 中的 let rec loop 创建了声明 replicate.loop。 注意，Lean 通过将出现在 let rec 声明中的任何局部变量添加为附加参数来“闭合”声明。例如，局部变量 a 出现在 let rec loop 中。

你也可以在策略模式下使用 let rec，以及用于创建归纳证明。

你也可以在定义之后使用 where 子句引入辅助递归声明。 Lean 将它们转换为 let rec。

8.5. 良基递归和归纳🔗

当无法使用结构递归时，我们可以使用良基递归来证明终止。 我们需要一个良基关系，以及一个证明，证明每个递归应用相对于该关系都是递减的。 依赖类型理论足够强大，可以编码和证明良基递归。让我们从理解其工作原理所需的逻辑背景开始。

Lean 的标准库定义了两个谓词 Acc r a 和 WellFounded r，其中 r 是类型 α 上的二元关系， a 是类型 α 的元素。

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 没有前驱，它是可访问的。给定任何类型 α， 我们应该能够递归地为 α 的每个可访问元素赋值，方法是首先为其所有前驱赋值。

关于 r 是良基的陈述，记为 WellFounded r，正是该类型的每个元素都是可访问的陈述。 根据上述考虑，如果 r 是类型 α 上的良基关系，我们应该在 α 上有一个关于关系 r 的良基递归原理。 确实，我们有：标准库定义了 WellFounded.fix，它正是用于此目的。

这里有很多角色，但我们已经看到了第一块：类型 α，关系 r，以及假设 h，即 r 是良基的。 变量 C 代表递归定义的动机：对于每个元素 x : α，我们想要构造一个 C x 的元素。 函数 F 提供了这样做的归纳配方：它告诉我们如何构造一个元素 C x，给定 x 的每个前驱 y 的 C y 元素。

注意，WellFounded.fix 同样可以作为归纳原理。它说如果 ≺ 是良基的，并且你想证明 ∀ x, C x， 只要证明对于任意 x，如果我们有 ∀ y, r y x → C y，那么我们有 C x 就足够了。

在上面的例子中，我们使用修饰符 noncomputable，因为代码生成器目前不支持 WellFounded.fix。 函数 WellFounded.fix 是 Lean 用来证明函数终止的另一个工具。

Lean 知道自然数上的通常顺序 < 是良基的。它还知道许多从其他良基顺序构造新良基顺序的方法，例如使用字典序。

这本质上是标准库中自然数除法的定义。

4

繁饰器（Elaborator）可以使这样的定义更加方便。它接受下列内容：

当 Lean 遇到递归定义时，它首先尝试结构递归，失败时才返回到良基递归。Lean 使用 decreasing_tactic 来显示递归应用会越来越小。 上面例子中的辅助命题 x - y < x 应该被视为这种策略的提示。

div 的定义公式不具有定义性，但我们可以使用 unfold 策略展开 div。 我们使用 conv 来选择要展开的 div 应用。