Minimal deterministic automaton

TheoremLeft quotients of continuation languages#✓fully proved

Let \(M\) be a DFA, write \(\delta^*(q, x)\) for the state \(M\) reaches from the state \(q\) by reading the word \(x\), and let \(L_M(q)\) be the language of words accepted by \(M\) when started in \(q\). For every state \(q\) and every word \(x\), the left quotient \(\{z : xz \in L_M(q)\}\) of \(L_M(q)\) by \(x\) equals \(L_M(\delta^*(q, x))\).

theorem leftQuotient_acceptsFrom (M : DFA Symbol State) (q : State) (x : List Symbol) :
    (M.acceptsFrom q).leftQuotient x = M.acceptsFrom (M.evalFrom q x)

Used by 3

Used byThe canonical residual map · Transitions of the minimized DFA on reached states · Moore's automaton is the minimal automaton

DefinitionResidual reached by a word#✓fully proved

For a DFA \(M\) and a word \(x\), the minimized state of \(x\) is the language accepted by \(M\) starting from the state that \(M\) reaches on reading \(x\) from its start state, viewed as an element of the reachable residuals of \(M\).

def minimizedState (M : DFA Symbol State) (x : List Symbol) : reachableResiduals M :=
  ⟨M.acceptsFrom (M.eval x), ⟨x, rfl⟩⟩

Uses 1 · Used by 6

Statement usesResidual languages of reachable states

Used byStates of Brzozowski's automaton as residual languages · Residual language of a state of Brzozowski's automaton · Brzozowski's automaton is the minimal automaton · States reached in the minimized DFA · Transitions of the minimized DFA on reached states · Moore's automaton is the minimal automaton

DefinitionLeft quotients as reachable residuals#✓fully proved

Let \(M\) be a DFA accepting the language \(L\). The set of left quotients \(\{z : xz \in L\}\) of \(L\) by words \(x\) equals the set of reachable residuals of \(M\) (the languages accepted by \(M\) from the states it reaches from its start state). The bijection from the first set to the second sends each language to itself.

noncomputable def leftQuotientEquivReachableResiduals (M : DFA Symbol State) :
    Set.range M.accepts.leftQuotient ≃ reachableResiduals M where
  toFun q := ⟨q.val, by
    rw [reachableResiduals_eq_range_leftQuotient]
    exact q.property⟩
  invFun q := ⟨q.val, by
    rw [← reachableResiduals_eq_range_leftQuotient]
    exact q.property⟩
  left_inv _ := Subtype.ext rfl
  right_inv _ := Subtype.ext rfl

Uses 1 · Used by 8

Statement usesResidual languages of reachable states

Used byMinimized DFA · The minimized DFA accepts the same language · The minimized DFA is accessible · States reached in the minimized DFA · Evaluation in the minimized DFA agrees with the left-quotient automaton · Transitions of the minimized DFA · The canonical automaton of a DFA's language is its minimized DFA · Moore's automaton is the minimal automaton

DefinitionMinimized DFA#✓fully proved

Let \(M\) be a DFA accepting the language \(L\). The minimized DFA of \(M\) has as states the reachable residuals of \(M\), that is, the languages accepted by \(M\) from the states it reaches from its start state. Its start state is \(L\); on a letter \(a\) it moves from a state \(K\) to the left quotient \(\{z : az \in K\}\); and its accepting states are those that contain the empty word.

It is the canonical automaton of \(L\), whose states are the left quotients of \(L\), with each state renamed to the same language viewed as a reachable residual of \(M\).

noncomputable def minimizedDFA (M : DFA Symbol State) : DFA Symbol (reachableResiduals M) :=
  DFA.reindex (leftQuotientEquivReachableResiduals M) M.accepts.toDFA

Uses 2 · Used by 10

Statement usesLeft quotients as reachable residuals · Residual languages of reachable states

Used byBrzozowski's automaton is the minimal automaton · The minimized DFA accepts the same language · The minimized DFA is accessible · States reached in the minimized DFA · Evaluation in the minimized DFA agrees with the left-quotient automaton · Transitions of the minimized DFA on reached states · Transitions of the minimized DFA · Reachable residuals of the minimized DFA · The canonical automaton of a DFA's language is its minimized DFA · Moore's automaton is the minimal automaton

