theorem String.lt_antisymm {s₁ s₂ : String} (h₁ : ¬s₁ < s₂) (h₂ : ¬s₂ < s₁) : s₁ = s₂

instance String.instLawfulLTOrd : Std.LawfulLTOrd String

theorem String.mk_length (s : List Char) : (mk s).length = s.length

theorem String.Pos.Raw.offsetBy_eq {p q : Raw} : p.offsetBy q = { byteIdx := q.byteIdx + p.byteIdx }

@[inline]

def String.utf8Len : List Char → Nat

The UTF-8 byte length of a list of characters. (This is intended for specification purposes.)

Equations

• String.utf8Len [] = 0
• String.utf8Len (c :: cs) = String.utf8Len cs + c.utf8Size

theorem String.utf8ByteSize_mk (cs : List Char) : (mk cs).utf8ByteSize = utf8Len cs

@[simp]

theorem String.utf8Len_nil : utf8Len [] = 0

@[simp]

theorem String.utf8Len_cons (c : Char) (cs : List Char) : utf8Len (c :: cs) = utf8Len cs + c.utf8Size

@[simp]

theorem String.utf8Len_append (cs₁ cs₂ : List Char) : utf8Len (cs₁ ++ cs₂) = utf8Len cs₁ + utf8Len cs₂

theorem String.utf8Len_reverseAux (cs₁ cs₂ : List Char) : utf8Len (cs₁.reverseAux cs₂) = utf8Len cs₁ + utf8Len cs₂

@[simp]

theorem String.utf8Len_reverse (cs : List Char) : utf8Len cs.reverse = utf8Len cs

@[simp]

theorem String.utf8Len_eq_zero {l : List Char} : utf8Len l = 0 ↔ l = []

theorem String.utf8Len_le_of_sublist {cs₁ cs₂ : List Char} : cs₁.Sublist cs₂ → utf8Len cs₁ ≤ utf8Len cs₂

theorem String.utf8Len_le_of_infix {cs₁ cs₂ : List Char} (h : cs₁ <:+: cs₂) : utf8Len cs₁ ≤ utf8Len cs₂

theorem String.utf8Len_le_of_suffix {cs₁ cs₂ : List Char} (h : cs₁ <:+ cs₂) : utf8Len cs₁ ≤ utf8Len cs₂

theorem String.utf8Len_le_of_prefix {cs₁ cs₂ : List Char} (h : cs₁ <+: cs₂) : utf8Len cs₁ ≤ utf8Len cs₂

@[simp]

theorem String.endPos_asString (cs : List Char) : cs.asString.endPos = { byteIdx := utf8Len cs }

theorem String.endPos_mk (cs : List Char) : (mk cs).endPos = { byteIdx := utf8Len cs }

@[simp]

theorem String.utf8Len_data (s : String) : utf8Len s.data = s.utf8ByteSize

theorem String.Pos.Raw.lt_addChar (p : Raw) (c : Char) : p < p + c

inductive String.Pos.Raw.Valid : String → Raw → Prop

A string position is valid if it is equal to the UTF-8 length of an initial substring of s.

• mk (cs cs' : List Char) {p : Raw} (hp : p.byteIdx = utf8Len cs) : Valid (String.mk (cs ++ cs')) p

  A string position is valid if it is equal to the UTF-8 length of an initial substring of s.

theorem String.Pos.Raw.Valid.intro {s : String} {p : Raw} (h : ∃ (cs : List Char), ∃ (cs' : List Char), cs ++ cs' = s.data ∧ p.byteIdx = utf8Len cs) : Valid s p

theorem String.Pos.Raw.Valid.exists {s : String} {p : Raw} : Valid s p → ∃ (cs : List Char), ∃ (cs' : List Char), String.mk (cs ++ cs') = s ∧ p = { byteIdx := utf8Len cs }

@[simp]

theorem String.Pos.Raw.valid_zero {s : String} : Valid s 0

@[simp]

theorem String.Pos.Raw.valid_endPos {s : String} : Valid s s.endPos

theorem String.Pos.Raw.Valid.le_endPos {s : String} {p : Raw} : Valid s p → p ≤ s.endPos

theorem String.endPos_eq_zero (s : String) : s.endPos = 0 ↔ s = ""

theorem String.isEmpty_iff (s : String) : s.isEmpty = true ↔ s = ""

def String.utf8InductionOn {motive : List Char → Pos.Raw → Sort u} (s : List Char) (i p : Pos.Raw) (nil : (i : Pos.Raw) → motive [] i) (eq : (c : Char) → (cs : List Char) → motive (c :: cs) p) (ind : (c : Char) → (cs : List Char) → (i : Pos.Raw) → i ≠ p → motive cs (i + c) → motive (c :: cs) i) : motive s i

Induction along the valid positions in a list of characters. (This definition is intended only for specification purposes.)

Equations

• String.utf8InductionOn [] i p nil eq ind = nil i
• String.utf8InductionOn (c :: cs) i p nil eq ind = if h : i = p then ⋯ ▸ eq c cs else ind c cs i h (String.utf8InductionOn cs (i + c) p nil eq ind)

theorem String.utf8GetAux_add_right_cancel (s : List Char) (i p n : Nat) : Pos.Raw.utf8GetAux s { byteIdx := i + n } { byteIdx := p + n } = Pos.Raw.utf8GetAux s { byteIdx := i } { byteIdx := p }

theorem String.utf8GetAux_addChar_right_cancel (s : List Char) (i p : Pos.Raw) (c : Char) : Pos.Raw.utf8GetAux s (i + c) (p + c) = Pos.Raw.utf8GetAux s i p

theorem String.utf8GetAux_of_valid (cs cs' : List Char) {i p : Nat} (hp : i + utf8Len cs = p) : Pos.Raw.utf8GetAux (cs ++ cs') { byteIdx := i } { byteIdx := p } = cs'.headD default

theorem String.get_of_valid (cs cs' : List Char) : Pos.Raw.get (mk (cs ++ cs')) { byteIdx := utf8Len cs } = cs'.headD default

