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₄

@[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.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.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.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.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.