Quicksort implemented and certified in Lean

quicksort.lean

open List

def quicksort : List Nat → List Nat
| nil => nil
| pivot :: rest =>
  quicksort (rest.filter (· < pivot))
  ++ [pivot]
  ++ quicksort (rest.filter (· ≥ pivot))
termination_by l => l.length decreasing_by
  all_goals
    simp only [length_unattach, length_cons]
    grind only [usr length_filter_le, = length_attach]

theorem quicksort_is_permutation : (quicksort l) ~ l := by
  fun_induction quicksort l with
  | case1 => simp
  | case2 pivot rest hl hr =>
    rw [unattach_filter] at hl hr
    simp only [unattach_attach] at hl hr
    have h₀ : rest ~ rest.filter (· < pivot) ++ rest.filter (· ≥ pivot) := by
      grind [filter_append_perm (· < pivot) rest]
    have h₁ : quicksort (rest.filter (· < pivot)) ++ quicksort (rest.filter (· ≥ pivot))
              ~ rest.filter (· < pivot) ++ rest.filter (· ≥ pivot) := Perm.append hl hr
    all_goals grind

theorem quicksort_is_sorted : (quicksort l).Pairwise (· ≤ ·) := by
  fun_induction quicksort l with
  | case1 => exact Pairwise.nil
  | case2 pivot rest hl hr =>
    rw [unattach_filter] at hl hr
    simp only [unattach_attach] at hl hr
    simp only [ge_iff_le, append_assoc, cons_append, nil_append, pairwise_append, pairwise_cons,
      mem_cons, forall_eq_or_imp]
    have hp(p) : ∀ x ∈ quicksort (rest.filter p), p x := by
      simp [Perm.mem_iff quicksort_is_permutation]
    and_intros
    exact hl
    intro x hx
    exact of_decide_eq_true (hp (· ≥ pivot) x hx)
    exact hr
    intro x hx
    and_intros
    exact Nat.le_of_lt (of_decide_eq_true (hp (· < pivot) x hx))
    all_goals grind

def main (args : List String) : IO Unit := do
  IO.println <| quicksort <| args.flatMap fun arg => arg.toNat?.toList