Regular languages

theorem Cslib.Language.IsRegular.iff_dfa {Symbol : Type u_1} {l : Language Symbol} : l.IsRegular ↔ ∃ (State : Type) (_ : Finite State) (dfa : Automata.DA.FinAcc State Symbol), Automata.Acceptor.language dfa = l

A characterization of Language.IsRegular in terms of DA. This is the only theorem in Cslib in which Mathlib's definition of Language.IsRegular is used.

theorem Cslib.Language.IsRegular.iff_nfa {Symbol : Type u_1} {l : Language Symbol} : l.IsRegular ↔ ∃ (State : Type) (_ : Finite State) (nfa : Automata.NA.FinAcc State Symbol), Automata.Acceptor.language nfa = l

A characterization of Language.IsRegular in terms of NA.

theorem Cslib.Language.IsRegular.compl {Symbol : Type u_1} {l : Language Symbol} (h : l.IsRegular) : lᶜ.IsRegular

The complementation of a regular language is regular.

@[simp]

theorem Cslib.Language.IsRegular.zero {Symbol : Type u_1} : Language.IsRegular 0

The empty language is regular.

@[simp]

theorem Cslib.Language.IsRegular.one {Symbol : Type u_1} : Language.IsRegular 1

The language containing only the empty word is regular.

@[simp]

theorem Cslib.Language.IsRegular.top {Symbol : Type u_1} : ⊤.IsRegular

The language of all finite words is regular.

@[simp]

theorem Cslib.Language.IsRegular.inf {Symbol : Type u_1} {l1 l2 : Language Symbol} (h1 : l1.IsRegular) (h2 : l2.IsRegular) : (l1 ⊓ l2).IsRegular

The intersection of two regular languages is regular.

@[simp]

theorem Cslib.Language.IsRegular.add {Symbol : Type u_1} {l1 l2 : Language Symbol} (h1 : l1.IsRegular) (h2 : l2.IsRegular) : (l1 + l2).IsRegular

The union of two regular languages is regular.

@[simp]

theorem Cslib.Language.IsRegular.iInf {Symbol : Type u_1} {I : Type u_2} [Finite I] {s : Set I} {l : I → Language Symbol} (h : ∀ i ∈ s, (l i).IsRegular) : (⨅ i ∈ s, l i).IsRegular

The intersection of any finite number of regular languages is regular.

@[simp]

theorem Cslib.Language.IsRegular.iSup {Symbol : Type u_1} {I : Type u_2} [Finite I] {s : Set I} {l : I → Language Symbol} (h : ∀ i ∈ s, (l i).IsRegular) : (⨆ i ∈ s, l i).IsRegular

The union of any finite number of regular languages is regular.

@[simp]

theorem Cslib.Language.IsRegular.mul {Symbol : Type u_1} [Inhabited Symbol] {l1 l2 : Language Symbol} (h1 : l1.IsRegular) (h2 : l2.IsRegular) : (l1 * l2).IsRegular

The concatenation of two regular languages is regular.

@[simp]

theorem Cslib.Language.IsRegular.kstar {Symbol : Type u_1} [Inhabited Symbol] {l : Language Symbol} (h : l.IsRegular) : (KStar.kstar l).IsRegular

The Kleene star of a regular language is regular.

@[simp]

theorem Cslib.Language.IsRegular.congr_fin_index {Symbol : Type} [c : RightCongruence Symbol] [Finite (Quotient c.eq)] (a : Quotient c.eq) : (RightCongruence.eqvCls a).IsRegular

If a right congruence is of finite index, then each of its equivalence classes is regular.