induction_and_recursion.md

归纳和递归

在上一章中，我们看到归纳定义提供了在 Lean 中引入新类型的强大手段。此外，构造子和递归器提供了在这些类型上定义函数的唯一手段。命题即类型的对应关系，意味着归纳法是证明的基本方法。

Lean 提供了定义递归函数、执行模式匹配和编写归纳证明的自然方法。它允许你通过指定它应该满足的方程来定义一个函数，它允许你通过指定如何处理可能出现的各种情况来证明一个定理。在它内部，这些描述被「方程编译器」程序「编译」成原始递归器。方程编译器不是可信代码库的一部分；它的输出包括由内核独立检查的项。

模式匹配

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

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

open Nat

def sub1 : Nat → Nat
  | zero   => zero
  | succ x => x

def isZero : Nat → Bool
  | zero   => true
  | succ x => false

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

# open Nat
# def sub1 : Nat → Nat
#   | zero   => zero
#   | succ x => x
# def isZero : Nat → Bool
#   | zero   => true
#   | succ x => false
example : sub1 0 = 0 := rfl
example (x : Nat) : sub1 (succ x) = x := rfl

example : isZero 0 = true := rfl
example (x : Nat) : isZero (succ x) = false := rfl

example : sub1 7 = 6 := rfl
example (x : Nat) : isZero (x + 3) = false := rfl

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

def sub1 : Nat → Nat
  | 0   => 0
  | x+1 => x

def isZero : Nat → Bool
  | 0   => true
  | x+1 => false

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

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

def swap : α × β → β × α
  | (a, b) => (b, a)

def foo : Nat × Nat → Nat
  | (m, n) => m + n

def bar : Option Nat → Nat
  | some n => n + 1
  | none   => 0

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

# namespace Hidden
def not : Bool → Bool
  | true  => false
  | false => true

theorem not_not : ∀ (b : Bool), not (not b) = b
  | true  => rfl  -- proof that not (not true) = true
  | false => rfl  -- proof that not (not false) = false
# end Hidden

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

example (p q : Prop) : p ∧ q → q ∧ p
  | And.intro h₁ h₂ => And.intro h₂ h₁

example (p q : Prop) : p ∨ q → q ∨ p
  | Or.inl hp => Or.inr hp
  | Or.inr hq => Or.inl hq

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

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

def sub2 : Nat → Nat
  | 0   => 0
  | 1   => 0
  | x+2 => x

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

# def sub2 : Nat → Nat
#   | 0   => 0
#   | 1   => 0
#   | x+2 => x
example : sub2 0 = 0 := rfl
example : sub2 1 = 0 := rfl
example : sub2 (x+2) = x := rfl

example : sub2 5 = 3 := rfl

你可以写 #print sub2 来看看这个函数是如何被编译成递归器的。（Lean 会告诉你 sub2 已经被定义为内部辅助函数 sub2.match_1，但你也可以把它打印出来）。Lean 使用这些辅助函数来编译 match 表达式。实际上，上面的定义被扩展为

def sub2 : Nat → Nat :=
  fun x =>
    match x with
    | 0   => 0
    | 1   => 0
    | x+2 => x

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

example (p q : α → Prop)
        : (∃ x, p x ∨ q x) → (∃ x, p x) ∨ (∃ x, q x)
  | Exists.intro x (Or.inl px) => Or.inl (Exists.intro x px)
  | Exists.intro x (Or.inr qx) => Or.inr (Exists.intro x qx)

def foo : Nat × Nat → Nat
  | (0, n)     => 0
  | (m+1, 0)   => 1
  | (m+1, n+1) => 2

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

def foo : Nat → Nat → Nat
  | 0,   n   => 0
  | m+1, 0   => 1
  | m+1, n+1 => 2

另一例：

def bar : List Nat → List Nat → Nat
  | [],      []      => 0
  | a :: as, []      => a
  | [],      b :: bs => b
  | a :: as, b :: bs => a + b

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

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

# namespace Hidden
def and : Bool → Bool → Bool
  | true,  a => a
  | false, _ => false

def or : Bool → Bool → Bool
  | true,  _ => true
  | false, a => a

def cond : Bool → α → α → α
  | true,  x, y => x
  | false, x, y => y
# end Hidden

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

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

def tail1 {α : Type u} : List α → List α
  | []      => []
  | a :: as => as

def tail2 : {α : Type u} → List α → List α
  | α, []      => []
  | α, a :: as => as

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

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

通配符和重叠模式

考虑上节的一个例子：

def foo : Nat → Nat → Nat
  | 0,   n   => 0
  | m+1, 0   => 1
  | m+1, n+1 => 2

也可以表述成

def foo : Nat → Nat → Nat
  | 0, n => 0
  | m, 0 => 1
  | m, n => 2

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

# def foo : Nat → Nat → Nat
#   | 0, n => 0
#   | m, 0 => 1
#   | m, n => 2
example : foo 0     0     = 0 := rfl
example : foo 0     (n+1) = 0 := rfl
example : foo (m+1) 0     = 1 := rfl
example : foo (m+1) (n+1) = 2 := rfl

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

def foo : Nat → Nat → Nat
  | 0, _ => 0
  | _, 0 => 1
  | _, _ => 2

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

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

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

def f1 : Nat → Nat → Nat
  | 0, _  => 1
  | _, 0  => 2
  | _, _  => default  -- 不完整的模式

