This library provides a characterization of stable mergesort functions using
relational parametricity, and deduces several functional correctness results,
including stability, solely from the characteristic property. This library
allows the users to prove their mergesort correct just by proving that the
mergesort in question satisfies the characteristic property. The functional
correctness lemmas are overloaded using a canonical structure
(StableSort.function) that bundles the characteristic property, and
automatically apply to any declared instance of this structure.
As instances of the characteristic property, this library provides two kinds of optimized mergesorts. The first kind is non-tail-recursive mergesort. In call-by-need evaluation, they compute the first k smallest elements of a list of length n in O(n + k log k) time, which is known to be the optimal time complexity of the partial and incremental sorting problems. However, the non-tail-recursive merge function linearly consumes the call stack and triggers a stack overflow in call-by-value evaluation. The second kind is tail-recursive mergesorts and thus solves the above issue in call-by-value evaluation. However, it does not allow us to compute the output incrementally regardless of the evaluation strategy. In addition, each of the above two kinds of mergesort functions has a smooth (also called natural) variant of mergesort, which takes advantage of sorted slices in the input.
- Author(s):
- Kazuhiko Sakaguchi (initial)
- Cyril Cohen
- License: CeCILL-B Free Software License Agreement
- Compatible Coq versions: 8.19 or later
- Additional dependencies:
- Coq namespace:
stablesort - Related publication(s):
The theories/ directory is the main part of the library. The
icfp25/ directory contains Rocq files corresponding more closely
to the paper. The latter files are not a part of the installation (see below),
and explained further in the dedicated README file.
The easiest way to install the development version of Stable sort algorithms in Rocq and its dependencies is via OPAM:
git clone https://github.com/pi8027/stablesort.git
cd stablesort
opam repo add rocq-released https://rocq-prover.org/opam/releasedTo build and install the theories/ files:
opam install ./rocq-stablesort.opamAlternatively, to build and install only the dependencies:
opam install ./rocq-stablesort.opam --deps-only --with-testGiven that the dependencies are installed, you can use one of the following
make targets to manually build the Rocq files:
- The default target: builds the
theories/files. build-icfp25: builds theicfp25/files.validate: checks the compiledtheories/files and their dependencies and prints a summary about their context (such as axioms), which should show that thetheories/files are axiom-free.validate-icfp25: checks the compiledicfp25/files and their dependencies and prints a summary about their context, which should print the axiom of dependent functional extensionality (functional_extensionality_dep) on which the Equation plugin relies.
The mergesort functions and the stability proofs provided in this library are
mostly based on ones in the path library of Mathematical Components.