coq - Coq 中 Fixpoint 的局限性？

Question

我正在和 Coq 鬼混。具体来说，我正在尝试实现合并排序，然后证明它是有效的。

我的实现尝试是:

Fixpoint sort ls :=
match ls with
| nil => nil
| cons x nil => cons x nil
| xs =>
  let (left, right) := split xs nil nil
  in merge (sort left) (sort right)
end.

因此我得到的错误是:

Error:
Recursive definition of sort is ill-formed.
In environment
sort : list nat -> list nat
ls : list nat
x : nat
l : list nat
y : nat
l0 : list nat
left : list nat
right : list nat
Recursive call to sort has principal argument equal to "left" instead of
one of the following variables: "l" "l0".
Recursive definition is:
"fun ls : list nat =>
match ls with
| nil => nil
| x :: nil => x :: nil
| x :: _ :: _ =>
    let (left, right) := split ls nil nil in merge (sort left) (sort right)
end".

我对这些错误的解释是，l 和 l0 是没有头部的 ls，x，以及没有 x 和 x 之后的元素的 ls(我猜它决定称之为 y？)。令人生气的是我没有在这些列表之一上递归，而是在本地定义的列表上递归。

我是否只允许递归直接来自模式匹配的内容？如果是的话，这似乎是一个严重的限制。有办法解决吗？我猜测 Coq 无法判断该函数将终止。有什么方法可以证明 left 和 right 都小于 xs 吗？

Answer 1

事实证明，CPDT 关于一般递归的章节正好解决了这个特定问题:

http://adam.chlipala.net/cpdt/html/GeneralRec.html

阅读名为“Well-founded recursion”的部分，它使用“well-founded recursion”实现合并排序，以帮助 Coq 的终止检查器满意。

可能还有其他方法可以使用函数或程序修复点来解决该问题，但我认为阅读有根据的递归不会有什么坏处。