example : f1 0     0     = 1       := rfl
example : f1 0     (a+1) = 1       := rfl
example : f1 (a+1) 0     = 2       := rfl
example : f1 (a+1) (b+1) = default := rfl

def f2 : Nat → Nat → Option Nat
  | 0, _  => some 1
  | _, 0  => some 2
  | _, _  => none     -- 不完整的模式

example : f2 0     0     = some 1 := rfl
example : f2 0     (a+1) = some 1 := rfl
example : f2 (a+1) 0     = some 2 := rfl
example : f2 (a+1) (b+1) = none   := rfl

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

def bar : Nat → List Nat → Bool → Nat
  | 0,   _,      false => 0
  | 0,   b :: _, _     => b
  | 0,   [],     true  => 7
  | a+1, [],     false => a
  | a+1, [],     true  => a + 1
  | a+1, b :: _, _     => a + b

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

def foo : Char → Nat
  | 'A' => 1
  | 'B' => 2
  | _   => 3

#print foo.match_1

结构化递归和归纳

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

• 结构性递归定义
• 良基的递归定义
• 相互递归的定义

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

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

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

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

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

theorem add_zero (m : Nat)   : add m zero = m := rfl
theorem add_succ (m n : Nat) : add m (succ n) = succ (add m n) := rfl

theorem zero_add : ∀ n, add zero n = n
  | zero   => rfl
  | succ n => congrArg succ (zero_add n)

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

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

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

open Nat
# def add : Nat → Nat → Nat
#   | m, zero   => m
#   | m, succ n => succ (add m n)
theorem zero_add : ∀ n, add zero n = n
  | zero   => by simp [add]
  | succ n => by simp [add, zero_add]

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

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

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

open Nat
def add (m n : Nat) : Nat :=
  match n with
  | zero   => m
  | succ n => succ (add m n)

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

def fib : Nat → Nat
  | 0   => 1
  | 1   => 1
  | n+2 => fib (n+1) + fib n

example : fib 0 = 1 := rfl
example : fib 1 = 1 := rfl
example : fib (n + 2) = fib (n + 1) + fib n := rfl

example : fib 7 = 21 := rfl

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

def fibFast (n : Nat) : Nat :=
  (loop n).2
where
  loop : Nat → Nat × Nat
    | 0   => (0, 1)
    | n+1 => let p := loop n; (p.2, p.1 + p.2)

#eval fibFast 100

下面是相同的定义，使用 let rec 代替 where。

def fibFast (n : Nat) : Nat :=
  let rec loop : Nat → Nat × Nat
    | 0   => (0, 1)
    | n+1 => let p := loop n; (p.2, p.1 + p.2)
  (loop n).2

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

为了处理结构递归，方程编译器使用 值过程 （course-of-values）递归，使用由每个归纳定义类型自动生成的常量 below 和 brecOn。你可以通过查看 Nat.below 和 Nat.brecOn 的类型来了解它是如何工作的。

variable (C : Nat → Type u)

#check (@Nat.below C : Nat → Type u)

#reduce @Nat.below C (3 : Nat)

#check (@Nat.brecOn C : (n : Nat) → ((n : Nat) → @Nat.below C n → C n) → C n)

类型 @Nat.below C (3 : nat) 是一个存储着 C 0，C 1，和 C 2 中元素的数据结构。值过程递归由 Nat.brecOn 实现。它根据该函数之前的所有值，定义类型为 (n : Nat) → C n 的依值函数在特定输入 n 时的值，表示为 @Nat.below C n 的一个元素。

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

def fib : Nat → Nat
  | 0   => 1
  | 1   => 1
  | n+2 => fib (n+1) + fib n

-- #eval fib 50 -- 这个很慢
#reduce fib 50  -- 用这个，这个快

#print fib

另一个递归定义的好例子是列表的 append 函数。

def append : List α → List α → List α
  | [],    bs => bs
  | a::as, bs => a :: append as bs

example : append [1, 2, 3] [4, 5] = [1, 2, 3, 4, 5] := rfl

这里是另一个：它将第一个列表中的元素和第二个列表中的元素分别相加，直到两个列表中的一个用尽。

def listAdd [Add α] : List α → List α → List α
  | [],      _       => []
  | _,       []      => []
  | a :: as, b :: bs => (a + b) :: listAdd as bs

#eval listAdd [1, 2, 3] [4, 5, 6, 6, 9, 10]
-- [5, 7, 9]

你可以在章末练习中尝试类似的例子。

局域递归声明

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

def replicate (n : Nat) (a : α) : List α :=
  let rec loop : Nat → List α → List α
    | 0,   as => as
    | n+1, as => loop n (a::as)
  loop n []

#check @replicate.loop
-- {α : Type} → α → Nat → List α → List α

Lean 为每个 let rec 创建一个辅助声明。在上面的例子中，它对于出现在 replicate 的 let rec loop 创建了声明 replication.loop。请注意，Lean 通过添加 let rec 声明中出现的任何局部变量作为附加参数来「关闭」声明。例如，局部变量 a 出现在 let rec 循环中。

你也可以在策略证明模式中使用 let rec，并通过归纳来创建证明。

