Ograniczenia Fixpoint w Coq?

Question

Oszukuję z Coq. W szczególności próbuję wdrożyć mergesort, a następnie udowodnić, że działa.

Moja próba implementacji było:

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. 

błędów, które dostaję w wyniku tego są:

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

Moja interpretacja tych błędów jest to, że L i l0 są ls bez jego głowa, x, i ls bez xi elementu po x (co, jak sądzę, zdecydowało się nazywać y?). To szaleństwo, że nie powróciłem na jedną z tych list i zamiast tego powróciłem na lokalnie zdefiniowaną listę.

Czy wolno mi się powtarzać tylko w przypadku rzeczy, które pochodzą bezpośrednio z dopasowania wzorca? Jeśli tak, wydaje się to poważnym ograniczeniem. Czy są na to sposoby? Zgaduję, że Coq nie może powiedzieć, że funkcja się zakończy. Czy jest jakiś sposób, aby udowodnić, że lewe i prawe są mniejsze niż xs?

Answer 1

Okazuje się, że rozdział CPDT na Walnym rekurencja rozwiązuje tylko ten konkretny problem:

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

Przeczytaj sekcję o nazwie Dobrze założony rekurencji, realizuje seryjnej sortowania używając ugruntowaną rekursji pomóż Coq'owi rozwiązać tester szczęścia.

Możliwe, że istnieją inne sposoby rozwiązania tego problemu przy użyciu albo Function lub Program Fixpoint, ale myślę, że czytanie o dobrze opracowanej rekursji nie zaszkodzi.