8.4.1. 归并排序🔗

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

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

1. 如果一个输入列表为空，则结果是另一个列表。

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

这在任何列表上都不是结构化递归。递归停机是因为在每次递归调用中都会从两个列表中的一个中删除一个项， 但它可能是任何一个列表。Lean 在幕后使用这个事实来证明它停机：

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

这个分割函数是结构化递归的。

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

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

fail to show termination for
  mergeSort
with errors
failed to infer structural recursion:
Not considering parameter α of mergeSort:
  it is unchanged in the recursive calls
Not considering parameter #2 of mergeSort:
  it is unchanged in the recursive calls
Cannot use parameter xs:
  failed to eliminate recursive application
    mergeSort halves.fst


Could not find a decreasing measure.
The basic measures relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
            xs #1
1) 70:11-31  ?  ?
2) 70:34-54  _  _

#1: xs.length

Please use `termination_by` to specify a decreasing measure.

它能停机的原因是 splitList 总是返回比其输入更短的列表，至少在应用于包含至少两个元素的列表时是这样。 因此，halves.fst 和 halves.snd 的长度小于 xs 的长度。 这可以使用 termination_by 子句来表示：

有了这个子句，错误信息就变了。 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_1xs:List αh:¬xs.length < 2halves:List α × List α := splitList xs⊢ (splitList xs).fst.length < xs.length

8.4.2. 分割列表使其变短🔗

还需要证明 (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"])，这两个输出列表都比输入列表短。

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

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

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

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

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

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

unsolved goals
consα:Type u_1x:αxs:List αih:(splitList xs).fst.length ≤ xs.length ∧ (splitList xs).snd.length ≤ xs.length⊢ (splitList xs).snd.length ≤ xs.length ∧ (splitList xs).fst.length ≤ xs.length + 1

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

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

换句话说，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 的假设：

unsolved goals
cons.introα:Type u_1x:αxs:List αleft✝:(splitList xs).fst.length ≤ xs.lengthright✝:(splitList xs).snd.length ≤ xs.length⊢ (splitList xs).snd.length ≤ xs.length ∧ (splitList xs).fst.length ≤ xs.length + 1

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

unsolved goals
cons.intro.leftα:Type u_1x:αxs:List αleft✝:(splitList xs).fst.length ≤ xs.lengthright✝:(splitList xs).snd.length ≤ xs.length⊢ (splitList xs).snd.length ≤ xs.length

cons.intro.rightα:Type u_1x:αxs:List αleft✝:(splitList xs).fst.length ≤ xs.lengthright✝:(splitList xs).snd.length ≤ xs.length⊢ (splitList xs).fst.length ≤ xs.length + 1

left 目标与 left✝ 假设非常相似，所以 assumption 策略将其分派：

unsolved goals
cons.intro.rightα:Type u_1x:αxs:List αleft✝:(splitList xs).fst.length ≤ xs.lengthright✝:(splitList xs).snd.length ≤ xs.length⊢ (splitList xs).fst.length ≤ xs.length + 1

同样，right 目标类似于 right✝ 假设，除了目标仅将 + 1 添加到输入列表的长度。 现在是时候证明不等式成立了。

unsolved goals
n m:Nat⊢ n ≤ m → n ≤ m + 1

unsolved goals
n m:Nath:n ≤ m⊢ n ≤ m + 1

unsolved goals
refln m:Nat⊢ n ≤ n + 1

unsolved goals
stepn m m✝:Nata✝:n.le m✝ih:n ≤ m✝ + 1⊢ n ≤ m✝.succ + 1