Intersection of Context-Free and Regular Languages

This file proves that the intersection of a context-free language with a regular language is context-free. This is a classic result in formal language theory, proved via the product construction of a CFG and a DFA.

Proof idea: thread DFA states through the nonterminals of the context-free grammar. A product nonterminal records both the original grammar symbol and the DFA state change that the substring generated by that symbol must realize, so a complete derivation exists exactly when the CFG derives the word and the DFA accepts it.

Main declarations

• CF_of_CF_inter_regular : the main theorem
• productGrammar : the product CFG×DFA grammar construction

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

CF_derivesIn g n w₁ w₂ means g transforms w₁ to w₂ in exactly n steps. Uses tail convention (matching ReflTransGen).

• refl {T : Type} {g : CF_grammar T} (w : List (symbol T g.nt)) : CF_derivesIn g 0 w w
• tail {T : Type} {g : CF_grammar T} {n : ℕ} {w₁ w₂ w₃ : List (symbol T g.nt)} : CF_derivesIn g n w₁ w₂ → CF_transforms g w₂ w₃ → CF_derivesIn g (n + 1) w₁ w₃

theorem CF_derivesIn_of_derives {T : Type} {g : CF_grammar T} {w₁ w₂ : List (symbol T g.nt)} (h : CF_derives g w₁ w₂) : ∃ (n : ℕ), CF_derivesIn g n w₁ w₂

theorem CF_derivesIn_head {T : Type} {g : CF_grammar T} {n : ℕ} {w₁ w₃ : List (symbol T g.nt)} (h : CF_derivesIn g (n + 1) w₁ w₃) : ∃ (w₂ : List (symbol T g.nt)), CF_transforms g w₁ w₂ ∧ CF_derivesIn g n w₂ w₃

theorem CF_derivesIn_append_split {T : Type} {g : CF_grammar T} {n : ℕ} {p q w : List (symbol T g.nt)} (h : CF_derivesIn g n (p ++ q) w) : ∃ (x : List (symbol T g.nt)) (y : List (symbol T g.nt)) (n₁ : ℕ) (n₂ : ℕ), w = x ++ y ∧ CF_derivesIn g n₁ p x ∧ CF_derivesIn g n₂ q y ∧ n = n₁ + n₂

noncomputable def threadSymbols {T σ : Type} [Fintype σ] (M : DFA T σ) {N : Type} (syms : List (symbol T N)) (p : σ) : List (List (symbol T (Option (σ × N × σ))) × σ)

Thread DFA states through a list of symbols, enumerating all valid annotated symbol lists with their ending DFA states.

Equations

• One or more equations did not get rendered due to their size.
• threadSymbols M [] p = [([], p)]

noncomputable def productGrammar {T σ : Type} [Fintype σ] (g : CF_grammar T) (M : DFA T σ) : CF_grammar T

The product grammar of a CFG g and a DFA M.

Equations

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

@[simp]

theorem threadSymbols_nil {T σ : Type} [Fintype σ] (M : DFA T σ) {N : Type} (p : σ) : threadSymbols M [] p = [([], p)]

@[simp]

theorem threadSymbols_terminal {T σ : Type} [Fintype σ] (M : DFA T σ) {N : Type} (a : T) (rest : List (symbol T N)) (p : σ) : threadSymbols M (symbol.terminal a :: rest) p = List.map (fun (x : List (symbol T (Option (σ × N × σ))) × σ) => match x with | (out, q) => (symbol.terminal a :: out, q)) (threadSymbols M rest (M.step p a))

@[simp]

theorem threadSymbols_nonterminal {T σ : Type} [Fintype σ] (M : DFA T σ) {N : Type} (B : N) (rest : List (symbol T N)) (p : σ) : threadSymbols M (symbol.nonterminal B :: rest) p = List.flatMap (fun (qmid : σ) => List.map (fun (x : List (symbol T (Option (σ × N × σ))) × σ) => match x with | (out, q) => (symbol.nonterminal (some (p, B, qmid)) :: out, q)) (threadSymbols M rest qmid)) Finset.univ.toList