TheoremStates reached in the residual-language DFA#✓fully proved

For every language \(L\) and every word \(x\), the state that the residual-language DFA of \(L\) reaches on reading \(x\) is the left quotient \(x^{-1}L = \{z : xz \in L\}\). This automaton has the left quotients of \(L\) as states, start state \(L\), transition from \(K\) on a letter \(a\) to \(a^{-1}K\), and accepts \(K\) when \(K\) contains the empty word.

@[simp]
theorem toDFA_eval_val (L : Language Symbol) (x : List Symbol) :
    (L.toDFA.eval x).val = L.leftQuotient x

Used by 2

Used byStates reached in the minimized DFA · The residual-language DFA is accessible

TheoremEvaluation in the minimized DFA agrees with the left-quotient automaton#✓fully proved

Let \(M\) be a DFA accepting the language \(L\), and consider the automaton whose states are the left quotients of \(L\), with start state \(L\), moving from \(K\) on a letter \(a\) to \(\{z : az \in K\}\). For every word \(x\), the state that the minimized DFA of \(M\) reaches on \(x\), carried to the left quotients of \(L\) by the bijection that sends each language to itself, is the state that this automaton reaches on \(x\).

@[simp]
theorem minimizedDFA_eval_equiv (M : DFA Symbol State) (x : List Symbol) :
    (leftQuotientEquivReachableResiduals M).symm ((minimizedDFA M).eval x) =
      M.accepts.toDFA.eval x

Uses 3 · Used by 1

Statement usesLeft quotients as reachable residuals · Minimized DFA · Residual languages of reachable states

Used byStates reached in the minimized DFA

TheoremStates reached in the minimized DFA#✓fully proved

For every DFA \(M\) and every word \(x\), the state that the minimized DFA of \(M\) reaches on \(x\) is the language accepted by \(M\) from the state that \(M\) reaches on \(x\).

@[simp]
theorem minimizedDFA_eval (M : DFA Symbol State) (x : List Symbol) :
    (minimizedDFA M).eval x = minimizedState M x

Uses 6 · Used by 2

Statement usesMinimized DFA · Residual reached by a word · Residual languages of reachable states

Proof usesLeft quotients as reachable residuals · Evaluation in the minimized DFA agrees with the left-quotient automaton · States reached in the residual-language DFA

Used byBrzozowski's automaton is the minimal automaton · Moore's automaton is the minimal automaton

TheoremTransitions of the minimized DFA#✓fully proved

Let \(M\) be a DFA. For every reachable residual \(K\) of \(M\) (a state of the minimized DFA of \(M\)) and every letter \(a\), the minimized DFA of \(M\) moves from \(K\) on input \(a\) to the left quotient \(\{z : az \in K\}\) of \(K\) by \(a\).

@[simp]
theorem minimizedDFA_step_val (M : DFA Symbol State) (q : reachableResiduals M) (a : Symbol) :
    ((minimizedDFA M).step q a).val = q.val.leftQuotient [a]

Uses 3 · Used by 2

Statement usesMinimized DFA · Residual languages of reachable states

Proof usesLeft quotients as reachable residuals

Used byTransitions of the minimized DFA on reached states · Moore's automaton is the minimal automaton

TheoremTransitions of the minimized DFA on reached states#✓fully proved

Let \(M\) be a DFA, and for a word \(x\) let \([x]\) be the language accepted by \(M\) from the state that \(M\) reaches on \(x\). For every word \(x\) and every letter \(a\), the minimized DFA of \(M\) moves from the state \([x]\) on input \(a\) to the state \([xa]\).

@[simp]
theorem minimizedDFA_step_minimizedState (M : DFA Symbol State) (x : List Symbol) (a : Symbol) :
    (minimizedDFA M).step (minimizedState M x) a = minimizedState M (x ++ [a])

Uses 5 · Used by 1

Statement usesMinimized DFA · Residual reached by a word · Residual languages of reachable states

Proof usesLeft quotients of continuation languages · Transitions of the minimized DFA

Used byBrzozowski's automaton is the minimal automaton

TheoremThe minimized DFA accepts the same language#✓fully proved

For every DFA \(M\), the minimized DFA of \(M\) accepts exactly the language accepted by \(M\).

