Preliminary developments for strings

This file contains the material about strings which we can write down without the results in Init.Data.String.Decode, i.e., without knowing about the bijection between String and List Char given by UTF-8 decoding and encoding.

Note that this file, despite being called Defs, contains quite a few lemmas.

@[simp]

theorem List.utf8Encode_nil : [].utf8Encode = ByteArray.empty

theorem List.utf8Encode_singleton {c : Char} : [c].utf8Encode = (String.utf8EncodeChar c).toByteArray

@[simp]

theorem List.utf8Encode_append {l l' : List Char} : (l ++ l').utf8Encode = l.utf8Encode ++ l'.utf8Encode

theorem List.utf8Encode_cons {c : Char} {l : List Char} : (c :: l).utf8Encode = [c].utf8Encode ++ l.utf8Encode

@[simp]

theorem String.utf8EncodeChar_ne_nil {c : Char} : utf8EncodeChar c ≠ []

@[simp]

theorem List.utf8Encode_eq_empty {l : List Char} : l.utf8Encode = ByteArray.empty ↔ l = []

theorem ByteArray.isValidUTF8_utf8Encode {l : List Char} : l.utf8Encode.IsValidUTF8

@[simp]

theorem ByteArray.isValidUTF8_empty : empty.IsValidUTF8

theorem Char.isValidUTF8_toByteArray_utf8EncodeChar {c : Char} : (String.utf8EncodeChar c).toByteArray.IsValidUTF8

theorem ByteArray.IsValidUTF8.append {b b' : ByteArray} (h : b.IsValidUTF8) (h' : b'.IsValidUTF8) : (b ++ b').IsValidUTF8

@[inline]

def String.fromUTF8 (a : ByteArray) (h : a.IsValidUTF8) : String

Decodes an array of bytes that encode a string as UTF-8 into the corresponding string.

@[extern lean_string_to_utf8]

def String.toUTF8 (a : String) : ByteArray

Encodes a string in UTF-8 as an array of bytes.

@[simp]

theorem String.toUTF8_eq_toByteArray {s : String} : s.toUTF8 = s.toByteArray

@[simp]

theorem String.toByteArray_empty : "".toByteArray = ByteArray.empty

@[extern lean_string_append]

def String.append (s : String) (t : String) : String

Appends two strings. Usually accessed via the ++ operator.

The internal implementation will perform destructive updates if the string is not shared.

Examples:

• "abc".append "def" = "abcdef"
• "abc" ++ "def" = "abcdef"
• "" ++ "" = ""

@[implicit_reducible]

instance instAppendString : Append String

@[simp]

theorem String.toByteArray_append {s t : String} : (s ++ t).toByteArray = s.toByteArray ++ t.toByteArray

theorem String.toByteArray_inj {s t : String} : s.toByteArray = t.toByteArray ↔ s = t

@[simp]

theorem String.toByteArray_ofList {l : List Char} : (ofList l).toByteArray = l.utf8Encode

@[deprecated String.toByteArray_ofList (since := "2025-10-30")]

theorem List.toByteArray_asString {l : List Char} : (String.ofList l).toByteArray = l.utf8Encode

theorem String.exists_eq_ofList (s : String) : ∃ (l : List Char), s = ofList l

@[deprecated String.exists_eq_ofList (since := "2025-10-30")]

theorem String.exists_eq_asString (s : String) : ∃ (l : List Char), s = ofList l

@[simp]

theorem String.utf8ByteSize_empty : "".utf8ByteSize = 0

@[simp]

theorem String.utf8ByteSize_append {s t : String} : (s ++ t).utf8ByteSize = s.utf8ByteSize + t.utf8ByteSize

@[simp]

theorem String.size_toByteArray {s : String} : s.toByteArray.size = s.utf8ByteSize

@[simp]

theorem String.toByteArray_push {s : String} {c : Char} : (s.push c).toByteArray = s.toByteArray ++ [c].utf8Encode

