@[reducible, inline]

abbrev State : Type

Equations

• State = ℕ

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

• 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.dropLast_nodup {X : Type u_1} (l : List X) : l.Nodup → l.dropLast.Nodup

theorem List.dropLasnodup {X : Type u_1} (l : List X) : l.Nodup → l.dropLast.Nodup

@[simp]

theorem Array.not_elem_back_pop {X : Type u_1} (a : Array X) (x : X) : a.toList.Nodup → a.back? = some x → x ∉ a.pop

theorem Array.back?_mem {X : Type u_1} (a : Array X) (x : X) : a.back? = some x → x ∈ a

theorem Array.not_elem_back_pop_list {X : Type u_1} (a : Array X) (x : X) : a.toList.Nodup → a.back? = some x → x ∉ a.toList.dropLast

theorem Array.back_mem {X : Type u_1} (a : Array X) (x : X) : a.back? = some x → x ∈ a

theorem Array.mem_of_mem_pop {α : Type u_1} (a : Array α) (x : α) : x ∈ a.pop → x ∈ a

theorem Array.mem_push {α : Type u_1} (a : Array α) (x : α) (y : α) : x ∈ a.push y → x ∈ a ∨ x = y

theorem Std.HashMap.keys_nodup {K : Type u_1} {V : Type u_2} [BEq K] [Hashable K] (m : Std.HashMap K V) : m.keys.Nodup

@[simp]

theorem Std.HashMap.mem_keys_iff_mem {K : Type u_1} {V : Type u_2} [BEq K] [Hashable K] (m : Std.HashMap K V) (k : K) : k ∈ m.keys ↔ k ∈ m

theorem Std.HashMap.mem_keys_insert_new {K : Type u_1} {V : Type u_2} {v : V} [BEq K] [LawfulBEq K] [Hashable K] [LawfulHashable K] (m : Std.HashMap K V) (k : K) : k ∈ m.insert k v

theorem Std.HashMap.mem_keys_insert_old {K : Type u_1} {V : Type u_2} {v : V} [BEq K] [LawfulBEq K] [Hashable K] [LawfulHashable K] (m : Std.HashMap K V) (k : K) (k' : K) : k ∈ m → k ∈ m.insert k' v

theorem Std.HashMap.get?_none_not_mem {K : Type u_1} {V : Type u_2} [BEq K] [LawfulBEq K] [Hashable K] [LawfulHashable K] (m : Std.HashMap K V) (k : K) : m.get? k = none → k ∉ m

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} [BEq S] [LawfulBEq S] [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} [BEq S] [LawfulBEq S] [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} [BEq S] [LawfulBEq S] [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} [BEq S] [LawfulBEq S] [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.

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

Equations

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

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

Equations

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

def product {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (final? : Bool → Bool → Bool) (m1 : NFA A) (m2 : NFA A) : NFA A

Equations

• product final? m1 m2 = product.go final? m1 m2 (product.init m1 m2 { m := NFA.empty, map := ∅, worklist := ∅ })

def product.init {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (m1 : NFA A) (m2 : NFA A) (st : product.State) : product.State

Equations

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

@[irreducible]

def product.go {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (final? : Bool → Bool → Bool) (m1 : NFA A) (m2 : NFA A) (st0 : product.State) : NFA A

Equations

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

def NFA.inter {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (m1 : NFA A) (m2 : NFA A) : NFA A

Equations

• m1.inter m2 = product (fun (b1 b2 : Bool) => b1 && b2) m1 m2

def NFA.union {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (m1 : NFA A) (m2 : NFA A) : NFA A

Equations

• m1.union m2 = product (fun (b1 b2 : Bool) => b1 || b2) m1.addSink m2.addSink

def HashSet.inter {A : Type u_1} [BEq A] [Hashable A] (m1 : Std.HashSet A) (m2 : Std.HashSet A) : Std.HashSet A

Equations

• HashSet.inter m1 m2 = Std.HashSet.fold (fun (mi : Std.HashSet A) (x : A) => if m2.contains x = true then mi.insert x else mi) Std.HashSet.empty m1

def Std.HashSet.isDisjoint {A : Type u_1} [BEq A] [Hashable A] (m1 : Std.HashSet A) (m2 : Std.HashSet A) : Bool

Equations

• m1.isDisjoint m2 = (HashSet.inter m1 m2).isEmpty

def HashSet.areIncluded {A : Type u_1} [BEq A] [Hashable A] (m1 : Std.HashSet A) (m2 : Std.HashSet A) : Bool

Equations

• HashSet.areIncluded m1 m2 = m1.all fun (x : A) => m2.contains x

instance hashableHashSet {A : Type} [BEq A] [Hashable A] : Hashable (Std.HashSet A)

Equations

• hashableHashSet = { hash := fun (s : Std.HashSet A) => Std.HashSet.fold (fun (h : UInt64) (x : A) => mixHash h (hash x)) 0 s }

def NFA.determinize {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (mi : NFA A) : NFA A

Equations

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

@[irreducible]

def NFA.determinize.go {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (mi : NFA A) (st : NFA.determinize.St) : NFA A

Equations

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

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

Equations

• m.neg = m.determinize.flipFinals

def NFA.isIncluded {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (m1 : NFA A) (m2 : NFA A) : Bool

Returns true when L(m1) ⊆ L(m2)

Equations

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

@[irreducible]

def NFA.isIncluded.go {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (m1 : NFA A) (m2 : NFA A) (st : isIncluded.State) : Bool

Equations

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

def NFA.isUniversal {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (m : NFA A) : Bool

Returns true when L(m) = A*

Equations

• m.isUniversal = NFA.isUniversal.go m { visited := [], worklist := [m.initials] }

@[irreducible]

def NFA.isUniversal.go {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (m : NFA A) (st : isUniversal.State) : Bool

Equations

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

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

Recognizes the empty word

Equations

• NFA.emptyWord = match NFA.empty.newState with | (s, m) => let m := m.addInitial s; let m := m.addFinal s; m

def NFA.isUniversal' {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (m : NFA A) : Bool

Returns true when L(m) ∪ {ε} = A*. This is useful because the bitvector of with width zero has strange properties.

Equations

• m.isUniversal' = (m.union NFA.emptyWord).isUniversal

def NFA.isEmpty {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (m : NFA A) : Bool

Equations

• m.isEmpty = m.finals.isEmpty

def NFA.isNotEmpty {A : Type} [BEq A] [Hashable A] [DecidableEq A] [FinEnum A] (m : NFA A) : Bool

Equations

• m.isNotEmpty = !m.finals.isEmpty

instance instHashableBitVec_sSA {n : ℕ} : Hashable (BitVec n)

Equations

• instHashableBitVec_sSA = { hash := fun (x : BitVec n) => hash x.toFin }

def transport {n2 : ℕ} {n1 : ℕ} (f : Fin n2 → Fin n1) (bv : BitVec n1) : BitVec n2

Equations

• transport f bv = List.foldl (fun (bv' : BitVec n2) (i : Fin n2) => bv' ||| BitVec.twoPow n2 ↑i * ↑bv[f i].toNat) (BitVec.zero n2) (Fin.list n2)

def NFA.lift {n1 : ℕ} {n2 : ℕ} (m1 : NFA (BitVec n1)) (f : Fin n1 → Fin n2) : NFA (BitVec n2)

Equations

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

def NFA.proj {n1 : ℕ} {n2 : ℕ} (m1 : NFA (BitVec n1)) (f : Fin n2 → Fin n1) : NFA (BitVec n2)

Equations

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