Context-Free Closure Under Substitution

This file imports mathlib's proof that context-free languages are closed under substitution and repackages it for this project's is_CF predicate.

Proof idea: translate the assumptions from is_CF to mathlib's Language.IsContextFree, apply mathlib's substitution closure theorem, and translate the result back.

Main declarations

• CF_of_subst_CF

theorem CF_of_subst_CF {α β : Type} (L : Language α) (f : α → Language β) : is_CF L → (∀ (a : α), is_CF (f a)) → is_CF (L.subst f)

The class of context-free languages is closed under substitution.

theorem CF_closedUnderSubstitution {α : Type} [Fintype α] : ClosedUnderSubstitution fun {α : Type} [Fintype α] => is_CF

The class of context-free languages is closed under substitution.