theorem String.Iterator.ext {it₁ it₂ : Iterator} (hs : it₁.s = it₂.s) (hi : it₁.i = it₂.i) : it₁ = it₂

theorem String.Iterator.ext_iff {it₁ it₂ : Iterator} : it₁ = it₂ ↔ it₁.s = it₂.s ∧ it₁.i = it₂.i

theorem String.Iterator.hasNext_of_not_atEnd {it : Iterator} (h : ¬it.atEnd = true) : it.hasNext = true

@[simp]

theorem String.Iterator.ne_next (it : Iterator) : it ≠ it.next

@[simp]

theorem String.Iterator.next_ne (it : Iterator) : it.next ≠ it

theorem String.Iterator.nextn_next_eq_next_nextn (it : Iterator) (n : ℕ) : (it.nextn n).next = it.next.nextn n

theorem String.eq_of_append_utf8Len {cs₁ cs₂ cs₃ cs₄ : List Char} (h₁ : cs₁ ++ cs₂ = cs₃ ++ cs₄) (h₂ : utf8Len cs₁ = utf8Len cs₃) : cs₁ = cs₃ ∧ cs₂ = cs₄

theorem String.eq_of_append_eq (l mr lm r : List Char) (le : utf8Len l ≤ utf8Len lm) (eq : l ++ mr = lm ++ r) : ∃ (m : List Char), mr = m ++ r ∧ lm = l ++ m

theorem String.Iterator.Valid.next' {it : Iterator} (v : it.Valid) (h : ¬it.atEnd = true) : it.next.Valid

theorem String.Iterator.Valid.validFor_of_valid_pos_le {it it' : Iterator} (v : it.Valid) (v' : it'.Valid) (eqs : it.toString = it'.toString) (le : it.pos ≤ it'.pos) : ∃ (l : List Char), ∃ (m : List Char), ∃ (r : List Char), ValidFor l.reverse (m ++ r) it ∧ ValidFor (m.reverse ++ l.reverse) r it'

theorem String.Iterator.Valid.valid_pos_le_of_validFor {it it' : Iterator} {l m r : List Char} (vf₁ : ValidFor l.reverse (m ++ r) it) (vf₂ : ValidFor (m.reverse ++ l.reverse) r it') : it.toString = it'.toString ∧ it.pos ≤ it'.pos

theorem String.Iterator.Valid.pos_le_or_ge_next {it it' : Iterator} (v : it.Valid) (v' : it'.Valid) (eqs : it.toString = it'.toString) : it.pos ≤ it'.pos ∨ it'.next.pos ≤ it.pos

theorem String.Iterator.Valid.validFor_of_hasNext {it : Iterator} (h : it.hasNext = true) (v : it.Valid) : ∃ (l : List Char), ∃ (r : List Char), ValidFor l (it.curr :: r) it

theorem String.Iterator.ValidFor.eq {it : Iterator} {l₁ r₁ l₂ r₂ : List Char} (v₁ : ValidFor l₁ r₁ it) (v₂ : ValidFor l₂ r₂ it) : l₁ = l₂ ∧ r₁ = r₂

theorem String.Iterator.ValidFor.eq_it {it₁ it₂ : Iterator} {l r : List Char} (v₁ : ValidFor l r it₁) (v₂ : ValidFor l r it₂) : it₁ = it₂

theorem String.Iterator.ValidFor.exists_cons_of_not_atEnd {l r : List Char} {it : Iterator} (v : ValidFor l r it) (h : ¬it.atEnd = true) : ∃ (r' : List Char), r = it.curr :: r'

theorem String.Iterator.ValidFor.pos_atEnd {l : List Char} {it : Iterator} (v : ValidFor l [] it) : it.pos = it.toString.endPos

theorem String.Iterator.eq_of_valid_of_next_eq {it₁ it₂ : Iterator} (v₁ : it₁.Valid) (v₂ : it₂.Valid) (h : it₁.next = it₂.next) : it₁ = it₂

theorem String.Iterator.find_toString {it : Iterator} {p : Char → Bool} : (it.find p).toString = it.toString

theorem String.Iterator.find_le_pos {it : Iterator} {p : Char → Bool} : it.pos ≤ (it.find p).pos

theorem String.Iterator.find_soundness (it it' : Iterator) (p : Char → Bool) (h : it' = it.find p) : ¬it'.atEnd = true ∧ p it'.curr = true ∨ it'.atEnd = true

theorem String.Iterator.find_valid_of_valid {it : Iterator} {p : Char → Bool} (v : it.Valid) : (it.find p).Valid

theorem String.Iterator.find_completenessAux (it it' : Iterator) {p : Char → Bool} {l r : List Char} (vf : ValidFor l r it) (h : it' = it.find p) : ∃ (m : List Char), ∃ (r' : List Char), ValidFor (m ++ l) r' it' ∧ ∀ (c : Char), c ∈ m → ¬p c = true

theorem String.Iterator.find_completeness {it : Iterator} {p : Char → Bool} (v : it.Valid) (it' : Iterator) (v' : it'.Valid) (eqs : it'.toString = it.toString) (ge : it.pos ≤ it'.pos) (lt : it'.pos < (it.find p).pos) : ¬p it'.curr = true

def String.Pos.ValidPlus (s : String) (p : Pos) : Prop

A variant of Valid that allows past-one position that represents the position after running a search at the end of the string.

Equations

• String.Pos.ValidPlus s p = (String.Pos.Valid s p ∨ p = s.endPos + { byteIdx := 1 })

theorem String.Pos.Valid.validPlus {s : String} {p : Pos} : Valid s p → ValidPlus s p

theorem String.Pos.next_endPos {s : String} : s.next s.endPos = s.endPos + { byteIdx := 1 }

theorem String.Pos.validPlus_of_next_valid {s : String} {p : Pos} (h : Valid s p) : ValidPlus s (s.next p)

theorem String.Pos.ValidPlus.valid_of_le {s : String} {p : Pos} (le : p ≤ s.endPos) (vp : ValidPlus s p) : Valid s p