@[simp]
theorem minimizedDFA_accepts (M : DFA Symbol State) :
    (minimizedDFA M).accepts = M.accepts

Uses 3 · Used by 2

Statement usesMinimized DFA · Residual languages of reachable states

Proof usesLeft quotients as reachable residuals

Used byBrzozowski's automaton is the minimal automaton · Reachable residuals of the minimized DFA

TheoremThe residual-language DFA is accessible#✓fully proved

For every language \(L\), the residual-language DFA of \(L\) is accessible. This automaton has as states the left quotients \(x^{-1}L = \{z : xz \in L\}\) for words \(x\), start state \(L\), transition from \(K\) on a letter \(a\) to \(a^{-1}K\), and accepts \(K\) when \(K\) contains the empty word.

theorem toDFA_accessible (L : Language Symbol) : Accessible L.toDFA

Uses 3 · Used by 1

Statement usesAccessible DFA

Proof usesReachable state of a DFA · States reached in the residual-language DFA

Used byThe minimized DFA is accessible

TheoremThe minimized DFA is accessible#✓fully proved

For every DFA \(M\), every state of the minimized DFA of \(M\) is reached from its start state by reading some word.

theorem minimizedDFA_accessible (M : DFA Symbol State) : Accessible (minimizedDFA M)

Uses 6

Statement usesAccessible DFA · Minimized DFA · Residual languages of reachable states

Proof usesReachable state of a DFA · Left quotients as reachable residuals · The residual-language DFA is accessible

DefinitionNerode classes and reachable residuals#✓fully proved

For a DFA \(M\) accepting the language \(L\), there is a bijection from the Nerode classes of \(L\) to the reachable residuals of \(M\); it sends the class of a word \(x\) to the left quotient \(x^{-1}L = \{z : xz \in L\}\).

noncomputable def nerodeClassEquivMinimizedState (M : DFA Symbol State) :
    NerodeClass M.accepts ≃ reachableResiduals M :=
  nerodeClassEquivReachableResiduals M rfl

Uses 3 · Used by 3

Statement usesNerode classes · Nerode classes correspond to reachable residuals · Residual languages of reachable states

Used byWhen finite, the minimized DFA has as many states as there are Nerode classes · Reachable residuals of the minimized DFA · Moore's automaton has one state per Nerode class

DefinitionReachable residuals of the minimized DFA#✓fully proved

Let \(M\) be a DFA accepting the language \(L\). The reachable residuals of the minimized DFA of \(M\) and the reachable residuals of \(M\) both form the set of left quotients \(x^{-1}L = \{z : xz \in L\}\) of \(L\) by words \(x\), and this is the bijection from the first set to the second that sends each language to itself.

It is built as the composite of the bijections from the Nerode classes of \(L\) to both sets, each sending the class of a word \(x\) to \(x^{-1}L\); so minimizing the minimized DFA again gives the same state space.

noncomputable def minimizedStateEquivIterated (M : DFA Symbol State) :
    reachableResiduals (minimizedDFA M) ≃ reachableResiduals M :=
  (nerodeClassEquivReachableResiduals (minimizedDFA M) (minimizedDFA_accepts M)).symm.trans
    (nerodeClassEquivMinimizedState M)

Uses 6

Statement usesNerode classes · Minimized DFA · The minimized DFA accepts the same language · Nerode classes and reachable residuals · Nerode classes correspond to reachable residuals · Residual languages of reachable states

TheoremWhen finite, the minimized DFA has as many states as there are Nerode classes#✓fully proved

Let \(M\) be a DFA accepting the language \(L\). If the set of reachable residuals of \(M\) (the states of the minimized DFA of \(M\)) and the set of Nerode classes of \(L\) are both finite, then they have the same number of elements.

theorem minimizedDFA_card_eq_nerode (M : DFA Symbol State) [Fintype (reachableResiduals M)]
    [Fintype (NerodeClass M.accepts)] :
    Fintype.card (reachableResiduals M) = Fintype.card (NerodeClass M.accepts)

Uses 3

Statement usesNerode classes · Residual languages of reachable states

Proof usesNerode classes and reachable residuals

DefinitionCSLib automata as Mathlib DFAs#✓fully proved

