remove upstreamed string lemmas

Batteries/Data/String/Lemmas.lean

@@ -9,14 +9,9 @@ import Batteries.Data.String.Basic
 import Batteries.Tactic.Lint.Misc
 import Batteries.Tactic.SeqFocus
 
-@[simp] theorem Char.length_toString (c : Char) : c.toString.length = 1 := rfl
-
 namespace String
 
-@[ext] theorem ext {s₁ s₂ : String} (h : s₁.data = s₂.data) : s₁ = s₂ :=
-  show ⟨s₁.data⟩ = (⟨s₂.data⟩ : String) from h ▸ rfl
-
-theorem ext_iff {s₁ s₂ : String} : s₁ = s₂ ↔ s₁.data = s₂.data := ⟨fun h => h ▸ rfl, ext⟩
+attribute [ext] ext
 
 theorem lt_trans {s₁ s₂ s₃ : String} : s₁ < s₂ → s₂ < s₃ → s₁ < s₃ :=
   List.lt_trans' (α := Char) Nat.lt_trans
@@ -34,34 +29,10 @@ instance : Batteries.LTOrd String := .compareOfLessAndEq
 
 instance : Batteries.BEqOrd String := .compareOfLessAndEq String.lt_irrefl
 
-@[simp] theorem default_eq : default = "" := rfl
-
-@[simp] theorem str_eq : str = push := rfl
-
 @[simp] theorem mk_length (s : List Char) : (String.mk s).length = s.length := rfl
 
-@[simp] theorem length_empty : "".length = 0 := rfl
-
-@[simp] theorem length_singleton (c : Char) : (String.singleton c).length = 1 := rfl
-
-@[simp] theorem length_push (c : Char) : (String.push s c).length = s.length + 1 := by
-  rw [push, mk_length, List.length_append, List.length_singleton, Nat.succ.injEq]
-  rfl
-
-@[simp] theorem length_pushn (c : Char) (n : Nat) : (pushn s c n).length = s.length + n := by
-  unfold pushn; induction n <;> simp [Nat.repeat, Nat.add_assoc, *]
-
-@[simp] theorem length_append (s t : String) : (s ++ t).length = s.length + t.length := by
-  simp only [length, append, List.length_append]
-
-@[simp] theorem data_push (s : String) (c : Char) : (s.push c).1 = s.1 ++ [c] := rfl
-
-@[simp] theorem data_append (s t : String) : (s ++ t).1 = s.1 ++ t.1 := rfl
-
 attribute [simp] toList -- prefer `String.data` over `String.toList` in lemmas
 
-theorem lt_iff (s t : String) : s < t ↔ s.1 < t.1 := .rfl
-
 private theorem add_csize_pos : 0 < i + csize c :=
   Nat.add_pos_right _ (csize_pos c)
 
@@ -115,69 +86,13 @@ end
 
 namespace Pos
 
