EncodedRG characterizes the regular languages

This file proves that the right-regular-grammar encoding EncodedRG denotes exactly the regular languages:

∀ L, L.IsRegular ↔ ∃ c : EncodedRG T, regularLanguageOf c = L

Soundness (every code denotes a regular language): an EncodedRG decodes — by construction — to a right-regular grammar toRG c whose RG_language equals regularLanguageOf c (both are the context-free language of the same underlying context-free grammar, via CF_grammar_of_RG). Hence the language is is_RG, so IsRegular.

def Regular.EncodedRG.rgRuleOf {T : Type} (c : EncodedRG T) (r : ℕ × Option (T × Option ℕ)) : RG_rule T (Fin c.toCFG.ntCount)

The right-regular grammar denoted by an encoded right-regular grammar: it reads each rule body back as a right-regular rule over the nonterminals Fin (toCFG c).ntCount.

Equations

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

def Regular.EncodedRG.toRG {T : Type} (c : EncodedRG T) : RG_grammar T

Decode an encoded right-regular grammar to a RG_grammar.

Equations

• c.toRG = { nt := Fin c.toCFG.ntCount, initial := c.toCFG.toNT c.toCFG.initialIdx, rules := List.map c.rgRuleOf c.2.2 }

theorem Regular.EncodedRG.cfGrammarOf_toRG {T : Type} (c : EncodedRG T) : CF_grammar_of_RG c.toRG = c.toCFG.toCFGrammar

The context-free grammar of toRG c is exactly the context-free grammar that regularLanguageOf already uses, namely (toCFG c).toCFGrammar.

theorem Regular.EncodedRG.rgLanguage_toRG {T : Type} (c : EncodedRG T) : RG_language c.toRG = c.regularLanguageOf

RG_language of toRG c is the language denoted by the code.

theorem Regular.EncodedRG.regularLanguageOf_isRegular {T : Type} [Fintype T] (c : EncodedRG T) : c.regularLanguageOf.IsRegular

Soundness: every code denotes a regular language.

Completeness: every regular language is encoded

def Regular.EncodedRG.rgRuleToBody {T : Type} {k : ℕ} : RG_rule T (Fin (k + 1)) → ℕ × Option (T × Option ℕ)

Encode a right-regular rule (over Fin (k+1)) back into the EncodedRG body format.

Equations

• Regular.EncodedRG.rgRuleToBody (RG_rule.cons A a B) = (↑A, some (a, some ↑B))
• Regular.EncodedRG.rgRuleToBody (RG_rule.single A a) = (↑A, some (a, none))
• Regular.EncodedRG.rgRuleToBody (RG_rule.epsilon A) = (↑A, none)

theorem Regular.EncodedRG.toNT_self {T : Type} (c : EncodedRG T) (A : Fin c.toCFG.ntCount) : c.toCFG.toNT ↑A = A

toNT is the identity on indices already in range.

theorem Regular.EncodedRG.rgRuleOf_rgRuleToBody {T : Type} (c : EncodedRG T) (r : RG_rule T (Fin c.toCFG.ntCount)) : c.rgRuleOf (rgRuleToBody r) = r

noncomputable def Regular.EncodedRG.encodeDFA {T : Type} [Fintype T] {k : ℕ} (M : DFA T (Fin (k + 1))) [DecidablePred fun (x : Fin (k + 1)) => x ∈ M.accept] : EncodedRG T

Encode a DFA over Fin (k+1) as a right-regular code.

Equations

• Regular.EncodedRG.encodeDFA M = (k, ↑M.start, List.map Regular.EncodedRG.rgRuleToBody (RG_of_DFA M).rules)

theorem Regular.EncodedRG.toRG_encodeDFA {T : Type} [Fintype T] {k : ℕ} (M : DFA T (Fin (k + 1))) [DecidablePred fun (x : Fin (k + 1)) => x ∈ M.accept] : (encodeDFA M).toRG = RG_of_DFA M

Decoding the encoding of a DFA recovers RG_of_DFA.

theorem Regular.EncodedRG.regularLanguageOf_complete {T : Type} [Fintype T] (L : Language T) (hL : L.IsRegular) : ∃ (c : EncodedRG T), c.regularLanguageOf = L

Completeness: every regular language is denoted by some code.

theorem Regular.EncodedRG.regularLanguageOf_characterizes {T : Type} [Fintype T] : Characterizes RG regularLanguageOf

EncodedRG characterizes the regular languages (the library's class RG).