Naive string matching

DefinitionNaive string matcher#✓fully proved

Let \(p = p_0 \cdots p_{m-1}\) be a pattern and \(t = t_0 \cdots t_{n-1}\) a text over an alphabet with a Boolean equality test. If \(m \le n\), the naive matcher handles the shifts \(s = 0, 1, \dots, n - m\) in turn: it compares \(p_i\) with \(t_{s+i}\) for \(i = 0, 1, \dots\) until a comparison fails or all \(m\) symbols are compared, and it reports \(s\) if no comparison failed. It returns the reported shifts in the order found, with cost the total number of symbol comparisons executed, failed comparisons included. If \(m > n\), it reports no shift at cost \(0\).

public def naiveMatches [BEq α] (pattern text : List α) : TimeM Nat (List Nat) :=
  if pattern.length ≤ text.length then
    timedScan pattern (text.tails.take (text.length - pattern.length + 1)) 0
  else
    pure []

Used by 17

Used byBoyer–Moore agrees with the naive matcher · Correctness of naive string matching · Naive matching with the empty pattern · Naive matching with a pattern longer than the text · Naive matching reports shifts in increasing order · Output of naive matching · Naive matching on a repeated symbol reports every shift · Exact comparison count of naive matching · Upper bound on the comparisons of naive matching · Comparison count of naive matching on a repeated symbol · Correctness of Rabin–Karp matching · Rabin–Karp matching with the empty pattern · Rabin–Karp matching with a pattern longer than the text · Rabin–Karp reports offsets in increasing order · Rabin–Karp and naive matching return the same offsets · Rabin–Karp offsets on repeated-symbol words · Correctness of the finite-automaton matcher

TheoremOutput of naive matching#✓fully proved

Let \(p\) be a pattern of length \(m\) and \(t\) a text of length \(n\). If \(m \le n\), the list of shifts reported by the naive matcher on \(p\) and \(t\) is the increasing list of all \(s \in \{0, \dots, n - m\}\) such that \(p\) is a prefix of the suffix of \(t\) starting at the zero-based position \(s\), with symbols compared by the Boolean equality of the alphabet. If \(m > n\), the list is empty.

theorem naiveMatches_ret [BEq α] (pattern text : List α) :
    (naiveMatches pattern text).ret =
      if pattern.length ≤ text.length then
        (text.tails.take (text.length - pattern.length + 1)).findIdxs pattern.isPrefixOf
      else []

Uses 1 · Used by 5

Statement usesNaive string matcher

Used byCorrectness of naive string matching · Naive matching with the empty pattern · Naive matching reports shifts in increasing order · Naive matching on a repeated symbol reports every shift · Rabin–Karp and naive matching return the same offsets

TheoremCorrectness of naive string matching#✓fully proved

Let \(\alpha\) be a type whose Boolean equality agrees with equality, and write \(|t|\) for the length of a list \(t\). For every pattern \(p\) and text \(t\) over \(\alpha\) and every natural number \(s\), the naive matcher run on \(p\) and \(t\) reports the shift \(s\) if and only if \(p\) matches \(t\) at \(s\), that is, \(s \le |t|\) and \(p\) is a prefix of the suffix of \(t\) obtained by dropping its first \(s\) symbols.

In particular, the empty pattern is reported at every shift \(s \le |t|\).

theorem mem_naiveMatches_iff [BEq α] [LawfulBEq α] (pattern text : List α) (offset : Nat) :
    offset ∈ (naiveMatches pattern text).ret ↔
      Cslib.Algorithms.Lean.StringMatching.MatchAt pattern text offset

Uses 3 · Used by 3

Statement usesPattern match at an offset · Naive string matcher

Proof usesOutput of naive matching

Used byBoyer–Moore agrees with the naive matcher · Correctness of Rabin–Karp matching · Correctness of the finite-automaton matcher

TheoremNaive matching reports shifts in increasing order#✓fully proved

For every pattern \(p\) and text \(t\), the list of shifts reported by the naive matcher on \(p\) and \(t\) is strictly increasing; in particular, no shift is reported twice.

theorem naiveMatches_pairwise [BEq α] (pattern text : List α) :
    (naiveMatches pattern text).ret.Pairwise (· < ·)

Uses 2 · Used by 3

Statement usesNaive string matcher

Proof usesOutput of naive matching

Used byBoyer–Moore agrees with the naive matcher · Rabin–Karp reports offsets in increasing order · Correctness of the finite-automaton matcher

