Sorting Network

Create a sorting network that sorts a list in O(n log^2 n) swaps.

Function Signature

def sorting_network (l : Nat) : List (Fin l × Fin l)

Theorem Signature

def sorting_network_sorts (xs : List Nat) :
  (Id.run do
    let mut sorted_xs := xs
    for (i1, i2) in (sorting_network xs.length) do
      let x1 := sorted_xs[i1]!
      let x2 := sorted_xs[i2]!
      if x1 > x2 then
        sorted_xs := sorted_xs.set i1 x2
        sorted_xs := sorted_xs.set i2 x1
    return sorted_xs) = xs.insertionSort (fun a b => a ≤ b)

Additional Theorem Signature

def sorting_network_efficient (l : Nat) :
  ∃ c, (sorting_network l).length ≤ c * l * (Nat.log l) ^ 2

View All Submissions

Please log in or register to submit a solution for this challenge.