Suffix array

DefinitionSuffix of a list at an index#✓fully proved

For a list \(s = (s_0, \dots, s_{n-1})\) over a linearly ordered alphabet and a natural number \(i\), the suffix of \(s\) at \(i\) is the list obtained from \(s\) by dropping its first \(i\) entries: it is \((s_i, \dots, s_{n-1})\) when \(i < n\) and the empty list when \(i \ge n\).

def suffix (s : List α) (i : Nat) : List α :=
  s.drop i

Used by 11

Used byLongest-common-prefix lengths of adjacent suffixes · The suffix array sorts the suffixes · The occurrences of a pattern are contiguous in the suffix array · Truncated suffix of a suffix-array row · Suffix-array search returns a valid row interval · Suffix-array search is correct · Suffix array · The suffix array is a permutation of the indices · Suffixes of the terminated string · Rotations of t$ compare as suffixes · The Burrows–Wheeler matrix is the suffix array of t$

DefinitionSuffixes of a list#✓fully proved

For a list \(s\) of length \(n\) over a linearly ordered alphabet, the list of suffixes of \(s\) is the list, for \(i = 0, 1, \dots, n\) in this order, of the lists obtained from \(s\) by dropping its first \(i\) entries. It starts with \(s\) itself and ends with the empty list.

def suffixes (s : List α) : List (List α) :=
  s.tails

DefinitionSuffix array#✓fully proved

For a list \(s\) of length \(n\) over a linearly ordered alphabet, the suffix array of \(s\) is the list of the indices \(0, 1, \dots, n - 1\), sorted so that the suffixes of \(s\) starting at them appear in lexicographic order.

Distinct indices below \(n\) give suffixes of different lengths, so these suffixes are pairwise distinct and the sorted order is unique.

def suffixArray (s : List α) : List Nat :=
  (List.range s.length).mergeSort (fun i j => decide (suffix s i ≤ suffix s j))

Uses 1 · Used by 18

Statement usesSuffix of a list at an index

Used byThe LCP array · The suffix array sorts the suffixes · The occurrences of a pattern are contiguous in the suffix array · Suffix-array search for a pattern's row interval · Suffix-array search returns a valid row interval · Suffix-array search is correct · The suffix array is a permutation of the indices · Backward-search intervals are suffix-array intervals · The transform from the suffix array · Sampled-suffix-array locate is correct · Locate takes at most s - 1 steps · The reported positions are exactly the occurrences · Occurrences of a pattern reported by the FM-index · Number of FM-index occurrences equals the interval length · FM-index reports each occurrence once · The Burrows–Wheeler matrix is the suffix array of t$ · The LF step moves one position left in the text · LF in suffix-array terms

TheoremThe suffix array is a permutation of the indices#✓fully proved

For a list \(s\) of length \(n\) over a linearly ordered alphabet, the suffix array of \(s\) is a permutation of the list \(0, 1, \dots, n - 1\) of all indices below \(n\).

theorem suffixArray_perm (s : List α) :
    (suffixArray s).Perm (List.range s.length)

Uses 2 · Used by 11

Statement usesSuffix array

Proof usesSuffix of a list at an index

Used byThe occurrences of a pattern are contiguous in the suffix array · Suffix-array search returns a valid row interval · Suffix-array search is correct · Backward-search intervals are suffix-array intervals · The transform from the suffix array · Sampled-suffix-array locate is correct · The reported positions are exactly the occurrences · Number of FM-index occurrences equals the interval length · FM-index reports each occurrence once · The Burrows–Wheeler matrix is the suffix array of t$ · The LF step moves one position left in the text

TheoremThe suffix array sorts the suffixes#✓fully proved

For a list \(s\) over a linearly ordered alphabet, the suffixes of \(s\) taken in suffix-array order are sorted lexicographically: whenever an index \(i\) comes before an index \(j\) in the suffix array of \(s\), the suffix of \(s\) starting at \(i\) is lexicographically less than or equal to the suffix of \(s\) starting at \(j\).

