Ограничения Fixpoint в Coq?

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 и ls без x и элемента после x (который, я думаю, он решил назвать y?). Это безумие, что я не рекурсировал ни в одном из этих списков и вместо этого рекурсировал в локально определенном списке.

Могу ли я использовать только те вещи, которые исходят непосредственно из совпадения шаблонов? Если да, это кажется серьезным ограничением. Есть ли способы обойти это? Я предполагаю, что Coq не может сказать, что функция завершится. Есть ли способ доказать, что левый и правый меньше, чем хз?

Answer 1

Оказывается, что глава CPDT по общей рекурсии касается именно этой конкретной проблемы:

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

Прочтите раздел "Обоснованная рекурсия", в нем реализована сортировка слиянием с использованием обоснованной рекурсии, чтобы помочь программе проверки завершения Coq.

Могут быть и другие способы решения этой проблемы с использованием Function или же Program Fixpoint, но я думаю, что чтение об обоснованной рекурсии не повредит.