Context-Free Definition Equivalence with Mathlib's ContextFreeGrammar

This file proves that the project's context-free predicate is_CF coincides with Mathlib's Language.IsContextFree. It defines translations mathlib_cfg_of_cfg and cfg_of_mathlib_cfg between the project's CF_grammar and Mathlib's ContextFreeGrammar, shows the generated languages agree (CF_language_eq_mathlib_language, by induction on the derivation relation in each direction), and concludes is_CF_iff_isContextFree.

Main declarations

• is_CF_iff_isContextFree

def Symbol_of_symbol {T N : Type} : symbol T N → Symbol T N

Equations

• Symbol_of_symbol (symbol.terminal t) = Symbol.terminal t
• Symbol_of_symbol (symbol.nonterminal n) = Symbol.nonterminal n

def symbol_of_Symbol {T N : Type} : Symbol T N → symbol T N

Equations

• symbol_of_Symbol (Symbol.terminal t) = symbol.terminal t
• symbol_of_Symbol (Symbol.nonterminal n) = symbol.nonterminal n

def lsSymbol_of_lssymbol {T N : Type} : List (symbol T N) → List (Symbol T N)

Equations

• lsSymbol_of_lssymbol = List.map Symbol_of_symbol

def lssymbol_of_lsSymbol {T N : Type} : List (Symbol T N) → List (symbol T N)

Equations

• lssymbol_of_lsSymbol = List.map symbol_of_Symbol

noncomputable def mathlib_cfg_of_cfg {T : Type} (g : CF_grammar T) : ContextFreeGrammar T

Equations

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

noncomputable def cfg_of_mathlib_cfg {T : Type} (g : ContextFreeGrammar T) : CF_grammar T

Equations

• cfg_of_mathlib_cfg g = { nt := g.NT, initial := g.initial, rules := List.map (fun (r : ContextFreeRule T g.NT) => (r.input, lssymbol_of_lsSymbol r.output)) g.rules.toList }

def CF_no_epsilon {T : Type} (g : CF_grammar T) : Prop

A context-free grammar has no ε-productions (every rule has a non-empty right-hand side).

Equations

• CF_no_epsilon g = ∀ r ∈ g.rules, r.2 ≠ []

theorem CF_language_eq_mathlib_language {T : Type} (g : CF_grammar T) : CF_language g = (mathlib_cfg_of_cfg g).language

theorem mathlib_cfg_of_cfg_of_mathlib_cfg {T : Type} (g : ContextFreeGrammar T) : mathlib_cfg_of_cfg (cfg_of_mathlib_cfg g) = g

theorem mathlib_language_eq_CF_language {T : Type} (g : ContextFreeGrammar T) : g.language = CF_language (cfg_of_mathlib_cfg g)

theorem is_CF_iff_isContextFree {T : Type} {L : Language T} : is_CF L ↔ L.IsContextFree