def RegularIsCFL.dfaToPDA {α : Type u} {σ : Type u_1} (D : DFA α σ) : PDA α σ PUnit.{u_2 + 1}

Convert a DFA D to a PDA over the same input alphabet that ignores its stack (using a trivial stack alphabet PUnit). The PDA's transition mirrors D.step on real input symbols and has no ε-transitions or stack moves.

theorem RegularIsCFL.dfaToPDA_step_characterize {α : Type u} {σ : Type u_1} (D : DFA α σ) {c₁ c₂ : σ × List α × List PUnit.{u_2 + 1}} (h : (dfaToPDA D).Step c₁ c₂) : ∃ (a : α), c₁.2.1 = a :: c₂.2.1 ∧ c₂.1 = D.step c₁.1 a ∧ c₂.2.2 = c₁.2.2

Any one-step transition of dfaToPDA D consumes a single input symbol a, moves the DFA state via D.step, and leaves the stack unchanged.

theorem RegularIsCFL.dfaToPDA_reaches_evalFrom {α : Type u} {σ : Type u_1} (D : DFA α σ) (q : σ) (w : List α) : (dfaToPDA D).Reaches (q, w, []) (D.evalFrom q w, [], [])

Starting from any DFA state q with input w and empty stack, the PDA dfaToPDA D reaches the configuration (D.evalFrom q w, [], []) after consuming the entire input.

theorem RegularIsCFL.dfaToPDA_reaches_inv {α : Type u} {σ : Type u_1} (D : DFA α σ) {c₁ c₂ : σ × List α × List PUnit.{u_2 + 1}} (hreach : (dfaToPDA D).Reaches c₁ c₂) (hs : c₁.2.2 = []) : c₂.2.2 = [] ∧ ∃ (pref : List α), c₁.2.1 = pref ++ c₂.2.1 ∧ c₂.1 = D.evalFrom c₁.1 pref

Inverse direction: any reachable configuration of dfaToPDA D from an empty-stack start has empty stack, and the consumed input is a prefix of the remaining input that drives D.evalFrom from the start to the current state.

theorem RegularIsCFL.dfaToPDA_language {α : Type u} {σ : Type u_1} (D : DFA α σ) : (dfaToPDA D).language = D.accepts

The PDA dfaToPDA D recognizes exactly the language of the DFA D.

theorem RegularIsCFL.regular_is_cfl {α : Type u} {A : Language α} (h : A.IsRegular) : A.IsContextFree

Sipser, Corollary 1 of Lecture 5. Every regular language is context-free. The proof converts the recognizing DFA into a stack-ignoring PDA, then uses the equivalence of PDAs and CFGs.