Je plaisante avec Coq. Spécifiquement, j'essaye de mettre en application le mergesort et ensuite prouver que cela fonctionne.Limites de Fixpoint dans Coq?
Ma tentative de mise en œuvre était:
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.
Les erreurs que je reçois à la suite de ce sont:
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".
Mon interprétation de ces erreurs est que l et L0 sont ls sans sa tête, x, et ls sans x et l'élément après x (que je suppose qu'il a décidé d'appeler y?). C'est fou que je n'ai pas recurse sur une de ces listes et à la place récursivement sur une liste définie localement.
Suis-je autorisé à recurder uniquement sur les objets qui proviennent directement du motif? Si oui, cela semble être une limitation sévère. Y a-t-il des façons de le contourner Je devine que Coq ne peut pas dire que la fonction se terminera. Existe-t-il un moyen de prouver que gauche et droite sont plus petites que xs?