Documentation

Batteries.Data.String.Lemmas

theorem String.lt_trans {s₁ : String} {s₂ : String} {s₃ : String} :
s₁ < s₂s₂ < s₃s₁ < s₃
theorem String.lt_antisymm {s₁ : String} {s₂ : String} (h₁ : ¬s₁ < s₂) (h₂ : ¬s₂ < s₁) :
s₁ = s₂
@[simp]
theorem String.mk_length (s : List Char) :
{ data := s }.length = s.length
@[inline]

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

Equations
Instances For
    @[simp]
    theorem String.utf8ByteSize_mk (cs : List Char) :
    { data := cs }.utf8ByteSize = String.utf8Len cs
    @[simp]
    theorem String.utf8Len_cons (c : Char) (cs : List Char) :
    String.utf8Len (c :: cs) = String.utf8Len cs + c.utf8Size
    @[simp]
    theorem String.utf8Len_append (cs₁ : List Char) (cs₂ : List Char) :
    String.utf8Len (cs₁ ++ cs₂) = String.utf8Len cs₁ + String.utf8Len cs₂
    theorem String.utf8Len_reverseAux (cs₁ : List Char) (cs₂ : List Char) :
    String.utf8Len (cs₁.reverseAux cs₂) = String.utf8Len cs₁ + String.utf8Len cs₂
    @[simp]
    theorem String.utf8Len_le_of_sublist {cs₁ : List Char} {cs₂ : List Char} :
    cs₁.Sublist cs₂String.utf8Len cs₁ String.utf8Len cs₂
    theorem String.utf8Len_le_of_infix {cs₁ : List Char} {cs₂ : List Char} (h : cs₁ <:+: cs₂) :
    theorem String.utf8Len_le_of_suffix {cs₁ : List Char} {cs₂ : List Char} (h : cs₁ <:+ cs₂) :
    theorem String.utf8Len_le_of_prefix {cs₁ : List Char} {cs₂ : List Char} (h : cs₁ <+: cs₂) :
    @[simp]
    theorem String.endPos_eq (cs : List Char) :
    { data := cs }.endPos = { byteIdx := String.utf8Len cs }
    theorem String.Pos.lt_addChar (p : String.Pos) (c : Char) :
    p < p + c

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

    Equations
    Instances For
      @[simp]
      theorem String.Pos.Valid.mk (cs : List Char) (cs' : List Char) :
      String.Pos.Valid { data := cs ++ cs' } { byteIdx := String.utf8Len cs }
      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 CharString.PosSort 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 pmotive 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
      Instances For
        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_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 } = cs'.headD default
        theorem String.get_of_valid (cs : List Char) (cs' : List Char) :
        { data := cs ++ cs' }.get { byteIdx := String.utf8Len cs } = cs'.headD default
        theorem String.get_cons_addChar (c : Char) (cs : List Char) (i : String.Pos) :
        { data := c :: cs }.get (i + c) = { data := cs }.get 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 } = cs'.head?
        theorem String.get?_of_valid (cs : List Char) (cs' : List Char) :
        { data := cs ++ cs' }.get? { byteIdx := String.utf8Len cs } = cs'.head?
        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) :
        { data := cs ++ cs' }.set { byteIdx := String.utf8Len cs } c' = { data := cs ++ List.modifyHead (fun (x : Char) => c') cs' }
        theorem String.modify_of_valid {f : CharChar} (cs : List Char) (cs' : List Char) :
        { data := cs ++ cs' }.modify { byteIdx := String.utf8Len cs } f = { data := cs ++ List.modifyHead f cs' }
        theorem String.next_of_valid' (cs : List Char) (cs' : List Char) :
        { data := cs ++ cs' }.next { byteIdx := String.utf8Len cs } = { byteIdx := String.utf8Len cs + (cs'.headD default).utf8Size }
        theorem String.next_of_valid (cs : List Char) (c : Char) (cs' : List Char) :
        { data := cs ++ c :: cs' }.next { byteIdx := String.utf8Len cs } = { byteIdx := String.utf8Len cs + c.utf8Size }
        @[simp]
        theorem String.atEnd_iff (s : String) (p : String.Pos) :
        s.atEnd p = true s.endPos p
        theorem String.valid_next {s : String} {p : String.Pos} (h : String.Pos.Valid s p) (h₂ : p < s.endPos) :
        String.Pos.Valid s (s.next p)
        theorem String.utf8PrevAux_of_valid {cs : List Char} {cs' : List Char} {c : Char} {i : Nat} {p : Nat} (hp : i + (String.utf8Len cs + c.utf8Size) = 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) :
        { data := cs ++ c :: cs' }.prev { byteIdx := String.utf8Len cs + c.utf8Size } = { byteIdx := String.utf8Len cs }
        theorem String.prev_of_valid' (cs : List Char) (cs' : List Char) :
        { data := cs ++ cs' }.prev { byteIdx := String.utf8Len cs } = { byteIdx := String.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 : List Char) (cs' : List Char) :
        { data := cs ++ cs' }.atEnd { byteIdx := String.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 : CharBool) (l : List Char) (m : List Char) (r : List Char) :
        { data := l ++ m ++ r }.findAux 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 : CharBool) (s : String) :
        s.find p = { byteIdx := String.utf8Len (List.takeWhile (fun (x : Char) => !p x) s.data) }
        theorem String.revFindAux_of_valid (p : CharBool) (l : List Char) (r : List Char) :
        { data := l.reverse ++ r }.revFindAux p { byteIdx := String.utf8Len l } = Option.map (fun (x : List Char) => { byteIdx := String.utf8Len x }) (List.dropWhile (fun (x : Char) => !p x) l).tail?
        theorem String.revFind_of_valid (p : CharBool) (s : String) :
        s.revFind p = Option.map (fun (x : List Char) => { byteIdx := String.utf8Len x }) (List.dropWhile (fun (x : Char) => !p x) s.data.reverse).tail?
        @[irreducible]
        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 (x1 x2 : Char) => decide (x1 = x2)) r₁ r₂).fst }
        theorem String.firstDiffPos_eq (a : String) (b : String) :
        a.firstDiffPos b = { byteIdx := String.utf8Len (List.takeWhile₂ (fun (x1 x2 : Char) => decide (x1 = x2)) 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 + iString.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₁_append_right (s : List Char) (t : List Char) (i : Nat) (b : Nat) (e : String.Pos) :
        b = String.utf8Len s + iString.extract.go₁ (s ++ t) { byteIdx := i } { byteIdx := b } e = String.extract.go₂ t { byteIdx := b } e
        theorem String.extract_cons_addChar (c : Char) (cs : List Char) (b : String.Pos) (e : String.Pos) :
        { data := c :: cs }.extract (b + c) (e + c) = { data := cs }.extract b e
        theorem String.extract_zero_endPos (s : String) :
        s.extract 0 s.endPos = s
        theorem String.extract_of_valid (l : List Char) (m : List Char) (r : List Char) :
        { data := l ++ m ++ r }.extract { byteIdx := String.utf8Len l } { byteIdx := String.utf8Len l + String.utf8Len m } = { data := m }
        @[irreducible]
        theorem String.splitAux_of_valid (p : CharBool) (l : List Char) (m : List Char) (r : List Char) (acc : List String) :
        { data := l ++ m ++ r }.splitAux p { byteIdx := String.utf8Len l } { byteIdx := String.utf8Len l + String.utf8Len m } acc = acc.reverse ++ List.map String.mk (List.splitOnP.go p r m.reverse)
        theorem String.split_of_valid (s : String) (p : CharBool) :
        s.split p = List.map String.mk (List.splitOnP p s.data)
        @[simp]
        theorem String.toString_toSubstring (s : String) :
        s.toSubstring.toString = s
        theorem String.join_eq (ss : List String) :
        String.join ss = { data := (List.map String.data ss).flatten }
        theorem String.join_eq.go (ss : List String) (cs : List Char) :
        List.foldl (fun (x1 x2 : String) => x1 ++ x2) { data := cs } ss = { data := cs ++ (List.map String.data ss).flatten }
        @[simp]
        theorem String.data_join (ss : List String) :
        (String.join ss).data = (List.map String.data ss).flatten
        @[deprecated String.append_empty]
        theorem String.append_nil (s : String) :
        s ++ "" = s

        Alias of String.append_empty.

        @[deprecated String.empty_append]
        theorem String.nil_append (s : String) :
        "" ++ s = s

        Alias of String.empty_append.

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

        Validity for a string iterator.

        Equations
        Instances For

          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.

          Instances For
            theorem String.Iterator.ValidFor.out {l : List Char} {r : List Char} {it : String.Iterator} :
            String.Iterator.ValidFor l r itit = { s := { data := l.reverseAux 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 itit = { s := { data := l.reverse ++ r }, i := { byteIdx := String.utf8Len l.reverse } }
            theorem String.Iterator.ValidFor.mk' {l : List Char} {r : List Char} :
            String.Iterator.ValidFor l r { s := { data := l.reverse ++ r }, i := { byteIdx := String.utf8Len l.reverse } }
            theorem String.Iterator.ValidFor.of_eq {l : List Char} {r : List Char} (it : String.Iterator) :
            it.s.data = l.reverseAux rit.i.byteIdx = String.utf8Len lString.Iterator.ValidFor l r it
            theorem String.Iterator.ValidFor.toString {l : List Char} {r : List Char} {it : String.Iterator} :
            String.Iterator.ValidFor l r itit.s = { data := l.reverseAux r }
            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 = it.s.endPos r = []
            theorem String.Iterator.ValidFor.curr {l : List Char} {r : List Char} {it : String.Iterator} :
            String.Iterator.ValidFor l r itit.curr = r.headD default
            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) (it.setCurr c)
            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 (m.reverse ++ l) r it₂) :
            it₁.extract it₂ = { data := m }
            theorem String.Iterator.ValidFor.remainingToString {l : List Char} {r : List Char} {it : String.Iterator} (h : String.Iterator.ValidFor l r it) :
            it.remainingToString = { 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 r.lengthString.Iterator.ValidFor ((List.take n r).reverse ++ l) (List.drop n r) (it.nextn n)
            theorem String.Iterator.ValidFor.prevn {l : List Char} {r : List Char} {it : String.Iterator} :
            String.Iterator.ValidFor l r it∀ (n : Nat), n l.lengthString.Iterator.ValidFor (List.drop n l) ((List.take n l).reverse ++ r) (it.prevn n)
            theorem String.Iterator.Valid.validFor {it : String.Iterator} :
            it.Valid∃ (l : List Char), ∃ (r : List Char), String.Iterator.ValidFor l r it
            theorem String.valid_mkIterator (s : String) :
            s.mkIterator.Valid
            theorem String.Iterator.Valid.remainingBytes_le {it : String.Iterator} :
            it.Validit.remainingBytes it.s.utf8ByteSize
            theorem String.Iterator.Valid.next {it : String.Iterator} :
            it.Validit.hasNext = trueit.next.Valid
            theorem String.Iterator.Valid.prev {it : String.Iterator} :
            it.Validit.prev.Valid
            theorem String.Iterator.Valid.setCurr {c : Char} {it : String.Iterator} :
            it.Valid(it.setCurr c).Valid
            theorem String.Iterator.Valid.toEnd (it : String.Iterator) :
            it.toEnd.Valid
            theorem String.Iterator.Valid.remainingToString {l : List Char} {r : List Char} {it : String.Iterator} (h : String.Iterator.ValidFor l r it) :
            it.remainingToString = { data := r }
            theorem String.Iterator.Valid.prevn {it : String.Iterator} (h : it.Valid) (n : Nat) :
            (it.prevn n).Valid
            theorem String.offsetOfPosAux_of_valid (l : List Char) (m : List Char) (r : List Char) (n : Nat) :
            { data := l ++ m ++ r }.offsetOfPosAux { byteIdx := String.utf8Len l + String.utf8Len m } { byteIdx := String.utf8Len l } n = n + m.length
            theorem String.offsetOfPos_of_valid (l : List Char) (r : List Char) :
            { data := l ++ r }.offsetOfPos { byteIdx := String.utf8Len l } = l.length
            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 : CharBool) (l : List Char) (m : List Char) (r : List Char) :
            { data := l ++ m ++ r }.anyAux { byteIdx := String.utf8Len l + String.utf8Len m } p { byteIdx := String.utf8Len l } = m.any p
            theorem String.any_eq (s : String) (p : CharBool) :
            s.any p = s.data.any p
            theorem String.any_iff (s : String) (p : CharBool) :
            s.any p = true ∃ (c : Char), c s.data p c = true
            theorem String.all_eq (s : String) (p : CharBool) :
            s.all p = s.data.all p
            theorem String.all_iff (s : String) (p : CharBool) :
            s.all p = true ∀ (c : Char), c s.datap c = true
            theorem String.contains_iff (s : String) (c : Char) :
            s.contains c = true c s.data
            theorem String.mapAux_of_valid (f : CharChar) (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 : CharChar) (s : String) :
            String.map f s = { data := List.map f s.data }
            theorem String.takeWhileAux_of_valid (p : CharBool) (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) }
            structure Substring.Valid (s : Substring) :

            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.

            Instances For
              theorem Substring.Valid.startValid {s : Substring} (self : s.Valid) :
              String.Pos.Valid s.str s.startPos

              The start position of a valid substring is valid.

              theorem Substring.Valid.stopValid {s : Substring} (self : s.Valid) :
              String.Pos.Valid s.str s.stopPos

              The stop position of a valid substring is valid.

              theorem Substring.Valid.le {s : Substring} (self : s.Valid) :
              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 : List Char) (m : List Char) (r : List Char) :

              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.

              Instances For
                theorem Substring.ValidFor.valid {l : List Char} {m : List Char} {r : List Char} {s : Substring} :
                Substring.ValidFor l m r ss.Valid
                theorem Substring.ValidFor.of_eq {l : List Char} {m : List Char} {r : List Char} (s : Substring) :
                s.str.data = l ++ m ++ rs.startPos.byteIdx = String.utf8Len ls.stopPos.byteIdx = String.utf8Len l + String.utf8Len mSubstring.ValidFor l m r s
                theorem String.validFor_toSubstring (s : String) :
                Substring.ValidFor [] s.data [] s.toSubstring
                theorem Substring.ValidFor.str {l : List Char} {m : List Char} {r : List Char} {s : Substring} :
                Substring.ValidFor l m r ss.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 ss.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 ss.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 ss.bsize = String.utf8Len m
                theorem Substring.ValidFor.isEmpty {l : List Char} {m : List Char} {r : List Char} {s : Substring} :
                Substring.ValidFor l m r s(s.isEmpty = true m = [])
                theorem Substring.ValidFor.toString {l : List Char} {m : List Char} {r : List Char} {s : Substring} :
                Substring.ValidFor l m r ss.toString = { data := m }
                theorem Substring.ValidFor.toIterator {l : List Char} {m : List Char} {r : List Char} {s : Substring} :
                Substring.ValidFor l m r sString.Iterator.ValidFor l.reverse (m ++ r) s.toIterator
                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 ss.get { 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 ss.next { byteIdx := String.utf8Len m₁ } = { byteIdx := String.utf8Len m₁ + c.utf8Size }
                theorem Substring.ValidFor.next_stop {l : List Char} {m : List Char} {r : List Char} {s : Substring} :
                Substring.ValidFor l m r ss.next { 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 ss.prev { byteIdx := String.utf8Len m₁ + c.utf8Size } = { 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), s.nextn 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), s.nextn 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 (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 : List Char} {r : List Char} {s : Substring} :
                Substring.ValidFor l (c :: m) r ss.front = 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 (s.drop 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) (s.take n)
                theorem Substring.ValidFor.atEnd {l : List Char} {m : List Char} {r : List Char} {p : Nat} {s : Substring} :
                Substring.ValidFor l m r s(s.atEnd { 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 sSubstring.ValidFor ml mm mr { str := { data := m }, startPos := b, stopPos := e }∃ (l' : List Char), ∃ (r' : List Char), Substring.ValidFor l' mm r' (s.extract 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 sSubstring.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 sSubstring.foldr f init s = List.foldr f init m
                theorem Substring.ValidFor.any {l : List Char} {m : List Char} {r : List Char} (f : CharBool) {s : Substring} :
                Substring.ValidFor l m r ss.any f = m.any f
                theorem Substring.ValidFor.all {l : List Char} {m : List Char} {r : List Char} (f : CharBool) {s : Substring} :
                Substring.ValidFor l m r ss.all f = m.all f
                theorem Substring.ValidFor.contains {l : List Char} {m : List Char} {r : List Char} (c : Char) {s : Substring} :
                Substring.ValidFor l m r s(s.contains c = true c m)
                theorem Substring.ValidFor.takeWhile {l : List Char} {m : List Char} {r : List Char} (p : CharBool) {s : Substring} :
                Substring.ValidFor l m r sSubstring.ValidFor l (List.takeWhile p m) (List.dropWhile p m ++ r) (s.takeWhile p)
                theorem Substring.ValidFor.dropWhile {l : List Char} {m : List Char} {r : List Char} (p : CharBool) {s : Substring} :
                Substring.ValidFor l m r sSubstring.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), 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 ss.Valid
                theorem String.valid_toSubstring (s : String) :
                s.toSubstring.Valid
                theorem Substring.Valid.bsize {s : Substring} :
                s.Valids.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.Valids.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.Valids.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.Valids.next { byteIdx := s.bsize } = { byteIdx := s.bsize }
                theorem Substring.Valid.prev {m₁ : List Char} {c : Char} {m₂ : List Char} {s : Substring} :
                s.Valids.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₁ : List Char} {m₂ : List Char} {s : Substring} :
                s.Valids.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₂ : List Char} {m₁ : List Char} {s : Substring} :
                s.Valids.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.Valids.toString.data = c :: ms.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 : String.Pos} {e : String.Pos} {s : Substring} :
                s.Valid{ str := s.toString, startPos := b, stopPos := e }.Valid(s.extract b e).Valid
                theorem Substring.Valid.toString_extract {b : String.Pos} {e : String.Pos} {s : Substring} :
                s.Valid{ str := s.toString, startPos := b, stopPos := e }.Valid(s.extract b e).toString = s.toString.extract b e
                theorem Substring.Valid.foldl {α : Type u_1} (f : αCharα) (init : α) {s : Substring} :
                s.ValidSubstring.foldl f init s = List.foldl f init s.toString.data
                theorem Substring.Valid.foldr {α : Type u_1} (f : Charαα) (init : α) {s : Substring} :
                s.ValidSubstring.foldr f init s = List.foldr f init s.toString.data
                theorem Substring.Valid.any (f : CharBool) {s : Substring} :
                s.Valids.any f = s.toString.data.any f
                theorem Substring.Valid.all (f : CharBool) {s : Substring} :
                s.Valids.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 : CharBool) {s : Substring} :
                s.Valid(s.takeWhile p).Valid
                theorem Substring.Valid.data_takeWhile (p : CharBool) {s : Substring} :
                s.Valid(s.takeWhile p).toString.data = List.takeWhile p s.toString.data
                theorem Substring.Valid.dropWhile (p : CharBool) {s : Substring} :
                s.Valid(s.dropWhile p).Valid
                theorem Substring.Valid.data_dropWhile (p : CharBool) {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 = { data := 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 = { data := 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 : CharBool) (s : String) :
                s.takeWhile p = { data := List.takeWhile p s.data }
                @[simp]
                theorem String.data_takeWhile (p : CharBool) (s : String) :
                (s.takeWhile p).data = List.takeWhile p s.data
                theorem String.dropWhile_eq (p : CharBool) (s : String) :
                s.dropWhile p = { data := List.dropWhile p s.data }
                @[simp]
                theorem String.data_dropWhile (p : CharBool) (s : String) :
                (s.dropWhile p).data = List.dropWhile p s.data