feat: Array.qsort_sorted

Std/Data/Array.lean

@@ -4,3 +4,5 @@ import Std.Data.Array.Lemmas
 import Std.Data.Array.Match
 import Std.Data.Array.Merge
 import Std.Data.Array.Monadic
+import Std.Data.Array.Perm
+import Std.Data.Array.QSort

Std/Data/Array/Lemmas.lean

@@ -870,3 +870,22 @@ theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i :=
     split
     · split <;> simp_all
     · split <;> simp_all
+
+theorem swap_self (a : Array α) (i : Fin a.size) : a.swap i i = a := by
+  apply ext
+  · simp only [size_swap]
+  · intros
+    simp only [get_swap']
+    split <;> simp_all
+
+theorem swap_of_append (as : Array α)
+  {A a B b C} {i j} (hi : A.length = i.1) (hj : i.1 + B.length + 1 = j.1)
+    (eq1 : as.data = A ++ a :: B ++ b :: C) :
+    (as.swap i j).data = A ++ b :: B ++ a :: C := by
+  simp only [swap, get, data_set, Fin.cast_mk,
+    fun a b => show ∀ (e : b = a) (v : Fin b), (e ▸ v) = v.cast e by rintro rfl v; rfl]
+  rw [List.get_of_append' (by simpa using eq1) hi]
+  rw [List.set_of_append (l₁ := A ++ b :: B) (a := b) (l₂ := C) _ ?_ (by simp [hi, ← hj]; rfl)]
+  rw [List.get_of_append' eq1 (by simp [hi, ← hj]; rfl)]
+  rw [List.set_of_append (l₁ := A) (a := a) (l₂ := B ++ b :: C) _ (by simp [eq1]) hi]
+  simp

Std/Data/Array/Perm.lean

@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2024 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Mario Carneiro
+-/
+import Std.Data.Array.Lemmas
+import Std.Data.List.Perm
+
+namespace Array
+open List
+
+theorem swap_of_append_right (as : Array α)
+  {A B b C} {i j} (hi : A.length = i.1) (hj : i.1 + B.length = j.1)
+    (eq1 : as.data = A ++ B ++ b :: C) :
+    ∃ B', B' ~ B ∧ (as.swap i j).data = A ++ b :: B' ++ C := by
+  match B with
+  | [] => exact ⟨[], .rfl, by cases Fin.ext hj; simp [swap_self, eq1]⟩
+  | a :: B =>
+    refine ⟨B ++ [a], perm_append_comm, ?_⟩
+    simpa using swap_of_append as hi (by simpa using hj) eq1
+
+theorem swap_of_append_left (as : Array α)
+  {A a B C} {i j} (hi : A.length = i.1) (hj : i.1 + B.length = j.1)
+    (eq1 : as.data = A ++ a :: B ++ C) :
+    ∃ B', B' ~ B ∧ (as.swap i j).data = A ++ B' ++ a :: C := by
+  obtain rfl | ⟨B, b, rfl⟩ := eq_nil_or_concat B
+  · exact ⟨[], .rfl, by cases Fin.ext hj; simp [swap_self, eq1]⟩
+  · refine ⟨b :: B, perm_append_comm (l₁ := [_]), ?_⟩
+    exact swap_of_append as hi (by simpa using hj) (by simp [eq1])
+
+theorem swap_perm (as : Array α) (i j : Fin as.size) : (as.swap i j).data ~ as.data := by
+  have {i j} (ij : i < j) : (as.swap i j).data ~ as.data := by
+    have ⟨A, a, B, b, C, h1, h2, eq⟩ := exists_three_of_lt _ ij j.2
+    rw [eq, swap_of_append as h1 h2 eq, List.append_assoc, List.append_assoc]
+    exact .append_left _ <| perm_middle.trans <| .cons _ perm_middle.symm
+  obtain h | h | h := Nat.lt_trichotomy i j
+  · exact this h
+  · rw [Fin.eq_of_val_eq h, swap_self]
+  · rw [swap_comm]; exact this h