-@[simp] theorem byteIdx_zero : (0 : Pos).byteIdx = 0 := rfl
-
-theorem byteIdx_mk (n : Nat) : byteIdx ⟨n⟩ = n := rfl
-
-@[simp] theorem mk_zero : ⟨0⟩ = (0 : Pos) := rfl
-
-@[simp] theorem mk_byteIdx (p : Pos) : ⟨p.byteIdx⟩ = p := rfl
-
-@[ext] theorem ext {i₁ i₂ : Pos} (h : i₁.byteIdx = i₂.byteIdx) : i₁ = i₂ :=
-  show ⟨i₁.byteIdx⟩ = (⟨i₂.byteIdx⟩ : Pos) from h ▸ rfl
-
-theorem ext_iff {i₁ i₂ : Pos} : i₁ = i₂ ↔ i₁.byteIdx = i₂.byteIdx := ⟨fun h => h ▸ rfl, ext⟩
-
-@[simp] theorem add_byteIdx (p₁ p₂ : Pos) : (p₁ + p₂).byteIdx = p₁.byteIdx + p₂.byteIdx := rfl
-
-theorem add_eq (p₁ p₂ : Pos) : p₁ + p₂ = ⟨p₁.byteIdx + p₂.byteIdx⟩ := rfl
-
-@[simp] theorem sub_byteIdx (p₁ p₂ : Pos) : (p₁ - p₂).byteIdx = p₁.byteIdx - p₂.byteIdx := rfl
-
-theorem sub_eq (p₁ p₂ : Pos) : p₁ - p₂ = ⟨p₁.byteIdx - p₂.byteIdx⟩ := rfl
-
-@[simp] theorem addChar_byteIdx (p : Pos) (c : Char) : (p + c).byteIdx = p.byteIdx + csize c := rfl
-
-theorem addChar_eq (p : Pos) (c : Char) : p + c = ⟨p.byteIdx + csize c⟩ := rfl
-
-theorem zero_addChar_byteIdx (c : Char) : ((0 : Pos) + c).byteIdx = csize c := by
-  simp only [addChar_byteIdx, byteIdx_zero, Nat.zero_add]
-
-theorem zero_addChar_eq (c : Char) : (0 : Pos) + c = ⟨csize c⟩ := by rw [← zero_addChar_byteIdx]
-
-theorem addChar_right_comm (p : Pos) (c₁ c₂ : Char) : p + c₁ + c₂ = p + c₂ + c₁ := by
-  apply ext
-  repeat rw [pos_add_char]
-  apply Nat.add_right_comm
+attribute [ext] ext
 
 theorem lt_addChar (p : Pos) (c : Char) : p < p + c := Nat.lt_add_of_pos_right (csize_pos _)
 
-theorem ne_of_lt {i₁ i₂ : Pos} (h : i₁ < i₂) : i₁ ≠ i₂ := mt ext_iff.1 (Nat.ne_of_lt h)
-
-theorem ne_of_gt {i₁ i₂ : Pos} (h : i₁ < i₂) : i₂ ≠ i₁ := (ne_of_lt h).symm
-
-@[simp] theorem addString_byteIdx (p : Pos) (s : String) :
-    (p + s).byteIdx = p.byteIdx + s.utf8ByteSize := rfl
-
-theorem addString_eq (p : Pos) (s : String) : p + s = ⟨p.byteIdx + s.utf8ByteSize⟩ := rfl
-
-theorem zero_addString_byteIdx (s : String) : ((0 : Pos) + s).byteIdx = s.utf8ByteSize := by
-  simp only [addString_byteIdx, byteIdx_zero, Nat.zero_add]
-
 private theorem zero_ne_addChar {i : Pos} {c : Char} : 0 ≠ i + c :=
   ne_of_lt add_csize_pos
 
-theorem zero_addString_eq (s : String) : (0 : Pos) + s = ⟨s.utf8ByteSize⟩ := by
-  rw [← zero_addString_byteIdx]
-
-theorem le_iff {i₁ i₂ : Pos} : i₁ ≤ i₂ ↔ i₁.byteIdx ≤ i₂.byteIdx := .rfl
-
-@[simp] theorem mk_le_mk {i₁ i₂ : Nat} : Pos.mk i₁ ≤ Pos.mk i₂ ↔ i₁ ≤ i₂ := .rfl
-
-theorem lt_iff {i₁ i₂ : Pos} : i₁ < i₂ ↔ i₁.byteIdx < i₂.byteIdx := .rfl
-
-@[simp] theorem mk_lt_mk {i₁ i₂ : Nat} : Pos.mk i₁ < Pos.mk i₂ ↔ i₁ < i₂ := .rfl
-
 /-- A string position is valid if it is equal to the UTF-8 length of an initial substring of `s`. -/
 def Valid (s : String) (p : Pos) : Prop :=
   ∃ cs cs', cs ++ cs' = s.1 ∧ p.1 = utf8Len cs
