Simultaneous minimum and maximum

DefinitionSimultaneous minimum and maximum#✓fully proved

Given a list \(xs\) over a linearly ordered type, the paired algorithm returns no result when \(xs\) is empty and otherwise returns a pair (a candidate minimum and a candidate maximum), counting one unit of time for each comparison of elements. On a one-element list \([a]\) it returns \((a, a)\) without a comparison. On a longer list of odd length both candidates start at the first element without a comparison; on a list of even length they start at the smaller and the larger of the first two elements, found with one comparison. The remaining elements are then taken in consecutive pairs: one comparison orders the pair, its smaller member replaces the candidate minimum if it is strictly smaller (one comparison), and its larger member replaces the candidate maximum if it is strictly larger (one comparison).

public def minMax {α : Type u} [LinearOrder α] (xs : List α) :
    TimeM Nat (Option (α × α)) :=
  match xs with
  | [] => pure none
  | [a] => pure (some (a, a))
  | a :: b :: rest =>
      if xs.length % 2 = 1 then
        some <$> scanPairs a a (b :: rest)
      else do
        let pair ← orderPair a b
        some <$> scanPairs pair.1 pair.2 rest

Used by 8

Used byThe min–max algorithm returns no result exactly on the empty list · Characterization of the min–max output · The min–max algorithm on the empty list · Correctness of the simultaneous minimum and maximum algorithm · The min–max algorithm on a one-element list · Comparison count of the simultaneous minimum and maximum algorithm · Comparisons of the min–max algorithm on even-length lists · Comparisons of the min–max algorithm on odd-length lists

TheoremCorrectness of the simultaneous minimum and maximum algorithm#✓fully proved

For every list \(xs\) over a linearly ordered type, the simultaneous minimum and maximum algorithm returns no result on \(xs\) when \(xs\) is empty, and returns the pair \((\min xs, \max xs)\) of the least and greatest elements of \(xs\) otherwise.

theorem minMax_ret {α : Type u} [LinearOrder α] (xs : List α) :
    (minMax xs).ret = xs.min?.bind (fun lo => xs.max?.map (fun hi => (lo, hi)))

Uses 1 · Used by 2

Statement usesSimultaneous minimum and maximum

Used byThe min–max algorithm returns no result exactly on the empty list · Characterization of the min–max output

TheoremThe min–max algorithm returns no result exactly on the empty list#✓fully proved

For every list \(xs\) over a linearly ordered type, the simultaneous minimum and maximum algorithm returns no result on \(xs\) if and only if \(xs\) is empty.

theorem minMax_eq_none_iff {α : Type u} [LinearOrder α] (xs : List α) :
    (minMax xs).ret = none ↔ xs = []

Uses 2

Statement usesSimultaneous minimum and maximum

Proof usesCorrectness of the simultaneous minimum and maximum algorithm

TheoremCharacterization of the min–max output#✓fully proved

For every list \(xs\) over a linearly ordered type and all elements \(lo\) and \(hi\) of that type, the simultaneous minimum and maximum algorithm returns the pair \((lo, hi)\) on \(xs\) if and only if \(lo\) and \(hi\) both belong to \(xs\), \(lo \le x\) for every \(x\) in \(xs\), and \(x \le hi\) for every \(x\) in \(xs\).

theorem minMax_eq_some_iff {α : Type u} [LinearOrder α] (xs : List α) (lo hi : α) :
    (minMax xs).ret = some (lo, hi) ↔
      lo ∈ xs ∧ hi ∈ xs ∧ (∀ x ∈ xs, lo ≤ x) ∧ (∀ x ∈ xs, x ≤ hi)

Uses 2

Statement usesSimultaneous minimum and maximum

Proof usesCorrectness of the simultaneous minimum and maximum algorithm

TheoremThe min–max algorithm on the empty list#✓fully proved

On the empty list, the simultaneous minimum and maximum algorithm returns no result and makes no comparisons.

@[simp] theorem minMax_nil {α : Type u} [LinearOrder α] :
    minMax ([] : List α) = pure none

Uses 1 · Used by 1

Statement usesSimultaneous minimum and maximum

Used byComparison count of the simultaneous minimum and maximum algorithm

TheoremThe min–max algorithm on a one-element list#✓fully proved

For every element \(a\) of a linearly ordered type, on the list \([a]\) the simultaneous minimum and maximum algorithm returns the pair \((a, a)\) and makes no comparisons.

@[simp] theorem minMax_singleton {α : Type u} [LinearOrder α] (a : α) :
    minMax [a] = pure (some (a, a))

Uses 1 · Used by 1

Statement usesSimultaneous minimum and maximum

Used byComparisons of the min–max algorithm on odd-length lists

TheoremComparisons of the min–max algorithm on odd-length lists#✓fully proved

For every natural number \(k\) and every list of length \(2k + 1\) over a linearly ordered type, the simultaneous minimum and maximum algorithm makes exactly \(3k\) comparisons.

theorem minMax_time_odd {α : Type u} [LinearOrder α] (xs : List α) (k : Nat)
    (hlen : xs.length = 2 * k + 1) : (minMax xs).time = 3 * k

Uses 2 · Used by 1

Statement usesSimultaneous minimum and maximum

Proof usesThe min–max algorithm on a one-element list

Used byComparison count of the simultaneous minimum and maximum algorithm

TheoremComparisons of the min–max algorithm on even-length lists#✓fully proved

For every natural number \(k \ge 1\) and every list of length \(2k\) over a linearly ordered type, the simultaneous minimum and maximum algorithm makes exactly \(3k - 2\) comparisons.

theorem minMax_time_even {α : Type u} [LinearOrder α] (xs : List α) (k : Nat)
    (hlen : xs.length = 2 * k) (hk : 1 ≤ k) : (minMax xs).time = 3 * k - 2

Uses 1 · Used by 1

Statement usesSimultaneous minimum and maximum

Used byComparison count of the simultaneous minimum and maximum algorithm

TheoremComparison count of the simultaneous minimum and maximum algorithm#✓fully proved

For every list of length \(n\) over a linearly ordered type, the simultaneous minimum and maximum algorithm makes no comparisons when \(n = 0\) and exactly \(\lceil 3n/2 \rceil - 2\) comparisons when \(n \ge 1\).

This counts element-order decisions, not full RAM instructions or comparator bit complexity.

theorem minMax_time {α : Type u} [LinearOrder α] (xs : List α) :
    (minMax xs).time =
      if xs.length = 0 then 0 else ((3 * xs.length + 1) / 2) - 2

Uses 4

Statement usesSimultaneous minimum and maximum

Proof usesThe min–max algorithm on the empty list · Comparisons of the min–max algorithm on even-length lists · Comparisons of the min–max algorithm on odd-length lists

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.