TheoremExact comparison count of naive matching#✓fully proved

Let \(p = p_0 \cdots p_{m-1}\) be a pattern and \(t = t_0 \cdots t_{n-1}\) a text. If \(m \le n\), the number of symbol comparisons performed by the naive matcher on \(p\) and \(t\) is

\[\sum_{s=0}^{n-m} \min(m, k_s + 1),\]

where \(k_s\) is the least \(i < m\) such that \(p_i\) and \(t_{s+i}\) are unequal under the Boolean equality of the alphabet, and \(k_s = m\) if there is no such \(i\). If \(m > n\), the naive matcher performs no comparisons.

theorem naiveMatches_time_eq [BEq α] (pattern text : List α) :
    (naiveMatches pattern text).time =
      if pattern.length ≤ text.length then
        ((text.tails.take (text.length - pattern.length + 1)).map fun suffix =>
          min pattern.length
            ((pattern.zip suffix).findIdx (fun pair => !(pair.1 == pair.2)) + 1)).sum
      else 0

Uses 1 · Used by 2

Statement usesNaive string matcher

Used byNaive matching with the empty pattern · Upper bound on the comparisons of naive matching

TheoremUpper bound on the comparisons of naive matching#✓fully proved

For a pattern of length \(m\) and a text of length \(n\), the naive matcher performs at most \((n - m + 1) \cdot m\) symbol comparisons if \(m \le n\), and no comparisons if \(m > n\).

theorem naiveMatches_time_le [BEq α] (pattern text : List α) :
    (naiveMatches pattern text).time ≤
      if pattern.length ≤ text.length then
        (text.length - pattern.length + 1) * pattern.length
      else 0

Uses 2

Statement usesNaive string matcher

Proof usesExact comparison count of naive matching

TheoremNaive matching on a repeated symbol reports every shift#✓fully proved

Let \(\alpha\) be a type whose Boolean equality is reflexive, let \(x \in \alpha\), and let \(m \le n\) be natural numbers. On the pattern consisting of \(m\) copies of \(x\) and the text consisting of \(n\) copies of \(x\), the naive matcher reports exactly the shifts \(0, 1, \dots, n - m\) in increasing order, so all overlapping occurrences are reported.

theorem naiveMatches_ret_replicate [BEq α] [ReflBEq α] (x : α) (m n : Nat) (hlen : m ≤ n) :
    (naiveMatches (List.replicate m x) (List.replicate n x)).ret = List.range (n - m + 1)

Uses 2 · Used by 1

Statement usesNaive string matcher

Proof usesOutput of naive matching

Used byRabin–Karp offsets on repeated-symbol words

TheoremComparison count of naive matching on a repeated symbol#✓fully proved

Let \(\alpha\) be a type whose Boolean equality is reflexive, let \(x \in \alpha\), and let \(m \le n\) be natural numbers. On the pattern consisting of \(m\) copies of \(x\) and the text consisting of \(n\) copies of \(x\), the naive matcher performs exactly \((n - m + 1) \cdot m\) symbol comparisons.

theorem naiveMatches_time_replicate [BEq α] [ReflBEq α] (x : α) (m n : Nat) (hlen : m ≤ n) :
    (naiveMatches (List.replicate m x) (List.replicate n x)).time = (n - m + 1) * m

Uses 1

Statement usesNaive string matcher

TheoremNaive matching with the empty pattern#✓fully proved

For every text \(t\) of length \(n\), the naive matcher run on the empty pattern and \(t\) reports exactly the shifts \(0, 1, \dots, n\) in increasing order and performs no symbol comparisons.

@[simp]
theorem naiveMatches_nil_pattern [BEq α] (text : List α) :
    naiveMatches [] text = ⟨List.range (text.length + 1), 0⟩

Uses 3 · Used by 2

Statement usesNaive string matcher

Proof usesOutput of naive matching · Exact comparison count of naive matching

Used byRabin–Karp matching with the empty pattern · Rabin–Karp and naive matching return the same offsets

TheoremNaive matching with a pattern longer than the text#✓fully proved

If the pattern \(p\) is longer than the text \(t\), then the naive matcher run on \(p\) and \(t\) reports no shifts and performs no symbol comparisons.

@[simp]
theorem naiveMatches_of_length_lt [BEq α] (pattern text : List α)
    (hlen : text.length < pattern.length) : naiveMatches pattern text = pure []

Uses 1 · Used by 1

Statement usesNaive string matcher

Used byRabin–Karp matching with a pattern longer than the text

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.