Context-Free Closure Converses Fail

This file proves that the closure properties of context-free languages under union, concatenation, and substitution are strict implications, not biconditionals. That is, while:

• is_CF L₁ ∧ is_CF L₂ → is_CF (L₁ + L₂) (closure under union),
• is_CF L₁ ∧ is_CF L₂ → is_CF (L₁ * L₂) (closure under concatenation),
• is_CF L ∧ (∀ a, is_CF (f a)) → is_CF (L.subst f) (closure under substitution), the converses of all three fail.

Proof sketch

All counterexamples derive from the existence of a non-context-free language, which is obtained from nnyCF_of_CF_i_CF (non-closure under intersection): there exist CF languages L₁, L₂ whose intersection L₁ ⊓ L₂ is not CF.

• Union: Take A = L₁ ⊓ L₂ (not CF) and B = L₁ (CF). Then A + B = (L₁ ⊓ L₂) ⊔ L₁ = L₁ is CF, but A is not CF.
• Concatenation: Take A = L₁ ⊓ L₂ (not CF) and B = 0 (empty language, CF). Then A * B = 0 is CF, but A is not CF.
• Substitution: Take L = 0 : Language Unit and f () = L₁ ⊓ L₂ (not CF). Then L.subst f = 0 is CF, but f maps to a non-CF language.

Main declarations

• not_iff_CF_union
• not_iff_CF_concat
• not_iff_CF_subst

theorem not_iff_CF_union : ¬∀ (T : Type) (L₁ L₂ : Language T), is_CF (L₁ + L₂) ↔ is_CF L₁ ∧ is_CF L₂

The converse of union closure fails: there exist languages where L₁ + L₂ is CF but not both L₁ and L₂ are CF.

theorem not_iff_CF_concat : ¬∀ (T : Type) (L₁ L₂ : Language T), is_CF (L₁ * L₂) ↔ is_CF L₁ ∧ is_CF L₂

The converse of concatenation closure fails: there exist languages where L₁ * L₂ is CF but not both L₁ and L₂ are CF.

theorem not_iff_CF_subst : ¬∀ (α β : Type) (L : Language α) (f : α → Language β), is_CF (L.subst f) ↔ is_CF L ∧ ∀ (a : α), is_CF (f a)

The converse of substitution closure fails: there exist a language L and substitution f where L.subst f is CF but the premises is_CF L ∧ ∀ a, is_CF (f a) fail.