The Coq mailing list

[Georges Gonthier <gonthier AT microsoft.com>]

> http://coq.inria.fr/V8.2/doc/html/stdlib/Coq.Sorting.Sorting.html

> This library provides a merge function over two sorted lists, but
> there is still some work to do to implement mergesort.  See:

> http://gallium.inria.fr/~xleroy/coq/Mergesort.html
> http://gallium.inria.fr/~xleroy/coq/Mergesort.v

> It's a nice exercise in using "Program".

  It's also possible to manage without Program; e.g., the ssreflect library 
uses the code below (replace seq by list and expand list notations to 
interface with the Coq standard library) -- enjoy.

  - Georges Gonthier

Fixpoint merge_sort_push (s1 : seq T) (ss : seq (seq T)) {struct ss} :=
  match ss with
  | nil :: ss' | nil as ss' => s1 :: ss'
  | s2 :: ss' => nil :: merge_sort_push (merge s1 s2) ss'
  end.

Fixpoint merge_sort_pop (s1 : seq T) (ss : seq (seq T)) {struct ss} :=
  if ss is s2 :: ss' then merge_sort_pop (merge s1 s2) ss' else s1.

Fixpoint merge_sort_rec (ss : seq (seq T)) (s : seq T) {struct s} :=
  if s is [:: x1, x2 & s'] then
    let s1 := if leT x1 x2 then [:: x1; x2] else [:: x2; x1] in
    merge_sort_rec (merge_sort_push s1 ss) s'
  else merge_sort_pop s ss.

Definition sort := merge_sort_rec [::].