Morphisms between DFAs

This file defines morphisms between DFAs, which are bundled functions between the state spaces that respect the transition function, start state, and accept states of the DFAs.

We then define a partial order on AccessibleFinDFAs where M ≤ N iff there exists a surjective morphism from N.toDFA to M.toDFA.

Main definitions

• DFA.Hom - A morphism from the DFA M to the DFA N, notated M →ₗ N.

• DFA.Equiv - An equivalence of DFAs, which is a bijective morphism, notated M ≃ₗ N.

• AccessibleFinDFA.HomSurj - A morphism on the underlying DFAs of the AccessibleFinDFAs that is surjective on states. Notated M ↠ N.

• AccessibleFinDFA.le - Notated ≤, the partial order on AccessibleFinDFAs.

• AccessibleFinDFA.IsMinimal - A predicate that M is minimal by the partial order, up to equivalence of the underlying DFAs.

Main theorems

• DFA.hom_pres_lang - M.accepts = N.accepts when there exists f : M →ₗ N.
• AccessibleFinDFA.le_refl - Reflexivity of ≤.
• AccessibleFinDFA.le_trans - Transitivity of ≤.
• AccessibleFinDFA.le_antisymm - Antisymmetry of ≤ up to equivalence of underlying DFAs.

Notation

• M →ₗ N - Notation for DFA.Hom M N.
• M ≃ₗ N - Notation for DFA.Equiv M N.
• M ↠ N - Notation for AccessibleFinDFA.HomSurj M N.
• M ≤ N - Notation for the partial order on AccessibleFinDFAs.

Blueprint

• One DEF entry for DFA.Hom and DFA.Equiv. Label : dfa-hom Lean defs : DFA.Hom, DFA.Equiv Content : explain the structures Dependencies : dfa

• One DEF entry for the partial order on AccessibleFinDFAs. Label : accessible-fin-dfa-le Lean defs : AccessibleFinDFA.HomSurj AccessibleFinDFA.le AccessibleFinDFA.le_refl AccessibleFinDFA.le_trans AccessibleFinDFA.le_antisymm AccessibleFinDFA.isMinimal Content : explain how we can define a partial order on AccessibleFinDFAs by the existence of a surjective morphism between their underlying DFAs. Prove that this is a partial order up to equivalence of the underlying DFAs. Explain what IsMinimal means by this definition. Dependencies : accessible-fin-dfa, dfa-hom

structure DFA.Hom {α : Type u} {σ₁ : Type v} {σ₂ : Type w} (M : DFA α σ₁) (N : DFA α σ₂) : Type (max v w)

A morphism of DFAs from M to N.

• toFun : σ₁ → σ₂

  Underlying function map from states of M to states of N.

• map_start : self.toFun M.start = N.start

  The function preserves the start state.

• map_accept (q : σ₁) : q ∈ M.accept ↔ self.toFun q ∈ N.accept

  The function preserves the set of accepting states.

• map_step (q : σ₁) (w : List α) : self.toFun (M.evalFrom q w) = N.evalFrom (self.toFun q) w

  The function preserves state transitions.

def DFA.«term_→ₗ_» : Lean.TrailingParserDescr

M →ₗ N denotes the type of DFA.Hom M N.

Equations

• DFA.«term_→ₗ_» = Lean.ParserDescr.trailingNode `DFA.«term_→ₗ_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →ₗ ") (Lean.ParserDescr.cat `term 25))

theorem DFA.Hom.pres_lang {α : Type u} {σ₁ : Type v} {σ₂ : Type w} {M : DFA α σ₁} {N : DFA α σ₂} (f : M →ₗ N) : M.accepts = N.accepts

A morphism of DFAs preserves the accepted language.

def DFA.Hom.refl {α : Type u} {σ₁ : Type v} (M : DFA α σ₁) : M →ₗ M

The identity morphism on a DFA.

Equations

• DFA.Hom.refl M = { toFun := id, map_start := ⋯, map_accept := ⋯, map_step := ⋯ }

structure DFA.Equiv {α : Type u} {σ₁ : Type v} {σ₂ : Type w} (M : DFA α σ₁) (N : DFA α σ₂) : Type (max v w)

An equivalence of DFAs is a bijective morphism.

• toDFAHom : M →ₗ N
• toInvDFAHom : N →ₗ M
• left_inv : Function.LeftInverse self.toInvDFAHom.toFun self.toDFAHom.toFun
• right_inv : Function.RightInverse self.toInvDFAHom.toFun self.toDFAHom.toFun

def DFA.«term_≃ₗ_» : Lean.TrailingParserDescr

M ≃ₗ N denotes the type of DFA.Equiv M N.

