Hi, Am Dienstag, den 18.09.2018, 10:21 +0200 schrieb Christian Sternagel:
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#...
(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.
just a shameless plug: As part of our hs-to-coq project, we mechanically translated Data.List.sort to Coq, proved its termination (for finite inputs, of course) and functional correctness; https://github.com/antalsz/hs-to-coq/blob/master/examples/containers/theorie...
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.
Cool! That’s of course not easily possible with out shallow embedding into Coq.
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: …
It _could_ have been benchmarked and measured and determined that it is actually faster to do less case analysis here. But I find that unlikely (both the investigation and this output), and it is probably simply an oversight, and I would expect that a patch to that effect would be appreciated ! Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/