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_reducible]

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_reducible]

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.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

theorem String.Slice.Pos.next_induction {s : Slice} {C : s.Pos → Prop} (p : s.Pos) (next : ∀ (x : s.Pos) (h : x ≠ s.endPos), C (x.next h) → C x) (endPos : C s.endPos) : C p

theorem String.Slice.Pos.prev_induction {s : Slice} {C : s.Pos → Prop} (p : s.Pos) (prev : ∀ (x : s.Pos) (h : x ≠ s.startPos), C (x.prev h) → C x) (startPos : C s.startPos) : C 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_reducible]

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_reducible]

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.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

theorem String.Pos.next_induction {s : String} {C : s.Pos → Prop} (p : s.Pos) (next : ∀ (x : s.Pos) (h : x ≠ s.endPos), C (x.next h) → C x) (endPos : C s.endPos) : C p

theorem String.Pos.prev_induction {s : String} {C : s.Pos → Prop} (p : s.Pos) (prev : ∀ (x : s.Pos) (h : x ≠ s.startPos), C (x.prev h) → C x) (startPos : C s.startPos) : C p

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