@[simp]

theorem Char.length_toString (c : Char) : String.length (Char.toString c) = 1

theorem String.ext {s₁ : String} {s₂ : String} (h : s₁.data = s₂.data) : s₁ = s₂

theorem String.ext_iff {s₁ : String} {s₂ : String} : s₁ = s₂ ↔ s₁.data = s₂.data

@[simp]

theorem String.default_eq : default = ""

@[simp]

theorem String.str_eq : String.str = String.push

@[simp]

theorem String.mk_length (s : List Char) : String.length { data := s } = List.length s

@[simp]

theorem String.length_empty : String.length "" = 0

@[simp]

theorem String.length_singleton (c : Char) : String.length (String.singleton c) = 1

@[simp]

theorem String.length_push {s : String} (c : Char) : String.length (String.push s c) = String.length s + 1

@[simp]

theorem String.length_pushn {s : String} (c : Char) (n : Nat) : String.length (String.pushn s c n) = String.length s + n

@[simp]

theorem String.length_append (s : String) (t : String) : String.length (s ++ t) = String.length s + String.length t

@[simp]

theorem String.data_push (s : String) (c : Char) : (String.push s c).data = s.data ++ [c]

@[simp]

theorem String.data_append (s : String) (t : String) : (s ++ t).data = s.data ++ t.data

theorem String.lt_iff (s : String) (t : String) : s < t ↔ s.data < t.data

@[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 = String.utf8ByteSize.go

@[simp]

theorem String.utf8ByteSize.go_eq : String.utf8ByteSize.go = String.utf8Len

@[simp]

theorem String.utf8ByteSize_mk (cs : List Char) : String.utf8ByteSize { data := cs } = String.utf8Len cs

@[simp]

theorem String.utf8Len_nil : String.utf8Len [] = 0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

theorem String.endPos_eq (cs : List Char) : String.endPos { data := cs } = { byteIdx := String.utf8Len cs }

@[simp]

theorem String.Pos.byteIdx_zero : 0.byteIdx = 0

theorem String.Pos.byteIdx_mk (n : Nat) : { byteIdx := n }.byteIdx = n

@[simp]

theorem String.Pos.mk_zero : { byteIdx := 0 } = 0

@[simp]

theorem String.Pos.mk_byteIdx (p : String.Pos) : { byteIdx := p.byteIdx } = p

theorem String.Pos.ext {i₁ : String.Pos} {i₂ : String.Pos} (h : i₁.byteIdx = i₂.byteIdx) : i₁ = i₂

theorem String.Pos.ext_iff {i₁ : String.Pos} {i₂ : String.Pos} : i₁ = i₂ ↔ i₁.byteIdx = i₂.byteIdx

@[simp]

theorem String.Pos.add_byteIdx (p₁ : String.Pos) (p₂ : String.Pos) : (p₁ + p₂).byteIdx = p₁.byteIdx + p₂.byteIdx

theorem String.Pos.add_eq (p₁ : String.Pos) (p₂ : String.Pos) : p₁ + p₂ = { byteIdx := p₁.byteIdx + p₂.byteIdx }

@[simp]

theorem String.Pos.sub_byteIdx (p₁ : String.Pos) (p₂ : String.Pos) : (p₁ - p₂).byteIdx = p₁.byteIdx - p₂.byteIdx

theorem String.Pos.sub_eq (p₁ : String.Pos) (p₂ : String.Pos) : p₁ - p₂ = { byteIdx := p₁.byteIdx - p₂.byteIdx }

@[simp]

theorem String.Pos.addChar_byteIdx (p : String.Pos) (c : Char) : (p + c).byteIdx = p.byteIdx + String.csize c

theorem String.Pos.addChar_eq (p : String.Pos) (c : Char) : p + c = { byteIdx := p.byteIdx + String.csize c }

theorem String.Pos.zero_addChar_byteIdx (c : Char) : (0 + c).byteIdx = String.csize c

theorem String.Pos.zero_addChar_eq (c : Char) : 0 + c = { byteIdx := String.csize c }

theorem String.Pos.addChar_right_comm (p : String.Pos) (c₁ : Char) (c₂ : Char) : p + c₁ + c₂ = p + c₂ + c₁

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

theorem String.Pos.ne_of_lt {i₁ : String.Pos} {i₂ : String.Pos} (h : i₁ < i₂) : i₁ ≠ i₂

theorem String.Pos.ne_of_gt {i₁ : String.Pos} {i₂ : String.Pos} (h : i₁ < i₂) : i₂ ≠ i₁

@[simp]

theorem String.Pos.addString_byteIdx (p : String.Pos) (s : String) : (p + s).byteIdx = p.byteIdx + String.utf8ByteSize s

theorem String.Pos.addString_eq (p : String.Pos) (s : String) : p + s = { byteIdx := p.byteIdx + String.utf8ByteSize s }

theorem String.Pos.zero_addString_byteIdx (s : String) : (0 + s).byteIdx = String.utf8ByteSize s

theorem String.Pos.zero_addString_eq (s : String) : 0 + s = { byteIdx := String.utf8ByteSize s }

theorem String.Pos.le_iff {i₁ : String.Pos} {i₂ : String.Pos} : i₁ ≤ i₂ ↔ i₁.byteIdx ≤ i₂.byteIdx

@[simp]

theorem String.Pos.mk_le_mk {i₁ : Nat} {i₂ : Nat} : { byteIdx := i₁ } ≤ { byteIdx := i₂ } ↔ i₁ ≤ i₂

theorem String.Pos.lt_iff {i₁ : String.Pos} {i₂ : String.Pos} : i₁ < i₂ ↔ i₁.byteIdx < i₂.byteIdx

@[simp]

theorem String.Pos.mk_lt_mk {i₁ : Nat} {i₂ : Nat} : { byteIdx := i₁ } < { byteIdx := i₂ } ↔ i₁ < i₂

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

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

Equations

• String.Pos.Valid s p = ∃ (cs : List Char), ∃ (cs' : List Char), cs ++ cs' = s.data ∧ p.byteIdx = String.utf8Len cs

@[simp]

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

@[simp]

theorem String.Pos.valid_endPos {s : String} : String.Pos.Valid s (String.endPos s)

theorem String.Pos.Valid.mk (cs : List Char) (cs' : List Char) : String.Pos.Valid { data := cs ++ cs' } { byteIdx := String.utf8Len cs }

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

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

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

def String.utf8InductionOn {motive : List Char → String.Pos → Sort u} (s : List Char) (i : String.Pos) (p : String.Pos) (nil : (i : String.Pos) → motive [] i) (eq : (c : Char) → (cs : List Char) → motive (c :: cs) p) (ind : (c : Char) → (cs : List Char) → (i : String.Pos) → 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 : Nat) (p : Nat) (n : Nat) : String.utf8GetAux s { byteIdx := i + n } { byteIdx := p + n } = String.utf8GetAux s { byteIdx := i } { byteIdx := p }

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

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

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

theorem String.get_cons_addChar (c : Char) (cs : List Char) (i : String.Pos) : String.get { data := c :: cs } (i + c) = String.get { data := cs } i

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

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

@[simp]

theorem String.get!_eq_get (s : String) (p : String.Pos) : String.get! s p = String.get s p

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

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

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

theorem String.next_of_valid' (cs : List Char) (cs' : List Char) : String.next { data := cs ++ cs' } { byteIdx := String.utf8Len cs } = { byteIdx := String.utf8Len cs + String.csize (List.headD cs' default) }

