Basic lemmas about strings

This file contains lemmas that could be in Init.Data.String.Basic but are not because they are not needed to define basic string operations.

@[simp]

theorem String.singleton_append_inj {c : Char} {s : String} {d : Char} {t : String} : singleton c ++ s = singleton d ++ t ↔ c = d ∧ s = t

@[simp]

theorem String.push_inj {s : String} {c : Char} {t : String} {d : Char} : s.push c = t.push d ↔ s = t ∧ c = d

@[simp]

theorem String.append_eq_empty_iff {s t : String} : s ++ t = "" ↔ s = "" ∧ t = ""

@[simp]

theorem String.append_eq_left_iff {s t : String} : s ++ t = s ↔ t = ""

@[simp]

theorem String.append_eq_right_iff {s t : String} : s ++ t = t ↔ s = ""

@[simp]

theorem String.empty_eq_iff {s : String} : "" = s ↔ s = ""

@[simp]

theorem String.push_ne_empty {s : String} {c : Char} : s.push c ≠ ""

@[simp]

theorem String.singleton_ne_empty {c : Char} : singleton c ≠ ""

theorem String.empty_ne_singleton {c : Char} : "" ≠ singleton c

@[simp]

theorem String.Slice.Pos.copy_inj {s : Slice} {p₁ p₂ : s.Pos} : p₁.copy = p₂.copy ↔ p₁ = p₂

@[simp]

theorem String.Pos.startPos_le {s : String} (p : s.Pos) : s.startPos ≤ p

@[simp]

theorem String.Slice.Pos.startPos_le {s : Slice} (p : s.Pos) : s.startPos ≤ p

theorem String.getUTF8Byte_eq_getUTF8Byte_toSlice {s : String} {p : Pos.Raw} {h : p < s.rawEndPos} : s.getUTF8Byte p h = s.toSlice.getUTF8Byte p ⋯

theorem String.getUTF8Byte_toSlice {s : String} {p : Pos.Raw} {h : p < s.toSlice.rawEndPos} : s.toSlice.getUTF8Byte p h = s.getUTF8Byte p h

@[simp]

theorem String.Pos.byte_toSlice {s : String} {p : s.Pos} {h : p.toSlice ≠ s.toSlice.endPos} : p.toSlice.byte h = p.byte ⋯

theorem String.Pos.byte_eq_byte_toSlice {s : String} {p : s.Pos} {h : p ≠ s.endPos} : p.byte h = p.toSlice.byte ⋯

theorem String.Slice.toByteArray_copy_slice {s : Slice} {p₁ p₂ : s.Pos} {h : p₁ ≤ p₂} : (s.slice p₁ p₂ h).copy.toByteArray = s.copy.toByteArray.extract p₁.offset.byteIdx p₂.offset.byteIdx

theorem String.toByteArray_copy_slice {s : String} {p₁ p₂ : s.Pos} {h : p₁ ≤ p₂} : (s.slice p₁ p₂ h).copy.toByteArray = s.toByteArray.extract p₁.offset.byteIdx p₂.offset.byteIdx

theorem String.Slice.utf8ByteSize_eq_size_toByteArray_copy {s : Slice} : s.utf8ByteSize = s.copy.toByteArray.size

@[simp]

theorem String.Slice.sliceTo_sliceFrom {s : Slice} {pos : s.Pos} {pos' : (s.sliceFrom pos).Pos} : (s.sliceFrom pos).sliceTo pos' = s.slice pos (Pos.ofSliceFrom pos') ⋯

@[simp]

theorem String.Slice.sliceFrom_sliceTo {s : Slice} {pos : s.Pos} {pos' : (s.sliceTo pos).Pos} : (s.sliceTo pos).sliceFrom pos' = s.slice (Pos.ofSliceTo pos') pos ⋯

@[simp]

theorem String.Slice.sliceFrom_sliceFrom {s : Slice} {pos : s.Pos} {pos' : (s.sliceFrom pos).Pos} : (s.sliceFrom pos).sliceFrom pos' = s.sliceFrom (Pos.ofSliceFrom pos')

@[simp]

theorem String.Slice.sliceTo_sliceTo {s : Slice} {pos : s.Pos} {pos' : (s.sliceTo pos).Pos} : (s.sliceTo pos).sliceTo pos' = s.sliceTo (Pos.ofSliceTo pos')

theorem String.Slice.copy_eq_copy_slice {s : Slice} {pos₁ pos₂ : s.Pos} {h : pos₁ ≤ pos₂} : s.copy = (s.sliceTo pos₁).copy ++ (s.slice pos₁ pos₂ h).copy ++ (s.sliceFrom pos₂).copy

theorem String.copy_toByteArray_sliceTo {s : String} {pos : s.Pos} : (s.sliceTo pos).copy.toByteArray = s.toByteArray.extract 0 pos.offset.byteIdx

theorem String.Slice.pos!_eq_pos {s : Slice} {p : Pos.Raw} (h : Pos.Raw.IsValidForSlice s p) : s.pos! p = s.pos p h

theorem String.pos!_eq_pos {s : String} {p : Pos.Raw} (h : Pos.Raw.IsValid s p) : s.pos! p = s.pos p h

@[simp]

theorem String.Slice.copy_pos {s : Slice} {p : Pos.Raw} {h : Pos.Raw.IsValidForSlice s p} : (s.pos p h).copy = s.copy.pos p ⋯

@[simp]

theorem String.Slice.cast_pos {s t : Slice} {p : Pos.Raw} {h : Pos.Raw.IsValidForSlice s p} {h' : s = t} : (s.pos p h).cast h' = t.pos p ⋯

@[simp]

theorem String.cast_pos {s t : String} {p : Pos.Raw} {h : Pos.Raw.IsValid s p} {h' : s = t} : (s.pos p h).cast h' = t.pos p ⋯

@[simp]

theorem String.Pos.Raw.isValidForSlice_zero {s : Slice} : IsValidForSlice s 0

@[simp]

theorem String.Pos.get_ofToSlice {s : String} {p : s.toSlice.Pos} {h : ofToSlice p ≠ s.endPos} : (ofToSlice p).get h = p.get ⋯