The Coq mailing list

[Suneel Sarswat <suneel.sarswat AT gmail.com>]

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