Three-way partitioning

StructureThree-way partition record#✓fully proved

A three-way partition over a type \(\alpha\) consists of three lists over \(\alpha\), called below, equal and above. They are meant to hold the elements strictly below, equal to, and strictly above a pivot; the record itself imposes no condition on them.

@[ext]
structure ThreeWayPartition (α : Type u) where
  /-- Elements strictly below the pivot. -/
  below : List α
  /-- Elements equal to the pivot. -/
  equal : List α
  /-- Elements strictly above the pivot. -/
  above : List α
deriving DecidableEq

Used by 26

Used byMedian-of-medians selection · Correctness of median-of-medians selection · Out-of-range ranks cost no comparisons · Median-of-medians selection is quickselect on short lists · Median-of-medians selection succeeds on valid ranks · Set rank of a median-of-medians result · Median of medians makes linearly many comparisons · Entries at most the pivot · Entries below the pivot · Counting through the below block · Counting through the above block · Quickselect · Correctness of quickselect · Quickselect fails exactly out of range · Worst-case comparison bound for quickselect · Quicksort · Correctness of quicksort · Expected comparisons of quicksort on a random permutation · Worst-case comparison bound for quicksort · Stable three-way partition · The above list of a three-way partition is a filter · The below list of a three-way partition is a filter · Correctness of the stable three-way partition · The equal list of a three-way partition is a filter · Sizes of the three parts of a three-way partition · Cost of the stable three-way partition

DefinitionStable three-way partition#✓fully proved

Let \(p\) be an element of a linearly ordered type \(\alpha\). The three-way partition of a list over \(\alpha\) around \(p\), together with the time it is charged, is defined by recursion on the list. The empty list gives three empty lists at no cost. For a list with head \(x\) and tail \(xs\), one unit of time is charged for comparing \(x\) with \(p\), the tail \(xs\) is partitioned, and \(x\) is put at the front of its below list if \(x < p\), of its equal list if \(x = p\), and of its above list if \(p < x\).

def partition3 (pivot : α) : List α → TimeM Nat (ThreeWayPartition α)
  | [] => pure { below := [], equal := [], above := [] }
  | x :: xs => do
      ✓
      let parts ← partition3 pivot xs
      match cmp x pivot with
      | .lt => return { parts with below := x :: parts.below }
      | .eq => return { parts with equal := x :: parts.equal }
      | .gt => return { parts with above := x :: parts.above }

@[ext]
structure ThreeWayPartition (α : Type u) where
  /-- Elements strictly below the pivot. -/
  below : List α
  /-- Elements equal to the pivot. -/
  equal : List α
  /-- Elements strictly above the pivot. -/
  above : List α
deriving DecidableEq

CSLibExt/Algorithms/Lean/Sort/Partition.lean:37

Uses 1 · Used by 25

Statement usesThree-way partition record

Used byMedian-of-medians selection · Correctness of median-of-medians selection · Out-of-range ranks cost no comparisons · Median-of-medians selection is quickselect on short lists · Median-of-medians selection succeeds on valid ranks · Set rank of a median-of-medians result · Median of medians makes linearly many comparisons · Entries at most the pivot · Entries below the pivot · Counting through the below block · Counting through the above block · Quickselect · Correctness of quickselect · Quickselect fails exactly out of range · Worst-case comparison bound for quickselect · Quicksort · Correctness of quicksort · Expected comparisons of quicksort on a random permutation · Worst-case comparison bound for quicksort · The above list of a three-way partition is a filter · The below list of a three-way partition is a filter · Correctness of the stable three-way partition · The equal list of a three-way partition is a filter · Sizes of the three parts of a three-way partition · Cost of the stable three-way partition

TheoremCost of the stable three-way partition#✓fully proved

For every element \(p\) of a linearly ordered type \(\alpha\) and every list \(xs\) over \(\alpha\), the time charged by the stable three-way partition of \(xs\) around \(p\) equals the length of \(xs\): one unit for each comparison, one comparison per element.

