Right-regular grammars = Mathlib-regular languages

This file proves that right-regular grammars (Type-3) generate exactly Mathlib's Language.IsRegular languages, via explicit conversions in both directions.

Proof outline

• RG → IsRegular. NFA_of_RG g is an NFA over the finite state set Option g.FinNT (the nonterminals occurring in g, plus a sink none marking a completed word): A → aB gives A —a→ B, A → a gives A —a→ none, and the accepting states are none together with the nonterminals having an A → ε rule. Forward/backward simulation against RG_derives yields NFA_of_RG_accepts : (NFA_of_RG g).accepts = RG_language g; Mathlib's NFA.toDFA then gives isRegular_of_is_RG.
• IsRegular → RG. RG_of_DFA M reads a DFA's transitions as rules q → a (M.step q a) and adds q → ε for accepting states; the invariant RG_of_DFA_derives_inv gives RG_of_DFA_language, hence is_RG_of_isRegular.

Main results

• is_RG_iff_isRegular — The Mathlib regular languages are equivalent to the right-regular languages.
• RG_eq_DFA — equality of the two language classes (over a finite alphabet).

References

• Hopcroft, Motwani, Ullman. Introduction to Automata Theory, Languages, and Computation, 3rd ed. Section 3.3.

def RG_rule.nonterminals {T N : Type} : RG_rule T N → List N

All nonterminals mentioned in a single RG rule.

Equations

• (RG_rule.cons A a B).nonterminals = [A, B]
• (RG_rule.single A a).nonterminals = [A]
• (RG_rule.epsilon A).nonterminals = [A]

def RG_grammar.nonterminalFinset {T : Type} (g : RG_grammar T) : Finset g.nt

Finset of all nonterminals appearing in a grammar (including the initial symbol).

Equations

• g.nonterminalFinset = (g.initial :: List.flatMap RG_rule.nonterminals g.rules).toFinset

theorem RG_grammar.initial_mem_nonterminalFinset {T : Type} (g : RG_grammar T) : g.initial ∈ g.nonterminalFinset

theorem RG_grammar.rule_nt_mem {T : Type} (g : RG_grammar T) {r : RG_rule T g.nt} (hr : r ∈ g.rules) {n : g.nt} (hn : n ∈ r.nonterminals) : n ∈ g.nonterminalFinset

@[reducible, inline]

abbrev RG_grammar.FinNT {T : Type} (g : RG_grammar T) : Type

Finite nonterminal subtype: only those nonterminals that appear in the grammar.

Equations

