Arithmetic of String.Pos.Raw

This file contains basic theory about which does not actually need to know anything about strings and therefore does not depend on Init.Data.String.Decode.

theorem String.Pos.Raw.ext_iff {x y : Raw} : x = y ↔ x.byteIdx = y.byteIdx

theorem String.Pos.Raw.ext {x y : Raw} (byteIdx : x.byteIdx = y.byteIdx) : x = y

instance String.instHSubRaw : HSub Pos.Raw String Pos.Raw

Equations

• String.instHSubRaw = { hSub := fun (p : String.Pos.Raw) (s : String) => { byteIdx := p.byteIdx - s.utf8ByteSize } }

instance String.instHSubRawChar : HSub Pos.Raw Char Pos.Raw

Equations

• String.instHSubRawChar = { hSub := fun (p : String.Pos.Raw) (c : Char) => { byteIdx := p.byteIdx - c.utf8Size } }

@[export lean_string_pos_sub]

def String.Pos.Internal.subImpl : Raw → Raw → Raw

Equations

• String.Pos.Internal.subImpl p₁ p₂ = { byteIdx := p₁.byteIdx - p₂.byteIdx }

instance String.instHAddRawChar : HAdd Pos.Raw Char Pos.Raw

Equations

• String.instHAddRawChar = { hAdd := fun (p : String.Pos.Raw) (c : Char) => { byteIdx := p.byteIdx + c.utf8Size } }

instance String.instHAddCharRaw : HAdd Char Pos.Raw Pos.Raw

Equations

• String.instHAddCharRaw = { hAdd := fun (c : Char) (p : String.Pos.Raw) => { byteIdx := c.utf8Size + p.byteIdx } }

instance String.instHAddRaw : HAdd String Pos.Raw Pos.Raw

Equations

• String.instHAddRaw = { hAdd := fun (s : String) (p : String.Pos.Raw) => { byteIdx := s.utf8ByteSize + p.byteIdx } }

instance String.instHAddRaw_1 : HAdd Pos.Raw String Pos.Raw

Equations

• String.instHAddRaw_1 = { hAdd := fun (p : String.Pos.Raw) (s : String) => { byteIdx := p.byteIdx + s.utf8ByteSize } }

instance String.instLERaw : LE Pos.Raw

Equations

• String.instLERaw = { le := fun (p₁ p₂ : String.Pos.Raw) => p₁.byteIdx ≤ p₂.byteIdx }

instance String.instLTRaw : LT Pos.Raw

Equations

• String.instLTRaw = { lt := fun (p₁ p₂ : String.Pos.Raw) => p₁.byteIdx < p₂.byteIdx }

instance String.instDecidableLeRaw (p₁ p₂ : Pos.Raw) : Decidable (p₁ ≤ p₂)

Equations

• String.instDecidableLeRaw p₁ p₂ = inferInstanceAs (Decidable (p₁.byteIdx ≤ p₂.byteIdx))

instance String.instDecidableLtRaw (p₁ p₂ : Pos.Raw) : Decidable (p₁ < p₂)

Equations

• String.instDecidableLtRaw p₁ p₂ = inferInstanceAs (Decidable (p₁.byteIdx < p₂.byteIdx))

instance String.instMinRaw : Min Pos.Raw

Equations

• String.instMinRaw = minOfLe

instance String.instMaxRaw : Max Pos.Raw

Equations

• String.instMaxRaw = maxOfLe

@[simp]

theorem String.Pos.Raw.byteIdx_sub_char {p : Raw} {c : Char} : (p - c).byteIdx = p.byteIdx - c.utf8Size

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem String.Pos.Raw.byteIdx_add_char {p : Raw} {c : Char} : (p + c).byteIdx = p.byteIdx + c.utf8Size

@[simp]

theorem String.Pos.Raw.byteIdx_char_add {c : Char} {p : Raw} : (c + p).byteIdx = c.utf8Size + p.byteIdx

