Splits predicates on String.Pos and String.Slice.Pos.

We introduce the predicate p.Splits t₁ t₂ for a position p on a string or slice s, which means that s = t₁ ++ t₂ with p lying between the two parts. This is a useful primitive when verifying string operations.

structure String.Pos.Splits {s : String} (p : s.Pos) (t₁ t₂ : String) : Prop

We say that p splits s into t₁ and t₂ if s = t₁ ++ t₂ and p is the position between t₁ and t₂.

• eq_append : s = t₁ ++ t₂
• offset_eq_rawEndPos : p.offset = t₁.rawEndPos

structure String.Slice.Pos.Splits {s : Slice} (p : s.Pos) (t₁ t₂ : String) : Prop

We say that p splits s into t₁ and t₂ if s = t₁ ++ t₂ and p is the position between t₁ and t₂.

• eq_append : s.copy = t₁ ++ t₂
• offset_eq_rawEndPos : p.offset = t₁.rawEndPos

@[simp]

theorem String.Pos.splits_cast_iff {s₁ s₂ : String} {h : s₁ = s₂} {p : s₁.Pos} {t₁ t₂ : String} : (p.cast h).Splits t₁ t₂ ↔ p.Splits t₁ t₂

theorem String.Pos.Splits.cast {s₁ s₂ : String} {p : s₁.Pos} {t₁ t₂ : String} (h : s₁ = s₂) : p.Splits t₁ t₂ → (p.cast h).Splits t₁ t₂

@[simp]

theorem String.Slice.Pos.splits_cast_iff {s₁ s₂ : Slice} {h : s₁ = s₂} {p : s₁.Pos} {t₁ t₂ : String} : (p.cast h).Splits t₁ t₂ ↔ p.Splits t₁ t₂

theorem String.Slice.Pos.Splits.cast {s₁ s₂ : Slice} {p : s₁.Pos} {t₁ t₂ : String} (h : s₁ = s₂) : p.Splits t₁ t₂ → (p.cast h).Splits t₁ t₂

theorem String.Slice.Pos.Splits.copy {s : Slice} {p : s.Pos} {t₁ t₂ : String} (h : p.Splits t₁ t₂) : p.copy.Splits t₁ t₂

theorem String.Slice.Pos.splits_of_splits_copy {s : Slice} {p : s.Pos} {t₁ t₂ : String} (h : p.copy.Splits t₁ t₂) : p.Splits t₁ t₂

@[simp]

theorem String.Slice.Pos.splits_copy_iff {s : Slice} {p : s.Pos} {t₁ t₂ : String} : p.copy.Splits t₁ t₂ ↔ p.Splits t₁ t₂

@[simp]

theorem String.Pos.splits_toSlice_iff {s : String} {p : s.Pos} {t₁ t₂ : String} : p.toSlice.Splits t₁ t₂ ↔ p.Splits t₁ t₂

theorem String.Pos.Splits.toSlice {s : String} {p : s.Pos} {t₁ t₂ : String} (h : p.Splits t₁ t₂) : p.toSlice.Splits t₁ t₂

theorem String.Pos.splits {s : String} (p : s.Pos) : p.Splits (s.sliceTo p).copy (s.sliceFrom p).copy

theorem String.Slice.Pos.splits {s : Slice} (p : s.Pos) : p.Splits (s.sliceTo p).copy (s.sliceFrom p).copy

theorem String.Pos.Splits.toByteArray_left_eq {s : String} {p : s.Pos} {t₁ t₂ : String} (h : p.Splits t₁ t₂) : t₁.toByteArray = s.toByteArray.extract 0 p.offset.byteIdx

theorem String.Pos.Splits.toByteArray_right_eq {s : String} {p : s.Pos} {t₁ t₂ : String} (h : p.Splits t₁ t₂) : t₂.toByteArray = s.toByteArray.extract p.offset.byteIdx s.utf8ByteSize

