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

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)

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