From 960c01fcae186960910ffecb1043e59329b0b104 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Wed, 14 Jan 2026 18:51:37 -0800
Subject: [PATCH] feat: `Sym.simp` rewrite on over-applied terms (#12012)

This PR implements support for rewrite on over-applied terms in
`Sym.simp`. Example: rewriting `id f a` using `id_eq`.
---
 src/Lean/Meta/Sym/Simp/App.lean      | 2 +-
 src/Lean/Meta/Sym/Simp/Rewrite.lean  | 9 ++++++---
 src/Lean/Meta/Sym/Simp/Theorems.lean | 3 +++
 tests/lean/run/sym_simp_1.lean       | 6 ++++++
 4 files changed, 16 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Meta/Sym/Simp/App.lean b/src/Lean/Meta/Sym/Simp/App.lean
index f285e79205..3a311e2b97 100644
--- a/src/Lean/Meta/Sym/Simp/App.lean
+++ b/src/Lean/Meta/Sym/Simp/App.lean
@@ -108,7 +108,7 @@ then `numArgs = 2` (the extra arguments) and we:
 **Note**: This is a fallback path without specialized optimizations. The common case (correct number of arguments)
 is handled more efficiently by the specific strategies.
 -/
-def simpOverApplied (e : Expr) (numArgs : Nat) (simpFn : Expr → SimpM Result) : SimpM Result := do
+public def simpOverApplied (e : Expr) (numArgs : Nat) (simpFn : Expr → SimpM Result) : SimpM Result := do
   let rec visit (e : Expr) (i : Nat) : SimpM Result := do
     if i == 0 then
       simpFn e
diff --git a/src/Lean/Meta/Sym/Simp/Rewrite.lean b/src/Lean/Meta/Sym/Simp/Rewrite.lean
index dbe9a963cd..0130516cd4 100644
--- a/src/Lean/Meta/Sym/Simp/Rewrite.lean
+++ b/src/Lean/Meta/Sym/Simp/Rewrite.lean
@@ -8,6 +8,7 @@ prelude
 public import Lean.Meta.Sym.Simp.SimpM
 public import Lean.Meta.Sym.Simp.Simproc
 public import Lean.Meta.Sym.Simp.Theorems
+public import Lean.Meta.Sym.Simp.App
 import Lean.Meta.Sym.InstantiateS
 import Lean.Meta.Sym.Simp.DiscrTree
 namespace Lean.Meta.Sym.Simp
@@ -41,9 +42,11 @@ public def Theorem.rewrite (thm : Theorem) (e : Expr) : SimpM Result := do
     return .rfl
 
 public def Theorems.rewrite (thms : Theorems) : Simproc := fun e => do
-  -- **TODO**: over-applied terms
-  for thm in thms.getMatch e do
-    let result ← thm.rewrite e
+  for (thm, numExtra) in thms.getMatchWithExtra e do
+    let result ← if numExtra == 0 then
+      thm.rewrite e
+    else
+      simpOverApplied e numExtra thm.rewrite
     if !result.isRfl then
       return result
   return .rfl
diff --git a/src/Lean/Meta/Sym/Simp/Theorems.lean b/src/Lean/Meta/Sym/Simp/Theorems.lean
index f6c8dcb2c4..b57430f952 100644
--- a/src/Lean/Meta/Sym/Simp/Theorems.lean
+++ b/src/Lean/Meta/Sym/Simp/Theorems.lean
@@ -38,6 +38,9 @@ def Theorems.insert (thms : Theorems) (thm : Theorem) : Theorems :=
 def Theorems.getMatch (thms : Theorems) (e : Expr) : Array Theorem :=
   Sym.getMatch thms.thms e
 
+def Theorems.getMatchWithExtra (thms : Theorems) (e : Expr) : Array (Theorem × Nat) :=
+  Sym.getMatchWithExtra thms.thms e
+
 def mkTheoremFromDecl (declName : Name) : MetaM Theorem := do
   let (pattern, rhs) ← mkEqPatternFromDecl declName
   return { expr := mkConst declName, pattern, rhs }
diff --git a/tests/lean/run/sym_simp_1.lean b/tests/lean/run/sym_simp_1.lean
index e010fd33a9..28adbc849d 100644
--- a/tests/lean/run/sym_simp_1.lean
+++ b/tests/lean/run/sym_simp_1.lean
@@ -123,3 +123,9 @@ example (h : ite (c > 0) a = g) : ite (c > 0) (0 + a) = g := by
   sym_simp [Nat.zero_add]
   trace_state
   exact h
+
+example (f : Nat → Nat) : id f a = f a := by
+  sym_simp [id_eq, eq_self]
+
+example (f : Nat → Nat) : id f (0 + a) = f a := by
+  sym_simp [id_eq, eq_self, Nat.zero_add]