Context-Free Closure Under Prefix and Suffix

This file proves that context-free languages are closed under the prefix and suffix operations. This strategy uses the construction of an explicit prefix grammar.

Main declarations

• CF_of_prefix_CF — CFLs are closed under prefix
• CF_of_suffix_CF — CFLs are closed under suffix (via reverse, prefix, reverse)

Strategy

The prefix closure proof constructs an explicit grammar. Given a CF grammar g, we build a "prefix grammar" whose nonterminals are Bool × g.nt, where (false, A) ("full mode") behaves like the original A, and (true, A) ("prefix mode") can derive any prefix of any word derivable from A.

To ensure soundness, we first filter the grammar to keep only "fully productive" rules (rules where every nonterminal in the RHS can derive some terminal string). This filtered grammar generates the same language as the original.

Productivity

def productive {T : Type} (g : CF_grammar T) (A : g.nt) : Prop

A nonterminal A in grammar g is productive if it can derive some terminal string.

Equations

• productive g A = ∃ (w : List T), CF_derives g [symbol.nonterminal A] (List.map symbol.terminal w)

def fullyProductiveRule {T : Type} (g : CF_grammar T) (r : g.nt × List (symbol T g.nt)) : Prop

A rule is fully productive if the LHS nonterminal and every nonterminal in the RHS are productive.

Equations

• fullyProductiveRule g r = (productive g r.1 ∧ ∀ (B : g.nt), symbol.nonterminal B ∈ r.2 → productive g B)

theorem productive_of_mem_derives_terminal {T : Type} {g : CF_grammar T} {s : List (symbol T g.nt)} {w : List T} (hs : CF_derives g s (List.map symbol.terminal w)) {B : g.nt} (hB : symbol.nonterminal B ∈ s) : productive g B

Productive Grammar

noncomputable def productiveGrammar {T : Type} (g : CF_grammar T) : CF_grammar T

Grammar with only fully productive rules (same nonterminal type, fewer rules).

Equations

• productiveGrammar g = { nt := g.nt, initial := g.initial, rules := List.filter (fun (r : g.nt × List (symbol T g.nt)) => decide (fullyProductiveRule g r)) g.rules }

theorem productiveGrammar_rules_productive {T : Type} {g : CF_grammar T} {r : (productiveGrammar g).nt × List (symbol T (productiveGrammar g).nt)} (hr : r ∈ (productiveGrammar g).rules) : fullyProductiveRule g r

theorem CF_derives_mono {T : Type} {g : CF_grammar T} {rules₁ rules₂ : List (g.nt × List (symbol T g.nt))} (hsub : ∀ r ∈ rules₁, r ∈ rules₂) {s₁ s₂ : List (symbol T g.nt)} (h : CF_derives { nt := g.nt, initial := g.initial, rules := rules₁ } s₁ s₂) : CF_derives { nt := g.nt, initial := g.initial, rules := rules₂ } s₁ s₂

theorem productive_iff_productiveGrammar {T : Type} {g : CF_grammar T} {A : g.nt} : productive g A ↔ productive (productiveGrammar g) A

theorem productiveGrammar_language {T : Type} (g : CF_grammar T) : CF_language (productiveGrammar g) = CF_language g

theorem productiveGrammar_allRulesFullyProductive {T : Type} (g : CF_grammar T) (r : (productiveGrammar g).nt × List (symbol T (productiveGrammar g).nt)) (hr : r ∈ (productiveGrammar g).rules) (B : (productiveGrammar g).nt) : symbol.nonterminal B ∈ r.2 → productive (productiveGrammar g) B

All rules in the productive grammar are fully productive (with respect to the productive grammar itself).

Prefix Grammar Construction

Stepped Derivations (for induction on step count)

def CF_derives_in {T : Type} (g : CF_grammar T) : ℕ → List (symbol T g.nt) → List (symbol T g.nt) → Prop

Derivation in exactly n steps.

Equations

• CF_derives_in g 0 x✝¹ x✝ = (x✝¹ = x✝)
• CF_derives_in g n.succ x✝¹ x✝ = ∃ (w₂ : List (symbol T g.nt)), CF_transforms g x✝¹ w₂ ∧ CF_derives_in g n w₂ x✝

theorem derives_of_derives_in {T : Type} {g : CF_grammar T} {n : ℕ} {w₁ w₂ : List (symbol T g.nt)} : CF_derives_in g n w₁ w₂ → CF_derives g w₁ w₂

theorem derives_in_of_derives {T : Type} {g : CF_grammar T} {w₁ w₂ : List (symbol T g.nt)} : CF_derives g w₁ w₂ → ∃ (n : ℕ), CF_derives_in g n w₁ w₂

theorem transform_in_append {T : Type} {g : CF_grammar T} {s₁ s₂ w : List (symbol T g.nt)} (h : CF_transforms g (s₁ ++ s₂) w) : (∃ (s₁' : List (symbol T g.nt)), CF_transforms g s₁ s₁' ∧ w = s₁' ++ s₂) ∨ ∃ (s₂' : List (symbol T g.nt)), CF_transforms g s₂ s₂' ∧ w = s₁ ++ s₂'

theorem head_tail_split_in {T : Type} {g : CF_grammar T} (n : ℕ) (s : symbol T g.nt) (ss x : List (symbol T g.nt)) (h : CF_derives_in g n (s :: ss) x) : ∃ (n₁ : ℕ) (n₂ : ℕ), n₁ + n₂ ≤ n ∧ ∃ (u : List (symbol T g.nt)) (v : List (symbol T g.nt)), CF_derives_in g n₁ [s] u ∧ CF_derives_in g n₂ ss v ∧ u ++ v = x

Full Lifting

Completeness: prefixLang (CF_language g) ⊆ CF_language (prefixGrammar g)

Soundness: CF_language (prefixGrammar g) ⊆ prefixLang (CF_language g)

This section assumes all rules in g are fully productive (every nonterminal appearing in any rule can derive some terminal string).

Main Theorems

theorem CF_of_prefix_CF {T : Type} (L : Language T) : is_CF L → is_CF L.prefixLang

The class of context-free languages is closed under taking prefixes.