structure Regex.Data.SparseSet (n : Nat) : Type

• count : Nat
• dense : Vector (Fin n) n
• sparse : Vector (Fin n) n
• sparse_dense (i : Fin n) : ↑i < self.count → self.sparse[↑self.dense[↑i]] = i
• le_count : self.count ≤ n

@[inline]

def Regex.Data.SparseSet.mem {n : Nat} (s : SparseSet n) (i : Fin n) : Bool

Equations

• s.mem i = (decide (↑s.sparse[i] < s.count) && s.dense[s.sparse[i]] == i)

instance Regex.Data.SparseSet.instMembershipFin {n : Nat} : Membership (Fin n) (SparseSet n)

Equations

• Regex.Data.SparseSet.instMembershipFin = { mem := fun (s : Regex.Data.SparseSet n) (i : Fin n) => s.mem i = true }

def Regex.Data.SparseSet.Subset ⦃n : Nat⦄ (s₁ s₂ : SparseSet n) : Prop

Equations

• s₁.Subset s₂ = ∀ (i : Fin n), i ∈ s₁ → i ∈ s₂

instance Regex.Data.SparseSet.instHasSubset {n : Nat} : HasSubset (SparseSet n)

Equations

• Regex.Data.SparseSet.instHasSubset = { Subset := Regex.Data.SparseSet.Subset }

@[inline]

instance Regex.Data.SparseSet.instDecidableMemFin {n : Nat} {s : SparseSet n} {i : Fin n} : Decidable (i ∈ s)

Equations

• Regex.Data.SparseSet.instDecidableMemFin = match h : s.mem i with | true => isTrue h | false => isFalse ⋯

def Regex.Data.SparseSet.empty {n : Nat} : SparseSet n

Equations

• Regex.Data.SparseSet.empty = { count := 0, dense := Vector.ofFn fun (x : Fin n) => ⟨0, ⋯⟩, sparse := Vector.ofFn fun (x : Fin n) => ⟨0, ⋯⟩, sparse_dense := ⋯, le_count := ⋯ }

def Regex.Data.SparseSet.insert {n : Nat} (s : SparseSet n) (i : Fin n) (mem : ¬i ∈ s) : SparseSet n

Equations

• s.insert i mem = { count := s.count + 1, dense := s.dense.set s.count i ⋯, sparse := s.sparse.set ↑i ⟨s.count, ⋯⟩ ⋯, sparse_dense := ⋯, le_count := ⋯ }

@[simp]

theorem Regex.Data.SparseSet.mem_insert {n : Nat} {s : SparseSet n} {i : Fin n} (h : ¬i ∈ s) : i ∈ s.insert i h

def Regex.Data.SparseSet.clear {n : Nat} (s : SparseSet n) : SparseSet n

Equations

• s.clear = { count := 0, dense := s.dense, sparse := s.sparse, sparse_dense := ⋯, le_count := ⋯ }

def Regex.Data.SparseSet.isEmpty {n : Nat} (s : SparseSet n) : Bool

Equations

• s.isEmpty = decide (s.count = 0)

@[simp]

theorem Regex.Data.SparseSet.isEmpty_empty {n : Nat} : empty.isEmpty = true

@[simp]

theorem Regex.Data.SparseSet.isEmpty_clear {n : Nat} {s : SparseSet n} : s.clear.isEmpty = true

@[simp]

theorem Regex.Data.SparseSet.not_mem_of_isEmpty {n : Nat} {s : SparseSet n} {i : Fin n} (h : s.isEmpty = true) : ¬i ∈ s

@[inline]

def Regex.Data.SparseSet.get {n : Nat} (s : SparseSet n) (i : Nat) (h : i < s.count) : Fin n

Equations

• s.get i h = s.dense[i]

@[inline]

instance Regex.Data.SparseSet.instGetElemNatFinLtCount {n : Nat} : GetElem (SparseSet n) Nat (Fin n) fun (s : SparseSet n) (i : Nat) => i < s.count

Equations

• Regex.Data.SparseSet.instGetElemNatFinLtCount = { getElem := Regex.Data.SparseSet.get }

def Regex.Data.SparseSet.measure {n : Nat} (s : SparseSet n) : Nat

Equations

• s.measure = n - s.count

theorem Regex.Data.SparseSet.measure_insert {n : Nat} {s : SparseSet n} {i : Fin n} (h : ¬i ∈ s) : (s.insert i h).measure = s.measure - 1

theorem Regex.Data.SparseSet.lt_measure_insert {n : Nat} {s : SparseSet n} {i : Fin n} (h : ¬s.mem i = true) : (s.insert i h).measure < s.measure

theorem Regex.Data.SparseSet.lt_measure_insert' {n : Nat} {s : SparseSet n} {i : Fin n} (h : ¬i ∈ s) : (s.insert i h).measure < s.measure