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  [ + [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

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

Library Coq.Sorting.Mergesort

Navigation