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

对于 nil 情形的目标，可以通过调用简化器并指示它展开 splitList 的定义来证明，因为空列表的长度小于或等于空列表的长度。 类似地，在 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 的一个证明由 And.intro 构造子应用于如下内容构成：在 left 字段中给出的 A 的证明，以及在 right 字段中给出的 B 的证明。

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