# def replicate (n : Nat) (a : α) : List α :=
#  let rec loop : Nat → List α → List α
#    | 0,   as => as
#    | n+1, as => loop n (a::as)
#  loop n []
theorem length_replicate (n : Nat) (a : α) : (replicate n a).length = n := by
  let rec aux (n : Nat) (as : List α)
              : (replicate.loop a n as).length = n + as.length := by
    match n with
    | 0   => simp [replicate.loop]
    | n+1 => simp [replicate.loop, aux n, Nat.add_succ, Nat.succ_add]
  exact aux n []

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

def replicate (n : Nat) (a : α) : List α :=
  loop n []
where
  loop : Nat → List α → List α
    | 0,   as => as
    | n+1, as => loop n (a::as)

theorem length_replicate (n : Nat) (a : α) : (replicate n a).length = n := by
  exact aux n []
where
  aux (n : Nat) (as : List α)
      : (replicate.loop a n as).length = n + as.length := by
    match n with
    | 0   => simp [replicate.loop]
    | n+1 => simp [replicate.loop, aux n, Nat.add_succ, Nat.succ_add]

良基递归和归纳

当不能使用结构递归时，我们可以使用良基递归（well-founded recursion）来证明终止性。我们需要一个良基关系和一个证明每个递归调用相对于该关系都是递减的证明。依值类型理论具有足够的表达能力来编码和证明良基递归。让我们从理解其工作原理所需的逻辑背景开始。

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

variable (α : Sort u)
variable (r : α → α → Prop)

#check (Acc r : α → Prop)
#check (WellFounded r : Prop)

首先 Acc 是一个归纳定义的谓词。根据定义，Acc r x 等价于 ∀ y, r y x → Acc r y。如果你把 r y x 考虑成一种序关系 y ≺ x，那么 Acc r x 说明 x 在下文中可访问， 从某种意义上说，它的所有前继都是可访问的。特别地，如果 x 没有前继，它是可访问的。给定任何类型 α，我们应该能够通过首先为 α 的所有前继元素赋值，递归地为 α 的每个可访问元素赋值。

使用 WellFounded r 来声明 r 是良基的，即说明该类型的每个元素都是可访问的。根据上述考虑，如果 r 是类型 α 上的一个成立良好的关系，那么对于关系 r，我们应该有一个关于 α 的成立良好的递归原则。确实，我们这样做了：标准库定义了 WellFounded.fix，它正好满足这个目的。

noncomputable def f {α : Sort u}
      (r : α → α → Prop)
      (h : WellFounded r)
      (C : α → Sort v)
      (F : (x : α) → ((y : α) → r y x → C y) → C x)
      : (x : α) → C x := WellFounded.fix h F

这里有一大堆字，但我们熟悉第一块：类型 α，关系 r 和假设 h，即 r 是有良基的。变量' C 代表递归定义的动机：对于每个元素 x : α，我们想构造一个 C x 的元素。函数 F 提供了这样做的归纳方法：它告诉我们如何构造一个元素 C x，给定 C y 的元素对于 x 的每个 y。

注意 WellFounded.fix 和归纳法原理一样有效。它说如果 ≺ 是良基的，而你想要证明 ∀ x, C x，那么只要证明对于任意的 x，如果我们有 ∀ y ≺ x, C y，那么我们就有 C x 就足够了。

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

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

下面是标准库中自然数除法的定义。

open Nat

theorem div_lemma {x y : Nat} : 0 < y ∧ y ≤ x → x - y < x :=
  fun h => sub_lt (Nat.lt_of_lt_of_le h.left h.right) h.left

def div.F (x : Nat) (f : (x₁ : Nat) → x₁ < x → Nat → Nat) (y : Nat) : Nat :=
  if h : 0 < y ∧ y ≤ x then
    f (x - y) (div_lemma h) y + 1
  else
    zero

noncomputable def div := WellFounded.fix (measure id).wf div.F

#reduce div 8 2 -- 4

这个定义有点难以理解。这里递归在 x 上， div.F x f : Nat → Nat 为固定的 x 返回「除以 y」函数。你要记住 div.F 的第二个参数 f 是递归的具体实现，这个函数对所有小于 x 的自然数 x₁ 返回「除以 y」函数。

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

def div (x y : Nat) : Nat :=
  if h : 0 < y ∧ y ≤ x then
    have : x - y < x := Nat.sub_lt (Nat.lt_of_lt_of_le h.1 h.2) h.1
    div (x - y) y + 1
  else
    0

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

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

# def div (x y : Nat) : Nat :=
#  if h : 0 < y ∧ y ≤ x then
#    have : x - y < x := Nat.sub_lt (Nat.lt_of_lt_of_le h.1 h.2) h.1
#    div (x - y) y + 1
#  else
#    0
example (x y : Nat) : div x y = if 0 < y ∧ y ≤ x then div (x - y) y + 1 else 0 := by
  conv => lhs; unfold div -- 展开方程左侧的div

example (x y : Nat) (h : 0 < y ∧ y ≤ x) : div x y = div (x - y) y + 1 := by
  conv => lhs; unfold div
  simp [h]

下面的示例与此类似：它将任何自然数转换为二进制表达式，表示为0和1的列表。我们必须提供递归调用正在递减的证据，我们在这里用 sorry 来做。sorry 并不会阻止解释器成功地对函数求值。

def natToBin : Nat → List Nat
  | 0     => [0]
  | 1     => [1]
  | n + 2 =>
    have : (n + 2) / 2 < n + 2 := sorry
    natToBin ((n + 2) / 2) ++ [n % 2]

#eval natToBin 1234567

