Binary search

TheoremArray binary search membership test agrees with binary search#✓fully proved

Let \(A\) be an array with entries in a type \(\alpha\), let \(k \in \alpha\), let \(\mathrm{lt}\) be any Boolean-valued comparison on \(\alpha\), and let \(\ell\) and \(h\) be natural numbers. Lean core's Boolean binary search membership test for \(k\) in \(A\), with comparison \(\mathrm{lt}\) and bounds \(\ell\) and \(h\), returns true exactly when Lean core's array binary search with the same arguments returns some element.

theorem binSearchContains_eq_isSome {α : Type} (as : Array α) (k : α)
    (lt : α → α → Bool) (lo hi : Nat) :
    as.binSearchContains k lt lo hi = (as.binSearch k lt lo hi).isSome
Used by 1
Used byBounded binary search membership test on a sorted array is correct

TheoremResult of bounded binary search on a sorted array#✓fully proved

Let \(A = (a_0, \dots, a_{n-1})\) be an array of length \(n\) with entries in a linearly ordered type, with \(a_i \le a_j\) whenever \(i < j\). Let \(k\) and \(a\) be elements of that type and \(\ell\), \(h\) natural numbers. Lean core's array binary search for \(k\) in \(A\), with the strict order \(<\) as comparison and inclusive bounds \(\ell\) and \(h\), returns \(a\) if and only if \(a = k\) and there is an index \(i < n\) with \(\ell \le i \le h\) and \(a_i = k\).

The requirement \(i < n\) reflects the implementation's clamping of an upper bound \(h \ge n\) to \(n - 1\).

theorem binSearch_eq_some_iff {α : Type} [LinearOrder α] {as : Array α}
    (hs : as.Pairwise (fun a b => a ≤ b)) {k a : α} {lo hi : Nat} :
    as.binSearch k (fun x y => decide (x < y)) lo hi = some a ↔
      a = k ∧ ∃ i, ∃ h : i < as.size, lo ≤ i ∧ i ≤ hi ∧ as[i] = k
Used by 1
Used byBinary search on a sorted array finds exactly its members

TheoremBounded binary search on a sorted array fails exactly when the key is absent#✓fully proved

Let \(A = (a_0, \dots, a_{n-1})\) be an array of length \(n\) with entries in a linearly ordered type, with \(a_i \le a_j\) whenever \(i < j\). Let \(k\) be an element of that type and \(\ell\), \(h\) natural numbers. Lean core's array binary search for \(k\) in \(A\), with the strict order \(<\) as comparison and inclusive bounds \(\ell\) and \(h\), returns no element if and only if there is no index \(i < n\) with \(\ell \le i \le h\) and \(a_i = k\).

theorem binSearch_eq_none_iff {α : Type} [LinearOrder α] {as : Array α}
    (hs : as.Pairwise (fun a b => a ≤ b)) {k : α} {lo hi : Nat} :
    as.binSearch k (fun x y => decide (x < y)) lo hi = none ↔
      ¬∃ i, ∃ h : i < as.size, lo ≤ i ∧ i ≤ hi ∧ as[i] = k
Used by 1
Used byBinary search on a sorted array fails exactly on non-members

TheoremBounded binary search membership test on a sorted array is correct#✓fully proved

Let \(A = (a_0, \dots, a_{n-1})\) be an array of length \(n\) with entries in a linearly ordered type, with \(a_i \le a_j\) whenever \(i < j\). Let \(k\) be an element of that type and \(\ell\), \(h\) natural numbers. Lean core's Boolean binary search membership test for \(k\) in \(A\), with the strict order \(<\) as comparison and inclusive bounds \(\ell\) and \(h\), returns true if and only if there is an index \(i < n\) with \(\ell \le i \le h\) and \(a_i = k\).

theorem binSearchContains_eq_true_iff {α : Type} [LinearOrder α] {as : Array α}
    (hs : as.Pairwise (fun a b => a ≤ b)) {k : α} {lo hi : Nat} :
    as.binSearchContains k (fun x y => decide (x < y)) lo hi = true ↔
      ∃ i, ∃ h : i < as.size, lo ≤ i ∧ i ≤ hi ∧ as[i] = k
Uses 1 · Used by 1
Proof usesArray binary search membership test agrees with binary search
Used byBinary search membership test on a sorted array is correct

TheoremBinary search on a sorted array finds exactly its members#✓fully proved

Let \(A\) be an array with entries in a linearly ordered type, sorted so that an earlier entry is never greater than a later one, and let \(k\) and \(a\) be elements of that type. Lean core's array binary search for \(k\) over the whole of \(A\), with the strict order \(<\) as comparison, returns \(a\) if and only if \(a = k\) and \(k\) is an entry of \(A\).

theorem binSearch_eq_some_iff_mem {α : Type} [LinearOrder α] {as : Array α}
    (hs : as.Pairwise (fun a b => a ≤ b)) {k a : α} :
    as.binSearch k (fun x y => decide (x < y)) = some a ↔ a = k ∧ k ∈ as
