feat: support local hypotheses in simp [h] for sym => mode

The `simp` tactic in `sym =>` mode now resolves identifiers in the extra
theorem list against local hypotheses first, falling back to global
constants. Local hypotheses are adapted via `mkTheoremFromExpr` (using
the `eq_true`/`eq_false`/`propext` adapter from #13041).

- Add `ExtraTheorem` inductive (`.const` / `.fvar`) for cache keying
- Add `resolveExtraTheorem` that checks the local context before globals
- Update `addExtraTheorems`, `mkDefaultMethods`, `elabVariant` signatures

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

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

@@ -1,29 +0,0 @@
-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-") or version1.startswith("leanprover/lean4-nightly:"):
+    if version1.startswith("leanprover/lean4:nightly-"):
         return False
     return parse_version(version1) >= parse_version(version2)
 

src/Init/Grind/Interactive.lean

@@ -107,9 +107,6 @@ 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
@@ -318,8 +315,5 @@ 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,14 +49,6 @@ 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,8 +329,7 @@ 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))
-    let isMeta := (← read).isMetaSection
-    withNewMCtxDepth <| normalizeInstance inst expectedType (logCompileErrors := logCompileErrors) (isMeta := isMeta)
+    withNewMCtxDepth <| normalizeInstance inst expectedType (logCompileErrors := logCompileErrors)
   else
     pure inst
   ensureHasType expectedType? inst

src/Lean/Elab/Command.lean

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

src/Lean/Elab/Deriving/Basic.lean

@@ -220,12 +220,10 @@ 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/BuiltinTactic.lean

@@ -76,10 +76,6 @@ 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/SimprocDSLBuiltin.lean

@@ -9,8 +9,6 @@ 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
@@ -25,14 +23,6 @@ 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/Term/TermElabM.lean

