CFL Pumping Lemma

The CFL pumping property (HasCFLPumpingProperty) is defined over mathlib's Language α (= Set (List α)).

Key Results

• cfl_pumping_lemma : L.IsContextFree → HasCFLPumpingProperty L — fully proved
• not_isContextFree_of_not_pumpable — contrapositive

Proof Structure

The proof follows the standard textbook argument via derivation trees:

1. exists_valid_tree ✓ (in CFGTree.lean)
2. yield_length_le_of_height ✓ (in CFGTree.lean)
3. pumping_from_tall_tree ✓: pigeonhole + subtree replacement + validFor_derives

def HasCFLPumpingProperty {α : Type u_1} (L : Language α) : Prop

The CFL pumping property for a language.

Every context-free language satisfies this property — the pumping lemma for CFLs. Showing a language lacks it proves it is not context-free.

Equations

• One or more equations did not get rendered due to their size.

theorem pumping_from_tall_tree {T : Type u_1} (g : ContextFreeGrammar T) (t : CFGTree T g.NT) (ht : CFGTree.ValidFor g t) (hroot : t.rootSymbol = Symbol.nonterminal g.initial) (hyield_long : t.yield.length ≥ g.pumpingConstant) : ∃ (u : List T) (v : List T) (x : List T) (y : List T) (z : List T), t.yield = u ++ v ++ x ++ y ++ z ∧ (v ++ x ++ y).length ≤ g.pumpingConstant ∧ v.length + y.length ≥ 1 ∧ ∀ (i : ℕ), u ++ (List.replicate i v).flatten ++ x ++ (List.replicate i y).flatten ++ z ∈ g.language

theorem cfl_pumping_lemma {T : Type u_1} (L : Language T) (hcf : L.IsContextFree) : HasCFLPumpingProperty L

The CFL pumping lemma. Every context-free language satisfies HasCFLPumpingProperty.

Proof: given a CFG g generating L, set p = g.pumpingConstant. For any w ∈ L with |w| ≥ p:

1. exists_valid_tree: w has a valid derivation tree t.
2. yield_length_le_of_height (contrapositive): |w| ≥ p = b^(k+1) forces t.height > k = g.rules.card.
3. pumping_from_tall_tree: the tall tree yields the decomposition.

theorem not_isContextFree_of_not_pumpable {T : Type u_1} (L : Language T) (h : ¬HasCFLPumpingProperty L) : ¬L.IsContextFree

Contrapositive of the CFL pumping lemma: if a language lacks the pumping property, it is not context-free.