This file contains the formalisation of exercise 2.3 c and d which deals with simulations between NFAs. The exercise sheet is available at https://iccl.inf.tu-dresden.de/w/images/2/28/FS2025-Blatt-02.pdf.

structure NFASimulation {Sigma : Type u} {Q1 : Type u1} {Q2 : Type u2} [Fintype Q1] [Fintype Q2] [Fintype Sigma] (nfa1 : NFA Q1 Sigma) (nfa2 : NFA Q2 Sigma) : Type (max u1 u2)

• rel : Set (Q1 × Q2)
• start (q01 : Q1) : q01 ∈ nfa1.Q0 → ∃ (q02 : Q2), q02 ∈ nfa2.Q0 ∧ (q01, q02) ∈ self.rel
• step {q1 : Q1} {q2 : Q2} {a : Sigma} : (q1, q2) ∈ self.rel → ∀ (q1' : Q1), q1' ∈ nfa1.δ q1 a → ∃ (q2' : Q2), q2' ∈ nfa2.δ q2 a ∧ (q1', q2') ∈ self.rel
• final {q1 : Q1} {q2 : Q2} : (q1, q2) ∈ self.rel → q1 ∈ nfa1.F → q2 ∈ nfa2.F

theorem part_a {Sigma : Type u} {Q1 : Type u1} {Q2 : Type u2} [Fintype Q1] [Fintype Q2] [Fintype Sigma] {nfa1 : NFA Q1 Sigma} {nfa2 : NFA Q2 Sigma} (sim : NFASimulation nfa1 nfa2) : nfa1.Language ⊆ nfa2.Language

If there is a simulation between nfa1 and nfa2 then the language of nfa1 is a subset of the language of nfa2.

How about the other direction - does language inclusion also imply a simulation between the NFAs recognising the languages? We can show that this is not true by giving a counterexample. In order to define NFAs we first need Fintypes for Q and Sigma. We cannot just use strings because there are infinitely many of those. Instead we use a subtype of String defined by a list of strings (statesList and sigma).

@[implicit_reducible]

def statesList : List String

Equations

• statesList = ["q0", "q1", "q2"]

def sigma : List Char

Equations

• sigma = ['a', 'b']

@[implicit_reducible]

def Q : Type

Equations

• Q = subtype_of_list statesList

def ⅀ : Type

Equations

• ⅀ = subtype_of_list sigma

@[implicit_reducible]

instance instFintypeQ : Fintype Q

Equations

• instFintypeQ = { elems := statesList.attach, complete := ⋯ }

@[implicit_reducible]

instance instDecidableEqQ : DecidableEq Q

Equations

• instDecidableEqQ a b = a.instDecidableEq b

@[implicit_reducible]

instance instFintype⅀ : Fintype ⅀

Equations

• instFintype⅀ = { elems := instFintype⅀._aux_1, complete := instFintype⅀._proof_3 }

@[implicit_reducible]

instance instDecidableEq⅀ : DecidableEq ⅀

Equations

• instDecidableEq⅀ = instDecidableEq⅀._aux_1

def 𝓜 : NFA Q ⅀

Finally we can define the NFA 𝓜.

Equations

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

For our counterexample we will use 𝓜 and its powerset DFA 𝓜'. Their languages are equal but there is not simulation between 𝓜 and 𝓜'. Simulations are defined for NFAs so we convert 𝓜' back into an NFA 𝓜''.

def 𝓜_total : TotalDFA (Powertype Q) ⅀

Equations

• 𝓜_total = 𝓜.to_TotalDFA

def 𝓜_total' : NFA (Powertype Q) ⅀

Equations

• 𝓜_total' = 𝓜_total.to_NFA

theorem part_b : ∃ (nfa1 : NFA (Powertype Q) ⅀), ∃ (nfa2 : NFA Q ⅀), nfa1.Language ⊆ nfa2.Language ∧ ¬∃ (x : NFASimulation nfa1 nfa2), True