k-Factors of a List

The contiguous length-k infixes of a list — the infix sibling of List.sublistsLen (length-k subsequences). A generic list combinator with no domain content; used by the subregular hierarchy and a candidate for Mathlib/Data/List/.

Main definitions

• List.kFactors k xs — the contiguous length-k infixes of xs.

Main results

• List.mem_kFactors — f is a k-factor of xs iff it is a length-k infix (the infix analog of List.mem_sublistsLen).
• List.take_append_take — truncating the right operand of an append before taking a length-n prefix is a no-op (a candidate for Mathlib/Data/List/).

theorem List.take_append_take {α : Type u_1} (n : ℕ) (X Y : List α) : take n (X ++ take n Y) = take n (X ++ Y)

Truncating the right operand to length n before taking the length-n prefix of an append is a no-op: the prefix already ignores everything past position n.

theorem List.isInfix_iff_exists_offset {α : Type u_1} (S A : List α) : S <:+: A ↔ ∃ (δ : ℕ), δ ≤ A.length ∧ ∀ (i : ℕ), i < S.length → A[i + δ]? = S[i]?

A list is an infix of another iff some shift aligns every position of S with A (getElem?-wise): S <:+: A exactly when there is an offset δ ≤ A.length with A[i + δ]? = S[i]? for every i < S.length. The positional companion of mem_kFactors.

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

The contiguous length-k infixes of xs. Built by enumerating suffixes and taking each one's length-k prefix; suffixes shorter than k are filtered out. (For k = 0 every suffix qualifies, so kFactors 0 xs is xs.length + 1 copies of []; the subregular hierarchy only uses k ≥ 1.)

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. The infix analog of List.mem_sublistsLen.

theorem List.length_of_mem_kFactors {α : Type u_1} {k : ℕ} {xs f : List α} (h : f ∈ kFactors k xs) : f.length = k

Every member of kFactors k xs has length exactly k.

theorem List.isInfix_of_mem_kFactors {α : Type u_1} {k : ℕ} {xs f : List α} (h : f ∈ kFactors k xs) : f <:+: xs

A k-factor of xs is a contiguous infix of xs.

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 the 2-factors of b :: rest: the inductive step for chain-based characterizations of the SL₂ and TSL₂ languages.

@[simp]

theorem List.kFactors_two_nil {α : Type u_1} : kFactors 2 [] = []

An empty list has no 2-factors.

@[simp]

theorem List.kFactors_two_singleton {α : Type u_1} (a : α) : kFactors 2 [a] = []

A singleton list has no 2-factors.