A CSLib deterministic automaton \(M\) on finite words is viewed as a Mathlib DFA with the same states, the same transition function, the same start state and the same set of accepting states as \(M\).

def toDFA (M : DA.FinAcc State Symbol) : DFA Symbol State where
  step := M.tr
  start := M.start
  accept := M.accept

Used by 3

Used byConverting a CSLib automaton to a Mathlib DFA preserves its language · The Nerode automaton is the residual-language automaton · The canonical automaton of a DFA's language is its minimized DFA

DefinitionMathlib DFAs as CSLib automata#✓fully proved

A Mathlib DFA \(M\) is viewed as a CSLib deterministic automaton on finite words with the same states, the same transition function, the same start state and the same set of accepting states as \(M\).

def ofDFA (M : DFA Symbol State) : DA.FinAcc State Symbol where
  tr := M.step
  start := M.start
  accept := M.accept

Used by 2

Used byThe two-way simulation of a DFA accepts the same language · The two-way simulation of a DFA agrees with that of its NFA

TheoremConverting a CSLib automaton to a Mathlib DFA preserves its language#✓fully proved

For every deterministic automaton \(M\) on finite words, the DFA with the same states, transition function, start state and accepting states as \(M\) accepts exactly the language of \(M\).

@[simp]
theorem language_toDFA (M : DA.FinAcc State Symbol) :
    M.toDFA.accepts = Acceptor.language M

Uses 1

Statement usesCSLib automata as Mathlib DFAs

TheoremThe Nerode congruence relates words with equal left quotients#✓fully proved

Let \(L\) be a language over an alphabet \(\Sigma\) and let \(x, y \in \Sigma^*\). Then \(x\) and \(y\) are related by the Nerode congruence of \(L\), that is, \(xz \in L \iff yz \in L\) for every word \(z\), if and only if they are Nerode equivalent for \(L\), that is, their left quotients \(x^{-1}L = \{z : xz \in L\}\) and \(y^{-1}L\) are equal.

theorem nerodeCongruence_r_iff {x y : List Symbol} :
    l.NerodeCongruence.r x y ↔ nerodeRel l x y

Uses 1 · Used by 2

Statement usesNerode equivalence

Used byNerode classes are the residual languages · The residual language of a Nerode class

DefinitionThe residual language of a Nerode class#✓fully proved

Let \(L\) be a language over an alphabet \(\Sigma\), and write \(x^{-1}L = \{z : xz \in L\}\) for the left quotient of \(L\) by a word \(x\). This is the map from the classes of the Nerode congruence of \(L\) to the set \(\{w^{-1}L : w \in \Sigma^*\}\) of residual languages of \(L\) that sends the class of each word \(x\) to \(x^{-1}L\); it is well defined because Nerode-congruent words have the same left quotient.

def nerodeResidual (l : Language Symbol) : l.NerodeQuotient → Set.range l.leftQuotient :=
  Quotient.lift (fun x => ⟨l.leftQuotient x, x, rfl⟩)
    (fun _ _ h => Subtype.ext (nerodeCongruence_r_iff.1 h))

Uses 2 · Used by 1

Statement usesThe Nerode congruence relates words with equal left quotients · Nerode equivalence

Used byNerode classes are the residual languages

DefinitionNerode classes are the residual languages#✓fully proved

Let \(L\) be a language over an alphabet \(\Sigma\), and write \(x^{-1}L = \{z : xz \in L\}\) for the left quotient of \(L\) by a word \(x\). This is the bijection from the classes of the Nerode congruence of \(L\) onto the set \(\{x^{-1}L : x \in \Sigma^*\}\) of residual languages of \(L\) that sends the class of each word \(x\) to \(x^{-1}L\).

The residual languages are the states of Mathlib's residual-language DFA of \(L\).

noncomputable def nerodeQuotientEquivResidual (l : Language Symbol) :
    l.NerodeQuotient ≃ Set.range l.leftQuotient :=
  Equiv.ofBijective _ nerodeResidual_bijective

Uses 3 · Used by 2

Statement usesThe Nerode congruence relates words with equal left quotients · The residual language of a Nerode class · Nerode equivalence

Used byThe Nerode automaton is the residual-language automaton · The canonical automaton of a DFA's language is its minimized DFA

