Limitations of Fixpoint in Coq?

Question

I am fooling around with Coq. Specifically, I am trying to implement mergesort and then prove that it works.

My attempt at an implementation was:

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".

My interpretation of these errors is that l and l0 are ls without its head, x, and ls without x and the element after x (which I guess it decided to call y?). It is mad that I did not recurse on one of these lists and instead recursed on a locally defined list.

Am I only allowed to recurse on things that come directly from the pattern match? If yes, this seems like a severe limitation. Are there ways around it? I am guessing that Coq can't tell that the function will terminate. Is there some way to prove to it that left and right are smaller than xs?

Answer 1

It turns out that the chapter of CPDT on General Recursion addresses just that particular issue:

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

Read the section called Well-founded recursion, it implements the merge sort using well-founded recursion to help Coq's termination checker be happy.

There may be other ways to solve that problem using either Function or Program Fixpoint, but I think reading about well-founded recursion will not hurt.