最后一个例子，我们观察到Ackermann函数可以直接定义，因为它可以被自然数上字典序的良基性证明。termination_by 子句指示 Lean 使用字典序。这个子句实际上是将函数参数映射到类型为 Nat × Nat 的元素。然后，Lean 使用类型类解析来合成类型为 WellFoundedRelation (Nat × Nat) 的元素。

def ack : Nat → Nat → Nat
  | 0,   y   => y+1
  | x+1, 0   => ack x 1
  | x+1, y+1 => ack x (ack (x+1) y)
termination_by x y => (x, y)

注意，在上面的例子中使用了字典序，因为实例 WellFoundedRelation (α × β) 使用了字典序。Lean 还定义了实例

instance (priority := low) [SizeOf α] : WellFoundedRelation α :=
  sizeOfWFRel

在下面的例子中，我们通过显示 as.size - i 在递归应用中是递减的来证明它会终止。

def takeWhile (p : α → Bool) (as : Array α) : Array α :=
  go 0 #[]
where
  go (i : Nat) (r : Array α) : Array α :=
    if h : i < as.size then
      let a := as.get ⟨i, h⟩
      if p a then
        go (i+1) (r.push a)
      else
        r
    else
      r
  termination_by as.size - i

注意，辅助函数 go 在这个例子中是递归的，但 takeWhile 不是。

默认情况下，Lean 使用 decreasing_tactic 来证明递归应用正在递减。修饰词 decreasing_by 允许我们提供自己的策略。这里有一个例子。

theorem div_lemma {x y : Nat} : 0 < y ∧ y ≤ x → x - y < x :=
  fun ⟨ypos, ylex⟩ => Nat.sub_lt (Nat.lt_of_lt_of_le ypos ylex) ypos

def div (x y : Nat) : Nat :=
  if h : 0 < y ∧ y ≤ x then
    div (x - y) y + 1
  else
    0
decreasing_by apply div_lemma; assumption

注意 decreasing_by 不是 termination_by 的替代，它们是互补的。 termination_by 用于指定一个良基关系， decreasing_by 用于提供我们自己的策略来显示递归应用正在递减。在下面的示例中，我们将同时使用它们。

def ack : Nat → Nat → Nat
  | 0,   y   => y+1
  | x+1, 0   => ack x 1
  | x+1, y+1 => ack x (ack (x+1) y)
termination_by x y => (x, y)
decreasing_by
  all_goals simp_wf -- 展开良基的递归辅助定义
  · apply Prod.Lex.left; simp_arith
  · apply Prod.Lex.right; simp_arith
  · apply Prod.Lex.left; simp_arith

我们可以使用 decreasing_by sorry 来指示 Lean 「相信」函数可以终止。

def natToBin : Nat → List Nat
  | 0     => [0]
  | 1     => [1]
  | n + 2 => natToBin ((n + 2) / 2) ++ [n % 2]
decreasing_by sorry

#eval natToBin 1234567

回想一下，使用 sorry 相当于使用一个新的公理，应该避免使用。在下面的例子中，我们用 sorry 来证明 False。命令 #print axioms 显示，unsound 依赖于用于实现 sorry 的不健全公理 sorryAx。

def unsound (x : Nat) : False :=
  unsound (x + 1)
decreasing_by sorry

#check unsound 0
-- `unsound 0` 是 `False` 的一个证明

#print axioms unsound
-- 'unsound' 依赖于公理：[sorryAx]

总结：

• 如果没有 termination_by，良基关系（可能）可以这样被导出：选择一个参数，然后使用类型类解析为该参数的类型合成一个良基关系。

• 如果指定了 termination_by，它将函数的参数映射为类型 α，并再次使用类型类解析。 回想一下，β × γ 的默认实例是基于 β 和 γ的良基关系的字典序。

• Nat 的默认良基关系实例是 <。

• 默认情况下，策略 decreasing_tactic 用于显示递归应用小于选择的良基关系。如果 decreasing_tactic 失败，错误信息包括剩余目标 ... |- G。注意，decreasing_tactic 使用 assumption。所以，你可以用 have 表达式来证明目标 G。你也可以使用 decreasing_by 来提供你自己的策略。

相互递归

Lean 还提供相互递归定义，语法类似相互归纳类型。例子：

mutual
  def even : Nat → Bool
    | 0   => true
    | n+1 => odd n

  def odd : Nat → Bool
    | 0   => false
    | n+1 => even n
end

example : even (a + 1) = odd a := by
  simp [even]

example : odd (a + 1) = even a := by
  simp [odd]

theorem even_eq_not_odd : ∀ a, even a = not (odd a) := by
  intro a; induction a
  . simp [even, odd]
  . simp [even, odd, *]

这是一个相互的定义，因为 even 是用 odd 递归定义的，而 odd 是用 even 递归定义的。在底层，它被编译为单个递归定义。内部定义的函数接受sum类型的元素作为参数，可以是 even 的输入，也可以是 odd 的输入。然后，它返回与输入相适应的输出。为了定义这个功能，Lean 使用了一个合适的、良基的度量。内部是对用户隐藏的；使用这些定义的规范方法是使用 simp （或 unfold），正如我们上面所做的那样。

相互递归定义还提供了处理相互和嵌套归纳类型的自然方法。回想一下前面提到的 Even 和 Odd 作为相互归纳谓词的定义。