TheoremThe Nerode automaton is the residual-language automaton#✓fully proved

Let \(L\) be a language over an alphabet \(\Sigma\), and write \(x^{-1}L = \{z : xz \in L\}\) for the left quotient of \(L\) by a word \(x\). Consider the canonical automaton of \(L\) as a DFA: its states are the classes \([x]\) of the Nerode congruence of \(L\), its start state is the class of the empty word, on a letter \(a\) it goes from \([x]\) to \([xa]\), and its accepting states are the classes of words of \(L\). Renaming each class \([x]\) to \(x^{-1}L\) gives exactly Mathlib's residual-language DFA of \(L\): its states are the residual languages \(x^{-1}L\) for \(x \in \Sigma^*\), its start state is \(L\), on a letter \(a\) it goes from \(K\) to \(a^{-1}K\), and its accepting states are the residual languages that contain the empty word.

theorem reindex_nerodeCongruenceDA (l : Language Symbol) :
    DFA.reindex (nerodeQuotientEquivResidual l) (toDFA l.NerodeCongruenceDA) = l.toDFA

Uses 2 · Used by 1

Statement usesNerode classes are the residual languages · CSLib automata as Mathlib DFAs

Used byThe canonical automaton of a DFA's language is its minimized DFA

TheoremThe canonical automaton of a DFA's language is its minimized DFA#✓fully proved

Let \(M\) be a DFA over an alphabet \(\Sigma\) accepting the language \(L\), and write \(x^{-1}L = \{z : xz \in L\}\) for the left quotient of \(L\) by a word \(x\). Consider the canonical automaton of \(L\) as a DFA: its states are the classes \([x]\) of the Nerode congruence of \(L\), its start state is the class of the empty word, on a letter \(a\) it goes from \([x]\) to \([xa]\), and its accepting states are the classes of words of \(L\). Renaming each class \([x]\) to \(x^{-1}L\), regarded as one of the languages accepted from the states of \(M\) reachable from its start state, gives exactly the minimized DFA of \(M\).

theorem reindex_nerodeCongruenceDA_eq_minimizedDFA {State : Type*} (M : DFA Symbol State) :
    DFA.reindex ((nerodeQuotientEquivResidual M.accepts).trans
      (leftQuotientEquivReachableResiduals M)) (toDFA M.accepts.NerodeCongruenceDA) =
        minimizedDFA M

Uses 6

Statement usesNerode classes are the residual languages · CSLib automata as Mathlib DFAs · Left quotients as reachable residuals · Minimized DFA · Residual languages of reachable states

Proof usesThe Nerode automaton is the residual-language automaton

StructureMorphisms of DFAs#✓fully proved

Let \(M\) and \(N\) be DFAs over the same alphabet with transition functions \(\delta_M\) and \(\delta_N\). A morphism from \(M\) to \(N\) is a map \(f\) from the states of \(M\) to the states of \(N\) that sends the start state of \(M\) to the start state of \(N\), satisfies \(f(\delta_M(q, a)) = \delta_N(f(q), a)\) for every state \(q\) of \(M\) and every symbol \(a\), and such that each state \(q\) of \(M\) is accepting if and only if \(f(q)\) is accepting in \(N\).

