Deterministic Finite Automata

This file contains the definition of a Deterministic Finite Automaton (DFA), a state machine which determines whether a string (implemented as a list over an arbitrary alphabet) is in a regular set in linear time. Note that this definition allows for Automaton with infinite states, a Fintype instance must be supplied for true DFA's.

Implementation notes

Currently, there are two disjoint sets of simp lemmas: one for DFA.eval, and another for DFA.evalFrom. You can switch from the former to the latter using simp [eval].

TODO

• Should we unify these simp sets, such that eval is rewritten to evalFrom automatically?
• Should mem_accepts and mem_acceptsFrom be marked @[simp]?

structure DFA (α : Type u) (σ : Type v) : Type (max u v)

A DFA is a set of states (σ), a transition function from state to state labelled by the alphabet (step), a starting state (start) and a set of acceptance states (accept).

• step : σ → α → σ

  A transition function from state to state labelled by the alphabet.

• start : σ

  Starting state.

• accept : Set σ

  Set of acceptance states.

instance DFA.instInhabited {α : Type u} {σ : Type v} [Inhabited σ] : Inhabited (DFA α σ)

Equations

• DFA.instInhabited = { default := { step := fun (x : σ) (x : α) => default, start := default, accept := ∅ } }

def DFA.evalFrom {α : Type u} {σ : Type v} (M : DFA α σ) (s : σ) : List α → σ

M.evalFrom s x evaluates M with input x starting from the state s.

Equations

• M.evalFrom s = List.foldl M.step s

@[simp]

theorem DFA.evalFrom_nil {α : Type u} {σ : Type v} (M : DFA α σ) (s : σ) : M.evalFrom s [] = s

@[simp]

theorem DFA.evalFrom_singleton {α : Type u} {σ : Type v} (M : DFA α σ) (s : σ) (a : α) : M.evalFrom s [a] = M.step s a

@[simp]

theorem DFA.evalFrom_append_singleton {α : Type u} {σ : Type v} (M : DFA α σ) (s : σ) (x : List α) (a : α) : M.evalFrom s (x ++ [a]) = M.step (M.evalFrom s x) a

def DFA.eval {α : Type u} {σ : Type v} (M : DFA α σ) : List α → σ

M.eval x evaluates M with input x starting from the state M.start.

Equations

• M.eval = M.evalFrom M.start

@[simp]

theorem DFA.eval_nil {α : Type u} {σ : Type v} (M : DFA α σ) : M.eval [] = M.start

@[simp]

theorem DFA.eval_singleton {α : Type u} {σ : Type v} (M : DFA α σ) (a : α) : M.eval [a] = M.step M.start a

@[simp]

theorem DFA.eval_append_singleton {α : Type u} {σ : Type v} (M : DFA α σ) (x : List α) (a : α) : M.eval (x ++ [a]) = M.step (M.eval x) a

theorem DFA.evalFrom_of_append {α : Type u} {σ : Type v} (M : DFA α σ) (start : σ) (x : List α) (y : List α) : M.evalFrom start (x ++ y) = M.evalFrom (M.evalFrom start x) y

def DFA.acceptsFrom {α : Type u} {σ : Type v} (M : DFA α σ) (s : σ) : Language α

M.acceptsFrom s is the language of x such that M.evalFrom s x is an accept state.

Equations

• M.acceptsFrom s = {x : List α | M.evalFrom s x ∈ M.accept}

theorem DFA.mem_acceptsFrom {α : Type u} {σ : Type v} (M : DFA α σ) {s : σ} {x : List α} : x ∈ M.acceptsFrom s ↔ M.evalFrom s x ∈ M.accept

def DFA.accepts {α : Type u} {σ : Type v} (M : DFA α σ) : Language α

M.accepts is the language of x such that M.eval x is an accept state.

Equations

• M.accepts = M.acceptsFrom M.start

theorem DFA.mem_accepts {α : Type u} {σ : Type v} (M : DFA α σ) {x : List α} : x ∈ M.accepts ↔ M.eval x ∈ M.accept

theorem DFA.evalFrom_split {α : Type u} {σ : Type v} (M : DFA α σ) [Fintype σ] {x : List α} {s : σ} {t : σ} (hlen : Fintype.card σ ≤ x.length) (hx : M.evalFrom s x = t) : ∃ (q : σ) (a : List α) (b : List α) (c : List α), x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t

theorem DFA.evalFrom_of_pow {α : Type u} {σ : Type v} (M : DFA α σ) {x : List α} {y : List α} {s : σ} (hx : M.evalFrom s x = s) (hy : y ∈ KStar.kstar {x}) : M.evalFrom s y = s