mutual
  inductive Even : Nat → Prop where
    | even_zero : Even 0
    | even_succ : ∀ n, Odd n → Even (n + 1)

  inductive Odd : Nat → Prop where
    | odd_succ : ∀ n, Even n → Odd (n + 1)
end

构造子 even_zero、even_succ 和 odd_succ 提供了显示数字是偶数还是奇数的积极方法。我们需要利用归纳类型是由这些构造子生成的这一事实来知道零不是奇数，并且后两个含义是相反的。像往常一样，构造子保存在以定义的类型命名的命名空间中，并且命令 open Even Odd 允许我们更方便地访问它们。

# mutual
#  inductive Even : Nat → Prop where
#    | even_zero : Even 0
#    | even_succ : ∀ n, Odd n → Even (n + 1)
#  inductive Odd : Nat → Prop where
#    | odd_succ : ∀ n, Even n → Odd (n + 1)
# end
open Even Odd

theorem not_odd_zero : ¬ Odd 0 :=
  fun h => nomatch h

theorem even_of_odd_succ : ∀ n, Odd (n + 1) → Even n
  | _, odd_succ n h => h

theorem odd_of_even_succ : ∀ n, Even (n + 1) → Odd n
  | _, even_succ n h => h

另一个例子，假设我们使用嵌套归纳类型来归纳定义一组项，这样，项要么是常量(由字符串给出名称)，要么是将常量应用于常量列表的结果。

inductive Term where
  | const : String → Term
  | app   : String → List Term → Term

然后，我们可以使用一个相互递归的定义来计算在一个项中出现的常量的数量，以及在一个项列表中出现的常量的数量。

# inductive Term where
#  | const : String → Term
#  | app   : String → List Term → Term
namespace Term

mutual
  def numConsts : Term → Nat
    | const _ => 1
    | app _ cs => numConstsLst cs

  def numConstsLst : List Term → Nat
    | [] => 0
    | c :: cs => numConsts c + numConstsLst cs
end

def sample := app "f" [app "g" [const "x"], const "y"]

#eval numConsts sample

end Term

作为最后一个例子，我们定义了一个函数 replaceConst a b e，它将项 e 中的常数 a 替换为 b，然后证明常数的数量是相同的。注意，我们的证明使用了相互递归（即归纳法）。

# inductive Term where
#  | const : String → Term
#  | app   : String → List Term → Term
# namespace Term
# mutual
#  def numConsts : Term → Nat
#    | const _ => 1
#    | app _ cs => numConstsLst cs
#   def numConstsLst : List Term → Nat
#    | [] => 0
#    | c :: cs => numConsts c + numConstsLst cs
# end
mutual
  def replaceConst (a b : String) : Term → Term
    | const c => if a == c then const b else const c
    | app f cs => app f (replaceConstLst a b cs)

  def replaceConstLst (a b : String) : List Term → List Term
    | [] => []
    | c :: cs => replaceConst a b c :: replaceConstLst a b cs
end

mutual
  theorem numConsts_replaceConst (a b : String) (e : Term)
            : numConsts (replaceConst a b e) = numConsts e := by
    match e with
    | const c => simp [replaceConst]; split <;> simp [numConsts]
    | app f cs => simp [replaceConst, numConsts, numConsts_replaceConstLst a b cs]

  theorem numConsts_replaceConstLst (a b : String) (es : List Term)
            : numConstsLst (replaceConstLst a b es) = numConstsLst es := by
    match es with
    | [] => simp [replaceConstLst, numConstsLst]
    | c :: cs =>
      simp [replaceConstLst, numConstsLst, numConsts_replaceConst a b c,
            numConsts_replaceConstLst a b cs]
end

依值模式匹配

我们在模式匹配一节中考虑的所有模式匹配示例都可以很容易地使用 casesOn 和 recOn 来编写。然而，对于索引归纳族，如 Vector α n，通常不是这种情况，因为区分情况要对索引的值施加约束。如果没有方程编译器，我们将需要大量的样板代码来定义非常简单的函数，例如使用递归定义 map、zip 和 unzip。为了理解其中的困难，考虑一下如何定义一个函数 tail，它接受一个向量 v : Vector α (succ n) 并删除第一个元素。首先想到的可能是使用 casesOn 函数:

inductive Vector (α : Type u) : Nat → Type u
  | nil  : Vector α 0
  | cons : α → {n : Nat} → Vector α n → Vector α (n+1)

namespace Vector

#check @Vector.casesOn
/-
  {α : Type u}
  → {motive : (a : Nat) → Vector α a → Sort v} →
  → {a : Nat} → (t : Vector α a)
  → motive 0 nil
  → ((a : α) → {n : Nat} → (a_1 : Vector α n) → motive (n + 1) (cons a a_1))
  → motive a t
-/

end Vector

但是在 nil 的情况下我们应该返回什么值呢？有趣的事情来了：如果 v 具有 Vector α (succ n) 类型，它「不能」为nil，但很难告诉 casesOn。

一种解决方案是定义一个辅助函数:

# inductive Vector (α : Type u) : Nat → Type u
#   | nil  : Vector α 0
#   | cons : α → {n : Nat} → Vector α n → Vector α (n+1)
# namespace Vector
def tailAux (v : Vector α m) : m = n + 1 → Vector α n :=
  Vector.casesOn (motive := fun x _ => x = n + 1 → Vector α n) v
    (fun h : 0 = n + 1 => Nat.noConfusion h)
    (fun (a : α) (m : Nat) (as : Vector α m) =>
     fun (h : m + 1 = n + 1) =>
       Nat.noConfusion h (fun h1 : m = n => h1 ▸ as))