• g.FinNT = { x : g.nt // x ∈ g.nonterminalFinset }

def NFA_of_RG {T : Type} (g : RG_grammar T) : NFA T (Option g.FinNT)

NFA with finite states constructed from a right-regular grammar.

Equations

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

theorem NFA_of_RG_some_forward {T : Type} {g : RG_grammar T} (A : g.nt) (hA : A ∈ g.nonterminalFinset) (B : g.nt) (hB : B ∈ g.nonterminalFinset) (w : List T) (h : some ⟨B, hB⟩ ∈ (NFA_of_RG g).evalFrom {some ⟨A, hA⟩} w) : RG_derives g [symbol.nonterminal A] (List.map symbol.terminal w ++ [symbol.nonterminal B])

theorem NFA_of_RG_none_forward {T : Type} {g : RG_grammar T} (A : g.nt) (hA : A ∈ g.nonterminalFinset) (w : List T) (h : none ∈ (NFA_of_RG g).evalFrom {some ⟨A, hA⟩} w) : RG_derives g [symbol.nonterminal A] (List.map symbol.terminal w)

theorem RG_derives_form {T : Type} {g : RG_grammar T} {A : g.nt} {s : List (symbol T g.nt)} (h : RG_derives g [symbol.nonterminal A] s) : (∃ (p : List T) (C : g.nt), s = List.map symbol.terminal p ++ [symbol.nonterminal C]) ∨ ∃ (p : List T), s = List.map symbol.terminal p

theorem RG_transforms_of_terminal_nt {T : Type} {g : RG_grammar T} {p : List T} {C : g.nt} {s : List (symbol T g.nt)} (h : RG_transforms g (List.map symbol.terminal p ++ [symbol.nonterminal C]) s) : (∃ (a : T) (D : g.nt), RG_rule.cons C a D ∈ g.rules ∧ s = List.map symbol.terminal p ++ [symbol.terminal a, symbol.nonterminal D]) ∨ (∃ (a : T), RG_rule.single C a ∈ g.rules ∧ s = List.map symbol.terminal p ++ [symbol.terminal a]) ∨ RG_rule.epsilon C ∈ g.rules ∧ s = List.map symbol.terminal p

theorem RG_derives_snoc {T : Type} {g : RG_grammar T} {A B : g.nt} {w : List T} (hw : w ≠ []) (h : RG_derives g [symbol.nonterminal A] (List.map symbol.terminal w ++ [symbol.nonterminal B])) : ∃ (C : g.nt), RG_derives g [symbol.nonterminal A] (List.map symbol.terminal w.dropLast ++ [symbol.nonterminal C]) ∧ RG_rule.cons C (w.getLast hw) B ∈ g.rules

theorem NFA_of_RG_some_backward {T : Type} {g : RG_grammar T} (A : g.nt) (hA : A ∈ g.nonterminalFinset) (B : g.nt) (hB : B ∈ g.nonterminalFinset) (w : List T) (h : RG_derives g [symbol.nonterminal A] (List.map symbol.terminal w ++ [symbol.nonterminal B])) : some ⟨B, hB⟩ ∈ (NFA_of_RG g).evalFrom {some ⟨A, hA⟩} w

theorem RG_generates_last_step {T : Type} {g : RG_grammar T} {A : g.nt} {w : List T} (h : RG_derives g [symbol.nonterminal A] (List.map symbol.terminal w)) : (∃ (C : g.nt) (p : List T), RG_derives g [symbol.nonterminal A] (List.map symbol.terminal p ++ [symbol.nonterminal C]) ∧ RG_rule.epsilon C ∈ g.rules ∧ w = p) ∨ ∃ (C : g.nt) (p : List T) (a : T), RG_derives g [symbol.nonterminal A] (List.map symbol.terminal p ++ [symbol.nonterminal C]) ∧ RG_rule.single C a ∈ g.rules ∧ w = p ++ [a]

theorem NFA_of_RG_accepts {T : Type} (g : RG_grammar T) : (NFA_of_RG g).accepts = RG_language g

theorem isRegular_of_is_RG {T : Type} {L : Language T} (h : is_RG L) : L.IsRegular

Every right-regular grammar language is Mathlib-regular.

def RG_of_DFA {T : Type} [Fintype T] {σ : Type} [Fintype σ] (M : DFA T σ) : RG_grammar T

Right-regular grammar constructed from a DFA over a finite alphabet.

Equations

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

theorem RG_of_DFA_cons_mem {T : Type} [Fintype T] {σ : Type} [Fintype σ] (M : DFA T σ) (q : σ) (a : T) : RG_rule.cons q a (M.step q a) ∈ (RG_of_DFA M).rules

theorem RG_of_DFA_epsilon_mem {T : Type} [Fintype T] {σ : Type} [Fintype σ] (M : DFA T σ) (q : σ) (hq : q ∈ M.accept) : RG_rule.epsilon q ∈ (RG_of_DFA M).rules

theorem RG_of_DFA_epsilon_mem_iff {T : Type} [Fintype T] {σ : Type} [Fintype σ] (M : DFA T σ) (q : σ) : RG_rule.epsilon q ∈ (RG_of_DFA M).rules ↔ q ∈ M.accept

theorem RG_of_DFA_derives_simulation {T : Type} [Fintype T] {σ : Type} [Fintype σ] (M : DFA T σ) (q : σ) (w : List T) : RG_derives (RG_of_DFA M) [symbol.nonterminal q] (List.map symbol.terminal w ++ [symbol.nonterminal (M.evalFrom q w)])

theorem RG_of_DFA_no_single {T : Type} [Fintype T] {σ : Type} [Fintype σ] (M : DFA T σ) (q : σ) (a : T) : RG_rule.single q a ∉ (RG_of_DFA M).rules

theorem RG_of_DFA_derives_inv {T : Type} [Fintype T] {σ : Type} [Fintype σ] (M : DFA T σ) (q : σ) (s : List (symbol T σ)) (h : RG_derives (RG_of_DFA M) [symbol.nonterminal q] s) : (∃ (p : List T), s = List.map symbol.terminal p ++ [symbol.nonterminal (M.evalFrom q p)]) ∨ ∃ (p : List T), s = List.map symbol.terminal p ∧ M.evalFrom q p ∈ M.accept

theorem RG_of_DFA_language {T : Type} [Fintype T] {σ : Type} [Fintype σ] (M : DFA T σ) : RG_language (RG_of_DFA M) = M.accepts

theorem is_RG_of_isRegular {T : Type} [Fintype T] {L : Language T} (h : L.IsRegular) : is_RG L

Every Mathlib-regular language over a finite alphabet is generated by a right-regular grammar.

theorem is_RG_iff_isRegular {T : Type} [Fintype T] {L : Language T} : is_RG L ↔ L.IsRegular

Right-regular grammars generate exactly the Mathlib-regular languages (over a finite alphabet).

theorem RG_eq_DFA {T : Type} [Fintype T] : RG = DFA.Class