Suffix tree

DefinitionTerminated string#✓fully proved

For a list \(s = (s_0, \dots, s_{n-1})\) over \(\alpha\), the terminated string of \(s\) is the list \((\mathrm{some}\,s_0, \dots, \mathrm{some}\,s_{n-1}, \mathrm{none})\) over \(\mathrm{Option}\,\alpha\): every symbol of \(s\) tagged \(\mathrm{some}\), followed by the terminator \(\mathrm{none}\).

def terminated (s : List α) : List (Option α) :=
  s.map some ++ [none]

Used by 8

Used byLookup in the suffix tree returns starting indices · Suffix-tree search finds exactly the prefixes of suffixes · Lookup of a suffix returns its starting index · The stored keys of a suffix tree are its terminated suffixes · Terminated suffixes are distinct · The suffix tree stores one key per suffix · Suffix entries of a string · Suffixes of the terminated string

TheoremSuffixes of the terminated string#✓fully proved

For a list \(s\) over \(\alpha\) and a natural number \(i \le |s|\), removing the first \(i\) entries of the terminated string of \(s\) gives the suffix of \(s\) starting at index \(i\) with every symbol tagged \(\mathrm{some}\), followed by \(\mathrm{none}\).

theorem terminated_drop_eq_suffix_map (s : List α) {i : Nat} (hi : i ≤ s.length) :
    (terminated s).drop i = (SuffixArray.suffix s i).map some ++ [none]

Uses 2

Statement usesSuffix of a list at an index · Terminated string

DefinitionSuffix entries of a string#✓fully proved

For a list \(s = (s_0, \dots, s_{n-1})\) over \(\alpha\), let \(\hat s = (\mathrm{some}\,s_0, \dots, \mathrm{some}\,s_{n-1}, \mathrm{none})\) be its terminated string. The suffix entries of \(s\) are the list of pairs \((\hat s_{\ge i}, i)\) for \(i = 0, 1, \dots, n\) in increasing order, where \(\hat s_{\ge i}\) is \(\hat s\) with its first \(i\) entries removed: each nonempty suffix of \(\hat s\) paired with its starting index.

def suffixEntries (s : List α) : List (List (Option α) × Nat) :=
  (List.range (s.length + 1)).map (fun i => ((terminated s).drop i, i))

Uses 1 · Used by 6

Statement usesTerminated string

Used byLookup in the suffix tree returns starting indices · Suffix-tree search finds exactly the prefixes of suffixes · Lookup of a suffix returns its starting index · The stored keys of a suffix tree are its terminated suffixes · The suffix tree stores one key per suffix · Suffix tree

TheoremTerminated suffixes are distinct#✓fully proved

Let \(s\) be a list over \(\alpha\). The lists obtained from the terminated string of \(s\) by removing its first \(i\) symbols, for \(i\) ranging over \(0, 1, \ldots, |s|\), are pairwise distinct.

They are distinct because their lengths differ.

theorem nodup_terminated_drops (s : List α) :
    ((List.range (s.length + 1)).map (fun i => (terminated s).drop i)).Nodup

Uses 1 · Used by 2

Statement usesTerminated string

Used byLookup of a suffix returns its starting index · The suffix tree stores one key per suffix

DefinitionSuffix tree#✓fully proved

For a list \(s = (s_0, \dots, s_{n-1})\) over \(\alpha\), let \(\hat s = (\mathrm{some}\,s_0, \dots, \mathrm{some}\,s_{n-1}, \mathrm{none})\) be its terminated string over \(\mathrm{Option}\,\alpha\). The suffix tree of \(s\) is the radix trie with keys over \(\mathrm{Option}\,\alpha\) and natural-number values obtained from the empty trie by inserting, for \(i = n, n - 1, \dots, 0\) in this order, the suffix of \(\hat s\) starting at index \(i\) with value \(i\).

def suffixTree (s : List α) : RadixTrie (Option α) Nat :=
  RadixTrie.buildFrom (suffixEntries s)

Uses 3 · Used by 7

Statement usesRadix trie · Radix trie built from a list of key-value pairs · Suffix entries of a string

Used byLookup in the suffix tree returns starting indices · Suffix-tree search finds exactly the prefixes of suffixes · Suffix-tree search finds exactly the infixes · Lookup of a suffix returns its starting index · The stored keys of a suffix tree are its terminated suffixes · Stored keys of the suffix tree · The suffix tree stores one key per suffix

TheoremLookup of a suffix returns its starting index#✓fully proved

Let \(s\) be a list over \(\alpha\) and \(i\) a natural number with \(i \le |s|\). Looking up, in the suffix tree of \(s\), the terminated string of \(s\) with its first \(i\) symbols removed returns \(i\).

theorem lookup_suffix {s : List α} {i : Nat} (hi : i ≤ s.length) :
    (suffixTree s).lookup ((terminated s).drop i) = some i

Uses 6

Statement usesRadix trie lookup · Suffix tree · Terminated string

Proof usesLookup in a radix trie built from a list with distinct keys · Terminated suffixes are distinct · Suffix entries of a string

TheoremLookup in the suffix tree returns starting indices#✓fully proved

Let \(s\) be a list over \(\alpha\), let \(k\) be a list over \(\alpha\) extended by a fresh terminator symbol, and let \(i\) be a natural number. If looking up \(k\) in the suffix tree of \(s\) returns \(i\), then \(i \le |s|\) and \(k\) is the terminated string of \(s\) with its first \(i\) symbols removed.

