[Haskell-cafe] natural mergesort in Data.List

[Christian Sternagel]

Dear Cafe,

some years ago I formalized the mergesort implementation [1] from


http://hackage.haskell.org/package/base-4.11.1.0/docs/src/Data.OldList.html#sort

(as far as I can tell it didn't change since 2012) in the proof
assistant Isabelle/HOL [2].

More specifically, I proved its functional correctness (the result is
sorted and contains all elements of the input with exactly the same
multiplicities) and that it is a stable sorting algorithm.

Very recently I also formalized a complexity result in Isabelle/HOL,
namely that the number of comparisons is bounded from above by

  n + n * ⌈log 2 n⌉

for lists of length n.

For this proof I had to change the definition of "sequences",
"ascending", and "descending" slightly.

Now here is my question: Does anyone now of reasons why the current
implementation of "sequences" is allowed to produce spurious empty lists
in its result? The version I used in my formalization only differs in
the following three spots:

  sequences [x] = [[x]] -- this is the only important change, since
  sequences [] = []     -- then the result does not contain empty lists

instead of

  sequences xs = [xs]

and

  ascending a as [] = let !x = as [a] in [x]

instead of

  ascending a as bs = let !x = as [a] in x : sequences bs

and

  descending a as []  = [a:as]

instead of

  descending a as bs = (a:as) : sequences bs

[1] https://www.isa-afp.org/entries/Efficient-Mergesort.html
[2] http://isabelle.in.tum.de/