theorem String.Pos.Splits.eq_left {s : String} {p : s.Pos} {t₁ t₂ t₃ t₄ : String} (h₁ : p.Splits t₁ t₂) (h₂ : p.Splits t₃ t₄) : t₁ = t₃

theorem String.Pos.Splits.eq_right {s : String} {p : s.Pos} {t₁ t₂ t₃ t₄ : String} (h₁ : p.Splits t₁ t₂) (h₂ : p.Splits t₃ t₄) : t₂ = t₄

theorem String.Pos.Splits.eq {s : String} {p : s.Pos} {t₁ t₂ t₃ t₄ : String} (h₁ : p.Splits t₁ t₂) (h₂ : p.Splits t₃ t₄) : t₁ = t₃ ∧ t₂ = t₄

theorem String.Slice.Pos.Splits.eq_left {s : Slice} {p : s.Pos} {t₁ t₂ t₃ t₄ : String} (h₁ : p.Splits t₁ t₂) (h₂ : p.Splits t₃ t₄) : t₁ = t₃

theorem String.Slice.Pos.Splits.eq_right {s : Slice} {p : s.Pos} {t₁ t₂ t₃ t₄ : String} (h₁ : p.Splits t₁ t₂) (h₂ : p.Splits t₃ t₄) : t₂ = t₄

theorem String.Slice.Pos.Splits.eq {s : Slice} {p : s.Pos} {t₁ t₂ t₃ t₄ : String} (h₁ : p.Splits t₁ t₂) (h₂ : p.Splits t₃ t₄) : t₁ = t₃ ∧ t₂ = t₄

theorem String.Pos.Splits.of_eq {s : String} {p : s.Pos} {t₁ t₂ t₃ t₄ : String} (h : p.Splits t₁ t₂) (h₁ : t₁ = t₃) (h₂ : t₂ = t₄) : p.Splits t₃ t₄

theorem String.Slice.Pos.Splits.of_eq {s : Slice} {p : s.Pos} {t₁ t₂ t₃ t₄ : String} (h : p.Splits t₁ t₂) (h₁ : t₁ = t₃) (h₂ : t₂ = t₄) : p.Splits t₃ t₄

@[simp]

theorem String.splits_endPos (s : String) : s.endPos.Splits s ""

@[simp]

theorem String.splits_endPos_iff {t₁ t₂ s : String} : s.endPos.Splits t₁ t₂ ↔ t₁ = s ∧ t₂ = ""

theorem String.Pos.Splits.eq_endPos_iff {t₁ t₂ s : String} {p : s.Pos} (h : p.Splits t₁ t₂) : p = s.endPos ↔ t₂ = ""

theorem String.splits_startPos (s : String) : s.startPos.Splits "" s

@[simp]

theorem String.splits_startPos_iff {t₁ t₂ s : String} : s.startPos.Splits t₁ t₂ ↔ t₁ = "" ∧ t₂ = s

theorem String.Pos.Splits.eq_startPos_iff {t₁ t₂ s : String} {p : s.Pos} (h : p.Splits t₁ t₂) : p = s.startPos ↔ t₁ = ""

@[simp]

theorem String.Slice.splits_endPos (s : Slice) : s.endPos.Splits s.copy ""

@[simp]

theorem String.Slice.splits_endPos_iff {t₁ t₂ : String} {s : Slice} : s.endPos.Splits t₁ t₂ ↔ t₁ = s.copy ∧ t₂ = ""

theorem String.Slice.Pos.Splits.eq_endPos_iff {t₁ t₂ : String} {s : Slice} {p : s.Pos} (h : p.Splits t₁ t₂) : p = s.endPos ↔ t₂ = ""

@[simp]

theorem String.Slice.splits_startPos (s : Slice) : s.startPos.Splits "" s.copy

@[simp]

theorem String.Slice.splits_startPos_iff {t₁ t₂ : String} {s : Slice} : s.startPos.Splits t₁ t₂ ↔ t₁ = "" ∧ t₂ = s.copy

