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.

.github/workflows/build-template.yml

@@ -33,7 +33,7 @@ jobs:
         include: ${{fromJson(inputs.config)}}
       # complete all jobs
       fail-fast: false
-    runs-on: ${{ endsWith(matrix.os, '-with-cache') && fromJSON(format('["{0}", "nscloud-git-mirror-1gb"]', matrix.os)) || matrix.os }}
+    runs-on: ${{ endsWith(matrix.os, '-with-cache') && fromJSON(format('["{0}", "nscloud-git-mirror-5gb"]', matrix.os)) || matrix.os }}
     defaults:
       run:
         shell: ${{ matrix.shell || 'nix develop -c bash -euxo pipefail {0}' }}

.github/workflows/check-empty-pr.yml

@@ -0,0 +1,29 @@
+name: Check for empty PR
+
+on:
+  merge_group:
+  pull_request:
+
+jobs:
+  check-empty-pr:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v6
+      with:
+        ref: ${{ github.event_name == 'pull_request' && github.event.pull_request.head.sha || github.sha }}
+        fetch-depth: 0
+        filter: tree:0
+
+    - name: Check for empty diff
+      run: |
+        if [[ "${{ github.event_name }}" == "pull_request" ]]; then
+          base=$(git merge-base "origin/${{ github.base_ref }}" HEAD)
+        else
+          base=$(git rev-parse HEAD^1)
+        fi
+        if git diff --quiet "$base" HEAD --; then
+          echo "This PR introduces no changes compared to its base branch." | tee "$GITHUB_STEP_SUMMARY"
+          echo "It may be a duplicate of an already-merged PR." | tee -a "$GITHUB_STEP_SUMMARY"
+          exit 1
+        fi
+      shell: bash

script/release_checklist.py

@@ -236,7 +236,7 @@ def parse_version(version_str):
 def is_version_gte(version1, version2):
     """Check if version1 >= version2, including proper handling of release candidates."""
     # Check if version1 is a nightly toolchain
-    if version1.startswith("leanprover/lean4:nightly-"):
+    if version1.startswith("leanprover/lean4:nightly-") or version1.startswith("leanprover/lean4-nightly:"):
         return False
     return parse_version(version1) >= parse_version(version2)
 

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/Iter.lean

@@ -6,29 +6,5 @@ Authors: Markus Himmel
 module
 
 prelude
-public import Init.Data.Iterators.Combinators.FilterMap
-public import Init.Data.Iterators.Consumers.Collect
-
-set_option doc.verso true
-
-namespace Std
-
-/--
-Convenience function for turning an iterator into a list of strings, provided the output of the
-iterator implements {name}`ToString`.
--/
-@[inline]
-public abbrev Iter.toStringList {α β : Type} [Iterator α Id β] [ToString β]
-    (it : Iter (α := α) β) : List String :=
-  it.map toString |>.toList
-
-/--
-Convenience function for turning an iterator into an array of strings, provided the output of the
-iterator implements {name}`ToString`.
--/
-@[inline]
-public abbrev Iter.toStringArray {α β : Type} [Iterator α Id β] [ToString β]
-    (it : Iter (α := α) β) : Array String :=
-  it.map toString |>.toArray
-
-end Std
+public import Init.Data.String.Iter.Basic
+public import Init.Data.String.Iter.Intercalate

src/Init/Data/String/Iter/Basic.lean

@@ -0,0 +1,34 @@
+/-
+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.Iterators.Combinators.FilterMap
+public import Init.Data.Iterators.Consumers.Collect
+
+set_option doc.verso true
+
+namespace Std
+
+/--
+Convenience function for turning an iterator into a list of strings, provided the output of the
+iterator implements {name}`ToString`.
+-/
+@[inline]
+public abbrev Iter.toStringList {α β : Type} [Iterator α Id β] [ToString β]
+    (it : Iter (α := α) β) : List String :=
+  it.map toString |>.toList
+
+/--
+Convenience function for turning an iterator into an array of strings, provided the output of the
+iterator implements {name}`ToString`.
+-/
+@[inline]
+public abbrev Iter.toStringArray {α β : Type} [Iterator α Id β] [ToString β]
+    (it : Iter (α := α) β) : Array String :=
+  it.map toString |>.toArray
+
+end Std

src/Init/Data/String/Iter/Intercalate.lean

@@ -0,0 +1,36 @@
+/-
+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.Iterators.Combinators.Monadic.FilterMap
+public import Init.Data.String.Basic
+import Init.Data.String.Slice
+
+set_option doc.verso true
+
+namespace Std
+
+/--
+Appends all the elements in the iterator, in order.
+-/
+public def Iter.joinString {α β : Type} [Iterator α Id β] [IteratorLoop α Id Id] [ToString β]
+    (it : Std.Iter (α := α) β) : String :=
+  (it.map toString).fold (init := "") (· ++ ·)
+
+/--
+Appends the elements of the iterator into a string, placing the separator {name}`s` between them.
+-/
+@[inline]
+public def Iter.intercalateString {α β : Type} [Iterator α Id β] [IteratorLoop α Id Id] [ToString β]
+    (s : String.Slice) (it : Std.Iter (α := α) β) : String :=
+  it.map toString
+    |>.fold (init := none) (fun
+      | none, sl => some sl
+      | some str, sl => some (str ++ s ++ sl))
+    |>.getD ""
+
+end Std

src/Init/Data/String/Lemmas.lean

