Burrows–Wheeler transform and FM-index

DefinitionText with an appended sentinel#✓fully proved

The text t with the sentinel ⊥ appended: t.map (↑) ++ [⊥]. The sentinel is the unique occurrence of ⊥ and is smaller than every letter.

def withSentinel {α : Type*} (t : List α) : List (WithBot α) := t.map (↑) ++ [⊥]

Used by 20

Used byCounting occurrences · Backward-search intervals are suffix-array intervals · Backward search is correct · Burrows–Wheeler transform · The transform from the suffix array · Inversion · Length of the Burrows–Wheeler transform · 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 · Rows of the Burrows–Wheeler matrix are sorted · Rotations of t$ compare as suffixes · Sorted rotations of a sentinel-terminated text · The Burrows–Wheeler matrix is the suffix array of t$ · The LF-mapping property · The LF step moves one position left in the text · LF in suffix-array terms

DefinitionSorted rotations of a sentinel-terminated text#✓fully proved

The starting positions 0, …, |t| of the rotations of withSentinel t, sorted by their rotations in lexicographic order: row r of the Burrows–Wheeler matrix is (withSentinel t).rotate ((sortedRotations t)[r]).

def sortedRotations {α : Type*} [LinearOrder α] (t : List α) : List ℕ :=
  (List.range (t.length + 1)).mergeSort
    (fun i j => decide ((withSentinel t).rotate i ≤ (withSentinel t).rotate j))

Uses 1 · Used by 14

Statement usesText with an appended sentinel

Used byCounting occurrences · Backward-search intervals are suffix-array intervals · Backward search is correct · Burrows–Wheeler transform · The transform from the suffix array · Inversion · Length of the Burrows–Wheeler transform · Sampled-suffix-array locate is correct · The reported positions are exactly the occurrences · Number of FM-index occurrences equals the interval length · Rows of the Burrows–Wheeler matrix are sorted · The Burrows–Wheeler matrix is the suffix array of t$ · The LF-mapping property · LF in suffix-array terms

DefinitionBurrows–Wheeler transform#✓fully proved

The Burrows–Wheeler transform: the last column of the sorted rotation matrix.

def bwt {α : Type*} [LinearOrder α] (t : List α) : List (WithBot α) :=
  (sortedRotations t).map fun i => ((withSentinel t).rotate i).getLastD ⊥

Uses 2 · Used by 15

Statement usesSorted rotations of a sentinel-terminated text · Text with an appended sentinel

Used byCounting occurrences · Backward-search intervals are suffix-array intervals · Backward search is correct · The transform from the suffix array · Inversion · Length of the Burrows–Wheeler transform · 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 LF-mapping property · The LF step moves one position left in the text · LF in suffix-array terms

DefinitionCount of smaller letters in the FM-index#✓fully proved

C[c]: the number of letters of L smaller than c.

def countLess {α : Type*} [LinearOrder α] (L : List (WithBot α)) (c : WithBot α) : ℕ :=
  L.countP (· < c)

Used by 5

Used byFM-index backward search · Backward search returns a genuine row interval · Backward search is correct · LF-mapping from the last column · The LF-mapping property

DefinitionRank of a letter in a prefix of the last column#✓fully proved

rank_c(L, r): the number of occurrences of c among the first r letters of L.

def rank {α : Type*} [LinearOrder α] (L : List (WithBot α)) (c : WithBot α) (r : ℕ) : ℕ :=
  (L.take r).count c

Used by 5

Used byFM-index backward search · Backward search returns a genuine row interval · Backward search is correct · LF-mapping from the last column · The LF-mapping property

DefinitionLF-mapping from the last column#✓fully proved

The LF-mapping computed from the last column alone: LF(r) = C[L[r]] + rank_{L[r]}(L, r).

def lf {α : Type*} [LinearOrder α] (L : List (WithBot α)) (r : ℕ) : ℕ :=
  countLess L (L.getD r ⊥) + rank L (L.getD r ⊥) r

Uses 2 · Used by 10

Statement usesCount of smaller letters in the FM-index · Rank of a letter in a prefix of the last column

Used byBackward search is correct · Steps of the Burrows–Wheeler inversion walk · Inversion · Step-bounded sampled-suffix-array locate · Sampled-suffix-array locate is correct · Number of LF steps taken by sampled locate · Locate takes at most s - 1 steps · The LF-mapping property · The LF step moves one position left in the text · LF in suffix-array terms

DefinitionSteps of the Burrows–Wheeler inversion walk#✓fully proved

k steps of the inversion walk from row r: the letters L[r], L[LF r], ….