theorem String.next_of_valid (cs : List Char) (c : Char) (cs' : List Char) : String.next { data := cs ++ c :: cs' } { byteIdx := String.utf8Len cs } = { byteIdx := String.utf8Len cs + String.csize c }

theorem String.lt_next' (s : String) (p : String.Pos) : p < String.next s p

@[simp]

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

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

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

theorem String.prev_of_valid (cs : List Char) (c : Char) (cs' : List Char) : String.prev { data := cs ++ c :: cs' } { byteIdx := String.utf8Len cs + String.csize c } = { byteIdx := String.utf8Len cs }

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

@[simp]

theorem String.prev_zero (s : String) : String.prev s 0 = 0

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

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

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

@[simp]

theorem String.get'_eq (s : String) (p : String.Pos) (h : ¬String.atEnd s p = true) : String.get' s p h = String.get s p

@[simp]

theorem String.next'_eq (s : String) (p : String.Pos) (h : ¬String.atEnd s p = true) : String.next' s p h = String.next s p

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem String.extract_cons_addChar (c : Char) (cs : List Char) (b : String.Pos) (e : String.Pos) : String.extract { data := c :: cs } (b + c) (e + c) = String.extract { data := cs } b e

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

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

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

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

@[simp]

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

theorem String.join_eq (ss : List String) : String.join ss = { data := List.join (List.map String.data ss) }

theorem String.join_eq.go (ss : List String) (cs : List Char) : List.foldl (fun (x x_1 : String) => x ++ x_1) { data := cs } ss = { data := cs ++ List.join (List.map String.data ss) }

@[simp]

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

theorem String.singleton_eq (c : Char) : String.singleton c = { data := [c] }

@[simp]

theorem String.data_singleton (c : Char) : (String.singleton c).data = [c]

@[simp]

theorem String.append_nil (s : String) : s ++ "" = s

@[simp]

theorem String.nil_append (s : String) : "" ++ s = s

theorem String.append_assoc (s₁ : String) (s₂ : String) (s₃ : String) : s₁ ++ s₂ ++ s₃ = s₁ ++ (s₂ ++ s₃)

@[simp]

theorem String.Iterator.forward_eq_nextn : String.Iterator.forward = String.Iterator.nextn

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

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

Validity for a string iterator.

Equations

• String.Iterator.Valid it = String.Pos.Valid it.s (String.Iterator.pos it)

inductive String.Iterator.ValidFor (l : List Char) (r : List Char) : String.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}, String.Iterator.ValidFor l r { s := { data := List.reverseAux l r }, i := { byteIdx := String.utf8Len l } }

  The canonical constructor for ValidFor.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

theorem Substring.prev_zero (s : Substring) : Substring.prev s 0 = 0

@[simp]

theorem Substring.prevn_zero (s : Substring) (n : Nat) : Substring.prevn s n 0 = 0

structure Substring.Valid (s : Substring) : Prop

Validity for a substring.

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

  The start position of a valid substring is valid.

• stopValid : String.Pos.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 : Substring.Valid default

inductive Substring.ValidFor (l : List Char) (m : List Char) (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}, Substring.ValidFor l m r { str := { data := 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 : List Char} {m : List Char} {r : List Char} {s : Substring} : Substring.ValidFor l m r s → Substring.Valid s

theorem Substring.ValidFor.of_eq {l : List Char} {m : List Char} {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 → Substring.ValidFor l m r s

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

theorem Substring.ValidFor.str {l : List Char} {m : List Char} {r : List Char} {s : Substring} : Substring.ValidFor l m r s → s.str = { data := l ++ m ++ r }

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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