theorem String.Pos.Raw.le_iff {i₁ i₂ : Raw} : i₁ ≤ i₂ ↔ i₁.byteIdx ≤ i₂.byteIdx

theorem String.Pos.Raw.lt_iff {i₁ i₂ : Raw} : i₁ < i₂ ↔ i₁.byteIdx < i₂.byteIdx

@[simp]

theorem String.Pos.Raw.byteIdx_zero : byteIdx 0 = 0

@[inline]

def String.Pos.Raw.byteDistance (lo hi : Raw) : Nat

Returns the size of the byte slice delineated by the positions lo and hi.

Equations

• lo.byteDistance hi = hi.byteIdx - lo.byteIdx

theorem String.Pos.Raw.byteDistance_eq {lo hi : Raw} : lo.byteDistance hi = hi.byteIdx - lo.byteIdx

@[simp]

theorem String.rawEndPos_empty : "".rawEndPos = 0

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

theorem String.endPos_empty : "".rawEndPos = 0

@[extern lean_string_get_byte_fast]

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

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

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

Equations

• s.getUTF8Byte p h = s.bytes[p.byteIdx]

@[reducible, inline, extern lean_string_get_byte_fast, deprecated String.getUTF8Byte (since := "2025-10-01")]

abbrev String.getUtf8Byte (s : String) (p : Pos.Raw) (h : p < s.rawEndPos) : UInt8

Equations

• s.getUtf8Byte p h = s.getUTF8Byte p h

theorem String.Pos.Raw.le_trans {a b c : Raw} : a ≤ b → b ≤ c → a ≤ c

theorem String.Pos.Raw.lt_of_lt_of_le {a b c : Raw} : a < b → b ≤ c → a < c

@[inline]

def String.Pos.Raw.offsetBy (p offset : Raw) : Raw

Offsets p by offset on the left. This is not an HAdd instance because it should be a relatively rare operation, so we use a name to make accidental use less likely. To offset a position by the size of a character character c or string s, you can use c + p resp. s + p.

This should be seen as an operation that converts relative positions into absolute positions.

See also Pos.Raw.increaseBy, which is an "advancing" operation.

Equations

• p.offsetBy offset = { byteIdx := offset.byteIdx + p.byteIdx }

@[simp]

theorem String.Pos.Raw.byteIdx_offsetBy {p offset : Raw} : (p.offsetBy offset).byteIdx = offset.byteIdx + p.byteIdx

theorem String.Pos.Raw.offsetBy_assoc {p q r : Raw} : (p.offsetBy q).offsetBy r = p.offsetBy (q.offsetBy r)

@[simp]

theorem String.Pos.Raw.offsetBy_zero_left {p : Raw} : offsetBy 0 p = p

@[inline]

def String.Pos.Raw.unoffsetBy (p offset : Raw) : Raw

Decreases p by offset. This is not an HSub instance because it should be a relatively rare operation, so we use a name to make accidental use less likely. To unoffset a position by the size of a character c or string s, you can use p - c resp. p - s.

This should be seen as an operation that converts absolute positions into relative positions.

See also Pos.Raw.decreaseBy, which is an "unadvancing" operation.

Equations

• p.unoffsetBy offset = { byteIdx := p.byteIdx - offset.byteIdx }

@[simp]

theorem String.Pos.Raw.byteIdx_unoffsetBy {p offset : Raw} : (p.unoffsetBy offset).byteIdx = p.byteIdx - offset.byteIdx

theorem String.Pos.Raw.offsetBy_unoffsetBy_of_le {p q : Raw} (h : q ≤ p) : (p.unoffsetBy q).offsetBy q = p

@[simp]

theorem String.Pos.Raw.unoffsetBy_offsetBy {p q : Raw} : (p.offsetBy q).unoffsetBy q = p

@[simp]