@@ -17,6 +17,8 @@ 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
+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/Intercalate.lean

@@ -10,6 +10,7 @@ public import Init.Data.String.Defs
 import all Init.Data.String.Defs
 public import Init.Data.String.Slice
 import all Init.Data.String.Slice
+import Init.ByCases
 
 public section
 
@@ -42,6 +43,16 @@ theorem intercalate_cons_of_ne_nil {s t : String} {l : List String} (h : l ≠ [
   match l, h with
   | u::l, _ => by simp
 
+theorem intercalate_append_of_ne_nil {l m : List String} {s : String} (hl : l ≠ []) (hm : m ≠ []) :
+    s.intercalate (l ++ m) = s.intercalate l ++ s ++ s.intercalate m := by
+  induction l with
+  | nil => simp_all
+  | cons hd tl ih =>
+    rw [List.cons_append, intercalate_cons_of_ne_nil (by simp_all)]
+    by_cases ht : tl = []
+    · simp_all
+    · simp [ih ht, intercalate_cons_of_ne_nil ht, String.append_assoc]
+
 @[simp]
 theorem toList_intercalate {s : String} {l : List String} :
     (s.intercalate l).toList = s.toList.intercalate (l.map String.toList) := by

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

@@ -0,0 +1,51 @@
+/-
+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.Iter.Intercalate
+public import Init.Data.String.Slice
+import all Init.Data.String.Iter.Intercalate
+import all Init.Data.String.Defs
+import Init.Data.String.Lemmas.Intercalate
+import Init.Data.Iterators.Lemmas.Consumers.Loop
+import Init.Data.Iterators.Lemmas.Combinators.FilterMap
+
+namespace Std.Iter
+
+@[simp]
+public theorem joinString_eq {α β : Type} [Std.Iterator α Id β] [Std.Iterators.Finite α Id]
+    [Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id] [ToString β]
+    {it : Std.Iter (α := α) β} : it.joinString = String.join (it.toList.map toString) := by
+  rw [joinString, String.join, ← foldl_toList, toList_map]
+
+@[simp]
+public theorem intercalateString_eq {α β : Type} [Std.Iterator α Id β] [Std.Iterators.Finite α Id]
+    [Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id] [ToString β] {s : String.Slice}
+    {it : Std.Iter (α := α) β} :
+    it.intercalateString s = s.copy.intercalate (it.toList.map toString) := by
+  simp only [intercalateString, String.appendSlice_eq, ← foldl_toList, toList_map]
+  generalize s.copy = s
+  suffices ∀ (l m : List String),
+      (l.foldl (init := if m = [] then none else some (s.intercalate m))
+        (fun | none, sl => some sl | some str, sl => some (str ++ s ++ sl))).getD ""
+        = s.intercalate (m ++ l) by
+    simpa [-foldl_toList] using this (it.toList.map toString) []
+  intro l m
+  induction l generalizing m with
+  | nil => cases m <;> simp
+  | cons hd tl ih =>
+    rw [List.append_cons, ← ih, List.foldl_cons]
+    congr
+    simp only [List.append_eq_nil_iff, List.cons_ne_self, and_false, ↓reduceIte]
+    match m with
+    | [] => simp
+    | x::xs =>
+      simp only [reduceCtorEq, ↓reduceIte, List.cons_append, Option.some.injEq]
+      rw [← List.cons_append, String.intercalate_append_of_ne_nil (by simp) (by simp),
+        String.intercalate_singleton]
+
+end Std.Iter

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

@@ -11,7 +11,7 @@ public import Init.Data.Ord.Basic
 public import Init.Data.Iterators.Combinators.FilterMap
 public import Init.Data.String.ToSlice
 public import Init.Data.String.Subslice
-public import Init.Data.String.Iter
+public import Init.Data.String.Iter.Basic
 public import Init.Data.String.Iterate
 import Init.Data.Iterators.Consumers.Collect
 import Init.Data.Iterators.Consumers.Loop
@@ -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

src/Init/Grind/Interactive.lean

@@ -107,6 +107,9 @@ syntax (name := showLocalThms) "show_local_thms" : grind
 -/
 syntax (name := showTerm) "show_term " grindSeq : grind
 
+/-- Shows the pending goals. -/
+syntax (name := showGoals) "show_goals" : grind
+
 declare_syntax_cat grind_ref (behavior := both)
 
 syntax:max anchor : grind_ref
@@ -205,7 +208,7 @@ macro:1 x:grind tk:" <;> " y:grind:2 : grind => `(grind|
     with_annotate_state $tk skip
     all_goals $y:grind)
 
-/-- `first | tac | ...` runs each `tac` until one succeeds, or else fails. -/
+/-- `first (tac) ...` runs each `tac` until one succeeds, or else fails. -/
 syntax (name := first) "first " withPosition((ppDedent(ppLine) colGe "(" grindSeq ")")+) : grind
 
 /-- `try tac` runs `tac` and succeeds even if `tac` failed. -/
@@ -304,5 +307,19 @@ syntax (name := symInternalizeAll) "internalize_all" : grind
 Only available in `sym =>` mode. -/
 syntax (name := symByContra) "by_contra" : grind
 
+/--
+`simp` applies the structural simplifier to the goal target.
+Only available in `sym =>` mode.
+
+- `simp` — uses the default (identity) variant
+- `simp myVariant` — uses a named variant registered via `register_sym_simp`
+- `simp [thm₁, thm₂, ...]` — default variant with extra rewrite theorems appended to `post`
+- `simp myVariant [thm₁, thm₂, ...]` — named variant with extra theorems
+-/
+syntax (name := symSimp) "simp" (ppSpace colGt ident)? (" [" ident,* "]")? : grind
+
+/-- `exact e` closes the main goal if its target type matches that of `e`. -/
+macro "exact " e:term : grind => `(grind| tactic => exact $e:term)
+
 end Grind
 end Lean.Parser.Tactic

src/Init/Sym/Simp/SimprocDSL.lean

@@ -49,6 +49,14 @@ syntax (name := ground) "ground" : sym_simproc
 /-- Simplify telescope binders but not the final body. -/
 syntax (name := telescope) "telescope" : sym_simproc
 
+/-- Simplify control-flow expressions (`if-then-else`, `match`, `cond`, `dite`).
+Visits only conditions and discriminants. Intended as a `pre` simproc. -/
+syntax (name := control) "control" : sym_simproc
+
+/-- Simplify arrow telescopes (`p₁ → p₂ → ... → q`) without entering binders.
+Simplifies each `pᵢ` and `q` individually. Intended as a `pre` simproc. -/
+syntax (name := arrowTelescope) "arrow_telescope" : sym_simproc
+
 /-- Rewrite using a named theorem set. Optionally specify a discharger for conditional rewrites. -/
 syntax (name := rewriteSet) "rewrite" ident (" with " sym_discharger)? : sym_simproc
 

src/Init/Tactics.lean

@@ -524,9 +524,6 @@ syntax location := withPosition(ppGroup(" at" (locationWildcard <|> locationHyp)
 -/
 syntax (name := change) "change " term (location)? : tactic
 
-@[tactic_alt change]
-syntax (name := changeWith) "change " term " with " term (location)? : tactic
-
 /--
 `show t` finds the first goal whose target unifies with `t`. It makes that the main goal,
 performs the unification, and replaces the target with the unified version of `t`.

src/Lean/Compiler/LCNF/InferBorrow.lean

@@ -213,6 +213,8 @@ inductive OwnReason where
   | jpArgPropagation (jpFVar : FVarId)
   /-- Tail call preservation at a join point jump. -/
   | jpTailCallPreservation (jpFVar : FVarId)
+  /-- Annotated as an owned parameter (currently only triggerable through `@[export]`)-/
+  | ownedAnnotation
 
 def OwnReason.toString (reason : OwnReason) : CompilerM String := do
   PP.run do
@@ -229,6 +231,7 @@ def OwnReason.toString (reason : OwnReason) : CompilerM String := do
     | .tailCallPreservation funcName => return s!"tail call preservation of {funcName}"
     | .jpArgPropagation jpFVar => return s!"backward propagation from JP {← PP.ppFVar jpFVar}"
     | .jpTailCallPreservation jpFVar => return s!"JP tail call preservation {← PP.ppFVar jpFVar}"
+    | .ownedAnnotation => return s!"Annotated as owned"
 
 /--
 Determine whether an `OwnReason` is necessary for correctness (forced) or just an optimization
@@ -245,7 +248,7 @@ def OwnReason.isForced (reason : OwnReason) : Bool :=
   | .constructorResult .. | .functionCallResult ..
   -- We cannot pass borrowed values to reset or have borrow annotations destroy tail calls for
   -- correctness reasons.
-  | .resetReuse .. | .tailCallPreservation .. | .jpTailCallPreservation ..
+  | .resetReuse .. | .tailCallPreservation .. | .jpTailCallPreservation .. | .ownedAnnotation
   | .forwardProjectionProp .. | .backwardProjectionProp .. => true
 
 /--
@@ -256,10 +259,19 @@ partial def infer (decls : Array (Decl .impure)) : CompilerM ParamMap := do
   return map.paramMap
 where
   go : InferM Unit := do
+    for (_, params) in (← get).paramMap.map do
+      for param in params do
+        if !param.borrow && param.type.isPossibleRef then
+          -- if the param already disqualifies as borrow now this is because of an annotation
+          ownFVar param.fvarId .ownedAnnotation
+    modify fun s => { s with modified := false }
+    loop
+
+  loop : InferM Unit := do
     step
     if (← get).modified then
       modify fun s => { s with modified := false }
-      go
+      loop
     else
       return ()
 

src/Lean/Elab/BuiltinTerm.lean

@@ -329,7 +329,8 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
   let inst ← if backward.inferInstanceAs.wrap.get (← getOptions) then
     -- Normalize to instance normal form.
     let logCompileErrors := !(← read).isNoncomputableSection && !(← read).declName?.any (Lean.isNoncomputable (← getEnv))
-    withNewMCtxDepth <| normalizeInstance inst expectedType (logCompileErrors := logCompileErrors)
+    let isMeta := (← read).isMetaSection
+    withNewMCtxDepth <| normalizeInstance inst expectedType (logCompileErrors := logCompileErrors) (isMeta := isMeta)
   else
     pure inst
   ensureHasType expectedType? inst

src/Lean/Elab/Command.lean

@@ -666,7 +666,8 @@ private def mkTermContext (ctx : Context) (s : State) : CommandElabM Term.Contex
   return {
     macroStack             := ctx.macroStack
     sectionVars            := sectionVars
-    isNoncomputableSection := scope.isNoncomputable }
+    isNoncomputableSection := scope.isNoncomputable
+    isMetaSection          := scope.isMeta }
 
 /--
 Lift the `TermElabM` monadic action `x` into a `CommandElabM` monadic action.

src/Lean/Elab/Deriving/Basic.lean

@@ -220,10 +220,12 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) (isNoncomputable
             instName ← liftMacroM <| mkUnusedBaseName instName
             if isPrivateName declName then
               instName := mkPrivateName env instName
+            let isMeta := (← read).isMetaSection
             let inst ← if backward.inferInstanceAs.wrap.get (← getOptions) then
               withDeclNameForAuxNaming instName <| withNewMCtxDepth <|
                 normalizeInstance result.instVal result.instType
                   (logCompileErrors := false)  -- covered by noncomputable check below
+                  (isMeta := isMeta)
             else
               pure result.instVal
             let closure ← Closure.mkValueTypeClosure result.instType inst (zetaDelta := true)

src/Lean/Elab/Tactic/Grind/Basic.lean

@@ -10,6 +10,7 @@ public import Lean.Meta.Tactic.Grind.Main
 import Lean.Meta.Tactic.Grind.Intro
 public import Lean.Meta.Sym.Apply
 public import Lean.Meta.Sym.Util
+public import Lean.Meta.Sym.Simp.SimpM
 import Init.Omega
 public section
 namespace Lean.Elab.Tactic.Grind
@@ -24,11 +25,25 @@ structure Context extends Tactic.Context where
 
 open Meta.Grind (Goal)
 
+/-- An extra theorem passed to `simp` in `sym =>` mode. -/
+inductive ExtraTheorem where
+  | const (declName : Name)
+  | fvar  (fvarId : FVarId)
+  deriving BEq, Hashable
+
+/-- Cache key for `Sym.simp` variant invocations. -/
+structure SimpCacheKey where
+  variant : Name
+  extras  : Array ExtraTheorem
+  deriving BEq, Hashable
+
 structure Cache where
   /-- Cache for `BackwardRule`s created from declaration names (sym mode only). -/
   backwardRuleName : PHashMap Name Sym.BackwardRule := {}
   /-- Cache for `BackwardRule`s created from elaborated terms, keyed by syntax byte position range (sym mode only). -/
   backwardRuleSyntax : PHashMap (Nat × Nat) Sym.BackwardRule := {}
+  /-- Per-variant persistent `Sym.simp` cache. Keyed by variant name + extra theorem names. -/
+  simpState : Std.HashMap SimpCacheKey Sym.Simp.State := {}
 
 structure State where
   symState   : Meta.Sym.State

src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean

@@ -76,6 +76,10 @@ def evalGrindSeq : GrindTactic := fun stx =>
 @[builtin_grind_tactic skip] def evalSkip : GrindTactic := fun _ =>
   return ()
 
+@[builtin_grind_tactic showGoals] def evalShowGoals : GrindTactic := fun _ => do
+  let goals ← getUnsolvedGoalMVarIds
+  addRawTrace (goalsToMessageData goals)
+
 @[builtin_grind_tactic paren] def evalParen : GrindTactic := fun stx =>
   evalGrindTactic stx[1]
 

src/Lean/Elab/Tactic/Grind/RegisterSymSimp.lean

@@ -7,14 +7,42 @@ module
 prelude
 import Init.Sym.Simp.SimprocDSL
 import Lean.Meta.Sym.Simp.Variant
+import Lean.Elab.Tactic.Grind.SimprocDSL
 import Lean.Elab.Command
 namespace Lean.Elab.Command
 open Meta Sym.Simp
 
+/--
+Runs a `GrindTacticM` computation in a minimal context for validation.
+-/
+def withGrindTacticM (k : Tactic.Grind.GrindTacticM α) : CommandElabM α := do
+  liftTermElabM do
+  let params ← Grind.mkDefaultParams {}
+  let (ctx, state) ← Grind.GrindM.run (params := params) do
+    let methods ← Grind.getMethods
+    let grindCtx ← readThe Meta.Grind.Context
+    let symCtx ← readThe Sym.Context
+    let grindState ← get
+    let symState ← getThe Sym.State
+    let ctx := {
+      elaborator := `registerSymSimp,
+      ctx := grindCtx, sctx := symCtx, methods, params
+    }
+    return (ctx, { grindState, symState, goals := [] })
+  let (a, _) ← Tactic.Grind.GrindTacticM.run k ctx state
+  return a
+
+def validateOptionSimprocSyntax (proc? : Option Syntax) : CommandElabM Unit := do
+  let some proc := proc? | return ()
+  discard <| withGrindTacticM <| Tactic.Grind.elabSymSimproc proc
+
 @[builtin_command_elab Lean.Parser.Command.registerSymSimp]
 def elabRegisterSymSimp : CommandElab := fun stx => do
   let id := stx[1]
   let name := id.getId
+  -- Check for duplicate variant
+  if (getSymSimpVariant? (← getEnv) name).isSome then
+    throwErrorAt id "Sym.simp variant `{name}` is already registered"
   let fields := stx[3].getArgs
   let mut pre? : Option Syntax := none
   let mut post? : Option Syntax := none
@@ -35,7 +63,10 @@ def elabRegisterSymSimp : CommandElab := fun stx => do
       unless post?.isNone do throwErrorAt field "duplicate `post` field"
       post? := some proc
     | _ => throwErrorAt field "unexpected field"
-  let config :=  { maxSteps := maxSteps?.getD 100_000, maxDischargeDepth := maxDischargeDepth?.getD 2 }
+  -- Validate pre/post by elaborating them
+  validateOptionSimprocSyntax pre?
+  validateOptionSimprocSyntax post?
+  let config := { maxSteps := maxSteps?.getD 100_000, maxDischargeDepth := maxDischargeDepth?.getD 2 }
   let variant : SymSimpVariant := { pre?, post?, config }
   modifyEnv fun env => symSimpVariantExtension.addEntry env { name, variant }
 

src/Lean/Elab/Tactic/Grind/SimprocDSLBuiltin.lean

@@ -9,6 +9,8 @@ import Lean.Elab.Tactic.Grind.SimprocDSL
 import Init.Sym.Simp.SimprocDSL
 import Lean.Meta.Sym.Simp.EvalGround
 import Lean.Meta.Sym.Simp.Telescope
+import Lean.Meta.Sym.Simp.ControlFlow
+import Lean.Meta.Sym.Simp.Forall
 import Lean.Meta.Sym.Simp.Rewrite
 namespace Lean.Elab.Tactic.Grind
 open Meta Sym.Simp
@@ -23,6 +25,14 @@ def elabSimprocGround : SymSimprocElab := fun _ =>
 def elabSimprocTelescope : SymSimprocElab := fun _ =>
   return simpTelescope
 
+@[builtin_sym_simproc Lean.Parser.Sym.Simp.control]
+def elabSimprocControl : SymSimprocElab := fun _ =>
+  return simpControl
+
+@[builtin_sym_simproc Lean.Parser.Sym.Simp.arrowTelescope]
+def elabSimprocArrowTelescope : SymSimprocElab := fun _ =>
+  return simpArrowTelescope
+
 @[builtin_sym_simproc self]
 def elabSimprocSelf : SymSimprocElab := fun _ =>
   return simp

src/Lean/Elab/Tactic/Grind/Sym.lean

@@ -6,7 +6,15 @@ Authors: Leonardo de Moura
 module
 prelude
 import Lean.Elab.Tactic.Grind.Basic
+import Lean.Elab.Tactic.Grind.SimprocDSL
 import Lean.Meta.Sym.Grind
+import Lean.Meta.Sym.Simp.Variant
+import Lean.Meta.Sym.Simp.Rewrite
+import Lean.Meta.Sym.Simp.EvalGround
+import Lean.Meta.Sym.Simp.Goal
+import Lean.Meta.Sym.Simp.Attr
+import Lean.Meta.Sym.Simp.ControlFlow
+import Lean.Meta.Sym.Simp.Forall
 import Lean.Meta.Tactic.Apply
 import Lean.Elab.SyntheticMVars
 namespace Lean.Elab.Tactic.Grind
@@ -135,4 +143,75 @@ private def getOrCreateBackwardRuleFromTerm (term : Syntax) : GrindTacticM Sym.B
   let goal ← liftGrindM <| Grind.Goal.internalizeAll goal
   replaceMainGoal [goal]
 
+section
+open Sym.Simp
+
+def trivialSimproc : Simproc := fun _ =>
+  return .rfl
+
+def elabOptSimproc (stx? : Option Syntax) : GrindTacticM Simproc := do
+  let some stx := stx? | return trivialSimproc
+  elabSymSimproc stx
+
+def resolveExtraTheorems (ids? :  Option (Array (TSyntax `ident))) : GrindTacticM (Array ExtraTheorem × Array Theorem) := do
+  let some ids := ids? | return (#[], #[])
+  let mut extras := #[]
+  let mut thms := #[]
+  let lctx ← getLCtx
+  for id in ids do
+    if let some decl := lctx.findFromUserName? id.getId then
+      extras := extras.push <| .fvar decl.fvarId
+      thms := thms.push (← mkTheoremFromExpr decl.toExpr)
+    else
+      let declName ← realizeGlobalConstNoOverload id
+      extras := extras.push <| .const declName
+      thms := thms.push (← mkTheoremFromDecl declName)
+  return (extras, thms)
+
+def addExtraTheorems (post : Simproc) (extraThms : Array Theorem) : GrindTacticM Simproc := do
+  if extraThms.isEmpty then return post
+  let mut thms : Theorems := {}
+  for thm in extraThms do
+    thms := thms.insert thm
+  return post >> thms.rewrite
+
+def mkDefaultMethods (extraThms : Array Theorem) : GrindTacticM Sym.Simp.Methods := do
+  let thms ← getSymSimpTheorems
+  let pre := simpControl >> simpArrowTelescope
+  let post ← addExtraTheorems (evalGround >> thms.rewrite) extraThms
+  return { pre, post }
+
+def elabVariant (variantName : Name) (extraThms : Array Theorem) : GrindTacticM (Sym.Simp.Methods × Sym.Simp.Config) := do
+  if variantName.isAnonymous then
+    return (← mkDefaultMethods extraThms, {})
+  let some v := getSymSimpVariant? (← getEnv) variantName
+    | throwError "unknown Sym.simp variant `{variantName}`"
+  let pre ← elabOptSimproc v.pre?
+  let post ← addExtraTheorems (← elabOptSimproc v.post?) extraThms
+  return ({ pre, post}, v.config)
+
+@[builtin_grind_tactic Parser.Tactic.Grind.symSimp] def evalSymSimp : GrindTactic := fun stx => withMainContext do
+  ensureSym
+  let `(grind| simp $[$variantId?]? $[[ $[$extraIds],* ]]?) := stx | throwUnsupportedSyntax
+  -- Resolve variant
+  let variantName := variantId?.map (·.getId) |>.getD .anonymous
+  -- Resolve extra theorems (local hypotheses first, then global constants)
+  let (extras, thms) ← resolveExtraTheorems extraIds
+  -- Cache lookup/creation
+  let cacheKey : SimpCacheKey := { variant := variantName, extras }
+  let simpState := (← get).cache.simpState[cacheKey]?.getD {}
+  let (methods, config) ← elabVariant variantName thms
+  let goal ← getMainGoal
+  let (simpResult, simpState) ← liftGrindM <| goal.withContext do
+    Sym.Simp.SimpM.run (Sym.Simp.simp (← goal.mvarId.getType)) methods config simpState
+  -- Save updated cache
+  modify fun s => { s with cache.simpState := s.cache.simpState.insert cacheKey simpState }
+  -- Apply result to goal
+  match (← liftGrindM <| Sym.Simp.Result.toSimpGoalResult simpResult goal.mvarId) with
+  | .closed => replaceMainGoal []
+  | .goal mvarId => replaceMainGoal [{ goal with mvarId }]
+  | .noProgress => throwError "`Sym.simp` made no progress"
+
+end
+
 end Lean.Elab.Tactic.Grind

src/Lean/Elab/Term/TermElabM.lean

@@ -309,6 +309,8 @@ structure Context where
   heedElabAsElim     : Bool            := true
   /-- Noncomputable sections automatically add the `noncomputable` modifier to any declaration we cannot generate code for. -/
   isNoncomputableSection : Bool        := false
+  /-- `true` when inside a `meta section`. -/
+  isMetaSection : Bool                 := false
   /-- When `true` we skip TC failures. We use this option when processing patterns. -/
   ignoreTCFailures : Bool := false
   /-- `true` when elaborating patterns. It affects how we elaborate named holes. -/

src/Lean/Meta/InstanceNormalForm.lean

@@ -99,7 +99,7 @@ Normalize an instance value to "instance normal form".
 See the module docstring for the full algorithm specification.
 -/
 partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true)
-    (logCompileErrors : Bool := true) : MetaM Expr := withTransparency .instances do
+    (logCompileErrors : Bool := true) (isMeta : Bool := false) : MetaM Expr := withTransparency .instances do
   withTraceNode `Meta.instanceNormalForm
       (fun _ => return m!"type: {expectedType}") do
   let some className ← isClass? expectedType
@@ -124,9 +124,11 @@ partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true
             return inst
           else
             let name ← mkAuxDeclName
-            let wrapped ← mkAuxDefinition name expectedType inst (compile := compile)
-              (logCompileErrors := logCompileErrors)
+            let wrapped ← mkAuxDefinition name expectedType inst (compile := false)
             setReducibilityStatus name .implicitReducible
+            if isMeta then modifyEnv (markMeta · name)
+            if compile then
+              compileDecls (logErrors := logCompileErrors) #[name]
             enableRealizationsForConst name
             return wrapped
         else
@@ -169,7 +171,7 @@ partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true
             catch _ => pure ()
 
           mvarId.assign (← normalizeInstance arg argExpectedType (compile := compile)
-            (logCompileErrors := logCompileErrors))
+            (logCompileErrors := logCompileErrors) (isMeta := isMeta))
         else
           -- For data fields, assign directly or wrap in aux def to fix types.
           if backward.inferInstanceAs.wrap.data.get (← getOptions) then
@@ -180,6 +182,7 @@ partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true
               let name ← mkAuxDeclName
               mvarId.assign (← mkAuxDefinition name argExpectedType arg (compile := false))
               setInlineAttribute name
+              if isMeta then modifyEnv (markMeta · name)
               if compile then
                 compileDecls (logErrors := logCompileErrors) #[name]
               enableRealizationsForConst name

src/Lean/Meta/Sym/Simp/Rewrite.lean

@@ -9,6 +9,7 @@ public import Lean.Meta.Sym.Simp.Simproc
 public import Lean.Meta.Sym.Simp.Theorems
 public import Lean.Meta.Sym.Simp.App
 public import Lean.Meta.Sym.Simp.Discharger
+import Lean.Meta.ACLt
 import Lean.Meta.Sym.InstantiateS
 import Lean.Meta.Sym.InstantiateMVarsS
 import Init.Data.Range.Polymorphic.Iterators
@@ -71,10 +72,16 @@ public def Theorem.rewrite (thm : Theorem) (e : Expr) (d : Discharger := dischar
     let expr  ← instantiateRevBetaS rhs args.toArray
     if isSameExpr e expr then
       return mkRflResultCD isCD
+    else if !(← checkPerm thm.perm e expr) then
+      return mkRflResultCD isCD
     else
       return .step expr proof (contextDependent := isCD)
   else
     return .rfl
+where
+  checkPerm (perm : Bool) (e result : Expr) : MetaM Bool := do
+    if !perm then return true
+    acLt result e
 
 public def Theorems.rewrite (thms : Theorems) (d : Discharger := dischargeNone) : Simproc := fun e => do
   -- Track `cd` across all attempted theorems. If theorem A fails with cd=true

src/Lean/Meta/Sym/Simp/Theorems.lean

@@ -8,7 +8,9 @@ prelude
 public import Lean.Meta.Sym.Pattern
 public import Lean.Meta.DiscrTree
 import Lean.Meta.Sym.Simp.DiscrTree
+import Lean.Meta.AppBuilder
 import Lean.ExtraModUses
+import Init.Omega
 public section
 namespace Lean.Meta.Sym.Simp
 
@@ -25,6 +27,10 @@ structure Theorem where
   pattern : Pattern
   /-- Right-hand side of the equation. -/
   rhs     : Expr
+  /-- If `true`, the theorem is a permutation rule (e.g., `x + y = y + x`).
+  Rewriting is only applied when the result is strictly less than the input
+  (using `acLt`), preventing infinite loops. -/
+  perm    : Bool := false
   deriving Inhabited
 
 instance : BEq Theorem where
@@ -44,9 +50,112 @@ def Theorems.getMatch (thms : Theorems) (e : Expr) : Array Theorem :=
 def Theorems.getMatchWithExtra (thms : Theorems) (e : Expr) : Array (Theorem × Nat) :=
   Sym.getMatchWithExtra thms.thms e
 
+/--
+Check whether `lhs` and `rhs` (with `numVars` pattern variables represented as `.bvar` indices
+`≥ 0` before any binder entry) are permutations of each other — same structure with only
+pattern variable indices rearranged via a consistent bijection.
+
+Bvars with index `< offset` are "local" (introduced by binders inside the pattern) and must
+match exactly. Bvars with index `≥ offset` are pattern variables and may be permuted,
+but the mapping must be a bijection.
+
+Simplified compared to `Meta.simp`'s `isPerm`:
+- Uses de Bruijn indices instead of metavariables
+- No `.proj` (folded into applications) or `.letE` (zeta-expanded) cases
+-/
+private abbrev IsPermM := ReaderT Nat $ StateT (Array (Option Nat)) $ Except Unit
+
+private partial def isPermAux (a b : Expr) : IsPermM Unit := do
+  match a, b with
+  | .bvar i, .bvar j =>
+    let offset ← read
+    if i < offset && j < offset then
+      unless i == j do throw ()
+    else if i >= offset && j >= offset then
+      let pi := i - offset
+      let pj := j - offset
+      let fwd ← get
+      if h : pi >= fwd.size then throw () else
+      match fwd[pi] with
+      | none =>
+        -- Check injectivity: pj must not already be a target of another mapping
+        if fwd.contains (some pj) then throw ()
+        set (fwd.set pi (some pj))
+      | some pj' => unless pj == pj' do throw ()
+    else throw ()
+  | .app f₁ a₁, .app f₂ a₂ => isPermAux f₁ f₂; isPermAux a₁ a₂
+  | .mdata _ s, t => isPermAux s t
+  | s, .mdata _ t => isPermAux s t
+  | .forallE _ d₁ b₁ _, .forallE _ d₂ b₂ _ => isPermAux d₁ d₂; withReader (· + 1) (isPermAux b₁ b₂)
+  | .lam _ d₁ b₁ _, .lam _ d₂ b₂ _ => isPermAux d₁ d₂; withReader (· + 1) (isPermAux b₁ b₂)
+  | s, t => unless s == t do throw ()
+
+def isPerm (numVars : Nat) (lhs rhs : Expr) : Bool :=
+  ((isPermAux lhs rhs).run 0 |>.run (Array.replicate numVars none)) matches .ok _
+
+/-- Describes how a theorem's conclusion was adapted to an equality for use in `Sym.simp`. -/
+private inductive EqAdaptation where
+  /-- Already an equality `lhs = rhs`. Proof is used as-is. -/
+  | eq
+  /-- Was `¬ p`. Proof `h` adapted to `eq_false h : p = False`. -/
+  | eqFalse
+  /-- Was `p ↔ q`. Proof `h` adapted to `propext h : p = q`. -/
+  | iff
+  /-- Was a proposition `p`. Proof `h` adapted to `eq_true h : p = True`. -/
+  | eqTrue
+
+/--
+Analyze the conclusion of a theorem type and extract `(lhs, rhs)` for use as a
+rewrite rule in `Sym.simp`. Handles:
+- `lhs = rhs` — used as-is
+- `¬ p` — adapted to `p = False`
+- `p ↔ q` — adapted to `p = q`
+- `p` (proposition) — adapted to `p = True`
+-/
+private def selectEqKey (type : Expr) : MetaM (Expr × Expr × EqAdaptation) := do
+  match_expr type with
+  | Eq _ lhs rhs => return (lhs, rhs, .eq)
+  | Not p => return (p, mkConst ``False, .eqFalse)
+  | Iff lhs rhs => return (lhs, rhs, .iff)
+  | _ =>
+    unless (← isProp type) do
+      throwError "cannot use as a simp theorem, conclusion is not a proposition{indentExpr type}"
+    return (type, mkConst ``True, .eqTrue)
+
+/--
+Wrap a proof expression according to the adaptation applied to its type.
+Given a proof `h : <original type>`, returns a proof of the adapted equality.
+This wrapping must be applied AFTER the proof has been applied to its quantified arguments.
+-/
+private def wrapProof (numVars : Nat) (expr : Expr) (adaptation : EqAdaptation) : MetaM Expr :=
+  match adaptation with
+  | .eq => return expr
+  | .eqFalse =>
+    wrapInner numVars expr fun h => mkAppM ``eq_false #[h]
+  | .iff =>
+    wrapInner numVars expr fun h => mkAppM ``propext #[h]
+  | .eqTrue =>
+    wrapInner numVars expr fun h => mkAppM ``eq_true #[h]
+where
+  /-- Wraps the innermost application of `expr` (after `numVars` arguments) with `wrap`. -/
+  wrapInner (numVars : Nat) (expr : Expr) (wrap : Expr → MetaM Expr) : MetaM Expr := do
+    let type ← inferType expr
+    forallBoundedTelescope type numVars fun xs _ => do
+      let h := mkAppN expr xs
+      mkLambdaFVars xs (← wrap h)
+
 def mkTheoremFromDecl (declName : Name) : MetaM Theorem := do
-  let (pattern, rhs) ← mkEqPatternFromDecl declName
-  return { expr := mkConst declName, pattern, rhs }
+  let (pattern, (rhs, adaptation)) ← mkPatternFromDeclWithKey declName selectEqKey
+  let expr ← wrapProof pattern.varTypes.size (mkConst declName) adaptation
+  let perm := isPerm pattern.varTypes.size pattern.pattern rhs
+  return { expr, pattern, rhs, perm }
+
+/-- Create a `Theorem` from a proof expression. Handles equalities, `¬`, `↔`, and propositions. -/
+def mkTheoremFromExpr (e : Expr) : MetaM Theorem := do
+  let (pattern, (rhs, adaptation)) ← mkPatternFromExprWithKey e [] selectEqKey
+  let expr ← wrapProof pattern.varTypes.size e adaptation
+  let perm := isPerm pattern.varTypes.size pattern.pattern rhs
+  return { expr, pattern, rhs, perm }
 
 /--
 Environment extension storing a set of `Sym.Simp` theorems.

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean

@@ -52,6 +52,12 @@ builtin_dsimproc [simp, seval] reduceSingleton (String.singleton _) := fun e =>
   let some c ← Char.fromExpr? e.appArg! | return .continue
   return .done <| toExpr (String.singleton c)
 
+builtin_dsimproc_decl reduceToSingleton ((_ : String)) := fun e => do
+  let some s ← fromExpr? e | return .continue
+  let l := s.toList
+  let [c] := l | return .continue
+  return .done <| mkApp (mkConst ``String.singleton) (toExpr c)
+
 @[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

src/Std/Data/String/ToInt.lean

@@ -98,18 +98,34 @@ end Slice
 public theorem isInt_toSlice {s : String} : s.toSlice.isInt = s.isInt :=
   (rfl)
 
+@[simp]
+public theorem isInt_comp_toSlice : String.Slice.isInt ∘ String.toSlice = String.isInt := by
+  ext; simp
+
 @[simp]
 public theorem toInt?_toSlice {s : String} : s.toSlice.toInt? = s.toInt? :=
   (rfl)
 
+@[simp]
+public theorem toInt?_comp_toSlice : String.Slice.toInt? ∘ String.toSlice = String.toInt? := by
+  ext; simp
+
 @[simp]
 public theorem Slice.isInt_copy {s : Slice} : s.copy.isInt = s.isInt := by
   simpa [← isInt_toSlice] using Slice.isInt_congr (by simp)
 
+@[simp]
+public theorem Slice.isInt_comp_copy : String.isInt ∘ String.Slice.copy = String.Slice.isInt := by
+  ext; simp
+
 @[simp]
 public theorem Slice.toInt?_copy {s : Slice} : s.copy.toInt? = s.toInt? := by
   simpa [← isInt_toSlice] using Slice.toInt?_congr (by simp)
 
+@[simp]
+public theorem Slice.toInt?_comp_copy : String.toInt? ∘ String.Slice.copy = String.Slice.toInt? := by
+  ext; simp
+
 public theorem toInt?_eq_some_iff {s : String} {a : Int} :
     s.toInt? = some a ↔ (∃ b, s.toNat? = some b ∧ a = (b : Int)) ∨ ∃ t, s = "-" ++ t ∧ ∃ b, t.toNat? = some b ∧ a = -(b : Int) := by
   simp [← toInt?_toSlice, Slice.toInt?_eq_some_iff]

src/Std/Data/String/ToNat.lean

@@ -221,18 +221,34 @@ namespace String
 public theorem isNat_toSlice {s : String} : s.toSlice.isNat = s.isNat :=
   (rfl)
 
+@[simp]
+public theorem isNat_comp_toSlice : String.Slice.isNat ∘ String.toSlice = String.isNat := by
+  ext; simp
+
 @[simp]
 public theorem toNat?_toSlice {s : String} : s.toSlice.toNat? = s.toNat? :=
   (rfl)
 
+@[simp]
+public theorem toNat?_comp_toSlice : String.Slice.toNat? ∘ String.toSlice = String.toNat? := by
+  ext; simp
+
 @[simp]
 public theorem Slice.isNat_copy {s : Slice} : s.copy.isNat = s.isNat := by
   simpa [← isNat_toSlice] using Slice.isNat_congr (by simp)
 
+@[simp]
+public theorem Slice.isNat_comp_copy : String.isNat ∘ String.Slice.copy = String.Slice.isNat := by
+  ext; simp
+
 @[simp]
 public theorem Slice.toNat?_copy {s : Slice} : s.copy.toNat? = s.toNat? := by
   simpa [← isNat_toSlice] using Slice.toNat?_congr (by simp)
 
+@[simp]
+public theorem Slice.toNat?_comp_copy : String.toNat? ∘ String.Slice.copy = String.Slice.toNat? := by
+  ext; simp
+
 public theorem isNat_iff {s : String} :
     s.isNat = true ↔
       s ≠ "" ∧