&= s_1 \concat s_2.    & (\text{\ref{item:s1_le_s2} and \cref{lemma:coq:allrel_merge}})
\end{align*}

For the second case, we show that
$\texttt{rev} ~ (\texttt{rev} ~ s'_2 \merge_\geq \texttt{rev} ~ s'_1) = s_1 \concat s_2$ holds
whenever $s_1 \concat s_2$ is pairwise sorted by $\leq$, which is equivalent to the following
conjunction (<ref>):

*  both $s_1$ and $s_2$ are pairwise sorted by $\leq$, and

*  $x \leq y$ holds for any $x \in s_1$ and $y \in s_2$,
or equivalently	(<ref>),
$y \geq x$ holds for any $y \in \texttt{rev} ~ s_2$ and $x \in \texttt{rev} ~ s_1$.

\begin{align*}
\texttt{rev} ~ (\texttt{rev} ~ s'_2 \merge_\geq \texttt{rev} ~ s'_1)
&= \texttt{rev} ~ (\texttt{rev} ~ s_2 \merge_\geq \texttt{rev} ~ s_1)
& (\text{\ref{item:s1_s2_pairwise'} and I.H.}) \\
&= \texttt{rev} ~ (\texttt{rev} ~ s_2 \concat \texttt{rev} ~ s_1)
& (\text{\ref{item:s1_le_s2'} and \cref{lemma:coq:allrel_merge}}) \\
&= s_1 \concat s_2.
& (\text{\cref{lemma:coq:rev_cat,lemma:coq:revK}})
\end{align*}

The last two cases are trivial.

For any transitive relation ${\leq} \subseteq T \times T$ and $s$ of type $\mathrm{list} ~ T$ sorted
by $\leq$, $\texttt{sort}_\leq ~ s$ is equal to $s$.

Lemma sorted_sort sort T (leT : rel T) :
transitive leT -> forall s : list T, sorted leT s -> sort T leT s = s.

Lemma sorted_sort_in sort T (P : pred T) (leT : rel T) :
in P        , transitive leT ->
forall s : list T, all P s -> sorted leT s -> sort T leT s = s.

This follows from <ref>.

For any ${\leq_1}, {\leq_2} \subseteq T \times T$ and $\mathit{xs}$ of type $\mathrm{list} ~ T$,
$\texttt{sort}_{\leq_1} ~ \mathit{xs}$ is sorted by the lexicographic order
${\leq_\mathrm{lex}} \coloneq {\leq_{(1, 2)}}$ whenever $\leq_1$ is total and $\mathit{xs}$ is
pairwise sorted by $\leq_2$.

Lemma sort_pairwise_stable sort T (leT leT' : rel T) : total leT ->
forall s : list T, pairwise leT' s -> sorted (lexord leT leT') (sort T leT s).

Lemma sort_pairwise_stable_in sort T (P : pred T) (leT leT' : rel T) :
in P    , total leT -> forall s : list T, all P s -> pairwise leT' s ->
sorted (lexord leT leT') (sort T leT s).

We prove it by induction on $\texttt{sort}_\leq ~ \mathit{xs}$ (<ref>).
See <ref> for details.

For any ${\leq_1}, {\leq_2} \subseteq T \times T$ and $\mathit{xs}$ of type $\mathrm{list} ~ T$,
$\texttt{sort}_{\leq_1} ~ \mathit{xs}$ is sorted by the lexicographic order
${\leq_\mathrm{lex}} \coloneq {\leq_{(1, 2)}}$ whenever $\leq_1$ is total, $\leq_2$ is transitive,
and $\mathit{xs}$ is sorted by $\leq_2$.

Lemma sort_stable sort T (leT leT' : rel T) : total leT -> transitive leT' ->
forall s : list T, sorted leT' s -> sorted (lexord leT leT') (sort T leT s).

Lemma sort_stable_in sort T (P : pred T) (leT leT' : rel T) :
in P    , total leT -> in P        , transitive leT' ->
forall s : list T, all P s -> sorted leT' s ->
sorted (lexord leT leT') (sort T leT s).

This follows from <ref>.

For any $p \subseteq T$, ${\leq} \subseteq T \times T$, and $s$ of type $\mathrm{list} ~ T$,
the numbers of the elements of $\texttt{sort}_\leq ~ s$ and $s$ satisfying $p$ are the same, ,
$\lvert \texttt{sort}_\leq ~ s \rvert_p = \lvert s \rvert_p$.

Lemma count_sort sort T (p : pred T) (leT : rel T) (s : list T) :
count p (sort T leT s) = count p s.

We prove it by induction on $\texttt{sort}_\leq ~ s$ (<ref>).
For the first case,

\begin{align*}
\lvert s'_1 \merge_\leq s'_2 \rvert_p
&= \lvert s'_1 \rvert_p + \lvert s'_2 \rvert_p
& (\text{\cref{lemma:coq:count_merge,lemma:coq:count_cat}}) \\
&= \lvert s_1 \rvert_p + \lvert s_2 \rvert_p   & (\text{I.H.}) \\
&= \lvert s_1 \concat s_2 \rvert_p.            & (\text{\cref{lemma:coq:count_cat}})
\intertext{For the second case,}
\lvert \texttt{rev} ~ (\texttt{rev} ~ s'_2 \merge_\geq \texttt{rev} ~ s'_1) \rvert_p
&= \lvert s'_2 \rvert_p + \lvert s'_1 \rvert_p
& (\text{\cref{lemma:coq:count_merge,lemma:coq:count_cat,lemma:coq:count_rev}}) \\
&= \lvert s'_1 \rvert_p + \lvert s'_2 \rvert_p \\
&= \lvert s_1 \rvert_p + \lvert s_2 \rvert_p   & (\text{I.H.}) \\
&= \lvert s_1 \concat s_2 \rvert_p.            & (\text{\cref{lemma:coq:count_cat}})
\end{align*}

The last two cases are trivial.

For any ${\leq} \subseteq T \times T$ and $s$ of type $\mathrm{list} ~ T$,
the lengths of $\texttt{sort}_\leq ~ s$ and $s$ are equal, ,
$\lvert \texttt{sort}_\leq ~ s \rvert = \lvert s \rvert$.

Lemma size_sort sort T (leT : rel T) (s : seq T) : size (sort T leT s) = size s.

This follows from <ref>.

Sorting the empty list gives the empty list.

Lemma sort_nil sort T (leT : rel T) : sort T leT [::] = [::].

The length of $\texttt{sort}_\leq ~ []$ is $0$ (<ref>), and thus, it must be
the empty list.

For any $p \subseteq T$, ${\leq} \subseteq T \times T$, and $s$ of type $\mathrm{list} ~ T$,
all elements of $\texttt{sort}_\leq ~ s$ satisfy $p$ iff all elements of $s$ satisfy $p$.

Lemma all_sort sort T (p : pred T) (leT : rel T) (s : list T) :
all p (sort T leT s) = all p s.

This follows from <ref>.

For any ${\leq} \subseteq T \times T$ and $s$ of type $\mathrm{list} ~ T$,
$\texttt{sort}_\leq ~ s$ is a permutation of $s$.

Lemma perm_sort sort (T : eqType) (leT : rel T) (s : list T) :
perm_eql (sort T leT s) s.

This follows from <ref>.

For any ${\leq} \subseteq T \times T$ and $s$ of type $\mathrm{list} ~ T$,
$\texttt{sort}_\leq ~ s$ has the same set of elements as $s$.

Lemma mem_sort sort (T : eqType) (leT : rel T) (s : list T) : sort T leT s =i s.

This follows from <ref>.

For any ${\leq} \subseteq T \times T$ and $s$ of type $\mathrm{list} ~ T$,
$\texttt{sort}_\leq ~ s$ is duplication free iff $s$ is duplication free.

Lemma sort_uniq sort (T : eqType) (leT : rel T) (s : list T) :
uniq (sort T leT s) = uniq s.

This follows from <ref>.

For any total preorder ${\leq} \subseteq T \times T$ and predicate $p \subseteq T$,
$\texttt{filter}_p$ commutes with $\texttt{sort}_\leq$ under function composition; that is, the
following equation holds for any $s$ of type $\mathrm{list} ~ T$:

\[
\texttt{filter}_p ~ (\texttt{sort}_\leq ~ s) =
\texttt{sort}_\leq ~ (\texttt{filter}_p ~ s).
\]

Lemma filter_sort sort T (leT : rel T) : total leT -> transitive leT ->
forall (p : pred T) (s : seq T), filter p (sort T leT s) = sort T leT (filter p s).

Lemma filter_sort_in sort T (P : pred T) (leT : rel T) :
in P    , total leT -> in P        , transitive leT ->
forall (p : pred T) (s : seq T),
all P s -> filter p (sort T leT s) = sort T leT (filter p s).

This follows mainly from
See the proof of <ref> for details.

For any total preorder ${\leq} \subseteq T \times T$, predicate $p \subseteq T$, and $s$ of type
$\mathrm{list} ~ T$,

\[
\texttt{filter}_p ~ (\texttt{sort}_\leq ~ s) = \texttt{filter}_p ~ s
\]

holds whenever $\texttt{filter}_p ~ s$ sorted by $\leq$.

Lemma sorted_filter_sort sort T (leT : rel T) :
total leT -> transitive leT ->
forall (p : pred T) (s : list T),
sorted leT (filter p s) -> filter p (sort _ leT s) = filter p s.

Lemma sorted_filter_sort_in sort T (P : pred T) (leT : rel T) :
in P    , total leT -> in P        , transitive leT ->
forall (p : pred T) (s : list T),
all P s -> sorted leT (filter p s) -> filter p (sort _ leT s) = filter p s.

This follows from <ref>.

For any total preorders ${\leq_1}, {\leq_2} \subseteq T \times T$,
sorting a list with $\leq_2$ and then $\leq_1$ gives the same result as sorting the same list with
the lexicographic order ${\leq_\mathrm{lex}} \coloneq {\leq_{(1, 2)}}$;
that is, the following equation holds for any $s$ of type $\mathrm{list} ~ T$:

\[
\texttt{sort}_{\leq_1} ~ (\texttt{sort}_{\leq_2} ~ s) = \texttt{sort}_{\leq_\mathrm{lex}} ~ s.
\]

Lemma sort_sort sort T (leT leT' : rel T) :
total leT -> transitive leT -> total leT' -> transitive leT' ->
forall s : list T, sort T leT (sort T leT' s) = sort T (lexord leT leT') s.

Lemma sort_sort_in sort T (P : pred T) (leT leT' : rel T) :
in P    , total leT -> in P        , transitive leT ->
in P    , total leT' -> in P        , transitive leT' ->
forall s : list T,
all P s -> sort T leT (sort T leT' s) = sort T (lexord leT leT') s.

As in the proof of <ref>, we replace $s$ everywhere with
$\texttt{map}_{\texttt{nth} ~ x_0 ~ s} ~ [0, \dots, \lvert s \rvert - 1]$
(<ref>), use the naturality of  (<ref>), and
apply the congruence rule with respect to .
It remains to prove

\[
\texttt{sort}_{\leq'_1} ~ (\texttt{sort}_{\leq'_2} ~ [0, \dots, \lvert s \rvert - 1])
= \texttt{sort}_{\leq'_\mathrm{lex}} ~ [0, \dots, \lvert s \rvert - 1]
\]

where $\leq'_1$, $\leq'_2$, and $\leq'_\mathrm{lex}$ are the preimages of
$\leq_1$, $\leq_2$, and $\leq_\mathrm{lex}$ under $\texttt{nth} ~ x_0 ~ s$, respectively.
Thanks to <ref>, each side of the above equation is respectively sorted by

* the (right-associative) lexicographic composition of $\leq'_1$, $\leq'_2$, and
$<_\mathbb{N}$, and

* the lexicographic composition of $\leq'_\mathrm{lex}$ and $<_\mathbb{N}$, which is by
definition equal to the (left-associative) lexicographic composition of $\leq'_1$,
$\leq'_2$, and $<_\mathbb{N}$

* $\leq'_1$, $\leq'_2$, and their lexicographic composition $\leq'_\mathrm{lex}$ are total

* $\leq'_2$, $<_\mathbb{N}$, and their lexicographic composition are transitive
(<ref>), and

* $[0, \dots, \lvert s \rvert - 1]$ is sorted by $<_\mathbb{N}$

Two lexicographic compositions of $\leq'_1$, $\leq'_2$, and $<_\mathbb{N}$ are equivalent
regardless of the associativity (<ref>), and transitive
(<ref>) and irreflexive.
Both sides of the equation have the same set of elements (<ref>).
Therefore, these two lists are equal (<ref>).

For any ${\leq} \subseteq T \times T$ and $s$ of type $\mathrm{list} ~ T$,
$\texttt{sort}_\leq ~ s$ is sorted by $\leq$ whenever $\leq$ is total.

Lemma sort_sorted sort T (leT : rel T) :
total leT -> forall s : list T, sorted leT (sort T leT s).

Lemma sort_sorted_in sort T (P : pred T) (leT : rel T) :
in P    , total leT ->
forall s : list T, all P s -> sorted leT (sort T leT s).

Since $s$ is sorted by the trivial relation $\mathrel{R}$ such that $x \mathrel{R} y$ holds for any
$x, y \in T$, <ref> implies that $\texttt{sort}_\leq ~ s$ is sorted by the
lexicographic order of $\leq$ and $\mathrel{R}$, which is equivalent to $\leq$.

For any total order ${\leq} \subseteq T \times T$, and $s_1$ and $s_2$ of type $\mathrel{list} ~ T$,
$\texttt{sort}_\leq ~ s_1 = \texttt{sort}_\leq ~ s_2$ holds iff $s_1$ is a permutation of $s_2$.

Lemma perm_sortP sort (T : eqType) (leT : rel T) :
total leT -> transitive leT -> antisymmetric leT ->
forall s1 s2 : list T,
reflect (sort T leT s1 = sort T leT s2) (perm_eq s1 s2).

Lemma perm_sort_inP sort (T : eqType) (leT : rel T) (s1 s2 : list T) :
in s1    , total leT -> in s1        , transitive leT ->
in s1    , antisymmetric leT ->
reflect (sort T leT s1 = sort T leT s2) (perm_eq s1 s2).

Since $\texttt{sort}_\leq ~ s_1$ and $\texttt{sort}_\leq ~ s_2$ are respectively permutations of
$s_1$ and $s_2$, $\texttt{sort}_\leq ~ s_1 \permeq \texttt{sort}_\leq ~ s_2$ holds iff
$s_1 \permeq s_2$ holds. Therefore, ($\Rightarrow$) is trivial.

($\Leftarrow$) $\texttt{sort}_\leq ~ s_1$ and $\texttt{sort}_\leq ~ s_2$ are sorted by $\leq$
(<ref>) and permutation of each other.
Thanks to <ref>, these two sorted lists are equal.

For any two stable sort functions $\texttt{sort}$ and $\texttt{sort}'$ and total preorder
${\leq} \subseteq T \times T$, $\texttt{sort}_\leq$ and $\texttt{sort}'_\leq$ are extensionally
equal; that is, $\texttt{sort}_\leq ~ s = \texttt{sort}'_\leq ~ s$ holds for any $s$ of type
$\mathrm{list} ~ T$.

Lemma eq_sort sort1 sort2 T (leT : rel T) :
total leT -> transitive leT -> sort1 T leT =1 sort2 T leT.

Lemma eq_in_sort sort1 sort2 T (P : pred T) (leT : rel T) :
in P    , total leT -> in P        , transitive leT ->
forall s : list T, all P s -> sort1 T leT s = sort2 T leT s.

We replace $s$ everywhere with
$\texttt{map}_{\texttt{nth} ~ x_0 ~ s} ~ [0, \dots, \lvert s \rvert - 1]$
(<ref>), use the naturality of $\texttt{sort}$ and $\texttt{sort}'$
(<ref>), and apply the congruence rule with respect to .
It remains to prove

\[
\texttt{sort}_{\leq_I} ~ [0, \dots, \lvert s \rvert - 1]
= \texttt{sort}'_{\leq_I} ~ [0, \dots, \lvert s \rvert - 1]
\]

where $x \leq_I y \coloneq \texttt{nth} ~ x_0 ~ s ~ x \leq \texttt{nth} ~ x_0 ~ s ~ y$.

Since $[0, \dots, \lvert s \rvert - 1]$ is sorted by $<_\mathbb{N}$
(<ref>), both sides of the above equation are sorted by $<_I$, the
lexicographic composition of $\leq_I$ and $<_\mathbb{N}$ (<ref>).
These two lists have the same set of elements (<ref>).
Therefore, they are equal (<ref>).

For any total preorder ${\leq} \subseteq T \times T$ and $s$ of type $\mathrm{list} ~ T$,
$\texttt{sort}_\leq ~ s = \texttt{isort}_\leq ~ s$ holds for the insertion sort
defined as follows.

\begin{align*}
\texttt{isort}_\leq ~ [] &\coloneq [] \\
\texttt{isort}_\leq ~ (x :: s) &\coloneq [x] \merge_\leq \texttt{isort}_\leq ~ s.
\end{align*}

Lemma eq_sort_insert sort T (leT : rel T) : total leT -> transitive leT ->
sort T leT =1 foldr (fun x : T => merge leT [:: x]) [::].

Lemma eq_in_sort_insert sort T (P : pred T) (leT : rel T) :
in P    , total leT -> in P        , transitive leT ->
forall s : list T, all P s ->
sort T leT s = foldr (fun x : T => merge leT [:: x]) [::] s.

This follows from <ref> and the fact that  satisfies our
characterization property.

For any total preorder ${\leq} \subseteq T \times T$, and $s_1$ and $s_2$ of type
$\mathrm{list} ~ T$,
$\texttt{sort}_\leq ~ (s_1 \concat s_2) =
\texttt{sort}_\leq ~ s_1 \merge_\leq \texttt{sort}_\leq ~ s_2$

Lemma sort_cat sort T (leT : rel T) : total leT -> transitive leT ->
forall s1 s2 : seq T,
sort T leT (s1 ++ s2) = merge leT (sort T leT s1) (sort T leT s2).

Lemma sort_cat_in sort T (P : pred T) (leT : rel T) :
in P    , total leT -> in P        , transitive leT ->
forall s1 s2 : seq T, all P s1 -> all P s2 ->
sort T leT (s1 ++ s2) = merge leT (sort T leT s1) (sort T leT s2).

We replace all the occurrences of  with the insertion sort
(<ref>), and prove the following equation by induction on $s_1$:

\[
\texttt{isort}_\leq ~ (s_1 \concat s_2) =
\texttt{isort}_\leq ~ s_1 \merge_\leq \texttt{isort}_\leq ~ s_2.
\]

If $s_1 = []$, the equation holds by definition.
Otherwise, $s_1 = x :: s'_1$ and

\begin{align*}
\texttt{isort}_\leq ~ (s_1 \concat s_2)
&= [x] \merge_\leq \texttt{isort}_\leq ~ (s'_1 \concat s_2)
& (\text{Definition}) \\
&= [x] \merge_\leq (\texttt{isort}_\leq ~ s'_1 \merge_\leq \texttt{isort}_\leq ~ s_2)
& (\text{I.H.}) \\
&= ([x] \merge_\leq \texttt{isort}_\leq ~ s'_1) \merge_\leq \texttt{isort}_\leq ~ s_2
& (\text{\cref{lemma:coq:mergeA}}) \\
&= \texttt{isort}_\leq ~ s_1 \merge_\leq \texttt{isort}_\leq ~ s_2.
& (\text{Definition}) & \qedhere
\end{align*}

For any total preorder ${\leq} \subseteq T \times T$, $s$ of type $\mathrm{list} ~ T$, and $m$ of
type $\mathrm{list} ~ \mathrm{bool}$, there exists $m'$ of type $\mathrm{list} ~ \mathrm{bool}$
that satisfies
$\texttt{mask}_{m'} ~ (\texttt{sort}_\leq ~ s) = \texttt{sort}_\leq ~ (\texttt{mask}_m ~ s)$.

Lemma mask_sort sort T (leT : rel T) : total leT -> transitive leT ->
forall (s : list T) (m : list bool),
m_s : list bool | mask m_s (sort T leT s) = sort T leT (mask m s).

Lemma mask_sort_in sort T (P : pred T) (leT : rel T) :
in P    , total leT -> in P        , transitive leT ->
forall (s : list T) (m : list bool), all P s ->
m_s : list bool | mask m_s (sort T leT s) = sort T leT (mask m s).

We replace $s$ everywhere with
$\texttt{map}_{\texttt{nth} ~ x_0 ~ s} ~ [0, \dots, \lvert s \rvert - 1]$
(<ref>), use the naturality of  (<ref>) and
(<ref>), and apply the congruence rule with respect to
It suffices to find $m'$ such that

\[
\texttt{mask}_{m'} ~ (\texttt{sort}_{\leq_I} ~ [0, \dots, \lvert s \rvert - 1])
= \texttt{sort}_{\leq_I} ~ (\texttt{mask}_m ~ [0, \dots, \lvert s \rvert - 1])
\]

where $i \leq_I j \coloneq \texttt{nth} ~ x_0 ~ s ~ i \leq \texttt{nth} ~ x_0 ~ s ~ j$.
We show that
$m' \coloneq \texttt{map}_p ~ (\texttt{sort}_{\leq_I} ~ [0, \dots, \lvert s \rvert - 1])$
where $p ~ i \coloneq i \in \texttt{mask}_m ~ [0, \dots, \lvert s \rvert - 1]$ satisfy the above

\begin{align*}
& \texttt{mask}_{m'} ~ (\texttt{sort}_{\leq_I} ~ [0, \dots, \lvert s \rvert - 1]) \\
={} & \texttt{filter}_p ~ (\texttt{sort}_{\leq_I} ~ [0, \dots, \lvert s \rvert - 1])
& (\text{\cref{lemma:coq:filter_mask}}) \\
={} & \texttt{sort}_{\leq_I} ~ (\texttt{filter}_p ~ [0, \dots, \lvert s \rvert - 1])
& (\text{\cref{lemma:coq:filter_sort}}) \\
={} & \texttt{sort}_{\leq_I} ~ (\texttt{mask}_m ~ [0, \dots, \lvert s \rvert - 1]).
& (\text{\cref{lemma:coq:mask_filter,lemma:coq:iota_uniq}}) & \qedhere
\end{align*}

For any total preorder ${\leq} \subseteq T \times T$, $s$ of type $\mathrm{list} ~ T$, and $m$ of
type $\mathrm{list} ~ \mathrm{bool}$, there exists $m'$ of type $\mathrm{list} ~ \mathrm{bool}$
that satisfies $\texttt{mask}_{m'} ~ (\texttt{sort}_\leq ~ s) = \texttt{mask}_m ~ s$, whenever
$\texttt{mask}_m ~ s$ is sorted by $\leq$.

Lemma sorted_mask_sort sort T (leT : rel T) : total leT -> transitive leT ->
forall (s : list T) (m : list bool), sorted leT (mask m s) ->
m_s : list bool | mask m_s (sort T leT s) = mask m s.

Lemma sorted_mask_sort_in sort T (P : pred T) (leT : rel T) :
in P    , total leT -> in P        , transitive leT ->
forall (s : list T) (m : list bool), all P s -> sorted leT (mask m s) ->
m_s : list bool | mask m_s (sort T leT s) = mask m s.

This follows from <ref>.

For any total preorder ${\leq} \subseteq T \times T$, $\texttt{sort}_\leq$ preserves the subsequence
relation; that is, for any $t$ and $s$ of type $\mathrm{list} ~ T$,
$\texttt{sort}_\leq ~ t$ is a subsequence of $\texttt{sort}_\leq ~ s$ whenever $t$ is a subsequence
of $s$.

Lemma subseq_sort sort (T : eqType) (leT : rel T) :
total leT -> transitive leT ->
forall t s : list T, subseq t s -> subseq (sort T leT t) (sort T leT s).

Lemma subseq_sort_in sort (T : eqType) (leT : rel T) (t s : list T) :
in s    , total leT -> in s        , transitive leT ->
subseq t s -> subseq (sort T leT t) (sort T leT s).

Using <ref> that $t$ is a subsequence of $s$ iff there exists $m$ of the same
size as $s$ such that $t = \texttt{mask}_m~s$, we are left to show that
$\texttt{sort}_{\leq} ~ (\texttt{mask}_m~s)$ is a subsequence of $\texttt{sort}_{\leq}~s$.
Now, by <ref>, there is a mask $m'$ such that
$\texttt{sort}_{\leq} ~ (\texttt{mask}_m~s) = \texttt{mask}_{m'} ~ (\texttt{sort}_{\leq}~s)$
which is indeed a subsequence of $\texttt{sort}_{\leq}~s$ (<ref>).

For any total preorder ${\leq} \subseteq T \times T$, and $t$ and $s$ of type $\mathrm{list} ~ T$,
$t$ is a subsequence of $\texttt{sort}_\leq ~ s$ whenever $t$ is a subsequence of $s$ and sorted by

Lemma sorted_subseq_sort sort (T : eqType) (leT : rel T) :
total leT -> transitive leT ->
forall t s : list T, subseq t s -> sorted leT t -> subseq t (sort T leT s).

Lemma sorted_subseq_sort_in sort (T : eqType) (leT : rel T) (t s : list T) :
in s    , total leT -> in s        , transitive leT ->
subseq t s -> sorted leT t -> subseq t (sort T leT s).

This follows from <ref>.

For any total preorder ${\leq} \subseteq T \times T$, $s$ of type $\mathrm{list} ~ T$, and $x$ and
$y$ of type $T$, $x$ and $y$ occur in order in $\texttt{sort}_\leq ~ s$ whenever $x \leq y$ holds
and $x$ and $y$ occur in order in $s$.

Lemma mem2_sort sort (T : eqType) (leT : rel T) :
total leT -> transitive leT ->
forall (s : list T) (x y : T),
leT x y -> mem2 s x y -> mem2 (sort T leT s) x y.

Lemma mem2_sort_in sort (T : eqType) (leT : rel T) (s : list T) :
in s    , total leT -> in s        , transitive leT ->
forall x y : T, leT x y -> mem2 s x y -> mem2 (sort T leT s) x y.

If $x = y$, the statement means that all the elements of $s$ are in
$\texttt{sort}_{\leq}~s$, which is a consequence of <ref>.
Otherwise we remark that $x$ and $y$ occur in order in $s$ iff the sequence
$[x, y]$ is a subsequence of $s$ (<ref>).
Using <ref>, we thus have
that $\texttt{sort}_{\leq} ~ [x, y]$ is a subsequence of $\texttt{sort}_{\leq}~s$.
Since $x \leq y$, we have that $\texttt{sort}_{\leq}~[x, y] = [x, y]$ (, by
computation through <ref>), hence $[x, y]$ a
subsequence of $\texttt{sort}_{\leq}~s$.

§ COMPARISON OF FORMULATIONS OF THE STABILITY

In this appendix, we compare the statements of the stability results we proved with those of related
work <cit.>.
proved the stability of a mergesort function in the following form.

For any total preorder $\leq$ on $T$, the equivalent elements, such that $x$ and $y$ satisfying
$x \sim y \coloneq x \leq y \land y \leq x$, always appear in the same order in the input and
output of sorting; that is, the following equation holds for any $x$ of type $T$ and $s$ of type
$\mathrm{list} ~ T$:

\[
[y \leftarrow \texttt{sort}_\leq ~ s \mid x \sim y] = [y \leftarrow s \mid x \sim y].
\]

Lemma sort_stable_leroy sort T (leT : rel T) :
total leT -> transitive leT ->
forall (x : T) (s : list T),
[seq y <- sort T leT s | leT x y        leT y x] =
[seq y <- s | leT x y        leT y x].

This follows from <ref>.
It suffices to show that $[y \leftarrow s \mid x \sim y]$ is sorted by $\leq$, which is trivial
since its all elements are equivalent to $x$.

proved the stability of
's mergesort in the following form, where the total preorder on $T$ is decomposed into a totally
ordered type $T'$ and a keying function $k$ of type $T \to T'$.

Let $k : T \to T'$ be a keying function whose codomain $T'$ is totally ordered by $\leq_{T'}$,
and ${\leq_T} \subseteq T \times T$ be the total preorder induced by $k$, ,
$x \leq_T y \coloneq k ~ x \leq_{T'} k ~ y$.
For any $s$ of type $\mathrm{list} ~ T$, the relative order of the elements of $s$ having the same
key is preserved by $\texttt{sort}_{\leq_T} ~ s$; that is, the following equation holds for any
$x$ of type $T$:

\[
[y \leftarrow \texttt{sort}_{\leq_T} ~ s \mid k ~ x = k ~ y] = [y \leftarrow s \mid k ~ x = k ~ y].
\]

Lemma sort_stable_sternagel
sort T (d : unit) (T' : orderType d) (key : T -> T') (x : T) (s : list T) :
[seq y <- sort T (relpre key <=
[seq y <- s | key x == key y].

where orderType is the interface of totally ordered types and <=
to a totally ordered type.

Since $\leq_{T'}$ is total order hence antisymmetric,
$x$ and $y$ of type $T$ have the same key ($k ~ x = k ~ y$) iff they have the same order
($x \leq_T y \land y \leq_T x$).
Since $\leq_T$ is total preorder, this follows from <ref>.

As it can be seen, both <ref> are
immediate consequences of <ref>, which follows from
As we argued in <ref>, <ref>
have the advantage that it can be used in a place
<ref> do not directly apply, , where
the predicate is not one collecting equivalent elements.
although <ref> imply
<ref>, and thus, <ref>.

§ DEFINITIONS OF MERGESORTS IN

In <ref>, we presented structurally-recursive non-tail-recursive and tail-recursive
mergesorts in .
In this appendix, we present their reimplementations, including some optimized ones such as
smooth variants (<ref>).
The formal correctness proofs of these implementations are omitted in this appendix and available
only in the supplementary material.

§.§ Non-tail-recursive mergesorts in

Module Type MergeSig.
Parameter merge : forall (T : Type) (leT : rel T), list T -> list T -> list T.
Parameter mergeE : forall (T : Type) (leT : rel T), merge leT =2 path.merge leT.
End MergeSig.

Module Merge <: MergeSig.

Fixpoint merge (T : Type) (leT : rel T) (xs ys : list T) : list T :=
if xs is x :: xs' then
(fix merge' (ys : list T) : list T :=
if ys is y :: ys' then
if leT x y then x :: merge leT xs' ys else y :: merge' ys'
else xs) ys
else ys.

Lemma mergeE (T : Type) (leT : rel T) : merge leT =2 path.merge leT.

End Merge.

Structurally-recursive non-tail-recursive merge in , , the counterpart of
merge in <ref>.

Module CBN_ (M : MergeSig).
Section CBN.
Context (T : Type) (leT : rel T).

Fixpoint push (xs : list T) (stack : list (list T)) struct stack :
list (list T) :=
match stack with
| [::] :: stack | [::] as stack => xs :: stack
| ys :: stack => [::] :: push (M.merge leT ys xs) stack

Fixpoint pop (xs : list T) (stack : list (list T)) struct stack : list T :=
if stack is ys :: stack then pop (M.merge leT ys xs) stack else xs.

Fixpoint sort1rec (stack : list (list T)) (xs : list T) struct xs : list T :=
if xs is x :: xs then sort1rec (push [:: x] stack) xs else pop [::] stack.

Definition sort1 : list T -> list T := sort1rec [::].

Fixpoint sort2rec (stack : list (list T)) (xs : list T) struct xs : list T :=
if xs is x1 :: x2 :: xs then
let t := if leT x1 x2 then [:: x1; x2] else [:: x2; x1] in
sort2rec (push t stack) xs
else pop xs stack.

Definition sort2 : list T -> list T := sort2rec [::].

End CBN.
End CBN_.

Structurally-recursive non-tail-recursive mergesorts in .
The push, pop, sort1rec, and sort1 functions in this figure are the counterparts of push, pop, sort_rec, and sort in
Some optimized implementations are omitted here as marked by [..] and shown in

In <ref>, we define a module type <cit.>
MergeSig abstracting out a non-tail-recursive merge function, and then, define one of its
instances Merge using the nested fixpoint technique (<ref>).
The purpose of this module type is to allow replacement of the implementation of merge function; for
example, one may replace the merge function with one that uses a single fixpoint and an explicit
termination proof, which has better performance in extracted <cit.> and code, and thus, is used in our benchmark (<ref>).
Therefore, the non-tail-recursive mergesort functions in <ref>
are provided as a functor module CBN_ that takes an instance M of MergeSig as a
In order to prove the mergesort functions in the CBN_ module correct, MergeSig and
Merge are equipped with the proof mergeE that the merge function implemented in the
module is extensionally equal to the one in the library (path.merge in
<ref>, or <ref>).

Inside the CBN_ module, we introduce a type T and a relation leT on T as
section variables <cit.>.
After closing the CBN section, these variables become inaccessible and declarations in the
section will be parameterized by them.
The functions push, pop, sort1rec, and sort1 inside this module correspond
to push, pop, sort_rec, and sort in
<ref>, respectively.

Fixpoint sort3rec (stack : list (list T)) (xs : list T) struct xs : list T :=
match xs with
| x1 :: x2 :: x3 :: xs =>
let t :=
if leT x1 x2 then
if leT x2 x3 then [:: x1; x2; x3]
else if leT x1 x3 then [:: x1; x3; x2] else [:: x3; x1; x2]
if leT x1 x3 then [:: x2; x1; x3]
else if leT x2 x3 then [:: x2; x3; x1] else [:: x3; x2; x1]
sort3rec (push t stack) xs
| [:: x1; x2] => pop (if leT x1 x2 then xs else [:: x2; x1]) stack
| _ => pop xs stack

Definition sort3 : list T -> list T := sort3rec [::].

A structurally-recursive non-tail-recursive mergesorts in , that takes three elements
from the input at a time. This implementation is omitted in the place marked by [..] in

Fixpoint sortNrec (stack : list (list T)) (x : T) (xs : list T) struct xs :
list T :=
if xs is y :: xs then
if leT x y then incr stack y xs [:: x] else decr stack y xs [:: x]
pop [:: x] stack
with incr (stack : list (list T)) (x : T) (xs accu : list T) struct xs :
list T :=
if xs is y :: xs then
if leT x y then
incr stack y xs (x :: accu)
sortNrec (push (catrev accu [:: x]) stack) y xs
pop (catrev accu [:: x]) stack
with decr (stack : list (list T)) (x : T) (xs accu : list T) struct xs :
list T :=
if xs is y :: xs then
if leT x y then
sortNrec (push (x :: accu) stack) y xs
decr stack y xs (x :: accu)
pop (x :: accu) stack.

Definition sortN (xs : list T) : list T :=
if xs is x :: xs then sortNrec [::] x xs else [::].

A smooth structurally-recursive non-tail-recursive mergesort in . This implementation
is omitted in the place marked by [..] in <ref>.

The sort2 function is an optimized variants of sort1 that perform sorting by
repetitively taking taking two elements from the input, locally sorting them, and pushing them to
the stack.
Similarly, the sort3 function in <ref> takes three
elements from the input at a time which is analogous to the optimization technique employed by
List.stable_sort of (see the end of <ref>).

The sortN function in <ref> is a smooth
structurally-recursive non-tail-recursive mergesort that takes the longest sorted prefix from the
input instead of a fixed number of elements.
The sortNrec function determines whether the prefix is increasing or decreasing one, and calls
either incr or decr depending on that.
The incr and decr respectively takes the longest weakly increasing and strictly
decreasing slice from the input, push it to the stack, and call sortNrec to process the next
sorted slice.
These three functions are made mutually recursive to pass the termination checker of .

§.§ Tail-recursive mergesorts in

Module Type RevmergeSig.
Parameter revmerge :
forall (T : Type) (leT : rel T), list T -> list T -> list T.
Parameter revmergeE : forall (T : Type) (leT : rel T) (xs ys : list T),
revmerge leT xs ys = rev (path.merge leT xs ys).
End RevmergeSig.

Module Revmerge <: RevmergeSig.

Fixpoint merge_rec (T : Type) (leT : rel T) (xs ys accu : list T) struct xs :
list T :=
if xs is x :: xs' then
(fix merge_rec' (ys accu : list T) struct ys :=
if ys is y :: ys' then
if leT x y then
merge_rec leT xs' ys (x :: accu) else merge_rec' ys' (y :: accu)
catrev xs accu) ys accu
else catrev ys accu.

Definition revmerge (T : Type) (leT : rel T) (xs ys : list T) : list T :=
merge_rec leT xs ys [::].

Lemma revmergeE (T : Type) (leT : rel T) (xs ys : list T) :
revmerge leT xs ys = rev (path.merge leT xs ys).

End Revmerge.

Structurally-recursive tail-recursive merge in . The merge_rec function in this
figure is the counterpart of revmerge in <ref>, and
revmerge in this figure instantiate it with [] as the accumulator.

Module CBV_ (M : RevmergeSig).
Section CBV.
Context (T : Type) (leT : rel T).
Let geT x y := leT y x.

Fixpoint push (xs : list T) (stack : list (list T)) struct stack :
list (list T) :=
match stack with
| [::] :: stack | [::] as stack => xs :: stack
| ys :: [::] :: stack | ys :: ([::] as stack) =>
[::] :: M.revmerge leT ys xs :: stack
| ys :: zs :: stack =>
[::] :: [::] :: push (M.revmerge geT (M.revmerge leT ys xs) zs) stack

Fixpoint pop (mode : bool) (xs : list T) (stack : list (list T)) struct stack
: list T :=
match stack, mode with
| [::], true => rev xs
| [::], false => xs
| [::] :: [::] :: stack, _ => pop mode xs stack
| [::] :: stack, _ => pop (   mode) (rev xs) stack
| ys :: stack, true => pop false (M.revmerge geT xs ys) stack
| ys :: stack, false => pop true (M.revmerge leT ys xs) stack

Fixpoint sort1rec (stack : list (list T)) (xs : list T) struct xs : list T :=
if xs is x :: xs then
sort1rec (push [:: x] stack) xs
pop false [::] stack.

Definition sort1 : list T -> list T := sort1rec [::].

Fixpoint sort2rec (stack : list (list T)) (xs : list T) struct xs : list T :=
if xs is x1 :: x2 :: xs then
let t := if leT x1 x2 then [:: x1; x2] else [:: x2; x1] in
sort2rec (push t stack) xs
else pop false xs stack.

Definition sort2 : list T -> list T := sort2rec [::].

End CBV.
End CBV_.

Structurally-recursive tail-recursive mergesorts in .
The push, pop, sort1rec, and sort1 functions in this figure are the counterparts of push, pop, sort_rec, and sort in
Some optimized implementations are omitted here as marked by [..] and shown in

Similarly to the non-tail-recursive counterpart
(<ref> in
<ref>), we define a module type RevmergeSig and its instance
Revmerge implementing a tail-recursive merge function (<ref>),
and the tail-recursive mergesort functions are provided as a functor module CBV_ that takes an
instance M of RevmergeSig as a parameter (<ref>).

Fixpoint sort3rec (stack : list (list T)) (xs : list T) struct xs : list T :=
match xs with
| x1 :: x2 :: x3 :: xs =>
let t :=
if leT x1 x2 then
if leT x2 x3 then [:: x1; x2; x3]
else if leT x1 x3 then [:: x1; x3; x2] else [:: x3; x1; x2]
if leT x1 x3 then [:: x2; x1; x3]
else if leT x2 x3 then [:: x2; x3; x1] else [:: x3; x2; x1]
sort3rec (push t stack) xs
| [:: x1; x2] => pop false (if leT x1 x2 then xs else [:: x2; x1]) stack
| _ => pop false xs stack

Definition sort3 : list T -> list T := sort3rec [::].

A structurally-recursive tail-recursive mergesorts in , that takes three elements from
the input at a time. This implementation is omitted in the place marked by [..] in

Fixpoint sortNrec (stack : list (list T)) (x : T) (xs : list T) struct xs :
list T :=
if xs is y :: xs then
if leT x y then incr stack y xs [:: x] else decr stack y xs [:: x]
pop false [:: x] stack
with incr (stack : list (list T)) (x : T) (xs accu : list T) struct xs :
list T :=
if xs is y :: xs then
if leT x y then
incr stack y xs (x :: accu)
sortNrec (push (catrev accu [:: x]) stack) y xs
pop false (catrev accu [:: x]) stack
with decr (stack : list (list T)) (x : T) (xs accu : list T) struct xs :
list T :=
if xs is y :: xs then
if leT x y then
sortNrec (push (x :: accu) stack) y xs
decr stack y xs (x :: accu)
pop false (x :: accu) stack.

Definition sortN (xs : list T) : list T :=
if xs is x :: xs then sortNrec [::] x xs else [::].

A smooth structurally-recursive tail-recursive mergesort in . This implementation is
omitted in the place marked by [..] in <ref>.

The sort2 and sort3 functions in
<ref> take two and three
elements from the input at a time, respectively.
Again, the latter is analogous to the optimization technique employed by List.stable_sort of
The sortN function in <ref> is a smooth
structurally-recursive tail-recursive mergesort, implemented in the same way as the
non-tail-recursive counterpart (<ref>).

We stress that the recursive functions defined and used in
are tail recursive except for push in <ref>, whose depth of
recursive calls is logarithmic in the length of the input.
Therefore, a linear consumption of stack space does not occur in any of the mergesort functions
presented in this section.

§ NON-TAIL-RECURSIVE MERGESORT IS TAIL-RECURSIVE MODULO CONS

In this appendix, we show that non-tail-recursive mergesort can actually be transformed to a
tail-recursive function in destination-passing style <cit.>.

Let us recall that the recursive calls of merge in <ref> appear in
non-tail position and its caller still have to compute one cons cell.
Nevertheless, if in-place update of constructor parameters is allowed, one may write an equivalent
tail-recursive function in destination-passing style.
It can be described as the merge_dps function in <ref> written in
pseudo-syntax borrowed from <cit.>.

The merge_dps function takes a new argument dst which is a cons cell, and writes the
resulting list to the tail of dst instead of returning it.
Focusing on the case that both arguments are not empty and x <= y holds, it first builds a
cons cell dst' (:= x :: Hole) where Hole means an uninitialized field,
updates the 1 field (counting from $0$, hence the tail) of dst with dst' by
dst.1 <- dst', and then calls merge_dps recursively to let it fill the uninitialized
tail of dst'.
The merge function wraps this merge_dps function to provide the same interface as the
non-tail-recursive merge function in <ref>.

let rec merge (<=) xs ys =
match xs, ys with
| [], ys -> ys
| xs, [] -> xs
| x :: xs', y :: ys' ->
if x <= y then
let dst = x :: Hole in
merge_dps dst 1 (<=) xs' ys;
let dst = y :: Hole in
merge_dps dst 1 (<=) xs ys';

and merge_dps dst i (<=) xs ys =
match xs, ys with
| [], ys -> dst.i <- ys
| xs, [] -> dst.i <- xs
| x :: xs', y :: ys' ->
if x <= y then
let dst' = x :: Hole in
dst.i <- dst';
merge_dps dst' 1 (<=) xs' ys
let dst' = y :: Hole in
dst.i <- dst';
merge_dps dst' 1 (<=) xs ys'

The non-tail-recursive merge function (<ref>) turned into a
tail-recursive merge function in destination-passing style by the Tail Modulo Cons (TMC)

In fact, this program transformation, called Tail Modulo Cons (TMC)
transformation <cit.><cit.>, introduced in 4.14, can automatically
turn tail calls modulo constructor <cit.> into tail calls in
destination-passing style.[At most one tail call modulo constructor in one branch can be
turned into a tail call in destination-passing style. The recursive function to be transformed
should be marked by the [@tail_mod_cons] attribute, and it is recommended to mark each tail
call modulo constructor to be transformed by the [@tailcall] attribute.]
For example, all the recursive functions in the naive bottom-up non-tail-recursive mergesort
(<ref>) and structurally-recursive non-tail-recursive mergesorts
(<ref>) are
The technique presented in <ref> allows us to implement a top-down
non-tail-recursive mergesort that is tail-recursive-modulo-cons except for the sort_rec
function, whose depth of recursive calls is logarithmic in the length of the input.
Therefore, this optimization technique works for both top-down and bottom-up non-tail-recursive
mergesort functions.

In <ref>, we show benchmark results indicating that structurally-recursive
non-tail-recursive mergesorts (<ref>) extracted to and then
automatically turned into tail-recursive mergesorts by the TMC transformation are consistently
slower than their tail-recursive counterparts (<ref>).

§ PERFORMANCE EVALUATION

This section evaluates the performance of and code
extracted <cit.> from our implementation of structurally-recursive
non-tail-recursive and tail-recursive mergesort functions (<ref>)
to verify our claims on the performance of mergesort argued in <ref>.
We also compare them with the performance of mergesort functions in the standard libraries, ,
List.stable_sort of and Data.List.sort of .
These benchmarks in and are intended to evaluate the performance of mergesort
functions in call-by-value and call-by-need evaluations, respectively.

The implementations we compare are the “three elements at a time” and smooth variants
(sort3 and sortN) of non-tail-recursive (<ref>) and
tail-recursive (<ref>) mergesorts.
The “one/two elements at a time” variants (sort1 and sort2) are consistently slower
than sort3 in any of our benchmark results, and thus excluded.
In any of these, the merge function is replaced with one using accessibility proofs
(<ref>) to avoid extracting nested recursion.

We evaluate their performance using two kinds of inputs: lists of random integers and those
preprocessed so that every block of length 50 is sorted in ascending order (hereinafter called
partially-sorted input). The latter kind of input is intended to evaluate their smoothness
For , we also evaluated their performance in case of obtaining the first 25% of the output,
to evaluate their laziness and incrementality (<ref>).

<Ref> shows the benchmark results of extracted code, including
non-tail-recursive mergesorts optimized by the TMC transformation (<ref>),
and List.stable_sort.
Besides the facts implied from the figure, non-tail-recursive variants use up stack space but their
TMC counterparts do not.

Regardless of whether the inputs are random or partially-sorted, the non-tail-recursive variants
( and ) are noticeably slower than any other, and their TMC
counterparts ( and ) are 4%–8% slower than their
tail-recursive counterparts ( and ), respectively.
For random inputs (<ref>), any TMC or tail-recursive variant achieve
quite comparable performances with List.stable_sort.
For partially-sorted inputs (<ref>), the smooth variants become faster
as expected.

<Ref> shows the benchmark results of extracted code and
If we compute only the first 25% of the output instead of the entire output
(<ref>), the
non-tail-recursive variants outperform their tail-recursive counterparts, in contrast to .
This observation corresponds to the fact that non-tail-recursive mergesort in call-by-need
evaluation is an optimal incremental sort algorithm (<ref>).

Furthermore, Data.List.sort is even faster than our non-tail-recursive mergesort
particularly for large random inputs (<ref>).
However, we have not identified the clear reason of this performance difference yet.
On the other hand, if we require the entire output
(<ref>), the tail-recursive
variants outperform the non-tail-recursive variants including Data.List.sort.

For partially sorted inputs
(<ref>), the smooth
variants including Data.List.sort become faster as expected.

enlargelimits=0.03, width=, height=7cm,
every axis plot/.append style=mark options=mark size=1.5, line width=0.3pt,
minor tick num=9, scaled y ticks=false,
tick label style=font=,
xlabel=size of input, ylabel=time relative to List.stable_sort (%),
label style=font=,
every axis legend/.append style=at=(1, 1.03), anchor=south east,
legend columns=2, legend cell align=left,
legend style=font=, row sep=-4pt,
cycle list=
densely dashed, mark=*,         every mark/.append style=solid, fill=gray,
densely dotted, mark=*,         every mark/.append style=solid, fill=black,

densely dashed, mark=diamond*,  every mark/.append style=solid, fill=gray,
densely dotted, mark=diamond*,  every mark/.append style=solid, fill=black,

densely dashed, mark=triangle*, every mark/.append style=solid, fill=gray,
densely dotted, mark=triangle*, every mark/.append style=solid, fill=black,
solid,          mark=asterisk,  every mark/.append style=solid

table [x=Size, y expr=100*CBNAcc.sort3/List.stable_sort] benchmark/ocaml-random.time.csv;
table [x=Size, y expr=100*CBNAcc.sortN/List.stable_sort] benchmark/ocaml-random.time.csv;

table [x=Size, y expr=100*CBNAcc.sort3 (TMC)/List.stable_sort] benchmark/ocaml-random.time.csv;
table [x=Size, y expr=100*CBNAcc.sortN (TMC)/List.stable_sort] benchmark/ocaml-random.time.csv;

table [x=Size, y expr=100*CBVAcc.sort3/List.stable_sort] benchmark/ocaml-random.time.csv;
table [x=Size, y expr=100*CBVAcc.sortN/List.stable_sort] benchmark/ocaml-random.time.csv;
table [x=Size, y expr=100*List.stable_sort/List.stable_sort] benchmark/ocaml-random.time.csv;
CBN.sort3, CBN.sortN, CBN.sort3 (TMC), CBN.sortN (TMC), CBV.sort3, CBV.sortN, List.stable_sort

For a random input, sort the entire list.

table [x=Size, y expr=100*CBNAcc.sort3/List.stable_sort] benchmark/ocaml-smooth.time.csv;
table [x=Size, y expr=100*CBNAcc.sortN/List.stable_sort] benchmark/ocaml-smooth.time.csv;

table [x=Size, y expr=100*CBNAcc.sort3 (TMC)/List.stable_sort] benchmark/ocaml-smooth.time.csv;
table [x=Size, y expr=100*CBNAcc.sortN (TMC)/List.stable_sort] benchmark/ocaml-smooth.time.csv;

table [x=Size, y expr=100*CBVAcc.sort3/List.stable_sort] benchmark/ocaml-smooth.time.csv;
table [x=Size, y expr=100*CBVAcc.sortN/List.stable_sort] benchmark/ocaml-smooth.time.csv;
table [x=Size, y expr=100*List.stable_sort/List.stable_sort] benchmark/ocaml-smooth.time.csv;
CBN.sort3, CBN.sortN, CBN.sort3 (TMC), CBN.sortN (TMC), CBV.sort3, CBV.sortN, List.stable_sort

For a input consisting of sorted blocks of length 50, sort the entire list.

Benchmark results of sorting in .

The program was compiled by 4.14.0 with an optimization flag  for the
Flambda <cit.> optimizer, and ran with  to avoid
stack overflow.
To avoid performing garbage collections during a measurement, the minor heap was enlarged
beforehand, and a full major garbage collection and a heap compaction (Gc.compact) were
invoked before each measurement.

enlargelimits=0.03, width=, height=7cm,
every axis plot/.append style=mark options=mark size=1.5, line width=0.3pt,
minor tick num=9, scaled y ticks=false,
tick label style=font=,
xlabel=size of input, ylabel=time relative to Data.List.sort (%),
label style=font=,
every axis legend/.append style=at=(.5, 1.03), anchor=south,
legend columns=2, legend cell align=left,
legend style=font=, row sep=-4pt,
cycle list=
densely dashed, mark=*,         every mark/.append style=solid, fill=gray,
densely dotted, mark=*,         every mark/.append style=solid, fill=black,

densely dashed, mark=triangle*, every mark/.append style=solid, fill=gray,
densely dotted, mark=triangle*, every mark/.append style=solid, fill=black,
solid,          mark=asterisk,  every mark/.append style=solid

table [x=Size, y expr=100*CBNAcc.sort3/Data.List.sort] benchmark/haskell-partial-random.time.csv;
table [x=Size, y expr=100*CBNAcc.sortN/Data.List.sort] benchmark/haskell-partial-random.time.csv;

table [x=Size, y expr=100*CBVAcc.sort3/Data.List.sort] benchmark/haskell-partial-random.time.csv;
table [x=Size, y expr=100*CBVAcc.sortN/Data.List.sort] benchmark/haskell-partial-random.time.csv;
table [x=Size, y expr=100*Data.List.sort/Data.List.sort] benchmark/haskell-partial-random.time.csv;
CBN.sort3, CBN.sortN, CBV.sort3, CBV.sortN, Data.List.sort

For a random input, compute the first 25% of the output.

table [x=Size, y expr=100*CBNAcc.sort3/Data.List.sort] benchmark/haskell-partial-smooth.time.csv;
table [x=Size, y expr=100*CBNAcc.sortN/Data.List.sort] benchmark/haskell-partial-smooth.time.csv;

table [x=Size, y expr=100*CBVAcc.sort3/Data.List.sort] benchmark/haskell-partial-smooth.time.csv;
table [x=Size, y expr=100*CBVAcc.sortN/Data.List.sort] benchmark/haskell-partial-smooth.time.csv;
table [x=Size, y expr=100*Data.List.sort/Data.List.sort] benchmark/haskell-partial-smooth.time.csv;
CBN.sort3, CBN.sortN, CBV.sort3, CBV.sortN, Data.List.sort

For a input consisting of sorted blocks of length 50, compute the first 25% of the

table [x=Size, y expr=100*CBNAcc.sort3/Data.List.sort] benchmark/haskell-total-random.time.csv;
table [x=Size, y expr=100*CBNAcc.sortN/Data.List.sort] benchmark/haskell-total-random.time.csv;

table [x=Size, y expr=100*CBVAcc.sort3/Data.List.sort] benchmark/haskell-total-random.time.csv;
table [x=Size, y expr=100*CBVAcc.sortN/Data.List.sort] benchmark/haskell-total-random.time.csv;
table [x=Size, y expr=100*Data.List.sort/Data.List.sort] benchmark/haskell-total-random.time.csv;
CBN.sort3, CBN.sortN, CBV.sort3, CBV.sortN, Data.List.sort

For a random input, sort the entire list.

table [x=Size, y expr=100*CBNAcc.sort3/Data.List.sort] benchmark/haskell-total-smooth.time.csv;
table [x=Size, y expr=100*CBNAcc.sortN/Data.List.sort] benchmark/haskell-total-smooth.time.csv;

table [x=Size, y expr=100*CBVAcc.sort3/Data.List.sort] benchmark/haskell-total-smooth.time.csv;
table [x=Size, y expr=100*CBVAcc.sortN/Data.List.sort] benchmark/haskell-total-smooth.time.csv;
table [x=Size, y expr=100*Data.List.sort/Data.List.sort] benchmark/haskell-total-smooth.time.csv;
CBN.sort3, CBN.sortN, CBV.sort3, CBV.sortN, Data.List.sort

For a input consisting of sorted blocks of length 50, sort the entire list.

Benchmark results of sorting in .

The program was compiled by GHC 8.10.7 with an optimization flag .
To avoid performing garbage collections during a measurement, the allocation area was enlarged
beforehand, and a major garbage collection (System.Mem.performMajorGC) was invoked
before each measurement.