theorem String.Pos.Raw.eq_zero_iff {p : Raw} : p = 0 ↔ p.byteIdx = 0

@[inline]

def String.Pos.Raw.increaseBy (p : Raw) (n : Nat) : Raw

Advances p by n bytes. This is not an HAdd instance because it should be a relatively rare operation, so we use a name to make accidental use less likely. To add the size of a character c or string s to a raw position p, you can use p + c resp. p + s.

This should be seen as an "advance" or "skip".

See also Pos.Raw.offsetBy, which turns relative positions into absolute positions.

Equations

• p.increaseBy n = { byteIdx := p.byteIdx + n }

@[simp]

theorem String.Pos.Raw.byteIdx_increaseBy {p : Raw} {n : Nat} : (p.increaseBy n).byteIdx = p.byteIdx + n

@[inline]

def String.Pos.Raw.decreaseBy (p : Raw) (n : Nat) : Raw

Move the position p back by n bytes. This is not an HSub instance because it should be a relatively rare operation, so we use a name to make accidental use less likely. To remove the size of a character c or string s from a raw position p, you can use p - c resp. p - s.

This should be seen as the inverse of an "advance" or "skip".

See also Pos.Raw.unoffsetBy, which turns absolute positions into relative positions.

Equations

• p.decreaseBy n = { byteIdx := p.byteIdx - n }

@[simp]

theorem String.Pos.Raw.byteIdx_decreaseBy {p : Raw} {n : Nat} : (p.decreaseBy n).byteIdx = p.byteIdx - n

theorem String.Pos.Raw.increaseBy_charUtf8Size {p : Raw} {c : Char} : p.increaseBy c.utf8Size = p + c

@[inline]

def String.Pos.Raw.inc (p : Raw) : Raw

Increases the byte offset of the position by 1. Not to be confused with ValidPos.next.

Equations

• p.inc = { byteIdx := p.byteIdx + 1 }

@[simp]

theorem String.Pos.Raw.byteIdx_inc {p : Raw} : p.inc.byteIdx = p.byteIdx + 1

@[inline]

def String.Pos.Raw.dec (p : Raw) : Raw

Decreases the byte offset of the position by 1. Not to be confused with ValidPos.prev.

Equations

• p.dec = { byteIdx := p.byteIdx - 1 }

@[simp]

theorem String.Pos.Raw.byteIdx_dec {p : Raw} : p.dec.byteIdx = p.byteIdx - 1

@[simp]

theorem String.Pos.Raw.le_refl {p : Raw} : p ≤ p

theorem String.Pos.Raw.lt_inc {p : Raw} : p < p.inc

theorem String.Pos.Raw.le_of_lt {p q : Raw} : p < q → p ≤ q

theorem String.Pos.Raw.inc_le {p q : Raw} : p.inc ≤ q ↔ p < q

theorem String.Pos.Raw.lt_of_le_of_lt {a b c : Raw} : a ≤ b → b < c → a < c

theorem String.Pos.Raw.ne_of_lt {a b : Raw} : a < b → a ≠ b

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

theorem String.pos_lt_eq (p₁ p₂ : Pos.Raw) : (p₁ < p₂) = (p₁.byteIdx < p₂.byteIdx)

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

theorem String.pos_add_char (p : Pos.Raw) (c : Char) : (p + c).byteIdx = p.byteIdx + c.utf8Size

theorem String.Pos.Raw.ne_zero_of_lt {a b : Raw} : a < b → b ≠ 0

@[reducible, inline]

abbrev String.Pos.Raw.min (p₁ p₂ : Raw) : Raw

Returns either p₁ or p₂, whichever has the least byte index.

Equations

• p₁.min p₂ = { byteIdx := p₁.byteIdx.min p₂.byteIdx }

@[export lean_string_pos_min]

def String.Pos.Raw.Internal.minImpl (p₁ p₂ : Raw) : Raw

Equations

