Knuth–Morris–Pratt algorithm

11 fully proved

Time M

DefinitionKnuth–Morris–Pratt search#✓fully proved

For lists \(p\) (the pattern) and \(t\) (the text) over a type with a boolean equality, KMP search for \(p\) in \(t\) returns either a zero-based offset or no offset, together with a cost: the number of symbol comparisons it makes. If \(p\) is empty, it returns the offset \(0\) at cost \(0\). Otherwise it first builds the prefix table of \(p\), a list of entries each pairing a symbol with a failure value. The transition of a table from a state \(s\) on a symbol \(x\) is defined as follows. If \(s\) is less than the number of entries and \(x\) equals the symbol of entry \(s\) (counting from \(0\)), the result is \(s + 1\). Otherwise the result is \(0\) when \(s = 0\), and when \(s > 0\) it is the transition from the failure value of entry \(s - 1\) on \(x\). Starting from the empty table, each symbol \(x\) of \(p\) in turn is appended as a new entry, with failure value the transition of the current table on \(x\) from the state equal to its number of entries. The search then reads \(t\) from the left, starting in state \(0\) and moving to the transition of the table on each symbol read. The first time the state equals \(|p|\), after \(j\) symbols have been read, it returns the offset \(j - |p|\). If this never happens, it returns no offset. The cost counts every equality test between two symbols, both while the table is built and while \(t\) is scanned. List operations, array access and arithmetic cost nothing.

When the boolean equality is lawful, the returned offset is the least offset at which \(p\) occurs in \(t\), and no offset is returned exactly when \(p\) does not occur in \(t\).

public def kmpSearch [BEq α] (pattern text : List α) : TimeM Nat (Option Nat) :=
  match pattern with
  | [] => pure (some 0)
  | _ :: _ =>
      let table := timedBuildFrom default pattern
      let result := timedScan table.ret 0 0 text
      ⟨result.ret, table.time + result.time⟩

Used by 6

Used byKMP search agrees with the first-infix split · KMP finds no match exactly when no offset matches · KMP finds no match exactly when the pattern does not occur · KMP returns the first match · KMP search on the empty pattern · KMP search makes linearly many comparisons

Array

TheoremSize of the KMP prefix table#✓fully proved

For every pattern \(p\), the KMP prefix table of \(p\) has exactly as many entries as \(p\) has symbols, one for each symbol of \(p\).

@[simp]
theorem mkPrefixTable_size {α : Type u} [BEq α] (pattern : List α) :
    (mkPrefixTable pattern.toArray).size = pattern.length

Used by 1

Used byThe KMP failure function

TheoremThe KMP prefix table stores the pattern#✓fully proved

Each entry of the Knuth–Morris–Pratt prefix table is a pair consisting of a symbol and a failure length. For every type with a Boolean equality test and every list \(p\) over it, the list of first components of the entries of the prefix table built from \(p\), read in order, equals \(p\).

theorem mkPrefixTable_symbols {α : Type u} [BEq α] (pattern : List α) :
    (mkPrefixTable pattern.toArray).toArray.toList.map Prod.fst = pattern

Time M

TheoremKMP returns the first match#✓fully proved

Let \(p\) and \(t\) be lists over a type with a lawful boolean equality, and write \(|t|\) for the length of \(t\). For every natural number \(i\), KMP search for \(p\) in \(t\) returns the offset \(i\) if and only if \(p\) matches \(t\) at \(i\) and at no \(j < i\), where \(p\) matches \(t\) at \(i\) when \(i \le |t|\) and \(p\) is a prefix of the list obtained from \(t\) by dropping its first \(i\) elements.

theorem kmpSearch_eq_some_iff [BEq α] [LawfulBEq α]
    (pattern text : List α) (offset : Nat) :
    (kmpSearch pattern text).ret = some offset ↔
      Cslib.Algorithms.Lean.StringMatching.MatchAt pattern text offset ∧
        ∀ earlier < offset,
          ¬Cslib.Algorithms.Lean.StringMatching.MatchAt pattern text earlier

Uses 2 · Used by 1

Statement usesPattern match at an offset · Knuth–Morris–Pratt search

Used byKMP search agrees with the first-infix split

TheoremKMP finds no match exactly when no offset matches#✓fully proved

For lists \(p\) and \(t\) over a type with a lawful boolean equality, write \(|t|\) for the length of \(t\). KMP search for \(p\) in \(t\) returns no offset if and only if there is no natural number \(i\) at which \(p\) matches \(t\), where \(p\) matches \(t\) at \(i\) when \(i \le |t|\) and \(p\) is a prefix of the list obtained from \(t\) by dropping its first \(i\) elements.

theorem kmpSearch_eq_none_iff [BEq α] [LawfulBEq α]
    (pattern text : List α) :
    (kmpSearch pattern text).ret = none ↔
      ∀ offset, ¬Cslib.Algorithms.Lean.StringMatching.MatchAt pattern text offset

Uses 2 · Used by 1

Statement usesPattern match at an offset · Knuth–Morris–Pratt search

Used byKMP finds no match exactly when the pattern does not occur

TheoremKMP finds no match exactly when the pattern does not occur#✓fully proved

For lists \(p\) (the pattern) and \(t\) (the text) over a type with a lawful boolean equality, KMP search for \(p\) in \(t\) returns no offset if and only if \(p\) is not a contiguous sublist of \(t\), that is, there are no lists \(u\), \(v\) with \(t = u \, p \, v\) (concatenation).