theorem pairwise_suffix_suffixArray (s : List α) :
    List.Pairwise (· ≤ ·) ((suffixArray s).map (suffix s))

Uses 2 · Used by 4

Statement usesSuffix of a list at an index · Suffix array

Used byThe occurrences of a pattern are contiguous in the suffix array · Suffix-array search returns a valid row interval · Suffix-array search is correct · The Burrows–Wheeler matrix is the suffix array of t$

DefinitionLongest common prefix length#✓fully proved

For lists \(x\) and \(y\), \(\mathrm{lcp}(x, y)\) is the length of the longest common prefix of \(x\) and \(y\): the number of positions, counted from the start, at which \(x\) and \(y\) agree before they first differ or one of them ends.

Only equality of letters is tested, so no order on the alphabet is needed.

def lcp : List α → List α → Nat
  | [], _ => 0
  | _ :: _, [] => 0
  | a :: as, b :: bs => if a = b then lcp as bs + 1 else 0

Used by 4

Used byLongest-common-prefix lengths of adjacent suffixes · Characterization of the longest common prefix length · Common prefixes of every shorter length · Two lists agree on their longest common prefix

TheoremTwo lists agree on their longest common prefix#✓fully proved

For lists \(x\) and \(y\) over a type with decidable equality, let \(\operatorname{lcp}(x, y)\) be the length of their longest common prefix. Then the first \(\operatorname{lcp}(x, y)\) elements of \(x\) and the first \(\operatorname{lcp}(x, y)\) elements of \(y\) form the same list.

theorem take_lcp_eq (x y : List α) : x.take (lcp x y) = y.take (lcp x y)

Uses 1 · Used by 1

Statement usesLongest common prefix length

Used byCommon prefixes of every shorter length

TheoremCommon prefixes of every shorter length#✓fully proved

Let \(x\) and \(y\) be lists and let \(\mathrm{lcp}(x, y)\) be the length of their longest common prefix. For every natural number \(q \le \mathrm{lcp}(x, y)\), the first \(q\) elements of \(x\) and of \(y\) agree.

theorem take_eq_of_le_lcp {x y : List α} {q : Nat} (h : q ≤ lcp x y) :
    x.take q = y.take q

Uses 2 · Used by 1

Statement usesLongest common prefix length

Proof usesTwo lists agree on their longest common prefix

Used byCharacterization of the longest common prefix length

TheoremCharacterization of the longest common prefix length#✓fully proved

For lists \(x\) and \(y\), let \(\mathrm{lcp}(x, y)\) be the length of the longest common prefix of \(x\) and \(y\). For every natural number \(q\), we have \(q \le \mathrm{lcp}(x, y)\) if and only if \(q\) is at most the lengths of both \(x\) and \(y\) and the first \(q\) elements of \(x\) and of \(y\) agree.

In particular \(\mathrm{lcp}(x, y)\) is the largest such \(q\).

theorem le_lcp_iff {x y : List α} {q : Nat} :
    q ≤ lcp x y ↔ q ≤ min x.length y.length ∧ x.take q = y.take q

Uses 2

Statement usesLongest common prefix length

Proof usesCommon prefixes of every shorter length

DefinitionLongest-common-prefix lengths of adjacent suffixes#✓fully proved

For a list \(s\) and a list of indices \(i_0, i_1, \dots, i_k\), this is the list of length \(k\) whose \(t\)-th entry, for \(t < k\), is the length of the longest common prefix of the suffixes of \(s\) starting at \(i_t\) and at \(i_{t+1}\), where the suffix starting at an index at or past the end of \(s\) is the empty list. It has one entry per adjacent pair of indices, and it is empty for an empty index list.

def adjLcp (s : List α) : List Nat → List Nat
  | [] => []
  | [_] => []
  | i :: j :: rest => lcp (suffix s i) (suffix s j) :: adjLcp s (j :: rest)

Uses 2 · Used by 1

Statement usesLongest common prefix length · Suffix of a list at an index

Used byThe LCP array

DefinitionThe LCP array#✓fully proved

