Documentation

Regex.Data.BitMatrix

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

bv : BitVec (w * h)

Instances For

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

instance Regex.Data.instReprBitMatrix {w✝ h✝ : Nat} :

Repr (BitMatrix w✝ h✝)

Equations

Regex.Data.instReprBitMatrix = { reprPrec := Regex.Data.reprBitMatrix✝ }

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) :

Equations

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

Instances For

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, ⋯⟩

Instances For

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) :

Equations

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

Instances For

@[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) :

Equations

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

Instances For

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) :

Equations

m.popcount = m.bv.popcount

Instances For

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