Word models

The model-theoretic representation underlying logical characterizations of subregular functions: a string viewed as a finite labeled linear order. A word model is the relational signature ⟨D, L, R⟩ — a domain D of positions, unary labels L, and the binary immediate-successor relation R; general precedence is the (FO-definable) transitive closure of successor and is not part of the quantifier-free fragment.

The carrier is List α itself: a string is its word model. This is deliberately where mathlib stops — it has strings (List/FreeMonoid) and automata (DFA, MyhillNerode) but no model-theoretic word structure — and it keeps the logic layer directly composable with Subregular's string functions (Subregular.IsInputStrictlyLocal, SFST).

Main definitions

• Subregular.Logic.WordModel — a string over α, viewed as ⟨D, label, succ⟩.
• WordModel.label? — the unary label (symbol) at a position, none off the edge.
• WordModel.Mem — domain membership of a position.
• WordModel.succ? / WordModel.pred? — successor/predecessor as partial functions.

Implementation notes

Positions are ℕ indices; a position is in-domain iff below length. Successor and predecessor are partial functions (Option ℕ) rather than relations — this is what lets the quantifier-free term language (Logic/QFLogic.lean) reach a bounded neighbourhood via succ/pred chains without quantifiers, the syntactic source of strict locality.

@[reducible, inline]

abbrev Subregular.Logic.WordModel (α : Type u_1) : Type u_1

A word model: a string over α, viewed model-theoretically as a finite linear order of positions carrying unary labels and an immediate-successor relation.

Equations

• Subregular.Logic.WordModel α = List α

def Subregular.Logic.WordModel.label? {α : Type u_1} (w : WordModel α) (n : ℕ) : Option α

The label (symbol) at position n, or none off the edge.

Equations

• w.label? n = w[n]?

def Subregular.Logic.WordModel.Mem {α : Type u_1} (w : WordModel α) (n : ℕ) : Prop

Position n lies in the domain.

Equations

• w.Mem n = (n < List.length w)

@[implicit_reducible]

instance Subregular.Logic.WordModel.instDecidableMem {α : Type u_1} (w : WordModel α) (n : ℕ) : Decidable (w.Mem n)

Equations

• w.instDecidableMem n = n.decLt (List.length w)

def Subregular.Logic.WordModel.succ? {α : Type u_1} (w : WordModel α) (n : ℕ) : Option ℕ

Successor as a partial function: the position after n, defined iff it is in range.

Equations

• w.succ? n = if n + 1 < List.length w then some (n + 1) else none

def Subregular.Logic.WordModel.pred? {α : Type u_1} (w : WordModel α) : ℕ → Option ℕ

Predecessor as a partial function: the position before n, defined iff n > 0.

Equations

• w.pred? 0 = none
• w.pred? n.succ = if n < List.length w then some n else none

@[simp]

theorem Subregular.Logic.WordModel.label?_eq_getElem? {α : Type u_1} (w : WordModel α) (n : ℕ) : w.label? n = w[n]?

theorem Subregular.Logic.WordModel.succ?_eq_some_iff {α : Type u_1} {w : WordModel α} {n m : ℕ} : w.succ? n = some m ↔ m = n + 1 ∧ n + 1 < List.length w

theorem Subregular.Logic.WordModel.succ?_congr {α : Type u_1} {w w' : WordModel α} (h : List.length w = List.length w') : w.succ? = w'.succ?

The successor structure depends only on the length.

theorem Subregular.Logic.WordModel.pred?_congr {α : Type u_1} {w w' : WordModel α} (h : List.length w = List.length w') : w.pred? = w'.pred?

The predecessor structure depends only on the length.

theorem Subregular.Logic.WordModel.pred?_eq_some_iff {α : Type u_1} {w : WordModel α} {n m : ℕ} : w.pred? n = some m ↔ n = m + 1 ∧ m < List.length w

@[simp]

theorem Subregular.Logic.WordModel.mem_iff {α : Type u_1} (w : WordModel α) (n : ℕ) : w.Mem n ↔ n < List.length w