is_regular_iff_enfa
theoremverified
A language is regular if and only if it is accepted by an epsilon-nondeterministic finite automaton with finitely many states.
Statement
theorem is_regular_iff_enfa {α : Type*} {L : Language α} : L.IsRegular ↔ ∃ (σ : Type) (_ : Fintype σ) (M : εNFA α σ), M.accepts = L
- Source
- Hopcroft, Motwani & Ullman, Theorem 2.13
- Verified
- 07 Sep 2026
- Axioms
Classical.choiceQuot.soundpropext- Built on 1
- is_regular_iff_nfaA language is regular if and only if it is accepted by a nondeterministic finite automaton with finitely many states.
- Used by 2
- is_regular_mulThe concatenation of two regular languages is regular.
- is_regular_kstarThe Kleene star of any regular language is regular.
Read back from the Lean
For any type α and any formal language L : Language α (i.e., L : Set (List α)), L is regular (L.IsRegular) if and only if there exists a type σ (in universe 0), a Fintype σ instance, and an ε-NFA M : εNFA α σ (a nondeterministic finite automaton with ε-transitions, alphabet α, and state type σ) 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 an epsilon-nondeterministic finite automaton with finitely many states. -/ theorem is_regular_iff_enfa {α : Type*} {L : Language α} : L.IsRegular ↔ ∃ (σ : Type) (_ : Fintype σ) (M : εNFA α σ), M.accepts = L := by rw [is_regular_iff_nfa] constructor · rintro ⟨σ, _, M, rfl⟩ exact ⟨σ, inferInstance, M.toεNFA, M.toεNFA_correct⟩ · rintro ⟨σ, _, M, rfl⟩ exact ⟨σ, inferInstance, M.toNFA, M.toNFA_correct⟩