For a list \(s\) over a linearly ordered alphabet, the LCP array of \(s\) is the list of longest-common-prefix lengths of adjacent suffixes in suffix-array order: if the suffix array of \(s\) is \(i_0, i_1, \dots, i_k\), then the LCP array has length \(k\) and its \(t\)-th entry, for \(t < k\), is the length of the longest common prefix of the suffixes of \(s\) starting at \(i_t\) and at \(i_{t+1}\). It is empty when \(s\) is empty.

def lcpArray (s : List α) : List Nat :=
  adjLcp s (suffixArray s)

Uses 2

Statement usesLongest-common-prefix lengths of adjacent suffixes · Suffix array

TheoremPrefix classes are lexicographic intervals#✓fully proved

If x ≤ y ≤ z and P is a prefix of both x and z, then P is a prefix of y.

theorem prefix_of_le_of_le {β : Type*} [LinearOrder β] {P x y z : List β} (hxy : x ≤ y)
    (hyz : y ≤ z) (hx : P <+: x) (hz : P <+: z) : P <+: y

Used by 1

Used byThe occurrences of a pattern are contiguous in the suffix array

TheoremTruncation is monotone for the lexicographic order#✓fully proved

Truncation is monotone for the lexicographic order: x ≤ y → x.take m ≤ y.take m.

theorem take_le_take {β : Type*} [LinearOrder β] {x y : List β} (h : x ≤ y) (m : ℕ) :
    x.take m ≤ y.take m

Used by 2

Used bySuffix-array search returns a valid row interval · Suffix-array search is correct

TheoremThe occurrences of a pattern are contiguous in the suffix array#✓fully proved

If rows r₁ ≤ r₂ ≤ r₃ of the suffix array of s are in range and the suffixes of rows r₁ and r₃ start with P, so does the suffix of row r₂.

theorem prefix_suffixArray_of_le_of_le (s P : List α) {r₁ r₂ r₃ : ℕ} (h₁₂ : r₁ ≤ r₂)
    (h₂₃ : r₂ ≤ r₃) (h₃ : r₃ < s.length)
    (hp₁ : P <+: suffix s ((suffixArray s).getD r₁ 0))
    (hp₃ : P <+: suffix s ((suffixArray s).getD r₃ 0)) :
    P <+: suffix s ((suffixArray s).getD r₂ 0)

Uses 5

Statement usesSuffix of a list at an index · Suffix array

Proof usesThe suffix array sorts the suffixes · The suffix array is a permutation of the indices · Prefix classes are lexicographic intervals

DefinitionBinary search for the boundary of a predicate#✓fully proved

Binary search for the boundary of a predicate on [lo, hi): the first index at which p is false, assuming p holds on an initial segment of [lo, hi) (lowerBound_spec). Each call probes the midpoint and recurses on one half.

def lowerBound (p : ℕ → Bool) (lo hi : ℕ) : ℕ :=
  if h : lo < hi then
    if p ((lo + hi) / 2) then lowerBound p ((lo + hi) / 2 + 1) hi
    else lowerBound p lo ((lo + hi) / 2)
  else lo
termination_by hi - lo
decreasing_by all_goals omega

Used by 4

Used byBinary search is correct · Suffix-array search for a pattern's row interval · Suffix-array search returns a valid row interval · Suffix-array search is correct

DefinitionNumber of probes made by the binary search#✓fully proved

The number of probes lowerBound p lo hi makes.

def lowerBoundSteps (p : ℕ → Bool) (lo hi : ℕ) : ℕ :=
  if h : lo < hi then
    if p ((lo + hi) / 2) then lowerBoundSteps p ((lo + hi) / 2 + 1) hi + 1
    else lowerBoundSteps p lo ((lo + hi) / 2) + 1
  else 0
termination_by hi - lo
decreasing_by all_goals omega

Used by 1

Used byBinary search is logarithmic

TheoremBinary search is correct#✓fully proved

