RegexCorrectness.Data.BoundedIterator

source

theorem Regex.Data.BoundedIterator.ext_pos {startIdx maxIdx : ℕ} {bit₁ bit₂ : BoundedIterator startIdx maxIdx} (h₁ : bit₁.toString = bit₂.toString) (h₂ : bit₁.pos = bit₂.pos) :

bit₁ = bit₂

source

theorem Regex.Data.BoundedIterator.ext_pos_iff {startIdx maxIdx : ℕ} {bit₁ bit₂ : BoundedIterator startIdx maxIdx} :

bit₁ = bit₂ ↔ bit₁.toString = bit₂.toString ∧ bit₁.pos = bit₂.pos

source

theorem Regex.Data.BoundedIterator.ext_index {startIdx maxIdx : ℕ} {bit₁ bit₂ : BoundedIterator startIdx maxIdx} (h₁ : bit₁.toString = bit₂.toString) (h₂ : bit₁.index = bit₂.index) :

bit₁ = bit₂

source

theorem Regex.Data.BoundedIterator.ext_index_iff {startIdx maxIdx : ℕ} {bit₁ bit₂ : BoundedIterator startIdx maxIdx} :

bit₁ = bit₂ ↔ bit₁.toString = bit₂.toString ∧ bit₁.index = bit₂.index

source

theorem Regex.Data.BoundedIterator.next_toString {startIdx maxIdx : ℕ} {bit : BoundedIterator startIdx maxIdx} (h : bit.hasNext = true) :

(bit.next h).toString = bit.toString

source

theorem Regex.Data.BoundedIterator.byteIdx_lt_next_byteIdx {startIdx maxIdx : ℕ} {bit : BoundedIterator startIdx maxIdx} (h : bit.hasNext = true) :

bit.pos.byteIdx < (bit.next h).pos.byteIdx

source

theorem Regex.Data.BoundedIterator.pos_lt_next_pos {startIdx maxIdx : ℕ} {bit : BoundedIterator startIdx maxIdx} (h : bit.hasNext = true) :

bit.pos < (bit.next h).pos

source

theorem Regex.Data.BoundedIterator.pos_eq_of_not_hasNext {startIdx maxIdx : ℕ} {bit : BoundedIterator startIdx maxIdx} (hnext : ¬bit.hasNext = true) :

bit.pos = bit.toString.endPos

source

theorem Regex.Data.BoundedIterator.valid_of_it_valid {startIdx maxIdx : ℕ} {bit : BoundedIterator startIdx maxIdx} (v : bit.it.Valid) :

bit.Valid

source

theorem Regex.Data.BoundedIterator.valid_of_valid {startIdx maxIdx : ℕ} {bit : BoundedIterator startIdx maxIdx} (v : bit.Valid) :

bit.it.Valid

source

theorem Regex.Data.BoundedIterator.next_valid {startIdx maxIdx : ℕ} {bit : BoundedIterator startIdx maxIdx} (h : bit.hasNext = true) (v : bit.Valid) :

(bit.next h).Valid

source

@[simp]

theorem Regex.Data.BoundedIterator.toEnd_toString {startIdx maxIdx : ℕ} (bit : BoundedIterator startIdx maxIdx) :

bit.toEnd.toString = bit.toString

source

theorem Regex.Data.BoundedIterator.toEnd_pos {startIdx maxIdx : ℕ} (bit : BoundedIterator startIdx maxIdx) :

bit.toEnd.pos = bit.toString.endPos

source

theorem Regex.Data.BoundedIterator.toEnd_valid {startIdx maxIdx : ℕ} (bit : BoundedIterator startIdx maxIdx) :

bit.toEnd.Valid

source

theorem Regex.Data.BoundedIterator.pos_le_toEnd_pos {startIdx maxIdx : ℕ} (bit : BoundedIterator startIdx maxIdx) :

bit.pos ≤ bit.toEnd.pos

source

theorem Regex.Data.BoundedIterator.toEnd_not_hasNext {startIdx maxIdx : ℕ} (bit : BoundedIterator startIdx maxIdx) :

