Helpers for termination arguments about functions operating on strings

def String.Slice.Pos.remainingBytes {s : Slice} (p : s.Pos) : Nat

The number of bytes between p and the end position. This number decreases as p advances.

theorem String.Slice.Pos.remainingBytes_eq_byteDistance {s : Slice} {p : s.Pos} : p.remainingBytes = p.offset.byteDistance s.endPos.offset

theorem String.Slice.Pos.remainingBytes_eq {s : Slice} {p : s.Pos} : p.remainingBytes = s.utf8ByteSize - p.offset.byteIdx

theorem String.Slice.Pos.remainingBytes_inj {s : Slice} {p q : s.Pos} : p.remainingBytes = q.remainingBytes ↔ p = q

theorem String.Slice.Pos.le_iff_remainingBytes_le {s : Slice} (p q : s.Pos) : p ≤ q ↔ q.remainingBytes ≤ p.remainingBytes

theorem String.Slice.Pos.lt_iff_remainingBytes_lt {s : Slice} (p q : s.Pos) : p < q ↔ q.remainingBytes < p.remainingBytes

theorem String.Slice.Pos.wellFounded_lt {s : Slice} : WellFounded fun (p q : s.Pos) => p < q

theorem String.Slice.Pos.wellFounded_gt {s : Slice} : WellFounded fun (p q : s.Pos) => q < p

instance String.Slice.Pos.instWellFoundedRelation {s : Slice} : WellFoundedRelation s.Pos

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

Type alias for String.Slice.Pos representing that the given position is expected to decrease in recursive calls.

• inner : s.Pos

def String.Slice.Pos.down {s : Slice} (p : s.Pos) : Down s

Use termination_by pos.down to signify that in a recursive call, the parameter pos is expected to decrease.

@[simp]

theorem String.Slice.Pos.inner_down {s : Slice} {p : s.Pos} : p.down.inner = p

instance String.Slice.Pos.instWellFoundedRelationDown {s : Slice} : WellFoundedRelation (Down s)

theorem String.Slice.Pos.ne_endPos_of_next?_eq_some {s : Slice} {p q : s.Pos} : p.next? = some q → p ≠ s.endPos

theorem String.Slice.Pos.eq_next_of_next?_eq_some {s : Slice} {p q : s.Pos} (h : p.next? = some q) : q = p.next ⋯

theorem String.Slice.Pos.ne_startPos_of_prev?_eq_some {s : Slice} {p q : s.Pos} : p.prev? = some q → p ≠ s.startPos

theorem String.Slice.Pos.eq_prev_of_prev?_eq_some {s : Slice} {p q : s.Pos} (h : p.prev? = some q) : q = p.prev ⋯

@[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.Slice.Pos.lt_next_next {s : Slice} {p : s.Pos} {h : p ≠ s.endPos} {h' : p.next h ≠ s.endPos} : p < (p.next h).next h'

@[simp]

theorem String.Slice.Pos.prev_prev_lt {s : Slice} {p : s.Pos} {h : p ≠ s.startPos} {h' : p.prev h ≠ s.startPos} : (p.prev h).prev h' < p

def String.Pos.remainingBytes {s : String} (p : s.Pos) : Nat

The number of bytes between p and the end position. This number decreases as p advances.

@[simp]

theorem String.Pos.remainingBytes_toSlice {s : String} {p : s.Pos} : p.toSlice.remainingBytes = p.remainingBytes

theorem String.Pos.remainingBytes_eq_byteDistance {s : String} {p : s.Pos} : p.remainingBytes = p.offset.byteDistance s.endPos.offset

theorem String.Pos.remainingBytes_eq {s : String} {p : s.Pos} : p.remainingBytes = s.utf8ByteSize - p.offset.byteIdx

theorem String.Pos.remainingBytes_inj {s : String} {p q : s.Pos} : p.remainingBytes = q.remainingBytes ↔ p = q

theorem String.Pos.le_iff_remainingBytes_le {s : String} (p q : s.Pos) : p ≤ q ↔ q.remainingBytes ≤ p.remainingBytes

theorem String.Pos.lt_iff_remainingBytes_lt {s : String} (p q : s.Pos) : p < q ↔ q.remainingBytes < p.remainingBytes

theorem String.Pos.wellFounded_lt {s : String} : WellFounded fun (p q : s.Pos) => p < q

theorem String.Pos.wellFounded_gt {s : String} : WellFounded fun (p q : s.Pos) => q < p

instance String.Pos.instWellFoundedRelation {s : String} : WellFoundedRelation s.Pos

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

Type alias for String.Pos representing that the given position is expected to decrease in recursive calls.

• inner : s.Pos

def String.Pos.down {s : String} (p : s.Pos) : Down s

Use termination_by pos.down to signify that in a recursive call, the parameter pos is expected to decrease.

@[simp]

theorem String.Pos.inner_down {s : String} {p : s.Pos} : p.down.inner = p

instance String.Pos.instWellFoundedRelationDown {s : String} : WellFoundedRelation (Down s)

theorem String.Pos.map_toSlice_next? {s : String} {p : s.Pos} : Option.map toSlice p.next? = p.toSlice.next?

theorem String.Pos.map_toSlice_prev? {s : String} {p : s.Pos} : Option.map toSlice p.prev? = p.toSlice.prev?

theorem String.Pos.ne_endPos_of_next?_eq_some {s : String} {p q : s.Pos} (h : p.next? = some q) : p ≠ s.endPos

theorem String.Pos.eq_next_of_next?_eq_some {s : String} {p q : s.Pos} (h : p.next? = some q) : q = p.next ⋯

theorem String.Pos.ne_startPos_of_prev?_eq_some {s : String} {p q : s.Pos} (h : p.prev? = some q) : p ≠ s.startPos

theorem String.Pos.eq_prev_of_prev?_eq_some {s : String} {p q : s.Pos} (h : p.prev? = some q) : q = p.prev ⋯

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

@[simp]

theorem String.Pos.lt_next_next {s : String} {p : s.Pos} {h : p ≠ s.endPos} {h' : p.next h ≠ s.endPos} : p < (p.next h).next h'

@[simp]

theorem String.Pos.prev_prev_lt {s : String} {p : s.Pos} {h : p ≠ s.startPos} {h' : p.prev h ≠ s.startPos} : (p.prev h).prev h' < p

theorem String.Pos.Splits.remainingBytes_eq {s : String} {p : s.Pos} {t₁ t₂ : String} (h : p.Splits t₁ t₂) : p.remainingBytes = t₂.utf8ByteSize

@[simp]

theorem String.Slice.Pos.remainingBytes_copy {s : Slice} {p : s.Pos} : p.copy.remainingBytes = p.remainingBytes

theorem String.Slice.Pos.Splits.remainingBytes_eq {s : Slice} {p : s.Pos} {t₁ t₂ : String} (h : p.Splits t₁ t₂) : p.remainingBytes = t₂.utf8ByteSize