def invertAux {α : Type*} [LinearOrder α] (L : List (WithBot α)) : ℕ → ℕ → List (WithBot α)
  | 0, _ => []
  | k + 1, r => L.getD r ⊥ :: invertAux L k (lf L r)

Uses 1 · Used by 2

Statement usesLF-mapping from the last column

Used byInversion of the Burrows–Wheeler transform · Inversion

DefinitionInversion of the Burrows–Wheeler transform#✓fully proved

Inversion of the Burrows–Wheeler transform: walk the LF-mapping |L| - 1 times from row 0 (the rotation that starts with the sentinel) and reverse the letters read.

def invert {α : Type*} [LinearOrder α] (L : List (WithBot α)) : List (WithBot α) :=
  (invertAux L (L.length - 1) 0).reverse

Uses 1 · Used by 1

Statement usesSteps of the Burrows–Wheeler inversion walk

Used byInversion

TheoremLength of the Burrows–Wheeler transform#✓fully proved

The Burrows–Wheeler transform of t has length |t| + 1 (the sentinel adds one letter).

theorem length_bwt {α : Type*} [LinearOrder α] (t : List α) :
    (bwt t).length = t.length + 1

Uses 3 · Used by 4

Statement usesBurrows–Wheeler transform

Proof usesSorted rotations of a sentinel-terminated text · Text with an appended sentinel

Used byCounting occurrences · Backward search is correct · Inversion · The LF-mapping property

TheoremThe sentinel stops every prefix match#✓fully proved

A sentinel-free word P is a prefix of u ++ ⊥ :: v (letters lifted to WithBot α) exactly when it is a prefix of u: the sentinel ⊥ stops every match.

theorem map_coe_prefix_append_bot_cons_iff {α : Type*} (P u : List α)
    (v : List (WithBot α)) :
    P.map (↑) <+: u.map (↑) ++ ⊥ :: v ↔ P <+: u

Used by 1

Used byCounting occurrences

TheoremRows of the Burrows–Wheeler matrix are sorted#✓fully proved

The rows of the Burrows–Wheeler matrix are sorted: the rotations listed by sortedRotations t are in lexicographically nondecreasing order.

theorem pairwise_sortedRotations {α : Type*} [LinearOrder α] (t : List α) :
    (sortedRotations t).Pairwise
      (fun i j => (withSentinel t).rotate i ≤ (withSentinel t).rotate j)

Uses 2 · Used by 2

Statement usesSorted rotations of a sentinel-terminated text · Text with an appended sentinel

Used byInversion · The LF-mapping property

TheoremThe LF-mapping property#✓fully proved

For every row r, row lf (bwt t) r holds the rotation of row r rotated right by one position, i.e. starting one position earlier in the text.

theorem sortedRotations_getD_lf {α : Type*} [LinearOrder α] (t : List α) (r : ℕ)
    (hr : r < t.length + 1) :
    lf (bwt t) r < t.length + 1 ∧
      (sortedRotations t).getD (lf (bwt t) r) 0 =
        ((sortedRotations t).getD r 0 + t.length) % (t.length + 1)

Uses 8 · Used by 3

Statement usesBurrows–Wheeler transform · LF-mapping from the last column · Sorted rotations of a sentinel-terminated text

Proof usesCount of smaller letters in the FM-index · Length of the Burrows–Wheeler transform · Rows of the Burrows–Wheeler matrix are sorted · Rank of a letter in a prefix of the last column · Text with an appended sentinel

Used byBackward search is correct · Inversion · LF in suffix-array terms

TheoremInversion#✓fully proved

The Burrows–Wheeler transform is inverted by the LF-mapping walk.

theorem invert_bwt {α : Type*} [LinearOrder α] (t : List α) : invert (bwt t) = t.map (↑)

Uses 9

Statement usesBurrows–Wheeler transform · Inversion of the Burrows–Wheeler transform

Proof usesSteps of the Burrows–Wheeler inversion walk · Length of the Burrows–Wheeler transform · LF-mapping from the last column · Rows of the Burrows–Wheeler matrix are sorted · Sorted rotations of a sentinel-terminated text · The LF-mapping property · Text with an appended sentinel

DefinitionFM-index backward search#✓fully proved

FM-index backward search: the half-open row interval [sp, ep) for a pattern, computed from the last column alone, processing the pattern from its last letter to its first. The interval for the suffix and C[c] are each computed once per letter, so a pattern of length m makes m recursive calls.

def backwardSearch {α : Type*} [LinearOrder α] (L : List (WithBot α)) : List α → ℕ × ℕ
  | [] => (0, L.length)
  | c :: P =>
      let r := backwardSearch L P
      let base := countLess L c
      (base + rank L c r.1, base + rank L c r.2)

