From fcdd9d1ae821497aeaedaae9bfd94f976d538d35 Mon Sep 17 00:00:00 2001
From: Markus Himmel <2065352+TwoFX@users.noreply.github.com>
Date: Mon, 23 Mar 2026 12:10:00 +0100
Subject: [PATCH] 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                    |  5 +++++
 src/Init/Data/String/Lemmas.lean          |  1 +
 src/Init/Data/String/Lemmas/Hashable.lean | 25 +++++++++++++++++++++++
 src/Init/Data/String/Lemmas/Slice.lean    |  3 +++
 src/Init/Data/String/Slice.lean           |  5 +++--
 tests/elab/string_slice.lean              |  4 ++++
 6 files changed, 41 insertions(+), 2 deletions(-)
 create mode 100644 src/Init/Data/String/Lemmas/Hashable.lean

diff --git a/src/Init/Data/BEq.lean b/src/Init/Data/BEq.lean
index 6f0d377241..23d3a4a74f 100644
--- a/src/Init/Data/BEq.lean
+++ b/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))
diff --git a/src/Init/Data/String/Lemmas.lean b/src/Init/Data/String/Lemmas.lean
index 59783b8adf..57ce958d8f 100644
--- a/src/Init/Data/String/Lemmas.lean
+++ b/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
diff --git a/src/Init/Data/String/Lemmas/Hashable.lean b/src/Init/Data/String/Lemmas/Hashable.lean
new file mode 100644
index 0000000000..3a7474a2eb
--- /dev/null
+++ b/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
diff --git a/src/Init/Data/String/Lemmas/Slice.lean b/src/Init/Data/String/Lemmas/Slice.lean
index 38abed8fb2..132b13ab4a 100644
--- a/src/Init/Data/String/Lemmas/Slice.lean
+++ b/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
diff --git a/src/Init/Data/String/Slice.lean b/src/Init/Data/String/Slice.lean
index 1048ae1121..e93ff45759 100644
--- a/src/Init/Data/String/Slice.lean
+++ b/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
diff --git a/tests/elab/string_slice.lean b/tests/elab/string_slice.lean
index fe0e0387e5..2ff7962b7e 100644
--- a/tests/elab/string_slice.lean
+++ b/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