From 7ffeacf967eb77c602edbaf85de39cc643a15e12 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 30 Apr 2025 23:32:05 +1000 Subject: [PATCH] chore: move `Array.qsort` to `Basic` file (#8177) No change to content, just moving into a subdirectory, to ease keeping a branch adding theorems in sync. --- src/Init/Data/Array/QSort.lean | 67 ++--------------------- src/Init/Data/Array/QSort/Basic.lean | 81 ++++++++++++++++++++++++++++ src/Init/Data/Vector/Lemmas.lean | 2 +- 3 files changed, 85 insertions(+), 65 deletions(-) create mode 100644 src/Init/Data/Array/QSort/Basic.lean diff --git a/src/Init/Data/Array/QSort.lean b/src/Init/Data/Array/QSort.lean index 2c48d71c7a..cbefecee76 100644 --- a/src/Init/Data/Array/QSort.lean +++ b/src/Init/Data/Array/QSort.lean @@ -1,70 +1,9 @@ /- -Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Copyright (c) 2024 Lean FRO. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura +Authors: Kim Morrison -/ module prelude -import Init.Data.Vector.Basic -import Init.Data.Ord - -set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. --- We do not enable `linter.indexVariables` because it is helpful to name index variables `lo`, `mid`, `hi`, etc. - -namespace Array - -private def qpartition {n} (as : Vector α n) (lt : α → α → Bool) (lo hi : Nat) - (hlo : lo < n := by omega) (hhi : hi < n := by omega) : {n : Nat // lo ≤ n} × Vector α n := - let mid := (lo + hi) / 2 - let as := if lt as[mid] as[lo] then as.swap lo mid else as - 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] - 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 - if lt as[j] pivot then - loop (as.swap i j) (i+1) (j+1) - else - loop as i (j+1) - else - (⟨i, ilo⟩, as.swap i hi) - loop as lo lo - -/-- -Sorts an array using the Quicksort algorithm. - -The optional parameter `lt` specifies an ordering predicate. It defaults to `LT.lt`, which must be -decidable to be used for sorting. Use `Array.qsortOrd` to sort the array according to the `Ord α` -instance. - -The optional parameters `low` and `high` delimit the region of the array that is sorted. Both are -inclusive, and default to sorting the entire array. --/ -@[inline] def qsort (as : Array α) (lt : α → α → Bool := by exact (· < ·)) - (low := 0) (high := as.size - 1) : Array α := - let rec @[specialize] sort {n} (as : Vector α n) (lo hi : Nat) - (hlo : lo < n := by omega) (hhi : hi < n := by omega) := - if h₁ : lo < hi then - let ⟨⟨mid, hmid⟩, as⟩ := qpartition as lt lo hi - if h₂ : mid ≥ hi then - as - else - sort (sort as lo mid) (mid+1) hi - else as - if h : as.size = 0 then - as - else - let low := min low (as.size - 1) - let high := min high (as.size - 1) - sort ⟨as, rfl⟩ low high |>.toArray - -set_option linter.unusedVariables.funArgs false in -/-- -Sorts an array using the Quicksort algorithm, using `Ord.compare` to compare elements. --/ -def qsortOrd [ord : Ord α] (xs : Array α) : Array α := - xs.qsort fun x y => compare x y |>.isLT - -end Array +import Init.Data.Array.QSort.Basic diff --git a/src/Init/Data/Array/QSort/Basic.lean b/src/Init/Data/Array/QSort/Basic.lean new file mode 100644 index 0000000000..cb8ac4c0f1 --- /dev/null +++ b/src/Init/Data/Array/QSort/Basic.lean @@ -0,0 +1,81 @@ +/- +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +module + +prelude +import Init.Data.Vector.Basic +import Init.Data.Ord + +set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables. +-- We do not enable `linter.indexVariables` because it is helpful to name index variables `lo`, `mid`, `hi`, etc. + + +namespace Array + +/-- +Internal implementation of `Array.qsort`. + +`qpartition as lt lo hi hlo hhi` returns a pair `(⟨m, h₁, h₂⟩, as')` where +`as'` is a permutation of `as` and `m` is a number such that: +- `lo ≤ m` +- `m < n` +- `∀ i, lo ≤ i → i < m → lt as[i] as[m]` +- `∀ j, m < j → j < hi → !lt as[j] as[m]` + +It does so by first swapping the elements at indices `lo`, `mid := (lo + hi) / 2`, and `hi` +if necessary so that the middle (pivot) element is at index `hi`. +We then iterate from `j = lo` to `j = hi`, with a pointer `i` starting at `lo`, and +swapping each element which is less than the pivot to position `i`, and then incrementing `i`. +-/ +def qpartition {n} (as : Vector α n) (lt : α → α → Bool) (lo hi : Nat) + (hlo : lo < n := by omega) (hhi : hi < n := by omega) : {m : Nat // lo ≤ m ∧ m < n} × Vector α n := + let mid := (lo + hi) / 2 + let as := if lt as[mid] as[lo] then as.swap lo mid else as + 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] + 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 + if lt as[j] pivot then + loop (as.swap i j) (i+1) (j+1) + else + loop as i (j+1) + else + (⟨i, ilo, by omega⟩, as.swap i hi) + loop as lo lo + +/-- +In-place quicksort. + +`qsort as lt low high` sorts the subarray `as[low:high+1]` in-place using `lt` to compare elements. +-/ +@[inline] def qsort (as : Array α) (lt : α → α → Bool := by exact (· < ·)) + (low := 0) (high := as.size - 1) : Array α := + let rec @[specialize] sort {n} (as : Vector α n) (lo hi : Nat) + (hlo : lo < n := by omega) (hhi : hi < n := by omega) := + if h₁ : lo < hi then + let ⟨⟨mid, hmid⟩, as⟩ := qpartition as lt lo hi + if h₂ : mid ≥ hi then + as + else + sort (sort as lo mid) (mid+1) hi + else as + if h : as.size = 0 then + as + else + let low := min low (as.size - 1) + let high := min high (as.size - 1) + sort as.toVector low high |>.toArray + +set_option linter.unusedVariables.funArgs false in +/-- +Sort an array using `compare` to compare elements. +-/ +def qsortOrd [ord : Ord α] (xs : Array α) : Array α := + xs.qsort fun x y => compare x y |>.isLT + +end Array diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index 77171a65d5..9d555ee4ca 100644 --- a/src/Init/Data/Vector/Lemmas.lean +++ b/src/Init/Data/Vector/Lemmas.lean @@ -3040,7 +3040,7 @@ theorem getElem_swap {xs : Vector α n} {i j : Nat} (hi hj) {k : Nat} (hk : k < (xs.swap i j hi hj)[i]'(by simpa using hi) = xs[j] := by simp [getElem_swap] -@[simp] theorem getElem_swap_of_ne {xs : Vector α n} {i j : Nat} (hi hj) (hk : k < n) +@[simp] theorem getElem_swap_of_ne {xs : Vector α n} {i j : Nat} {hi hj} {hk : k < n} (hi' : k ≠ i) (hj' : k ≠ j) : (xs.swap i j hi hj)[k] = xs[k] := by simp_all [getElem_swap]