theorem CF_derivesIn_terminal_zero {T : Type} {g' : CF_grammar T} {n : ℕ} {a : T} {w : List (symbol T g'.nt)} (h : CF_derivesIn g' n [symbol.terminal a] w) : n = 0 ∧ w = [symbol.terminal a]

theorem append_eq_map_terminal {T N : Type} {u v : List (symbol T N)} {w : List T} (h : u ++ v = List.map symbol.terminal w) : ∃ (w₁ : List T) (w₂ : List T), u = List.map symbol.terminal w₁ ∧ v = List.map symbol.terminal w₂ ∧ w = w₁ ++ w₂

theorem forward_thread {T : Type} {g : CF_grammar T} {σ : Type} [Fintype σ] {M : DFA T σ} (N_bound : ℕ) (syms : List (symbol T g.nt)) (out : List (symbol T (Option (σ × g.nt × σ)))) (p q : σ) (w : List T) (n : ℕ) (hn : n < N_bound) (hthread : (out, q) ∈ threadSymbols M syms p) (hder : CF_derivesIn (productGrammar g M) n out (List.map symbol.terminal w)) (ih : ∀ k < N_bound, ∀ (p' : σ) (A' : g.nt) (q' : σ) (w' : List T), CF_derivesIn (productGrammar g M) k [symbol.nonterminal (some (p', A', q'))] (List.map symbol.terminal w') → CF_derives g [symbol.nonterminal A'] (List.map symbol.terminal w') ∧ M.evalFrom p' w' = q') : CF_derives g syms (List.map symbol.terminal w) ∧ M.evalFrom p w = q

theorem forward_key {T : Type} {g : CF_grammar T} {σ : Type} [Fintype σ] {M : DFA T σ} (n : ℕ) (p : σ) (A : g.nt) (q : σ) (w : List T) (hder : CF_derivesIn (productGrammar g M) n [symbol.nonterminal (some (p, A, q))] (List.map symbol.terminal w)) : CF_derives g [symbol.nonterminal A] (List.map symbol.terminal w) ∧ M.evalFrom p w = q

theorem backward_thread_nil {T : Type} {g : CF_grammar T} {σ : Type} {_M : DFA T σ} (w : List T) (p : σ) (n : ℕ) (hder : CF_derivesIn g n [] (List.map symbol.terminal w)) : w = [] ∧ n = 0

theorem backward_thread {T : Type} {g : CF_grammar T} {σ : Type} [Fintype σ] {M : DFA T σ} (N_bound : ℕ) (syms : List (symbol T g.nt)) (w : List T) (p : σ) (n : ℕ) (hn : n < N_bound) (hder : CF_derivesIn g n syms (List.map symbol.terminal w)) (ih : ∀ k < N_bound, ∀ (B : g.nt) (w' : List T) (p' q' : σ), CF_derivesIn g k [symbol.nonterminal B] (List.map symbol.terminal w') → M.evalFrom p' w' = q' → CF_derives (productGrammar g M) [symbol.nonterminal (some (p', B, q'))] (List.map symbol.terminal w')) : ∃ (out : List (symbol T (Option (σ × g.nt × σ)))) (q : σ), (out, q) ∈ threadSymbols M syms p ∧ q = M.evalFrom p w ∧ CF_derives (productGrammar g M) out (List.map symbol.terminal w)

theorem productGrammar_language {T σ : Type} [Fintype σ] (g : CF_grammar T) (M : DFA T σ) : CF_language (productGrammar g M) = CF_language g ⊓ M.accepts

theorem CF_of_CF_inter_regular {T : Type} {L₁ L₂ : Language T} (h₁ : is_CF L₁) (h₂ : L₂.IsRegular) : is_CF (L₁ ⊓ L₂)

theorem CF_closedUnderIntersectionWithRegular {T : Type} : ClosedUnderIntersectionWithRegular is_CF

The class of context-free languages is closed under intersection with regular languages.