chore: upstream String.dropPrefix? (#5728)

Useful String helper functions widely used in tactic implementations.

src/Init/Data/String/Basic.lean

@@ -317,6 +317,9 @@ theorem _root_.Char.utf8Size_le_four (c : Char) : c.utf8Size ≤ 4 := by
 
 @[simp] theorem pos_add_char (p : Pos) (c : Char) : (p + c).byteIdx = p.byteIdx + c.utf8Size := rfl
 
+protected theorem Pos.ne_zero_of_lt : {a b : Pos} → a < b → b ≠ 0
+  | _, _, hlt, rfl => Nat.not_lt_zero _ hlt
+
 theorem lt_next (s : String) (i : Pos) : i.1 < (s.next i).1 :=
   Nat.add_lt_add_left (Char.utf8Size_pos _) _
 
@@ -1021,6 +1024,66 @@ instance hasBeq : BEq Substring := ⟨beq⟩
 def sameAs (ss1 ss2 : Substring) : Bool :=
   ss1.startPos == ss2.startPos && ss1 == ss2
 
+/--
+Returns the longest common prefix of two substrings.
+The returned substring will use the same underlying string as `s`.
+-/
+def commonPrefix (s t : Substring) : Substring :=
+  { s with stopPos := loop s.startPos t.startPos }
+where
+  /-- Returns the ending position of the common prefix, working up from `spos, tpos`. -/
+  loop spos tpos :=
+    if h : spos < s.stopPos ∧ tpos < t.stopPos then
+      if s.str.get spos == t.str.get tpos then
+        have := Nat.sub_lt_sub_left h.1 (s.str.lt_next spos)
+        loop (s.str.next spos) (t.str.next tpos)
+      else
+        spos
+    else
+      spos
+  termination_by s.stopPos.byteIdx - spos.byteIdx
+
+/--
+Returns the longest common suffix of two substrings.
+The returned substring will use the same underlying string as `s`.
+-/
+def commonSuffix (s t : Substring) : Substring :=
+  { s with startPos := loop s.stopPos t.stopPos }
+where
+  /-- Returns the starting position of the common prefix, working down from `spos, tpos`. -/
+  loop spos tpos :=
+    if h : s.startPos < spos ∧ t.startPos < tpos then
+      let spos' := s.str.prev spos
+      let tpos' := t.str.prev tpos
+      if s.str.get spos' == t.str.get tpos' then
+        have : spos' < spos := s.str.prev_lt_of_pos spos (String.Pos.ne_zero_of_lt h.1)
+        loop spos' tpos'
+      else
+        spos
+    else
+      spos
+  termination_by spos.byteIdx
+
+/--
+If `pre` is a prefix of `s`, i.e. `s = pre ++ t`, returns the remainder `t`.
+-/
+def dropPrefix? (s : Substring) (pre : Substring) : Option Substring :=
+  let t := s.commonPrefix pre
+  if t.bsize = pre.bsize then
+    some { s with startPos := t.stopPos }
+  else
+    none
+
+/--
+If `suff` is a suffix of `s`, i.e. `s = t ++ suff`, returns the remainder `t`.
+-/
+def dropSuffix? (s : Substring) (suff : Substring) : Option Substring :=
+  let t := s.commonSuffix suff
+  if t.bsize = suff.bsize then
+    some { s with stopPos := t.startPos }
+  else
+    none
+
 end Substring
 
 namespace String
@@ -1082,6 +1145,28 @@ namespace String
 @[inline] def decapitalize (s : String) :=
   s.set 0 <| s.get 0 |>.toLower
 
+/--
+If `pre` is a prefix of `s`, i.e. `s = pre ++ t`, returns the remainder `t`.
+-/
+def dropPrefix? (s : String) (pre : Substring) : Option Substring :=
+  s.toSubstring.dropPrefix? pre
+
+/--
+If `suff` is a suffix of `s`, i.e. `s = t ++ suff`, returns the remainder `t`.
+-/
+def dropSuffix? (s : String) (suff : Substring) : Option Substring :=
+  s.toSubstring.dropSuffix? suff
+
+/-- `s.stripPrefix pre` will remove `pre` from the beginning of `s` if it occurs there,
+or otherwise return `s`. -/
+def stripPrefix (s : String) (pre : Substring) : String :=
+  s.dropPrefix? pre |>.map Substring.toString |>.getD s
+
+/-- `s.stripSuffix suff` will remove `suff` from the end of `s` if it occurs there,
+or otherwise return `s`. -/
+def stripSuffix (s : String) (suff : Substring) : String :=
+  s.dropSuffix? suff |>.map Substring.toString |>.getD s
+
 end String
 
 namespace Char