From fedfc22c53ceedce939824875807ba4952744f7e Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Thu, 26 Feb 2026 16:05:41 +0100
Subject: [PATCH] feat: lemmas for `String.intercalate` (#12707)

This PR adds lemmas about `String.intercalate` and
`String.Slice.intercalate`.
---
 src/Init/Data/String/Lemmas.lean             |  1 +
 src/Init/Data/String/Lemmas/Intercalate.lean | 70 ++++++++++++++++++++
 2 files changed, 71 insertions(+)
 create mode 100644 src/Init/Data/String/Lemmas/Intercalate.lean

diff --git a/src/Init/Data/String/Lemmas.lean b/src/Init/Data/String/Lemmas.lean
index b53f0b32bc..3918ce6a6c 100644
--- a/src/Init/Data/String/Lemmas.lean
+++ b/src/Init/Data/String/Lemmas.lean
@@ -16,6 +16,7 @@ public import Init.Data.String.Lemmas.IsEmpty
 public import Init.Data.String.Lemmas.Pattern
 public import Init.Data.String.Lemmas.Slice
 public import Init.Data.String.Lemmas.Iterate
+public import Init.Data.String.Lemmas.Intercalate
 import Init.Data.Order.Lemmas
 public import Init.Data.String.Basic
 import Init.Data.Char.Lemmas
diff --git a/src/Init/Data/String/Lemmas/Intercalate.lean b/src/Init/Data/String/Lemmas/Intercalate.lean
new file mode 100644
index 0000000000..6ccc83bb81
--- /dev/null
+++ b/src/Init/Data/String/Lemmas/Intercalate.lean
@@ -0,0 +1,70 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.String.Defs
+import all Init.Data.String.Defs
+public import Init.Data.String.Slice
+import all Init.Data.String.Slice
+
+public section
+
+namespace String
+
+@[simp]
+theorem intercalate_nil {s : String} : s.intercalate [] = "" := by
+  simp [intercalate]
+
+@[simp]
+theorem intercalate_singleton {s t : String} : s.intercalate [t] = t := by
+  simp [intercalate, intercalate.go]
+
+private theorem intercalateGo_append {s t u : String} {l : List String} :
+    intercalate.go (s ++ t) u l = s ++ intercalate.go t u l := by
+  induction l generalizing t <;> simp [intercalate.go, String.append_assoc, *]
+
+@[simp]
+theorem intercalate_cons_cons {s t u : String} {l : List String} :
+    s.intercalate (t :: u :: l) = t ++ s ++ s.intercalate (u :: l) := by
+  simp [intercalate, intercalate.go, intercalateGo_append]
+
+@[simp]
+theorem intercalate_cons_append {s t u : String} {l : List String} :
+    s.intercalate ((t ++ u) :: l) = t ++ s.intercalate (u :: l) := by
+  cases l <;> simp [String.append_assoc]
+
+theorem intercalate_cons_of_ne_nil {s t : String} {l : List String} (h : l ≠ []) :
+    s.intercalate (t :: l) = t ++ s ++ s.intercalate l :=
+  match l, h with
+  | u::l, _ => by simp
+
+@[simp]
+theorem toList_intercalate {s : String} {l : List String} :
+    (s.intercalate l).toList = s.toList.intercalate (l.map String.toList) := by
+  induction l with
+  | nil => simp
+  | cons hd tl ih => cases tl <;> simp_all
+
+namespace Slice
+
+@[simp]
+theorem _root_.String.appendSlice_eq {s : String} {t : Slice} : s ++ t = s ++ t.copy := rfl
+
+private theorem intercalateGo_append {s t : String} {u : Slice} {l : List Slice} :
+    intercalate.go (s ++ t) u l = s ++ intercalate.go t u l := by
+  induction l generalizing t <;> simp [intercalate.go, String.append_assoc, *]
+
+@[simp]
+theorem intercalate_eq {s : Slice} {l : List Slice} :
+    s.intercalate l = s.copy.intercalate (l.map Slice.copy) := by
+  induction l with
+  | nil => simp [intercalate]
+  | cons hd tl ih => cases tl <;> simp_all [intercalate, intercalate.go, intercalateGo_append]
+
+end Slice
+
+end String