theorem eq_drop_of_lookup_suffixTree {s : List α} {k : List (Option α)} {i : Nat}
    (h : (suffixTree s).lookup k = some i) :
    i ≤ s.length ∧ k = (terminated s).drop i

Uses 5

Statement usesRadix trie lookup · Suffix tree · Terminated string

Proof usesLookups in a radix trie built from a list come from the list · Suffix entries of a string

TheoremThe stored keys of a suffix tree are its terminated suffixes#✓fully proved

Let \(s\) be a list over \(\alpha\). A key \(k\) is stored in the suffix tree of \(s\) if and only if there is a natural number \(i \le |s|\) such that \(k\) is the terminated string of \(s\) with its first \(i\) symbols removed.

theorem mem_suffixTree_keys {s : List α} {k : List (Option α)} :
    k ∈ (suffixTree s).keys ↔ ∃ i ≤ s.length, k = (terminated s).drop i

Uses 7 · Used by 2

Statement usesStored keys of a radix trie · Suffix tree · Terminated string

Proof usesRadix trie · Radix trie built from a list of key-value pairs · Keys of a radix trie built from a list · Suffix entries of a string

Used bySuffix-tree search finds exactly the prefixes of suffixes · The suffix tree stores one key per suffix

DefinitionStored keys of the suffix tree#✓fully proved

For a list \(s\) over \(\alpha\), the stored keys of \(s\) form the list of keys stored in the suffix tree of \(s\), in stored sibling order.

They are exactly the terminated suffixes. This concerns stored keys, not structural trie leaves: a valid radix trie may carry values at internal nodes, and no leaf characterization is claimed.

def storedKeys (s : List α) : List (List (Option α)) :=
  (suffixTree s).keys

Uses 2 · Used by 1

Statement usesStored keys of a radix trie · Suffix tree

Used byThe suffix tree stores one key per suffix

TheoremThe suffix tree stores one key per suffix#✓fully proved

For a list \(s\) over \(\alpha\), the list of stored keys of the suffix tree of \(s\) has length \(|s| + 1\).

There is one key for each terminated suffix.

theorem storedKeys_length (s : List α) : (storedKeys s).length = s.length + 1

Uses 11

Statement usesStored keys of the suffix tree

Proof usesValid radix trie · The empty radix trie is valid · Insertion preserves validity of radix tries · Stored keys of a valid radix trie are distinct · Radix trie built from a list of key-value pairs · The stored keys of a suffix tree are its terminated suffixes · Terminated suffixes are distinct · Suffix entries of a string · Suffix tree · Terminated string

TheoremA tagged pattern cannot reach past the terminator#✓fully proved

For lists \(p\) and \(q\) over \(\alpha\), view their symbols in \(\alpha\) extended by a fresh terminator symbol. If \(p\) is a prefix of \(q\) followed by the terminator, then \(p\) is a prefix of \(q\).

The terminator differs from every symbol of \(\alpha\), so the pattern cannot reach past it.

theorem isPrefix_of_map_some_prefix_append_none {p q : List α} :
    (p.map some) <+: (q.map some ++ [none]) → p <+: q

Used by 1

Used bySuffix-tree search finds exactly the prefixes of suffixes

TheoremInfixes are prefixes of suffixes#✓fully proved

For lists \(s\) and \(p\), \(p\) is an infix (a contiguous sublist) of \(s\) if and only if there is a natural number \(i\) such that \(p\) is a prefix of the list obtained from \(s\) by removing its first \(i\) symbols.

theorem isInfix_iff_exists_isPrefix_drop {s p : List α} :
    p <:+: s ↔ ∃ i, p <+: s.drop i

Used by 1

Used bySuffix-tree search finds exactly the infixes

TheoremSuffix-tree search finds exactly the prefixes of suffixes#✓fully proved

For lists \(s\) and \(p\) over \(\alpha\), prefix search for \(p\) (each symbol viewed in the alphabet extended by the terminator) in the suffix tree of \(s\) succeeds if and only if there is a natural number \(i\) such that \(p\) is a prefix of the list obtained from \(s\) by removing its first \(i\) symbols.

theorem hasPrefix_suffixTree_iff_exists {s p : List α} :
    (suffixTree s).hasPrefix (p.map some) = true ↔ ∃ i, p <+: s.drop i

Uses 12 · Used by 1

Statement usesPrefix search in a radix trie · Suffix tree

Proof usesValid radix trie · The empty radix trie is valid · Insertion preserves validity of radix tries · Radix trie built from a list of key-value pairs · Prefix search is correct on valid radix tries · Stored keys of a radix trie · A tagged pattern cannot reach past the terminator · The stored keys of a suffix tree are its terminated suffixes · Suffix entries of a string · Terminated string

Used bySuffix-tree search finds exactly the infixes

TheoremSuffix-tree search finds exactly the infixes#✓fully proved

For lists \(s\) and \(p\) over \(\alpha\), prefix search for \(p\) (each symbol viewed in the alphabet extended by the terminator) in the suffix tree of \(s\) succeeds if and only if \(p\) occurs in \(s\) as a contiguous sublist (an infix).

theorem hasPrefix_suffixTree_iff_isInfix {s p : List α} :
    (suffixTree s).hasPrefix (p.map some) = true ↔ p <:+: s

Uses 4

Statement usesPrefix search in a radix trie · Suffix tree

Proof usesSuffix-tree search finds exactly the prefixes of suffixes · Infixes are prefixes of suffixes

14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.