Skip to content
  1. CLRS-Lean
  2. Chapters 1–35 · CLRS Fourth Edition
  3. Chapter 32. String Matching
  4. 32.1. The Naive String-Matching Algorithm
Browse chapters
Imports
import Mathlib

32.1. The Naive String-Matching Algorithm

This section defines the string/text model used throughout Chapter 32: string matching. A string is a list of elements drawn from an alphabet. We define the basic operations — length, prefix, suffix, and the corresponding predicates — that the finite-automaton and KMP constructions rely on.

The definitions are parameterized over the element type α; for concrete executability, instantiate α := Char or α := UInt8.

Key definitions

  • Text α: a string (alias for List α).

  • length: number of characters.

  • textPrefix t k: the first k characters of t.

  • suffix t k: the last k characters of t.

  • isPrefix p t: p is a prefix of t.

  • isSuffix p t: p is a suffix of t.

All operations are zero-indexed: the first character is at position 0, and taking a prefix of length 0 yields the empty list.

Implementation details

namespace CLRSnamespace Chapter32

A text (string) is a list of elements from an alphabet. Use α := Char for concrete text, or a generic α for abstract reasoning.

abbrev Text (α : Type) := List α
variable {α : Type}

The length of a text.

abbrev length (t : Text α) : ℕ := t.length

The prefix of t of length k. If k exceeds the text length, the result is the full text.

def textPrefix (t : Text α) (k : ℕ) : Text α := t.take k

The suffix of t of length k. If k exceeds the text length, the result is the full text.

def suffix (t : Text α) (k : ℕ) : Text α := t.drop (t.length - k)

p is a prefix of t.

def isPrefix (p t : Text α) : Prop := ∃ s, p ++ s = t

p is a suffix of t.

def isSuffix (p t : Text α) : Prop := ∃ s, s ++ p = t

p is a proper prefix of t: a prefix that is strictly shorter than t.

def isProperPrefix (p t : Text α) : Prop := isPrefix p t ∧ p.length < t.length

p is a proper suffix of t: a suffix that is strictly shorter than t.

def isProperSuffix (p t : Text α) : Prop := isSuffix p t ∧ p.length < t.length

The empty text is a prefix of every text.

theorem isPrefix_empty (t : Text α) : isPrefix [] t := ⟨t, by simp [This simp argument is unused: isPrefix Hint: Omit it from the simp argument list. simp ̵[̵i̵s̵P̵r̵e̵f̵i̵x̵]̵ Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`isPrefix]⟩

The empty text is a suffix of every text.

theorem isSuffix_empty (t : Text α) : isSuffix [] t := ⟨t, by simp [This simp argument is unused: isSuffix Hint: Omit it from the simp argument list. simp ̵[̵i̵s̵S̵u̵f̵f̵i̵x̵]̵ Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`isSuffix]⟩

Every text is a prefix of itself.

theorem isPrefix_self (t : Text α) : isPrefix t t := ⟨[], by simp [This simp argument is unused: isPrefix Hint: Omit it from the simp argument list. simp ̵[̵i̵s̵P̵r̵e̵f̵i̵x̵]̵ Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`isPrefix]⟩

Every text is a suffix of itself.

theorem isSuffix_self (t : Text α) : isSuffix t t := ⟨[], by simp [This simp argument is unused: isSuffix Hint: Omit it from the simp argument list. simp ̵[̵i̵s̵S̵u̵f̵f̵i̵x̵]̵ Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`isSuffix]⟩

If p is a prefix of t, then p.length ≤ t.length.

theorem isPrefix_length_le (hp : isPrefix p t) : p.length ≤ t.length := by rcases hp with ⟨s, h⟩ have := calc t.length = (p ++ s).length := by rw [h] _ = p.length + s.length := by simp omega

If p is a suffix of t, then p.length ≤ t.length.

theorem isSuffix_length_le (hp : isSuffix p t) : p.length ≤ t.length := by rcases hp with ⟨s, h⟩ have := calc t.length = (s ++ p).length := by rw [h] _ = s.length + p.length := by simp omega