def String.rawStartPos (_s : String) : Pos.Raw

The start position of the string, as a String.Pos.Raw.

@[simp]

theorem String.rawStartPos_eq {s : String} : s.rawStartPos = 0

@[simp]

theorem String.byteIdx_rawEndPos {s : String} : s.rawEndPos.byteIdx = s.utf8ByteSize

@[deprecated String.byteIdx_rawEndPos (since := "2025-10-20")]

theorem String.byteIdx_endPos {s : String} : s.rawEndPos.byteIdx = s.utf8ByteSize

@[simp]

theorem String.utf8ByteSize_ofByteArray {b : ByteArray} {h : b.IsValidUTF8} : { toByteArray := b, isValidUTF8 := h }.utf8ByteSize = b.size

@[simp]

theorem String.toByteArray_singleton {c : Char} : (singleton c).toByteArray = [c].utf8Encode

theorem String.singleton_eq_ofList {c : Char} : singleton c = ofList [c]

@[deprecated String.singleton_eq_ofList (since := "2025-10-30")]

theorem String.singleton_eq_asString {c : Char} : singleton c = ofList [c]

@[simp]

theorem String.append_singleton {s : String} {c : Char} : s ++ singleton c = s.push c

@[simp]

theorem String.append_left_inj {s₁ s₂ : String} (t : String) : s₁ ++ t = s₂ ++ t ↔ s₁ = s₂

@[simp]

theorem String.append_right_inj (s : String) {t₁ t₂ : String} : s ++ t₁ = s ++ t₂ ↔ t₁ = t₂

theorem String.append_assoc {s₁ s₂ s₃ : String} : s₁ ++ s₂ ++ s₃ = s₁ ++ (s₂ ++ s₃)

@[simp]

theorem String.utf8ByteSize_eq_zero_iff {s : String} : s.utf8ByteSize = 0 ↔ s = ""

theorem String.rawEndPos_eq_zero_iff {b : String} : b.rawEndPos = 0 ↔ b = ""

@[deprecated String.rawEndPos_eq_zero_iff (since := "2025-10-20")]

theorem String.endPos_eq_zero_iff {b : String} : b.rawEndPos = 0 ↔ b = ""

@[inline]

def String.pushn (s : String) (c : Char) (n : Nat) : String

Adds multiple repetitions of a character to the end of a string.

Returns s, with n repetitions of c at the end. Internally, the implementation repeatedly calls String.push, so the string is modified in-place if there is a unique reference to it.

Examples:

• "indeed".pushn '!' 2 = "indeed!!"
• "indeed".pushn '!' 0 = "indeed"
• "".pushn ' ' 4 = " "

theorem String.pushn_eq_repeat_push {s : String} {c : Char} {n : Nat} : s.pushn c n = Nat.repeat (fun (s : String) => s.push c) n s

@[export lean_string_pushn]

def String.Internal.pushnImpl (s : String) (c : Char) (n : Nat) : String

@[inline]

def String.isEmpty (s : String) : Bool

Checks whether a string is empty.

Empty strings are equal to "" and have length and end position 0.

Examples:

• "".isEmpty = true
• "empty".isEmpty = false
• " ".isEmpty = false

@[export lean_string_isempty]

def String.Internal.isEmptyImpl (s : String) : Bool

@[inline]

def String.join (l : List String) : String

Appends all the strings in a list of strings, in order.

Use String.intercalate to place a separator string between the strings in a list.

Examples:

• String.join ["gr", "ee", "n"] = "green"
• String.join ["b", "", "l", "", "ue"] = "blue"
• String.join [] = ""

def String.intercalate (s : String) : List String → String

Appends the strings in a list of strings, placing the separator s between each pair.

Examples:

• ", ".intercalate ["red", "green", "blue"] = "red, green, blue"
• " and ".intercalate ["tea", "coffee"] = "tea and coffee"
• " | ".intercalate ["M", "", "N"] = "M | | N"

