Words as blank-padded indexed families

List.config reads a word as a two-sided indexed family ℤ → Option α: letters on [0, w.length), blank (none) elsewhere; List.window k w i is its width-k slice at i. Position-indexed statements about words replace factor-of-augmented-word bookkeeping: a window entry is a letter or a blank according to a single interval test, so occurrence pinning is interval arithmetic.

[UPSTREAM] candidate: Mathlib.Data.List, on the List.toFinsupp precedent — a list as an indexed family with a default.

def List.config {α : Type u_1} (w : List α) : ℤ → Option α

The two-sided configuration of a word: letters on [0, w.length), blank elsewhere.

Equations

• w.config i = if 0 ≤ i then w[i.toNat]? else none

@[simp]

theorem List.config_natCast {α : Type u_1} (w : List α) (n : ℕ) : w.config ↑n = w[n]?

theorem List.config_neg {α : Type u_1} {w : List α} {i : ℤ} (h : i < 0) : w.config i = none

@[simp]

theorem List.config_nil {α : Type u_1} {i : ℤ} : [].config i = none

theorem List.config_eq_none_iff {α : Type u_1} {w : List α} {i : ℤ} : w.config i = none ↔ i < 0 ∨ ↑w.length ≤ i

theorem List.bounds_of_config_eq_some {α : Type u_1} {w : List α} {i : ℤ} {a : α} (h : w.config i = some a) : 0 ≤ i ∧ i < ↑w.length

theorem List.getElem?_of_config_eq_some {α : Type u_1} {w : List α} {i : ℤ} {a : α} (h : w.config i = some a) : w[i.toNat]? = some a

theorem List.eq_of_config_agree {α : Type u_1} {w y : List α} (h : ∀ (j : ℤ), j ≤ ↑w.length → y.config j = w.config j) : y = w

Agreement of configurations up to the word's length forces equality.

theorem List.take_eq_of_config_agree {α : Type u_1} {w y : List α} {c : ℕ} (h : ∀ (j : ℤ), j < ↑c → y.config j = w.config j) : take c y = take c w

Agreement of configurations below c transfers c-prefixes.

theorem List.config_append_left {α : Type u_1} {u v : List α} {i : ℤ} (h : i < ↑u.length) : (u ++ v).config i = u.config i

theorem List.config_take {α : Type u_1} {w : List α} {i : ℤ} {c : ℕ} (h : i < ↑c) : (take c w).config i = w.config i

Windows

def List.window {α : Type u_1} (k : ℕ) (w : List α) (i : ℤ) : List (Option α)

The width-k window of w at i: the configuration restricted to [i, i + k).

Equations

• List.window k w i = List.ofFn fun (j : Fin k) => w.config (i + ↑↑j)

@[simp]

theorem List.length_window {α : Type u_1} {w : List α} {i : ℤ} {k : ℕ} : (window k w i).length = k

theorem List.getElem?_window {α : Type u_1} {w : List α} {i : ℤ} {k j : ℕ} (h : j < k) : (window k w i)[j]? = some (w.config (i + ↑j))

theorem List.window_eq_window_iff {α : Type u_1} {w y : List α} {i q : ℤ} {k : ℕ} : window k w i = window k y q ↔ ∀ (j : ℕ), j < k → w.config (i + ↑j) = y.config (q + ↑j)