chore: check for empty PRs in CI (#12956)

This PR adds a CI check that fails when a PR introduces no changes
compared to its base branch. This catches cases where a duplicate PR is
queued for merge after an identical PR has already landed (as happened
with https://github.com/leanprover/lean4/pull/12876 and
https://github.com/leanprover/lean4/pull/12877).

The check is added as a second job in the existing `check-stage0.yml`
workflow, which already has the same trigger conditions and git setup
pattern. On `pull_request` events it diffs against the merge base; on
`merge_group` events it diffs `HEAD^1..HEAD` (the PR's contribution to
the synthetic merge commit). Note that batched merge groups are treated
as a unit — if the entire group is non-empty the check passes, which is
the right behaviour for lean4's typical single-PR queuing.

🤖 Prepared with Claude Code

Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>

.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/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
@@ -315,5 +318,8 @@ Only available in `sym =>` mode.
 -/
 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/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

@@ -25,10 +25,16 @@ structure Context extends Tactic.Context where
 
 open Meta.Grind (Goal)
 
-/-- Cache key for `Sym.simp` variant invocations: variant name + ordered extra theorem names. -/
+/-- 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  : List Name
+  extras  : Array ExtraTheorem
   deriving BEq, Hashable
 
 structure Cache where

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

@@ -153,39 +153,54 @@ def elabOptSimproc (stx? : Option Syntax) : GrindTacticM Simproc := do
   let some stx := stx? | return trivialSimproc
   elabSymSimproc stx
 
-def addExtraTheorems (post : Simproc) (extraNames : Array Name) : GrindTacticM Simproc := do
-  if extraNames.isEmpty then return post
+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 name in extraNames do
-    thms := thms.insert (← mkTheoremFromDecl name)
+  for thm in extraThms do
+    thms := thms.insert thm
   return post >> thms.rewrite
 
-def mkDefaultMethods (extraNames : Array Name) : GrindTacticM Sym.Simp.Methods := do
+def mkDefaultMethods (extraThms : Array Theorem) : GrindTacticM Sym.Simp.Methods := do
   let thms ← getSymSimpTheorems
   let pre := simpControl >> simpArrowTelescope
-  let post ← addExtraTheorems (evalGround >> thms.rewrite) extraNames
+  let post ← addExtraTheorems (evalGround >> thms.rewrite) extraThms
   return { pre, post }
 
-def elabVariant (variantName : Name) (extraNames : Array Name) : GrindTacticM (Sym.Simp.Methods × Sym.Simp.Config) := do
+def elabVariant (variantName : Name) (extraThms : Array Theorem) : GrindTacticM (Sym.Simp.Methods × Sym.Simp.Config) := do
   if variantName.isAnonymous then
-    return (← mkDefaultMethods extraNames, {})
+    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?) extraNames
+  let post ← addExtraTheorems (← elabOptSimproc v.post?) extraThms
   return ({ pre, post}, v.config)
 
-@[builtin_grind_tactic Parser.Tactic.Grind.symSimp] def evalSymSimp : GrindTactic := fun stx => do
+@[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
-  -- Compose extra theorems into post
-  let extraNames ← (extraIds.getD #[]).mapM fun id => realizeGlobalConstNoOverload id
+  -- Resolve extra theorems (local hypotheses first, then global constants)
+  let (extras, thms) ← resolveExtraTheorems extraIds
   -- Cache lookup/creation
-  let cacheKey : SimpCacheKey := { variant := variantName, extras := extraNames.toList }
+  let cacheKey : SimpCacheKey := { variant := variantName, extras }
   let simpState := (← get).cache.simpState[cacheKey]?.getD {}
-  let (methods, config) ← elabVariant variantName extraNames
+  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

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.

tests/elab/12897.lean

@@ -0,0 +1,12 @@
+-- Tests that `inferInstanceAs` auxiliary definitions are properly marked `meta`
+-- when used inside a `meta` section.
+
+module
+
+meta section
+
+def Foo := List Nat
+
+instance : EmptyCollection Foo := inferInstanceAs (EmptyCollection (List Nat))
+
+end

tests/elab/sym_simp_adapt1.lean

@@ -0,0 +1,99 @@
+import Lean
+set_option linter.unusedVariables false
+set_option warn.sorry false
+/-! Tests for `mkTheoremFromDecl` adaptation of non-equality theorems -/
+
+opaque p : Nat → Prop
+opaque q : Nat → Prop
+
+-- Equality theorem (no adaptation needed)
+theorem eq_thm : p x = q x := sorry
+
+-- Negation theorem: `¬ p x` adapted to `p x = False`
+theorem neg_thm : ¬ p x := sorry
+
+-- Iff theorem: `p x ↔ q x` adapted to `p x = q x`
+theorem iff_thm : p x ↔ q x := sorry
+
+-- Proposition theorem: `p x` adapted to `p x = True`
+theorem prop_thm : p x := sorry
+
+-- Quantified negation: `∀ x, ¬ p x` adapted to `∀ x, p x = False`
+theorem quant_neg : ∀ x, ¬ p x := sorry
+
+-- Quantified prop: `∀ x, p x` adapted to `∀ x, p x = True`
+theorem quant_prop : ∀ x, p x := sorry
+
+-- Test: `simp` with a proposition theorem (`h : p x`) rewrites `p x` to `True`
+register_sym_simp propSimp where
+  post := ground >> rewrite [prop_thm]
+
+example : p x = True := by
+  sym => simp propSimp
+
+-- Test: `simp` with a negation theorem (`h : ¬ p x`) rewrites `p x` to `False`
+register_sym_simp negSimp where
+  post := ground >> rewrite [neg_thm]
+
+example : p x = False := by
+  sym => simp negSimp
+
+-- Test: `simp` with an iff theorem (`h : p x ↔ q x`) rewrites `p x` to `q x`
+register_sym_simp iffSimp where
+  post := ground >> rewrite [iff_thm]
+
+example : p x = q x := by
+  sym => simp iffSimp
+
+-- Test: quantified prop still works
+register_sym_simp quantPropSimp where
+  post := ground >> rewrite [quant_prop]
+
+example (y : Nat) : p y = True := by
+  sym => simp quantPropSimp
+
+-- Test: quantified negation still works
+register_sym_simp quantNegSimp where
+  post := ground >> rewrite [quant_neg]
+
+example (y : Nat) : p y = False := by
+  sym => simp quantNegSimp
+
+register_sym_simp simple where
+  post := ground
+
+example (x : Nat) : p x := by
+  sym => simp simple [quant_prop]
+
+example (x : Nat) : ¬ p x := by
+  sym => simp simple [quant_neg]
+
+example (x : Nat) : p x = q x := by
+  sym => simp simple [iff_thm]
+
+-- Tests for local hypothesis support in `simp [h]`
+
+-- Local hypothesis `h : p x` rewrites `p x` to `True`
+example (x : Nat) (h : p x) : p x = True := by
+  sym => simp simple [h]
+
+-- Local hypothesis `h : ¬ p x` rewrites `p x` to `False`
+example (x : Nat) (h : ¬ p x) : p x = False := by
+  sym => simp simple [h]
+
+-- Local hypothesis `h : p x ↔ q x` rewrites `p x` to `q x`
+example (x : Nat) (h : p x ↔ q x) : p x = q x := by
+  sym => simp simple [h]
+
+-- Local hypothesis `h : p x = q x` (already an equality)
+example (x : Nat) (h : p x = q x) : p x = q x := by
+  sym => simp simple [h]
+
+-- Local hypothesis with intro
+example (x : Nat) : p x → p x = True := by
+  sym =>
+    intro h
+    simp simple [h]
+
+example (h : ∀ x, p x = q x) : p a = q a ∧ p b = q b := by
+  sym => simp simple [h, and_true]

tests/elab/sym_simp_cd.lean

@@ -42,153 +42,120 @@ example : 2 + 3 = 5 := by
 -- and lands in the transient cache. On the second invocation, the transient cache is
 -- cleared, so there should be NO persistent cache hit for the overall expression.
 -- Only context-independent sub-expressions (literals, fvars) get persistent cache hits.
-theorem Nat.add_comm_of_pos (a b : Nat) (_h : 0 < a) : a + b = b + a := Nat.add_comm a b
+opaque f : Nat → Nat
+axiom f_idem (a : Nat) (_h : 0 < a) : f (f a) = f a
 
 set_option trace.sym.simp.debug.cache true in
 /--
-trace: [sym.simp.debug.cache] persistent cache hit: 2
-[sym.simp.debug.cache] persistent cache hit: n
-[sym.simp.debug.cache] transient cache hit: 2 + n
+trace: [sym.simp.debug.cache] persistent cache hit: f n
+[sym.simp.debug.cache] transient cache hit: f (f n)
+[sym.simp.debug.cache] persistent cache hit: f n
 [sym.simp.debug.cache] second traversal
-[sym.simp.debug.cache] persistent cache hit: n
-[sym.simp.debug.cache] persistent cache hit: 2
-[sym.simp.debug.cache] persistent cache hit: 2
-[sym.simp.debug.cache] persistent cache hit: n
-[sym.simp.debug.cache] transient cache hit: 2 + n
+[sym.simp.debug.cache] persistent cache hit: f n
+[sym.simp.debug.cache] persistent cache hit: f n
+[sym.simp.debug.cache] transient cache hit: f (f n)
+[sym.simp.debug.cache] persistent cache hit: f n
 -/
 #guard_msgs in
-example (n : Nat) (h : 0 < n) : n + 2 = 2 + n := by
-  sym_simp_twice [Nat.add_comm_of_pos]
+example (n : Nat) (h : 0 < n) : f (f n) = f (f (f n)) := by
+  sym_simp_twice [f_idem]
 
 -- Test 3: Congruence — cd propagates through function application.
--- `n + 2` rewrites context-dependently (cd=true), `3 + 4` evaluates ground (cd=false).
--- The congruence combines both, so the overall result is cd=true.
--- On second traversal: ground sub-expressions (`3 + 4`, `7`) hit persistent cache,
--- but cd-tainted expressions (`2 + n`, `2 + n + 7`) are only in transient.
 set_option trace.sym.simp.debug.cache true in
 /--
-trace: [sym.simp.debug.cache] persistent cache hit: 2
-[sym.simp.debug.cache] persistent cache hit: n
-[sym.simp.debug.cache] transient cache hit: 2 + n
-[sym.simp.debug.cache] transient cache hit: (2 + n) * 7
+trace: [sym.simp.debug.cache] persistent cache hit: f n
+[sym.simp.debug.cache] persistent cache hit: f n
+[sym.simp.debug.cache] persistent cache hit: f n + 7
 [sym.simp.debug.cache] second traversal
-[sym.simp.debug.cache] persistent cache hit: n
-[sym.simp.debug.cache] persistent cache hit: 2
-[sym.simp.debug.cache] persistent cache hit: 2
-[sym.simp.debug.cache] persistent cache hit: n
+[sym.simp.debug.cache] persistent cache hit: f n
+[sym.simp.debug.cache] persistent cache hit: f n
 [sym.simp.debug.cache] persistent cache hit: 3 + 4
-[sym.simp.debug.cache] transient cache hit: 2 + n
-[sym.simp.debug.cache] persistent cache hit: 7
-[sym.simp.debug.cache] transient cache hit: (2 + n) * 7
+[sym.simp.debug.cache] persistent cache hit: f n + 7
+[sym.simp.debug.cache] persistent cache hit: f n + 7
 -/
 #guard_msgs in
-example (n : Nat) (h : 0 < n) : (n + 2) * (3 + 4) = (2 + n) * 7 := by
-  sym_simp_twice [Nat.add_comm_of_pos]
+example (n : Nat) (h : 0 < n) : f (f n) + (3 + 4) = f n + 7 := by
+  sym_simp_twice [f_idem]
 
--- Similar to previous test, but `Nat.add_comm_of_pos` is not applicable, but discharger must return `cd := true`.
+-- Similar to previous test, but `f_idem` is not applicable (no hypothesis), but discharger must return `cd := true`.
 set_option trace.sym.simp.debug.cache true in
 /--
-trace: [sym.simp.debug.cache] transient cache hit: n + 2
-[sym.simp.debug.cache] transient cache hit: (n + 2) * 7
+trace: [sym.simp.debug.cache] transient cache hit: f (f n)
+[sym.simp.debug.cache] transient cache hit: f (f n) + 7
 [sym.simp.debug.cache] second traversal
-[sym.simp.debug.cache] persistent cache hit: n
-[sym.simp.debug.cache] persistent cache hit: 2
+[sym.simp.debug.cache] persistent cache hit: f n
 [sym.simp.debug.cache] persistent cache hit: 3 + 4
-[sym.simp.debug.cache] transient cache hit: n + 2
+[sym.simp.debug.cache] transient cache hit: f (f n)
 [sym.simp.debug.cache] persistent cache hit: 7
-[sym.simp.debug.cache] transient cache hit: (n + 2) * 7
+[sym.simp.debug.cache] transient cache hit: f (f n) + 7
 -/
 #guard_msgs in
-example (n : Nat) : (n + 2) * (3 + 4) = (n + 2) * 7 := by
-  sym_simp_twice [Nat.add_comm_of_pos]
+example (n : Nat) : f (f n) + (3 + 4) = f (f n) + 7 := by
+  sym_simp_twice [f_idem]
 
 -- Test 4: Arrow — cd propagates through implication.
--- The hypothesis `n + 2 = 2 + n` is simplified context-dependently to `True`.
--- `True → True` simplifies to `True`. The whole result is cd=true.
--- `True` hits persistent cache; `2 + n` is only in transient.
 set_option trace.sym.simp.debug.cache true in
 /--
-trace: [sym.simp.debug.cache] persistent cache hit: 2
-[sym.simp.debug.cache] persistent cache hit: n
-[sym.simp.debug.cache] transient cache hit: 2 + n
+trace: [sym.simp.debug.cache] persistent cache hit: f n
+[sym.simp.debug.cache] persistent cache hit: f n
 [sym.simp.debug.cache] second traversal
-[sym.simp.debug.cache] persistent cache hit: n
-[sym.simp.debug.cache] persistent cache hit: 2
-[sym.simp.debug.cache] persistent cache hit: 2
-[sym.simp.debug.cache] persistent cache hit: n
-[sym.simp.debug.cache] transient cache hit: 2 + n
+[sym.simp.debug.cache] persistent cache hit: f n
+[sym.simp.debug.cache] persistent cache hit: f n
+[sym.simp.debug.cache] persistent cache hit: f n
 [sym.simp.debug.cache] persistent cache hit: True
 -/
 #guard_msgs in
 set_option linter.unusedVariables false in
-example (n : Nat) (h : 0 < n) : (n + 2 = 2 + n) → True := by
-  sym_simp_twice [Nat.add_comm_of_pos]
+example (n : Nat) (h : 0 < n) : (f (f n) = f n) → True := by
+  sym_simp_twice [f_idem]
 
 -- Test 5: Lambda — cd propagates through funext.
--- Body `n + 2` is simplified context-dependently inside the binder.
--- `withFreshTransientCache` clears the transient cache on binder entry.
--- The lambda result `fun x => 2 + n` is only in transient.
 set_option trace.sym.simp.debug.cache true in
 /--
-trace: [sym.simp.debug.cache] persistent cache hit: 2
-[sym.simp.debug.cache] persistent cache hit: n
-[sym.simp.debug.cache] persistent cache hit: 2
-[sym.simp.debug.cache] persistent cache hit: n
-[sym.simp.debug.cache] transient cache hit: fun x => 2 + n
+trace: [sym.simp.debug.cache] persistent cache hit: f n
+[sym.simp.debug.cache] persistent cache hit: f n
+[sym.simp.debug.cache] persistent cache hit: fun x => f n
 [sym.simp.debug.cache] second traversal
-[sym.simp.debug.cache] persistent cache hit: n
-[sym.simp.debug.cache] persistent cache hit: 2
-[sym.simp.debug.cache] persistent cache hit: 2
-[sym.simp.debug.cache] persistent cache hit: n
-[sym.simp.debug.cache] persistent cache hit: 2
-[sym.simp.debug.cache] persistent cache hit: n
-[sym.simp.debug.cache] transient cache hit: fun x => 2 + n
+[sym.simp.debug.cache] persistent cache hit: f n
+[sym.simp.debug.cache] persistent cache hit: f n
+[sym.simp.debug.cache] persistent cache hit: fun x => f n
+[sym.simp.debug.cache] persistent cache hit: fun x => f n
 -/
 #guard_msgs in
-example (n : Nat) (_h : 0 < n) : (fun _ : Nat => n + 2) = (fun _ : Nat => 2 + n) := by
-  sym_simp_twice [Nat.add_comm_of_pos]
+example (n : Nat) (_h : 0 < n) : (fun _ : Nat => f (f n)) = (fun _ : Nat => f n) := by
+  sym_simp_twice [f_idem]
 
 -- Test 6: Control flow — cd propagates through `ite` condition.
--- The condition `n + 2 = 2 + n` is simplified context-dependently.
--- The `ite` result inherits cd, and `1` (ground) is in persistent cache.
 set_option trace.sym.simp.debug.cache true in
 /--
-trace: [sym.simp.debug.cache] persistent cache hit: 2
-[sym.simp.debug.cache] persistent cache hit: n
-[sym.simp.debug.cache] transient cache hit: 2 + n
+trace: [sym.simp.debug.cache] persistent cache hit: f n
+[sym.simp.debug.cache] persistent cache hit: f n
 [sym.simp.debug.cache] persistent cache hit: 1
 [sym.simp.debug.cache] second traversal
-[sym.simp.debug.cache] persistent cache hit: n
-[sym.simp.debug.cache] persistent cache hit: 2
-[sym.simp.debug.cache] persistent cache hit: 2
-[sym.simp.debug.cache] persistent cache hit: n
-[sym.simp.debug.cache] transient cache hit: 2 + n
+[sym.simp.debug.cache] persistent cache hit: f n
+[sym.simp.debug.cache] persistent cache hit: f n
+[sym.simp.debug.cache] persistent cache hit: f n
 [sym.simp.debug.cache] persistent cache hit: 1
 [sym.simp.debug.cache] persistent cache hit: 1
 -/
 #guard_msgs in
-example (n : Nat) (h : 0 < n) : (if n + 2 = 2 + n then 1 else 0) = 1 := by
-  sym_simp_twice [Nat.add_comm_of_pos]
+example (n : Nat) (h : 0 < n) : (if f (f n) = f n then 1 else 0) = 1 := by
+  sym_simp_twice [f_idem]
 
 -- Test 7: Dependent forall — body cd under binder with `withFreshTransientCache`.
--- Simplifying `∀ (m : Nat), n + 2 = 2 + n` enters a binder (for `m`).
--- The transient cache is cleared on binder entry (`withFreshTransientCache`).
--- The body uses a cd rewrite, so the overall result is cd=true.
--- After "second traversal": `Nat` (the binder type) hits persistent cache.
 set_option trace.sym.simp.debug.cache true in
 /--
-trace: [sym.simp.debug.cache] persistent cache hit: 2
-[sym.simp.debug.cache] persistent cache hit: n
-[sym.simp.debug.cache] transient cache hit: 2 + n
+trace: [sym.simp.debug.cache] persistent cache hit: f n
+[sym.simp.debug.cache] transient cache hit: f (f n)
+[sym.simp.debug.cache] persistent cache hit: f n
 [sym.simp.debug.cache] second traversal
 [sym.simp.debug.cache] persistent cache hit: Nat
-[sym.simp.debug.cache] persistent cache hit: n
-[sym.simp.debug.cache] persistent cache hit: 2
-[sym.simp.debug.cache] persistent cache hit: 2
-[sym.simp.debug.cache] persistent cache hit: n
-[sym.simp.debug.cache] transient cache hit: 2 + n
+[sym.simp.debug.cache] persistent cache hit: f n
+[sym.simp.debug.cache] persistent cache hit: f n
+[sym.simp.debug.cache] transient cache hit: f (f n)
+[sym.simp.debug.cache] persistent cache hit: f n
 -/
 #guard_msgs in
 set_option linter.unusedVariables false in
-example (n : Nat) (h : 0 < n) : ∀ (_ : Nat), n + 2 = 2 + n := by
-  sym_simp_twice [Nat.add_comm_of_pos]
+example (n : Nat) (h : 0 < n) : ∀ (_ : Nat), f (f n) = f (f (f n)) := by
+  sym_simp_twice [f_idem]

tests/elab/sym_simp_dsl_control1.lean

@@ -0,0 +1,97 @@
+/-! Tests for `control` and `arrow_telescope` simproc DSL primitives.
+Based on `sym_simp_4.lean` but using `register_sym_simp` + DSL instead of custom Lean tactics. -/
+
+register_sym_simp mySimp where
+  pre  := control >> arrow_telescope
+  post := ground >> rewrite [and_true] with self
+
+example : (if true then a else b) = a := by
+  sym => simp mySimp
+
+example : (if True then a else b) = a := by
+  sym => simp mySimp
+
+example : (if False then a else b) = b := by
+  sym => simp mySimp
+
+/--
+trace: case grind
+α✝ : Sort u_1
+x : α✝
+p q : Prop
+h : p → q
+⊢ p → q
+-/
+#guard_msgs in
+example (p q : Prop) (h : p → q) : True → p → x = x → q := by
+  sym =>
+    simp mySimp
+    show_goals
+    exact h
+
+example (p q : Prop) : q → p → True := by
+  sym => simp mySimp
+
+example (p q : Prop) : q → p → x = x := by
+  sym => simp mySimp
+
+example (q : Prop) : q → x ≠ x → True := by
+  sym => simp mySimp
+
+example (α : Type) (p : Prop) : α → p → x = x := by
+  sym => simp mySimp
+
+example (q : Prop) (α : Type) (p : Prop) : q → α → p → x = x := by
+  sym => simp mySimp
+
+example (α β : Type) (p q : Prop) : q → β → p → α → True := by
+  sym => simp mySimp
+
+/--
+trace: case grind
+α : Type u
+x : α
+p : Prop
+h : α → p → True → α
+⊢ α → p → True → α
+-/
+#guard_msgs in
+example (α : Type u) (x : α) (p : Prop) (h : α → p → True → α) : α → p → x = x → α := by
+  sym =>
+    simp mySimp
+    show_goals
+    exact h
+
+set_option linter.unusedVariables false
+
+def F := False
+
+/--
+trace: case grind
+α : Type
+x : α
+q : Prop
+h : F
+⊢ ∀ (a b : α), q
+-/
+#guard_msgs in
+example (α : Type) (x : α) (q : Prop) (h : F) : (a : α) → x = x → (b : α) → True → q := by
+  sym =>
+    simp mySimp
+    show_goals
+    exact False.elim h
+
+/--
+trace: case grind
+α : Sort u
+x : α
+p q : Prop
+h : F
+⊢ ∀ (a : α) {b : α}, q
+-/
+#guard_msgs in
+example (α : Sort u) (x : α) (p q : Prop) (h : F) : (a : α) → x = x → {b : α} → True → (q ∧ True) := by
+  sym =>
+    simp mySimp
+    show_goals
+    exact False.elim h

tests/elab/sym_simp_interactive1.lean

@@ -111,3 +111,29 @@ example (f : Nat → Nat) (x y : Nat) (h : f (f (f (f x))) = y) : 0 + x = x ∧
     simp simple
     try simp simple
     apply h
+
+/-! ## Test 11: duplicate variant name is rejected -/
+
+/--
+error: Sym.simp variant `simple` is already registered
+-/
+#guard_msgs in
+register_sym_simp simple where
+
+/-! ## Test 12: unknown theorem in `rewrite [...]` is rejected -/
+
+/--
+error: Unknown constant `bla`
+-/
+#guard_msgs in
+register_sym_simp simple₁ where
+  pre := rewrite [bla]
+
+/-! ## Test 13: unknown theorem set in `rewrite setName` is rejected -/
+
+/--
+error: unknown Sym.simp theorem set `boo`
+-/
+#guard_msgs in
+register_sym_simp simple₃ where
+  pre := rewrite boo

tests/elab/sym_simp_perm1.lean

@@ -0,0 +1,37 @@
+import Lean
+
+/-! Tests for permutation theorem support in `Sym.simp` -/
+
+-- Nat.add_comm is a permutation theorem: x + y = y + x
+-- Without perm support, `simp` with this theorem would loop.
+
+register_sym_simp commSimp where
+  post := ground >> rewrite [Nat.add_comm]
+
+-- This should terminate: Nat.add_comm is detected as perm,
+-- and only applied when result < input.
+example (x y : Nat) : x + y = y + x := by
+  sym =>
+    simp commSimp
+
+-- Combining perm with non-perm theorems
+register_sym_simp commZeroSimp where
+  post := ground >> rewrite [Nat.add_comm, Nat.zero_add, Nat.add_zero]
+
+example (x y : Nat) : 0 + (x + y) = y + x := by
+  sym =>
+    simp commZeroSimp
+
+-- Verify perm doesn't interfere with non-perm theorems
+register_sym_simp nonPermSimp where
+  post := ground >> rewrite [Nat.zero_add]
+
+example (x : Nat) : 0 + x = x := by
+  sym =>
+    simp nonPermSimp
+
+register_sym_simp simple where
+  post := ground
+
+example (x y z w : Nat) : x + y + z + w = w + (z + y) + x := by
+  sym => simp simple [Nat.add_comm, Nat.add_assoc, Nat.add_left_comm]