@[export lean_string_intercalate]

def String.Internal.intercalateImpl (s : String) : List String → String

structure String.Pos.Raw.IsValid (s : String) (off : Raw) : Prop

Predicate for validity of positions inside a String.

There are multiple equivalent definitions for validity.

We say that a position is valid if the string obtained by taking all of the bytes up to, but excluding, the given position, is valid UTF-8; see Pos.isValid_iff_isValidUTF8_extract_zero.

Similarly, a position is valid if the string obtained by taking all of the bytes starting at the given position is valid UTF-8; see Pos.isValid_iff_isValidUTF8_extract_utf8ByteSize.

An equivalent condition is that the position is the length of the UTF-8 encoding of some prefix of the characters of the string; see Pos.isValid_iff_exists_append and Pos.isValid_iff_exists_take_data.

Another equivalent condition that can be checked efficiently is that the position is either the end position or strictly smaller than the end position and the byte at the position satisfies UInt8.IsUTF8FirstByte; see Pos.isValid_iff_isUTF8FirstByte.

Examples:

• String.Pos.IsValid "abc" ⟨0⟩
• String.Pos.IsValid "abc" ⟨1⟩
• String.Pos.IsValid "abc" ⟨3⟩
• ¬ String.Pos.IsValid "abc" ⟨4⟩
• String.Pos.IsValid "𝒫(A)" ⟨0⟩
• ¬ String.Pos.IsValid "𝒫(A)" ⟨1⟩
• ¬ String.Pos.IsValid "𝒫(A)" ⟨2⟩
• ¬ String.Pos.IsValid "𝒫(A)" ⟨3⟩
• String.Pos.IsValid "𝒫(A)" ⟨4⟩

• le_rawEndPos : off ≤ s.rawEndPos
• isValidUTF8_extract_zero : (s.toByteArray.extract 0 off.byteIdx).IsValidUTF8

theorem String.Pos.Raw.IsValid.le_utf8ByteSize {s : String} {off : Raw} (h : IsValid s off) : off.byteIdx ≤ s.utf8ByteSize

theorem String.Pos.Raw.isValid_iff_isValidUTF8_extract_zero {s : String} {p : Raw} : IsValid s p ↔ p ≤ s.rawEndPos ∧ (s.toByteArray.extract 0 p.byteIdx).IsValidUTF8

@[deprecated String.Pos.Raw.IsValid.le_rawEndPos (since := "2025-10-20")]

theorem String.Pos.Raw.IsValid.le_endPos {s : String} {off : Raw} (h : IsValid s off) : off ≤ s.rawEndPos

@[simp]

theorem String.Pos.Raw.isValid_zero {s : String} : IsValid s 0

@[simp]

theorem String.Pos.Raw.isValid_rawEndPos {s : String} : IsValid s s.rawEndPos

theorem String.Pos.Raw.isValid_of_eq_rawEndPos {s : String} {p : Raw} (h : p = s.rawEndPos) : IsValid s p

@[simp]

theorem String.Pos.Raw.isValid_empty_iff {p : Raw} : IsValid "" p ↔ p = 0

structure String.Pos (s : String) : Type

A Pos s is a byte offset in s together with a proof that this position is at a UTF-8 character boundary.

• offset : Raw

  The underlying byte offset of the Pos.

• isValid : Raw.IsValid s self.offset

  The proof that offset is valid for the string s.

theorem String.Pos.ext_iff {s : String} {x y : s.Pos} : x = y ↔ x.offset = y.offset

theorem String.Pos.ext {s : String} {x y : s.Pos} (offset : x.offset = y.offset) : x = y

def String.instDecidableEqPos.decEq {s✝ : String} (x✝ x✝¹ : s✝.Pos) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance String.instDecidableEqPos {s✝ : String} : DecidableEq s✝.Pos

@[inline]

