@[reducible, inline]

abbrev State : Type

Equations

• State = ℕ

structure NFA (A : Type) [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] : Type

The definition of a computational automaton. It is meant to be more efficient than the definition in Mathlib.

• stateMax : State
• initials : Std.HashSet State
• finals : Std.HashSet State
• trans : Std.HashMap (State × A) (Std.HashSet State)

instance instReprNFA : {A : Type} → {inst : BEq A} → {inst_1 : Hashable A} → {inst_2 : DecidableEq A} → {inst_3 : FinEnum A} → [inst_4 : Repr A] → Repr (NFA A)

Equations

• instReprNFA = { reprPrec := reprNFA✝ }

def NFA.empty {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] : NFA A

Equations

• NFA.empty = { stateMax := 0, initials := ∅, finals := ∅, trans := ∅ }

def NFA.newState {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (m : NFA A) : State × NFA A

Equations

• m.newState = (m.stateMax, { stateMax := m.stateMax + 1, initials := m.initials, finals := m.finals, trans := m.trans })

def NFA.addTrans {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (m : NFA A) (a : A) (s : State) (s' : State) : NFA A

Equations

• m.addTrans a s s' = { stateMax := m.stateMax, initials := m.initials, finals := m.finals, trans := m.trans.insert (s, a) ((m.trans.getD (s, a) ∅).insert s') }

def NFA.addManyTrans {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (m : NFA A) (a : List A) (s : State) (s' : State) : NFA A

Equations

• m.addManyTrans a s s' = List.foldl (fun (m : NFA A) (a : A) => m.addTrans a s s') m a

def NFA.addInitial {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (m : NFA A) (s : State) : NFA A

Equations

• m.addInitial s = { stateMax := m.stateMax, initials := m.initials.insert s, finals := m.finals, trans := m.trans }

def NFA.addFinal {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (m : NFA A) (s : State) : NFA A

Equations

• m.addFinal s = { stateMax := m.stateMax, initials := m.initials, finals := m.finals.insert s, trans := m.trans }

def NFA.transSet {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (m : NFA A) (ss : Std.HashSet State) (a : A) : Std.HashSet State

Equations

• m.transSet ss a = Std.HashSet.fold (fun (ss' : Std.HashSet State) (s : State) => ss'.insertMany (m.trans.getD (s, a) ∅)) ∅ ss

instance NFA_Inhabited {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] : Inhabited (NFA A)

Equations

• NFA_Inhabited = { default := NFA.empty }

@[reducible, inline]

abbrev inSS {S : Type} (stateSpace : Finset S) : Type

Equations

• inSS stateSpace = { sa : S // sa ∈ stateSpace }

theorem List.perm_subset_iff_right {α : Type u_1} {l1 : List α} {l2 : List α} (hperm : l1.Perm l2) (l : List α) : l ⊆ l1 ↔ l ⊆ l2

theorem addOrCreateState_grow (A : Type) [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] {S : Type} [Hashable S] [DecidableEq S] (stateSpace : Finset S) (st : worklist.St A stateSpace) (b : Bool) (sa : inSS stateSpace) : match worklist.St.addOrCreateState A stateSpace st b sa with | (fst, st') => ∃ (sas : List (inSS stateSpace)), st'.map.keys.Perm (sas ++ st.map.keys) ∧ st'.worklist.toList = st.worklist.toList ++ sas

theorem processOneElem_grow (A : Type) [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] {S : Type} [Hashable S] [DecidableEq S] (stateSpace : Finset S) (st : worklist.St A stateSpace) (final : S → Bool) (a : A) (sa' : inSS stateSpace) (s : State) : let st' := processOneElem A stateSpace final s st (a, sa'); ∃ (sas : List (inSS stateSpace)), st'.map.keys.Perm (sas ++ st.map.keys) ∧ st'.worklist.toList = st.worklist.toList ++ sas

def worklist.initState (A : Type) [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] {S : Type} [Hashable S] [DecidableEq S] (stateSpace : Finset S) (init : inSS stateSpace) : worklist.St A stateSpace

Equations

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

def worklistRunAux (A : Type) [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] {S : Type} [Hashable S] [DecidableEq S] (stateSpace : Finset S) (final : S → Bool) (f : S → Array (A × inSS stateSpace)) (init : inSS stateSpace) : NFA A

Equations

• worklistRunAux A stateSpace final f init = worklistRunAux.go A stateSpace final f init (worklist.initState A stateSpace init)

@[irreducible]

def worklistRunAux.go (A : Type) [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] {S : Type} [Hashable S] [DecidableEq S] (stateSpace : Finset S) (final : S → Bool) (f : S → Array (A × inSS stateSpace)) (init : inSS stateSpace) (st0 : worklist.St A stateSpace) : NFA A

Equations

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