The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

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

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

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

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