The Coq mailing list

[Xavier Leroy <xavier.leroy AT college-de-france.fr>]

On Tue, Jan 30, 2024 at 3:24 PM Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr> wrote:

Indeed, as Xavier remarks, I forgot to say that the order should

be a *total* order ie "any two elements are always comparable".

That is not enough.  The example I gave (pairs of integers compared by their first elements) is a total order (any two pairs are either <= or >=) yet is not antisymmetric (two pairs can be both <= and >= yet not Leibniz-equal).

If the order is partial like eg the flat order (equality,

which is antisymmetric btw) then of course the stated

result does not hold.

Concerning the stability property of MergeSort, doesn't it depend on

the way you split the pre-ordered list?

Would it work with a split like:

let split =

  let rec loop a b = function

  | [] -> (rev a,rev b)

  | x::l -> loop b (x::a) l

  in loop [] []

The original merge sort algorithm works on arrays, and performs no such reversal of sub-arrays; that's why it's stable.

For a merge sort working over immutable lists, it's better to avoid  the recursive splitting altogether and just start with a list of singleton lists, then repeatedly merge pairs of adjacent lists into a bigger list.  That's stable too.

- Xavier Leroy

Dominique

---

De: "xavier leroy" <xavier.leroy AT college-de-france.fr>
À: "coq-club" <coq-club AT inria.fr>
Envoyé: Mardi 30 Janvier 2024 15:04:35
Objet: Re: [Coq-Club] Merge Sort: Sorted L -> L = sort dec L?

On Tue, Jan 30, 2024 at 2:44 PM Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr> wrote:

Dear Suneel,

The spec of MergeSort should be enough:

if two lists are sorted and *permutable*, then they are equal.

Only if the ordering used is antisymmetric.  If you sort pairs of integers on their first components, for example,

[ (0, 10) ; (0, 5) ; (1, 1) ]

and

[ (0, 5) ; (0, 10) ; (1, 1) ]

are both sorted, and are permutable, but are not equal.

The property Suneel wants to prove is probably true for all orders, but only because merge sort is stable, i.e. preserves the relative ordering of list elements that compare as equal.

Stability of merge sort is not proved in the Coq standard library as far as I can tell, but here is a proof for a different implementation of merge sort: https://xavierleroy.org/coq/Mergesort.html

- Xavier Leroy

Best,

Dominique

---

De: "Suneel Sarswat" <suneel.sarswat AT gmail.com>
À: "coq-club" <coq-club AT inria.fr>
Envoyé: Mardi 30 Janvier 2024 14:08:27
Objet: [Coq-Club] Merge Sort: Sorted L -> L = sort dec L?

Dear Members,

I have list L of unique records type.

I have defined ordertype "dec" on these records. I am using MergeSort module from standard library. Now I need to prove a basic result on this list. Any help would be appreciated.

Lemma sort_sorted L:

Sorted dec L -> L = sort dec L.

Thanks,

Suneel