perf: add three-way partitioning to Array.qsort

[kim-em]

This PR makes Array.qsort efficiently handle inputs with repeated values by grouping pivot-equal elements and excluding them from recursive calls.

The partitioner retains the low-overhead scan for distinct inputs and switches to a three-way partition once it encounters an element equal to the pivot. This fixes the quadratic behavior reported in #8087 without regressing the existing random-input benchmark. qsortOrd now passes its three-way comparison directly, while the Boolean-comparator API is adapted internally.

It adds a regression test for repeated values and a Radar benchmark covering constant and low-cardinality arrays. The suggestion snapshots change because unstable sorting may now choose a different order among equal elements. The obsolete implementation-coupled proof test is removed; stacked follow-up #14658 replaces it with stronger proofs in the library.

Previous attempts and related groundwork:

• #5346 attempted a replacement quicksort together with bounds and correctness proofs.
• #7995 added the current grind-based verification to the test suite; #12510 later attempted to complete those proofs.
• #14033 directly attempted to fix Array.qsort has quadratic runtime on constant arrays #8087, but its Radar runs showed a roughly 39% instruction regression in compiled/io_compute.
• #13409 established comparator specialization and the current io_compute performance baseline.
• The Zulip discussion on moving the verification into the library records why the proofs remained in the test suite pending an implementation change.

🤖 prepared with assistance from codex and claude

[kim-em]

!radar

[leanprover-radar]

Benchmark results for 8208e78 against e51752c are in. There are significant results. @kim-em

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

• Bench repo commit hashes for run build differ between commits.
• Bench repo commit hashes for run other differ between commits.

• 🟥 build//instructions: +20.3G (+0.17%)

Large changes (2✅)

• ✅ compiled/io_compute//instructions: -626.8M (-5.69%)
• ✅ vcgen/GetThrowSet/200/kernel//wall-clock: -11ms (-17.19%)

Medium changes (3🟥)

• 🟥 size/Init/.olean.private//bytes: +1MiB (+0.44%)
• 🟥 size/compile/.out//bytes: +14MiB (+0.50%)
• 🟥 size/libleanshared.so//bytes: +905kiB (+0.40%)

Small changes (3✅, 86🟥)

• 🟥 build/module/Init.Data.Array.QSort.Basic//instructions: +10.3G (+95.91%) (reduced significance based on *//lines)
• 🟥 build/module/Lake.CLI.BuiltinLint//instructions: +93.4M (+1.78%)
• 🟥 build/module/Lake.CLI.Shake//instructions: +49.8M (+0.40%)
• 🟥 build/module/Lean.Attributes//instructions: +98.8M (+1.89%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Compiler.IR.CompilerM//instructions: +54.5M (+2.47%)
• 🟥 build/module/Lean.Compiler.LCNF.AlphaEqv//instructions: +55.5M (+1.44%)
• 🟥 build/module/Lean.Compiler.LCNF.ElimDeadBranches//instructions: +103.2M (+1.23%)
• 🟥 build/module/Lean.Compiler.LCNF.EmitC//instructions: +62.6M (+0.30%)
• 🟥 build/module/Lean.Compiler.LCNF.ExplicitRC//instructions: +45.2M (+0.59%)
• 🟥 build/module/Lean.Compiler.LCNF.PhaseExt//instructions: +51.7M (+1.95%)
• 🟥 build/module/Lean.Compiler.LCNF.SpecInfo//instructions: +43.1M (+1.61%)
• 🟥 build/module/Lean.Compiler.MetaAttr//instructions: +34.3M (+3.52%)
• 🟥 build/module/Lean.Compiler.Specialize//instructions: +40.4M (+2.33%)
• 🟥 build/module/Lean.CoreM//instructions: +60.3M (+0.80%)
• ✅ build/module/Lean.Data.Lsp//instructions: -9.4M (-1.28%)
• 🟥 build/module/Lean.Elab.AssertExists//instructions: +53.4M (+2.08%)
• 🟥 build/module/Lean.Elab.Command//instructions: +69.9M (+0.35%)
• 🟥 build/module/Lean.Elab.DeclUtil//instructions: +36.5M (+2.48%)
• 🟥 build/module/Lean.Elab.DocString.Builtin.Keywords//instructions: +52.2M (+0.34%)
• 🟥 build/module/Lean.Elab.DocString.Builtin//instructions: +185.1M (+0.45%)
• and 68 more
• and 1 hidden

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e51752cf2f9a8b305e67ea90c5aa631b210056ce --onto 5b8d06c1764fa367a1e27b3e89f64667eac425af. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-02 06:46:48)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase e51752cf2f9a8b305e67ea90c5aa631b210056ce --onto 23393b959b33e3a8d15796b2397f8a04c315b9f4. You can force reference manual CI using the force-manual-ci label. (2026-08-02 06:46:50)