theorem DFA.pumping_lemma {α : Type u} {σ : Type v} (M : DFA α σ) [Fintype σ] {x : List α} (hx : x ∈ M.accepts) (hlen : Fintype.card σ ≤ x.length) : ∃ (a : List α) (b : List α) (c : List α), x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ {a} * KStar.kstar {b} * {c} ≤ M.accepts

@[simp]

theorem DFA.comap_start {α : Type u} {σ : Type v} {α' : Type u_1} (f : α' → α) (M : DFA α σ) : (DFA.comap f M).start = M.start

@[simp]

theorem DFA.comap_accept {α : Type u} {σ : Type v} {α' : Type u_1} (f : α' → α) (M : DFA α σ) : (DFA.comap f M).accept = M.accept

@[simp]

theorem DFA.comap_step {α : Type u} {σ : Type v} {α' : Type u_1} (f : α' → α) (M : DFA α σ) (s : σ) (a : α') : (DFA.comap f M).step s a = M.step s (f a)

def DFA.comap {α : Type u} {σ : Type v} {α' : Type u_1} (f : α' → α) (M : DFA α σ) : DFA α' σ

M.comap f pulls back the alphabet of M along f. In other words, it applies f to the input before passing it to M.

Equations

• DFA.comap f M = { step := fun (s : σ) (a : α') => M.step s (f a), start := M.start, accept := M.accept }

@[simp]

theorem DFA.comap_id {α : Type u} {σ : Type v} (M : DFA α σ) : DFA.comap id M = M

@[simp]

theorem DFA.evalFrom_comap {α : Type u} {σ : Type v} (M : DFA α σ) {α' : Type u_1} (f : α' → α) (s : σ) (x : List α') : (DFA.comap f M).evalFrom s x = M.evalFrom s (List.map f x)

@[simp]

theorem DFA.eval_comap {α : Type u} {σ : Type v} (M : DFA α σ) {α' : Type u_1} (f : α' → α) (x : List α') : (DFA.comap f M).eval x = M.eval (List.map f x)

@[simp]

theorem DFA.accepts_comap {α : Type u} {σ : Type v} (M : DFA α σ) {α' : Type u_1} (f : α' → α) : (DFA.comap f M).accepts = List.map f ⁻¹' M.accepts

@[simp]

theorem DFA.reindex_apply_start {α : Type u} {σ : Type v} {σ' : Type u_2} (g : σ ≃ σ') (M : DFA α σ) : ((DFA.reindex g) M).start = g M.start

@[simp]

theorem DFA.reindex_apply_step {α : Type u} {σ : Type v} {σ' : Type u_2} (g : σ ≃ σ') (M : DFA α σ) (s : σ') (a : α) : ((DFA.reindex g) M).step s a = g (M.step (g.symm s) a)

@[simp]

theorem DFA.reindex_apply_accept {α : Type u} {σ : Type v} {σ' : Type u_2} (g : σ ≃ σ') (M : DFA α σ) : ((DFA.reindex g) M).accept = ⇑g.symm ⁻¹' M.accept

def DFA.reindex {α : Type u} {σ : Type v} {σ' : Type u_2} (g : σ ≃ σ') : DFA α σ ≃ DFA α σ'

Lifts an equivalence on states to an equivalence on DFAs.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem DFA.reindex_refl {α : Type u} {σ : Type v} (M : DFA α σ) : (DFA.reindex (Equiv.refl σ)) M = M

@[simp]

theorem DFA.symm_reindex {α : Type u} {σ : Type v} {σ' : Type u_2} (g : σ ≃ σ') : (DFA.reindex g).symm = DFA.reindex g.symm

@[simp]

theorem DFA.evalFrom_reindex {α : Type u} {σ : Type v} (M : DFA α σ) {σ' : Type u_2} (g : σ ≃ σ') (s : σ') (x : List α) : ((DFA.reindex g) M).evalFrom s x = g (M.evalFrom (g.symm s) x)

@[simp]

theorem DFA.eval_reindex {α : Type u} {σ : Type v} (M : DFA α σ) {σ' : Type u_2} (g : σ ≃ σ') (x : List α) : ((DFA.reindex g) M).eval x = g (M.eval x)

@[simp]

theorem DFA.accepts_reindex {α : Type u} {σ : Type v} (M : DFA α σ) {σ' : Type u_2} (g : σ ≃ σ') : ((DFA.reindex g) M).accepts = M.accepts

theorem DFA.comap_reindex {α : Type u} {σ : Type v} (M : DFA α σ) {α' : Type u_1} {σ' : Type u_2} (f : α' → α) (g : σ ≃ σ') : DFA.comap f ((DFA.reindex g) M) = (DFA.reindex g) (DFA.comap f M)

def Language.IsRegular {T : Type u} (L : Language T) : Prop

A regular language is a language that is defined by a DFA with finite states.

Equations

• L.IsRegular = ∃ (σ : Type) (x : Fintype σ) (M : DFA T σ), M.accepts = L