FinDFA: Computable DFAs

This file defines structures FinDFA and AccessibleFinDFA, and a function FinDFA.toAccessible that converts a FinDFA to an AccessibleFinDFA. This function is proven to preserve the language accepted by FinDFA.toAccessible_pres_lang.

Main definitions

• FinDFA α σ - A DFA with alphabet α and state space σ. This is like DFA α σ, but with the accepting states given as a Finset σ rather than a Set σ.

• FinDFA.getWordsLeqLength (n : ℕ) - Returns a Finset of all words of length less than or equal to n over the alphabet of the FinDFA.

• FinDFA.IsAccessibleState - A predicate on states, true if the state is reachable from the start state by some word.

• FinDFA.isAccessibleStateDecidable - A decidability instance for FinDFA.IsAccessibleState.

• AccessibleFinDFA - A structure extending FinDFA with a proof that every state is accessible.

• FinDFA.toAccessible - A function that converts a FinDFA to an AccessibleFinDFA.

Main theorems

• FinDFA.getWordsLeqLength_correct - w ∈ M.getWordsLeqLength n ↔ w.length ≤ n.

• FinDFA.exists_short_access_word - In order to construct AccessibleFinDFAs from FinDFAs, we need to define a decidability instance on FinDFA.isAccessibleState. As written, this involves searching the infinite space of all words. However, we prove in FinDFA.exists_short_access_word that, if a state is accessible by any word, then it is accessible by some word of length at most the number of states in the FinDFA. This allows us to search through a finite space of words using our FinDFA.getWordsLeqLength function.

• FinDFA.toAccessible_pres_lang - The language of a FinDFA is the same as the language of the AccessibleFinDFA obtained by applying FinDFA.toAccessible.

Implementation notes

We provide coercions from FinDFA and AccessibleFinDFA to DFA. This means that when you have M : FinDFA α σ or M : AccessibleFinDFA α σ, you can use functions defined on DFA α σ such as eval, evalFrom, and accepts by writing (M : DFA α σ).eval or M.toDFA.eval.

Note that, just like DFA, the definitions of FinDFA and AccessibleFinDFA do not require the state space or alphabet to be finite or to have decidable equality.

Blueprint

• One DEF entry for Mathlib's DFA Label : dfa Lean definitions to tag : None Content : Explain that this is Mathlib's DFA defintitoin. Explain that DFA α σ has fields step, start, accept, and methods eval, evalFrom, accepts. Explain the types of these. Explain that this definition does not require the state space or alphabet to be finite or decidable. (explain what decidable equality is) Dependencies : None

• One DEF entry for FinDFA Label : fin-dfa lean defs :

  • FinDFA Content : Explain the definition of the FinDFA structure, and how it differes from DFA by requiring Fintype and DecidableEq instances on the alphabet and state space (explain what those classes are) and by requiring the accepting states to be a Finset rather than a Set (explain the differnece) Explain how this allows a decidable procedure (what is that?) for determining if a state is accepting. Explain how this can be converted to a DFA in lean and how we use the DFA definitions for .evalFrom, .accepts, etc. Dependencies : None

• One DEF entry for Accessible State and DFA definition label : accessable-fin-dfa lean defs :

  • FinDFA.IsAccessibleState
  • AccessibleFinDFA Content : Explain the definition of accessible states and the AccessibleFinDFA structure. Dependencies : fin-dfa

• One lemma entry for FinDFA.exists_short_access_word Label : exists-short-access-word Lean lemmas to tag :

  • FinDFA.exists_short_access_word
  • FinDFA.isAccessibleStateDecidable
  • FinDFA.toAccessible
  • FinDFA.toAccessible_pres_lang Content : Prove it and explain why this means that every word that is accessible is accessible by a short word. Explain how this is used to create a DECIDABLE procedure for determining if a state is accessible. Explain how that allows for a language-preserving conversion from FinDFA to AccessibleFinDFA by restricting the state space. Dependencies : accessible-fin-dfa

@[reducible, inline]

abbrev List.prependInjection {α : Type u_1} (w : List α) : α ↪ List α

Given a word, the injection sending each letter to its prepending to that word.

Equations

