Ich mache mit Coq herumalbern. Insbesondere versuche ich, Mergesort zu implementieren und dann zu beweisen, dass es funktioniert.Einschränkungen des Fixpunkts in Coq?
Mein Versuch einer Umsetzung war:
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.
die Fehler, die ich als Folge davon zu bekommen sind:
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".
Meine Interpretation dieser Fehler, dass l und l0 sind ls ohne sein Kopf, x, und ls ohne x und das Element nach x (was ich denke, es entschieden, y zu nennen?). Es ist verrückt, dass ich nicht auf eine dieser Listen rekurriert habe und stattdessen auf einer lokal definierten Liste rekurriert habe.
Kann ich nur auf Dinge rekrutieren, die direkt aus der Musterübereinstimmung kommen? Wenn ja, scheint dies eine schwerwiegende Einschränkung zu sein. Gibt es Möglichkeiten um es herum? Ich vermute, dass Coq nicht sagen kann, dass die Funktion beendet wird. Gibt es einen Weg, um zu beweisen, dass links und rechts kleiner als xs sind?