The Coq Proof Assistant

# Library Coq.Sorting.Mergesort

A modular implementation of mergesort (the complexity is O(n.log n) in the length of the list)
Require Import List Setoid Permutation Sorted Orders.
Notations and conventions
Local Notation "[ ]" := nil.
Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..).
Open Scope bool_scope.
Local Coercion is_true : bool >-> Sortclass.
The main module defining mergesort on a given boolean order <=?. We require minimal hypotheses : this boolean order should only be total: forall x y, (x<=?y) \/ (y<=?x). Transitivity is not mandatory, but without it one can only prove LocallySorted and not StronglySorted.
Module Sort (Import X:Orders.TotalLeBool').
Fixpoint merge l1 l2 :=
let fix merge_aux l2 :=
match l1, l2 with
| [], _ => l2
| _, [] => l1
| a1::l1', a2::l2' =>
if a1 <=? a2 then a1 :: merge l1' l2 else a2 :: merge_aux l2'
end
in merge_aux l2.
We implement mergesort using an explicit stack of pending mergings. Pending merging are represented like a binary number where digits are either None (denoting 0) or Some list to merge (denoting 1). The n-th digit represents the pending list to be merged at level n, if any. Merging a list to a stack is like adding 1 to the binary number represented by the stack but the carry is propagated by merging the lists. In practice, when used in mergesort, the n-th digit, if non 0, carries a list of length 2^n. For instance, adding singleton list 3 to the stack Some 4::Some 2;6::None::Some 1;3;5;5 reduces to propagate the carry 3;4 (resulting of the merge of 3 and 4) to the list Some 2;6::None::Some 1;3;5;5, which reduces to propagating the carry 2;3;4;6 (resulting of the merge of 3;4 and 2;6) to the list None::Some 1;3;5;5, which locally produces Some 2;3;4;6::Some 1;3;5;5, i.e. which produces the final result None::None::Some 2;3;4;6::Some 1;3;5;5.
For instance, here is how 6;2;3;1;5 is sorted:

           operation             stack                list
           iter_merge            []                   [6;2;3;1;5]
        =  append_list_to_stack  [ + [6]]             [2;3;1;5]
        -> iter_merge            [[6]]                [2;3;1;5]
        =  append_list_to_stack  [[6] + [2]]          [3;1;5]
        =  append_list_to_stack  [ + [2;6];]          [3;1;5]
        -> iter_merge            [[2;6];]             [3;1;5]
        =  append_list_to_stack  [[2;6]; + [3]]       [1;5]
        -> merge_list            [[2;6];[3]]          [1;5]
        =  append_list_to_stack  [[2;6];[3] + [1]     [5]
        =  append_list_to_stack  [[2;6] + [1;3];]     [5]
        =  append_list_to_stack  [ + [1;2;3;6];;]     [5]
        -> merge_list            [[1;2;3;6];;]        [5]
        =  append_list_to_stack  [[1;2;3;6];; + [5]]  []
        -> merge_stack           [[1;2;3;6];;[5]]
        =                                             [1;2;3;5;6]

The complexity of the algorithm is n*log n, since there are 2^(p-1) mergings to do of length 2, 2^(p-2) of length 4, ..., 2^0 of length 2^p for a list of length 2^p. The algorithm does not need explicitly cutting the list in 2 parts at each step since it the successive accumulation of fragments on the stack which ensures that lists are merged on a dichotomic basis.
Fixpoint merge_list_to_stack stack l :=
match stack with
| [] => [Some l]
| None :: stack' => Some l :: stack'
| Some l' :: stack' => None :: merge_list_to_stack stack' (merge l' l)
end.
Fixpoint merge_stack stack :=
match stack with
| [] => []
| None :: stack' => merge_stack stack'
| Some l :: stack' => merge l (merge_stack stack')
end.
Fixpoint iter_merge stack l :=
match l with
| [] => merge_stack stack
| a::l' => iter_merge (merge_list_to_stack stack [a]) l'
end.
Definition sort := iter_merge [].
The proof of correctness
Local Notation Sorted := (LocallySorted leb) (only parsing).
Fixpoint SortedStack stack :=
match stack with
| [] => True
| None :: stack' => SortedStack stack'
| Some l :: stack' => Sorted l /\ SortedStack stack'
end.
Local Ltac invert H := inversion H; subst; clear H.
Fixpoint flatten_stack (stack : list (option (list t))) :=
match stack with
| [] => []
| None :: stack' => flatten_stack stack'
| Some l :: stack' => l ++ flatten_stack stack'
end.
Theorem Sorted_merge : forall l1 l2,
Sorted l1 -> Sorted l2 -> Sorted (merge l1 l2).
Theorem Permuted_merge : forall l1 l2, Permutation (l1++l2) (merge l1 l2).
Theorem Sorted_merge_list_to_stack : forall stack l,
SortedStack stack -> Sorted l -> SortedStack (merge_list_to_stack stack l).
Theorem Permuted_merge_list_to_stack : forall stack l,
Permutation (l ++ flatten_stack stack) (flatten_stack (merge_list_to_stack stack l)).
Theorem Sorted_merge_stack : forall stack,
SortedStack stack -> Sorted (merge_stack stack).
Theorem Permuted_merge_stack : forall stack,
Permutation (flatten_stack stack) (merge_stack stack).
Theorem Sorted_iter_merge : forall stack l,
SortedStack stack -> Sorted (iter_merge stack l).
Theorem Permuted_iter_merge : forall l stack,
Permutation (flatten_stack stack ++ l) (iter_merge stack l).
Theorem LocallySorted_sort : forall l, Sorted (sort l).
Corollary Sorted_sort : forall l, Sorted.Sorted leb (sort l).
Theorem Permuted_sort : forall l, Permutation l (sort l).
Corollary StronglySorted_sort : forall l,
Transitive leb -> StronglySorted leb (sort l).
End Sort.
An example
Module NatOrder <: TotalLeBool.
Definition t := nat.
Fixpoint leb x y :=
match x, y with
| 0, _ => true
| _, 0 => false
| S x', S y' => leb x' y'
end.
Infix "<=?" := leb (at level 70, no associativity).
Theorem leb_total : forall a1 a2, a1 <=? a2 \/ a2 <=? a1.
End NatOrder.
Module Import NatSort := Sort NatOrder.
Example SimpleMergeExample := Eval compute in sort [5;3;6;1;8;6;0].