Regular Closure Under Suffix

Proof idea: reduce suffix closure to prefix closure by reversing twice. A suffix of a word in L reverses to a prefix of a word in L.reverse, and regular languages are closed under both reverse and prefix.

Regular Closure Under Suffix

This file proves that regular languages are closed under the suffix operation, via the decomposition suffixLang L = reverse(prefixLang(reverse L)), and shows that the converse fails over any nontrivial alphabet.

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 regular languages under:

• reversal (Language.isRegular_reverse_iff'), and
• prefix (Language.IsRegular.prefixLang).

Main declarations

• Language.IsRegular.suffixLang
• Language.not_iff_regular_suffix

theorem Language.IsRegular.suffixLang {α : Type u_1} {L : Language α} (h : L.IsRegular) : L.suffixLang.IsRegular

Regular languages are closed under the suffix operation.

theorem Language.not_iff_regular_suffix {α : Type u_1} [Nontrivial α] : ¬∀ (L : Language α), L.suffixLang.IsRegular ↔ L.IsRegular

The converse of suffix closure fails over any nontrivial alphabet.