theorem String.Slice.Pos.Splits.eq_startPos_iff {t₁ t₂ : String} {s : Slice} {p : s.Pos} (h : p.Splits t₁ t₂) : p = s.startPos ↔ t₁ = ""

theorem String.Pos.splits_next_right {s : String} (p : s.Pos) (hp : p ≠ s.endPos) : p.Splits (s.sliceTo p).copy (singleton (p.get hp) ++ (s.sliceFrom (p.next hp)).copy)

theorem String.Pos.splits_next {s : String} (p : s.Pos) (hp : p ≠ s.endPos) : (p.next hp).Splits ((s.sliceTo p).copy ++ singleton (p.get hp)) (s.sliceFrom (p.next hp)).copy

theorem String.Pos.splits_prev_right {s : String} (p : s.Pos) (hp : p ≠ s.startPos) : p.Splits ((s.sliceTo (p.prev hp)).copy ++ singleton ((p.prev hp).get ⋯)) (s.sliceFrom p).copy

theorem String.Pos.splits_prev {s : String} (p : s.Pos) (hp : p ≠ s.startPos) : (p.prev hp).Splits (s.sliceTo (p.prev hp)).copy (singleton ((p.prev hp).get ⋯) ++ (s.sliceFrom p).copy)

theorem String.Slice.Pos.splits_next_right {s : Slice} (p : s.Pos) (hp : p ≠ s.endPos) : p.Splits (s.sliceTo p).copy (singleton (p.get hp) ++ (s.sliceFrom (p.next hp)).copy)

theorem String.Slice.Pos.splits_next {s : Slice} (p : s.Pos) (hp : p ≠ s.endPos) : (p.next hp).Splits ((s.sliceTo p).copy ++ singleton (p.get hp)) (s.sliceFrom (p.next hp)).copy

theorem String.Slice.Pos.splits_prev_right {s : Slice} (p : s.Pos) (hp : p ≠ s.startPos) : p.Splits ((s.sliceTo (p.prev hp)).copy ++ singleton ((p.prev hp).get ⋯)) (s.sliceFrom p).copy

theorem String.Slice.Pos.splits_prev {s : Slice} (p : s.Pos) (hp : p ≠ s.startPos) : (p.prev hp).Splits (s.sliceTo (p.prev hp)).copy (singleton ((p.prev hp).get ⋯) ++ (s.sliceFrom p).copy)

