Merging sorted lists

A good algorithm to sort lists is the merging algorithm that relies en merging sublists that are already sorted. The structure of this algorithm can be summarized by the following two equations (in both cases one supposes that a is smaller than b):

merge (a :: l) (b :: l') = a :: merge l (b :: l')
merge (b :: l) (a :: l') = a :: merge (b :: l) l'

This function is not structural recursive with respect to the the first list (because of the second equation) or with respect to the second list (because of the first equation), but the sum of length of lists decreases at each recursive call. Use this remark to build an algorithm that sorts lists of elements of type A, working in a functor taking a module with the following type as argument.

Module Type Comparable_data.
Parameter A : Set.
Parameter Ale : A -> A -> Prop.
Parameter Ale_dec : forall x y:A, {Ale x y}+{Ale y x}
End Comparable_data.

Solution

Look at this file.

Additional Exercise