feat: rm partial / bounds checks in Array.qsort

[digama0]

With omega in core, it is now more feasible to perform the necessary proofs to eliminate the partial from Array.qsort, as well as the many uses of Array.get! and Array.swap!. (This is also a perfect example of the kind of code that would benefit from the proposed Vector API.)

I wrote this code over a year ago, but the stance regarding proofs in lean core has shifted so I think this is now more likely to be accepted. This is in any case blocking some proofs in Std which are built on top of uses of Array.qsort.

[digama0]

!bench

[leanprover-bot]

Here are the benchmark results for commit 228efff.
The entire run failed.
Found no significant differences.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 88ee503f02e047c8c3fd1eb3ac8310b123380038 --onto d3e004932c1f5ac3946850692940512d381c7634. (2024-04-17 12:10:44)
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 036b5381f0f1a193f1734ca9ffb608f09c7b7f0b --onto d3e004932c1f5ac3946850692940512d381c7634. (2024-04-17 20:12:37)
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 036b5381f0f1a193f1734ca9ffb608f09c7b7f0b --onto 62cdb51ed5b9d8487877d5a4adbcd4659d81fc6a. (2024-04-24 06:24:17)

[digama0]

!bench

[leanprover-bot]

Here are the benchmark results for commit 28c305a.
There were significant changes against commit 036b538:

  Benchmark   Metric          Change
  ============================================
- stdlib      instructions      2.0% (371.8 σ)
- stdlib      task-clock        1.3%  (11.5 σ)
- stdlib      type checking     9.0%  (11.0 σ)
- stdlib      wall-clock        8.0%  (86.5 σ)

[hargoniX]

Do you know why this gets the stdlib benchmark slower by a clearly significant margin? This seems rather counter intuitive to me. Are the proofs in Array.qsort taking so long?

[collares]

Not necessarily relevant for this PR, but one simple improvement to quicksort (as explained in the Sedgewick paper) is to recurse on the smallest subproblem first. This ensures a stack depth of O(log n) because the other call will be in tail position.

[digama0]

The proof is actually suspiciously slow (the definition of qpartition is about 2 seconds). I think it might actually be the compiler too; this code contains three if statements at the beginning and an @[inline] and this seems to hit a relatively bad case for the compiler (there were other variations of this code that behaved even worse). The generated code itself seems to be fine though.

This code is slightly suboptimal, in that n is passed as an argument to qpartition even though it is redundant, and likewise lo and hi are passed unnecessarily to qpartition.loop. My original version of this code used some tricks to eliminate this, at the cost of making the proof (and code) significantly more obtuse; I decided that this was not a good tradeoff for maintenance reasons and submitted the simpler version here. Ideally, this would be solved by marking these parameters as "ghost" / not computationally relevant.

[digama0]

!bench

[digama0]

(The version that was previously benched had a sharing bug. Unsure if that is related to the stdlib slowdown.)

[leanprover-bot]

Here are the benchmark results for commit 824a7fe.
There were significant changes against commit 036b538:

  Benchmark   Metric          Change
  ===========================================
- stdlib      type checking     4.6% (17.2 σ)
- stdlib      wall-clock        3.8% (23.5 σ)

[Kha]

Marking draft pending further benchmarking (build time and run time)

[kim-em]

Oh, sorry, I missed this, and did it independently. (Additionally, using Vector to clean up a bit.)

I also have most of proof that the result is sorted, on a branch.