Length-k infixes of a list

List.kFactors k xs lists the contiguous length-k infixes of xs, the infix sibling of List.sublistsLen (length-k subsequences): List.mem_kFactors characterizes membership as f <:+: xs ∧ f.length = k, and List.kFactors_cons is the recursion that computes it. The name is the subregular literature's "k-factor"; mathlib has no length-k infix enumerator.

Main definitions

• List.kFactors: the contiguous length-k infixes of a list, in order of occurrence.

Main results

• List.mem_kFactors: membership is being a length-k infix, mirroring List.mem_sublistsLen.
• List.kFactors_nil, List.kFactors_cons, List.kFactors_two_cons_cons: the recursion, and its k = 2 form used by chain characterizations of the strictly 2-local languages.
• List.mem_kFactors_append: a k-factor of a concatenation lies in one of the two words or across the seam between them.
• List.kFactors_map: mapping a function over a list maps it over the k-factors.

def List.kFactors {α : Type u_1} (k : ℕ) (xs : List α) : List (List α)

The contiguous length-k infixes of xs, in order of occurrence: the length-k prefixes of the suffixes long enough to have one.

Equations

• List.kFactors k xs = List.map (fun (x : List α) => List.take k x) (List.filter (fun (x : List α) => decide (k ≤ x.length)) xs.tails)

theorem List.mem_kFactors {α : Type u_1} {k : ℕ} {xs f : List α} : f ∈ kFactors k xs ↔ f <:+: xs ∧ f.length = k

A list is a k-factor of xs iff it is a length-k infix.

@[simp]

theorem List.kFactors_nil {α : Type u_1} {k : ℕ} : kFactors k [] = if k = 0 then [[]] else []

@[simp]

theorem List.kFactors_cons {α : Type u_1} {k : ℕ} (a : α) (l : List α) : kFactors k (a :: l) = if k ≤ l.length + 1 then take k (a :: l) :: kFactors k l else kFactors k l

theorem List.kFactors_two_cons_cons {α : Type u_1} (a b : α) (rest : List α) : kFactors 2 (a :: b :: rest) = [a, b] :: kFactors 2 (b :: rest)

The 2-factors of a :: b :: rest are [a, b] followed by those of b :: rest.

theorem List.mem_kFactors_append {α : Type u_1} {k : ℕ} {f u v : List α} : f ∈ kFactors k (u ++ v) ↔ f ∈ kFactors k u ∨ f ∈ kFactors k v ∨ f ∈ kFactors k (u.rtake (k - 1) ++ take (k - 1) v)

A k-factor of u ++ v lies in u, in v, or across the seam, in the last k - 1 letters of u followed by the first k - 1 letters of v.

@[simp]

theorem List.kFactors_map {α : Type u_1} {k : ℕ} {β : Type u_2} (g : α → β) (xs : List α) : kFactors k (map g xs) = map (map g) (kFactors k xs)