def tail (v : Vector α (n+1)) : Vector α n :=
  tailAux v rfl
# end Vector

在 nil 的情况下，m 被实例化为 0，noConfusion 利用了 0 = succ n 不能出现的事实。否则，v 的形式为 a :: w，我们可以简单地将 w 从长度 m 的向量转换为长度 n 的向量后返回 w。

定义 tail 的困难在于维持索引之间的关系。 tailAux 中的假设 e : m = n + 1 用于传达 n 与与小前提相关的索引之间的关系。此外，zero = n + 1 的情况是不可达的，而放弃这种情况的规范方法是使用 noConfusion。

然而，tail 函数很容易使用递归方程来定义，并且方程编译器会自动为我们生成所有样板代码。下面是一些类似的例子:

# inductive Vector (α : Type u) : Nat → Type u
#   | nil  : Vector α 0
#   | cons : α → {n : Nat} → Vector α n → Vector α (n+1)
# namespace Vector
def head : {n : Nat} → Vector α (n+1) → α
  | n, cons a as => a

def tail : {n : Nat} → Vector α (n+1) → Vector α n
  | n, cons a as => as

theorem eta : ∀ {n : Nat} (v : Vector α (n+1)), cons (head v) (tail v) = v
  | n, cons a as => rfl

def map (f : α → β → γ) : {n : Nat} → Vector α n → Vector β n → Vector γ n
  | 0,   nil,       nil       => nil
  | n+1, cons a as, cons b bs => cons (f a b) (map f as bs)

def zip : {n : Nat} → Vector α n → Vector β n → Vector (α × β) n
  | 0,   nil,       nil       => nil
  | n+1, cons a as, cons b bs => cons (a, b) (zip as bs)
# end Vector

注意，对于「不可达」的情况，例如 head nil，我们可以省略递归方程。为索引族自动生成的定义远非直截了当。例如:

# inductive Vector (α : Type u) : Nat → Type u
#   | nil  : Vector α 0
#   | cons : α → {n : Nat} → Vector α n → Vector α (n+1)
# namespace Vector
def map (f : α → β → γ) : {n : Nat} → Vector α n → Vector β n → Vector γ n
  | 0,   nil,       nil       => nil
  | n+1, cons a as, cons b bs => cons (f a b) (map f as bs)

#print map
#print map.match_1
# end Vector

与 tail 函数相比，map 函数手工定义更加繁琐。我们鼓励您尝试使用 recOn、casesOn 和 noConfusion。

不可访问模式

有时候，依值匹配模式中的参数对定义来说并不是必需的，但是必须包含它来适当地确定表达式的类型。Lean 允许用户将这些子项标记为「不可访问」以进行模式匹配。例如，当左侧出现的项既不是变量也不是构造子应用时，这些注解是必不可少的，因为它们不适合用于模式匹配的目标。我们可以将这种不可访问的模式视为模式的「不关心」组件。你可以通过写 .(t) 来声明子项不可访问。如果不可访问的模式可以被推断出来，你也可以写 _。

下面的例子中，我们声明了一个归纳类型，它定义了「在 f 的像中」的属性。您可以将 ImageOf f b 类型的元素视为 b 位于 f 的像中的证据，构造子 imf 用于构建此类证据。然后，我们可以定义任何函数 f 的「逆」，逆函数将 f 的像中的任何元素赋给映射到它的元素。类型规则迫使我们为第一个参数写 f a，但是这个项既不是变量也不是构造子应用，并且在模式匹配定义中没有作用。为了定义下面的函数 inverse，我们必须将 f a 标记为不可访问。

inductive ImageOf {α β : Type u} (f : α → β) : β → Type u where
  | imf : (a : α) → ImageOf f (f a)

open ImageOf

def inverse {f : α → β} : (b : β) → ImageOf f b → α
  | .(f a), imf a => a

def inverse' {f : α → β} : (b : β) → ImageOf f b → α
  | _, imf a => a

在上面的例子中，不可访问记号清楚地表明 f 不是一个模式匹配变量。

不可访问模式可用于澄清和控制使用依值模式匹配的定义。考虑函数 Vector.add 的以下定义，假设该类型有满足结合律的加法函数，它将一个类型的两个元素向量相加:

inductive Vector (α : Type u) : Nat → Type u
  | nil  : Vector α 0
  | cons : α → {n : Nat} → Vector α n → Vector α (n+1)

namespace Vector

def add [Add α] : {n : Nat} → Vector α n → Vector α n → Vector α n
  | 0,   nil,       nil       => nil
  | n+1, cons a as, cons b bs => cons (a + b) (add as bs)

end Vector

参数 {n : Nat} 出现在冒号之后，因为它不能在整个定义中保持固定。在实现这个定义时，方程编译器首先区分第一个参数是 0 还是 n+1。对接下来的两个参数嵌套地区分情况，在每种情况下，方程编译器都会排除与第一个模式不兼容的情况。

但事实上，在第一个参数上不需要区分情况；当我们对第二个参数区分情况时，Vector 的 casesOn 消去器会自动抽象该参数，并将其替换为 0 和 n + 1。使用不可访问的模式，我们可以提示方程编译器不要在 n 上区分情况。