@@ -309,8 +309,6 @@ 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) (isMeta : Bool := false) : MetaM Expr := withTransparency .instances do
+    (logCompileErrors : Bool := true) : MetaM Expr := withTransparency .instances do
   withTraceNode `Meta.instanceNormalForm
       (fun _ => return m!"type: {expectedType}") do
   let some className ← isClass? expectedType
@@ -124,11 +124,9 @@ partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true
             return inst
           else
             let name ← mkAuxDeclName
-            let wrapped ← mkAuxDefinition name expectedType inst (compile := false)
+            let wrapped ← mkAuxDefinition name expectedType inst (compile := compile)
+              (logCompileErrors := logCompileErrors)
             setReducibilityStatus name .implicitReducible
-            if isMeta then modifyEnv (markMeta · name)
-            if compile then
-              compileDecls (logErrors := logCompileErrors) #[name]
             enableRealizationsForConst name
             return wrapped
         else
@@ -171,7 +169,7 @@ partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true
             catch _ => pure ()
 
           mvarId.assign (← normalizeInstance arg argExpectedType (compile := compile)
-            (logCompileErrors := logCompileErrors) (isMeta := isMeta))
+            (logCompileErrors := logCompileErrors))
         else
           -- For data fields, assign directly or wrap in aux def to fix types.
           if backward.inferInstanceAs.wrap.data.get (← getOptions) then
@@ -182,7 +180,6 @@ 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,7 +9,6 @@ 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
@@ -72,16 +71,10 @@ 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

@@ -10,7 +10,6 @@ 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
 
@@ -27,10 +26,6 @@ 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
@@ -50,49 +45,6 @@ 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. -/
@@ -147,15 +99,13 @@ where
 def mkTheoremFromDecl (declName : Name) : MetaM Theorem := do
   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 }
+  return { expr, pattern, rhs }
 
 /-- 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 }
+  return { expr, pattern, rhs }
 
 /--
 Environment extension storing a set of `Sym.Simp` theorems.

tests/elab/12897.lean

@@ -1,12 +0,0 @@
--- 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_cd.lean

@@ -42,120 +42,153 @@ 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.
-opaque f : Nat → Nat
-axiom f_idem (a : Nat) (_h : 0 < a) : f (f a) = f a
+theorem Nat.add_comm_of_pos (a b : Nat) (_h : 0 < a) : a + b = b + a := Nat.add_comm a b
 
 set_option trace.sym.simp.debug.cache true in
 /--
-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
+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] second traversal
-[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
+[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
 -/
 #guard_msgs in
-example (n : Nat) (h : 0 < n) : f (f n) = f (f (f n)) := by
-  sym_simp_twice [f_idem]
+example (n : Nat) (h : 0 < n) : n + 2 = 2 + n := by
+  sym_simp_twice [Nat.add_comm_of_pos]
 
 -- 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: f n
-[sym.simp.debug.cache] persistent cache hit: f n
-[sym.simp.debug.cache] persistent cache hit: f n + 7
+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
 [sym.simp.debug.cache] second traversal
-[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: 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: 3 + 4
-[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) : f (f n) + (3 + 4) = f n + 7 := by
-  sym_simp_twice [f_idem]
-
--- 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: 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: f n
-[sym.simp.debug.cache] persistent cache hit: 3 + 4
-[sym.simp.debug.cache] transient cache hit: f (f n)
+[sym.simp.debug.cache] transient cache hit: 2 + n
 [sym.simp.debug.cache] persistent cache hit: 7
-[sym.simp.debug.cache] transient cache hit: f (f n) + 7
+[sym.simp.debug.cache] transient cache hit: (2 + n) * 7
 -/
 #guard_msgs in
-example (n : Nat) : f (f n) + (3 + 4) = f (f n) + 7 := by
-  sym_simp_twice [f_idem]
+example (n : Nat) (h : 0 < n) : (n + 2) * (3 + 4) = (2 + n) * 7 := by
+  sym_simp_twice [Nat.add_comm_of_pos]
+
+-- Similar to previous test, but `Nat.add_comm_of_pos` is not applicable, 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
+[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: 3 + 4
+[sym.simp.debug.cache] transient cache hit: n + 2
+[sym.simp.debug.cache] persistent cache hit: 7
+[sym.simp.debug.cache] transient cache hit: (n + 2) * 7
+-/
+#guard_msgs in
+example (n : Nat) : (n + 2) * (3 + 4) = (n + 2) * 7 := by
+  sym_simp_twice [Nat.add_comm_of_pos]
 
 -- 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: f n
-[sym.simp.debug.cache] persistent cache hit: f n
+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] second traversal
-[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: 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: True
 -/
 #guard_msgs in
 set_option linter.unusedVariables false in
-example (n : Nat) (h : 0 < n) : (f (f n) = f n) → True := by
-  sym_simp_twice [f_idem]
+example (n : Nat) (h : 0 < n) : (n + 2 = 2 + n) → True := by
+  sym_simp_twice [Nat.add_comm_of_pos]
 
 -- 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: f n
-[sym.simp.debug.cache] persistent cache hit: f n
-[sym.simp.debug.cache] persistent cache hit: fun x => f n
+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
 [sym.simp.debug.cache] second traversal
-[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
+[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
 -/
 #guard_msgs in
-example (n : Nat) (_h : 0 < n) : (fun _ : Nat => f (f n)) = (fun _ : Nat => f n) := by
-  sym_simp_twice [f_idem]
+example (n : Nat) (_h : 0 < n) : (fun _ : Nat => n + 2) = (fun _ : Nat => 2 + n) := by
+  sym_simp_twice [Nat.add_comm_of_pos]
 
 -- 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: f n
-[sym.simp.debug.cache] persistent cache hit: f n
+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] persistent cache hit: 1
 [sym.simp.debug.cache] second traversal
-[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: 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: 1
 [sym.simp.debug.cache] persistent cache hit: 1
 -/
 #guard_msgs in
-example (n : Nat) (h : 0 < n) : (if f (f n) = f n then 1 else 0) = 1 := by
-  sym_simp_twice [f_idem]
+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]
 
 -- 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: f n
-[sym.simp.debug.cache] transient cache hit: f (f n)
-[sym.simp.debug.cache] persistent cache hit: f n
+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] second traversal
 [sym.simp.debug.cache] persistent cache hit: Nat
-[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
+[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
 -/
 #guard_msgs in
 set_option linter.unusedVariables false in
-example (n : Nat) (h : 0 < n) : ∀ (_ : Nat), f (f n) = f (f (f n)) := by
-  sym_simp_twice [f_idem]
+example (n : Nat) (h : 0 < n) : ∀ (_ : Nat), n + 2 = 2 + n := by
+  sym_simp_twice [Nat.add_comm_of_pos]

tests/elab/sym_simp_dsl_control1.lean

@@ -1,97 +0,0 @@
-/-! 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_perm1.lean

@@ -1,37 +0,0 @@
-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]