@@ -262,8 +177,6 @@ theorem utf8GetAux?_of_valid (cs cs' : List Char) {i p : Nat} (hp : i + utf8Len
 theorem get?_of_valid (cs cs' : List Char) : get? ⟨cs ++ cs'⟩ ⟨utf8Len cs⟩ = cs'.head? :=
   utf8GetAux?_of_valid _ _ (Nat.zero_add _)
 
-@[simp] theorem get!_eq_get (s : String) (p : Pos) : get! s p = get s p := rfl
-
 theorem utf8SetAux_of_valid (c' : Char) (cs cs' : List Char) {i p : Nat} (hp : i + utf8Len cs = p) :
     utf8SetAux c' (cs ++ cs') ⟨i⟩ ⟨p⟩ = cs ++ cs'.modifyHead fun _ => c' := by
   match cs, cs' with
@@ -290,8 +203,6 @@ theorem next_of_valid' (cs cs' : List Char) :
 theorem next_of_valid (cs : List Char) (c : Char) (cs' : List Char) :
     next ⟨cs ++ c :: cs'⟩ ⟨utf8Len cs⟩ = ⟨utf8Len cs + csize c⟩ := next_of_valid' ..
 
-theorem lt_next' (s : String) (p : Pos) : p < next s p := lt_next ..
-
 @[simp] theorem atEnd_iff (s : String) (p : Pos) : atEnd s p ↔ s.endPos ≤ p :=
   decide_eq_true_iff _
 
@@ -325,8 +236,6 @@ theorem prev_of_valid' (cs cs' : List Char) :
   | _, .inl rfl => rfl
   | _, .inr ⟨cs, c, rfl⟩ => simp [prev_of_valid]
 
-@[simp] theorem prev_zero (s : String) : prev s 0 = 0 := rfl
-
 theorem front_eq (s : String) : front s = s.1.headD default := by
   unfold front; exact get_of_valid [] s.1
 
@@ -340,10 +249,6 @@ theorem atEnd_of_valid (cs : List Char) (cs' : List Char) :
   rw [atEnd_iff]
   cases cs' <;> simp [Nat.lt_add_of_pos_right add_csize_pos]
 
-@[simp] theorem get'_eq (s : String) (p : Pos) (h) : get' s p h = get s p := rfl
-
-@[simp] theorem next'_eq (s : String) (p : Pos) (h) : next' s p h = next s p := rfl
-
 unseal posOfAux findAux in
 theorem posOfAux_eq (s c) : posOfAux s c = findAux s (· == c) := rfl
 
@@ -518,16 +423,8 @@ theorem join_eq (ss : List String) : join ss = ⟨(ss.map data).join⟩ := go ss
 @[simp] theorem data_join (ss : List String) : (join ss).data = (ss.map data).join := by
   rw [join_eq]
 
-theorem singleton_eq (c : Char) : singleton c = ⟨[c]⟩ := rfl
-
-@[simp] theorem data_singleton (c : Char) : (singleton c).data = [c] := rfl
-
-@[simp] theorem append_nil (s : String) : s ++ "" = s := ext (List.append_nil _)
-
-@[simp] theorem nil_append (s : String) : "" ++ s = s := rfl
-
-theorem append_assoc (s₁ s₂ s₃ : String) : (s₁ ++ s₂) ++ s₃ = s₁ ++ (s₂ ++ s₃) :=
-  ext (List.append_assoc ..)
+@[deprecated (since := "2024-06-06")] alias append_nil := append_empty
+@[deprecated (since := "2024-06-06")] alias nil_append := empty_append
 
 namespace Iterator
 
@@ -803,12 +700,6 @@ open String
 
 namespace Substring
 
-@[simp] theorem prev_zero (s : Substring) : s.prev 0 = 0 := by simp [prev, Pos.add_eq]
-
-@[simp] theorem prevn_zero (s : Substring) : ∀ n, s.prevn n 0 = 0
-  | 0 => rfl
-  | n+1 => by simp [prevn, prevn_zero s n]
-
 /-- Validity for a substring. -/
 structure Valid (s : Substring) : Prop where
   /-- The start position of a valid substring is valid. -/