# inductive Vector (α : Type u) : Nat → Type u
#   | nil  : Vector α 0
#   | cons : α → {n : Nat} → Vector α n → Vector α (n+1)
# namespace Vector
def add [Add α] : {n : Nat} → Vector α n → Vector α n → Vector α n
  | .(_), nil,       nil       => nil
  | .(_), cons a as, cons b bs => cons (a + b) (add as bs)
# end Vector

将位置标记为不可访问模式首先告诉方程编译器，参数的形式应该从其他参数所构成的约束中推断出来，其次，第一个参数不应该参与模式匹配。

为简便起见，不可访问的模式 .(_) 可以写成 _。

# inductive Vector (α : Type u) : Nat → Type u
#   | nil  : Vector α 0
#   | cons : α → {n : Nat} → Vector α n → Vector α (n+1)
# namespace Vector
def add [Add α] : {n : Nat} → Vector α n → Vector α n → Vector α n
  | _, nil,       nil       => nil
  | _, cons a as, cons b bs => cons (a + b) (add as bs)
# end Vector

如前所述，参数 {n : Nat} 是模式匹配的一部分，因为它不能在整个定义中保持固定。在以前的 Lean 版本中，用户经常发现必须包含这些额外的判别符是很麻烦的。因此，Lean 4 实现了一个新特性， 判别精炼（discriminant refinement） ，它自动为我们包含了这些额外的判别。

# inductive Vector (α : Type u) : Nat → Type u
#   | nil  : Vector α 0
#   | cons : α → {n : Nat} → Vector α n → Vector α (n+1)
# namespace Vector
def add [Add α] {n : Nat} : Vector α n → Vector α n → Vector α n
  | nil,       nil       => nil
  | cons a as, cons b bs => cons (a + b) (add as bs)
# end Vector

当与「自动绑定隐式」特性结合使用时，你可以进一步简化声明并这样写：

# inductive Vector (α : Type u) : Nat → Type u
#   | nil  : Vector α 0
#   | cons : α → {n : Nat} → Vector α n → Vector α (n+1)
# namespace Vector
def add [Add α] : Vector α n → Vector α n → Vector α n
  | nil,       nil       => nil
  | cons a as, cons b bs => cons (a + b) (add as bs)
# end Vector

使用这些新特性，您可以更紧凑地编写在前几节中定义的其他向量函数，如下所示:

# inductive Vector (α : Type u) : Nat → Type u
#   | nil  : Vector α 0
#   | cons : α → {n : Nat} → Vector α n → Vector α (n+1)
# namespace Vector
def head : Vector α (n+1) → α
  | cons a as => a

def tail : Vector α (n+1) → Vector α n
  | cons a as => as

theorem eta : (v : Vector α (n+1)) → cons (head v) (tail v) = v
  | cons a as => rfl

def map (f : α → β → γ) : Vector α n → Vector β n → Vector γ n
  | nil,       nil       => nil
  | cons a as, cons b bs => cons (f a b) (map f as bs)

def zip : Vector α n → Vector β n → Vector (α × β) n
  | nil,       nil       => nil
  | cons a as, cons b bs => cons (a, b) (zip as bs)
# end Vector

Match 表达式

Lean 还提供「match-with」表达式，它在很多函数式语言中都能找到。

def isNotZero (m : Nat) : Bool :=
  match m with
  | 0   => false
  | n+1 => true

这看起来与普通的模式匹配定义没有太大的不同，但关键是 match 可以在表达式中的任何地方使用，并带有任意参数。

def isNotZero (m : Nat) : Bool :=
  match m with
  | 0   => false
  | n+1 => true

def filter (p : α → Bool) : List α → List α
  | []      => []
  | a :: as =>
    match p a with
    | true => a :: filter p as
    | false => filter p as

example : filter isNotZero [1, 0, 0, 3, 0] = [1, 3] := rfl

另一例：

def foo (n : Nat) (b c : Bool) :=
  5 + match n - 5, b && c with
      | 0,   true  => 0
      | m+1, true  => m + 7
      | 0,   false => 5
      | m+1, false => m + 3

#eval foo 7 true false

example : foo 7 true false = 9 := rfl

Lean 使用内建的 match 来实现系统所有地方的模式匹配。因此，这四种定义具有相同的净效果。

def bar₁ : Nat × Nat → Nat
  | (m, n) => m + n

def bar₂ (p : Nat × Nat) : Nat :=
  match p with
  | (m, n) => m + n

def bar₃ : Nat × Nat → Nat :=
  fun (m, n) => m + n

def bar₄ (p : Nat × Nat) : Nat :=
  let (m, n) := p; m + n

这些变体在解构命题中也是同样有用的：

variable (p q : Nat → Prop)

example : (∃ x, p x) → (∃ y, q y) → ∃ x y, p x ∧ q y
  | ⟨x, px⟩, ⟨y, qy⟩ => ⟨x, y, px, qy⟩

example (h₀ : ∃ x, p x) (h₁ : ∃ y, q y)
        : ∃ x y, p x ∧ q y :=
  match h₀, h₁ with
  | ⟨x, px⟩, ⟨y, qy⟩ => ⟨x, y, px, qy⟩

example : (∃ x, p x) → (∃ y, q y) → ∃ x y, p x ∧ q y :=
  fun ⟨x, px⟩ ⟨y, qy⟩ => ⟨x, y, px, qy⟩

