Sto scherzando con Coq. Nello specifico, sto cercando di implementare mergesort e quindi di dimostrare che funziona.Limitazioni di Fixpoint in Coq?
Il mio tentativo di un'implementazione era:
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.
Gli errori che ottengo come risultato di questo sono:
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".
La mia interpretazione di questi errori è che l e l0 sono ls senza la sua testa, x, e ls senza x e l'elemento dopo x (che immagino abbia deciso di chiamare y?). È assurdo che non abbia reclamato su uno di questi elenchi e che invece sia stato ricorsivamente in una lista definita localmente.
Sono autorizzato solo a recitare su cose che provengono direttamente dalla corrispondenza di modello? Se sì, sembra una grave limitazione. Ci sono dei modi per aggirarlo? Sto indovinando che Coq non può dire che la funzione terminerà. C'è un modo per dimostrare che sinistra e destra sono più piccoli di xs?