¬bit.toEnd.hasNext = true

source

@[simp]

theorem Regex.Data.BoundedIterator.next_toEnd {startIdx maxIdx : ℕ} {bit : BoundedIterator startIdx maxIdx} (h : bit.hasNext = true) :

(bit.next h).toEnd = bit.toEnd

source

theorem Regex.Data.BoundedIterator.nextn_valid {startIdx maxIdx : ℕ} {bit : BoundedIterator startIdx maxIdx} {n : ℕ} (v : bit.Valid) :

(bit.nextn n).Valid

source

theorem Regex.Data.BoundedIterator.next_nextn {startIdx maxIdx : ℕ} {bit : BoundedIterator startIdx maxIdx} {n : ℕ} (hnext : bit.hasNext = true) :

(bit.next hnext).nextn n = bit.nextn (n + 1)

source

theorem Regex.Data.BoundedIterator.byteIdx_le_nextn_byteIdx {startIdx maxIdx : ℕ} (bit : BoundedIterator startIdx maxIdx) (n : ℕ) :

bit.pos.byteIdx ≤ (bit.nextn n).pos.byteIdx

source

theorem Regex.Data.BoundedIterator.nextn_toString {startIdx maxIdx : ℕ} {bit : BoundedIterator startIdx maxIdx} {n : ℕ} :

(bit.nextn n).toString = bit.toString

source

theorem Regex.Data.BoundedIterator.hasNext_of_nextn_hasNext {startIdx maxIdx : ℕ} {bit : BoundedIterator startIdx maxIdx} {n : ℕ} (hnext : (bit.nextn n).hasNext = true) :

bit.hasNext = true

source

theorem Regex.Data.BoundedIterator.nextn_next_eq_next_nextn {startIdx maxIdx : ℕ} {bit : BoundedIterator startIdx maxIdx} {n : ℕ} (hnext : (bit.nextn n).hasNext = true) :

(bit.nextn n).next hnext = (bit.next ⋯).nextn n

source

theorem Regex.Data.BoundedIterator.nextn_next {startIdx maxIdx : ℕ} {bit : BoundedIterator startIdx maxIdx} {n : ℕ} (hnext : (bit.nextn n).hasNext = true) :

(bit.nextn n).next hnext = bit.nextn (n + 1)

source

theorem Regex.Data.BoundedIterator.nextn_not_hasNext {startIdx maxIdx : ℕ} {bit : BoundedIterator startIdx maxIdx} {n : ℕ} (hnext : ¬bit.hasNext = true) :

bit.nextn n = bit

source

theorem Regex.Data.BoundedIterator.nextn_add {startIdx maxIdx : ℕ} (bit : BoundedIterator startIdx maxIdx) (n₁ n₂ : ℕ) :

bit.nextn (n₁ + n₂) = (bit.nextn n₁).nextn n₂

source

def Regex.Data.BoundedIterator.ValidFor {startIdx maxIdx : ℕ} (l r : List Char) (bit : BoundedIterator startIdx maxIdx) :

Prop

Equations

Regex.Data.BoundedIterator.ValidFor l r bit = String.Iterator.ValidFor l r bit.it

Instances For

source

theorem Regex.Data.BoundedIterator.ValidFor.hasNext {startIdx maxIdx : ℕ} {l r : List Char} {bit : BoundedIterator startIdx maxIdx} (vf : ValidFor l r bit) :

bit.hasNext = true ↔ r ≠ []

source

theorem Regex.Data.BoundedIterator.ValidFor.next {startIdx maxIdx : ℕ} {l : List Char} {c : Char} {r : List Char} {bit : BoundedIterator startIdx maxIdx} (vf : ValidFor l (c :: r) bit) :

ValidFor (c :: l) r (bit.next ⋯)

source

theorem Regex.Data.BoundedIterator.ValidFor.next' {startIdx maxIdx : ℕ} {l r : List Char} {bit : BoundedIterator startIdx maxIdx} (h : bit.hasNext = true) (vf : ValidFor l r bit) :

