# 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

Open Scope bool_scope.

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  [ + ]             [2;3;1;5]
-> iter_merge            []                [2;3;1;5]
=  append_list_to_stack  [ + ]          [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]; + ]       [1;5]
-> merge_list            [[2;6];]          [1;5]
=  append_list_to_stack  [[2;6]; +      
=  append_list_to_stack  [[2;6] + [1;3];]     
=  append_list_to_stack  [ + [1;2;3;6];;]     
-> merge_list            [[1;2;3;6];;]        
=  append_list_to_stack  [[1;2;3;6];; + ]  []
-> merge_stack           [[1;2;3;6];;]
=                                             [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

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].