feat: helper theorem for proving termination of simple String traversal functions

src/Init/Data/String/Basic.lean

@@ -215,7 +215,7 @@ abbrev iter := mkIterator
 instance : SizeOf String.Iterator where
   sizeOf i := i.1.utf8ByteSize - i.2
 
-theorem String.Iterator.sizeOf_eq (i : String.Iterator) : sizeOf i = i.1.utf8ByteSize - i.2 :=
+theorem Iterator.sizeOf_eq (i : String.Iterator) : sizeOf i = i.1.utf8ByteSize - i.2 :=
   rfl
 
 namespace Iterator

src/Init/Data/String/Extra.lean

@@ -39,4 +39,17 @@ theorem eq_empty_of_bsize_eq_zero (h : s.bsize = 0) : s = "" := by
     have : utf8ByteSize.go cs + 1 ≤ utf8ByteSize.go cs + csize c := Nat.add_le_add_left (one_le_csize c) _
     simp_arith [h] at this
 
+theorem lt_next (s : String) (i : String.Pos) : i < s.next i := by
+  simp_arith [next]; apply one_le_csize
+
+theorem Iterator.sizeOf_next_lt (i : String.Iterator) (h : i.hasNext) : sizeOf i.next < sizeOf i := by
+  cases i; rename_i s pos; simp [Iterator.next, Iterator.sizeOf_eq]; simp [Iterator.hasNext] at h
+  have := String.lt_next s pos
+  apply Nat.sub.elim (motive := fun k => k < _) (utf8ByteSize s) (String.next s pos)
+  . intro hle k he
+    simp [he]; rw [Nat.add_comm, Nat.add_sub_assoc (Nat.le_of_lt this)]
+    have := Nat.zero_lt_sub_of_lt this
+    simp_all_arith
+  . intro; apply Nat.zero_lt_sub_of_lt h
+
 end String