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.

The errors that I get as a result of this are:

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是没有它的头部x的ls，x后面的元素也不包括在它们内（我猜y是指这些元素）。由于我没有在这些列表之一上进行递归，而是在一个本地定义的列表上进行了递归，所以出现了错误。 我只能对来自模式匹配的东西进行递归吗？如果是的话，这似乎是一个严重的限制。有没有办法绕过它？我想Coq无法确定函数是否会终止。有没有一些方法证明left和right比xs小？

- mushroom

Answer 1

原来 CPDT 的关于 General Recursion 的一章就解决了这个问题:

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

阅读名为 Well-founded recursion 的部分，它使用良基递归来实现归并排序，以帮助 Coq 的终止检查器满意。

也许使用 Function 或 Program Fixpoint 还有其他解决该问题的方法，但我认为阅读关于良基递归的内容不会有坏处。

- Ptival