Nondeterministic and Deterministic Finite Automata

This file packages Mathlib's subset construction as a language-class equivalence. Mathlib proves that NFA.toDFA and DFA.toNFA preserve accepted languages; here we add the corresponding Langlib recognizability predicate and class equality.

Main declarations

• is_NFA -- recognition by a finite-state nondeterministic automaton.
• is_NFA_iff_is_DFA -- NFAs and DFAs recognize the same languages.
• NFA_eq_DFA -- equality of the two language classes.

def is_NFA {T : Type} (L : Language T) : Prop

A language is NFA-recognizable if it is accepted by some nondeterministic finite automaton with a finite state type.

Equations

• is_NFA L = ∃ (σ : Type) (x : Fintype σ) (M : NFA T σ), M.accepts = L

def NFA.Class {T : Type} : Set (Language T)

The class of NFA-recognizable languages.

Equations

• NFA.Class = setOf is_NFA

theorem is_NFA_iff_is_DFA {T : Type} {L : Language T} : is_NFA L ↔ is_DFA L

Nondeterministic and deterministic finite automata recognize exactly the same languages.

theorem NFA_eq_DFA {T : Type} : NFA.Class = DFA.Class

Equality of the NFA- and DFA-recognizable language classes.