The Coq mailing list

["Yevgeniy Makarov" <emakarov AT gmail.com>]

Hello,

I followed Benjamin's hint, and here's my version of merge on lists of
natural numbers:

Require Import List.
Require Import Compare_dec.

Fixpoint merge (l1 : list nat) : list nat -> list nat :=
fix merge_helper (l2 : list nat) :=
match l1, l2 with
| nil, nil => nil
| nil, l => l
| l, nil => l
| x1 :: l1, x2 :: l2 =>
  if leb x1 x2
  then x1 :: merge l1 (x2 :: l2)
  else x2 :: merge_helper l2
end.

However, structural recursion won't work for the mergesort itself,
where one has to recur on halfs of the list, and there Function would
be handy.

Concerning Pierre Castéran's page for mergesort, it looks a little
strange since the traditional presentation of the algorithm does not
mention trees...

Evgeny