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.iff_epsilon_nfa {Symbol : Type u_1} {l : Language Symbol} : l.IsRegular ↔ ∃ (State : Type) (_ : Finite State) (enfa : Automata.εNA.FinAcc State Symbol), Automata.Acceptor.language enfa = 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.

theorem Cslib.Language.IsRegular.iff_twoWayNA {Symbol : Type u_1} {l : Language Symbol} : l.IsRegular ↔ ∃ (State : Type) (_ : Finite State) (a : Automata.TwoWayNA State Symbol), Automata.Acceptor.language a = l

A language is regular if and only if it is accepted by some two-way nondeterministic automaton with finitely many states.

@[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_3} [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_3} [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} {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} {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 : Language.RightCongruence Symbol] [Finite (Quotient c.eq)] (a : Quotient c.eq) : (Language.RightCongruence.eqvCls a).IsRegular

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

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

The reversal of a regular language is regular.

@[simp]

theorem Cslib.Language.IsRegular.reverse_iff {Symbol : Type u_1} {l : Language Symbol} : l.reverse.IsRegular ↔ l.IsRegular

A language is regular iff its reversal is regular.

theorem Cslib.Language.IsRegular.preimage {Symbol : Type u_1} {Symbol' : Type u_2} (f : Language.Hom Symbol' Symbol) {l : Language Symbol} (h : l.IsRegular) : (Language.preimage (⇑f) l).IsRegular

The preimage of a regular languge under a language homomorphism is regular.

@[simp]

theorem Cslib.Language.IsRegular.char {Symbol : Type u_1} (a : Symbol) : {[a]}.IsRegular

The language containing only the one character string a is regular.

theorem Cslib.Language.IsRegular.regex {Symbol : Type u_1} (r : RegularExpression Symbol) : r.matches'.IsRegular

Languages matching regular expressions are regular.

theorem Cslib.Language.IsRegular.iff_regex {Symbol : Type u_1} [Finite Symbol] {l : Language Symbol} : l.IsRegular ↔ ∃ (r : RegularExpression Symbol), l = r.matches'

A characterization of Language.IsRegular in terms of RegularExpression.