example (h₀ : ∃ x, p x) (h₁ : ∃ y, q y)
        : ∃ x y, p x ∧ q y :=
  let ⟨x, px⟩ := h₀
  let ⟨y, qy⟩ := h₁
  ⟨x, y, px, qy⟩

局域递归声明

可以通过 let rec 关键字定义局域递归声明。

def replicate (n : Nat) (a : α) : List α :=
  let rec loop : Nat → List α → List α
    | 0,   as => as
    | n+1, as => loop n (a::as)
  loop n []

#check @replicate.loop
-- {α : Type} → α → Nat → List α → List α

Lean 对每个 let rec创建一个辅助声明。上例中，它为出现在 replicate 中的 let rec loop 创建了一个声明 replicate.loop。注意到，Lean 通过添加任意的出现在 let rec 声明中的局域变量作为附加参数来「关闭」声明。例如，局域变量 a 出现在 let rec loop 当中。

也在策略模式中可使用 let rec 来建立归纳证明。

# def replicate (n : Nat) (a : α) : List α :=
#  let rec loop : Nat → List α → List α
#    | 0,   as => as
#    | n+1, as => loop n (a::as)
#  loop n []
theorem length_replicate (n : Nat) (a : α) : (replicate n a).length = n := by
  let rec aux (n : Nat) (as : List α)
              : (replicate.loop a n as).length = n + as.length := by
    match n with
    | 0   => simp [replicate.loop]
    | n+1 => simp [replicate.loop, aux n, Nat.add_succ, Nat.succ_add]
  exact aux n []

也可以用 where 语句在定义后面引入辅助递归声明，Lean 自动把它们转译成 let rec。

def replicate (n : Nat) (a : α) : List α :=
  loop n []
where
  loop : Nat → List α → List α
    | 0,   as => as
    | n+1, as => loop n (a::as)

theorem length_replicate (n : Nat) (a : α) : (replicate n a).length = n := by
  exact aux n []
where
  aux (n : Nat) (as : List α)
      : (replicate.loop a n as).length = n + as.length := by
    match n with
    | 0   => simp [replicate.loop]
    | n+1 => simp [replicate.loop, aux n, Nat.add_succ, Nat.succ_add]

练习

1. 打开命名空间 Hidden 以避免命名冲突，并使用方程编译器定义自然数的加法、乘法和幂运算。然后用方程编译器派生出它们的一些基本属性。

2. 类似地，使用方程编译器定义列表上的一些基本操作(如 reverse 函数)，并通过归纳法证明关于列表的定理（例如对于任何列表 xs，reverse (reverse xs) = xs ）。

3. 定义您自己的函数来对自然数执行值的过程递归。同样，看看你是否能弄清楚如何定义 WellFounded.fix。

4. 按照依值模式匹配中的例子，定义一个追加（append）两个向量的函数。提示：你必须定义一个辅助函数。

5. 考虑以下类型的算术表达式。这个想法是，var n 是一个变量 vₙ，const n 是一个常量，它的值是 n。

inductive Expr where
  | const : Nat → Expr
  | var : Nat → Expr
  | plus : Expr → Expr → Expr
  | times : Expr → Expr → Expr
  deriving Repr

open Expr

def sampleExpr : Expr :=
  plus (times (var 0) (const 7)) (times (const 2) (var 1))

此处 sampleExpr 表示 (v₀ * 7) + (2 * v₁)。

写一个函数来计算这些表达式，对每个 var n 赋值 v n.

# inductive Expr where
#   | const : Nat → Expr
#   | var : Nat → Expr
#   | plus : Expr → Expr → Expr
#   | times : Expr → Expr → Expr
#   deriving Repr
# open Expr
# def sampleExpr : Expr :=
#   plus (times (var 0) (const 7)) (times (const 2) (var 1))
def eval (v : Nat → Nat) : Expr → Nat
  | const n     => sorry
  | var n       => v n
  | plus e₁ e₂  => sorry
  | times e₁ e₂ => sorry

def sampleVal : Nat → Nat
  | 0 => 5
  | 1 => 6
  | _ => 0

-- 如果答案是47说明你写的对。
-- #eval eval sampleVal sampleExpr

实现「常数融合」，这是一个将 5 + 7 等子术语化简为 12 的过程。使用辅助函数 simpConst，定义一个函数「fuse」:为了化简加号或乘号，首先递归地化简参数，然后应用 simpConst 尝试化简结果。

# inductive Expr where
#   | const : Nat → Expr
#   | var : Nat → Expr
#   | plus : Expr → Expr → Expr
#   | times : Expr → Expr → Expr
#   deriving Repr
# open Expr
# def eval (v : Nat → Nat) : Expr → Nat
#   | const n     => sorry
#   | var n       => v n
#   | plus e₁ e₂  => sorry
#   | times e₁ e₂ => sorry
def simpConst : Expr → Expr
  | plus (const n₁) (const n₂)  => const (n₁ + n₂)
  | times (const n₁) (const n₂) => const (n₁ * n₂)
  | e                           => e

def fuse : Expr → Expr := sorry

theorem simpConst_eq (v : Nat → Nat)
        : ∀ e : Expr, eval v (simpConst e) = eval v e :=
  sorry

theorem fuse_eq (v : Nat → Nat)
        : ∀ e : Expr, eval v (fuse e) = eval v e :=
  sorry

最后两个定理表明，定义保持值不变。