Uses 2 · Used by 8

Statement usesCount of smaller letters in the FM-index · Rank of a letter in a prefix of the last column

Used byBackward search returns a genuine row interval · Counting occurrences · Backward-search intervals are suffix-array intervals · Backward search is correct · 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

TheoremBackward search returns a genuine row interval#✓fully proved

Backward search always returns a genuine interval of rows, sp ≤ ep ≤ |L|, on any list L (so the difference in backwardSearch_count involves no truncated subtraction).

theorem backwardSearch_bounds {α : Type*} [LinearOrder α]
    (L : List (WithBot α)) (P : List α) :
    (backwardSearch L P).1 ≤ (backwardSearch L P).2 ∧
      (backwardSearch L P).2 ≤ L.length

Uses 3 · Used by 3

Statement usesFM-index backward search

Proof usesCount of smaller letters in the FM-index · Rank of a letter in a prefix of the last column

Used byCounting occurrences · The reported positions are exactly the occurrences · Number of FM-index occurrences equals the interval length

TheoremBackward search is correct#✓fully proved

After processing P, the interval [sp, ep) is exactly the set of rows whose rotation starts with P.

theorem backwardSearch_spec {α : Type*} [LinearOrder α] (t P : List α) (r : ℕ)
    (hr : r < t.length + 1) :
    (backwardSearch (bwt t) P).1 ≤ r ∧ r < (backwardSearch (bwt t) P).2 ↔
      P.map (↑) <+: (withSentinel t).rotate ((sortedRotations t).getD r 0)

Uses 9 · Used by 2

Statement usesFM-index backward search · Burrows–Wheeler transform · Sorted rotations of a sentinel-terminated text · Text with an appended sentinel

Proof usesCount of smaller letters in the FM-index · Length of the Burrows–Wheeler transform · LF-mapping from the last column · Rank of a letter in a prefix of the last column · The LF-mapping property

Used byCounting occurrences · Backward-search intervals are suffix-array intervals

TheoremCounting occurrences#✓fully proved

ep - sp is the number of positions i ≤ |t| at which P occurs in t.

theorem backwardSearch_count {α : Type*} [LinearOrder α] (t P : List α) :
    (backwardSearch (bwt t) P).2 - (backwardSearch (bwt t) P).1 =
      (List.range (t.length + 1)).countP (fun i => P <+: t.drop i)

Uses 8

Statement usesFM-index backward search · Burrows–Wheeler transform

Proof usesBackward search returns a genuine row interval · Backward search is correct · Length of the Burrows–Wheeler transform · The sentinel stops every prefix match · Sorted rotations of a sentinel-terminated text · Text with an appended sentinel

TheoremRotations of t$ compare as suffixes#✓fully proved

For i, j ≤ |t|, rotation i of withSentinel t is smaller than rotation j exactly when suffix i is smaller than suffix j.

theorem rotate_lt_rotate_iff (t : List α) {i j : ℕ} (hi : i ≤ t.length) (hj : j ≤ t.length) :
    (withSentinel t).rotate i < (withSentinel t).rotate j ↔
      suffix (withSentinel t) i < suffix (withSentinel t) j

Uses 2 · Used by 1

Statement usesSuffix of a list at an index · Text with an appended sentinel

Used byThe Burrows–Wheeler matrix is the suffix array of t$

TheoremThe Burrows–Wheeler matrix is the suffix array of t$#✓fully proved

Sorting the rotations of withSentinel t orders the starting positions exactly as sorting its suffixes.

theorem sortedRotations_eq_suffixArray (t : List α) :
    sortedRotations t = suffixArray (withSentinel t)

Uses 7 · Used by 3

Statement usesSuffix array · Sorted rotations of a sentinel-terminated text · Text with an appended sentinel

Proof usesThe suffix array sorts the suffixes · Suffix of a list at an index · The suffix array is a permutation of the indices · Rotations of t$ compare as suffixes

Used byBackward-search intervals are suffix-array intervals · The transform from the suffix array · LF in suffix-array terms

TheoremThe transform from the suffix array#✓fully proved

bwt[r] = t$[SA[r] - 1], the letter cyclically before the suffix of row r (the sentinel for the row of the whole text, SA[r] = 0).

theorem bwt_eq_map_suffixArray (t : List α) :
    bwt t = (suffixArray (withSentinel t)).map
      fun i => (withSentinel t).getD ((i + t.length) % (t.length + 1)) ⊥

Uses 6

Statement usesSuffix array · Burrows–Wheeler transform · Text with an appended sentinel

