structure Regex.Data.BitMatrix (w h : Nat) : Type

• bv : BitVec (w * h)

theorem Regex.Data.BitMatrix.ext_iff {w h : Nat} {x y : BitMatrix w h} : x = y ↔ x.bv = y.bv

theorem Regex.Data.BitMatrix.ext {w h : Nat} {x y : BitMatrix w h} (bv : x.bv = y.bv) : x = y

def Regex.Data.instReprBitMatrix.repr {w✝ h✝ : Nat} : BitMatrix w✝ h✝ → Nat → Std.Format

Equations

• Regex.Data.instReprBitMatrix.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "bv" ++ Std.Format.text " := " ++ (Std.Format.nest 6 (repr x✝.bv)).group) " }"

instance Regex.Data.instReprBitMatrix {w✝ h✝ : Nat} : Repr (BitMatrix w✝ h✝)

Equations

• Regex.Data.instReprBitMatrix = { reprPrec := Regex.Data.instReprBitMatrix.repr }

instance Regex.Data.BitMatrix.instToString {w h : Nat} : ToString (BitMatrix w h)

Equations

• Regex.Data.BitMatrix.instToString = { toString := fun (m : Regex.Data.BitMatrix w h) => toString m.bv }

def Regex.Data.BitMatrix.zero (w h : Nat) : BitMatrix w h

Equations

• Regex.Data.BitMatrix.zero w h = { bv := BitVec.zero (w * h) }

def Regex.Data.BitMatrix.index {w h : Nat} (x : Fin w) (y : Fin h) : Fin (w * h)

Equations

• Regex.Data.BitMatrix.index x y = ⟨↑y * w + ↑x, ⋯⟩

theorem Regex.Data.BitMatrix.index_ne_of_ne_x {w h : Nat} (x x' : Fin w) (y y' : Fin h) (hx : x ≠ x') : index x y ≠ index x' y'

theorem Regex.Data.BitMatrix.index_ne_of_ne_y {w h : Nat} (x x' : Fin w) (y y' : Fin h) (hy : y ≠ y') : index x y ≠ index x' y'

theorem Regex.Data.BitMatrix.index_ne_of_ne {w h : Nat} (x x' : Fin w) (y y' : Fin h) (hne : x ≠ x' ∨ y ≠ y') : index x y ≠ index x' y'

def Regex.Data.BitMatrix.get {w h : Nat} (m : BitMatrix w h) (x : Fin w) (y : Fin h) : Bool

Equations

• m.get x y = m.bv[Regex.Data.BitMatrix.index x y]

@[simp]

theorem Regex.Data.BitMatrix.get_zero {w h : Nat} (x : Fin w) (y : Fin h) : (zero w h).get x y = false

theorem Regex.Data.BitMatrix.eq_of_get_eq {w h : Nat} {m m' : BitMatrix w h} (eq : ∀ (x : Fin w) (y : Fin h), m.get x y = m'.get x y) : m = m'

theorem Regex.Data.BitMatrix.eq_of_get_eq_iff {w h : Nat} {m m' : BitMatrix w h} : m = m' ↔ ∀ (x : Fin w) (y : Fin h), m.get x y = m'.get x y

def Regex.Data.BitMatrix.set {w h : Nat} (m : BitMatrix w h) (x : Fin w) (y : Fin h) : BitMatrix w h

Equations

• m.set x y = { bv := m.bv.set ↑(Regex.Data.BitMatrix.index x y) }

theorem Regex.Data.BitMatrix.get_set_eq {w h : Nat} {m : BitMatrix w h} (x : Fin w) (y : Fin h) : (m.set x y).get x y = true

theorem Regex.Data.BitMatrix.get_set_ne {w h : Nat} {m : BitMatrix w h} (x x' : Fin w) (y y' : Fin h) (hne : x ≠ x' ∨ y ≠ y') : (m.set x y).get x' y' = m.get x' y'

theorem Regex.Data.BitMatrix.get_set {w h : Nat} {m : BitMatrix w h} (x x' : Fin w) (y y' : Fin h) : (m.set x y).get x' y' = decide (x = x' ∧ y = y' ∨ m.get x' y' = true)

theorem Regex.Data.BitMatrix.get_set_of_get {w h : Nat} {m : BitMatrix w h} {x x' : Fin w} {y y' : Fin h} : m.get x y = true → (m.set x' y').get x y = true

theorem Regex.Data.BitMatrix.eq_set_of_get {w h : Nat} {m : BitMatrix w h} {x : Fin w} {y : Fin h} : m.get x y = true → m.set x y = m

def Regex.Data.BitMatrix.popcount {w h : Nat} (m : BitMatrix w h) : Nat

Equations

• m.popcount = m.bv.popcount

theorem Regex.Data.BitMatrix.popcount_le {w h : Nat} {m : BitMatrix w h} : m.popcount ≤ w * h

theorem Regex.Data.BitMatrix.popcount_decreasing {w h : Nat} (m : BitMatrix w h) (x : Fin w) (y : Fin h) (hget : ¬m.get x y = true) : w * h + 1 - (m.set x y).popcount < w * h + 1 - m.popcount