feat: simprocs for String.toList and String.push (#12642)

TwoFX · web-flow · commit 7b3d778ab047 · 2026-02-23T07:39:27.000Z
This PR adds dsimprocs for reducing `String.toList` and `String.push`.
diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean
@@ -35,6 +35,17 @@ builtin_dsimproc [simp, seval] reduceOfList (String.ofList _) := fun e => do
   unless e.isAppOfArity ``String.ofList 1 do return .continue
   reduceListChar e.appArg! ""
 
+builtin_dsimproc [simp, seval] reduceToList (String.toList _) := fun e => do
+  unless e.isAppOfArity ``String.toList 1 do return .continue
+  let some s ← fromExpr? e.appArg! | return .continue
+  return .done <| toExpr s.toList
+
+builtin_dsimproc [simp, seval] reducePush (String.push _ _) := fun e => do
+  unless e.isAppOfArity ``String.push 2 do return .continue
+  let some n ← fromExpr? e.appFn!.appArg! | return .continue
+  let some m ← Char.fromExpr? e.appArg! | return .continue
+  return .done <| toExpr (n.push m)
+
 @[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : String → String → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← fromExpr? e.appFn!.appArg! | return .continue
diff --git a/tests/lean/run/simprocString.lean b/tests/lean/run/simprocString.lean
@@ -0,0 +1,54 @@
+-- String.reduceAppend
+example : "hello" ++ " " ++ "world" = "hello world" := by simp
+example : "" ++ "a" = "a" := by simp
+example : "a" ++ "" = "a" := by simp
+example : "" ++ "" = "" := by simp
+
+-- String.reduceOfList
+example : String.ofList ['a', 'b', 'c'] = "abc" := by simp
+example : String.ofList [] = "" := by simp
+example : String.ofList ['x'] = "x" := by simp
+
+-- String.reduceToList
+example : "abc".toList = ['a', 'b', 'c'] := by simp
+example : "".toList = [] := by simp
+example : "x".toList = ['x'] := by simp
+example : "hello".toList = ['h', 'e', 'l', 'l', 'o'] := by simp
+
+-- String.reducePush
+example : "abc".push 'd' = "abcd" := by simp
+example : "".push 'a' = "a" := by simp
+
+-- String.reduceEq
+example : "hello" = "hello" := by simp
+example : "hello" = "foo" → False := by simp
+
+-- String.reduceNe
+example : "hello" ≠ "foo" := by simp
+
+-- String.reduceBEq
+example : ("hello" == "hello") = true := by simp
+example : ("hello" == "foo") = false := by simp
+
+-- String.reduceBNe
+example : ("hello" != "foo") = true := by simp
+example : ("hello" != "hello") = false := by simp
+
+-- String.reduceLT
+example : "abc" < "abd" := by simp
+example : "a" < "b" := by simp
+
+-- String.reduceLE
+example : "abc" ≤ "abc" := by simp
+example : "abc" ≤ "abd" := by simp
+
+-- String.reduceGT
+example : "abd" > "abc" := by simp
+example : "b" > "a" := by simp
+
+-- String.reduceGE
+example : "abc" ≥ "abc" := by simp
+example : "abd" ≥ "abc" := by simp
+
+-- Combined: roundtrip toList/ofList
+example : String.ofList "hello".toList = "hello" := by simp