theorem String.get_cons_addChar (c : Char) (cs : List Char) (i : Pos.Raw) : Pos.Raw.get (c :: cs).asString (i + c) = Pos.Raw.get cs.asString i

theorem String.utf8GetAux?_of_valid (cs cs' : List Char) {i p : Nat} (hp : i + utf8Len cs = p) : Pos.Raw.utf8GetAux? (cs ++ cs') { byteIdx := i } { byteIdx := p } = cs'.head?

theorem String.get?_of_valid (cs cs' : List Char) : Pos.Raw.get? (cs ++ cs').asString { byteIdx := utf8Len cs } = cs'.head?

theorem String.utf8SetAux_of_valid (c' : Char) (cs cs' : List Char) {i p : Nat} (hp : i + utf8Len cs = p) : Pos.Raw.utf8SetAux c' (cs ++ cs') { byteIdx := i } { byteIdx := p } = cs ++ List.modifyHead (fun (x : Char) => c') cs'

theorem String.set_of_valid (cs cs' : List Char) (c' : Char) : Pos.Raw.set (mk (cs ++ cs')) { byteIdx := utf8Len cs } c' = (cs ++ List.modifyHead (fun (x : Char) => c') cs').asString

theorem String.modify_of_valid {f : Char → Char} (cs cs' : List Char) : Pos.Raw.modify (mk (cs ++ cs')) { byteIdx := utf8Len cs } f = (cs ++ List.modifyHead f cs').asString

theorem String.next_of_valid' (cs cs' : List Char) : Pos.Raw.next (mk (cs ++ cs')) { byteIdx := utf8Len cs } = { byteIdx := utf8Len cs + (cs'.headD default).utf8Size }

theorem String.next_of_valid (cs : List Char) (c : Char) (cs' : List Char) : Pos.Raw.next (mk (cs ++ c :: cs')) { byteIdx := utf8Len cs } = { byteIdx := utf8Len cs + c.utf8Size }

@[simp]

theorem String.atEnd_iff (s : String) (p : Pos.Raw) : Pos.Raw.atEnd s p = true ↔ s.endPos ≤ p

theorem String.valid_next {s : String} {p : Pos.Raw} (h : Pos.Raw.Valid s p) (h₂ : p < s.endPos) : Pos.Raw.Valid s (Pos.Raw.next s p)

theorem String.utf8PrevAux_of_valid {cs cs' : List Char} {c : Char} {i p : Nat} (hp : i + (utf8Len cs + c.utf8Size) = p) : Pos.Raw.utf8PrevAux (cs ++ c :: cs') { byteIdx := i } { byteIdx := p } = { byteIdx := i + utf8Len cs }

theorem String.prev_of_valid (cs : List Char) (c : Char) (cs' : List Char) : Pos.Raw.prev (mk (cs ++ c :: cs')) { byteIdx := utf8Len cs + c.utf8Size } = { byteIdx := utf8Len cs }

theorem String.prev_of_valid' (cs cs' : List Char) : Pos.Raw.prev (mk (cs ++ cs')) { byteIdx := utf8Len cs } = { byteIdx := utf8Len cs.dropLast }

theorem String.front_eq (s : String) : s.front = s.data.headD default

theorem String.back_eq (s : String) : s.back = s.data.getLastD default

theorem String.atEnd_of_valid (cs cs' : List Char) : Pos.Raw.atEnd (mk (cs ++ cs')) { byteIdx := utf8Len cs } = true ↔ cs' = []

theorem String.posOfAux_eq (s : String) (c : Char) : s.posOfAux c = s.findAux fun (x : Char) => x == c

theorem String.posOf_eq (s : String) (c : Char) : s.posOf c = s.find fun (x : Char) => x == c

theorem String.revPosOfAux_eq (s : String) (c : Char) : s.revPosOfAux c = s.revFindAux fun (x : Char) => x == c

theorem String.revPosOf_eq (s : String) (c : Char) : s.revPosOf c = s.revFind fun (x : Char) => x == c

theorem String.findAux_of_valid (p : Char → Bool) (l m r : List Char) : (mk (l ++ m ++ r)).findAux p { byteIdx := utf8Len l + utf8Len m } { byteIdx := utf8Len l } = { byteIdx := utf8Len l + utf8Len (List.takeWhile (fun (x : Char) => !p x) m) }

theorem String.find_of_valid (p : Char → Bool) (s : String) : s.find p = { byteIdx := utf8Len (List.takeWhile (fun (x : Char) => !p x) s.data) }

theorem String.revFindAux_of_valid (p : Char → Bool) (l r : List Char) : (mk (l.reverse ++ r)).revFindAux p { byteIdx := utf8Len l } = Option.map (fun (x : List Char) => { byteIdx := utf8Len x }) (List.dropWhile (fun (x : Char) => !p x) l).tail?

theorem String.revFind_of_valid (p : Char → Bool) (s : String) : s.revFind p = Option.map (fun (x : List Char) => { byteIdx := utf8Len x }) (List.dropWhile (fun (x : Char) => !p x) s.data.reverse).tail?

@[irreducible]

theorem String.firstDiffPos_loop_eq (l₁ l₂ r₁ r₂ : List Char) (stop p : Nat) (hl₁ : p = utf8Len l₁) (hl₂ : p = utf8Len l₂) (hstop : stop = min (utf8Len l₁ + utf8Len r₁) (utf8Len l₂ + utf8Len r₂)) : firstDiffPos.loop (mk (l₁ ++ r₁)) (mk (l₂ ++ r₂)) { byteIdx := stop } { byteIdx := p } = { byteIdx := p + utf8Len (List.takeWhile₂ (fun (x1 x2 : Char) => decide (x1 = x2)) r₁ r₂).fst }

theorem String.firstDiffPos_eq (a b : String) : a.firstDiffPos b = { byteIdx := utf8Len (List.takeWhile₂ (fun (x1 x2 : Char) => decide (x1 = x2)) a.data b.data).fst }

theorem String.Pos.Raw.extract.go₂_add_right_cancel (s : List Char) (i e n : Nat) : go₂ s { byteIdx := i + n } { byteIdx := e + n } = go₂ s { byteIdx := i } { byteIdx := e }

theorem String.Pos.Raw.extract.go₂_append_left (s t : List Char) (i e : Nat) : e = utf8Len s + i → go₂ (s ++ t) { byteIdx := i } { byteIdx := e } = s

theorem String.Pos.Raw.extract.go₁_add_right_cancel (s : List Char) (i b e n : Nat) : go₁ s { byteIdx := i + n } { byteIdx := b + n } { byteIdx := e + n } = go₁ s { byteIdx := i } { byteIdx := b } { byteIdx := e }

theorem String.Pos.Raw.extract.go₁_cons_addChar (c : Char) (cs : List Char) (b e : Raw) : go₁ (c :: cs) 0 (b + c) (e + c) = go₁ cs 0 b e

theorem String.Pos.Raw.extract.go₁_append_right (s t : List Char) (i b : Nat) (e : Raw) : b = utf8Len s + i → go₁ (s ++ t) { byteIdx := i } { byteIdx := b } e = go₂ t { byteIdx := b } e

theorem String.Pos.Raw.extract.go₁_zero_utf8Len (s : List Char) : go₁ s 0 0 { byteIdx := utf8Len s } = s

theorem String.extract_cons_addChar (c : Char) (cs : List Char) (b e : Pos.Raw) : Pos.Raw.extract (mk (c :: cs)) (b + c) (e + c) = Pos.Raw.extract (mk cs) b e

theorem String.extract_zero_endPos (s : String) : Pos.Raw.extract s 0 s.endPos = s

theorem String.extract_of_valid (l m r : List Char) : Pos.Raw.extract (mk (l ++ m ++ r)) { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } = mk m

@[irreducible]

theorem String.splitAux_of_valid (p : Char → Bool) (l m r : List Char) (acc : List String) : (mk (l ++ m ++ r)).splitAux p { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } acc = acc.reverse ++ List.map mk (List.splitOnP.go p r m.reverse)

theorem String.splitToList_of_valid (s : String) (p : Char → Bool) : s.splitToList p = List.map mk (List.splitOnP p s.data)

@[deprecated String.splitToList_of_valid (since := "2025-10-18")]

theorem String.split_of_valid (s : String) (p : Char → Bool) : s.splitToList p = List.map mk (List.splitOnP p s.data)

@[simp]

theorem String.toString_toSubstring (s : String) : s.toSubstring.toString = s

theorem String.join_eq (ss : List String) : join ss = mk (List.map data ss).flatten

@[simp]

theorem String.data_join (ss : List String) : (join ss).data = (List.map data ss).flatten

@[simp]

theorem String.Iterator.forward_eq_nextn : forward = nextn

theorem String.Iterator.hasNext_cons_addChar (c : Char) (cs : List Char) (i : Pos.Raw) : { s := String.mk (c :: cs), i := i + c }.hasNext = { s := String.mk cs, i := i }.hasNext

def String.Iterator.Valid (it : Iterator) : Prop

Validity for a string iterator.

Equations

• it.Valid = String.Pos.Raw.Valid it.s it.pos

inductive String.Iterator.ValidFor (l r : List Char) : Iterator → Prop

it.ValidFor l r means that it is a string iterator whose underlying string is l.reverse ++ r, and where the cursor is pointing at the end of l.reverse.

• mk {l r : List Char} : ValidFor l r { s := String.mk (l.reverseAux r), i := { byteIdx := utf8Len l } }

  The canonical constructor for ValidFor.

theorem String.Iterator.ValidFor.valid {l r : List Char} {it : Iterator} : ValidFor l r it → it.Valid

theorem String.Iterator.ValidFor.out {l r : List Char} {it : Iterator} : ValidFor l r it → it = { s := String.mk (l.reverseAux r), i := { byteIdx := utf8Len l } }

theorem String.Iterator.ValidFor.out' {l r : List Char} {it : Iterator} : ValidFor l r it → it = { s := String.mk (l.reverse ++ r), i := { byteIdx := utf8Len l.reverse } }

theorem String.Iterator.ValidFor.mk' {l r : List Char} : ValidFor l r { s := String.mk (l.reverse ++ r), i := { byteIdx := utf8Len l.reverse } }

theorem String.Iterator.ValidFor.of_eq {l r : List Char} (it : Iterator) : it.s.data = l.reverseAux r → it.i.byteIdx = utf8Len l → ValidFor l r it

theorem String.validFor_mkIterator (s : String) : Iterator.ValidFor [] s.data s.mkIterator

theorem String.Iterator.ValidFor.remainingBytes {l r : List Char} {it : Iterator} : ValidFor l r it → it.remainingBytes = utf8Len r

theorem String.Iterator.ValidFor.toString {l r : List Char} {it : Iterator} : ValidFor l r it → it.s = String.mk (l.reverseAux r)

theorem String.Iterator.ValidFor.pos {l r : List Char} {it : Iterator} : ValidFor l r it → it.i = { byteIdx := utf8Len l }

theorem String.Iterator.ValidFor.pos_eq_zero {l r : List Char} {it : Iterator} (h : ValidFor l r it) : it.i = 0 ↔ l = []

theorem String.Iterator.ValidFor.pos_eq_endPos {l r : List Char} {it : Iterator} (h : ValidFor l r it) : it.i = it.s.endPos ↔ r = []

theorem String.Iterator.ValidFor.curr {l r : List Char} {it : Iterator} : ValidFor l r it → it.curr = r.headD default

theorem String.Iterator.ValidFor.next {l : List Char} {c : Char} {r : List Char} {it : Iterator} : ValidFor l (c :: r) it → ValidFor (c :: l) r it.next

theorem String.Iterator.ValidFor.prev {c : Char} {l r : List Char} {it : Iterator} : ValidFor (c :: l) r it → ValidFor l (c :: r) it.prev

theorem String.Iterator.ValidFor.prev_nil {r : List Char} {it : Iterator} : ValidFor [] r it → ValidFor [] r it.prev

theorem String.Iterator.ValidFor.atEnd {l r : List Char} {it : Iterator} : ValidFor l r it → (it.atEnd = true ↔ r = [])

theorem String.Iterator.ValidFor.hasNext {l r : List Char} {it : Iterator} : ValidFor l r it → (it.hasNext = true ↔ r ≠ [])

theorem String.Iterator.ValidFor.hasPrev {l r : List Char} {it : Iterator} : ValidFor l r it → (it.hasPrev = true ↔ l ≠ [])

theorem String.Iterator.ValidFor.setCurr' {l r : List Char} {c : Char} {it : Iterator} : ValidFor l r it → ValidFor l (List.modifyHead (fun (x : Char) => c) r) (it.setCurr c)

theorem String.Iterator.ValidFor.setCurr {l : List Char} {c : Char} {r : List Char} {it : Iterator} (h : ValidFor l (c :: r) it) : ValidFor l (c :: r) (it.setCurr c)

theorem String.Iterator.ValidFor.toEnd {l r : List Char} {it : Iterator} (h : ValidFor l r it) : ValidFor (r.reverse ++ l) [] it.toEnd

theorem String.Iterator.ValidFor.toEnd' (it : Iterator) : ValidFor it.s.data.reverse [] it.toEnd

theorem String.Iterator.ValidFor.extract {l m r : List Char} {it₁ it₂ : Iterator} (h₁ : ValidFor l (m ++ r) it₁) (h₂ : ValidFor (m.reverse ++ l) r it₂) : it₁.extract it₂ = String.mk m

theorem String.Iterator.ValidFor.remainingToString {l r : List Char} {it : Iterator} (h : ValidFor l r it) : it.remainingToString = String.mk r

theorem String.Iterator.ValidFor.nextn {l r : List Char} {it : Iterator} : ValidFor l r it → ∀ (n : Nat), n ≤ r.length → ValidFor ((List.take n r).reverse ++ l) (List.drop n r) (it.nextn n)

theorem String.Iterator.ValidFor.prevn {l r : List Char} {it : Iterator} : ValidFor l r it → ∀ (n : Nat), n ≤ l.length → ValidFor (List.drop n l) ((List.take n l).reverse ++ r) (it.prevn n)

theorem String.Iterator.Valid.validFor {it : Iterator} : it.Valid → ∃ (l : List Char), ∃ (r : List Char), ValidFor l r it

theorem String.valid_mkIterator (s : String) : s.mkIterator.Valid

theorem String.Iterator.Valid.remainingBytes_le {it : Iterator} : it.Valid → it.remainingBytes ≤ it.s.utf8ByteSize

theorem String.Iterator.Valid.next {it : Iterator} : it.Valid → it.hasNext = true → it.next.Valid

theorem String.Iterator.Valid.prev {it : Iterator} : it.Valid → it.prev.Valid

theorem String.Iterator.Valid.setCurr {c : Char} {it : Iterator} : it.Valid → (it.setCurr c).Valid

theorem String.Iterator.Valid.toEnd (it : Iterator) : it.toEnd.Valid

theorem String.Iterator.Valid.remainingToString {l r : List Char} {it : Iterator} (h : ValidFor l r it) : it.remainingToString = String.mk r

theorem String.Iterator.Valid.prevn {it : Iterator} (h : it.Valid) (n : Nat) : (it.prevn n).Valid

theorem String.offsetOfPosAux_of_valid (l m r : List Char) (n : Nat) : (mk (l ++ m ++ r)).offsetOfPosAux { byteIdx := utf8Len l + utf8Len m } { byteIdx := utf8Len l } n = n + m.length

theorem String.offsetOfPos_of_valid (l r : List Char) : (mk (l ++ r)).offsetOfPos { byteIdx := utf8Len l } = l.length

theorem String.foldlAux_of_valid {α : Type u_1} (f : α → Char → α) (l m r : List Char) (a : α) : foldlAux f (mk (l ++ m ++ r)) { byteIdx := utf8Len l + utf8Len m } { byteIdx := utf8Len l } a = List.foldl f a m

theorem String.foldl_eq {α : Type u_1} (f : α → Char → α) (s : String) (a : α) : foldl f a s = List.foldl f a s.data

theorem String.foldrAux_of_valid {α : Type u_1} (f : Char → α → α) (l m r : List Char) (a : α) : foldrAux f a (mk (l ++ m ++ r)) { byteIdx := utf8Len l + utf8Len m } { byteIdx := utf8Len l } = List.foldr f a m

theorem String.foldr_eq {α : Type u_1} (f : Char → α → α) (s : String) (a : α) : foldr f a s = List.foldr f a s.data

theorem String.anyAux_of_valid (p : Char → Bool) (l m r : List Char) : (mk (l ++ m ++ r)).anyAux { byteIdx := utf8Len l + utf8Len m } p { byteIdx := utf8Len l } = m.any p

theorem String.any_eq (s : String) (p : Char → Bool) : s.any p = s.data.any p

theorem String.any_iff (s : String) (p : Char → Bool) : s.any p = true ↔ ∃ (c : Char), c ∈ s.data ∧ p c = true

theorem String.all_eq (s : String) (p : Char → Bool) : s.all p = s.data.all p

theorem String.all_iff (s : String) (p : Char → Bool) : s.all p = true ↔ ∀ (c : Char), c ∈ s.data → p c = true

theorem String.contains_iff (s : String) (c : Char) : s.contains c = true ↔ c ∈ s.data

theorem String.mapAux_of_valid (f : Char → Char) (l r : List Char) : mapAux f { byteIdx := utf8Len l } (mk (l ++ r)) = mk (l ++ List.map f r)

theorem String.map_eq (f : Char → Char) (s : String) : map f s = mk (List.map f s.data)

theorem String.takeWhileAux_of_valid (p : Char → Bool) (l m r : List Char) : Substring.takeWhileAux (mk (l ++ m ++ r)) { byteIdx := utf8Len l + utf8Len m } p { byteIdx := utf8Len l } = { byteIdx := utf8Len l + utf8Len (List.takeWhile p m) }

@[simp]

theorem String.map_eq_empty_iff (s : String) (f : Char → Char) : map f s = "" ↔ s = ""

@[simp]

theorem String.map_isEmpty_eq_isEmpty (s : String) (f : Char → Char) : (map f s).isEmpty = s.isEmpty

@[simp]

theorem String.length_map (s : String) (f : Char → Char) : (map f s).length = s.length

theorem String.length_eq_of_map_eq {a b : String} {f g : Char → Char} : map f a = map g b → a.length = b.length

structure Substring.Valid (s : Substring) : Prop

Validity for a substring.

• startValid : String.Pos.Raw.Valid s.str s.startPos

  The start position of a valid substring is valid.

• stopValid : String.Pos.Raw.Valid s.str s.stopPos

  The stop position of a valid substring is valid.

• le : s.startPos ≤ s.stopPos

  The stop position of a substring is at least the start.

theorem Substring.Valid_default : default.Valid

inductive Substring.ValidFor (l m r : List Char) : Substring → Prop

A substring is represented by three lists l m r, where m is the middle section (the actual substring) and l ++ m ++ r is the underlying string.

• mk {l m r : List Char} : ValidFor l m r { str := String.mk (l ++ m ++ r), startPos := { byteIdx := String.utf8Len l }, stopPos := { byteIdx := String.utf8Len l + String.utf8Len m } }

  The constructor for ValidFor.

theorem Substring.ValidFor.valid {l m r : List Char} {s : Substring} : ValidFor l m r s → s.Valid

theorem Substring.ValidFor.of_eq {l m r : List Char} (s : Substring) : s.str.data = l ++ m ++ r → s.startPos.byteIdx = String.utf8Len l → s.stopPos.byteIdx = String.utf8Len l + String.utf8Len m → ValidFor l m r s

theorem String.validFor_toSubstring (s : String) : Substring.ValidFor [] s.data [] s.toSubstring

theorem Substring.ValidFor.str {l m r : List Char} {s : Substring} : ValidFor l m r s → s.str = String.mk (l ++ m ++ r)

theorem Substring.ValidFor.startPos {l m r : List Char} {s : Substring} : ValidFor l m r s → s.startPos = { byteIdx := String.utf8Len l }

theorem Substring.ValidFor.stopPos {l m r : List Char} {s : Substring} : ValidFor l m r s → s.stopPos = { byteIdx := String.utf8Len l + String.utf8Len m }

theorem Substring.ValidFor.bsize {l m r : List Char} {s : Substring} : ValidFor l m r s → s.bsize = String.utf8Len m

theorem Substring.ValidFor.isEmpty {l m r : List Char} {s : Substring} : ValidFor l m r s → (s.isEmpty = true ↔ m = [])

theorem Substring.ValidFor.toString {l m r : List Char} {s : Substring} : ValidFor l m r s → s.toString = String.mk m

theorem Substring.ValidFor.toIterator {l m r : List Char} {s : Substring} : ValidFor l m r s → String.Iterator.ValidFor l.reverse (m ++ r) s.toIterator

theorem Substring.ValidFor.get {l m₁ : List Char} {c : Char} {m₂ r : List Char} {s : Substring} : ValidFor l (m₁ ++ c :: m₂) r s → s.get { byteIdx := String.utf8Len m₁ } = c

theorem Substring.ValidFor.next {l m₁ : List Char} {c : Char} {m₂ r : List Char} {s : Substring} : ValidFor l (m₁ ++ c :: m₂) r s → s.next { byteIdx := String.utf8Len m₁ } = { byteIdx := String.utf8Len m₁ + c.utf8Size }

theorem Substring.ValidFor.next_stop {l m r : List Char} {s : Substring} : ValidFor l m r s → s.next { byteIdx := String.utf8Len m } = { byteIdx := String.utf8Len m }

theorem Substring.ValidFor.prev {l m₁ : List Char} {c : Char} {m₂ r : List Char} {s : Substring} : ValidFor l (m₁ ++ c :: m₂) r s → s.prev { byteIdx := String.utf8Len m₁ + c.utf8Size } = { byteIdx := String.utf8Len m₁ }

theorem Substring.ValidFor.nextn_stop {l m r : List Char} {s : Substring} : ValidFor l m r s → ∀ (n : Nat), s.nextn n { byteIdx := String.utf8Len m } = { byteIdx := String.utf8Len m }

theorem Substring.ValidFor.nextn {l m₁ m₂ r : List Char} {s : Substring} : ValidFor l (m₁ ++ m₂) r s → ∀ (n : Nat), s.nextn n { byteIdx := String.utf8Len m₁ } = { byteIdx := String.utf8Len m₁ + String.utf8Len (List.take n m₂) }

theorem Substring.ValidFor.prevn {l m₂ r m₁ : List Char} {s : Substring} : ValidFor l (m₁.reverse ++ m₂) r s → ∀ (n : Nat), s.prevn n { byteIdx := String.utf8Len m₁ } = { byteIdx := String.utf8Len (List.drop n m₁) }

theorem Substring.ValidFor.front {l : List Char} {c : Char} {m r : List Char} {s : Substring} : ValidFor l (c :: m) r s → s.front = c

theorem Substring.ValidFor.drop {l m r : List Char} {s : Substring} : ValidFor l m r s → ∀ (n : Nat), ValidFor (l ++ List.take n m) (List.drop n m) r (s.drop n)

theorem Substring.ValidFor.take {l m r : List Char} {s : Substring} : ValidFor l m r s → ∀ (n : Nat), ValidFor l (List.take n m) (List.drop n m ++ r) (s.take n)

theorem Substring.ValidFor.atEnd {l m r : List Char} {p : Nat} {s : Substring} : ValidFor l m r s → (s.atEnd { byteIdx := p } = true ↔ p = String.utf8Len m)

theorem Substring.ValidFor.extract' {l ml mm mr r : List Char} {b e : String.Pos.Raw} {s : Substring} : ValidFor l (ml ++ mm ++ mr) r s → ValidFor ml mm mr { str := String.mk (ml ++ mm ++ mr), startPos := b, stopPos := e } → ∃ (l' : List Char), ∃ (r' : List Char), ValidFor l' mm r' (s.extract b e)

theorem Substring.ValidFor.extract {l m r ml mm mr : List Char} {b e : String.Pos.Raw} {s : Substring} : ValidFor l m r s → ValidFor ml mm mr { str := String.mk m, startPos := b, stopPos := e } → ∃ (l' : List Char), ∃ (r' : List Char), ValidFor l' mm r' (s.extract b e)

theorem Substring.ValidFor.foldl {α : Type u_1} {l m r : List Char} (f : α → Char → α) (init : α) {s : Substring} : ValidFor l m r s → Substring.foldl f init s = List.foldl f init m

theorem Substring.ValidFor.foldr {α : Type u_1} {l m r : List Char} (f : Char → α → α) (init : α) {s : Substring} : ValidFor l m r s → Substring.foldr f init s = List.foldr f init m

theorem Substring.ValidFor.any {l m r : List Char} (f : Char → Bool) {s : Substring} : ValidFor l m r s → s.any f = m.any f

theorem Substring.ValidFor.all {l m r : List Char} (f : Char → Bool) {s : Substring} : ValidFor l m r s → s.all f = m.all f

theorem Substring.ValidFor.contains {l m r : List Char} (c : Char) {s : Substring} : ValidFor l m r s → (s.contains c = true ↔ c ∈ m)

theorem Substring.ValidFor.takeWhile {l m r : List Char} (p : Char → Bool) {s : Substring} : ValidFor l m r s → ValidFor l (List.takeWhile p m) (List.dropWhile p m ++ r) (s.takeWhile p)

theorem Substring.ValidFor.dropWhile {l m r : List Char} (p : Char → Bool) {s : Substring} : ValidFor l m r s → ValidFor (l ++ List.takeWhile p m) (List.dropWhile p m) r (s.dropWhile p)

theorem Substring.Valid.validFor {s : Substring} : s.Valid → ∃ (l : List Char), ∃ (m : List Char), ∃ (r : List Char), ValidFor l m r s

theorem Substring.Valid.valid {l m r : List Char} {s : Substring} : ValidFor l m r s → s.Valid

theorem String.valid_toSubstring (s : String) : s.toSubstring.Valid

theorem Substring.Valid.bsize {s : Substring} : s.Valid → s.bsize = String.utf8Len s.toString.data

theorem Substring.Valid.isEmpty {s : Substring} : s.Valid → (s.isEmpty = true ↔ s.toString = "")

theorem Substring.Valid.get {m₁ : List Char} {c : Char} {m₂ : List Char} {s : Substring} : s.Valid → s.toString.data = m₁ ++ c :: m₂ → s.get { byteIdx := String.utf8Len m₁ } = c

theorem Substring.Valid.next {m₁ : List Char} {c : Char} {m₂ : List Char} {s : Substring} : s.Valid → s.toString.data = m₁ ++ c :: m₂ → s.next { byteIdx := String.utf8Len m₁ } = { byteIdx := String.utf8Len m₁ + c.utf8Size }

theorem Substring.Valid.next_stop {s : Substring} : s.Valid → s.next { byteIdx := s.bsize } = { byteIdx := s.bsize }

theorem Substring.Valid.prev {m₁ : List Char} {c : Char} {m₂ : List Char} {s : Substring} : s.Valid → s.toString.data = m₁ ++ c :: m₂ → s.prev { byteIdx := String.utf8Len m₁ + c.utf8Size } = { byteIdx := String.utf8Len m₁ }

theorem Substring.Valid.nextn_stop {s : Substring} : s.Valid → ∀ (n : Nat), s.nextn n { byteIdx := s.bsize } = { byteIdx := s.bsize }

theorem Substring.Valid.nextn {m₁ m₂ : List Char} {s : Substring} : s.Valid → s.toString.data = m₁ ++ m₂ → ∀ (n : Nat), s.nextn n { byteIdx := String.utf8Len m₁ } = { byteIdx := String.utf8Len m₁ + String.utf8Len (List.take n m₂) }

theorem Substring.Valid.prevn {m₂ m₁ : List Char} {s : Substring} : s.Valid → s.toString.data = m₁.reverse ++ m₂ → ∀ (n : Nat), s.prevn n { byteIdx := String.utf8Len m₁ } = { byteIdx := String.utf8Len (List.drop n m₁) }

theorem Substring.Valid.front {c : Char} {m : List Char} {s : Substring} : s.Valid → s.toString.data = c :: m → s.front = c

theorem Substring.Valid.drop {s : Substring} : s.Valid → ∀ (n : Nat), (s.drop n).Valid

theorem Substring.Valid.data_drop {s : Substring} : s.Valid → ∀ (n : Nat), (s.drop n).toString.data = List.drop n s.toString.data

theorem Substring.Valid.take {s : Substring} : s.Valid → ∀ (n : Nat), (s.take n).Valid

theorem Substring.Valid.data_take {s : Substring} : s.Valid → ∀ (n : Nat), (s.take n).toString.data = List.take n s.toString.data

theorem Substring.Valid.atEnd {p : Nat} {s : Substring} : s.Valid → (s.atEnd { byteIdx := p } = true ↔ p = s.toString.utf8ByteSize)

theorem Substring.Valid.extract {b e : String.Pos.Raw} {s : Substring} : s.Valid → { str := s.toString, startPos := b, stopPos := e }.Valid → (s.extract b e).Valid

theorem Substring.Valid.toString_extract {b e : String.Pos.Raw} {s : Substring} : s.Valid → { str := s.toString, startPos := b, stopPos := e }.Valid → (s.extract b e).toString = String.Pos.Raw.extract s.toString b e

theorem Substring.Valid.foldl {α : Type u_1} (f : α → Char → α) (init : α) {s : Substring} : s.Valid → Substring.foldl f init s = List.foldl f init s.toString.data

theorem Substring.Valid.foldr {α : Type u_1} (f : Char → α → α) (init : α) {s : Substring} : s.Valid → Substring.foldr f init s = List.foldr f init s.toString.data

theorem Substring.Valid.any (f : Char → Bool) {s : Substring} : s.Valid → s.any f = s.toString.data.any f

theorem Substring.Valid.all (f : Char → Bool) {s : Substring} : s.Valid → s.all f = s.toString.data.all f

theorem Substring.Valid.contains (c : Char) {s : Substring} : s.Valid → (s.contains c = true ↔ c ∈ s.toString.data)

theorem Substring.Valid.takeWhile (p : Char → Bool) {s : Substring} : s.Valid → (s.takeWhile p).Valid

theorem Substring.Valid.data_takeWhile (p : Char → Bool) {s : Substring} : s.Valid → (s.takeWhile p).toString.data = List.takeWhile p s.toString.data

theorem Substring.Valid.dropWhile (p : Char → Bool) {s : Substring} : s.Valid → (s.dropWhile p).Valid

theorem Substring.Valid.data_dropWhile (p : Char → Bool) {s : Substring} : s.Valid → (s.dropWhile p).toString.data = List.dropWhile p s.toString.data

theorem String.drop_eq (s : String) (n : Nat) : s.drop n = mk (List.drop n s.data)

@[simp]

theorem String.data_drop (s : String) (n : Nat) : (s.drop n).data = List.drop n s.data

@[simp]

theorem String.drop_empty {n : Nat} : "".drop n = ""

theorem String.take_eq (s : String) (n : Nat) : s.take n = mk (List.take n s.data)

@[simp]

theorem String.data_take (s : String) (n : Nat) : (s.take n).data = List.take n s.data

theorem String.takeWhile_eq (p : Char → Bool) (s : String) : s.takeWhile p = mk (List.takeWhile p s.data)

@[simp]

theorem String.data_takeWhile (p : Char → Bool) (s : String) : (s.takeWhile p).data = List.takeWhile p s.data

theorem String.dropWhile_eq (p : Char → Bool) (s : String) : s.dropWhile p = mk (List.dropWhile p s.data)

@[simp]

theorem String.data_dropWhile (p : Char → Bool) (s : String) : (s.dropWhile p).data = List.dropWhile p s.data