def String.startPos (s : String) : s.Pos

The start position of s, as an s.Pos.

@[simp]

theorem String.offset_startPos {s : String} : s.startPos.offset = 0

@[implicit_reducible]

instance String.instInhabitedPos {s : String} : Inhabited s.Pos

@[inline]

def String.endPos (s : String) : s.Pos

The past-the-end position of s, as an s.Pos.

@[simp]

theorem String.offset_endPos {s : String} : s.endPos.offset = s.rawEndPos

@[implicit_reducible]

instance String.instLEPos {s : String} : LE s.Pos

@[implicit_reducible]

instance String.instLTPos {s : String} : LT s.Pos

theorem String.Pos.le_iff {s : String} {l r : s.Pos} : l ≤ r ↔ l.offset ≤ r.offset

theorem String.Pos.lt_iff {s : String} {l r : s.Pos} : l < r ↔ l.offset < r.offset

@[implicit_reducible]

instance String.instDecidableLePos {s : String} (l r : s.Pos) : Decidable (l ≤ r)

@[implicit_reducible]

instance String.instDecidableLtPos {s : String} (l r : s.Pos) : Decidable (l < r)

structure String.Slice : Type

A region or slice of some underlying string.

A slice consists of a string together with the start and end byte positions of a region of interest. Actually extracting a substring requires copying and memory allocation, while many slices of the same underlying string may exist with very little overhead. While this could be achieved by tracking the bounds by hand, the slice API is much more convenient.

String.Slice bundles proofs to ensure that the start and end positions always delineate a valid string. For this reason, it should be preferred over Substring.Raw.

• str : String

  The underlying strings.

• startInclusive : self.str.Pos

  The byte position of the start of the string slice.

• endExclusive : self.str.Pos

  The byte position of the end of the string slice.

• startInclusive_le_endExclusive : self.startInclusive ≤ self.endExclusive

  The slice is not degenerate (but it may be empty).

theorem String.Slice.ext {x y : Slice} (str : x.str = y.str) (startInclusive : x.startInclusive ≍ y.startInclusive) (endExclusive : x.endExclusive ≍ y.endExclusive) : x = y

theorem String.Slice.ext_iff {x y : Slice} : x = y ↔ x.str = y.str ∧ x.startInclusive ≍ y.startInclusive ∧ x.endExclusive ≍ y.endExclusive

@[implicit_reducible]

instance String.instInhabitedSlice : Inhabited Slice

@[inline]

def String.toSlice (s : String) : Slice

Returns a slice that contains the entire string.

@[implicit_reducible]

instance String.instCoeSlice : Coe String Slice

@[simp]

theorem String.startInclusive_toSlice {s : String} : s.toSlice.startInclusive = s.startPos

@[simp]

theorem String.endExclusive_toSlice {s : String} : s.toSlice.endExclusive = s.endPos

@[simp]

theorem String.str_toSlice {s : String} : s.toSlice.str = s

@[inline]

def String.Slice.utf8ByteSize (s : Slice) : Nat

The number of bytes of the UTF-8 encoding of the string slice.

theorem String.Slice.utf8ByteSize_eq {s : Slice} : s.utf8ByteSize = s.endExclusive.offset.byteIdx - s.startInclusive.offset.byteIdx

@[implicit_reducible]

instance String.instHAddRawSlice : HAdd Pos.Raw Slice Pos.Raw

@[implicit_reducible]

instance String.instHAddSliceRaw : HAdd Slice Pos.Raw Pos.Raw

@[implicit_reducible]

instance String.instHSubRawSlice : HSub Pos.Raw Slice Pos.Raw

@[simp]

theorem String.Pos.Raw.byteIdx_add_slide {p : Raw} {s : Slice} : (p + s).byteIdx = p.byteIdx + s.utf8ByteSize

@[simp]

