Correctness of Batcher sorting

Bitonic merge orders the projected keys, while the permutation theorems in Basic preserve complete records. Sorting the two halves in opposite directions supplies the bitonic invariant.

Main results

• Cslib.BitonicSort.monotone_sort: ascending sorting orders the keys.
• Cslib.BitonicSort.antitone_sort: descending sorting orders the keys.

References

• Adapted from MassProduction/SortingSemantics/Internal.lean in S. Schlesinger, Boolean circuit mass production formalization.

theorem Cslib.BitonicSort.IsBitonic.min_le_max_halves {κ : Type u_2} [LinearOrder κ] {n : ℕ} (first second : Fin n → κ) (h : IsBitonic (Fin.append first second)) (i j : Fin n) : min (first i) (second i) ≤ max (first j) (second j)

Every minimum half-entry lies below every maximum half-entry of a bitonic tuple.

theorem Cslib.BitonicSort.isBitonic_append {κ : Type u_2} [LinearOrder κ] {n m : ℕ} {first : Fin n → κ} {second : Fin m → κ} (hfirst : Monotone first) (hsecond : Antitone second) : IsBitonic (Fin.append first second)

An increasing tuple followed by a decreasing tuple is bitonic.

theorem Cslib.BitonicSort.compareLayer_keys {α : Type u_1} {κ : Type u_2} [LinearOrder κ] (key : α → κ) {n : ℕ} (ascending : Bool) (input : Fin (n + n) → α) : key ∘ compareLayer key ascending input = have first := key ∘ input ∘ Fin.castAdd n; have second := key ∘ input ∘ Fin.natAdd n; if ascending = true then Fin.append (first ⊓ second) (first ⊔ second) else Fin.append (first ⊔ second) (first ⊓ second)

Projected keys after one layer are the pointwise minima and maxima of the two halves.

theorem Cslib.BitonicSort.merge_sorted {α : Type u_1} {κ : Type u_2} [LinearOrder κ] (key : α → κ) (depth : ℕ) (ascending : Bool) (input : Fin (arity depth) → α) (hbitonic : IsBitonic (key ∘ input)) : if ascending = true then Monotone (key ∘ merge key depth ascending input) else Antitone (key ∘ merge key depth ascending input)

Merging a bitonic tuple orders its keys in the chosen direction.

theorem Cslib.BitonicSort.sort_sorted {α : Type u_1} {κ : Type u_2} [LinearOrder κ] (key : α → κ) (depth : ℕ) (ascending : Bool) (input : Fin (arity depth) → α) : if ascending = true then Monotone (key ∘ sort key depth ascending input) else Antitone (key ∘ sort key depth ascending input)

Batcher sorting orders the keys in either direction on every input.

theorem Cslib.BitonicSort.monotone_sort {α : Type u_1} {κ : Type u_2} [LinearOrder κ] (key : α → κ) (depth : ℕ) (input : Fin (arity depth) → α) : Monotone (key ∘ sort key depth true input)

Ascending Batcher sorting gives nondecreasing keys.

theorem Cslib.BitonicSort.antitone_sort {α : Type u_1} {κ : Type u_2} [LinearOrder κ] (key : α → κ) (depth : ℕ) (input : Fin (arity depth) → α) : Antitone (key ∘ sort key depth false input)

Descending Batcher sorting gives nonincreasing keys.