The prefix of length 0 is the empty list.

@[simp] theorem textPrefix_zero (t : Text α) : textPrefix t 0 = [] := by simp [textPrefix]

Taking the prefix of length equal to the text length returns the whole text.

@[simp] theorem textPrefix_length (t : Text α) : textPrefix t t.length = t := by simp [textPrefix]

The suffix of length 0 is the empty list.

@[simp] theorem suffix_zero (t : Text α) : suffix t 0 = [] := by simp [suffix]

Taking the suffix of length equal to the text length returns the whole text.

@[simp] theorem suffix_length (t : Text α) : suffix t t.length = t := by simp [suffix]

The empty text has no non-empty prefix.

theorem textPrefix_nil_of_length_eq_zero (t : Text α) (h : length t = 0) (k : ℕ) : textPrefix t k = [] := by have : t = [] := by simpa [length] using h subst this; simp [textPrefix]

The empty text has no non-empty suffix.

theorem suffix_nil_of_length_eq_zero (t : Text α) (h : length t = 0) (k : ℕ) : suffix t k = [] := by have : t = [] := by simpa [length] using h subst this; simp [suffix]

textPrefix is a prefix of the original text.

theorem isPrefix_textPrefix (t : Text α) (k : ℕ) : isPrefix (textPrefix t k) t := by refine ⟨t.drop k, ?_⟩ simp [This simp argument is unused: isPrefix Hint: Omit it from the simp argument list. simp [i̵s̵P̵r̵e̵f̵i̵x̵,̵ ̵textPrefix, List.take_append_drop] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`isPrefix, textPrefix, List.take_append_drop]

suffix is a suffix of the original text.

theorem isSuffix_suffix (t : Text α) (k : ℕ) : isSuffix (suffix t k) t := by refine ⟨t.take (t.length - k), ?_⟩ simp [This simp argument is unused: isSuffix Hint: Omit it from the simp argument list. simp [̵i̵s̵S̵u̵f̵f̵i̵x̵,̵ ̵s̵u̵f̵f̵i̵x̵,̵[̲s̲u̲f̲f̲i̲x̲,̲ List.take_append_drop, add_comm] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`isSuffix, suffix, List.take_append_drop, This simp argument is unused: add_comm Hint: Omit it from the simp argument list. simp [isSuffix, suffix, List.take_append_drop,̵ ̵a̵d̵d̵_̵c̵o̵m̵m̵] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`add_comm]
end Chapter32end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_32.Section_32_1_String_Model.Naive_Matcher

Section 32.1 — Naive String-Matching Algorithm

The naive string-matching algorithm (CLRS §32.1) finds all occurrences of a pattern P of length m in a text T of length n by trying every possible shift s = 0, 1, …, n-m and checking whether P matches T at that position. The worst-case running time is Θ((n-m+1)·m) = O(m·n).

Key definitions

  • matchesAt T P s — pattern P occurs in text T starting at shift s.

  • naiveMatcher T P — returns the list of all shifts where P occurs in T.

  • noMatch — convenience abbreviation for the empty match list.

Notation

This file uses Text α = List α from Section_32_1_String_Model and standard Nat-based lengths.

namespace CLRSnamespace Chapter32variable {α : Type} [BEq α] [DecidableEq α]

Pattern P matches text T at shift s: the substring of T from position s of length |P| equals P. Formally, (T.drop s).take |P| = P.

def matchesAt (T P : Text α) (s : ℕ) : Bool := if s + P.length ≤ T.length then (T.drop s).take P.length == P else false

The naive string matcher: enumerate all shifts s ∈ [0, n-m] and return those where the pattern matches.

def naiveMatcher (T P : Text α) : List ℕ := if P.length = 0 then List.range (T.length + 1) else let n := T.length let m := P.length let maxShift := n - m (List.range (maxShift + 1)).filter fun s => matchesAt T P s

Convenience abbreviation for "no match".

abbrev noMatch : List ℕ := []

If a shift s is in naiveMatcher T P, then matchesAt T P s is true.

automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_sound`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_sound`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_sound`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_sound`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_sound`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_sound`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_sound`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_sound`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_sound`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_sound`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_sound`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_sound`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_sound`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_sound`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_sound`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_sound`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_sound`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_sound`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_sound`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_sound`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_sound`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_sound`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`theorem naiveMatcher_sound (T P : Text α) (s : ℕ) (h : s ∈ naiveMatcher T P) : matchesAt T P s := by unfold naiveMatcher at h split at h · -- case: P.length = 0 rename_i hzero have hempty : P = [] := by cases P · rfl · simp at hzero subst hempty unfold matchesAt have hs : s ≤ T.length := by have := List.mem_range.mp h omega simp [hs] · -- case: P.length ≠ 0 have hmem := List.mem_filter.mp h exact hmem.2

If matchesAt T P s is true, then s is in naiveMatcher T P.

automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_complete`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`theorem naiveMatcher_complete (T P : Text α) (s : ℕ) (hmatch : matchesAt T P s) : s ∈ naiveMatcher T P := by unfold naiveMatcher by_cases hzero : P.length = 0 · -- empty pattern: all shifts are included, need s ≤ T.length from hmatch have hempty : P = [] := by cases P · rfl · simp at hzero subst hempty unfold matchesAt at hmatch -- hmatch: (if s + 0 ≤ T.length then [] == [] else false) = true simp at hmatch -- hmatch now gives s ≤ T.length have hs : s < T.length + 1 := by omega simp [hs] · -- non-empty pattern have hbound : s + P.length ≤ T.length := by unfold matchesAt at hmatch split at hmatch · assumption · simp at hmatch have hshift : s ≤ T.length - P.length := by omega have hle : s < (T.length - P.length) + 1 := by omega have hmatch' : matchesAt T P s = true := hmatch simpa [hzero] using List.mem_filter.mpr ⟨List.mem_range.mpr hle, hmatch'⟩

The empty pattern matches at every position.

automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_empty`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_empty`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_empty`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` @[simp] automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_empty`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`theorem naiveMatcher_empty (T : Text α) : naiveMatcher T [] = List.range (T.length + 1) := by unfold naiveMatcher; simp

If the pattern is longer than the text, there are no matches.

automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_pattern_too_long`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_pattern_too_long`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_pattern_too_long`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_pattern_too_long`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_pattern_too_long`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_pattern_too_long`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_pattern_too_long`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_pattern_too_long`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_pattern_too_long`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_pattern_too_long`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_pattern_too_long`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_pattern_too_long`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_pattern_too_long`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_pattern_too_long`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_pattern_too_long`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`Try `simp at h` instead of `simpa using h` Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_pattern_too_long`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_pattern_too_long`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_pattern_too_long`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_pattern_too_long`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_pattern_too_long`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` automatically included section variable(s) unused in theorem `CLRS.Chapter32.naiveMatcher_pattern_too_long`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`theorem naiveMatcher_pattern_too_long (T P : Text α) (h : T.length < P.length) : naiveMatcher T P = noMatch := by unfold naiveMatcher noMatch by_cases hzero : P.length = 0 · -- P is empty, impossible because T.length < 0 would be contradiction have : T.length < 0 := by Try `simp at h` instead of `simpa using h` Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hzero] using h omega · have hsub : T.length - P.length = 0 := by omega simp [hzero, hsub] -- Need to show: filter (matchesAt T P) (range 1) = [] -- range 1 = [0], and matchesAt T P 0 = false because 0+P.length > T.length have hfalse : matchesAt T P 0 = false := by unfold matchesAt simp omega simp [hfalse]

Shifts returned by naiveMatcher are within bounds.

theorem naiveMatcher_shifts_valid (T P : Text α) (s : ℕ) (h : s ∈ naiveMatcher T P) : s + P.length ≤ T.length := by have hmatch := naiveMatcher_sound T P s h unfold matchesAt at hmatch split at hmatch · assumption · simp at hmatch
end Chapter32end CLRS