String matching problem

DefinitionPattern match at an offset#✓fully proved

For lists \(p\) (the pattern) and \(t\) (the text) over a type \(\alpha\) and a natural number \(k\), the pattern \(p\) matches the text \(t\) at the zero-based offset \(k\) when \(k\) is at most the length of \(t\) and \(p\) is a prefix of the list obtained from \(t\) by dropping its first \(k\) entries.

The explicit bound on \(k\) excludes offsets beyond the end of the text for an empty pattern.

def MatchAt (pattern text : List α) (offset : Nat) : Prop :=
  offset ≤ text.length ∧ pattern <+: text.drop offset

Used by 11

Used byBoyer–Moore agrees with the naive matcher · Boyer–Moore returns exactly the occurrences · KMP 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 · Correctness of naive string matching · Correctness of Rabin–Karp matching · A pattern occurs in a text iff it matches at some offset · Characterization of a match at an offset · Correctness of the finite-automaton matcher

TheoremCharacterization of a match at an offset#✓fully proved

For lists \(p\) and \(t\) and a natural number \(k\), the pattern \(p\) matches the text \(t\) at the zero-based offset \(k\) if and only if \(k\) is at most the length of \(t\) and \(p\) is a prefix of the list obtained from \(t\) by dropping its first \(k\) entries.

theorem matchAt_iff (pattern text : List α) (offset : Nat) :
    MatchAt pattern text offset ↔ offset ≤ text.length ∧ pattern <+: text.drop offset

Uses 1

Statement usesPattern match at an offset

TheoremA pattern occurs in a text iff it matches at some offset#✓fully proved

For lists \(p\) and \(t\), there is an offset \(k\) such that the pattern \(p\) matches the text \(t\) at \(k\) if and only if \(p\) is an infix of \(t\), that is, \(t\) is the concatenation of some list \(u\), then \(p\), then some list \(v\).

theorem exists_matchAt_iff_isInfix (pattern text : List α) :
    (∃ offset, MatchAt pattern text offset) ↔ pattern <:+: text

Uses 1 · Used by 1

Statement usesPattern match at an offset

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

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.