theorem String.Pos.Raw.byteIdx_slice_add {s : Slice} {p : Raw} : (s + p).byteIdx = s.utf8ByteSize + p.byteIdx

@[simp]

theorem String.Pos.Raw.byteIdx_sub_slice {p : Raw} {s : Slice} : (p - s).byteIdx = p.byteIdx - s.utf8ByteSize

@[inline]

def String.Slice.rawEndPos (s : Slice) : Pos.Raw

The end position of a slice, as a Pos.Raw.

@[simp]

theorem String.Slice.byteIdx_rawEndPos {s : Slice} : s.rawEndPos.byteIdx = s.utf8ByteSize

structure String.Pos.Raw.IsValidForSlice (s : Slice) (p : Raw) : Prop

Criterion for validity of positions in string slices.

• le_rawEndPos : p ≤ s.rawEndPos
• isValid_offsetBy : IsValid s.str (p.offsetBy s.startInclusive.offset)

theorem String.Pos.Raw.IsValidForSlice.le_utf8ByteSize {s : Slice} {p : Raw} (h : IsValidForSlice s p) : p.byteIdx ≤ s.utf8ByteSize

@[inline]

def String.Slice.getUTF8Byte (s : Slice) (p : Pos.Raw) (h : p < s.rawEndPos) : UInt8

Accesses the indicated byte in the UTF-8 encoding of a string slice.

At runtime, this function is implemented by efficient, constant-time code.

def String.Slice.getUTF8Byte! (s : Slice) (p : Pos.Raw) : UInt8

Accesses the indicated byte in the UTF-8 encoding of the string slice, or panics if the position is out-of-bounds.

structure String.Slice.Pos (s : Slice) : Type

A Slice.Pos s is a byte offset in s together with a proof that this position is at a UTF-8 character boundary.

• offset : Pos.Raw

  The underlying byte offset of the Slice.Pos.

• isValidForSlice : Pos.Raw.IsValidForSlice s self.offset

  The proof that offset is valid for the string slice s.

theorem String.Slice.Pos.ext {s : Slice} {x y : s.Pos} (offset : x.offset = y.offset) : x = y

theorem String.Slice.Pos.ext_iff {s : Slice} {x y : s.Pos} : x = y ↔ x.offset = y.offset

@[implicit_reducible]

instance String.Slice.instDecidableEqPos {s✝ : Slice} : DecidableEq s✝.Pos

def String.Slice.instDecidableEqPos.decEq {s✝ : Slice} (x✝ x✝¹ : s✝.Pos) : Decidable (x✝ = x✝¹)

@[inline]

def String.Slice.startPos (s : Slice) : s.Pos

The start position of s, as an s.Pos.

@[simp]

theorem String.Slice.offset_startPos {s : Slice} : s.startPos.offset = 0

@[implicit_reducible]

instance String.instInhabitedPos_1 {s : Slice} : Inhabited s.Pos

@[simp]

theorem String.Slice.offset_startInclusive_add_self {s : Slice} : s.startInclusive.offset + s = s.endExclusive.offset

@[simp]

theorem String.Pos.Raw.offsetBy_rawEndPos_left {p : Raw} {s : String} : s.rawEndPos.offsetBy p = p + s

@[simp]

theorem String.Pos.Raw.offsetBy_rawEndPos_right {p : Raw} {s : String} : p.offsetBy s.rawEndPos = s + p

@[simp]

theorem String.Pos.Raw.offsetBy_sliceRawEndPos_left {p : Raw} {s : Slice} : s.rawEndPos.offsetBy p = p + s

@[simp]

theorem String.Pos.Raw.offsetBy_sliceRawEndPos_right {p : Raw} {s : Slice} : p.offsetBy s.rawEndPos = s + p

@[simp]

theorem String.Pos.Raw.isValidForSlice_rawEndPos {s : Slice} : IsValidForSlice s s.rawEndPos