Uses 1
Proof usesResult of bounded binary search on a sorted array

TheoremBinary search on a sorted array fails exactly on non-members#✓fully proved

Let \(A\) be an array with entries in a linearly ordered type, sorted so that an earlier entry is never greater than a later one, and let \(k\) be an element of that type. Lean core's array binary search for \(k\) over the whole of \(A\), with the strict order \(<\) as comparison, returns no element if and only if \(k\) is not an entry of \(A\).

theorem binSearch_eq_none_iff_not_mem {α : Type} [LinearOrder α] {as : Array α}
    (hs : as.Pairwise (fun a b => a ≤ b)) {k : α} :
    as.binSearch k (fun x y => decide (x < y)) = none ↔ k ∉ as
Uses 1
Proof usesBounded binary search on a sorted array fails exactly when the key is absent

TheoremBinary search membership test on a sorted array is correct#✓fully proved

Let \(A\) be an array with entries in a linearly ordered type, sorted so that an earlier entry is never greater than a later one, and let \(k\) be an element of that type. Lean core's Boolean binary search membership test for \(k\) over the whole of \(A\), with the strict order \(<\) as comparison, returns true if and only if \(k\) is an entry of \(A\).

theorem binSearchContains_eq_true_iff_mem {α : Type} [LinearOrder α] {as : Array α}
    (hs : as.Pairwise (fun a b => a ≤ b)) {k : α} :
    as.binSearchContains k (fun x y => decide (x < y)) = true ↔ k ∈ as
Uses 1
Proof usesBounded binary search membership test on a sorted array is correct

DefinitionLower-bound search#✓fully proved

Given an array \(a = (a_0, \dots, a_{n-1})\) over a linearly ordered type and a key \(k\), lower-bound search maintains a half-open interval \([l, h)\) of indices, starting from \([0, n)\). While \(l < h\), it compares \(a_m\) with \(k\) at the midpoint \(m = l + \lfloor (h - l)/2 \rfloor\), charging one unit for this comparison, and continues with \([m + 1, h)\) if \(a_m < k\) and with \([l, m)\) otherwise. When \(l = h\) it returns \(l\).

When \(a\) is sorted in nondecreasing order (or at least partitioned at \(k\): every entry before the returned index is \(< k\) and every entry from that index on is \(\ge k\)), the result is the first index \(i\) with \(k \le a_i\), or \(n\) if every entry is below \(k\). On an unsorted array the result is unspecified: for \(a = (2, 1)\) and \(k = 2\) the search returns \(2\), not the first index \(0\) with \(k \le a_0\).

Cslib.Algorithms.Lean.TimeM.lowerBound · 18 lines 
def lowerBound (xs : Array α) (key : α) : TimeM Nat Nat :=
  let rec loop (lo hi : Nat) (hlohi : lo ≤ hi) (hhi : hi ≤ xs.size) : TimeM Nat Nat :=
    if h : lo < hi then
      let mid := lo + (hi - lo) / 2
      have hmidhi : mid < hi := by
        dsimp [mid]
        omega
      have hmid : mid < xs.size := hmidhi.trans_le hhi
      do
        ✓
        if xs[mid] < key then
          loop (mid + 1) hi (by omega) hhi
        else
          loop lo mid (by omega) (hmidhi.le.trans hhi)
    else
      pure lo
  termination_by hi - lo
  loop 0 xs.size (Nat.zero_le _) le_rfl
Used by 11
Used byComparison bound for patience sorting · Patience step · A patience step grows the tails by at most one · The patience scan preserves the invariant · Binary search for the first occurrence · Binary search reports absence exactly when the key is absent · Binary search returns the first occurrence of the key · Exact comparison count of binary search for the first occurrence · Comparison bound for binary search for the first occurrence · Correctness of lower-bound search · Comparison bound for lower-bound search

TheoremCorrectness of lower-bound search#✓fully proved

Let \(a = (a_0, \dots, a_{n-1})\) be an array over a linearly ordered type, sorted in nondecreasing order, let \(k\) be a key, and let \(\ell\) be the index returned by lower-bound search for \(k\) in \(a\). Then \(\ell \le n\), \(a_j < k\) for every \(j < \ell\), and \(k \le a_j\) for every \(j\) with \(\ell \le j < n\).

theorem lowerBound_spec (xs : Array α) (key : α)
    (hs : xs.Pairwise (fun x y => x ≤ y)) :
    (lowerBound xs key).ret ≤ xs.size ∧
      (∀ j (_hj : j < (lowerBound xs key).ret) (_hjs : j < xs.size), xs[j] < key) ∧
      (∀ j (_hj : (lowerBound xs key).ret ≤ j) (_hjs : j < xs.size), key ≤ xs[j])
Uses 1 · Used by 3
Statement usesLower-bound search
Used byThe patience scan preserves the invariant · Binary search reports absence exactly when the key is absent · Binary search returns the first occurrence of the key

TheoremComparison bound for lower-bound search#✓fully proved