If p holds on an initial segment of [lo, hi) (whenever it holds at j, it holds at every i with lo ≤ i ≤ j), then lowerBound p lo hi is the end k of that segment: lo ≤ k ≤ hi, p holds on [lo, k) and fails on [k, hi).

theorem lowerBound_spec (p : ℕ → Bool) (lo hi : ℕ) (hlo : lo ≤ hi)
    (hmono : ∀ i j, lo ≤ i → i ≤ j → j < hi → p j = true → p i = true) :
    lo ≤ lowerBound p lo hi ∧ lowerBound p lo hi ≤ hi ∧
      (∀ i, lo ≤ i → i < lowerBound p lo hi → p i = true) ∧
      (∀ i, lowerBound p lo hi ≤ i → i < hi → p i = false)

Uses 1 · Used by 2

Statement usesBinary search for the boundary of a predicate

Used bySuffix-array search returns a valid row interval · Suffix-array search is correct

TheoremBinary search is logarithmic#✓fully proved

At most ⌊log₂ (hi - lo)⌋ + 1 probes, for any predicate.

theorem lowerBoundSteps_le (p : ℕ → Bool) (lo hi : ℕ) :
    lowerBoundSteps p lo hi ≤ Nat.log 2 (hi - lo) + 1

Uses 1

Statement usesNumber of probes made by the binary search

DefinitionTruncated suffix of a suffix-array row#✓fully proved

The suffix of row r of the (precomputed) suffix array sa of s, truncated to m letters: the key compared with the pattern during the search. sa is computed once by saSearch and passed in, so probes do not rebuild the suffix array.

def rowKey (sa : List ℕ) (s : List α) (m r : ℕ) : List α :=
  (suffix s (sa.getD r 0)).take m

Uses 1 · Used by 3

Statement usesSuffix of a list at an index

Used bySuffix-array search for a pattern's row interval · Suffix-array search returns a valid row interval · Suffix-array search is correct

DefinitionSuffix-array search for a pattern's row interval#✓fully proved

Suffix-array search (Manber and Myers 1993): the row interval [sp, ep) of the suffixes of s that start with P, found by two binary searches over the rows [0, |s|). The suffix array is computed once and shared by both searches.

def saSearch (s P : List α) : ℕ × ℕ :=
  let sa := suffixArray s
  (lowerBound (fun r => decide (rowKey sa s P.length r < P)) 0 s.length,
    lowerBound (fun r => decide (rowKey sa s P.length r ≤ P)) 0 s.length)

Uses 3 · Used by 2

Statement usesSuffix array · Binary search for the boundary of a predicate · Truncated suffix of a suffix-array row

Used bySuffix-array search returns a valid row interval · Suffix-array search is correct

TheoremSuffix-array search returns a valid row interval#✓fully proved

The search returns a genuine interval of rows: sp ≤ ep ≤ |s|.

theorem saSearch_bounds (s P : List α) :
    (saSearch s P).1 ≤ (saSearch s P).2 ∧ (saSearch s P).2 ≤ s.length

Uses 9

Statement usesSuffix-array search for a pattern's row interval

Proof usesThe suffix array sorts the suffixes · Suffix of a list at an index · Suffix array · The suffix array is a permutation of the indices · Binary search for the boundary of a predicate · Binary search is correct · Truncated suffix of a suffix-array row · Truncation is monotone for the lexicographic order

TheoremSuffix-array search is correct#✓fully proved

A row r < |s| lies in [sp, ep) exactly when the suffix of row r starts with P.

theorem saSearch_spec (s P : List α) (r : ℕ) (hr : r < s.length) :
    (saSearch s P).1 ≤ r ∧ r < (saSearch s P).2 ↔
      P <+: suffix s ((suffixArray s).getD r 0)

Uses 9

Statement usesSuffix of a list at an index · Suffix array · Suffix-array search for a pattern's row interval

Proof usesThe suffix array sorts the suffixes · The suffix array is a permutation of the indices · Binary search for the boundary of a predicate · Binary search is correct · Truncated suffix of a suffix-array row · Truncation is monotone for the lexicographic order

22 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.