feat: verification of qsort via grind (#7995)

This PR adds a verification of `Array.qsort` properties, trying to use
`grind` and `fun_induction` where possible.
Currently this is in the `tests/` folder, but once `grind` is ready for
production use we will move it out into the library.

Note that the current `qsort` algorithm has quadratic behaviour on
constant lists, and needs to be adjusted. We'll only move the
verification out into the library once this has been fixed (and the
proofs adapted). These verification theorems may be commented out in the
meantime if it's urgent to fix `qsort`.

---------

Co-authored-by: Kyle Miller <[email protected]>
Co-authored-by: Joachim Breitner <[email protected]>

Author: 3 people

src/Init/Data/Array/QSort/Basic.lean

@@ -37,6 +37,10 @@ def qpartition {n} (as : Vector α n) (lt : α → α → Bool) (lo hi : Nat)
   let as  := if lt as[hi]  as[lo] then as.swap lo hi  else as
   let as  := if lt as[mid] as[hi] then as.swap mid hi else as
   let pivot := as[hi]
+  -- During this loop, elements below in `[lo, i)` are less than `pivot`,
+  -- elements in `[i, j)` are greater than or equal to `pivot`,
+  -- elements in `[j, hi)` are unexamined,
+  -- while `as[hi]` is (by definition) the pivot.
   let rec loop (as : Vector α n) (i j : Nat)
       (ilo : lo ≤ i := by omega) (jh : j < n := by omega) (w : i ≤ j := by omega) :=
     if h : j < hi then
@@ -60,8 +64,11 @@ In-place quicksort.
     if h₁ : lo < hi then
       let ⟨⟨mid, hmid⟩, as⟩ := qpartition as lt lo hi
       if h₂ : mid ≥ hi then
+        -- This only occurs when `hi ≤ lo`,
+        -- and thus `as[low:high+1]` is trivially already sorted.
         as
       else
+        -- Otherwise, we recursively sort the two subarrays.
         sort (sort as lo mid) (mid+1) hi
     else as
   if h : as.size = 0 then

src/Init/Grind/Tactics.lean

@@ -98,7 +98,7 @@ structure Config where
   This approach is cheaper but incomplete. -/
   qlia : Bool := false
   /--
-  If `mbtc` is `true`, `grind` will use model-based theory commbination for creating new case splits.
+  If `mbtc` is `true`, `grind` will use model-based theory combination for creating new case splits.
   See paper "Model-based Theory Combination" for details.
   -/
   mbtc : Bool := true