Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Limitations of Fixpoint in Coq?

Tags:

coq

totality

I am fooling around with Coq. Specifically, I am trying to implement mergesort and then prove that it works.

My attempt at an implementation was:

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.

The errors that I get as a result of this are:

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

My interpretation of these errors is that l and l0 are ls without its head, x, and ls without x and the element after x (which I guess it decided to call y?). It is mad that I did not recurse on one of these lists and instead recursed on a locally defined list.

Am I only allowed to recurse on things that come directly from the pattern match? If yes, this seems like a severe limitation. Are there ways around it? I am guessing that Coq can't tell that the function will terminate. Is there some way to prove to it that left and right are smaller than xs?

like image 776
mushroom Avatar asked Dec 10 '12 04:12

mushroom


1 Answers

It turns out that the chapter of CPDT on General Recursion addresses just that particular issue:

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

Read the section called Well-founded recursion, it implements the merge sort using well-founded recursion to help Coq's termination checker be happy.

There may be other ways to solve that problem using either Function or Program Fixpoint, but I think reading about well-founded recursion will not hurt.

like image 184
Ptival Avatar answered Nov 13 '22 06:11

Ptival