feat: EquivBEq and LawfulHashable for String.Slice (#13058)

This PR adds `EquivBEq` and `LawfulHashable` instances to
`String.Slice`.

To this end, we redefine `String.Slice.hash`, which used to be
completely opaque, to be defined as `String.hash s.copy` (and then
`String.hash` remains opaque). We add tests that the `lean_slice_hash`
and `lean_string_hash` functions do indeed satisfy this relationship.

Of course, it would be even better to have a streaming MurmurHash64A
implementation in core that could be used to implement both of these so
that we can avoid the `opaque`, but that is a project for another day.

src/Init/Data/BEq.lean

@@ -66,3 +66,8 @@ theorem BEq.neq_of_beq_of_neq [BEq α] [PartialEquivBEq α] {a b c : α} :
 instance (priority := low) [BEq α] [LawfulBEq α] : EquivBEq α where
   symm h := beq_iff_eq.2 <| Eq.symm <| beq_iff_eq.1 h
   trans hab hbc := beq_iff_eq.2 <| (beq_iff_eq.1 hab).trans <| beq_iff_eq.1 hbc
+
+theorem equivBEq_of_iff_apply_eq [BEq α] (f : α → β) (hf : ∀ a b, a == b ↔ f a = f b) : EquivBEq α where
+  rfl := by simp [hf]
+  symm := by simp [hf, eq_comm]
+  trans hab hbc := (hf _ _).2 (Eq.trans ((hf _ _).1 hab) ((hf _ _).1 hbc))

src/Init/Data/String/Lemmas.lean

@@ -18,6 +18,7 @@ public import Init.Data.String.Lemmas.Slice
 public import Init.Data.String.Lemmas.Iterate
 public import Init.Data.String.Lemmas.Intercalate
 public import Init.Data.String.Lemmas.Iter
+public import Init.Data.String.Lemmas.Hashable
 import Init.Data.Order.Lemmas
 public import Init.Data.String.Basic
 import Init.Data.Char.Lemmas

src/Init/Data/String/Lemmas/Hashable.lean

@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Julia Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.String.Slice
+public import Init.Data.LawfulHashable
+import all Init.Data.String.Slice
+import Init.Data.String.Lemmas.Slice
+
+namespace String
+
+public theorem hash_eq {s : String} : hash s = String.hash s := rfl
+
+namespace Slice
+
+public theorem hash_eq {s : String.Slice} : hash s = String.hash s.copy := (rfl)
+
+public instance : LawfulHashable String.Slice where
+  hash_eq a b hab := by simp [hash_eq, beq_eq_true_iff.1 hab]
+
+end String.Slice

src/Init/Data/String/Lemmas/Slice.lean

@@ -36,6 +36,9 @@ theorem beq_eq_false_iff {s t : Slice} : (s == t) = false ↔ s.copy ≠ t.copy
 theorem beq_eq_decide {s t : Slice} : (s == t) = decide (s.copy = t.copy) := by
   cases h : s == t <;> simp_all
 
+instance : EquivBEq String.Slice :=
+  equivBEq_of_iff_apply_eq copy (by simp)
+
 end BEq
 
 end String.Slice

src/Init/Data/String/Slice.lean

@@ -84,10 +84,11 @@ instance : ToString String.Slice where
 theorem toStringToString_eq : ToString.toString = String.Slice.copy := (rfl)
 
 @[extern "lean_slice_hash"]
-opaque hash (s : @& Slice) : UInt64
+protected def hash (s : @& Slice) : UInt64 :=
+  String.hash s.copy
 
 instance : Hashable Slice where
-  hash := hash
+  hash := Slice.hash
 
 instance : LT Slice where
   lt x y := x.copy < y.copy

tests/elab/string_slice.lean

@@ -263,3 +263,7 @@ example {s : String} : (Id.run do
     List.forIn_pure_yield_eq_foldl, bind_pure, Id.run_pure, ← String.toList_inj]
   suffices ∀ (t : String), (cs.foldl (fun b a => b.push a) t).toList = t.toList ++ cs by simpa using this ""
   induction cs <;> simp_all
+
+example : hash "abc" = hash "abc".toSlice := by native_decide
+example : hash "abc" = hash ("aabc".toSlice.drop 1) := by native_decide
+example : hash "abc" = hash ("aabcc".toSlice.drop 1 |>.take 3) := by native_decide