@[simp]
theorem partition3_time (pivot : α) (xs : List α) :
    (partition3 pivot xs).time = xs.length

def partition3 (pivot : α) : List α → TimeM Nat (ThreeWayPartition α)
  | [] => pure { below := [], equal := [], above := [] }
  | x :: xs => do
      ✓
      let parts ← partition3 pivot xs
      match cmp x pivot with
      | .lt => return { parts with below := x :: parts.below }
      | .eq => return { parts with equal := x :: parts.equal }
      | .gt => return { parts with above := x :: parts.above }

CSLibExt/Algorithms/Lean/Sort/Partition.lean:47

Uses 2 · Used by 4

Statement usesThree-way partition record · Stable three-way partition

Used byMedian of medians makes linearly many comparisons · Worst-case comparison bound for quickselect · Expected comparisons of quicksort on a random permutation · Worst-case comparison bound for quicksort

TheoremCorrectness of the stable three-way partition#✓fully proved

Let \(p\) be an element of a linearly ordered type \(\alpha\), let \(xs\) be a list over \(\alpha\), and let \(B\), \(E\) and \(A\) be the below, equal and above lists of the stable three-way partition of \(xs\) around \(p\). Then the concatenation \(B\), \(E\), \(A\) is a permutation of \(xs\), every element \(x\) of \(B\) satisfies \(x < p\), every element of \(E\) equals \(p\), and every element \(x\) of \(A\) satisfies \(p < x\).

theorem partition3_correct (pivot : α) (xs : List α) :
    List.Perm
        ((partition3 pivot xs).ret.below ++
          (partition3 pivot xs).ret.equal ++
          (partition3 pivot xs).ret.above)
        xs ∧
      (∀ x ∈ (partition3 pivot xs).ret.below, x < pivot) ∧
      (∀ x ∈ (partition3 pivot xs).ret.equal, x = pivot) ∧
      ∀ x ∈ (partition3 pivot xs).ret.above, pivot < x

def partition3 (pivot : α) : List α → TimeM Nat (ThreeWayPartition α)
  | [] => pure { below := [], equal := [], above := [] }
  | x :: xs => do
      ✓
      let parts ← partition3 pivot xs
      match cmp x pivot with
      | .lt => return { parts with below := x :: parts.below }
      | .eq => return { parts with equal := x :: parts.equal }
      | .gt => return { parts with above := x :: parts.above }

CSLibExt/Algorithms/Lean/Sort/Partition.lean:47

Uses 2 · Used by 10

Statement usesThree-way partition record · Stable three-way partition

Used byCorrectness of median-of-medians selection · Median-of-medians selection succeeds on valid ranks · Median of medians makes linearly many comparisons · Entries at most the pivot · Entries below the pivot · Counting through the below block · Counting through the above block · Correctness of quickselect · Correctness of quicksort · Sizes of the three parts of a three-way partition

TheoremThe below list of a three-way partition is a filter#✓fully proved

For every element \(p\) of a linearly ordered type \(\alpha\) and every list \(xs\) over \(\alpha\), the below list of the stable three-way partition of \(xs\) around \(p\) is the list of the elements \(x\) of \(xs\) with \(x < p\), in their order in \(xs\) and with their multiplicities.

theorem partition3_below_eq_filter (pivot : α) (xs : List α) :
    (partition3 pivot xs).ret.below = xs.filter (fun x => x < pivot)

def partition3 (pivot : α) : List α → TimeM Nat (ThreeWayPartition α)
  | [] => pure { below := [], equal := [], above := [] }
  | x :: xs => do
      ✓
      let parts ← partition3 pivot xs
      match cmp x pivot with
      | .lt => return { parts with below := x :: parts.below }
      | .eq => return { parts with equal := x :: parts.equal }
      | .gt => return { parts with above := x :: parts.above }

CSLibExt/Algorithms/Lean/Sort/Partition.lean:47

Uses 2 · Used by 1

Statement usesThree-way partition record · Stable three-way partition