• w.prependInjection = { toFun := fun (a : α) => a :: w, inj' := ⋯ }

@[reducible, inline]

abbrev List.getNextWords {α : Type u_1} [Fintype α] (w : List α) : Finset (List α)

Given a word, the finset of all one-letter (preprended) extensions.

Equations

• w.getNextWords = Finset.map w.prependInjection Finset.univ

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

A computable DFA. Just like DFA but accept is a Finset

• step : σ → α → σ

  Transition function.

• start : σ

  Start state.

• accept : Finset σ

  Accepting states as a Finset.

def FinDFA.toDFA {α : Type u} {σ : Type v} (M : FinDFA α σ) : DFA α σ

Convert a FinDFA to a DFA.

Equations

• M.toDFA = { step := M.step, start := M.start, accept := ↑M.accept }

instance FinDFA.instCoeDFA {α : Type u} {σ : Type v} : Coe (FinDFA α σ) (DFA α σ)

Coercion from FinDFA to DFA.

Equations

• FinDFA.instCoeDFA = { coe := FinDFA.toDFA }

@[simp]

theorem FinDFA.coe_start {α : Type u} {σ : Type v} (M : FinDFA α σ) : M.toDFA.start = M.start

@[simp]

theorem FinDFA.coe_step {α : Type u} {σ : Type v} (M : FinDFA α σ) : M.toDFA.step = M.step

@[simp]

theorem FinDFA.coe_accept {α : Type u} {σ : Type v} (M : FinDFA α σ) : M.toDFA.accept = ↑M.accept

def FinDFA.getWordsOfLength {α : Type u} {σ : Type v} [Fintype α] [DecidableEq α] (M : FinDFA α σ) (n : ℕ) : Finset (List α)

Return all words of length n in the alphabet.

Equations

• M.getWordsOfLength 0 = {[]}
• M.getWordsOfLength n_2.succ = (M.getWordsOfLength n_2).biUnion List.getNextWords

@[simp]

theorem FinDFA.getWordsOfLength_correct {α : Type u} {σ : Type v} [Fintype α] [DecidableEq α] (M : FinDFA α σ) (n : ℕ) (w : List α) : w ∈ M.getWordsOfLength n ↔ w.length = n

def FinDFA.getWordsLeqLength {α : Type u} {σ : Type v} [Fintype α] [DecidableEq α] (M : FinDFA α σ) (n : ℕ) : Finset (List α)

Return all words of length at most n.

Equations

• M.getWordsLeqLength 0 = M.getWordsOfLength 0
• M.getWordsLeqLength n_2.succ = M.getWordsOfLength (n_2 + 1) ∪ M.getWordsLeqLength n_2

@[simp]

theorem FinDFA.getWordsLeqLength_correct {α : Type u} {σ : Type v} [Fintype α] [DecidableEq α] (M : FinDFA α σ) {n : ℕ} {w : List α} : w ∈ M.getWordsLeqLength n ↔ w.length ≤ n

Accessible States

@[reducible, inline]

abbrev FinDFA.IsAccessibleState {α : Type u} {σ : Type v} (M : FinDFA α σ) (s : σ) : Prop

A state is accessible if there exists some word that reaches it from the start state.

Equations

• M.IsAccessibleState s = ∃ (w : List α), M.toDFA.evalFrom M.start w = s

theorem FinDFA.exists_short_access_word {α : Type u} {σ : Type v} [Fintype σ] (M : FinDFA α σ) (s : σ) {w : List α} (hw : M.toDFA.evalFrom M.start w = s) : ∃ (v : List α), v.length ≤ Fintype.card σ ∧ s = M.toDFA.evalFrom M.start v

Every accessible state is reachable by a word of length at most the number of states.

def FinDFA.getAccessibleStates {α : Type u} {σ : Type v} [Fintype α] [DecidableEq α] [Fintype σ] [DecidableEq σ] (M : FinDFA α σ) : Finset σ

The finset of all accessible states.

Equations

• M.getAccessibleStates = (M.getWordsLeqLength (Fintype.card σ)).biUnion fun (s : List α) => {M.toDFA.evalFrom M.start s}

@[simp]

theorem FinDFA.getAccessibleStates_correct {α : Type u} {σ : Type v} [Fintype α] [DecidableEq α] [Fintype σ] [DecidableEq σ] (M : FinDFA α σ) (s : σ) : s ∈ M.getAccessibleStates ↔ M.IsAccessibleState s

Characterization of accessible states.

instance FinDFA.isAccessibleStateDecidable {α : Type u} {σ : Type v} [Fintype α] [DecidableEq α] [Fintype σ] [DecidableEq σ] (M : FinDFA α σ) : DecidablePred M.IsAccessibleState

Decidability of state accessibility.

Equations

• M.isAccessibleStateDecidable s = decidable_of_decidable_of_iff ⋯

Accessible DFAs

structure AccessibleFinDFA (α : Type u) (σ : Type v) extends FinDFA α σ : Type (max u v)

A DFA where every state is accessible from the start state.

• step : σ → α → σ
• start : σ
• accept : Finset σ
• is_accessible (s : σ) : self.IsAccessibleState s

def AccessibleFinDFA.toFinDFA {α : Type u} {σ : Type v} (M : AccessibleFinDFA α σ) : FinDFA α σ

Convert an AccessibleFinDFA to a FinDFA.

Equations

• M.toFinDFA = M.M

def AccessibleFinDFA.toDFA {α : Type u} {σ : Type v} (M : AccessibleFinDFA α σ) : DFA α σ

Convert an AccessibleFinDFA to a DFA.

Equations

• M.toDFA = M.toFinDFA.toDFA

instance AccessibleFinDFA.instCoeFinDFA {α : Type u} {σ : Type v} : Coe (AccessibleFinDFA α σ) (FinDFA α σ)

Coercion from AccessibleFinDFA to FinDFA.

Equations

• AccessibleFinDFA.instCoeFinDFA = { coe := AccessibleFinDFA.toFinDFA }

@[simp]

theorem AccessibleFinDFA.coe_start' {α : Type u} {σ : Type v} (M : AccessibleFinDFA α σ) : M.toFinDFA.start = M.start

@[simp]

theorem AccessibleFinDFA.coe_step' {α : Type u} {σ : Type v} (M : AccessibleFinDFA α σ) : M.toFinDFA.step = M.step

@[simp]

theorem AccessibleFinDFA.coe_accept' {α : Type u} {σ : Type v} (M : AccessibleFinDFA α σ) : M.toFinDFA.accept = M.accept

instance AccessibleFinDFA.instCoeDFA {α : Type u} {σ : Type v} : Coe (AccessibleFinDFA α σ) (DFA α σ)

Coercion from AccessibleFinDFA to DFA.

Equations

• AccessibleFinDFA.instCoeDFA = { coe := AccessibleFinDFA.toDFA }

@[simp]

theorem AccessibleFinDFA.coe_start {α : Type u} {σ : Type v} (M : AccessibleFinDFA α σ) : M.toDFA.start = M.start

@[simp]

theorem AccessibleFinDFA.coe_step {α : Type u} {σ : Type v} (M : AccessibleFinDFA α σ) : M.toDFA.step = M.step

@[simp]

theorem AccessibleFinDFA.coe_accept {α : Type u} {σ : Type v} (M : AccessibleFinDFA α σ) : M.toDFA.accept = ↑M.accept

FinDFA → AccessibleFinDFA

By restricting the state space to only the accessible states, we can convert any FinDFA to an AccessibleFinDFA. We prove that this conversion preserves the language accepted by the DFA.

def FinDFA.toAccessible {α : Type u} {σ : Type v} [Fintype α] [DecidableEq α] [Fintype σ] [DecidableEq σ] (M : FinDFA α σ) : AccessibleFinDFA α { s : σ // M.IsAccessibleState s }

Convert a FinDFA to an AccessibleFinDFA by restricting to accessible states.

Equations

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

@[simp]

theorem FinDFA.toAccessible_step_val {α : Type u} {σ : Type v} [Fintype α] [DecidableEq α] [Fintype σ] [DecidableEq σ] (M : FinDFA α σ) (s : { s : σ // M.IsAccessibleState s }) (a : α) : ↑(M.toAccessible.step s a) = M.step (↑s) a

theorem FinDFA.toAccessible_evalFrom_val {α : Type u} {σ : Type v} [Fintype α] [DecidableEq α] [Fintype σ] [DecidableEq σ] (M : FinDFA α σ) (s : { s : σ // M.IsAccessibleState s }) (w : List α) : ↑(M.toAccessible.toDFA.evalFrom s w) = M.toDFA.evalFrom (↑s) w

Evaluating toAccessible from an accessible state matches the original evaluation.

theorem FinDFA.toAccessible_eval_val {α : Type u} {σ : Type v} [Fintype α] [DecidableEq α] [Fintype σ] [DecidableEq σ] (M : FinDFA α σ) (w : List α) : ↑(M.toAccessible.toDFA.eval w) = M.toDFA.eval w

Evaluating toAccessible from the start matches the original evaluation.

theorem FinDFA.toAccessible_pres_lang {α : Type u} {σ : Type v} [Fintype α] [DecidableEq α] [Fintype σ] [DecidableEq σ] (M : FinDFA α σ) : M.toAccessible.toDFA.accepts = M.toDFA.accepts

The language accepted by toAccessible equals the language accepted by the original DFA.