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

instance Regex.Data.instReprSparseSet {n : Nat} : Repr (SparseSet n)

Equations

• Regex.Data.instReprSparseSet = { reprPrec := fun (s : Regex.Data.SparseSet n) (i : Nat) => reprPrec (s.dense.toSubarray 0 s.count) i }

instance Regex.Data.instToStringSparseSet {n : Nat} : ToString (SparseSet n)

Equations

• Regex.Data.instToStringSparseSet = { toString := fun (s : Regex.Data.SparseSet n) => toString (s.dense.toSubarray 0 s.count) }

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 := ⋯ }

theorem Regex.Data.SparseSet.sparse_dense_fin {n : Nat} {s : SparseSet n} {i : Fin n} (h : ↑i < s.count) : s.sparse[s.dense[i]] = i

@[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 }

@[simp]

theorem Regex.Data.SparseSet.mem_mem {n : Nat} {s : SparseSet n} {i : Fin n} : i ∈ s ↔ 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 ⋯

theorem Regex.Data.SparseSet.mem_dense_of_lt {n : Nat} {s : SparseSet n} {i : Fin n} (h : ↑i < s.count) : s.dense[i] ∈ s

theorem Regex.Data.SparseSet.dense_inj {n : Nat} {s : SparseSet n} {i j : Fin n} (hi : ↑i < s.count) (hj : ↑j < s.count) (eq : s.dense[i] = s.dense[j]) : i = j

theorem Regex.Data.SparseSet.dense_surj {n : Nat} {s : SparseSet n} {j : Fin n} (h : j ∈ s) : ∃ (i : Fin n), ↑i < s.count ∧ s.dense[i] = j

theorem Regex.Data.SparseSet.dense_sparse_of_full {n : Nat} {s : SparseSet n} {j : Fin n} (h : n ≤ s.count) : s.dense[s.sparse[j]] = j

theorem Regex.Data.SparseSet.lt_of_mem {n : Nat} {s : SparseSet n} (i : Fin n) (h : ¬i ∈ s) : s.count < n

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

Equations

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

@[simp]

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

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.foldl {n : Nat} {α : Type} (f : α → Fin n → α) (init : α) (s : SparseSet n) : α

Equations

• Regex.Data.SparseSet.foldl f init s = Regex.Data.SparseSet.foldl.go f s init 0 ⋯

@[irreducible, specialize #[]]

def Regex.Data.SparseSet.foldl.go {n : Nat} {α : Type} (f : α → Fin n → α) (s : SparseSet n) (accum : α) (i : Nat) (hle : i ≤ s.count) : α

Equations

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

@[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).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).measure < s.measure

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