is_regular_iff_nfa
theoremverified
A language is regular if and only if it is accepted by a nondeterministic finite automaton with finitely many states.
Statement
theorem is_regular_iff_nfa {α : Type*} {L : Language α} : L.IsRegular ↔ ∃ (σ : Type) (_ : Fintype σ) (M : NFA α σ), M.accepts = L
- Source
- Sipser, Theorem 1.39
- Verified
- 07 Sep 2026
- Axioms
Classical.choiceQuot.soundpropext- Used by 1
- is_regular_iff_enfaA language is regular if and only if it is accepted by an epsilon-nondeterministic finite automaton with finitely many states.
Read back from the Lean
For any type α and any language L over α (L : Language α), L is regular (L.IsRegular) if and only if there exist a type σ (in Type 0), a proof/instance that σ is finite (Fintype σ), and a nondeterministic finite automaton M with alphabet α and state space σ (NFA α σ) such that the language accepted by M is equal to L (M.accepts = L).
Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.
Lean source view module on GitHub
/-- A language is regular if and only if it is accepted by a nondeterministic finite automaton with finitely many states. -/ theorem is_regular_iff_nfa {α : Type*} {L : Language α} : L.IsRegular ↔ ∃ (σ : Type) (_ : Fintype σ) (M : NFA α σ), M.accepts = L := by constructor · rintro ⟨σ, _, M, rfl⟩ exact ⟨σ, inferInstance, M.toNFA, M.toNFA_correct⟩ · rintro ⟨σ, _, M, rfl⟩ exact ⟨Set σ, inferInstance, M.toDFA, NFA.toDFA_correct⟩