theorem RegularLanguages.foldl_sink {α : Type u_1} [DecidableEq α] (a₀ : α) (l : List α) : List.foldl (fun (s : Fin 3) (c : α) => if s = 0 ∧ c = a₀ then 1 else 2) 2 l = 2

Once the 3-state DFA used in isRegular_char enters the "sink" state 2, it stays there: folding the transition function over any list l starting at state 2 returns 2.

theorem RegularLanguages.foldl_bool_sink {α : Type u_1} (l : List α) : List.foldl (fun (x : Bool) (x_1 : α) => false) false l = false

Folding the constant-false transition over any list starting at false yields false; used as a sink-state lemma for the ε automaton in isRegular_epsilon.

theorem RegularLanguages.isRegular_empty {α : Type u_1} : Language.IsRegular 0

The empty language ∅ (a.k.a. 0) is regular: a one-state DFA with no accept states recognizes it.

theorem RegularLanguages.isRegular_epsilon {α : Type u_1} : Language.IsRegular 1

The language {ε} containing only the empty string (a.k.a. 1) is regular: a two-state DFA with start state true ∈ F and a sink state false recognizes it.

theorem RegularLanguages.isRegular_char {α : Type u_1} [DecidableEq α] (a₀ : α) : {[a₀]}.IsRegular

The singleton language {[a₀]} containing only the length-one string a₀ is regular: a three-state DFA with states 0 (start), 1 (accept), 2 (sink) and the obvious transitions recognizes it.

theorem RegularLanguages.regex_language_isRegular {α : Type u_1} [DecidableEq α] (R : RegularExpression α) : R.matches'.IsRegular

Regular expressions to regular languages.

For any regular expression R over α, the language L(R) = R.matches' is regular. The proof is by structural induction on R, using the base cases isRegular_empty, isRegular_epsilon, isRegular_char and the closure theorems IsRegular.add (union), regular_concat (concatenation), and regular_star (Kleene star).

This corresponds to Sipser's theorem: If R is a regular expression and A = L(R) then A is regular.