Context-Free Closure Under Suffix

This file proves that context-free languages are closed under the suffix operation, via the decomposition suffixLang L = reverse(prefixLang(reverse L)).

Strategy

We use the identity suffixLang L = (prefixLang L.reverse).reverse (proved in LanguageOperations.lean as suffixLang_eq_reverse_prefixLang_reverse), together with the already-established closure of context-free languages under:

• reversal (CF_of_reverse_CF, CF_of_reverse_CF_rev), and
• prefix (is_CF_prefixLang).

Main declarations

• is_CF_suffixLang
• Language.IsContextFree.suffixLang

theorem is_CF_suffixLang {T : Type} [Fintype T] {L : Language T} (h : is_CF L) : is_CF L.suffixLang

Context-free languages are closed under the suffix operation (project-level is_CF formulation). The proof decomposes suffix as reverse ∘ prefix ∘ reverse: suffixLang L = (prefixLang L.reverse).reverse and applies the known closure of CFLs under reversal and prefix.

theorem Language.IsContextFree.suffixLang {T : Type} [Fintype T] {L : Language T} (h : L.IsContextFree) : L.suffixLang.IsContextFree

Context-free languages are closed under the suffix operation (Mathlib-style Language.IsContextFree formulation).