Merge Sort
This development is a specification and a proof of merge sort.Merge sort takes two arguments :
- a comparison function (morally less or equal)
- a list to sort
- a permutation of its imput
- sorted in increasing order (according to the comparison function)
It runs in constant heap space and logarithmic stack space and most of the auxiliary functions are tail recursive.
I like this development, since it shows that we can write and prove some efficient functions in Coq. The original code comes from the Ocaml library, I have made some modifications to get an efficient evaluation in Coq.