[kim-em]

!radar

[leanprover-radar]

Benchmark results for 7a8781f against e51752c are in. There are significant results. @kim-em

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

• Bench repo commit hashes for run build differ between commits.
• Bench repo commit hashes for run other differ between commits.

• 🟥 build//instructions: +14.9G (+0.13%)

Large changes (2✅)

• ✅ compiled/io_compute//instructions: -626.6M (-5.69%)
• ✅ vcgen/GetThrowSet/200/kernel//wall-clock: -10ms (-15.63%)

Medium changes (2🟥)

• 🟥 size/compile/.out//bytes: +11MiB (+0.42%)
• 🟥 vcgen/MatchIota/1000/vcgen//wall-clock: +17ms (+14.66%)

Small changes (1✅, 75🟥)

• 🟥 build/module/Init.Data.Array.QSort.Basic//instructions: +6.5G (+60.75%) (reduced significance based on *//lines)
• 🟥 build/module/Lake.CLI.BuiltinLint//instructions: +74.7M (+1.42%)
• 🟥 build/module/Lean.Attributes//instructions: +81.2M (+1.56%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Compiler.IR.CompilerM//instructions: +44.1M (+2.00%)
• 🟥 build/module/Lean.Compiler.LCNF.AlphaEqv//instructions: +46.9M (+1.22%)
• 🟥 build/module/Lean.Compiler.LCNF.ElimDeadBranches//instructions: +88.9M (+1.06%)
• 🟥 build/module/Lean.Compiler.LCNF.PhaseExt//instructions: +38.6M (+1.46%)
• 🟥 build/module/Lean.Compiler.LCNF.SpecInfo//instructions: +33.4M (+1.25%)
• 🟥 build/module/Lean.Compiler.MetaAttr//instructions: +26.9M (+2.76%)
• 🟥 build/module/Lean.Compiler.Specialize//instructions: +34.7M (+2.00%)
• 🟥 build/module/Lean.CoreM//instructions: +50.9M (+0.67%)
• ✅ build/module/Lean.Data.Lsp//instructions: -10.1M (-1.37%)
• 🟥 build/module/Lean.Elab.DeclUtil//instructions: +30.1M (+2.05%)
• 🟥 build/module/Lean.Elab.DocString.Builtin//instructions: +135.2M (+0.33%)
• 🟥 build/module/Lean.Elab.DocString//instructions: +92.9M (+0.22%)
• 🟥 build/module/Lean.Elab.PreDefinition.Structural.Main//instructions: +42.2M (+0.98%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Elab.Tactic.Conv.Pattern//instructions: +75.9M (+2.47%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Elab.Tactic.Decide//instructions: +33.9M (+0.81%)
• 🟥 build/module/Lean.Elab.Tactic.Do.Spec//instructions: +51.7M (+0.66%)
• 🟥 build/module/Lean.Elab.Tactic.Doc//instructions: +74.0M (+1.85%)
• and 56 more

[cursor]

Bugbot is not enabled for your account, so this pull request was not reviewed.

Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs.