更多不等式

Lean 的内置证明自动化足以检查 arrayMapHelper 和 findHelper 是否停机。 所需要做的就是提供一个值随着每次递归调用而减小的表达式。 但是，Lean 的内置自动化不是万能的，它通常需要一些帮助。

归并排序

一个停机证明非平凡的函数示例是 List 上的归并排序。归并排序包含两个阶段： 首先，将列表分成两半。使用归并排序对每一半进行排序， 然后使用一个将两个已排序列表合并为一个更大的已排序列表的函数合并结果。 基本情况是空列表和单元素列表，它们都被认为已经排序。

要合并两个已排序列表，需要考虑两个基本情况：

1. 如果一个输入列表为空，则结果是另一个列表。
2. 如果两个列表都不为空，则应比较它们的头部。该函数的结果是两个头部中较小的一个， 后面是合并两个列表的剩余项的结果。

这在任何列表上都不是结构化递归。递归停机是因为在每次递归调用中都会从两个列表中的一个中删除一个项， 但它可能是任何一个列表。termination_by 子句使用两个列表长度的和作为递减值：

def merge [Ord α] (xs : List α) (ys : List α) : List α :=
  match xs, ys with
  | [], _ => ys
  | _, [] => xs
  | x'::xs', y'::ys' =>
    match Ord.compare x' y' with
    | .lt | .eq => x' :: merge xs' (y' :: ys')
    | .gt => y' :: merge (x'::xs') ys'
termination_by merge xs ys => xs.length + ys.length

除了使用列表的长度外，还可以提供一个包含两个列表的偶对：

def merge [Ord α] (xs : List α) (ys : List α) : List α :=
  match xs, ys with
  | [], _ => ys
  | _, [] => xs
  | x'::xs', y'::ys' =>
    match Ord.compare x' y' with
    | .lt | .eq => x' :: merge xs' (y' :: ys')
    | .gt => y' :: merge (x'::xs') ys'
termination_by merge xs ys => (xs, ys)

它有效是因为 Lean 有一个内置的数据大小概念，通过一个称为 WellFoundedRelation 的类型类来表示。如果偶对中的第一个或第二个项缩小，偶对的实例会自动认为它们会变小。

分割列表的一个简单方法是将输入列表中的每个项添加到两个交替的输出列表中：

def splitList (lst : List α) : (List α × List α) :=
  match lst with
  | [] => ([], [])
  | x :: xs =>
    let (a, b) := splitList xs
    (x :: b, a)

归并排序检查是否已达到基本情况。如果是，则返回输入列表。 如果不是，则分割输入，并合并对每一半排序的结果：

def mergeSort [Ord α] (xs : List α) : List α :=
  if h : xs.length < 2 then
    match xs with
    | [] => []
    | [x] => [x]
  else
    let halves := splitList xs
    merge (mergeSort halves.fst) (mergeSort halves.snd)

Lean 的模式匹配编译器能够判断由测试 xs.length < 2 的 if 引入的前提 h 排除了长度超过一个条目的列表，因此没有「缺少情况」的错误。 然而，即使此程序总是停机，它也不是结构化递归的：

fail to show termination for
  mergeSort
with errors
argument #3 was not used for structural recursion
  failed to eliminate recursive application
    mergeSort halves.fst

structural recursion cannot be used

failed to prove termination, use `termination_by` to specify a well-founded relation

它能停机的原因是 splitList 总是返回比其输入更短的列表。 因此，halves.fst 和 halves.snd 的长度小于 xs 的长度。 这可以使用 termination_by 子句来表示：

def mergeSort [Ord α] (xs : List α) : List α :=
  if h : xs.length < 2 then
    match xs with
    | [] => []
    | [x] => [x]
  else
    let halves := splitList xs
    merge (mergeSort halves.fst) (mergeSort halves.snd)
termination_by mergeSort xs => xs.length

有了这个子句，错误信息就变了。Lean 不会抱怨函数不是结构化递归的， 而是指出它无法自动证明 (splitList xs).fst.length < xs.length：

failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
α : Type u_1
xs : List α
h : ¬List.length xs < 2
halves : List α × List α := splitList xs
⊢ List.length (splitList xs).fst < List.length xs

分割列表使其变短

还需要证明 (splitList xs).snd.length < xs.length。由于 splitList 在向两个列表添加条目之间交替进行，因此最简单的方法是同时证明这两个语句， 这样证明的结构就可以遵循用于实现 splitList 的算法。换句话说，最简单的方法是证明 ∀(lst : List), (splitList lst).fst.length < lst.length ∧ (splitList lst).snd.length < lst.length。

不幸的是，这个陈述是错误的。特别是， splitList [] 是 ([], [])。 两个输出列表的长度都是 0，这并不小于输入列表的长度 0。类似地， splitList ["basalt"] 求值为 ([\"basalt\"], [])，而 ["basalt"] 并不比 ["basalt"] 短。然而， splitList ["basalt", "granite"] 求值为 (["basalt"], ["granite"])， 这两个输出列表都比输入列表短。

输出列表的长度始终小于或等于输入列表的长度，但仅当输入列表至少包含两个条目时， 它们才严格更短。事实证明，最容易证明前一个陈述，然后将其扩展到后一个陈述。 从定理的陈述开始：

theorem splitList_shorter_le (lst : List α) :
    (splitList lst).fst.length ≤ lst.length ∧
      (splitList lst).snd.length ≤ lst.length := by
  skip

unsolved goals
α : Type u_1
lst : List α
⊢ List.length (splitList lst).fst ≤ List.length lst ∧ List.length (splitList lst).snd ≤ List.length lst

由于 splitList 在列表上是结构化递归的，因此证明应使用归纳法。 splitList 中的结构化递归非常适合归纳证明：归纳法的基本情况与递归的基本情况匹配， 归纳步骤与递归调用匹配。induction 策略给出了两个目标：

theorem splitList_shorter_le (lst : List α) :
    (splitList lst).fst.length ≤ lst.length ∧
      (splitList lst).snd.length ≤ lst.length := by
  induction lst with
  | nil => skip
  | cons x xs ih => skip

unsolved goals
case nil
α : Type u_1
⊢ List.length (splitList []).fst ≤ List.length [] ∧ List.length (splitList []).snd ≤ List.length []

unsolved goals
case cons
α : Type u_1
x : α
xs : List α
ih : List.length (splitList xs).fst ≤ List.length xs ∧ List.length (splitList xs).snd ≤ List.length xs
⊢ List.length (splitList (x :: xs)).fst ≤ List.length (x :: xs) ∧
    List.length (splitList (x :: xs)).snd ≤ List.length (x :: xs)

可以通过调用简化器并指示它展开 splitList 的定义来证明 nil 情况的目标， 因为空列表的长度小于或等于空列表的长度。类似地，在 cons 情况下使用 splitList 简化会在目标中的长度周围放置 Nat.succ：

theorem splitList_shorter_le (lst : List α) :
    (splitList lst).fst.length ≤ lst.length ∧
      (splitList lst).snd.length ≤ lst.length := by
  induction lst with
  | nil => simp [splitList]
  | cons x xs ih =>
    simp [splitList]

unsolved goals
case cons
α : Type u_1
x : α
xs : List α
ih : List.length (splitList xs).fst ≤ List.length xs ∧ List.length (splitList xs).snd ≤ List.length xs
⊢ Nat.succ (List.length (splitList xs).snd) ≤ Nat.succ (List.length xs) ∧
    List.length (splitList xs).fst ≤ Nat.succ (List.length xs)

这是因为对 List.length 的调用消耗了列表 x :: xs 的头部，将其转换为 Nat.succ， 既在输入列表的长度中，也在第一个输出列表的长度中。

在 Lean 中编写 A ∧ B 是 And A B 的缩写。 And 是 Prop 宇宙中的一个结构体类型：

structure And (a b : Prop) : Prop where
  intro ::
  left : a
  right : b

换句话说，A ∧ B 的证明包括应用于 left 字段中 A 的证明和应用于 right 字段中 B 的证明的 And.intro 构造子。

cases 策略允许证明依次考虑数据类型的每个构造子或命题的每个潜在证明。 它对应于没有递归的 match 表达式。对结构体使用 cases 会导致结构体被分解， 并为结构体的每个字段添加一个假设，就像模式匹配表达式提取结构体的字段以用于程序中一样。 由于结构体只有一个构造子，因此对结构体使用 cases 不会产生额外的目标。

由于 ih 是 List.length (splitList xs).fst ≤ List.length xs ∧ List.length (splitList xs).snd ≤ List.length xs 的一个证明，使用 cases ih 会产生一个 List.length (splitList xs).fst ≤ List.length xs 的假设 和一个 List.length (splitList xs).snd ≤ List.length xs 的假设:

theorem splitList_shorter_le (lst : List α) :
    (splitList lst).fst.length ≤ lst.length ∧
      (splitList lst).snd.length ≤ lst.length := by
  induction lst with
  | nil => simp [splitList]
  | cons x xs ih =>
    simp [splitList]
    cases ih

unsolved goals
case cons.intro
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ Nat.succ (List.length (splitList xs).snd) ≤ Nat.succ (List.length xs) ∧
    List.length (splitList xs).fst ≤ Nat.succ (List.length xs)

由于证明的目标也是一个 And，因此可以使用 constructor 策略应用 And.intro， 从而为每个参数生成一个目标：

theorem splitList_shorter_le (lst : List α) :
    (splitList lst).fst.length ≤ lst.length ∧
      (splitList lst).snd.length ≤ lst.length := by
  induction lst with
  | nil => simp [splitList]
  | cons x xs ih =>
    simp [splitList]
    cases ih
    constructor

unsolved goals
case cons.intro.left
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ Nat.succ (List.length (splitList xs).snd) ≤ Nat.succ (List.length xs)

case cons.intro.right
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ List.length (splitList xs).fst ≤ Nat.succ (List.length xs)

left 目标与 left✝ 假设非常相似，除了目标用 Nat.succ 包装不等式的两侧。 同样，right 目标类似于 right✝ 假设，除了目标仅将 Nat.succ 添加到输入列表的长度。 现在是时候证明 Nat.succ 的这些包装保留了陈述的真值了。

两边同时加一

对于 left 目标，要证明的语句是 Nat.succ_le_succ : n ≤ m → Nat.succ n ≤ Nat.succ m。 换句话说，如果 n ≤ m，那么在两边都加一并不会改变这一事实。为什么这是真的？ 证明 n ≤ m 是一个 Nat.le.refl 构造子，周围有 m - n 个 Nat.le.step 构造子的实例。 在两边都加一只是意味着 refl 应用于比之前大一的数，并且具有相同数量的 step 构造子。

更形式化地说，证明是通过归纳法来证明 n ≤ m 的证据。如果证据是 refl，则 n = m， 因此 Nat.succ n = Nat.succ m，并且可以再次使用 refl。 如果证据是 step，则归纳假设提供了 Nat.succ n ≤ Nat.succ m 的证据， 并且目标是证明 Nat.succ n ≤ Nat.succ (Nat.succ m)。 这可以通过将 step 与归纳假设一起使用来完成。

在 Lean 中，该定理陈述为：

theorem Nat.succ_le_succ : n ≤ m → Nat.succ n ≤ Nat.succ m := by
  skip

错误信息对其进行了概括：

unsolved goals
n m : Nat
⊢ n ≤ m → Nat.succ n ≤ Nat.succ m

第一步是使用 intro 策略，将假设 n ≤ m 引入作用域并为其命名：

theorem Nat.succ_le_succ : n ≤ m → Nat.succ n ≤ Nat.succ m := by
  intro h

unsolved goals
n m : Nat
h : n ≤ m
⊢ Nat.succ n ≤ Nat.succ m

由于证明是通过归纳法对证据 n ≤ m 进行的，因此下一个策略是 induction h：

theorem Nat.succ_le_succ : n ≤ m → Nat.succ n ≤ Nat.succ m := by
  intro h
  induction h

这会产生两个目标，每个目标对应于 Nat.le 的一个构造子：

unsolved goals
case refl
n m : Nat
⊢ Nat.succ n ≤ Nat.succ n

case step
n m m✝ : Nat
a✝ : Nat.le n m✝
a_ih✝ : Nat.succ n ≤ Nat.succ m✝
⊢ Nat.succ n ≤ Nat.succ (Nat.succ m✝)

refl 的目标可以使用 refl 本身来解决，constructor 策略会选择它。 step 的目标还需要使用 step 构造子：

theorem Nat.succ_le_succ : n ≤ m → Nat.succ n ≤ Nat.succ m := by
  intro h
  induction h with
  | refl => constructor
  | step h' ih => constructor

unsolved goals
case step.a
n m m✝ : Nat
h' : Nat.le n m✝
ih : Nat.succ n ≤ Nat.succ m✝
⊢ Nat.le (Nat.succ n) (m✝ + 1)

该目标不再使用 ≤ 运算符显示，但它等价于归纳假设 ih。 assumption 策略会自动选择一个满足目标的假设，证明完毕：

theorem Nat.succ_le_succ : n ≤ m → Nat.succ n ≤ Nat.succ m := by
  intro h
  induction h with
  | refl => constructor
  | step h' ih =>
    constructor
    assumption

写成递归函数，证明如下：

theorem Nat.succ_le_succ : n ≤ m → Nat.succ n ≤ Nat.succ m
  | .refl => .refl
  | .step h' => .step (Nat.succ_le_succ h')

将基于策略的归纳证明与这个递归函数进行比较是有指导意义的。哪些证明步骤对应于定义的哪些部分？

在较大的一侧加一

证明 splitList_shorter_le 所需的第二个不等式是 ∀(n m : Nat), n ≤ m → n ≤ Nat.succ m。 这个证明几乎与 Nat.succ_le_succ 相同。同样，传入的假设 n ≤ m 基本上跟踪了 n 和 m 在 Nat.le.step 构造子数量上的差异。因此，证明应该在基本情况下添加一个额外的 Nat.le.step。 证明可以写成：

theorem Nat.le_succ_of_le : n ≤ m → n ≤ Nat.succ m := by
  intro h
  induction h with
  | refl => constructor; constructor
  | step => constructor; assumption

为了揭示幕后发生的事情，apply 和 exact 策略可用于准确指示正在应用哪个构造子。 apply 策略通过应用一个返回类型匹配的函数或构造子来解决当前目标， 为每个未提供的参数创建新的目标，而如果需要任何新目标，exact 就会失败：

theorem Nat.le_succ_of_le : n ≤ m → n ≤ Nat.succ m := by
  intro h
  induction h with
  | refl => apply Nat.le.step; exact Nat.le.refl
  | step _ ih => apply Nat.le.step; exact ih

证明可以简化：

theorem Nat.le_succ_of_le (h : n ≤ m) : n ≤ Nat.succ m := by
  induction h <;> repeat (first | constructor | assumption)

在这个简短的策略脚本中，由 induction 引入的两个目标都使用 repeat (first | constructor | assumption) 来解决。策略 first | T1 | T2 | ... | Tn 表示按顺序尝试 T1 到 Tn，然后使用第一个成功的策略。 换句话说，repeat (first | constructor | assumption) 会尽可能地应用构造子， 然后尝试使用假设来解决目标。

最后，证明可以写成一个递归函数：

theorem Nat.le_succ_of_le : n ≤ m → n ≤ Nat.succ m
  | .refl => .step .refl
  | .step h => .step (Nat.le_succ_of_le h)

每种证明风格都适用于不同的情况。详细的证明脚本在初学者阅读代码或证明步骤提供某种见解的情况下很有用。 简短、高度自动化的证明脚本通常更容易维护，因为自动化通常在面对定义和数据类型的细微更改时既灵活又健壮。 递归函数通常从数学证明的角度来看更难理解，也更难维护，但对于开始使用交互式定理证明的程序员来说， 它可能是一个有用的桥梁。

完成证明

现在已经证明了两个辅助定理，splitList_shorter_le 的其余部分将很快完成。 当前的证明状态有两个目标，用于 And 的左侧和右侧：

unsolved goals
case cons.intro.left
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ Nat.succ (List.length (splitList xs).snd) ≤ Nat.succ (List.length xs)

case cons.intro.right
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ List.length (splitList xs).fst ≤ Nat.succ (List.length xs)

目标以 And 结构体的字段命名。这意味着 case 策略（不要与 cases 混淆）可以依次关注于每个目标：

theorem splitList_shorter_le (lst : List α) :
    (splitList lst).fst.length ≤ lst.length ∧ (splitList lst).snd.length ≤ lst.length := by
  induction lst with
  | nil => simp [splitList]
  | cons x xs ih =>
    simp [splitList]
    cases ih
    constructor
    case left => skip
    case right => skip

现在不再是一个错误列出两个未解决的目标，而是有两个错误信息， 每个 skip 上一个。对于left目标，可以使用Nat.succ_le_succ：

unsolved goals
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ Nat.succ (List.length (splitList xs).snd) ≤ Nat.succ (List.length xs)

在右侧目标中，Nat.le_suc_of_le 适合：

unsolved goals
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ List.length (splitList xs).fst ≤ Nat.succ (List.length xs)

这两个定理都包含前提条件 n ≤ m。它们可以作为 left✝ 和 right✝ 假设找到， 这意味着 assumption 策略可以处理最终目标：

theorem splitList_shorter_le (lst : List α) :
    (splitList lst).fst.length ≤ lst.length ∧ (splitList lst).snd.length ≤ lst.length := by
  induction lst with
  | nil => simp [splitList]
  | cons x xs ih =>
    simp [splitList]
    cases ih
    constructor
    case left => apply Nat.succ_le_succ; assumption
    case right => apply Nat.le_succ_of_le; assumption

下一步是返回到证明归并排序停机所需的实际定理：只要一个列表至少有两个条目， 则分割它的两个结果都严格短于它。

theorem splitList_shorter (lst : List α) (_ : lst.length ≥ 2) :
    (splitList lst).fst.length < lst.length ∧
      (splitList lst).snd.length < lst.length := by
  skip

unsolved goals
α : Type u_1
lst : List α
x✝ : List.length lst ≥ 2
⊢ List.length (splitList lst).fst < List.length lst ∧ List.length (splitList lst).snd < List.length lst

模式匹配在策略脚本中与在程序中一样有效。因为 lst 至少有两个条目， 所以它们可以用 match 暴露出来，它还通过依值模式匹配来细化类型：

theorem splitList_shorter (lst : List α) (_ : lst.length ≥ 2) :
    (splitList lst).fst.length < lst.length ∧
      (splitList lst).snd.length < lst.length := by
  match lst with
  | x :: y :: xs =>
    skip

unsolved goals
α : Type u_1
lst : List α
x y : α
xs : List α
x✝ : List.length (x :: y :: xs) ≥ 2
⊢ List.length (splitList (x :: y :: xs)).fst < List.length (x :: y :: xs) ∧
    List.length (splitList (x :: y :: xs)).snd < List.length (x :: y :: xs)

使用 splitList 简化会删除 x 和 y，导致列表的计算长度每个都获得 Nat.succ：

theorem splitList_shorter (lst : List α) (_ : lst.length ≥ 2) :
    (splitList lst).fst.length < lst.length ∧
      (splitList lst).snd.length < lst.length := by
  match lst with
  | x :: y :: xs =>
    simp [splitList]

unsolved goals
α : Type u_1
lst : List α
x y : α
xs : List α
x✝ : List.length (x :: y :: xs) ≥ 2
⊢ Nat.succ (List.length (splitList xs).fst) < Nat.succ (Nat.succ (List.length xs)) ∧
    Nat.succ (List.length (splitList xs).snd) < Nat.succ (Nat.succ (List.length xs))

用 simp_arith 替换 simp 会删除这些 Nat.succ 构造子， 因为 simp_arith 利用了 n + 1 < m + 1 意味着 n < m 的事实：

theorem splitList_shorter (lst : List α) (_ : lst.length ≥ 2) :
    (splitList lst).fst.length < lst.length ∧
      (splitList lst).snd.length < lst.length := by
  match lst with
  | x :: y :: xs =>
    simp_arith [splitList]

unsolved goals
α : Type u_1
lst : List α
x y : α
xs : List α
x✝ : List.length (x :: y :: xs) ≥ 2
⊢ List.length (splitList xs).fst ≤ List.length xs ∧ List.length (splitList xs).snd ≤ List.length xs

此目标现在匹配 splitList_shorter_le，可用于结束证明：

theorem splitList_shorter (lst : List α) (_ : lst.length ≥ 2) :
    (splitList lst).fst.length < lst.length ∧
      (splitList lst).snd.length < lst.length := by
  match lst with
  | x :: y :: xs =>
    simp_arith [splitList]
    apply splitList_shorter_le

证明 mergeSort 停机所需的事实可以从结果 And 中提取出来：

theorem splitList_shorter_fst (lst : List α) (h : lst.length ≥ 2) :
    (splitList lst).fst.length < lst.length :=
  splitList_shorter lst h |>.left

theorem splitList_shorter_snd (lst : List α) (h : lst.length ≥ 2) :
    (splitList lst).snd.length < lst.length :=
  splitList_shorter lst h |>.right

归并排序停机证明

归并排序有两个递归调用，一个用于 splitList 返回的每个子列表。 每个递归调用都需要证明传递给它的列表的长度短于输入列表的长度。 通常分两步编写停机证明会更方便：首先，写下允许 Lean 验证停机的命题，然后证明它们。 否则，可能会投入大量精力来证明命题，却发现它们并不是所需的在更小的输入上建立递归调用的内容。

sorry 策略可以证明任何目标，即使是错误的目标。它不适用于生产代码或最终证明， 但它是一种便捷的方法，可以提前「勾勒出」证明或程序。任何使用 sorry 的定义或定理都会附有警告。

使用 sorry 的 mergeSort 停机论证的初始草图可以通过将 Lean 无法证明的目标复制到 have 表达式中来编写。在 Lean 中，have 类似于 let。使用 have 时，名称是可选的。 通常，let 用于定义引用关键值的名称，而 have 用于局部证明命题， 当 Lean 在寻找「数组查找是否在范围内」或「函数是否停机」的证据时，可以找到这些命题。

def mergeSort [Ord α] (xs : List α) : List α :=
  if h : xs.length < 2 then
    match xs with
    | [] => []
    | [x] => [x]
  else
    let halves := splitList xs
    have : halves.fst.length < xs.length := by
      sorry
    have : halves.snd.length < xs.length := by
      sorry
    merge (mergeSort halves.fst) (mergeSort halves.snd)
termination_by mergeSort xs => xs.length

警告位于名称 mergeSort 上：

declaration uses 'sorry'

因为没有错误，所以建议的命题足以建立停机证明。

证明从应用辅助定理开始：

def mergeSort [Ord α] (xs : List α) : List α :=
  if h : xs.length < 2 then
    match xs with
    | [] => []
    | [x] => [x]
  else
    let halves := splitList xs
    have : halves.fst.length < xs.length := by
      apply splitList_shorter_fst
    have : halves.snd.length < xs.length := by
      apply splitList_shorter_snd
    merge (mergeSort halves.fst) (mergeSort halves.snd)
termination_by mergeSort xs => xs.length

两个证明都失败了，因为 splitList_shorter_fst 和 splitList_shorter_snd 都需要证明 xs.length ≥ 2：

unsolved goals
case h
α : Type ?u.37732
inst✝ : Ord α
xs : List α
h : ¬List.length xs < 2
halves : List α × List α := splitList xs
⊢ List.length xs ≥ 2

要检查这是否足以完成证明，请使用 sorry 添加它并检查错误：

def mergeSort [Ord α] (xs : List α) : List α :=
  if h : xs.length < 2 then
    match xs with
    | [] => []
    | [x] => [x]
  else
    let halves := splitList xs
    have : xs.length ≥ 2 := by sorry
    have : halves.fst.length < xs.length := by
      apply splitList_shorter_fst
      assumption
    have : halves.snd.length < xs.length := by
      apply splitList_shorter_snd
      assumption
    merge (mergeSort halves.fst) (mergeSort halves.snd)
termination_by mergeSort xs => xs.length

同样，只会有一个警告。

declaration uses 'sorry'

有一个有希望的假设可用：h : ¬List.length xs < 2，它来自 if。 显然，如果不是 xs.length < 2，那么 xs.length ≥ 2。 Lean 库以 Nat.ge_of_not_lt 的名称提供了此定理。程序现在已完成：

def mergeSort [Ord α] (xs : List α) : List α :=
  if h : xs.length < 2 then
    match xs with
    | [] => []
    | [x] => [x]
  else
    let halves := splitList xs
    have : xs.length ≥ 2 := by
      apply Nat.ge_of_not_lt
      assumption
    have : halves.fst.length < xs.length := by
      apply splitList_shorter_fst
      assumption
    have : halves.snd.length < xs.length := by
      apply splitList_shorter_snd
      assumption
    merge (mergeSort halves.fst) (mergeSort halves.snd)
termination_by mergeSort xs => xs.length

该函数可以在示例上进行测试：

#eval mergeSort ["soapstone", "geode", "mica", "limestone"]

["geode", "limestone", "mica", "soapstone"]

#eval mergeSort [5, 3, 22, 15]

[3, 5, 15, 22]

用减法迭代表示除法

正如乘法是迭代的加法，指数是迭代的乘法，除法可以理解为迭代的减法。 本书中对递归函数的第一个描述 给出了除法的一个版本，当除数不为零时停机，但 Lean 并不接受。证明除法终止需要使用关于不等式的事实。

第一步是细化除法的定义，使其需要证据证明除数不为零：

def div (n k : Nat) (ok : k > 0) : Nat :=
  if n < k then
    0
  else
    1 + div (n - k) k ok

由于增加了参数，错误信息会稍长一些，但它包含基本相同的信息：

fail to show termination for
  div
with errors
argument #1 was not used for structural recursion
  failed to eliminate recursive application
    div (n - k) k ok

argument #2 was not used for structural recursion
  failed to eliminate recursive application
    div (n - k) k ok

argument #3 was not used for structural recursion
  application type mismatch
    @Nat.le.brecOn (Nat.succ 0) fun k ok => Nat → Nat
  argument
    fun k ok => Nat → Nat
  has type
    (k : Nat) → k > 0 → Type : Type 1
  but is expected to have type
    (a : Nat) → Nat.le (Nat.succ 0) a → Prop : Type

structural recursion cannot be used

failed to prove termination, use `termination_by` to specify a well-founded relation

div 的这个定义会停机，因为第一个参数 n 在每次递归调用时都更小。 这可以使用 termination_by 子句来表示：

def div (n k : Nat) (ok : k > 0) : Nat :=
  if h : n < k then
    0
  else
    1 + div (n - k) k ok
termination_by div n k ok => n

现在，错误仅限于递归调用：

failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
n k : Nat
ok : k > 0
h : ¬n < k
⊢ n - k < n

This can be proved using a theorem from the standard library, Nat.sub_lt. This theorem states that (the curly braces indicate that n and k are implicit arguments). Using this theorem requires demonstrating that both n and k are greater than zero. Because k > 0 is syntactic sugar for 0 < k, the only necessary goal is to show that 0 < n. There are two possibilities: either n is 0, or it is n' + 1 for some other Nat n'. But n cannot be 0. The fact that the if selected the second branch means that ¬ n < k, but if n = 0 and k > 0 then n must be less than k, which would be a contradiction. This, n = Nat.succ n', and Nat.succ n' is clearly greater than 0. 这可以使用标准库中的定理 Nat.sub_lt 来证明。该定理指出 ∀ {n k : Nat}, 0 < n → 0 < k → n - k < n （花括号表示 n 和 k 是隐式参数）。使用此定理需要证明 n 和 k 都大于零。 因为 k > 0 是 0 < k 的语法糖，所以唯一必要的目标是证明 0 < n。 有两种可能性：n 为 0，或它为某个其他 Nat n' 的 n' + 1。 但 n 不能为 0。if 选择第二个分支的事实意味着 ¬ n < k， 但如果 n = 0 且 k > 0，则 n 必须小于 k，这将会产生矛盾。 在这里，n = Nat.succ n'，而 Nat.succ n' 明显大于 0。

div 的完整定义，包括停机证明：

def div (n k : Nat) (ok : k > 0) : Nat :=
  if h : n < k then
    0
  else
    have : 0 < n := by
      cases n with
      | zero => contradiction
      | succ n' => simp_arith
    have : n - k < n := by
      apply Nat.sub_lt <;> assumption
    1 + div (n - k) k ok
termination_by div n k ok => n

练习

证明以下定理：

• 对于所有的自然数 \( n \)，\( 0 < n + 1 \)。
• 对于所有的自然数 \( n \)，\( 0 \leq n \)。
• 对于所有的自然数 \( n \) 和 \( k \)，\( (n + 1) - (k + 1) = n - k \)
• 对于所有的自然数 \( n \) 和 \( k \), 若 \( k < n \) 则 \( n \neq 0 \)
• 对于所有的自然数 \( n \)，\( n - n = 0 \)
• 对于所有的自然数 \( n \) 和 \( k \)，若 \( n + 1 < k \) 则 \( n < k \)