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_inj {c d : Char} : singleton c = singleton d ↔ c = d

@[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.ofList_cons {c : Char} {l : List Char} : ofList (c :: l) = singleton c ++ ofList l

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

theorem String.Slice.ext {s t : Slice} (h : s.str = t.str) (hsi : s.startInclusive.cast h = t.startInclusive) (hee : s.endExclusive.cast h = t.endExclusive) : s = t

@[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')

@[simp]

theorem String.Slice.sliceFrom_slice {s : Slice} {p₁ p₂ : s.Pos} {h : p₁ ≤ p₂} {p : (s.slice p₁ p₂ h).Pos} : (s.slice p₁ p₂ h).sliceFrom p = s.slice (Pos.ofSlice p) p₂ ⋯

@[simp]

theorem String.Slice.sliceTo_slice {s : Slice} {p₁ p₂ : s.Pos} {h : p₁ ≤ p₂} {p : (s.slice p₁ p₂ h).Pos} : (s.slice p₁ p₂ h).sliceTo p = s.slice p₁ (Pos.ofSlice p) ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem String.sliceFrom_slice {s : String} {p₁ p₂ : s.Pos} {h : p₁ ≤ p₂} {p : (s.slice p₁ p₂ h).Pos} : (s.slice p₁ p₂ h).sliceFrom p = s.slice (Pos.ofSlice p) p₂ ⋯

@[simp]

theorem String.sliceTo_slice {s : String} {p₁ p₂ : s.Pos} {h : p₁ ≤ p₂} {p : (s.slice p₁ p₂ h).Pos} : (s.slice p₁ p₂ h).sliceTo p = s.slice p₁ (Pos.ofSlice p) ⋯

@[simp]

theorem String.Slice.sliceFrom_startPos {s : Slice} : s.sliceFrom s.startPos = s

@[simp]

theorem String.Slice.sliceFrom_eq_self_iff {s : Slice} {p : s.Pos} : s.sliceFrom p = s ↔ p = s.startPos

@[simp]

theorem String.Slice.sliceTo_endPos {s : Slice} : s.sliceTo s.endPos = s

@[simp]

theorem String.Slice.sliceTo_eq_self_iff {s : Slice} {p : s.Pos} : s.sliceTo p = s ↔ p = s.endPos

@[simp]

theorem String.Slice.slice_startPos {s : Slice} {p : s.Pos} : s.slice s.startPos p ⋯ = s.sliceTo p

@[simp]

theorem String.Slice.slice_eq_self_iff {s : Slice} {p₁ p₂ : s.Pos} {h : p₁ ≤ p₂} : s.slice p₁ p₂ h = s ↔ p₁ = s.startPos ∧ p₂ = s.endPos

@[simp]

theorem String.Slice.slice_endPos {s : Slice} {p : s.Pos} : s.slice p s.endPos ⋯ = s.sliceFrom p

@[simp]

theorem String.sliceFrom_startPos {s : String} : s.sliceFrom s.startPos = s.toSlice

@[simp]

theorem String.sliceFrom_eq_toSlice_iff {s : String} {p : s.Pos} : s.sliceFrom p = s.toSlice ↔ p = s.startPos

@[simp]

theorem String.sliceTo_endPos {s : String} : s.sliceTo s.endPos = s.toSlice

@[simp]

theorem String.sliceTo_eq_toSlice_iff {s : String} {p : s.Pos} : s.sliceTo p = s.toSlice ↔ p = s.endPos

@[simp]

theorem String.slice_startPos {s : String} {p : s.Pos} : s.slice s.startPos p ⋯ = s.sliceTo p

@[simp]

theorem String.slice_endPos {s : String} {p : s.Pos} : s.slice p s.endPos ⋯ = s.sliceFrom p

@[simp]

theorem String.slice_eq_toSlice_iff {s : String} {p₁ p₂ : s.Pos} {h : p₁ ≤ p₂} : s.slice p₁ p₂ h = s.toSlice ↔ p₁ = s.startPos ∧ p₂ = s.endPos

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.copy = t.copy} {h'' : Pos.Raw.IsValidForSlice t p} : (s.pos p h).cast h' = t.pos p h''

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

@[simp]

theorem String.push_empty {c : Char} : "".push c = singleton c

@[simp]

theorem String.Slice.Pos.nextn_zero {s : Slice} {p : s.Pos} : p.nextn 0 = p

theorem String.Slice.Pos.nextn_add_one {n : Nat} {s : Slice} {p : s.Pos} : p.nextn (n + 1) = if h : p = s.endPos then p else (p.next h).nextn n

@[simp]

theorem String.Slice.Pos.nextn_endPos {n : Nat} {s : Slice} : s.endPos.nextn n = s.endPos

theorem String.Pos.nextn_eq_nextn_toSlice {n : Nat} {s : String} {p : s.Pos} : p.nextn n = ofToSlice (p.toSlice.nextn n)

@[simp]

theorem String.Pos.nextn_zero {s : String} {p : s.Pos} : p.nextn 0 = p

theorem String.Pos.nextn_add_one {n : Nat} {s : String} {p : s.Pos} : p.nextn (n + 1) = if h : p = s.endPos then p else (p.next h).nextn n

theorem String.Pos.nextn_toSlice {n : Nat} {s : String} {p : s.Pos} : p.toSlice.nextn n = (p.nextn n).toSlice

theorem String.Pos.toSlice_nextn {n : Nat} {s : String} {p : s.Pos} : (p.nextn n).toSlice = p.toSlice.nextn n

@[simp]

theorem String.Pos.nextn_endPos {n : Nat} {s : String} : s.endPos.nextn n = s.endPos

@[simp]

theorem String.Slice.Pos.cast_toSlice_copy {s : Slice} {pos : s.Pos} : pos.copy.toSlice.cast ⋯ = pos

@[simp]

theorem String.Slice.Pos.sliceFrom_eq_startPos {s : Slice} {p : s.Pos} : p.sliceFrom p ⋯ = (s.sliceFrom p).startPos

@[simp]

theorem String.Slice.Pos.sliceFrom_endPos {s : Slice} {p : s.Pos} : p.sliceFrom s.endPos ⋯ = (s.sliceFrom p).endPos

@[simp]

theorem String.Slice.Pos.sliceTo_startPos {s : Slice} {p : s.Pos} : p.sliceTo s.startPos ⋯ = (s.sliceTo p).startPos

@[simp]

theorem String.Slice.Pos.sliceTo_eq_endPos {s : Slice} {p : s.Pos} : p.sliceTo p ⋯ = (s.sliceTo p).endPos

@[simp]

theorem String.Slice.Pos.slice_eq_startPos {s : Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} : p₀.slice p₀ p₁ ⋯ h = (s.slice p₀ p₁ ⋯).startPos

@[simp]

theorem String.Slice.Pos.slice_eq_endPos {s : Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} : p₁.slice p₀ p₁ h ⋯ = (s.slice p₀ p₁ ⋯).endPos