Proof usesThe suffix array is a permutation of the indices · Sorted rotations of a sentinel-terminated text · The Burrows–Wheeler matrix is the suffix array of t$

TheoremBackward-search intervals are suffix-array intervals#✓fully proved

Row r ≤ |t| lies in the interval [sp, ep) computed by backward search on bwt t exactly when P is a prefix of the suffix of t at position SA[r].

theorem backwardSearch_iff_prefix (t P : List α) (r : ℕ) (hr : r < t.length + 1) :
    (backwardSearch (bwt t) P).1 ≤ r ∧ r < (backwardSearch (bwt t) P).2 ↔
      P <+: t.drop ((suffixArray (withSentinel t)).getD r 0)

Uses 8 · Used by 1

Statement usesSuffix array · FM-index backward search · Burrows–Wheeler transform · Text with an appended sentinel

Proof usesThe suffix array is a permutation of the indices · Backward search is correct · Sorted rotations of a sentinel-terminated text · The Burrows–Wheeler matrix is the suffix array of t$

Used byThe reported positions are exactly the occurrences

DefinitionOccurrences of a pattern reported by the FM-index#✓fully proved

The occurrences of P reported by the FM-index: the suffix-array entries SA[sp], …, SA[ep - 1] of the backward-search interval. The BWT and the interval are bound once with let and reused, so one query builds the BWT and runs the backward search once, not three times.

def occurrences (t P : List α) : List ℕ :=
  let L := bwt t
  let interval := backwardSearch L P
  ((suffixArray (withSentinel t)).drop interval.1).take (interval.2 - interval.1)

Uses 4 · Used by 3

Statement usesSuffix array · FM-index backward search · Burrows–Wheeler transform · Text with an appended sentinel

Used byThe reported positions are exactly the occurrences · Number of FM-index occurrences equals the interval length · FM-index reports each occurrence once

TheoremThe reported positions are exactly the occurrences#✓fully proved

i is reported for P exactly when i ≤ |t| and P is a prefix of t.drop i (the empty pattern occurs at all |t| + 1 positions).

theorem mem_occurrences_iff (t P : List α) (i : ℕ) :
    i ∈ occurrences t P ↔ i ≤ t.length ∧ P <+: t.drop i

Uses 9

Statement usesOccurrences of a pattern reported by the FM-index

Proof usesSuffix array · The suffix array is a permutation of the indices · FM-index backward search · Backward search returns a genuine row interval · Burrows–Wheeler transform · Sorted rotations of a sentinel-terminated text · Text with an appended sentinel · Backward-search intervals are suffix-array intervals

TheoremFM-index reports each occurrence once#✓fully proved

Each occurrence is reported once.

theorem occurrences_nodup (t P : List α) : (occurrences t P).Nodup

Uses 6

Statement usesOccurrences of a pattern reported by the FM-index

Proof usesSuffix array · The suffix array is a permutation of the indices · FM-index backward search · Burrows–Wheeler transform · Text with an appended sentinel

TheoremNumber of FM-index occurrences equals the interval length#✓fully proved

The number of reported positions is the length ep - sp of the backward-search interval.

theorem occurrences_length (t P : List α) :
    (occurrences t P).length = (backwardSearch (bwt t) P).2 - (backwardSearch (bwt t) P).1

Uses 8

Statement usesFM-index backward search · Burrows–Wheeler transform · Occurrences of a pattern reported by the FM-index

Proof usesSuffix array · The suffix array is a permutation of the indices · Backward search returns a genuine row interval · Sorted rotations of a sentinel-terminated text · Text with an appended sentinel

TheoremLF in suffix-array terms#✓fully proved

For a row r ≤ |t|, LF r is a row and SA[LF r] = SA[r] - 1 cyclically (SA[LF r] = |t| when SA[r] = 0).

theorem suffixArray_getD_lf (t : List α) (r : ℕ) (hr : r < t.length + 1) :
    lf (bwt t) r < t.length + 1 ∧
      (suffixArray (withSentinel t)).getD (lf (bwt t) r) 0 =
        ((suffixArray (withSentinel t)).getD r 0 + t.length) % (t.length + 1)

Uses 7 · Used by 3

Statement usesSuffix array · Burrows–Wheeler transform · LF-mapping from the last column · Text with an appended sentinel

Proof usesSorted rotations of a sentinel-terminated text · The LF-mapping property · The Burrows–Wheeler matrix is the suffix array of t$

Used bySampled-suffix-array locate is correct · Locate takes at most s - 1 steps · The LF step moves one position left in the text

TheoremThe LF step moves one position left in the text#✓fully proved