Used byExpected comparisons of quicksort on a random permutation

TheoremThe equal list of a three-way partition is a filter#✓fully proved

For every element \(p\) of a linearly ordered type \(\alpha\) and every list \(xs\) over \(\alpha\), the equal list of the stable three-way partition of \(xs\) around \(p\) is the list of the elements \(x\) of \(xs\) with \(x = p\), in their order in \(xs\) and with their multiplicities.

theorem partition3_equal_eq_filter (pivot : α) (xs : List α) :
    (partition3 pivot xs).ret.equal = xs.filter (fun x => x = pivot)

def partition3 (pivot : α) : List α → TimeM Nat (ThreeWayPartition α)
  | [] => pure { below := [], equal := [], above := [] }
  | x :: xs => do
      ✓
      let parts ← partition3 pivot xs
      match cmp x pivot with
      | .lt => return { parts with below := x :: parts.below }
      | .eq => return { parts with equal := x :: parts.equal }
      | .gt => return { parts with above := x :: parts.above }

CSLibExt/Algorithms/Lean/Sort/Partition.lean:47

Uses 2 · Used by 3

Statement usesThree-way partition record · Stable three-way partition

Used byMedian-of-medians selection succeeds on valid ranks · Set rank of a median-of-medians result · Expected comparisons of quicksort on a random permutation

TheoremThe above list of a three-way partition is a filter#✓fully proved

For every element \(p\) of a linearly ordered type \(\alpha\) and every list \(xs\) over \(\alpha\), the above list of the stable three-way partition of \(xs\) around \(p\) is the list of the elements \(x\) of \(xs\) with \(p < x\), in their order in \(xs\) and with their multiplicities.

theorem partition3_above_eq_filter (pivot : α) (xs : List α) :
    (partition3 pivot xs).ret.above = xs.filter (fun x => pivot < x)

def partition3 (pivot : α) : List α → TimeM Nat (ThreeWayPartition α)
  | [] => pure { below := [], equal := [], above := [] }
  | x :: xs => do
      ✓
      let parts ← partition3 pivot xs
      match cmp x pivot with
      | .lt => return { parts with below := x :: parts.below }
      | .eq => return { parts with equal := x :: parts.equal }
      | .gt => return { parts with above := x :: parts.above }

CSLibExt/Algorithms/Lean/Sort/Partition.lean:47

Uses 2 · Used by 1

Statement usesThree-way partition record · Stable three-way partition

Used byExpected comparisons of quicksort on a random permutation

TheoremSizes of the three parts of a three-way partition#✓fully proved

For every element \(p\) of a linearly ordered type \(\alpha\) and every list \(xs\) over \(\alpha\), the lengths of the below, equal and above lists of the stable three-way partition of \(xs\) around \(p\) add up to the length of \(xs\).

theorem partition3_length (pivot : α) (xs : List α) :
    (partition3 pivot xs).ret.below.length +
        (partition3 pivot xs).ret.equal.length +
        (partition3 pivot xs).ret.above.length = xs.length

def partition3 (pivot : α) : List α → TimeM Nat (ThreeWayPartition α)
  | [] => pure { below := [], equal := [], above := [] }
  | x :: xs => do
      ✓
      let parts ← partition3 pivot xs
      match cmp x pivot with
      | .lt => return { parts with below := x :: parts.below }
      | .eq => return { parts with equal := x :: parts.equal }
      | .gt => return { parts with above := x :: parts.above }

CSLibExt/Algorithms/Lean/Sort/Partition.lean:47

Uses 3 · Used by 8

Statement usesThree-way partition record · Stable three-way partition

Proof usesCorrectness of the stable three-way partition

Used byMedian-of-medians selection succeeds on valid ranks · Median of medians makes linearly many comparisons · Correctness of quickselect · Quickselect fails exactly out of range · Worst-case comparison bound for quickselect · Correctness of quicksort · Expected comparisons of quicksort on a random permutation · Worst-case comparison bound for quicksort

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.