• String.Pos.Raw.Internal.minImpl p₁ p₂ = p₁.min p₂

theorem String.Pos.Raw.byteIdx_mk (n : Nat) : { byteIdx := n }.byteIdx = n

@[simp]

theorem String.Pos.Raw.mk_zero : { } = 0

@[simp]

theorem String.Pos.Raw.mk_byteIdx (p : Raw) : { byteIdx := p.byteIdx } = p

@[deprecated String.Pos.Raw.byteIdx_offsetBy (since := "2025-10-08")]

theorem String.Pos.Raw.add_byteIdx {p₁ p₂ : Raw} : (p₂.offsetBy p₁).byteIdx = p₁.byteIdx + p₂.byteIdx

@[deprecated String.Pos.Raw.byteIdx_offsetBy (since := "2025-10-08")]

theorem String.Pos.Raw.add_eq {p₁ p₂ : Raw} : p₂.offsetBy p₁ = { byteIdx := p₁.byteIdx + p₂.byteIdx }

@[deprecated String.Pos.Raw.byteIdx_unoffsetBy (since := "2025-10-08")]

theorem String.Pos.Raw.sub_byteIdx (p₁ p₂ : Raw) : (p₁.unoffsetBy p₂).byteIdx = p₁.byteIdx - p₂.byteIdx

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

theorem String.Pos.Raw.addChar_byteIdx (p : Raw) (c : Char) : (p + c).byteIdx = p.byteIdx + c.utf8Size

theorem String.Pos.Raw.add_char_eq (p : Raw) (c : Char) : p + c = { byteIdx := p.byteIdx + c.utf8Size }

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

theorem String.Pos.Raw.addChar_eq (p : Raw) (c : Char) : p + c = { byteIdx := p.byteIdx + c.utf8Size }

theorem String.Pos.Raw.byteIdx_zero_add_char (c : Char) : (0 + c).byteIdx = c.utf8Size

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

theorem String.Pos.Raw.zero_addChar_byteIdx (c : Char) : (0 + c).byteIdx = c.utf8Size

theorem String.Pos.Raw.zero_add_char_eq (c : Char) : 0 + c = { byteIdx := c.utf8Size }

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

theorem String.Pos.Raw.zero_addChar_eq (c : Char) : 0 + c = { byteIdx := c.utf8Size }

theorem String.Pos.Raw.add_char_right_comm (p : Raw) (c₁ c₂ : Char) : p + c₁ + c₂ = p + c₂ + c₁

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

theorem String.Pos.Raw.addChar_right_comm (p : Raw) (c₁ c₂ : Char) : p + c₁ + c₂ = p + c₂ + c₁

theorem String.Pos.Raw.ne_of_gt {i₁ i₂ : Raw} (h : i₁ < i₂) : i₂ ≠ i₁

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

theorem String.Pos.Raw.byteIdx_addString (p : Raw) (s : String) : (p + s).byteIdx = p.byteIdx + s.utf8ByteSize

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

theorem String.Pos.Raw.byteIdx_zero_add_string (s : String) : (0 + s).byteIdx = s.utf8ByteSize

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

theorem String.Pos.Raw.byteIdx_zero_addString (s : String) : (0 + s).byteIdx = s.utf8ByteSize

theorem String.Pos.Raw.zero_add_string_eq (s : String) : 0 + s = { byteIdx := s.utf8ByteSize }

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

theorem String.Pos.Raw.zero_addString_eq (s : String) : 0 + s = { byteIdx := s.utf8ByteSize }

@[simp]

theorem String.Pos.Raw.mk_le_mk {i₁ i₂ : Nat} : { byteIdx := i₁ } ≤ { byteIdx := i₂ } ↔ i₁ ≤ i₂

@[simp]

theorem String.Pos.Raw.mk_lt_mk {i₁ i₂ : Nat} : { byteIdx := i₁ } < { byteIdx := i₂ } ↔ i₁ < i₂