Regular Languages Included in Context-Free Languages

This file proves that every right-regular language is context-free.

Main results

• is_CF_of_is_RG — every regular language is context-free
• RG_subclass_CF — RG ⊆ CF

def CF_grammar_of_RG {T : Type} (g : RG_grammar T) : CF_grammar T

Convert a right-regular grammar to a context-free grammar.

Equations

• CF_grammar_of_RG g = { nt := g.nt, initial := g.initial, rules := List.map (fun (r : RG_rule T g.nt) => (r.lhs, r.output)) g.rules }

theorem CF_transforms_of_RG_transforms {T : Type} {g : RG_grammar T} {w₁ w₂ : List (symbol T g.nt)} (h : RG_transforms g w₁ w₂) : CF_transforms (CF_grammar_of_RG g) w₁ w₂

theorem RG_transforms_of_CF_transforms {T : Type} {g : RG_grammar T} {w₁ w₂ : List (symbol T g.nt)} (h : CF_transforms (CF_grammar_of_RG g) w₁ w₂) : RG_transforms g w₁ w₂

theorem RG_derives_iff_CF_derives {T : Type} (g : RG_grammar T) (w₁ w₂ : List (symbol T g.nt)) : RG_derives g w₁ w₂ ↔ CF_derives (CF_grammar_of_RG g) w₁ w₂

theorem is_CF_of_is_RG {T : Type} {L : Language T} (h : is_RG L) : is_CF L

Every right-regular language is context-free.

theorem RG_subclass_CF {T : Type} : RG ⊆ CF