From 47833725eaded4cec8cc7944ab656eaf05208da7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= <wojciech@lean-fro.org>
Date: Thu, 12 Mar 2026 11:52:06 +0000
Subject: [PATCH] feat: add `String` simprocs to `cbv` (#12888)

This PR adds `String`-specific simprocs to `cbv` tactic.
---
 .../Tactic/Cbv/BuiltinCbvSimprocs/Array.lean  |  8 +--
 .../Tactic/Cbv/BuiltinCbvSimprocs/String.lean | 53 +++++++++++++++++
 src/Lean/Meta/Tactic/Cbv/Main.lean            |  1 +
 src/Lean/Meta/Tactic/Cbv/Util.lean            |  7 +++
 tests/elab/cbv1.lean                          |  7 +--
 tests/elab/cbv_string.lean                    | 59 +++++++++++++++++++
 6 files changed, 123 insertions(+), 12 deletions(-)
 create mode 100644 src/Lean/Meta/Tactic/Cbv/BuiltinCbvSimprocs/String.lean
 create mode 100644 tests/elab/cbv_string.lean

diff --git a/src/Lean/Meta/Tactic/Cbv/BuiltinCbvSimprocs/Array.lean b/src/Lean/Meta/Tactic/Cbv/BuiltinCbvSimprocs/Array.lean
index 84da3e1b68..4fac0aba03 100644
--- a/src/Lean/Meta/Tactic/Cbv/BuiltinCbvSimprocs/Array.lean
+++ b/src/Lean/Meta/Tactic/Cbv/BuiltinCbvSimprocs/Array.lean
@@ -11,17 +11,11 @@ import Lean.Meta.Sym.LitValues
 import Lean.Meta.Sym.InferType
 import Init.CbvSimproc
 import Lean.Meta.Tactic.Cbv.CbvSimproc
+import Lean.Meta.Tactic.Cbv.Util
 import Init.GetElem
 
 namespace Lean.Meta.Tactic.Cbv
 
-/-- Extract elements from a `List.cons`/`List.nil` chain. -/
-private partial def getListLitElems (e : Expr) (acc : Array Expr := #[]) : Option <| Array Expr :=
-  match_expr e with
-  | List.nil _ => some acc
-  | List.cons _ a as => getListLitElems as <| acc.push a
-  | _ => none
-
 /-- Extract elements from an array literal (`Array.mk` applied to a list literal). -/
 private def getArrayLitElems? (e : Expr) : Option <| Array Expr :=
   match_expr e with
diff --git a/src/Lean/Meta/Tactic/Cbv/BuiltinCbvSimprocs/String.lean b/src/Lean/Meta/Tactic/Cbv/BuiltinCbvSimprocs/String.lean
new file mode 100644
index 0000000000..f56e41032b
--- /dev/null
+++ b/src/Lean/Meta/Tactic/Cbv/BuiltinCbvSimprocs/String.lean
@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+-/
+module
+
+prelude
+import Lean.Meta.Sym.Simp.SimpM
+import Lean.Meta.Sym.LitValues
+import Init.CbvSimproc
+import Lean.Meta.Tactic.Cbv.CbvSimproc
+import Lean.Meta.Tactic.Cbv.Util
+
+namespace Lean.Meta.Tactic.Cbv
+
+/-- Reduce `"abc" ++ "def"` to `"abcdef"` for literal strings. -/
+builtin_cbv_simproc cbv_eval simpStringAppend (@HAppend.hAppend String String String _ _ _) := fun e => do
+  let some a := Sym.getStringValue? e.appFn!.appArg! | return .rfl
+  let some b := Sym.getStringValue? e.appArg! | return .rfl
+  let result ← Sym.share <| toExpr (a ++ b)
+  return .step result (← Sym.mkEqRefl result)
+
+/-- Reduce `String.push "abc" 'd'` to `"abcd"` for literal strings and chars. -/
+builtin_cbv_simproc cbv_eval simpStringPush (String.push _ _) := fun e => do
+  let some s := Sym.getStringValue? e.appFn!.appArg! | return .rfl
+  let some c := Sym.getCharValue? e.appArg! | return .rfl
+  let result ← Sym.share <| toExpr (s.push c)
+  return .step result (← Sym.mkEqRefl result)
+
+/-- Reduce `String.singleton 'a'` to `"a"` for literal chars. -/
+builtin_cbv_simproc cbv_eval simpStringSingleton (String.singleton _) := fun e => do
+  let some c := Sym.getCharValue? e.appArg! | return .rfl
+  let result ← Sym.share <| toExpr (String.singleton c)
+  return .step result (← Sym.mkEqRefl result)
+
+/-- Reduce `String.ofList ['a', 'b', 'c']` to `"abc"` for literal char lists. -/
+builtin_cbv_simproc cbv_eval simpStringOfList (String.ofList _) := fun e => do
+  let some elems := getListLitElems e.appArg! | return .rfl
+  let mut s := ""
+  for elem in elems do
+    let some c := Sym.getCharValue? elem | return .rfl
+    s := s.push c
+  let result ← Sym.share <| toExpr s
+  return .step result (← Sym.mkEqRefl result)
+
+/-- Reduce `String.toList "abc"` to `['a', 'b', 'c']` for literal strings. -/
+builtin_cbv_simproc cbv_eval simpStringToList (String.toList _) := fun e => do
+  let some s := Sym.getStringValue? e.appArg! | return .rfl
+  let result ← Sym.share <| toExpr s.toList
+  return .step result (← Sym.mkEqRefl result)
+
+end Lean.Meta.Tactic.Cbv
diff --git a/src/Lean/Meta/Tactic/Cbv/Main.lean b/src/Lean/Meta/Tactic/Cbv/Main.lean
index ba010c18a1..399ef2799c 100644
--- a/src/Lean/Meta/Tactic/Cbv/Main.lean
+++ b/src/Lean/Meta/Tactic/Cbv/Main.lean
@@ -12,6 +12,7 @@ public import Lean.Meta.Tactic.Cbv.Opaque
 public import Lean.Meta.Tactic.Cbv.ControlFlow
 import Lean.Meta.Tactic.Cbv.BuiltinCbvSimprocs.Core
 import Lean.Meta.Tactic.Cbv.BuiltinCbvSimprocs.Array
+import Lean.Meta.Tactic.Cbv.BuiltinCbvSimprocs.String
 import Lean.Meta.Tactic.Cbv.Util
 import Lean.Meta.Tactic.Cbv.TheoremsLookup
 import Lean.Meta.Tactic.Cbv.CbvEvalExt
diff --git a/src/Lean/Meta/Tactic/Cbv/Util.lean b/src/Lean/Meta/Tactic/Cbv/Util.lean
index 5c53ef5082..5ba0380f15 100644
--- a/src/Lean/Meta/Tactic/Cbv/Util.lean
+++ b/src/Lean/Meta/Tactic/Cbv/Util.lean
@@ -101,4 +101,11 @@ def isProof (e : Expr) : Sym.SymM Bool := do
 public def isProofTerm : Simproc := fun e => do
   return .rfl (← isProof e)
 
+/-- Extract elements from a `List.cons`/`List.nil` chain. -/
+public partial def getListLitElems (e : Expr) (acc : Array Expr := #[]) : Option <| Array Expr :=
+  match_expr e with
+  | List.nil _ => some acc
+  | List.cons _ a as => getListLitElems as <| acc.push a
+  | _ => none
+
 end Lean.Meta.Tactic.Cbv
diff --git a/tests/elab/cbv1.lean b/tests/elab/cbv1.lean
index c1932666e0..ab493972ac 100644
--- a/tests/elab/cbv1.lean
+++ b/tests/elab/cbv1.lean
@@ -106,29 +106,26 @@ example : removeVowels "abcdef" = "bcdf" := by
   conv =>
     lhs
     cbv
-  rfl
 
 example : removeVowels "abcdef\nghijklm" = "bcdf\nghjklm" := by
   conv =>
     lhs
     cbv
-  rfl
+
 example : removeVowels "aaaaa" = "" := by
   conv =>
     lhs
     cbv
-  rfl
+
 example : removeVowels "aaBAA" = "B" := by
   conv =>
     lhs
     cbv
-  rfl
 
 example : removeVowels "zbcd" = "zbcd" := by
   conv =>
     lhs
     cbv
-  rfl
 
 def Nat.factorial : Nat → Nat
   | 0 => 1
diff --git a/tests/elab/cbv_string.lean b/tests/elab/cbv_string.lean
new file mode 100644
index 0000000000..52095a0ea0
--- /dev/null
+++ b/tests/elab/cbv_string.lean
@@ -0,0 +1,59 @@
+import Std
+set_option cbv.warning false
+
+-- String append
+theorem testAppend : "abc" ++ "def" = "abcdef" := by cbv
+
+/--
+info: theorem testAppend : "abc" ++ "def" = "abcdef" :=
+of_eq_true (Eq.trans (congrFun' (congrArg Eq (Eq.refl "abcdef")) "abcdef") (eq_self "abcdef"))
+-/
+#guard_msgs in
+#print testAppend
+
+-- String push
+theorem testPush : String.push "abc" 'd' = "abcd" := by cbv
+
+/--
+info: theorem testPush : "abc".push 'd' = "abcd" :=
+of_eq_true (Eq.trans (congrFun' (congrArg Eq (Eq.refl "abcd")) "abcd") (eq_self "abcd"))
+-/
+#guard_msgs in
+#print testPush
+
+-- String singleton
+theorem testSingleton : String.singleton 'a' = "a" := by cbv
+
+/--
+info: theorem testSingleton : String.singleton 'a' = "a" :=
+of_eq_true (Eq.trans (congrFun' (congrArg Eq (Eq.refl "a")) "a") (eq_self "a"))
+-/
+#guard_msgs in
+#print testSingleton
+
+-- String.ofList
+theorem testOfList : String.ofList ['a', 'b', 'c'] = "abc" := by cbv
+
+/--
+info: theorem testOfList : String.ofList ['a', 'b', 'c'] = "abc" :=
+of_eq_true (Eq.trans (congrFun' (congrArg Eq (Eq.refl "abc")) "abc") (eq_self "abc"))
+-/
+#guard_msgs in
+#print testOfList
+
+-- String.toList
+theorem testToList : String.toList "abc" = ['a', 'b', 'c'] := by cbv
+
+/--
+info: theorem testToList : "abc".toList = ['a', 'b', 'c'] :=
+of_eq_true (Eq.trans (congrFun' (congrArg Eq (Eq.refl ['a', 'b', 'c'])) ['a', 'b', 'c']) (eq_self ['a', 'b', 'c']))
+-/
+#guard_msgs in
+#print testToList
+
+-- Empty string operations
+theorem testAppendEmpty : "" ++ "" = "" := by cbv
+
+theorem testOfListEmpty : String.ofList [] = "" := by cbv
+
+theorem testToListEmpty : String.toList "" = [] := by cbv