feat: verification of String.dropPrefix? (#12999)

This PR verifies the `String.dropPrefix?` function for our various
patterns.

src/Init/Data/String/Lemmas/Pattern/TakeDrop/Basic.lean

@@ -26,6 +26,9 @@ theorem skipPrefix?_eq_forwardPatternSkipPrefix? {ρ : Type} {pat : ρ} [Forward
 theorem startsWith_eq_forwardPatternStartsWith {ρ : Type} {pat : ρ} [ForwardPattern pat] {s : Slice} :
     s.startsWith pat = ForwardPattern.startsWith pat s := (rfl)
 
+theorem dropPrefix?_eq_map_skipPrefix? {ρ : Type} {pat : ρ} [ForwardPattern pat] {s : Slice} :
+    s.dropPrefix? pat = (s.skipPrefix? pat).map s.sliceFrom := (rfl)
+
 theorem Pattern.Model.skipPrefix?_eq_some_iff {ρ : Type} {pat : ρ} [ForwardPatternModel pat] [ForwardPattern pat]
     [LawfulForwardPatternModel pat] {s : Slice} {pos : s.Pos} :
     s.skipPrefix? pat = some pos ↔ IsLongestMatch pat pos := by
@@ -52,14 +55,23 @@ theorem Pattern.Model.startsWith_iff {ρ : Type} {pat : ρ} [ForwardPatternModel
     s.startsWith pat = true ↔ MatchesAt pat s.startPos := by
   rw [← Bool.not_eq_false, startsWith_eq_false_iff, Classical.not_not]
 
-theorem dropPrefix?_eq_map_skipPrefix? {ρ : Type} {pat : ρ} [ForwardPattern pat] {s : Slice} :
-    s.dropPrefix? pat = (s.skipPrefix? pat).map s.sliceFrom := (rfl)
-
 @[simp]
 theorem skipPrefix?_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPattern pat] [LawfulForwardPattern pat]
     {s : Slice} : s.skipPrefix? pat = none ↔ s.startsWith pat = false := by
   rw [← Option.isNone_iff_eq_none, ← Option.isSome_eq_false_iff, isSome_skipPrefix?]
 
+@[simp]
+theorem dropPrefix?_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPattern pat] [LawfulForwardPattern pat]
+    {s : Slice} : s.dropPrefix? pat = none ↔ s.startsWith pat = false := by
+  simp [dropPrefix?_eq_map_skipPrefix?]
+
+theorem Pattern.Model.eq_append_of_dropPrefix?_eq_some {ρ : Type} {pat : ρ} [ForwardPatternModel pat] [ForwardPattern pat]
+    [LawfulForwardPatternModel pat] {s res : Slice} (h : s.dropPrefix? pat = some res) :
+    ∃ t, ForwardPatternModel.Matches pat t ∧ s.copy = t ++ res.copy := by
+  simp only [dropPrefix?_eq_map_skipPrefix?, Option.map_eq_some_iff, skipPrefix?_eq_some_iff] at h
+  obtain ⟨pos, h₁, h₂⟩ := h
+  exact ⟨(s.sliceTo pos).copy, h₁.isMatch.matches_copy, by simp [← h₂, ← copy_eq_copy_sliceTo]⟩
+
 end Slice
 
 theorem skipPrefix?_eq_skipPrefix?_toSlice {ρ : Type} {pat : ρ} [ForwardPattern pat] {s : String} :
@@ -68,4 +80,7 @@ theorem skipPrefix?_eq_skipPrefix?_toSlice {ρ : Type} {pat : ρ} [ForwardPatter
 theorem startsWith_eq_startsWith_toSlice {ρ : Type} {pat : ρ} [ForwardPattern pat] {s : String} :
     s.startsWith pat = s.toSlice.startsWith pat := (rfl)
 
+theorem dropPrefix?_eq_dropPrefix?_toSlice {ρ : Type} {pat : ρ} [ForwardPattern pat] {s : String} :
+    s.dropPrefix? pat = s.toSlice.dropPrefix? pat := (rfl)
+
 end String

src/Init/Data/String/Lemmas/Pattern/TakeDrop/Char.lean

@@ -40,6 +40,10 @@ theorem startsWith_char_eq_head? {c : Char} {s : Slice} :
   simp only [← toList_inj, toList_append, toList_singleton, List.cons_append, List.nil_append]
   cases h : s.copy.toList <;> simp_all [← ofList_inj]
 
+theorem eq_append_of_dropPrefix?_char_eq_some {c : Char} {s res : Slice} (h : s.dropPrefix? c = some res) :
+    s.copy = singleton c ++ res.copy := by
+  simpa [ForwardPatternModel.Matches] using Pattern.Model.eq_append_of_dropPrefix?_eq_some h
+
 end Slice
 
 theorem skipPrefix?_char_eq_some_iff {c : Char} {s : String} {pos : s.Pos} :
@@ -59,4 +63,9 @@ theorem startsWith_char_eq_head? {c : Char} {s : String} :
     s.startsWith c = (s.toList.head? == some c) := by
   simp [startsWith_eq_startsWith_toSlice, Slice.startsWith_char_eq_head?]
 
+theorem eq_append_of_dropPrefix?_char_eq_some {c : Char} {s : String} {res : Slice} (h : s.dropPrefix? c = some res) :
+    s = singleton c ++ res.copy := by
+  rw [dropPrefix?_eq_dropPrefix?_toSlice] at h
+  simpa using Slice.eq_append_of_dropPrefix?_char_eq_some h
+
 end String

src/Init/Data/String/Lemmas/Pattern/TakeDrop/Pred.lean

@@ -43,6 +43,11 @@ theorem startsWith_bool_eq_head? {p : Char → Bool} {s : Slice} :
   · obtain ⟨t, ht⟩ := s.splits_startPos.exists_eq_singleton_append h
     simp [h, ht]
 
+theorem eq_append_of_dropPrefix?_bool_eq_some {p : Char → Bool} {s res : Slice} (h : s.dropPrefix? p = some res) :
+    ∃ c, s.copy = singleton c ++ res.copy ∧ p c = true := by
+  obtain ⟨_, ⟨c, ⟨rfl, h₁⟩⟩, h₂⟩ := by simpa [ForwardPatternModel.Matches] using Pattern.Model.eq_append_of_dropPrefix?_eq_some h
+  exact ⟨_, h₂, h₁⟩
+
 theorem skipPrefix?_prop_eq_some_iff {P : Char → Prop} [DecidablePred P] {s : Slice} {pos : s.Pos} :
     s.skipPrefix? P = some pos ↔ ∃ h, pos = s.startPos.next h ∧ P (s.startPos.get h) := by
   simp [skipPrefix?_prop_eq_skipPrefix?_decide, skipPrefix?_bool_eq_some_iff]
@@ -59,6 +64,11 @@ theorem startsWith_prop_eq_head? {P : Char → Prop} [DecidablePred P] {s : Slic
     s.startsWith P = s.copy.toList.head?.any (decide <| P ·) := by
   simp [startsWith_prop_eq_startsWith_decide, startsWith_bool_eq_head?]
 
+theorem eq_append_of_dropPrefix_prop_eq_some {P : Char → Prop} [DecidablePred P] {s res : Slice} (h : s.dropPrefix? P = some res) :
+    ∃ c, s.copy = singleton c ++ res.copy ∧ P c := by
+  rw [dropPrefix?_prop_eq_dropPrefix?_decide] at h
+  simpa using eq_append_of_dropPrefix?_bool_eq_some h
+
 end Slice
 
 theorem skipPrefix?_bool_eq_some_iff {p : Char → Bool} {s : String} {pos : s.Pos} :
@@ -78,6 +88,11 @@ theorem startsWith_bool_eq_head? {p : Char → Bool} {s : String} :
     s.startsWith p = s.toList.head?.any p := by
   simp [startsWith_eq_startsWith_toSlice, Slice.startsWith_bool_eq_head?]
 
+theorem eq_append_of_dropPrefix?_bool_eq_some {p : Char → Bool} {s : String} {res : Slice} (h : s.dropPrefix? p = some res) :
+    ∃ c, s = singleton c ++ res.copy ∧ p c = true := by
+  rw [dropPrefix?_eq_dropPrefix?_toSlice] at h
+  simpa using Slice.eq_append_of_dropPrefix?_bool_eq_some h
+
 theorem skipPrefix?_prop_eq_some_iff {P : Char → Prop} [DecidablePred P] {s : String} {pos : s.Pos} :
     s.skipPrefix? P = some pos ↔ ∃ h, pos = s.startPos.next h ∧ P (s.startPos.get h) := by
   simp [skipPrefix?_eq_skipPrefix?_toSlice, Slice.skipPrefix?_prop_eq_some_iff, ← Pos.toSlice_inj,
@@ -95,4 +110,9 @@ theorem startsWith_prop_eq_head? {P : Char → Prop} [DecidablePred P] {s : Stri
     s.startsWith P = s.toList.head?.any (decide <| P ·) := by
   simp [startsWith_eq_startsWith_toSlice, Slice.startsWith_prop_eq_head?]
 
+theorem eq_append_of_dropPrefix?_prop_eq_some {P : Char → Prop} [DecidablePred P] {s : String} {res : Slice}
+    (h : s.dropPrefix? P = some res) : ∃ c, s = singleton c ++ res.copy ∧ P c := by
+  rw [dropPrefix?_eq_dropPrefix?_toSlice] at h
+  simpa using Slice.eq_append_of_dropPrefix_prop_eq_some h
+
 end String

src/Init/Data/String/Lemmas/Pattern/TakeDrop/String.lean

@@ -13,6 +13,7 @@ import Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
 import Init.Data.String.Lemmas.Pattern.String
 import Init.Data.List.Sublist
 import Init.Data.Option.Lemmas
+import Init.Data.String.Lemmas.Basic
 
 public section
 
@@ -22,6 +23,10 @@ namespace String
 
 namespace Slice
 
+theorem skipPrefix?_slice_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true) :
+    s.skipPrefix? pat = some s.startPos := by
+  rw [skipPrefix?_eq_forwardPatternSkipPrefix?, ForwardSliceSearcher.skipPrefix?_of_isEmpty hpat]
+
 @[simp]
 theorem skipPrefix?_slice_eq_some_iff {pat s : Slice} {pos : s.Pos} :
     s.skipPrefix? pat = some pos ↔ ∃ t, pos.Splits pat.copy t := by
@@ -29,9 +34,11 @@ theorem skipPrefix?_slice_eq_some_iff {pat s : Slice} {pos : s.Pos} :
   | false =>
     have := ForwardSliceSearcher.lawfulForwardPatternModel h
     rw [Pattern.Model.skipPrefix?_eq_some_iff, ForwardSliceSearcher.isLongestMatch_iff_splits h]
-  | true =>
-    rw [skipPrefix?_eq_forwardPatternSkipPrefix?, ForwardSliceSearcher.skipPrefix?_of_isEmpty h]
-    simp [(show pat.copy = "" by simpa), eq_comm]
+  | true => simp [skipPrefix?_slice_of_isEmpty h, (show pat.copy = "" by simpa), eq_comm]
+
+theorem startsWith_slice_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true) :
+    s.startsWith pat = true := by
+  rw [startsWith_eq_forwardPatternStartsWith, ForwardSliceSearcher.startsWith_of_isEmpty hpat]
 
 @[simp]
 theorem startsWith_slice_iff {pat s : Slice} :
@@ -43,32 +50,67 @@ theorem startsWith_slice_iff {pat s : Slice} :
       splits_startPos_iff, exists_and_left, exists_eq_left]
     simp only [← toList_inj, toList_append, List.prefix_iff_exists_append_eq]
     exact ⟨fun ⟨t, ht⟩ => ⟨t.toList, by simp [ht]⟩, fun ⟨t, ht⟩ => ⟨String.ofList t, by simp [← ht]⟩⟩
-  | true =>
-    rw [startsWith_eq_forwardPatternStartsWith, ForwardSliceSearcher.startsWith_of_isEmpty h]
-    simp [(show pat.copy = "" by simpa)]
+  | true => simp [startsWith_slice_of_isEmpty h, (show pat.copy = "" by simpa)]
 
 @[simp]
 theorem startsWith_slice_eq_false_iff {pat s : Slice} :
     s.startsWith pat = false ↔ ¬ (pat.copy.toList <+: s.copy.toList) := by
   simp [← Bool.not_eq_true, startsWith_slice_iff]
 
+theorem dropPrefix?_slice_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true) :
+    s.dropPrefix? pat = some s := by
+  simp [dropPrefix?_eq_map_skipPrefix?, skipPrefix?_slice_of_isEmpty hpat]
+
+theorem eq_append_of_dropPrefix?_slice_eq_some {pat s res : Slice} (h : s.dropPrefix? pat = some res) :
+    s.copy = pat.copy ++ res.copy := by
+  match hpat : pat.isEmpty with
+  | false =>
+    have := ForwardSliceSearcher.lawfulForwardPatternModel hpat
+    have := Pattern.Model.eq_append_of_dropPrefix?_eq_some h
+    simp only [ForwardPatternModel.Matches] at this
+    obtain ⟨_, ⟨-, rfl⟩, h⟩ := this
+    exact h
+  | true => simp [Option.some.inj (h ▸ dropPrefix?_slice_of_isEmpty hpat), (show pat.copy = "" by simpa)]
+
 @[simp]
 theorem skipPrefix?_string_eq_some_iff {pat : String} {s : Slice} {pos : s.Pos} :
     s.skipPrefix? pat = some pos ↔ ∃ t, pos.Splits pat t := by
   simp [skipPrefix?_string_eq_skipPrefix?_toSlice]
 
+@[simp]
+theorem skipPrefix?_string_empty {s : Slice} : s.skipPrefix? "" = some s.startPos := by
+  simp
+
 @[simp]
 theorem startsWith_string_iff {pat : String} {s : Slice} :
     s.startsWith pat ↔ pat.toList <+: s.copy.toList := by
   simp [startsWith_string_eq_startsWith_toSlice]
 
+@[simp]
+theorem startsWith_string_empty {s : Slice} : s.startsWith "" = true := by
+  simp
+
 @[simp]
 theorem startsWith_string_eq_false_iff {pat : String} {s : Slice} :
     s.startsWith pat = false ↔ ¬ (pat.toList <+: s.copy.toList) := by
   simp [startsWith_string_eq_startsWith_toSlice]
 
+@[simp]
+theorem dropPrefix?_string_empty {s : Slice} : s.dropPrefix? "" = some s := by
+  simpa [dropPrefix?_string_eq_dropPrefix?_toSlice] using dropPrefix?_slice_of_isEmpty (by simp)
+
+theorem eq_append_of_dropPrefix?_string_eq_some {pat : String} {s res : Slice} (h : s.dropPrefix? pat = some res) :
+    s.copy = pat ++ res.copy := by
+  rw [dropPrefix?_string_eq_dropPrefix?_toSlice] at h
+  simpa using eq_append_of_dropPrefix?_slice_eq_some h
+
 end Slice
 
+theorem skipPrefix?_slice_of_isEmpty {pat : Slice} {s : String} (hpat : pat.isEmpty = true) :
+    s.skipPrefix? pat = some s.startPos := by
+  rw [skipPrefix?_eq_skipPrefix?_toSlice, Slice.skipPrefix?_slice_of_isEmpty hpat]
+  simp
+
 @[simp]
 theorem skipPrefix?_slice_eq_some_iff {pat : Slice} {s : String} {pos : s.Pos} :
     s.skipPrefix? pat = some pos ↔ ∃ t, pos.Splits pat.copy t := by
@@ -78,6 +120,10 @@ theorem skipPrefix?_slice_eq_some_iff {pat : Slice} {s : String} {pos : s.Pos} :
   rintro ⟨pos, h, rfl⟩
   simpa
 
+theorem startsWith_slice_of_isEmpty {pat : Slice} {s : String} (hpat : pat.isEmpty = true) :
+    s.startsWith pat = true := by
+  rw [startsWith_eq_startsWith_toSlice, Slice.startsWith_slice_of_isEmpty hpat]
+
 @[simp]
 theorem startsWith_slice_iff {pat : Slice} {s : String} :
     s.startsWith pat ↔ pat.copy.toList <+: s.toList := by
@@ -88,6 +134,19 @@ theorem startsWith_slice_eq_false_iff {pat : Slice} {s : String} :
     s.startsWith pat = false ↔ ¬ (pat.copy.toList <+: s.toList) := by
   simp [startsWith_eq_startsWith_toSlice]
 
+theorem dropPrefix?_slice_of_isEmpty {pat : Slice} {s : String} (hpat : pat.isEmpty = true) :
+    s.dropPrefix? pat = some s.toSlice := by
+  rw [dropPrefix?_eq_dropPrefix?_toSlice, Slice.dropPrefix?_slice_of_isEmpty hpat]
+
+theorem eq_append_of_dropPrefix?_slice_eq_some {pat res : Slice} {s : String} (h : s.dropPrefix? pat = some res) :
+    s = pat.copy ++ res.copy := by
+  rw [dropPrefix?_eq_dropPrefix?_toSlice] at h
+  simpa using Slice.eq_append_of_dropPrefix?_slice_eq_some h
+
+@[simp]
+theorem skipPrefix?_string_empty {s : String} : s.skipPrefix? "" = some s.startPos := by
+  simp [skipPrefix?_eq_skipPrefix?_toSlice]
+
 @[simp]
 theorem skipPrefix?_string_eq_some_iff {pat s : String} {pos : s.Pos} :
     s.skipPrefix? pat = some pos ↔ ∃ t, pos.Splits pat t := by
@@ -97,6 +156,10 @@ theorem skipPrefix?_string_eq_some_iff {pat s : String} {pos : s.Pos} :
   rintro ⟨pos, h, rfl⟩
   simpa
 
+@[simp]
+theorem startsWith_string_empty {s : String} : s.startsWith "" = true := by
+  simp [startsWith_eq_startsWith_toSlice]
+
 @[simp]
 theorem startsWith_string_iff {pat s : String} :
     s.startsWith pat ↔ pat.toList <+: s.toList := by
@@ -107,4 +170,13 @@ theorem startsWith_string_eq_false_iff {pat s : String} :
     s.startsWith pat = false ↔ ¬ (pat.toList <+: s.toList) := by
   simp [startsWith_eq_startsWith_toSlice]
 
+@[simp]
+theorem dropPrefix?_string_empty {s : String} : s.dropPrefix? "" = some s.toSlice := by
+  simp [dropPrefix?_eq_dropPrefix?_toSlice]
+
+theorem eq_append_of_dropPrefix?_string_eq_some {s pat : String} {res : Slice} (h : s.dropPrefix? pat = some res) :
+    s = pat ++ res.copy := by
+  rw [dropPrefix?_eq_dropPrefix?_toSlice] at h
+  simpa using Slice.eq_append_of_dropPrefix?_string_eq_some h
+
 end String