Splits predicates on String.ValidPos 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.ValidPos.Splits {s : String} (p : s.ValidPos) (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.ValidPos.splits_cast_iff {s₁ s₂ : String} {h : s₁ = s₂} {p : s₁.ValidPos} {t₁ t₂ : String} : (p.cast h).Splits t₁ t₂ ↔ p.Splits t₁ t₂

theorem String.ValidPos.Splits.cast {s₁ s₂ : String} {p : s₁.ValidPos} {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.toCopy {s : Slice} {p : s.Pos} {t₁ t₂ : String} (h : p.Splits t₁ t₂) : p.toCopy.Splits t₁ t₂

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

@[simp]

theorem String.Slice.Pos.splits_toCopy_iff {s : Slice} {p : s.Pos} {t₁ t₂ : String} : p.toCopy.Splits t₁ t₂ ↔ p.Splits t₁ t₂

@[simp]

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

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

theorem String.ValidPos.splits {s : String} (p : s.ValidPos) : p.Splits (s.replaceEnd p).copy (s.replaceStart p).copy

theorem String.Slice.Pos.splits {s : Slice} (p : s.Pos) : p.Splits (s.replaceEnd p).copy (s.replaceStart p).copy

theorem String.ValidPos.Splits.bytes_left_eq {s : String} {p : s.ValidPos} {t₁ t₂ : String} (h : p.Splits t₁ t₂) : t₁.bytes = s.bytes.extract 0 p.offset.byteIdx

theorem String.ValidPos.Splits.bytes_right_eq {s : String} {p : s.ValidPos} {t₁ t₂ : String} (h : p.Splits t₁ t₂) : t₂.bytes = s.bytes.extract p.offset.byteIdx s.utf8ByteSize

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

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

theorem String.ValidPos.Splits.eq {s : String} {p : s.ValidPos} {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_endValidPos (s : String) : s.endValidPos.Splits s ""

@[simp]

theorem String.splits_endValidPos_iff {t₁ t₂ s : String} : s.endValidPos.Splits t₁ t₂ ↔ t₁ = s ∧ t₂ = ""

theorem String.ValidPos.Splits.eq_endValidPos_iff {t₁ t₂ s : String} {p : s.ValidPos} (h : p.Splits t₁ t₂) : p = s.endValidPos ↔ t₂ = ""

theorem String.splits_startValidPos (s : String) : s.startValidPos.Splits "" s

@[simp]

theorem String.splits_startValidPos_iff {t₁ t₂ s : String} : s.startValidPos.Splits t₁ t₂ ↔ t₁ = "" ∧ t₂ = s

theorem String.ValidPos.Splits.eq_startValidPos_iff {t₁ t₂ s : String} {p : s.ValidPos} (h : p.Splits t₁ t₂) : p = s.startValidPos ↔ 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.ValidPos.splits_next_right {s : String} (p : s.ValidPos) (hp : p ≠ s.endValidPos) : p.Splits (s.replaceEnd p).copy (singleton (p.get hp) ++ (s.replaceStart (p.next hp)).copy)

theorem String.ValidPos.splits_next {s : String} (p : s.ValidPos) (hp : p ≠ s.endValidPos) : (p.next hp).Splits ((s.replaceEnd p).copy ++ singleton (p.get hp)) (s.replaceStart (p.next hp)).copy

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

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

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

theorem String.ValidPos.Splits.exists_eq_append_singleton {t₁ t₂ s : String} {p : s.ValidPos} (hp : p ≠ s.endValidPos) (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.ValidPos.Splits.ne_endValidPos_of_singleton {t₁ : String} {c : Char} {t₂ s : String} {p : s.ValidPos} (h : p.Splits t₁ (singleton c ++ t₂)) : p ≠ s.endValidPos

theorem String.ValidPos.Splits.ne_startValidPos_of_singleton {t₁ : String} {c : Char} {t₂ s : String} {p : s.ValidPos} (h : p.Splits (t₁ ++ singleton c) t₂) : p ≠ s.startValidPos

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.ValidPos.Splits.next {t₁ : String} {c : Char} {t₂ s : String} {p : s.ValidPos} (h : p.Splits t₁ (singleton c ++ t₂)) : (p.next ⋯).Splits (t₁ ++ singleton c) t₂

You might want to invoke ValidPos.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.