Substring.ValidFor.bsize
theorem Substring.ValidFor.bsize :
∀ {l m r : List Char} {s : Substring}, Substring.ValidFor l m r s → s.bsize = String.utf8Len m
The theorem `Substring.ValidFor.bsize` states that for any three lists of characters `l`, `m`, `r` and any substring `s`, if the substring `s` is valid for the concatenation of the lists `l`, `m` and `r` (meaning that `s` is a substring of the string formed by concatenating `l`, `m`, and `r`), then the byte length of the substring `s` (as calculated by the function `Substring.bsize`) is equal to the UTF-8 byte length of the list of characters `m` (as calculated by the function `String.utf8Len`). This theorem essentially establishes a relationship between the byte length of a valid substring and the UTF-8 byte length of a segment of the original string.
More concisely: For any lists of characters `l`, `m`, `r`, and substring `s`, if `s` is a valid substring of the concatenation of `l`, `m`, and `r`, then `Substring.bsize s = String.utf8Len m`.
|
Substring.ValidFor.any
theorem Substring.ValidFor.any :
∀ {l m r : List Char} (f : Char → Bool) {s : Substring}, Substring.ValidFor l m r s → s.any f = m.any f
The theorem `Substring.ValidFor.any` states that for any lists of characters `l`, `m`, `r`, a function `f` from characters to Booleans, and a substring `s` which is valid for these lists, the application of the function `f` if it ever returns `true` for any character in the substring `s` is equivalent to the application of the function `f` if it ever returns `true` for any character in the list `m`. In other words, checking if there's any character in the substring `s` that makes the function `f` return `true` is the same as checking this condition in the list `m` where the substring `s` is valid for `l`, `m`, `r`.
More concisely: For any lists of characters `l`, `m`, substring `s` valid for `l`, `m`, and function `f` from characters to Booleans, if `s` contains a character making `f` return `true`, then `m` contains such a character.
|
Substring.ValidFor.of_eq
theorem Substring.ValidFor.of_eq :
∀ {l m r : List Char} (s : Substring),
s.str.data = l ++ m ++ r →
s.startPos.byteIdx = String.utf8Len l →
s.stopPos.byteIdx = String.utf8Len l + String.utf8Len m → Substring.ValidFor l m r s
This theorem states that for any three lists of characters `l`, `m`, and `r`, and any substring `s`, if the data of the substring `s` is equal to the concatenation of `l`, `m`, and `r`, and the starting byte index of `s` is equal to the UTF-8 byte length of `l`, and the stopping byte index of `s` is equal to the sum of the UTF-8 byte length of `l` and the UTF-8 byte length of `m`, then `s` is a valid substring for the lists `l`, `m`, and `r`. This essentially is a condition for the validity of a substring based on its byte indices and the byte lengths of certain lists of characters.
More concisely: For lists of characters `l`, `m`, and `r`, and substring `s` with data equal to `l ++ m ++ r`, starting index equal to the UTF-8 byte length of `l`, and stopping index equal to the sum of the UTF-8 byte lengths of `l` and `m`, `s` is a valid substring of the concatenation of `l` and `r`.
|
Substring.Valid.validFor
theorem Substring.Valid.validFor : ∀ {s : Substring}, s.Valid → ∃ l m r, Substring.ValidFor l m r s
This theorem states that for every substring 's', if 's' is valid, then there exist strings 'l', 'm', and 'r' such that 's' is valid for the concatenation of 'l', 'm', and 'r'. In other words, any valid substring must be part of some valid concatenation of three other strings.
More concisely: For every valid string `s`, there exist strings `l`, `m`, and `r` such that `l & m & r = s` holds, where `&` denotes string concatenation.
|
Substring.ValidFor.startPos
theorem Substring.ValidFor.startPos :
∀ {l m r : List Char} {s : Substring}, Substring.ValidFor l m r s → s.startPos = { byteIdx := String.utf8Len l }
This theorem, named `Substring.ValidFor.startPos`, states that for any lists of characters `l`, `m`, and `r`, and any `Substring` `s`, if `s` is valid for the concatenation of `l`, `m`, and `r`, then the starting position of the substring `s` is equal to the UTF-8 byte length of the list `l`. In other words, the start of the substring is positioned right after the list of characters `l` when `l`, `m`, and `r` are concatenated.
More concisely: Given lists of characters `l`, `m`, and `r`, and a valid substring `s` of their concatenation, the starting position of `s` equals the length of `l` in UTF-8 bytes.
|
Substring.Valid.le
theorem Substring.Valid.le : ∀ {s : Substring}, s.Valid → s.startPos ≤ s.stopPos
This theorem states that for any substring `s`, if `s` is valid, then the start position of `s` (represented as `s.startPos`) is less than or equal to the stop position of `s` (represented as `s.stopPos`). This means that the point where a substring begins in a string is always at the same or an earlier position compared to where it ends, which aligns with the intuitive understanding of a substring.
More concisely: For any substring `s` in a string, `s.startPos` is less than or equal to `s.stopPos`.
|
Substring.Valid.stopValid
theorem Substring.Valid.stopValid : ∀ {s : Substring}, s.Valid → String.Pos.Valid s.str s.stopPos
This theorem states that for any given substring, if the substring is valid, then the stop position of the substring is also valid. Here, a stop position is considered valid if it is equivalent to the UTF-8 length of an initial substring of the parent string. The substring validity predication is premised on the existence of two sequences of characters such that their concatenation forms the parent string and the byte index of the stop position equals the UTF-8 length of the first sequence.
More concisely: If a substring of a UTF-8 encoded string is valid, then its stop position is also a valid byte index equivalent to the UTF-8 length of the initial substring.
|
Substring.ValidFor.str
theorem Substring.ValidFor.str :
∀ {l m r : List Char} {s : Substring}, Substring.ValidFor l m r s → s.str = { data := l ++ m ++ r }
This theorem states that for any lists of characters `l`, `m`, and `r`, and any substring `s`, if `s` is a valid substring for `l`, `m`, and `r`, then the string value of `s` is equal to the list formed by concatenating `l`, `m`, and `r` in that order. Essentially, it asserts that a valid substring represents the concatenation of its list parameters.
More concisely: For any lists of characters `l`, `m`, and `r`, and substring `s` that is a valid substring of the concatenation of `l`, `m`, and `r`, the string value of `s` equals the concatenation of `l`, `m`, and `r`.
|
Substring.ValidFor.valid
theorem Substring.ValidFor.valid : ∀ {l m r : List Char} {s : Substring}, Substring.ValidFor l m r s → s.Valid := by
sorry
This theorem states that for any lists of characters `l`, `m`, and `r`, and any substring `s`, if `s` is a valid substring for the concatenation of `l`, `m`, and `r`, then `s` is a valid substring in general. Essentially, it suggests that the validity of a substring in a larger context implies its validity in any context.
More concisely: If `s` is a valid substring of the concatenation of lists `l`, `m`, and `r` in Lean 4, then `s` is a valid substring in Lean 4.
|
Substring.ValidFor.nextn
theorem Substring.ValidFor.nextn :
∀ {l m₁ m₂ r : List Char} {s : Substring},
Substring.ValidFor l (m₁ ++ m₂) r s →
∀ (n : ℕ),
s.nextn n { byteIdx := String.utf8Len m₁ } =
{ byteIdx := String.utf8Len m₁ + String.utf8Len (List.take n m₂) }
This theorem, `Substring.ValidFor.nextn`, states that for any lists of characters `l`, `m₁`, `m₂`, and `r`, and for any substring `s` that is valid for the concatenation of `m₁` and `m₂` embedded in `l` and `r`, for any natural number `n`, the `n`-th next position in the substring `s` from the position corresponding to the UTF-8 byte length of `m₁` equals the position corresponding to the sum of the UTF-8 byte length of `m₁` and the UTF-8 byte length of the first `n` characters in `m₂`. This provides a way of finding the `n`-th next position in a valid substring that is formed by concatenating two lists of characters.
More concisely: For any valid substring `s` of length `|m₁| + |m₂|` in the concatenation of lists `l` containing `m₁` and `r` containing `m₂` of UTF-8 encoded characters, the index of the `n`-th next position in `s` after the position determined by the UTF-8 byte length of `m₁` is equal to the sum of the UTF-8 byte lengths of the first `n` characters in `m₂`.
|
Substring.ValidFor.toString
theorem Substring.ValidFor.toString :
∀ {l m r : List Char} {s : Substring}, Substring.ValidFor l m r s → s.toString = { data := m }
The theorem `Substring.ValidFor.toString` states that for any three lists of characters `l`, `m`, and `r`, and any substring `s`, if `s` is a valid substring for the concatenation of `l`, `m`, and `r`, then the string representation of `s` is equivalent to the list `m`. In simpler terms, this theorem guarantees that the `toString` function of a valid substring derived from a concatenation of character lists correctly returns the middle part `m` of the concatenation as a string.
More concisely: If `s` is a valid substring of the concatenation of lists `l`, `m`, and `r` in Lean's `Char` type, then `toString s = m`.
|
Substring.Valid.startValid
theorem Substring.Valid.startValid : ∀ {s : Substring}, s.Valid → String.Pos.Valid s.str s.startPos
This theorem states that for any substring `s`, if `s` is valid, then the start position of `s` is a valid position in the original string from which `s` is extracted. Here, a valid position refers to a position that equals the UTF-8 length of an initial substring of the original string.
More concisely: If `s` is a valid substring of a string, then the start position of `s` in the original string is a valid position (i.e., equals the UTF-8 length of an initial substring of the original string).
|