coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Merge Sort: Sorted L -> L = sort dec L?

From: Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Merge Sort: Sorted L -> L = sort dec L?
Date: Tue, 30 Jan 2024 14:44:42 +0100 (CET)
Authentication-results: mail2-relais-roc.national.inria.fr; dkim=none (message not signed) header.i=none; spf=Pass smtp.mailfrom=dominique.larchey-wendling AT loria.fr; spf=None smtp.helo=postmaster AT zcs-store7.inria.fr

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

[Coq-Club] Merge Sort: Sorted L -> L = sort dec L?, Suneel Sarswat, 01/30/2024
- Re: [Coq-Club] Merge Sort: Sorted L -> L = sort dec L?, Kazuhiko Sakaguchi, 01/30/2024
  - Re: [Coq-Club] Merge Sort: Sorted L -> L = sort dec L?, Suneel Sarswat, 01/30/2024
- Re: [Coq-Club] Merge Sort: Sorted L -> L = sort dec L?, Dominique Larchey-Wendling, 01/30/2024
  - Re: [Coq-Club] Merge Sort: Sorted L -> L = sort dec L?, Xavier Leroy, 01/30/2024
    - Re: [Coq-Club] Merge Sort: Sorted L -> L = sort dec L?, Dominique Larchey-Wendling, 01/30/2024
      - Re: [Coq-Club] Merge Sort: Sorted L -> L = sort dec L?, Xavier Leroy, 01/30/2024
  - Re: [Coq-Club] Merge Sort: Sorted L -> L = sort dec L?, Suneel Sarswat, 01/30/2024
    - Re: [Coq-Club] Merge Sort: Sorted L -> L = sort dec L?, Dominique Larchey-Wendling, 01/30/2024