theorem String.Pos.Raw.isValidForSlice_of_eq_rawEndPos {p : Raw} {s : Slice} (h : p = s.rawEndPos) : IsValidForSlice s p

@[inline]

def String.Slice.endPos (s : Slice) : s.Pos

The past-the-end position of s, as an s.Pos.

@[simp]

theorem String.Slice.offset_endPos {s : Slice} : s.endPos.offset = s.rawEndPos

@[implicit_reducible]

instance String.instLEPos_1 {s : Slice} : LE s.Pos

@[implicit_reducible]

instance String.instLTPos_1 {s : Slice} : LT s.Pos

theorem String.Slice.Pos.le_iff {s : Slice} {l r : s.Pos} : l ≤ r ↔ l.offset ≤ r.offset

theorem String.Slice.Pos.lt_iff {s : Slice} {l r : s.Pos} : l < r ↔ l.offset < r.offset

@[implicit_reducible]

instance String.instDecidableLePos_1 {s : Slice} (l r : s.Pos) : Decidable (l ≤ r)

@[implicit_reducible]

instance String.instDecidableLtPos_1 {s : Slice} (l r : s.Pos) : Decidable (l < r)

@[reducible, inline]

abbrev String.Pos.IsAtEnd {s : String} (pos : s.Pos) : Prop

pos.IsAtEnd is just shorthand for pos = s.endPos that is easier to write if s is long.

@[simp]

theorem String.Pos.isAtEnd_iff {s : String} {pos : s.Pos} : pos.IsAtEnd ↔ pos = s.endPos

@[implicit_reducible, inline]

instance String.instDecidableIsAtEnd {s : String} {pos : s.Pos} : Decidable pos.IsAtEnd

@[reducible, inline]

abbrev String.Slice.Pos.IsAtEnd {s : Slice} (pos : s.Pos) : Prop

pos.IsAtEnd is just shorthand for pos = s.endPos that is easier to write if s is long.

@[simp]

theorem String.Slice.Pos.isAtEnd_iff {s : Slice} {pos : s.Pos} : pos.IsAtEnd ↔ pos = s.endPos

@[implicit_reducible, inline]

instance String.instDecidableIsAtEnd_1 {s : Slice} {pos : s.Pos} : Decidable pos.IsAtEnd

@[inline]

def String.Slice.Pos.byte {s : Slice} (pos : s.Pos) (h : pos ≠ s.endPos) : UInt8

Returns the byte at a position in a slice that is not the end position.

@[simp]

theorem String.default_eq : default = ""

theorem String.push_eq_append {s : String} (c : Char) : s.push c = s ++ singleton c

@[inline]

def String.Slice.isEmpty (s : Slice) : Bool

Checks whether a slice is empty.

Empty slices have {name}utf8ByteSize {lean}0.

Examples:

• {lean}"".toSlice.isEmpty = true
• {lean}" ".toSlice.isEmpty = false

@[simp]

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

theorem String.Slice.Pos.lt_trans {s : Slice} {p q r : s.Pos} : p < q → q < r → p < r

@[simp]

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

theorem String.Pos.lt_trans {s : String} {p q r : s.Pos} : p < q → q < r → p < r

@[deprecated String.toRawSubstring (since := "2025-11-18")]

def String.toSubstring (s : String) : Substring.Raw

@[deprecated String.toRawSubstring' (since := "2025-11-18")]

def String.toSubstring' (s : String) : Substring.Raw

@[reducible, inline, deprecated String.Pos (since := "2025-11-24")]

abbrev String.ValidPos (s : String) : Type

@[reducible, inline, deprecated String.startPos (since := "2025-11-24")]

abbrev String.startValidPos (s : String) : s.Pos

@[reducible, inline, deprecated String.endPos (since := "2025-11-24")]

abbrev String.endValidPos (s : String) : s.Pos

@[reducible, inline, deprecated String.toByteArray (since := "2025-11-24")]

abbrev String.String.bytes (s : String) : ByteArray