Documentation

Regex.Data.BVPos

structure Regex.Data.BVPos {s : String} (startPos : s.ValidPos) :

A valid position in a string with a lower bound.

current : s.ValidPos
le : startPos ≤ self.current

Instances For

theorem Regex.Data.BVPos.ext_iff {s : String} {startPos : s.ValidPos} {x y : BVPos startPos} :

x = y ↔ x.current = y.current

theorem Regex.Data.BVPos.ext {s : String} {startPos : s.ValidPos} {x y : BVPos startPos} (current : x.current = y.current) :

x = y

def Regex.Data.instDecidableEqBVPos.decEq {s✝ : String} {startPos✝ : s✝.ValidPos} (x✝ x✝¹ : BVPos startPos✝) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

instance Regex.Data.instDecidableEqBVPos {s✝ : String} {startPos✝ : s✝.ValidPos} :

DecidableEq (BVPos startPos✝)

Equations

Regex.Data.instDecidableEqBVPos = Regex.Data.instDecidableEqBVPos.decEq

def String.endBVPos (s : String) (startPos : s.ValidPos) :

Regex.Data.BVPos startPos

Equations

s.endBVPos startPos = { current := s.endValidPos, le := ⋯ }

Instances For

def Regex.Data.BVPos.start {s : String} (startPos : s.ValidPos) :

BVPos startPos

Equations

Regex.Data.BVPos.start startPos = { current := startPos, le := ⋯ }

Instances For

def Regex.Data.BVPos.index {s : String} {startPos : s.ValidPos} (bp : BVPos startPos) :

Fin (startPos.remainingBytes + 1)

Equations

bp.index = ⟨startPos.offset.byteDistance bp.current.offset, ⋯⟩

Instances For

theorem Regex.Data.BVPos.ne_iff_current_ne {s : String} {startPos : s.ValidPos} {bp₁ bp₂ : BVPos startPos} :

bp₁ ≠ bp₂ ↔ bp₁.current ≠ bp₂.current

theorem Regex.Data.BVPos.ne_end_iff_current_ne_end {s : String} {startPos : s.ValidPos} {bp : BVPos startPos} :

bp ≠ s.endBVPos startPos ↔ bp.current ≠ s.endValidPos

def Regex.Data.BVPos.next {s : String} {startPos : s.ValidPos} (bp : BVPos startPos) (h : bp ≠ s.endBVPos startPos) :

BVPos startPos

Equations

bp.next h = { current := bp.current.next ⋯, le := ⋯ }

Instances For

@[simp]

theorem Regex.Data.BVPos.next_current {s : String} {startPos : s.ValidPos} {bp : BVPos startPos} (ne : bp ≠ s.endBVPos startPos) :

(bp.next ne).current = bp.current.next ⋯

@[simp]

theorem Regex.Data.BVPos.endBVPos_current {s : String} {startPos : s.ValidPos} :

(s.endBVPos startPos).current = s.endValidPos

def Regex.Data.BVPos.nextn {s : String} {startPos : s.ValidPos} (bp : BVPos startPos) (n : Nat) :

BVPos startPos

Equations

bp.nextn 0 = bp
bp.nextn n_2.succ = if h : bp ≠ s.endBVPos startPos then (bp.next h).nextn n_2 else bp

Instances For

def Regex.Data.BVPos.get {s : String} {startPos : s.ValidPos} (bp : BVPos startPos) (h : bp ≠ s.endBVPos startPos) :

Equations

bp.get h = bp.current.get ⋯

Instances For

def Regex.Data.BVPos.lt {s : String} {startPos : s.ValidPos} (bp₁ bp₂ : BVPos startPos) :

Equations

bp₁.lt bp₂ = (bp₁.current < bp₂.current)

Instances For

instance Regex.Data.BVPos.instLT {s : String} {startPos : s.ValidPos} :

LT (BVPos startPos)

Equations

Regex.Data.BVPos.instLT = { lt := Regex.Data.BVPos.lt }

@[simp]

theorem Regex.Data.BVPos.lt_next {s : String} {startPos : s.ValidPos} {bp : BVPos startPos} (h : bp ≠ s.endBVPos startPos) :

bp < bp.next h

theorem Regex.Data.BVPos.wellFounded_gt {s : String} {startPos : s.ValidPos} :

WellFounded fun (p q : BVPos startPos) => q < p

instance Regex.Data.BVPos.instWellFoundedRelation {s : String} {startPos : s.ValidPos} :

WellFoundedRelation (BVPos startPos)

Equations

Regex.Data.BVPos.instWellFoundedRelation = { rel := fun (p q : Regex.Data.BVPos startPos) => q < p, wf := ⋯ }

instance Regex.Data.BVPos.instLE {s : String} {startPos : s.ValidPos} :

LE (BVPos startPos)

Equations

Regex.Data.BVPos.instLE = { le := fun (bp₁ bp₂ : Regex.Data.BVPos startPos) => bp₁.current ≤ bp₂.current }

theorem Regex.Data.BVPos.le_iff {s : String} {startPos : s.ValidPos} {bp₁ bp₂ : BVPos startPos} :

bp₁ ≤ bp₂ ↔ bp₁.current ≤ bp₂.current

theorem Regex.Data.BVPos.le_refl {s : String} {startPos : s.ValidPos} (bp : BVPos startPos) :

bp ≤ bp

theorem Regex.Data.BVPos.le_trans {s : String} {startPos : s.ValidPos} {bp₁ bp₂ bp₃ : BVPos startPos} (le₁₂ : bp₁ ≤ bp₂) (le₂₃ : bp₂ ≤ bp₃) :

bp₁ ≤ bp₃

theorem Regex.Data.BVPos.le_of_lt {s : String} {startPos : s.ValidPos} {bp₁ bp₂ : BVPos startPos} (lt : bp₁ < bp₂) :

bp₁ ≤ bp₂

theorem Regex.Data.BVPos.not_le_of_lt {s : String} {startPos : s.ValidPos} {bp₁ bp₂ : BVPos startPos} (lt : bp₁ < bp₂) :

¬bp₂ ≤ bp₁

theorem Regex.Data.BVPos.not_lt_of_le {s : String} {startPos : s.ValidPos} {bp₁ bp₂ : BVPos startPos} (le : bp₂ ≤ bp₁) :

¬bp₁ < bp₂

theorem Regex.Data.BVPos.lt_or_eq_of_le {s : String} {startPos : s.ValidPos} {bp₁ bp₂ : BVPos startPos} (le : bp₁ ≤ bp₂) :

bp₁ < bp₂ ∨ bp₁ = bp₂

theorem Regex.Data.BVPos.le_endBVPos {s : String} {startPos : s.ValidPos} (bp : BVPos startPos) :

bp ≤ s.endBVPos startPos

theorem Regex.Data.BVPos.lt_next_iff_lt_or_eq {s : String} {startPos : s.ValidPos} {bp₁ bp₂ : BVPos startPos} (h : bp₂ ≠ s.endBVPos startPos) :

bp₁ < bp₂.next h ↔ bp₁ < bp₂ ∨ bp₁ = bp₂