Coq中定點的侷限性？

Question

我正在與Coq鬼混。具體來說，我試圖實施mergesort，然後證明它的工作原理。

我在執行的嘗試是：

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和10是沒有LS它的頭，x和ls沒有x和x之後的元素（我想它決定調用y？）。我不會在這些列表中遞歸，而是在本地定義的列表上遞歸。

我只允許在模式匹配中直接發送的東西遞歸嗎？如果是的話，這似乎是一個嚴重的限制。有沒有辦法解決它？我猜測Coq不能說這個函數會終止。有什麼方法可以證明左右比xs小嗎？

Answer 1

事實證明，CPDT對一般遞歸章處理只是特定問題：

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

閱讀稱爲有根有據遞歸的部分，它實現了某種使用有根有據遞歸合併幫助Coq的終止檢查員感到高興。

可能還有其他方法可以使用Function或Program Fixpoint來解決這個問題，但我認爲閱讀有根有據的遞歸併不會造成傷害。