Equations

• DFA.«term_≃ₗ_» = Lean.ParserDescr.trailingNode `DFA.«term_≃ₗ_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃ₗ ") (Lean.ParserDescr.cat `term 25))

def DFA.Equiv.refl {α : Type u} {σ₁ : Type v} (M : DFA α σ₁) : M ≃ₗ M

The identity equivalence on a DFA.

Equations

• DFA.Equiv.refl M = { toDFAHom := DFA.Hom.refl M, toInvDFAHom := DFA.Hom.refl M, left_inv := ⋯, right_inv := ⋯ }

Surjective Morphisms of AccessibleFinDFAs

structure AccessibleFinDFA.HomSurj {α : Type u} {σ₁ : Type v} {σ₂ : Type w} (M : AccessibleFinDFA α σ₁) (N : AccessibleFinDFA α σ₂) extends M.toDFA →ₗ N.toDFA : Type (max v w)

A surjective morphism between the underlying DFAs of AccessibleFinDFAs.

• toFun : σ₁ → σ₂
• map_start : self.toFun M.toDFA.start = N.toDFA.start
• map_accept (q : σ₁) : q ∈ M.toDFA.accept ↔ self.toFun q ∈ N.toDFA.accept
• map_step (q : σ₁) (w : List α) : self.toFun (M.toDFA.evalFrom q w) = N.toDFA.evalFrom (self.toFun q) w
• surjective : Function.Surjective self.toFun

  The function is surjective.

def AccessibleFinDFA.«term_↠_» : Lean.TrailingParserDescr

M ↠ N denotes the type of AccessibleFinDFA.HomSurj M N.

Equations

• AccessibleFinDFA.«term_↠_» = Lean.ParserDescr.trailingNode `AccessibleFinDFA.«term_↠_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↠ ") (Lean.ParserDescr.cat `term 25))

def AccessibleFinDFA.HomSurj.toDFAHom {α : Type u} {σ₁ : Type v} {σ₂ : Type w} {M : AccessibleFinDFA α σ₁} {N : AccessibleFinDFA α σ₂} (f : M ↠ N) : M.toDFA →ₗ N.toDFA

Forget the surjectivity proof and view HomSurj as a DFA morphism.

Equations

• f.toDFAHom = f.f

Partial Order on AccessibleFinDFAs

def AccessibleFinDFA.le {α : Type u} {σ₁ : Type v} {σ₂ : Type w} (M : AccessibleFinDFA α σ₁) (N : AccessibleFinDFA α σ₂) : Prop

The preorder on AccessibleFinDFAs: M ≤ N iff there is a surjective morphism N ↠ M.

Equations

• (M ≤ N) = Nonempty (N ↠ M)

def AccessibleFinDFA.«term_≤_» : Lean.TrailingParserDescr

M ≤ N denotes the proposition le M N.

Equations

• AccessibleFinDFA.«term_≤_» = Lean.ParserDescr.trailingNode `AccessibleFinDFA.«term_≤_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤ ") (Lean.ParserDescr.cat `term 26))

theorem AccessibleFinDFA.le_refl {α : Type u} {σ₁ : Type v} (M : AccessibleFinDFA α σ₁) : M ≤ M

Reflexivity of the preorder on AccessibleFinDFAs.

theorem AccessibleFinDFA.le_trans {α : Type u} {σ₁ : Type v} {σ₂ : Type w} {σ₃ : Type u_1} {M : AccessibleFinDFA α σ₁} {N : AccessibleFinDFA α σ₂} {O : AccessibleFinDFA α σ₃} (h₁ : M ≤ N) (h₂ : N ≤ O) : M ≤ O

Transitivity of the preorder on AccessibleFinDFAs.

theorem AccessibleFinDFA.le_antisymm {α : Type u} {σ₁ : Type v} {σ₂ : Type w} (M : AccessibleFinDFA α σ₁) (N : AccessibleFinDFA α σ₂) (h₁ : M ≤ N) (h₂ : N ≤ M) : Nonempty (M.toDFA ≃ₗ N.toDFA)

Antisymmetry of the preorder up to equivalence of the underlying DFAs.

def AccessibleFinDFA.IsMinimal {α : Type u} {σ₁ : Type v} (M : AccessibleFinDFA α σ₁) : Prop

An AccessibleFinDFA is minimal if every smaller DFA is equivalent to it.

Equations

• M.IsMinimal = ∀ {σ₂ : Type ?u.21} [Fintype σ₂] [DecidableEq σ₂] (N : AccessibleFinDFA α σ₂), N ≤ M → Nonempty (M.toDFA ≃ₗ N.toDFA)