structure DFAHom (M : DFA Symbol State) (N : DFA Symbol State') where
  toFun : State → State'
  map_start : toFun M.start = N.start
  map_step : ∀ q a, toFun (M.step q a) = N.step (toFun q) a
  mem_accept_iff : ∀ q, q ∈ M.accept ↔ toFun q ∈ N.accept

Used by 10

Used byDFA morphisms preserve the accepted language · The canonical residual map · Injectivity of the canonical residual map · The canonical residual map is surjective · Uniqueness of the canonical residual map · Composition of DFA morphisms · DFA morphisms commute with evaluation · DFA morphisms commute with evaluation from a state · Identity DFA morphism · States of an accessible, state-separated DFA correspond to residuals

TheoremDFA morphisms commute with evaluation from a state#✓fully proved

If \(f\) is a morphism from a DFA \(M\) to a DFA \(N\), then for every state \(q\) of \(M\) and every word \(x\), running \(N\) on \(x\) from \(f(q)\) ends in the image under \(f\) of the state reached by running \(M\) on \(x\) from \(q\).

theorem DFAHom.map_evalFrom {M : DFA Symbol State} {N : DFA Symbol State'}
    (f : DFAHom M N) (q : State) (x : List Symbol) :
    f (M.evalFrom q x) = N.evalFrom (f q) x

Uses 1 · Used by 1

Statement usesMorphisms of DFAs

Used byDFA morphisms commute with evaluation

TheoremDFA morphisms commute with evaluation#✓fully proved

If \(f\) is a morphism from a DFA \(M\) to a DFA \(N\), then for every word \(x\), the state that \(N\) reaches on input \(x\) from its start state is the image under \(f\) of the state that \(M\) reaches on input \(x\) from its start state.

theorem DFAHom.map_eval {M : DFA Symbol State} {N : DFA Symbol State'}
    (f : DFAHom M N) (x : List Symbol) : f (M.eval x) = N.eval x

Uses 2 · Used by 2

Statement usesMorphisms of DFAs

Proof usesDFA morphisms commute with evaluation from a state

Used byDFA morphisms preserve the accepted language · Uniqueness of the canonical residual map

TheoremDFA morphisms preserve the accepted language#✓fully proved

If \(f\) is a morphism from a DFA \(M\) to a DFA \(N\) over the same alphabet, then \(M\) and \(N\) accept the same language.

theorem DFAHom.accepts_eq {M : DFA Symbol State} {N : DFA Symbol State'}
    (f : DFAHom M N) : M.accepts = N.accepts

Uses 2

Statement usesMorphisms of DFAs

Proof usesDFA morphisms commute with evaluation

DefinitionIdentity DFA morphism#✓fully proved

For every DFA \(M\), the identity map on the states of \(M\) is a DFA morphism from \(M\) to itself.

def DFAHom.refl (M : DFA Symbol State) : DFAHom M M where
  toFun := id
  map_start := rfl
  map_step := fun _ _ ↦ rfl
  mem_accept_iff := fun _ ↦ Iff.rfl

Uses 1

Statement usesMorphisms of DFAs

DefinitionComposition of DFA morphisms#✓fully proved

If \(f\) is a DFA morphism from \(M\) to \(N\) and \(g\) is a DFA morphism from \(N\) to \(P\), where \(M\), \(N\), \(P\) are DFAs over the same alphabet, then the composite of \(g\) and \(f\) is the DFA morphism from \(M\) to \(P\) whose state map is \(g \circ f\).

def DFAHom.comp {State'' : Type*} {M : DFA Symbol State} {N : DFA Symbol State'}
    {P : DFA Symbol State''} (g : DFAHom N P) (f : DFAHom M N) : DFAHom M P where
  toFun := g ∘ f
  map_start := by rw [Function.comp_apply, f.map_start, g.map_start]
  map_step := by intro q a; rw [Function.comp_apply, f.map_step, g.map_step, Function.comp_apply]
  mem_accept_iff := fun q ↦ (f.mem_accept_iff q).trans (g.mem_accept_iff (f q))

Uses 1

Statement usesMorphisms of DFAs

DefinitionState-separated DFA#✓fully proved

A DFA \(M\) is state-separated when any two equivalent states of \(M\) are equal: if \(p \ne q\), then the languages of words accepted by \(M\) starting from \(p\) and from \(q\) are different.

def StateSeparated (M : DFA Symbol State) : Prop :=
  ∀ ⦃p q⦄, StateEquivalent M p q → p = q

Uses 1 · Used by 7

Statement usesEquivalent states of a DFA

Used byInjectivity of the canonical residual map · States of an accessible, state-separated DFA correspond to residuals · Action of the syntactic monoid on states · Image of the syntactic action · Syntactic congruence as a kernel · Syntactic equivalence via transition actions · Syntactically equivalent words act identically

DefinitionThe canonical residual map#✓fully proved

Let \(M\) be an accessible DFA accepting the language \(L\). The residual-language DFA of \(L\) has as states the left quotients \(x^{-1}L = \{y \mid xy \in L\}\) for words \(x\), start state \(L\), transitions \(K \mapsto a^{-1}K\) on a symbol \(a\), and a state \(K\) is accepting when it contains the empty word. The canonical residual map is the DFA morphism from \(M\) to this DFA that sends each state \(q\) of \(M\) to its continuation language, the set of words \(z\) such that running \(M\) from \(q\) on \(z\) ends in an accepting state.

Cslib.Language.canonicalResidualHom · 18 lines

noncomputable def canonicalResidualHom (M : DFA Symbol State) (hacc : Accessible M) :
    DFAHom M M.accepts.toDFA where
  toFun q := by
    refine ⟨M.acceptsFrom q, ?_⟩
    obtain ⟨x, hx⟩ := hacc q
    refine ⟨x, ?_⟩
    rw [Language.leftQuotient_accepts_apply, hx]
  map_start := by
    apply Subtype.ext
    rfl
  map_step q a := by
    apply Subtype.ext
    change M.acceptsFrom (M.step q a) = (M.acceptsFrom q).leftQuotient [a]
    rw [← DFA.evalFrom_singleton]
    exact (leftQuotient_acceptsFrom M q [a]).symm
  mem_accept_iff q := by
    change q ∈ M.accept ↔ [] ∈ M.acceptsFrom q
    rfl

Uses 4 · Used by 4

Statement usesAccessible DFA · Morphisms of DFAs · Reachable state of a DFA · Left quotients of continuation languages

Used byInjectivity of the canonical residual map · The canonical residual map is surjective · Uniqueness of the canonical residual map · States of an accessible, state-separated DFA correspond to residuals

TheoremThe canonical residual map is surjective#✓fully proved

For an accessible DFA \(M\), every state of the residual-language DFA of the language accepted by \(M\) is the image of some state of \(M\) under the canonical residual map.

theorem canonicalResidualHom_surjective (M : DFA Symbol State) (hacc : Accessible M) :
    Function.Surjective (canonicalResidualHom M hacc)

Uses 3 · Used by 1

Statement usesAccessible DFA · Morphisms of DFAs · The canonical residual map

Used byStates of an accessible, state-separated DFA correspond to residuals

TheoremInjectivity of the canonical residual map#✓fully proved

For an accessible DFA \(M\), the canonical residual map from \(M\) to the residual-language DFA of its accepted language is injective if and only if \(M\) is state-separated, that is, any two states of \(M\) with the same continuation language are equal.

theorem canonicalResidualHom_injective_iff (M : DFA Symbol State) (hacc : Accessible M) :
    Function.Injective (canonicalResidualHom M hacc) ↔ StateSeparated M

Uses 5 · Used by 1

Statement usesAccessible DFA · Morphisms of DFAs · State-separated DFA · The canonical residual map

Proof usesEquivalent states of a DFA

Used byStates of an accessible, state-separated DFA correspond to residuals

DefinitionStates of an accessible, state-separated DFA correspond to residuals#✓fully proved

Let \(M\) be a DFA that is accessible and state-separated, and let \(L\) be the language it accepts. The map sending each state \(q\) of \(M\) to the language of words accepted by \(M\) starting from \(q\) is a bijection from the states of \(M\) onto the set of left quotients \(\{z : xz \in L\}\) of \(L\) by words \(x\).

noncomputable def stateEquivResidualsOfSeparated (M : DFA Symbol State) (hacc : Accessible M)
    (hsep : StateSeparated M) : State ≃ Set.range M.accepts.leftQuotient :=
  Equiv.ofBijective (canonicalResidualHom M hacc)
    ⟨(canonicalResidualHom_injective_iff M hacc).mpr hsep,
      canonicalResidualHom_surjective M hacc⟩

Uses 6

Statement usesAccessible DFA · Morphisms of DFAs · State-separated DFA · The canonical residual map · Injectivity of the canonical residual map · The canonical residual map is surjective

TheoremUniqueness of the canonical residual map#✓fully proved

For an accessible DFA \(M\) accepting the language \(L\), every DFA morphism from \(M\) to the residual-language DFA of \(L\) equals the canonical residual map.

theorem canonicalResidualHom_unique (M : DFA Symbol State) (hacc : Accessible M)
    (f : DFAHom M M.accepts.toDFA) : f = canonicalResidualHom M hacc

Uses 5

Statement usesAccessible DFA · Morphisms of DFAs · The canonical residual map

Proof usesDFA morphisms commute with evaluation · Reachable state of a DFA

35 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.