The Coq mailing list

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

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