Closure Properties of Context-Free Languages

CFLs are closed under several operations relevant to non-context-freeness arguments: string homomorphism, intersection with regular languages, and reversal. Mathlib (as of this writing) proves only Language.IsContextFree.reverse; homomorphism closure is proved in Map.lean (Language.IsContextFree.stringMap) and intersection-with-regular closure is proved in InterRegular.lean (Language.IsContextFree.inter_isRegular, via the Bar-Hillel triple-product). This file owns the contrapositive corollaries that consume both.

What this file enables

The contrapositive corollaries (the useful direction for non-CF arguments) ARE proved here:

• Language.not_isContextFree_of_stringMap_not — if a homomorphic image is not context-free, neither is the source.
• Language.not_isContextFree_of_inter_regular_not — if L ∩ R is not context-free for some regular R, neither is L.
• Language.not_isContextFree_via_witness — the packaged @cite{shieber-1985} proof schema: argue L is non-CF by mapping it through a homomorphism, intersecting with a regular filter, and exhibiting a non-CF witness in the result. Used by Swiss German non-CF (Shieber 1985), Dutch non-CF (Huybregts 1976 / Bresnan et al. 1982), and any future natural-language non-CF argument.

@[simp]

theorem Language.stringMap_letterMap {α : Type u_1} {β : Type u_2} (f : α → β) (L : Language α) : stringMap (Core.StringHom.letterMap f) L = (map f) L

Bridge to mathlib's Language.map. When h is the letter-to-letter StringHom.letterMap f (each input symbol → singleton output), the homomorphic image collapses to mathlib's Language.map f, the letter-by-letter image. Lifts mathlib's existing ringHom structure to the letter-map case of stringMap automatically.

theorem Language.not_isContextFree_of_stringMap_not {α : Type u_1} {β : Type u_2} (h : Core.StringHom α β) {L : Language α} (hImg : ¬(stringMap h L).IsContextFree) : ¬L.IsContextFree

Contrapositive of homomorphism closure: if the homomorphic image of L is not context-free, then L is not context-free.

theorem Language.not_isContextFree_of_inter_regular_not {α : Type u_1} {L R : Language α} (hR : R.IsRegular) (hInter : ¬(L ⊓ R).IsContextFree) : ¬L.IsContextFree

Contrapositive of regular-intersection closure: if L ∩ R is not context-free for some regular R, then L is not context-free.

theorem Language.not_isContextFree_via_witness {α : Type u_1} {β : Type u_2} (h : Core.StringHom α β) (R : Language β) {L : Language α} (hR : R.IsRegular) (hWitness : ¬(stringMap h L ⊓ R).IsContextFree) : ¬L.IsContextFree

The Shieber-style non-context-freeness proof schema. If the homomorphic image of L intersected with a regular language R contains a non-context-free witness, then L is not context-free.

This is the proof shape used by @cite{shieber-1985} for Swiss German, closely paralleled by @cite{huybregts-1976} for Dutch, and applicable to any future natural-language non-CF argument that proceeds via homomorphic abstraction (e.g., case-marker-only projection) plus regular filtering (e.g., case-sorted clause shape).