1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17

import Mathlib

-- https://byorgey.github.io/blog/posts/2019/02/16/worstsort.html

def BadSort [LinearOrder α] (A : List α)
  | 0 => A.insertionSort (· ≤ ·)
  | Nat.succ n => BadSort A.permutations n |>.headD []

def WorstSort [LinearOrder α] (A : List α) (f : ℕ → ℕ) := BadSort A <| f A.length

def DiabolicalSort [LinearOrder α] (A : List α) := WorstSort A fun n ↦ ack n n

theorem BadSortCorrect [LinearOrder α] (A : List α) n : (BadSort A n).Perm A ∧ (BadSort A n).SortedLE := by
  sorry


-- Probably not to hard to prove that this is correct but left as an exercise to the reader