For every array \(a\) of length \(n\) over a linearly ordered type and every key \(k\), lower-bound search for \(k\) in \(a\) makes at most \(\lceil \log_2 (n + 1) \rceil\) element comparisons.

theorem lowerBound_time_le (xs : Array α) (key : α) :
    (lowerBound xs key).time ≤ Nat.clog 2 (xs.size + 1)
Uses 1 · Used by 2
Statement usesLower-bound search
Used byComparison bound for patience sorting · Comparison bound for binary search for the first occurrence

DefinitionBinary search for the first occurrence#✓fully proved

Given an array \(a = (a_0, \dots, a_{n-1})\) over a linearly ordered type and a key \(k\), binary search for the first occurrence of \(k\) in \(a\) runs lower-bound search for \(k\) in \(a\), obtaining an index \(\ell\). If \(\ell < n\), it makes one further comparison, charged one unit, and returns \(\ell\) when \(a_\ell = k\) and no index otherwise; if \(\ell \ge n\), it returns no index without further cost.

When \(a\) is sorted in nondecreasing order, the result is the first index \(i\) with \(a_i = k\), or no index when \(k\) does not occur in \(a\). On an unsorted array a present key can be missed and the result can be no index.

def binarySearchFirst? (xs : Array α) (key : α) : TimeM Nat (Option Nat) := do
  let i ← lowerBound xs key
  if h : i < xs.size then
    ✓
    if xs[i] = key then
      return some i
    else
      return none
  else
    return none
Uses 1 · Used by 4
Statement usesLower-bound search
Used byBinary search reports absence exactly when the key is absent · Binary search returns the first occurrence of the key · Exact comparison count of binary search for the first occurrence · Comparison bound for binary search for the first occurrence

TheoremBinary search returns the first occurrence of the key#✓fully proved

Let \(a = (a_0, \dots, a_{n-1})\) be an array over a linearly ordered type, sorted in nondecreasing order, let \(k\) be a key and let \(i\) be a natural number. Binary search for the first occurrence of \(k\) in \(a\) returns the index \(i\) if and only if \(i < n\), \(a_i = k\), and \(a_j < k\) for every \(j < i\).

theorem binarySearchFirst?_eq_some_iff (xs : Array α) (key : α)
    (hs : xs.Pairwise (fun x y => x ≤ y)) (i : Nat) :
    (binarySearchFirst? xs key).ret = some i ↔
      ∃ hi : i < xs.size,
        xs[i] = key ∧
          ∀ j (_hj : j < i) (_hjs : j < xs.size), xs[j] < key
Uses 3 · Used by 1
Statement usesBinary search for the first occurrence
Proof usesLower-bound search · Correctness of lower-bound search
Used byBinary search reports absence exactly when the key is absent

TheoremBinary search reports absence exactly when the key is absent#✓fully proved

Let \(a = (a_0, \dots, a_{n-1})\) be an array over a linearly ordered type, sorted in nondecreasing order, and let \(k\) be a key. Binary search for the first occurrence of \(k\) in \(a\) returns no index if and only if \(a_i \ne k\) for every \(i < n\).

theorem binarySearchFirst?_eq_none_iff (xs : Array α) (key : α)
    (hs : xs.Pairwise (fun x y => x ≤ y)) :
    (binarySearchFirst? xs key).ret = none ↔
      ∀ i (hi : i < xs.size), xs[i] ≠ key
Uses 4
Statement usesBinary search for the first occurrence
Proof usesBinary search returns the first occurrence of the key · Lower-bound search · Correctness of lower-bound search

TheoremExact comparison count of binary search for the first occurrence#✓fully proved

Let \(a\) be an array of length \(n\) over a linearly ordered type, let \(k\) be a key, and let \(\ell\) be the index returned by lower-bound search for \(k\) in \(a\). The number of element comparisons made by binary search for the first occurrence of \(k\) in \(a\) equals the number made by lower-bound search for \(k\) in \(a\), plus \(1\) if \(\ell < n\) and plus \(0\) otherwise.

theorem binarySearchFirst?_time (xs : Array α) (key : α) :
    (binarySearchFirst? xs key).time =
      (lowerBound xs key).time + if (lowerBound xs key).ret < xs.size then 1 else 0
Uses 2 · Used by 1
Statement usesBinary search for the first occurrence · Lower-bound search
Used byComparison bound for binary search for the first occurrence

TheoremComparison bound for binary search for the first occurrence#✓fully proved

For every array \(a\) of length \(n\) over a linearly ordered type and every key \(k\), binary search for the first occurrence of \(k\) in \(a\) makes at most \(\lceil \log_2 (n + 1) \rceil + 1\) element comparisons.

theorem binarySearchFirst?_time_le (xs : Array α) (key : α) :
    (binarySearchFirst? xs key).time ≤ Nat.clog 2 (xs.size + 1) + 1
Uses 4
Statement usesBinary search for the first occurrence
Proof usesExact comparison count of binary search for the first occurrence · Lower-bound search · Comparison bound for lower-bound search
15 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.