coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Sorting

From: Taral <taralx AT gmail.com>
To: dimitrisg7 <dvekris AT hotmail.com>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Sorting
Date: Fri, 10 Apr 2009 17:39:28 -0700
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; b=rYP+FWFwGiaPx7MVJtdM8phWdiz2mpqgI5GxVUFnBaTjR4wWCnbGF+IZ7CVoIKEYs4 4u4l/FPTsWEfcyDImZ3X6eh1qB4tqK5sF52F3nzEX6SLw2xfoU2N8DJVu1HIB0EvYoSB 7PMVh16OF9VMwXcUXCw3Q9fnUqSpdsZaEwDvM=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Fri, Apr 10, 2009 at 8:19 AM, dimitrisg7
<dvekris AT hotmail.com>
wrote:
> The problem is that I have a list of integers (given unsorted unfortunately
> in my proof) and I want to sort them in ascending order, which means I want
> to construct the object (Sorted: sort le l), where l is a list of nat. Is
> that possible or am I complicating things?

Sure it's possible. Pick a sort algorithm. Given the structure of
List, you probably want merge sort. Oh, will you look at that! It's
been done!

http://coq.inria.fr/V8.2/doc/html/stdlib/Coq.Sorting.Sorting.html

;-)

--
Taral
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
-- Unknown

[Coq-Club] Sorting, dimitrisg7
- Re: [Coq-Club] Sorting, Taral
  - Re: [Coq-Club] Sorting, Xavier Leroy
    - Re: [Coq-Club] Sorting, Adam Koprowski
    - RE: [Coq-Club] Sorting, Georges Gonthier