BadSort

Changes

1 changed files (+13/-0)

• BadSort.lean (new)
  • @@ -0,0 +1,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