Linear languages under terminal maps (alphabet renamings)

This file concerns the letter-to-letter map Language.map f for f : T₁ → T₂ (an alphabet renaming). It is not the general string homomorphism α → List β of the ClosedUnderHomomorphism predicate — the symbol-to-string case is not treated here.

Relabelling the terminals of a grammar by such an f (the construction map_grammar) keeps the nonterminals untouched, so it preserves the linear rule shape. Because a linear grammar's rules have empty left/right context, the relabelled grammar generates exactly the f-image of the original language — even when f is not injective. This yields:

• is_Linear_map — Linear is closed under terminal maps Language.map f.
• is_Linear_of_map_injective — and is reflected along injective maps.

The reflection direction is what lets a non-linearity result over a small concrete alphabet (e.g. Fin 4) be transported to any larger alphabet.

theorem eq_map_terminal_of_all {T₁ N : Type} {l : List (symbol T₁ N)} : (∀ s ∈ l, ∃ (t : T₁), s = symbol.terminal t) → ∃ (o : List T₁), l = List.map symbol.terminal o

A symbol list whose entries are all terminals is the image of a terminal word.

theorem map_grammar_linear {T₁ T₂ : Type} {g : grammar T₁} (hg : grammar_linear g) (f : T₁ → T₂) : grammar_linear (map_grammar g f)

Relabelling preserves the linear rule shape (nonterminals are untouched).

theorem map_grammar_derives {T₁ T₂ : Type} {g : grammar T₁} (f : T₁ → T₂) {x y : List (symbol T₁ g.nt)} (h : grammar_derives g x y) : grammar_derives (map_grammar g f) (List.map (map_symbol_fn f) x) (List.map (map_symbol_fn f) y)

Forward relabelling of derivations.

theorem map_symbol_fn_eq_sandwich {T₁ T₂ N : Type} {f : T₁ → T₂} {N0 : N} {x : List (symbol T₁ N)} {U V : List (symbol T₂ N)} : List.map (map_symbol_fn f) x = U ++ [symbol.nonterminal N0] ++ V → ∃ (Ux : List (symbol T₁ N)) (Vx : List (symbol T₁ N)), x = Ux ++ [symbol.nonterminal N0] ++ Vx ∧ U = List.map (map_symbol_fn f) Ux ∧ V = List.map (map_symbol_fn f) Vx

A relabelled list splits around a nonterminal exactly as the original does.

theorem map_grammar_derives_reflect {T₁ T₂ : Type} {g : grammar T₁} (hg : grammar_linear g) (f : T₁ → T₂) {z : List (symbol T₂ g.nt)} (h : grammar_derives (map_grammar g f) [symbol.nonterminal g.initial] z) : ∃ (x : List (symbol T₁ g.nt)), z = List.map (map_symbol_fn f) x ∧ grammar_derives g [symbol.nonterminal g.initial] x

Reflection of derivations: any derivation of the relabelled (linear) grammar comes from a derivation of the original grammar (this uses the empty context of linear rules).

theorem map_grammar_language_linear {T₁ T₂ : Type} {g : grammar T₁} (hg : grammar_linear g) (f : T₁ → T₂) : grammar_language (map_grammar g f) = (Language.map f) (grammar_language g)

The relabelled grammar generates exactly the f-image of the original language.

theorem is_Linear_map {T₁ T₂ : Type} {L : Language T₁} (hL : is_Linear L) (f : T₁ → T₂) : is_Linear ((Language.map f) L)

Linear languages are closed under terminal maps.

theorem is_Linear_of_map_injective {T₁ T₂ : Type} [Nonempty T₁] {f : T₁ → T₂} (hf : Function.Injective f) {L : Language T₁} (h : is_Linear ((Language.map f) L)) : is_Linear L

Linearity is reflected along injective terminal maps.