theorem String.Pos.Splits.exists_eq_singleton_append {t₁ t₂ s : String} {p : s.Pos} (hp : p ≠ s.endPos) (h : p.Splits t₁ t₂) : ∃ (t₂' : String), t₂ = singleton (p.get hp) ++ t₂'

theorem String.Pos.Splits.exists_eq_append_singleton {t₁ t₂ s : String} {p : s.Pos} (hp : p ≠ s.endPos) (h : (p.next hp).Splits t₁ t₂) : ∃ (t₁' : String), t₁ = t₁' ++ singleton (p.get hp)

theorem String.Pos.Splits.exists_eq_append_singleton_of_ne_startPos {t₁ t₂ s : String} {p : s.Pos} (hp : p ≠ s.startPos) (h : p.Splits t₁ t₂) : ∃ (t₁' : String), t₁ = t₁' ++ singleton ((p.prev hp).get ⋯)

theorem String.Pos.Splits.exists_eq_singleton_append_of_ne_startPos {t₁ t₂ s : String} {p : s.Pos} (hp : p ≠ s.startPos) (h : (p.prev hp).Splits t₁ t₂) : ∃ (t₂' : String), t₂ = singleton ((p.prev hp).get ⋯) ++ t₂'

theorem String.Slice.Pos.Splits.exists_eq_singleton_append {t₁ t₂ : String} {s : Slice} {p : s.Pos} (hp : p ≠ s.endPos) (h : p.Splits t₁ t₂) : ∃ (t₂' : String), t₂ = singleton (p.get hp) ++ t₂'

theorem String.Slice.Pos.Splits.exists_eq_append_singleton {t₁ t₂ : String} {s : Slice} {p : s.Pos} (hp : p ≠ s.endPos) (h : (p.next hp).Splits t₁ t₂) : ∃ (t₁' : String), t₁ = t₁' ++ singleton (p.get hp)

theorem String.Slice.Pos.Splits.exists_eq_append_singleton_of_ne_startPos {t₁ t₂ : String} {s : Slice} {p : s.Pos} (hp : p ≠ s.startPos) (h : p.Splits t₁ t₂) : ∃ (t₁' : String), t₁ = t₁' ++ singleton ((p.prev hp).get ⋯)

theorem String.Slice.Pos.Splits.exists_eq_singleton_append_of_ne_startPos {t₁ t₂ : String} {s : Slice} {p : s.Pos} (hp : p ≠ s.startPos) (h : (p.prev hp).Splits t₁ t₂) : ∃ (t₂' : String), t₂ = singleton ((p.prev hp).get ⋯) ++ t₂'

theorem String.Pos.Splits.ne_endPos_of_singleton {t₁ : String} {c : Char} {t₂ s : String} {p : s.Pos} (h : p.Splits t₁ (singleton c ++ t₂)) : p ≠ s.endPos

theorem String.Pos.Splits.ne_startPos_of_singleton {t₁ : String} {c : Char} {t₂ s : String} {p : s.Pos} (h : p.Splits (t₁ ++ singleton c) t₂) : p ≠ s.startPos

theorem String.Slice.Pos.Splits.ne_endPos_of_singleton {t₁ : String} {c : Char} {t₂ : String} {s : Slice} {p : s.Pos} (h : p.Splits t₁ (singleton c ++ t₂)) : p ≠ s.endPos

theorem String.Slice.Pos.Splits.ne_startPos_of_singleton {t₁ : String} {c : Char} {t₂ : String} {s : Slice} {p : s.Pos} (h : p.Splits (t₁ ++ singleton c) t₂) : p ≠ s.startPos

theorem String.Pos.Splits.next {t₁ : String} {c : Char} {t₂ s : String} {p : s.Pos} (h : p.Splits t₁ (singleton c ++ t₂)) : (p.next ⋯).Splits (t₁ ++ singleton c) t₂

You might want to invoke Pos.Splits.exists_eq_singleton_append to be able to apply this.

theorem String.Slice.Pos.Splits.next {t₁ : String} {c : Char} {t₂ : String} {s : Slice} {p : s.Pos} (h : p.Splits t₁ (singleton c ++ t₂)) : (p.next ⋯).Splits (t₁ ++ singleton c) t₂

You might want to invoke Slice.Pos.Splits.exists_eq_singleton_append to be able to apply this.

theorem String.Pos.Splits.prev {t₁ : String} {c : Char} {t₂ s : String} {p : s.Pos} (h : p.Splits (t₁ ++ singleton c) t₂) : (p.prev ⋯).Splits t₁ (singleton c ++ t₂)

You might want to invoke Pos.Splits.exists_eq_singleton_append_of_ne_startPos to be able to apply this.

theorem String.Slice.Pos.Splits.prev {t₁ : String} {c : Char} {t₂ : String} {s : Slice} {p : s.Pos} (h : p.Splits (t₁ ++ singleton c) t₂) : (p.prev ⋯).Splits t₁ (singleton c ++ t₂)

You might want to invoke Slice.Pos.Splits.exists_eq_singleton_append_of_ne_startPos to be able to apply this.

theorem String.Slice.sliceTo_copy_eq_iff_exists_splits {s : Slice} {p : s.Pos} {t₁ : String} : (s.sliceTo p).copy = t₁ ↔ ∃ (t₂ : String), p.Splits t₁ t₂

theorem String.sliceTo_copy_eq_iff_exists_splits {s : String} {p : s.Pos} {t₁ : String} : (s.sliceTo p).copy = t₁ ↔ ∃ (t₂ : String), p.Splits t₁ t₂

theorem String.Pos.Splits.offset_eq_decreaseBy {t₁ t₂ s : String} {p : s.Pos} (h : p.Splits t₁ t₂) : p.offset = s.rawEndPos.decreaseBy t₂.utf8ByteSize

theorem String.Slice.Pos.Splits.offset_eq_decreaseBy {t₁ t₂ : String} {s : Slice} {p : s.Pos} (h : p.Splits t₁ t₂) : p.offset = s.rawEndPos.decreaseBy t₂.utf8ByteSize

theorem String.Slice.Pos.Splits.pos_eq {s : Slice} {p q : s.Pos} {s✝ t t' : String} (h : p.Splits s✝ t) (h' : q.Splits s✝ t') : p = q

theorem String.Slice.Pos.Splits.pos_eq_of_eq_right {s : Slice} {p q : s.Pos} {s✝ s' t : String} (h : p.Splits s✝ t) (h' : q.Splits s' t) : p = q

theorem String.Pos.Splits.pos_eq {s : String} {p q : s.Pos} {s✝ t t' : String} (h : p.Splits s✝ t) (h' : q.Splits s✝ t') : p = q

theorem String.Pos.Splits.pos_eq_of_eq_right {s : String} {p q : s.Pos} {s✝ s' t : String} (h : p.Splits s✝ t) (h' : q.Splits s' t) : p = q

theorem String.Slice.Pos.Splits.get_eq_of_singleton {s : Slice} {p : s.Pos} {h : p ≠ s.endPos} {t₁ t₂ : String} {c : Char} (hs : (p.next h).Splits (t₁ ++ singleton c) t₂) : p.get h = c

theorem String.Pos.Splits.get_eq_of_singleton {s : String} {p : s.Pos} {h : p ≠ s.endPos} {t₁ t₂ : String} {c : Char} (hs : (p.next h).Splits (t₁ ++ singleton c) t₂) : p.get h = c

theorem String.Slice.splits_singleton_iff {s : Slice} {p : s.Pos} {c : Char} {t : String} : p.Splits (singleton c) t ↔ ∃ (h : s.startPos ≠ s.endPos), p = s.startPos.next h ∧ s.startPos.get h = c ∧ s.copy = singleton c ++ t

theorem String.splits_singleton_iff {s : String} {p : s.Pos} {c : Char} {t : String} : p.Splits (singleton c) t ↔ ∃ (h : s.startPos ≠ s.endPos), p = s.startPos.next h ∧ s.startPos.get h = c ∧ s = singleton c ++ t

@[simp]

theorem String.Slice.copy_sliceTo_startPos {s : Slice} : (s.sliceTo s.startPos).copy = ""

@[simp]

theorem String.copy_sliceTo_startPos {s : String} : (s.sliceTo s.startPos).copy = ""

theorem String.Slice.splits_next_startPos {s : Slice} {h : s.startPos ≠ s.endPos} : (s.startPos.next h).Splits (singleton (s.startPos.get h)) (s.sliceFrom (s.startPos.next h)).copy

theorem String.splits_next_startPos {s : String} {h : s.startPos ≠ s.endPos} : (s.startPos.next h).Splits (singleton (s.startPos.get h)) (s.sliceFrom (s.startPos.next h)).copy

theorem String.Slice.Pos.Splits.toByteArray_eq_left {s : Slice} {p : s.Pos} {t₁ t₂ : String} (h : p.Splits t₁ t₂) : t₁.toByteArray = s.copy.toByteArray.extract 0 p.offset.byteIdx

theorem String.Pos.Splits.toByteArray_eq_left {s : String} {p : s.Pos} {t₁ t₂ : String} (h : p.Splits t₁ t₂) : t₁.toByteArray = s.toByteArray.extract 0 p.offset.byteIdx

theorem String.Slice.Pos.Splits.toByteArray_eq_right {s : Slice} {p : s.Pos} {t₁ t₂ : String} (h : p.Splits t₁ t₂) : t₂.toByteArray = s.copy.toByteArray.extract p.offset.byteIdx s.copy.toByteArray.size

theorem String.Pos.Splits.toByteArray_eq_right {s : String} {p : s.Pos} {t₁ t₂ : String} (h : p.Splits t₁ t₂) : t₂.toByteArray = s.toByteArray.extract p.offset.byteIdx s.toByteArray.size

theorem String.Slice.Pos.Splits.le_iff_exists_eq_append {s : Slice} {p₁ p₂ : s.Pos} {t₁ t₂ t₃ t₄ : String} (h : p₁.Splits t₁ t₂) (h' : p₂.Splits t₃ t₄) : p₁ ≤ p₂ ↔ ∃ (t₅ : String), t₃ = t₁ ++ t₅ ∧ t₂ = t₅ ++ t₄

theorem String.Slice.Pos.Splits.lt_iff_exists_eq_append {s : Slice} {p₁ p₂ : s.Pos} {t₁ t₂ t₃ t₄ : String} (h : p₁.Splits t₁ t₂) (h' : p₂.Splits t₃ t₄) : p₁ < p₂ ↔ ∃ (t₅ : String), t₅ ≠ "" ∧ t₃ = t₁ ++ t₅ ∧ t₂ = t₅ ++ t₄

theorem String.Pos.Splits.le_iff_exists_eq_append {s : String} {p₁ p₂ : s.Pos} {t₁ t₂ t₃ t₄ : String} (h : p₁.Splits t₁ t₂) (h' : p₂.Splits t₃ t₄) : p₁ ≤ p₂ ↔ ∃ (t₅ : String), t₃ = t₁ ++ t₅ ∧ t₂ = t₅ ++ t₄

theorem String.Pos.Splits.lt_iff_exists_eq_append {s : String} {p₁ p₂ : s.Pos} {t₁ t₂ t₃ t₄ : String} (h : p₁.Splits t₁ t₂) (h' : p₂.Splits t₃ t₄) : p₁ < p₂ ↔ ∃ (t₅ : String), t₅ ≠ "" ∧ t₃ = t₁ ++ t₅ ∧ t₂ = t₅ ++ t₄

@[simp]

theorem String.Slice.Pos.splits_ofToSlice_iff {s : String} {p : s.toSlice.Pos} {t₁ t₂ : String} : (Pos.ofToSlice p).Splits t₁ t₂ ↔ p.Splits t₁ t₂

@[inline]

def String.Slice.Pos.Splits.rotateRight {s : Slice} {p : s.Pos} {t₁ t₂ t₃ : String} (h : p.Splits t₁ (t₂ ++ t₃)) : s.Pos

Given a position that splits s into t₁ and t₂ ++ t₃ with witness h, constructs a position h.rotateRight that splits s into t₁ ++ t₂ and t₃. Use h.splits_rotateRight for the witness that h.rotateRight splits s as required.

Equations

• h.rotateRight = s.pos (p.offset.increaseBy t₂.utf8ByteSize) ⋯

theorem String.Slice.Pos.Splits.splits_rotateRight {s : Slice} {p : s.Pos} {t₁ t₂ t₃ : String} (h : p.Splits t₁ (t₂ ++ t₃)) : h.rotateRight.Splits (t₁ ++ t₂) t₃

@[inline]

def String.Slice.Pos.Splits.rotateLeft {s : Slice} {p : s.Pos} {t₁ t₂ t₃ : String} (h : p.Splits (t₁ ++ t₂) t₃) : s.Pos

Given a position that splits s into t₁ ++ t₂ and t₃ with witness h, construct a position h.rotateLeft that splits s into t₁ and t₂ ++ t₃. Use h.splits_rotateLeft for the witness that h.rotateLEft splits s as required.

Equations

• h.rotateLeft = s.pos t₁.rawEndPos ⋯

theorem String.Slice.Pos.Splits.splits_rotateLeft {s : Slice} {p : s.Pos} {t₁ t₂ t₃ : String} (h : p.Splits (t₁ ++ t₂) t₃) : h.rotateLeft.Splits t₁ (t₂ ++ t₃)

@[inline]

def String.Pos.Splits.rotateRight {s : String} {p : s.Pos} {t₁ t₂ t₃ : String} (h : p.Splits t₁ (t₂ ++ t₃)) : s.Pos

Given a position that splits s into t₁ and t₂ ++ t₃ with witness h, constructs a position h.rotateRight that splits s into t₁ ++ t₂ and t₃. Use h.splits_rotateRight for the witness that h.rotateRight splits s as required.

Equations

• h.rotateRight = String.Pos.ofToSlice ⋯.rotateRight

theorem String.Pos.Splits.splits_rotateRight {s : String} {p : s.Pos} {t₁ t₂ t₃ : String} (h : p.Splits t₁ (t₂ ++ t₃)) : h.rotateRight.Splits (t₁ ++ t₂) t₃

@[inline]

def String.Pos.Splits.rotateLeft {s : String} {p : s.Pos} {t₁ t₂ t₃ : String} (h : p.Splits (t₁ ++ t₂) t₃) : s.Pos

Given a position that splits s into t₁ ++ t₂ and t₃ with witness h, construct a position h.rotateLeft that splits s into t₁ and t₂ ++ t₃. Use h.splits_rotateLeft for the witness that h.rotateLEft splits s as required.

Equations

• h.rotateLeft = String.Pos.ofToSlice ⋯.rotateLeft

theorem String.Pos.Splits.splits_rotateLeft {s : String} {p : s.Pos} {t₁ t₂ t₃ : String} (h : p.Splits (t₁ ++ t₂) t₃) : h.rotateLeft.Splits t₁ (t₂ ++ t₃)

theorem String.Slice.copy_slice_eq_iff_splits {t : String} {s : Slice} {pos₁ pos₂ : s.Pos} : (∃ (h : pos₁ ≤ pos₂), (s.slice pos₁ pos₂ h).copy = t) ↔ ∃ (t₁ : String), ∃ (t₂ : String), pos₁.Splits t₁ (t ++ t₂) ∧ pos₂.Splits (t₁ ++ t) t₂

theorem String.copy_slice_eq_iff_splits {t s : String} {pos₁ pos₂ : s.Pos} : (∃ (h : pos₁ ≤ pos₂), (s.slice pos₁ pos₂ h).copy = t) ↔ ∃ (t₁ : String), ∃ (t₂ : String), pos₁.Splits t₁ (t ++ t₂) ∧ pos₂.Splits (t₁ ++ t) t₂

theorem String.Pos.splits_append_rawEndPos {s t : String} : ((s ++ t).pos s.rawEndPos ⋯).Splits s t

theorem String.Pos.Splits.copy_sliceTo_eq {t₁ t₂ s : String} {p : s.Pos} (h : p.Splits t₁ t₂) : (s.sliceTo p).copy = t₁

theorem String.Pos.Splits.copy_sliceFrom_eq {t₁ t₂ s : String} {p : s.Pos} (h : p.Splits t₁ t₂) : (s.sliceFrom p).copy = t₂

theorem String.Slice.Pos.Splits.copy_sliceTo_eq {t₁ t₂ : String} {s : Slice} {p : s.Pos} (h : p.Splits t₁ t₂) : (s.sliceTo p).copy = t₁

theorem String.Slice.Pos.Splits.copy_sliceFrom_eq {t₁ t₂ : String} {s : Slice} {p : s.Pos} (h : p.Splits t₁ t₂) : (s.sliceFrom p).copy = t₂