Higman's lemma with one distinguished occurrence

This file packages the marked-letter argument used in the shrinking lemma for indexed languages. If one occurrence of a word is distinguished, Higman's lemma supplies a member of a fixed finite basis whose sublist embedding keeps that occurrence.

The Boolean component of a marked word records the distinguished occurrence. Using an explicit marked sublist in RetainsAt avoids confusing two equal letters occurring at different positions.

Reference

• R. H. Gilman, "A shrinking lemma for indexed languages", Theoretical Computer Science 163 (1996), 277--281.

def MarkedHigman.eraseMarks {α : Type u_1} (z : List (α × Bool)) : List α

Erase the Boolean marks from a marked word.

Equations

• MarkedHigman.eraseMarks z = List.map Prod.fst z

def MarkedHigman.markAt {α : Type u_1} (y : List α) (i : Fin y.length) : List (α × Bool)

Mark exactly the occurrence at position i.

Equations

• MarkedHigman.markAt y i = List.map (fun (a : α) => (a, false)) (List.take (↑i) y) ++ (y.get i, true) :: List.map (fun (a : α) => (a, false)) (List.drop (↑i + 1) y)

def MarkedHigman.mappedIndex {α : Type u_1} {β : Type u_2} (f : α → β) (y : List α) (i : Fin y.length) : Fin (List.map f y).length

The position corresponding to i after mapping a list.

Equations

• MarkedHigman.mappedIndex f y i = ⟨↑i, ⋯⟩

def MarkedHigman.leftIndex {α : Type u_1} (y suffix : List α) (i : Fin y.length) : Fin (y ++ suffix).length

An index in the left list, viewed after appending a suffix.

Equations

• MarkedHigman.leftIndex y suffix i = ⟨↑i, ⋯⟩

def MarkedHigman.shiftedIndex {α : Type u_1} (pre y : List α) (i : Fin y.length) : Fin (pre ++ y).length

Shift an index past a prepended prefix.

Equations

• MarkedHigman.shiftedIndex pre y i = ⟨pre.length + ↑i, ⋯⟩

def MarkedHigman.ExactlyOneMarked {α : Type u_1} (z : List (α × Bool)) : Prop

A marked word has exactly one marked occurrence.

The existential decomposition is deliberately structural: it neither needs decidable equality on the alphabet nor identifies equal occurrences.

Equations

• MarkedHigman.ExactlyOneMarked z = ∃ (l : List α) (a : α) (r : List α), z = List.map (fun (b : α) => (b, false)) l ++ (a, true) :: List.map (fun (b : α) => (b, false)) r

def MarkedHigman.RetainsAt {α : Type u_1} (x y : List α) (i : Fin y.length) : Prop

x is selected from y while retaining the exact occurrence at i.

The witness z is the marked sublist. Its true Boolean marker can only be the marker placed at i, even when the underlying letter occurs repeatedly.

Equations

• MarkedHigman.RetainsAt x y i = ∃ (z : List (α × Bool)), z.Sublist (MarkedHigman.markAt y i) ∧ MarkedHigman.eraseMarks z = x ∧ (y.get i, true) ∈ z

@[simp]

theorem MarkedHigman.eraseMarks_markAt {α : Type u_1} (y : List α) (i : Fin y.length) : eraseMarks (markAt y i) = y

@[simp]

theorem MarkedHigman.length_markAt {α : Type u_1} (y : List α) (i : Fin y.length) : (markAt y i).length = y.length

theorem MarkedHigman.exactlyOneMarked_markAt {α : Type u_1} (y : List α) (i : Fin y.length) : ExactlyOneMarked (markAt y i)

@[simp]

theorem MarkedHigman.markAt_map {α : Type u_1} {β : Type u_2} (f : α → β) (y : List α) (i : Fin y.length) : markAt (List.map f y) (mappedIndex f y i) = List.map (fun (p : α × Bool) => (f p.1, p.2)) (markAt y i)

@[simp]

theorem MarkedHigman.markAt_append_right {α : Type u_1} (y suffix : List α) (i : Fin y.length) : markAt (y ++ suffix) (leftIndex y suffix i) = markAt y i ++ List.map (fun (a : α) => (a, false)) suffix

@[simp]

theorem MarkedHigman.markAt_append_left {α : Type u_1} (pre y : List α) (i : Fin y.length) : markAt (pre ++ y) (shiftedIndex pre y i) = List.map (fun (a : α) => (a, false)) pre ++ markAt y i

theorem MarkedHigman.ExactlyOneMarked.exists_marked_mem {α : Type u_1} {z : List (α × Bool)} (hz : ExactlyOneMarked z) : ∃ (a : α), (a, true) ∈ z

theorem MarkedHigman.fst_eq_get_of_marked_mem_markAt {α : Type u_1} {y : List α} {i : Fin y.length} {a : α} (h : (a, true) ∈ markAt y i) : a = y.get i

theorem MarkedHigman.RetainsAt.sublist {α : Type u_1} {x y : List α} {i : Fin y.length} (h : RetainsAt x y i) : x.Sublist y

theorem MarkedHigman.RetainsAt.cast {α : Type u_1} {x y y' : List α} (hyy : y = y') {i : Fin y.length} (h : RetainsAt x y i) : RetainsAt x y' (Fin.cast ⋯ i)

Transport occurrence retention along equality of the ambient words.

theorem MarkedHigman.retainsAt_refl {α : Type u_1} (y : List α) (i : Fin y.length) : RetainsAt y y i

Every word retains each of its own occurrences.

theorem MarkedHigman.RetainsAt.append_right_sublist {α : Type u_1} {x y xr yr : List α} {i : Fin y.length} (h : RetainsAt x y i) (hright : xr.Sublist yr) : RetainsAt (x ++ xr) (y ++ yr) (leftIndex y yr i)

Append an arbitrary sublist on the right while retaining an occurrence from the left word.

theorem MarkedHigman.RetainsAt.append_left_sublist {α : Type u_1} {xl yl x y : List α} {i : Fin y.length} (hleft : xl.Sublist yl) (h : RetainsAt x y i) : RetainsAt (xl ++ x) (yl ++ y) (shiftedIndex yl y i)

Prepend an arbitrary sublist while retaining an occurrence from the right word.

theorem MarkedHigman.RetainsAt.map {α : Type u_1} {β : Type u_2} (f : α → β) {x y : List α} {i : Fin y.length} (h : RetainsAt x y i) : RetainsAt (List.map f x) (List.map f y) (mappedIndex f y i)

Pointwise maps preserve the selected occurrence.

theorem MarkedHigman.RetainsAt.exists_preimage {α : Type u_1} {β : Type u_2} (f : α → β) {x : List β} {y : List α} {i : Fin y.length} (h : RetainsAt x (List.map f y) (mappedIndex f y i)) : ∃ (x' : List α), RetainsAt x' y i ∧ List.map f x' = x

Pull a retained occurrence back through a pointwise map. Injectivity of the map is unnecessary: the unique Boolean marker identifies the original occurrence even when several letters have the same image.

theorem MarkedHigman.exists_finite_retaining_basis (α : Type u_2) [Fintype α] (Y : Set (List α)) : ∃ (X : Set (List α)), X.Finite ∧ X ⊆ Y ∧ ∀ y ∈ Y, y ∉ X → ∀ (i : Fin y.length), ∃ x ∈ X, x.length < y.length ∧ RetainsAt x y i

One-position marked form of Higman's finite-basis lemma.

For every language over a finite alphabet there is a finite subset X such that every word outside X, with any one occurrence distinguished, has a proper sublist in X whose sublist embedding retains that occurrence.