Documentation

Mathlib.Computability.DFA

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 #

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.

Instances For
    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
    Instances For
      @[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
      Instances For
        @[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 : σ) :

        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}
        Instances For
          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 α σ) :

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

          Equations
          • M.accepts = M.acceptsFrom M.start
          Instances For
            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_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)
            @[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_start {α : Type u} {σ : Type v} {α' : Type u_1} (f : α'α) (M : DFA α σ) :
            (DFA.comap f M).start = M.start
            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 }
            Instances For
              @[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_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
              @[simp]
              theorem DFA.reindex_apply_start {α : Type u} {σ : Type v} {σ' : Type u_2} (g : σ σ') (M : DFA α σ) :
              ((DFA.reindex g) M).start = g M.start
              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.
              Instances For
                @[simp]
                theorem DFA.reindex_refl {α : Type u} {σ : Type v} (M : DFA α σ) :
                @[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 : σ σ') :