SA[r] = SA[LF r] + 1 when SA[r] > 0.

theorem suffixArray_getD_eq_lf_add_one (t : List α) (r : ℕ) (hr : r < t.length + 1)
    (hpos : 0 < (suffixArray (withSentinel t)).getD r 0) :
    (suffixArray (withSentinel t)).getD r 0 =
      (suffixArray (withSentinel t)).getD (lf (bwt t) r) 0 + 1

Uses 6 · Used by 2

Statement usesSuffix array · Burrows–Wheeler transform · LF-mapping from the last column · Text with an appended sentinel

Proof usesThe suffix array is a permutation of the indices · LF in suffix-array terms

Used bySampled-suffix-array locate is correct · Locate takes at most s - 1 steps

DefinitionStep-bounded sampled-suffix-array locate#✓fully proved

k steps of sampled-suffix-array locate from row r: return the stored value of the first sampled row reached along the LF-mapping, plus the number of LF steps taken. sample r is the stored value SA[r] of row r, if any.

def locateAux (L : List (WithBot α)) (sample : ℕ → Option ℕ) : ℕ → ℕ → ℕ
  | 0, r => (sample r).getD 0
  | k + 1, r =>
    match sample r with
    | some v => v
    | none => locateAux L sample k (lf L r) + 1

Uses 1 · Used by 2

Statement usesLF-mapping from the last column

Used bySampled-suffix-array locate · Sampled-suffix-array locate is correct

DefinitionSampled-suffix-array locate#✓fully proved

Sampled-suffix-array locate (Ferragina and Manzini 2000): the text position of row r from the last column L and the samples, with at most |L| LF steps.

def locate (L : List (WithBot α)) (sample : ℕ → Option ℕ) (r : ℕ) : ℕ :=
  locateAux L sample L.length r

Uses 1 · Used by 1

Statement usesStep-bounded sampled-suffix-array locate

Used bySampled-suffix-array locate is correct

DefinitionNumber of LF steps taken by sampled locate#✓fully proved

The number of LF steps locateAux L sample k r takes.

def locateSteps (L : List (WithBot α)) (sample : ℕ → Option ℕ) : ℕ → ℕ → ℕ
  | 0, _ => 0
  | k + 1, r =>
    match sample r with
    | some _ => 0
    | none => locateSteps L sample k (lf L r) + 1

Uses 1 · Used by 1

Statement usesLF-mapping from the last column

Used byLocate takes at most s - 1 steps

TheoremSampled-suffix-array locate is correct#✓fully proved

If every stored value is correct (sample r = some v → v = SA[r] for rows r ≤ |t|) and every row of text position 0 is sampled, then locate returns SA[r] for every row r ≤ |t|.

theorem locate_eq (t : List α) (sample : ℕ → Option ℕ)
    (hsound : ∀ r v, r < t.length + 1 → sample r = some v →
      v = (suffixArray (withSentinel t)).getD r 0)
    (hzero : ∀ r, r < t.length + 1 → (suffixArray (withSentinel t)).getD r 0 = 0 →
      (sample r).isSome)
    (r : ℕ) (hr : r < t.length + 1) :
    locate (bwt t) sample r = (suffixArray (withSentinel t)).getD r 0

Uses 10

Statement usesSuffix array · Burrows–Wheeler transform · Text with an appended sentinel · Sampled-suffix-array locate

Proof usesThe suffix array is a permutation of the indices · LF-mapping from the last column · Sorted rotations of a sentinel-terminated text · Step-bounded sampled-suffix-array locate · The LF step moves one position left in the text · LF in suffix-array terms

TheoremLocate takes at most s - 1 steps#✓fully proved

For 0 < s, if every row whose text position is a multiple of s is sampled, then from row r ≤ |t| locate makes at most SA[r] mod s LF steps (for any amount of fuel k). At s = 0 the s - 1 bound would be 0 while the proof only gives SA[r] mod 0 = SA[r] steps.

theorem locateSteps_le (t : List α) (sample : ℕ → Option ℕ) (s : ℕ) (_hs : 0 < s)
    (hsample : ∀ r, r < t.length + 1 → (suffixArray (withSentinel t)).getD r 0 % s = 0 →
      (sample r).isSome) :
    ∀ k r, r < t.length + 1 →
      locateSteps (bwt t) sample k r ≤ (suffixArray (withSentinel t)).getD r 0 % s

Uses 7

Statement usesSuffix array · Burrows–Wheeler transform · Text with an appended sentinel · Number of LF steps taken by sampled locate

Proof usesLF-mapping from the last column · The LF step moves one position left in the text · LF in suffix-array terms

32 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.