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.

Equations

• p.remainingBytes = p.offset.byteDistance s.endPos.offset

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

Equations

• String.Slice.Pos.instWellFoundedRelation = { rel := fun (p q : s.Pos) => q < p, wf := ⋯ }

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.

Equations

• p.down = { inner := p }

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

Equations

• String.Slice.Pos.instWellFoundedRelationDown = { rel := fun (p q : String.Slice.Pos.Down s) => p.inner < q.inner, wf := ⋯ }

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.ValidPos.remainingBytes {s : String} (p : s.ValidPos) : Nat

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

Equations

• p.remainingBytes = p.toSlice.remainingBytes

@[simp]

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

theorem String.ValidPos.remainingBytes_eq_byteDistance {s : String} {p : s.ValidPos} : p.remainingBytes = p.offset.byteDistance s.endValidPos.offset

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

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

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

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

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

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

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

Equations

• String.ValidPos.instWellFoundedRelation = { rel := fun (p q : s.ValidPos) => q < p, wf := ⋯ }

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

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

• inner : s.ValidPos

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

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

Equations

• p.down = { inner := p }

@[simp]

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

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

Equations

• String.ValidPos.instWellFoundedRelationDown = { rel := fun (p q : String.ValidPos.Down s) => p.inner < q.inner, wf := ⋯ }

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

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

theorem String.ValidPos.ne_endValidPos_of_next?_eq_some {s : String} {p q : s.ValidPos} (h : p.next? = some q) : p ≠ s.endValidPos

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

theorem String.ValidPos.ne_startValidPos_of_prev?_eq_some {s : String} {p q : s.ValidPos} (h : p.prev? = some q) : p ≠ s.startValidPos

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

@[simp]

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

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

theorem String.ValidPos.le_trans {s : String} {p q r : s.ValidPos} : p ≤ q → q ≤ r → p ≤ r

theorem String.ValidPos.le_of_lt {s : String} {p q : s.ValidPos} : p < q → p ≤ q

@[simp]

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

@[simp]

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

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

@[simp]

theorem String.Slice.Pos.remainingBytes_toCopy {s : Slice} {p : s.Pos} : p.toCopy.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