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

@@ -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

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

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 }

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]