Skip to content

Commit

Permalink
feat: Array.qsort_sorted
Browse files Browse the repository at this point in the history
  • Loading branch information
digama0 committed Apr 21, 2024
1 parent 6a12bf7 commit f38f18e
Show file tree
Hide file tree
Showing 5 changed files with 471 additions and 6 deletions.
2 changes: 2 additions & 0 deletions Std/Data/Array.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
19 changes: 19 additions & 0 deletions Std/Data/Array/Lemmas.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
40 changes: 40 additions & 0 deletions Std/Data/Array/Perm.lean
Original file line number Diff line number Diff line change
@@ -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
Loading

0 comments on commit f38f18e

Please sign in to comment.