structure Sipser.GNFA (Q : Type u_1) (σ : Type u_2) [Fintype Q] : Type (max u_1 u_2)

Definition (Generalized Nondeterministic Finite Automaton). A GNFA over states Q and alphabet σ is like an NFA, but its transitions are labeled with regular expressions rather than single symbols. For convenience we assume:

• one start state and one accept state (distinct, start_ne_accept);
• one arrow δ q q' (a regex) between every pair of states, with the restrictions that no arrow enters the start state (no_enter_start) and no arrow exits the accept state (no_exit_accept).

• start : Q
• accept : Q
• start_ne_accept : self.start ≠ self.accept
• δ : Q → Q → RegularExpression σ
• no_enter_start (q : Q) : self.δ q self.start = RegularExpression.zero
• no_exit_accept (q : Q) : self.δ self.accept q = RegularExpression.zero

inductive Sipser.GNFA.AcceptPath {Q : Type u_1} {σ : Type u_2} [Fintype Q] (G : GNFA Q σ) : Q → Q → List σ → Prop

AcceptPath G q q' w says that the word w labels a path in the GNFA G from state q to state q': either w = [] and the path is the trivial self-loop at q (nil), or w = w₁ ++ w₂ where some prefix w₁ reaches an intermediate state qmid and w₂ is matched by the regex G.δ qmid q' labelling the edge from qmid to q' (cons).

• nil {Q : Type u_1} {σ : Type u_2} [Fintype Q] {G : GNFA Q σ} (q : Q) : G.AcceptPath q q []
• cons {Q : Type u_1} {σ : Type u_2} [Fintype Q] {G : GNFA Q σ} {q qmid q' : Q} {w₁ w₂ : List σ} (path : G.AcceptPath q qmid w₁) (hmatch : w₂ ∈ (G.δ qmid q').matches') : G.AcceptPath q q' (w₁ ++ w₂)

def Sipser.GNFA.accepts {Q : Type u_1} {σ : Type u_2} [Fintype Q] (G : GNFA Q σ) (w : List σ) : Prop

The GNFA G accepts the word w iff there is an AcceptPath from G.start to G.accept labelled by w.

def Sipser.GNFA.language {Q : Type u_1} {σ : Type u_2} [Fintype Q] (G : GNFA Q σ) : Language σ

The language L(G) recognised by the GNFA G: the set of all words it accepts.

@[simp]

theorem Sipser.GNFA.mem_language {Q : Type u_1} {σ : Type u_2} [Fintype Q] {G : GNFA Q σ} {w : List σ} : w ∈ G.language ↔ G.accepts w

Membership in G.language unfolds to G.accepts; a simp rewrite for convenience.

theorem Sipser.GNFA.AcceptPath.trans {Q : Type u_1} {σ : Type u_2} [Fintype Q] {q₁ q₂ : Q} {w₁ : List σ} {q₃ : Q} {w₂ : List σ} {G : GNFA Q σ} (h₁ : G.AcceptPath q₁ q₂ w₁) (h₂ : G.AcceptPath q₂ q₃ w₂) : G.AcceptPath q₁ q₃ (w₁ ++ w₂)

Concatenation of accept paths: if w₁ labels a path from q₁ to q₂ and w₂ labels a path from q₂ to q₃, then w₁ ++ w₂ labels a path from q₁ to q₃.

theorem Sipser.GNFA.accepts_of_single_transition {Q : Type u_1} {σ : Type u_2} [Fintype Q] {G : GNFA Q σ} {w : List σ} (h : w ∈ (G.δ G.start G.accept).matches') : G.accepts w

If a word w is matched by the regular expression labelling the direct arrow from G.start to G.accept, then G accepts w.