∃ (c : Char ), ∃ (r' : List Char), r = c :: r' ∧ ValidFor (c :: l) r' (bit.next h)

source

theorem Regex.Data.BoundedIterator.ValidFor.curr {startIdx maxIdx : ℕ} {l : List Char} {c : Char} {r : List Char} {bit : BoundedIterator startIdx maxIdx} (vf : ValidFor l (c :: r) bit) :

bit.curr ⋯ = c

source

theorem Regex.Data.BoundedIterator.ValidFor.toString {startIdx maxIdx : ℕ} {l r : List Char} {bit : BoundedIterator startIdx maxIdx} (vf : ValidFor l r bit) :

bit.toString = { data := l.reverse ++ r }

source

theorem Regex.Data.BoundedIterator.ValidFor.pos {startIdx maxIdx : ℕ} {l r : List Char} {bit : BoundedIterator startIdx maxIdx} (vf : ValidFor l r bit) :

bit.pos = { byteIdx := String.utf8Len l }

source

theorem Regex.Data.BoundedIterator.ValidFor.valid {startIdx maxIdx : ℕ} {l r : List Char} {bit : BoundedIterator startIdx maxIdx} (vf : ValidFor l r bit) :

bit.Valid

source

theorem Regex.Data.BoundedIterator.ValidFor.eq {startIdx maxIdx : ℕ} {l l' r r' : List Char} {bit : BoundedIterator startIdx maxIdx} (vf : ValidFor l r bit) (vf' : ValidFor l' r' bit) :

l = l' ∧ r = r'

source

theorem Regex.Data.BoundedIterator.ValidFor.eq_it {startIdx maxIdx : ℕ} {l r : List Char} {bit bit' : BoundedIterator startIdx maxIdx} (vf : ValidFor l r bit) (vf' : ValidFor l r bit') :

bit = bit'

source

theorem Regex.Data.BoundedIterator.Valid.validFor {startIdx maxIdx : ℕ} {bit : BoundedIterator startIdx maxIdx} (v : bit.Valid) :

∃ (l : List Char), ∃ (r : List Char), ValidFor l r bit

source

theorem Regex.Data.BoundedIterator.Valid.validFor_of_hasNext {startIdx maxIdx : ℕ} {bit : BoundedIterator startIdx maxIdx} (h : bit.hasNext = true) (v : bit.Valid) :

∃ (l : List Char), ∃ (r : List Char), ValidFor l (bit.curr h :: r) bit

source

theorem Regex.Data.BoundedIterator.Valid.next {startIdx maxIdx : ℕ} {bit : BoundedIterator startIdx maxIdx} (hnext : bit.hasNext = true) (v : bit.Valid) :

(bit.next hnext).Valid

source

theorem Regex.Data.BoundedIterator.toEnd_validFor {startIdx maxIdx : ℕ} (bit : BoundedIterator startIdx maxIdx) :

ValidFor bit.toString.data.reverse [] bit.toEnd

source

theorem Regex.Data.BoundedIterator.eq_of_valid_of_next_eq {startIdx maxIdx : ℕ} {bit bit' : BoundedIterator startIdx maxIdx} (v : bit.Valid) (v' : bit'.Valid) (hnext : bit.hasNext = true) (hnext' : bit'.hasNext = true) (eq : bit.next hnext = bit'.next hnext') :

bit = bit'

source

inductive Regex.Data.BoundedIterator.Reaches {startIdx maxIdx : ℕ} :

BoundedIterator startIdx maxIdx → BoundedIterator startIdx maxIdx → Prop

refl {startIdx maxIdx : ℕ} {bit : BoundedIterator startIdx maxIdx} (v : bit.Valid) : bit.Reaches bit
next {startIdx maxIdx : ℕ} {bit₁ bit₂ : BoundedIterator startIdx maxIdx} (v : bit₁.Valid) (hnext : bit₁.hasNext = true) (rest : (bit₁.next hnext).Reaches bit₂) : bit₁.Reaches bit₂

Instances For

source

theorem Regex.Data.BoundedIterator.Reaches.trans {startIdx maxIdx : ℕ} {bit₁ bit₂ bit₃ : BoundedIterator startIdx maxIdx} (h₁ : bit₁.Reaches bit₂) (h₂ : bit₂.Reaches bit₃) :

bit₁.Reaches bit₃

source

theorem Regex.Data.BoundedIterator.Reaches.validL {startIdx maxIdx : ℕ} {bit₁ bit₂ : BoundedIterator startIdx maxIdx} (h : bit₁.Reaches bit₂) :

bit₁.Valid

source

theorem Regex.Data.BoundedIterator.Reaches.validR {startIdx maxIdx : ℕ} {bit₁ bit₂ : BoundedIterator startIdx maxIdx} (h : bit₁.Reaches bit₂) :

bit₂.Valid

source

theorem Regex.Data.BoundedIterator.Reaches.toString {startIdx maxIdx : ℕ} {bit₁ bit₂ : BoundedIterator startIdx maxIdx} (h : bit₁.Reaches bit₂) :

bit₂.toString = bit₁.toString

source

theorem Regex.Data.BoundedIterator.Reaches.le_pos {startIdx maxIdx : ℕ} {bit₁ bit₂ : BoundedIterator startIdx maxIdx} (h : bit₁.Reaches bit₂) :

bit₁.pos ≤ bit₂.pos

source

theorem Regex.Data.BoundedIterator.Reaches.next' {startIdx maxIdx : ℕ} {bit₁ bit₂ : BoundedIterator startIdx maxIdx} (hnext₂ : bit₂.hasNext = true) (h : bit₁.Reaches bit₂) :

bit₁.Reaches (bit₂.next hnext₂)

source

theorem Regex.Data.BoundedIterator.Reaches.next'_iff' {startIdx maxIdx : ℕ} {bit₁ bit₂ bit₂' : BoundedIterator startIdx maxIdx} (v₂ : bit₂.Valid) (hnext₂ : bit₂.hasNext = true) (eq : bit₂.next hnext₂ = bit₂') :

bit₁.Reaches bit₂' ↔ bit₁.Reaches bit₂ ∨ bit₁.Valid ∧ bit₁ = bit₂'

source

@[simp]

theorem Regex.Data.BoundedIterator.Reaches.next'_iff {startIdx maxIdx : ℕ} {bit₁ bit₂ : BoundedIterator startIdx maxIdx} (v₂ : bit₂.Valid) (hnext₂ : bit₂.hasNext = true) :

bit₁.Reaches (bit₂.next hnext₂) ↔ bit₁.Reaches bit₂ ∨ bit₁.Valid ∧ bit₁ = bit₂.next hnext₂

source

theorem Regex.Data.BoundedIterator.Reaches.of_validFor {startIdx maxIdx : ℕ} {bit₁ bit₂ : BoundedIterator startIdx maxIdx} {l m r : List Char} (vf₁ : ValidFor l.reverse (m ++ r) bit₁) (vf₂ : ValidFor (m.reverse ++ l.reverse) r bit₂) :

bit₁.Reaches bit₂

source

theorem Regex.Data.BoundedIterator.Reaches.validFor {startIdx maxIdx : ℕ} {bit₁ bit₂ : BoundedIterator startIdx maxIdx} (h : bit₁.Reaches bit₂) :

∃ (l : List Char), ∃ (m : List Char), ∃ (r : List Char), ValidFor l.reverse (m ++ r) bit₁ ∧ ValidFor (m.reverse ++ l.reverse) r bit₂

source

theorem Regex.Data.BoundedIterator.Reaches.iff_validFor {startIdx maxIdx : ℕ} {bit₁ bit₂ : BoundedIterator startIdx maxIdx} :

bit₁.Reaches bit₂ ↔ ∃ (l : List Char), ∃ (m : List Char), ∃ (r : List Char), ValidFor l.reverse (m ++ r) bit₁ ∧ ValidFor (m.reverse ++ l.reverse) r bit₂

source

theorem Regex.Data.BoundedIterator.Reaches.iff_valid_le_pos {startIdx maxIdx : ℕ} {bit₁ bit₂ : BoundedIterator startIdx maxIdx} :

bit₁.Reaches bit₂ ↔ bit₁.Valid ∧ bit₂.Valid ∧ bit₁.toString = bit₂.toString ∧ bit₁.pos ≤ bit₂.pos

source

theorem Regex.Data.BoundedIterator.reaches_toEnd {startIdx maxIdx : ℕ} {bit : BoundedIterator startIdx maxIdx} (v : bit.Valid) :

bit.Reaches bit.toEnd

source

theorem Regex.Data.BoundedIterator.Reaches.reaches_toEnd_of_reaches {startIdx maxIdx : ℕ} {bit₁ bit₂ : BoundedIterator startIdx maxIdx} (h : bit₁.Reaches bit₂) :

bit₂.Reaches bit₁.toEnd

source

def Regex.Data.BoundedIterator.BetweenI {startIdx maxIdx : ℕ} (bit bs be : BoundedIterator startIdx maxIdx) :

Prop

Equations

bit.BetweenI bs be = (bs.Reaches bit ∧ bit.Reaches be)

Instances For

source

def Regex.Data.BoundedIterator.BetweenE {startIdx maxIdx : ℕ} (bit bs be : BoundedIterator startIdx maxIdx) :

Prop

Equations

bit.BetweenE bs be = (bit.pos < be.pos ∧ bit.BetweenI bs be)

Instances For

source

theorem Regex.Data.BoundedIterator.BetweenI.reachesSE {startIdx maxIdx : ℕ} {bit bs be : BoundedIterator startIdx maxIdx} (h : bit.BetweenI bs be) :

bs.Reaches be

source

theorem Regex.Data.BoundedIterator.BetweenI.le_pos {startIdx maxIdx : ℕ} {bit bs be : BoundedIterator startIdx maxIdx} (h : bit.BetweenI bs be) :

bit.pos ≤ be.pos

source

@[simp]

theorem Regex.Data.BoundedIterator.BetweenI.next_iff {startIdx maxIdx : ℕ} {bit bs be : BoundedIterator startIdx maxIdx} (v : be.Valid) (hnext : be.hasNext = true) :

bit.BetweenI bs (be.next hnext) ↔ bit.BetweenI bs be ∨ bs.Reaches bit ∧ bit = be.next hnext

source

theorem Regex.Data.BoundedIterator.BetweenI.iffE {startIdx maxIdx : ℕ} {bit bs be : BoundedIterator startIdx maxIdx} :

bit.BetweenI bs be ↔ bit.BetweenE bs be ∨ bs.Reaches bit ∧ bit = be

source

theorem Regex.Data.BoundedIterator.BetweenE.validE {startIdx maxIdx : ℕ} {bit bs be : BoundedIterator startIdx maxIdx} (h : bit.BetweenE bs be) :

be.Valid

source

theorem Regex.Data.BoundedIterator.BetweenE.ne_end {startIdx maxIdx : ℕ} {bit bs be : BoundedIterator startIdx maxIdx} (h : bit.BetweenE bs be) :

bit ≠ be

source

theorem Regex.Data.BoundedIterator.BetweenE.next_iffI {startIdx maxIdx : ℕ} {bit bs be : BoundedIterator startIdx maxIdx} (v : be.Valid) (hnext : be.hasNext = true) :

bit.BetweenE bs (be.next hnext) ↔ bit.BetweenI bs be

source

@[simp]

theorem Regex.Data.BoundedIterator.BetweenE.next_iff {startIdx maxIdx : ℕ} {bit bs be : BoundedIterator startIdx maxIdx} (v : be.Valid) (hnext : be.hasNext = true) :

bit.BetweenE bs (be.next hnext) ↔ bit.BetweenE bs be ∨ bs.Reaches bit ∧ bit = be

source

@[simp]

theorem Regex.Data.BoundedIterator.BetweenE.not_self {startIdx maxIdx : ℕ} {bit₁ bit₂ : BoundedIterator startIdx maxIdx} :

¬bit₁.BetweenE bit₂ bit₂