Sorting algorithms

Stream: Is there code for X?

[Scott Morrison]

Any sorting algorithms out there that I can use, and reason about with rfl? No particular performance requirements, I just need to be able to run it. :-)

Unfortunately Array.qsort isn't what I need:

#eval #[3, 2, 1].qsort (· < ·)    -- works fine: #[1, 2, 3]
example : #[3, 2, 1].qsort (· < ·) = #[1, 2, 3] := rfl    -- fails with type mismatch

[Jun Yoshida]

docs#Array.heapSort for example?

[Scott Morrison]

Indeed,

import Mathlib.Data.BinaryHeap

example : #[3, 2, 1].heapSort (· < ·) = #[1, 2, 3] := rfl

works.

I would need to move this out of Mathlib, but that looks feasible.

[Mario Carneiro]

Isn't there an insertionSort in core?

[Mario Carneiro]

Incidentally I have a qsort implementation which eliminates the partial, but I didn't PR it at the time because I didn't want to do the... stuff I would need to do to get it approved

[Scott Morrison]

#8143 removes the Mathlib imports from Mathlib.Data.BinaryHeap, just in case we decide we want that too.

[Scott Morrison]

Hmm... my sorting requirements are trivial right now, so I don't want to be the one to say yes. :-) But good to know it is there!