The Coq mailing list

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

Dear Suneel,

Assuming you can work with the conditions listed below

where I do not write implicit universal quantification on

x, y, z, l, m,

R : X -> X -> Prop is an order:

reflexive : R x x

antisymmetric : R x y -> R y x -> x = y  

transitive : R x y -> R y z -> R x z

Notice that antisymmetry is dropped for *pre-orders* but

is *included* in the definition of an order in the usual terminology.

Moreover we assume that R is total (or linear):

total: R x y \/ R y x

Then one can show (and I invite you to do it because

it is enriching to do such proofs by yourself):

sorted R l -> sorted R m -> Permutation l m -> l = m

To *compute* the sorting of a list, you actually

need moreover:

decR : { R x y } + { ~ R x y }

or something similar.

Then since sort decR l satisfies both

1) sorted (sort decR l)

2) Permutation l (sort decR l)

which is the functional spec of any sorting algo

on lists,

you automatically get l = sort decR l when sorted R l holds

This result holds for ANY sorting algorithm under the

conditions above described, not just merge sort.

But this is not the same thing as the stability property

that X. Leroy was mentioning in his messages, which

is especially relevant when R is only a pre-order, like

in the example he gives on pairs where the right component

does not count in the comparison.

Best

Dominique

---

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

Thanks Dominique,

I still need to prove it? Is there any lemma that just allows me to rewrite (sort L) with L if L is Sorted?

Thanks,

Suneel

On Tue, Jan 30, 2024 at 7:15 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.

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