Array (and Vector) sorting API

Stream: lean4

[Wrenna Robson]

There are various sort functions on Array: Array.qsort, Array.insertionSort, Array.heapSort, plus some merging functions but no sorts as such.

What I can't find is any API for these - in particular, any assertion that these do actually sort an array or indeed all produce the same function. We also don't I think have any sorting capability for Vector, despite it really being a natural thing to define because sorting doesn't change the size of an Array.

Am I wrong about this? Could this be added? What actually needs to be added?

[Henrik Böving]

The verification of Array.qsort is being delayed on purpose as it needs to be refactored to a proper qsort implementation that is more robust. Array.insertionSort is more of a meta programming gadget though I guess it might be interesting to verify it. I can't speak on heapSort.

[Wrenna Robson]

Meta-programming in the sense that it is not efficient so it isn't good for actual implementations?

[Aaron Liu]

Metaprogramming as in there are times in the metaprogramming where you have to sort an almost sorted list

[Aaron Liu]

so it's used for that

[Wrenna Robson]

Right

[Aaron Liu]

I forgot where is used though

[Ruben Van de Velde]

I'm not sure that counts as "specific for metaprogramming" rather than "specific for programming"

[Aaron Liu]

Well I guess also in programming you have to sort lists

[Ruben Van de Velde]

That's what most of my algorithms class claimed, yes :)

[Wrenna Robson]

It would at least be good to have some kind of predicate for "this array is sorted" or "these two arrays are the same but permuted" - like List.Sorted or List.Perm.

[Wrenna Robson]

Ah in fact Array.Perm exists.

[Wrenna Robson]

But is somewhat undersupported because it's just a wrapper around List.Perm.

[Wrenna Robson]

There is no Array.isPermthough (which would be good).

[Shreyas Srinivas]

I started a repo for collecting efficient sorting algorithms in lean. Progress is slow since I only work on this repo twice a month. But PRs are always welcome : https://github.com/Shreyas4991/Sorting-in-Lean

[Shreyas Srinivas]

Henrik Böving said:

The verification of Array.qsort is being delayed on purpose as it needs to be refactored to a proper qsort implementation that is more robust. Array.insertionSort is more of a meta programming gadget though I guess it might be interesting to verify it. I can't speak on heapSort.

insertion sort has some interesting uses. It's basically as good as it gets for streams, and it is a useful primitive for sorting small subarrays.

[Henrik Böving]

Shreyas Srinivas said:

I started a repo for collecting efficient sorting algorithms in lean. Progress is slow since I only work on this repo twice a month. But PRs are always welcome : https://github.com/Shreyas4991/Sorting-in-Lean

AFAICT there is no code in there at all?

[Shreyas Srinivas]

Takes time to lit search

[Shreyas Srinivas]

I only started this last month 3 weeks ago.

[Wrenna Robson]

I would quite like Batcher's odd-even sorting network.

[Wrenna Robson]

But in general I wanted this because if an array as represents a permutation p (i.e. as[i] = p i), then if you sort the array whose ith element is (as[i], i) with the lexographic order, the resulting array has ith element (i, p.symm i).

[Wrenna Robson]

Which is a useful way of applying the inverse of a permutation stored as an array while avoiding conditional memory lookups, if you use a sorting network.