feat: redefine String, part two (#10457)

This PR introduces safe alternatives to `String.Pos` and `Substring`
that can only represent valid positions/slices.

Specifically, the PR

- introduces the predicate `String.Pos.IsValid`;
- proves several nontrivial equivalent conditions for
`String.Pos.IsValid`;
- introduces `String.ValidPos`, which is a `String.Pos` with an
`IsValid` proof;
- introduces `String.Slice`, which is like `Substring` but made from
`String.ValidPos` instead of `Pos`;
- introduces `String.Pos.IsValidForSlice`, which is like
`String.Pos.IsValid` but for slices;
- introduces `String.Slice.Pos`, which is like `String.ValidPos` but for
slices;
- introduces various functions for converting between the two types of
positions.

The API added in this PR is not complete. It will be expanded in future
PRs with addional operations and verification.

Author: TwoFX

src/Init/Data/ByteArray/Lemmas.lean

@@ -167,9 +167,9 @@ theorem ByteArray.append_inj_left {xs₁ xs₂ ys₁ ys₂ : ByteArray} (h : xs
   simp only [ByteArray.ext_iff, ← ByteArray.size_data, ByteArray.data_append] at *
   exact Array.append_inj_left h hl
 
-theorem ByteArray.extract_append_eq_right {a b : ByteArray} {i : Nat} (hi : i = a.size) :
-    (a ++ b).extract i (a ++ b).size = b := by
-  subst hi
+theorem ByteArray.extract_append_eq_right {a b : ByteArray} {i j : Nat} (hi : i = a.size) (hj : j = a.size + b.size) :
+    (a ++ b).extract i j = b := by
+  subst hi hj
   ext1
   simp [← size_data]
 

src/Init/Data/List/Nat/TakeDrop.lean

@@ -162,6 +162,9 @@ theorem take_eq_take_iff :
   | x :: xs, 0, j + 1 => by simp [succ_min_succ]
   | x :: xs, i + 1, j + 1 => by simp [succ_min_succ, take_eq_take_iff]
 
+theorem take_eq_take_min {l : List α} {i : Nat} : l.take i = l.take (min i l.length) := by
+  simp
+
 @[grind =]
 theorem take_add {l : List α} {i j : Nat} : l.take (i + j) = l.take i ++ (l.drop i).take j := by
   suffices take (i + j) (take i l ++ drop i l) = take i l ++ take j (drop i l) by