theorem kmpSearch_eq_none_iff_not_isInfix [BEq α] [LawfulBEq α]
    (pattern text : List α) :
    (kmpSearch pattern text).ret = none ↔ ¬pattern.IsInfix text

Uses 4

Statement usesKnuth–Morris–Pratt search

Proof usesPattern match at an offset · A pattern occurs in a text iff it matches at some offset · KMP finds no match exactly when no offset matches

TheoremKMP search agrees with the first-infix split#✓fully proved

Let \(p\) and \(t\) be lists over a type with a lawful boolean equality, with \(p\) nonempty. Let the first-infix split of \(t\) by \(p\) be the pair \((u, v)\) with \(t = u \, p \, v\) (concatenation) and \(u\) as short as possible, or nothing if \(p\) does not occur in \(t\). Then the value returned by KMP search for \(p\) in \(t\) is the length of \(u\) if the split exists, and no offset otherwise.

theorem kmpSearch_eq_dropInfix?_map_length [BEq α] [LawfulBEq α]
    (pattern text : List α) (hpattern : pattern ≠ []) :
    (kmpSearch pattern text).ret =
      (List.dropInfix? text pattern).map fun result => result.1.length

Uses 3

Statement usesKnuth–Morris–Pratt search

Proof usesPattern match at an offset · KMP returns the first match

TheoremKMP search makes linearly many comparisons#✓fully proved

For any pattern \(p\) and text \(t\), lists over a type with a boolean equality, KMP search for \(p\) in \(t\) makes at most \(2|p| + 2|t|\) symbol comparisons in total, those made while building the prefix table included, where \(|p|\) and \(|t|\) are the lengths of \(p\) and \(t\).

theorem kmpSearch_time_le [BEq α] (pattern text : List α) :
    (kmpSearch pattern text).time ≤ 2 * pattern.length + 2 * text.length

Uses 1

Statement usesKnuth–Morris–Pratt search

Array

TheoremThe KMP failure function#✓fully proved

Let \(p\) be a pattern of length \(n\) over a type with a lawful boolean equality, and write \(p_{\lt k}\) for its prefix of length \(k\). Each entry of the KMP prefix table of \(p\) pairs a symbol of \(p\) with a failure value. For every \(q < n\), the failure value \(f\) of entry \(q\) (counting from \(0\)) is the length of the longest proper prefix of \(p_{\lt q+1}\) that is also a suffix of \(p_{\lt q+1}\): \(f \le q\), \(p_{\lt f}\) is a suffix of \(p_{\lt q+1}\), and every \(k \le q\) such that \(p_{\lt k}\) is a suffix of \(p_{\lt q+1}\) satisfies \(k \le f\).

theorem mkPrefixTable_failure_spec {α : Type u} [BEq α] [LawfulBEq α]
    (pattern : List α) (q : Nat) (hq : q < pattern.length) :
    let table := mkPrefixTable pattern.toArray
    let failure := (table.toArray[q]'(by
      change q < (mkPrefixTable pattern.toArray).size
      rw [mkPrefixTable_size]
      exact hq)).2
    failure ≤ q ∧
      (pattern.take failure).IsSuffix (pattern.take (q + 1)) ∧
      ∀ k, k ≤ q → (pattern.take k).IsSuffix (pattern.take (q + 1)) → k ≤ failure

Uses 1

Statement usesSize of the KMP prefix table

TheoremCorrectness of the KMP transition#✓fully proved

Let \(p\) be a pattern of length \(n\) over a type with a lawful boolean equality, and write \(p_{\lt k}\) for its prefix of length \(k\). Let \(c\) be a list, \(x\) a symbol, and \(cx\) the list \(c\) followed by \(x\). Suppose the state \(s \le n\) is the length of the longest prefix of \(p\) that is a suffix of \(c\): \(p_{\lt s}\) is a suffix of \(c\), and every \(k \le n\) such that \(p_{\lt k}\) is a suffix of \(c\) satisfies \(k \le s\). Then the state \(s'\) that the transition of the KMP prefix table of \(p\) produces from \(s\) on reading \(x\) is the length of the longest prefix of \(p\) that is a suffix of \(cx\): \(s' \le n\), \(p_{\lt s'}\) is a suffix of \(cx\), and every \(k \le n\) such that \(p_{\lt k}\) is a suffix of \(cx\) satisfies \(k \le s'\).

theorem mkPrefixTable_step_spec {α : Type u} [BEq α] [LawfulBEq α]
    (pattern consumed : List α) (x : α)
    (state : Fin ((mkPrefixTable pattern.toArray).size + 1))
    (hstate : state.val ≤ pattern.length ∧
      (pattern.take state.val).IsSuffix consumed ∧
      ∀ k, k ≤ pattern.length → (pattern.take k).IsSuffix consumed → k ≤ state.val) :
    let table := mkPrefixTable pattern.toArray
    let next := table.step x state
    next.val ≤ pattern.length ∧
      (pattern.take next.val).IsSuffix (consumed ++ [x]) ∧
      ∀ k, k ≤ pattern.length →
        (pattern.take k).IsSuffix (consumed ++ [x]) → k ≤ next.val

Time M

TheoremKMP search on the empty pattern#✓fully proved

For every text \(t\), KMP search for the empty pattern in \(t\) returns offset \(0\) at cost \(0\), that is, without any symbol comparisons.

@[simp]
theorem kmpSearch_nil_pattern [BEq α] (text : List α) :
    kmpSearch [] text = pure (some 0)

Uses 1

Statement usesKnuth–Morris–Pratt search

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.