feat: seval tactic skeleton

We are going to reuse these methods to implement a symbolic/partial evaluator.

src/Init/Tactics.lean

@@ -452,6 +452,12 @@ definitionally equal to the input.
 syntax (name := dsimp) "dsimp" (config)? (discharger)? (&" only")?
   (" [" withoutPosition((simpErase <|> simpLemma),*,?) "]")? (location)? : tactic
 
+/--
+The `seval` tactic is a symbolic evaluator. It reduces nested ground terms.
+**WARNING**: This tactic is under development. Do not use it in your project unless you are working with the tactic developer.
+-/
+syntax (name := seval) "seval" : tactic
+
 /--
 `delta id1 id2 ...` delta-expands the definitions `id1`, `id2`, ....
 This is a low-level tactic, it will expose how recursive definitions have been

src/Lean/Elab/Tactic.lean

@@ -22,3 +22,4 @@ import Lean.Elab.Tactic.Unfold
 import Lean.Elab.Tactic.Cache
 import Lean.Elab.Tactic.Calc
 import Lean.Elab.Tactic.Congr
+import Lean.Elab.Tactic.SEval

src/Lean/Elab/Tactic/SEval.lean

@@ -0,0 +1,20 @@
+/-
+Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.Tactic.SymEval
+import Lean.Elab.Tactic.Basic
+
+namespace Lean.Elab.Tactic
+
+open Meta Tactic
+
+@[builtin_tactic Lean.Parser.Tactic.seval] def evalSEval : Tactic := fun _ => withMainContext do
+  let mvarId ← getMainGoal
+  let result? ← sevalTarget mvarId {}
+  match result? with
+  | none => replaceMainGoal []
+  | some mvarId => replaceMainGoal [mvarId]
+
+end Lean.Elab.Tactic

src/Lean/Meta/Tactic.lean

@@ -28,4 +28,5 @@ import Lean.Meta.Tactic.Rename
 import Lean.Meta.Tactic.LinearArith
 import Lean.Meta.Tactic.AC
 import Lean.Meta.Tactic.Refl
-import Lean.Meta.Tactic.Congr
+import Lean.Meta.Tactic.Congr
+import Lean.Meta.Tactic.SymEval

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -30,45 +30,6 @@ def Config.updateArith (c : Config) : CoreM Config := do
   else
     return c
 
-def Result.getProof (r : Result) : MetaM Expr := do
-  match r.proof? with
-  | some p => return p
-  | none   => mkEqRefl r.expr
-
-/--
-  Similar to `Result.getProof`, but adds a `mkExpectedTypeHint` if `proof?` is `none`
-  (i.e., result is definitionally equal to input), but we cannot establish that
-  `source` and `r.expr` are definitionally when using `TransparencyMode.reducible`. -/
-def Result.getProof' (source : Expr) (r : Result) : MetaM Expr := do
-  match r.proof? with
-  | some p => return p
-  | none   =>
-    if (← isDefEq source r.expr) then
-      mkEqRefl r.expr
-    else
-      /- `source` and `r.expr` must be definitionally equal, but
-         are not definitionally equal at `TransparencyMode.reducible` -/
-      mkExpectedTypeHint (← mkEqRefl r.expr) (← mkEq source r.expr)
-
-def mkCongrFun (r : Result) (a : Expr) : MetaM Result :=
-  match r.proof? with
-  | none   => return { expr := mkApp r.expr a, proof? := none }
-  | some h => return { expr := mkApp r.expr a, proof? := (← Meta.mkCongrFun h a) }
-
-def mkCongr (r₁ r₂ : Result) : MetaM Result :=
-  let e := mkApp r₁.expr r₂.expr
-  match r₁.proof?, r₂.proof? with
-  | none,     none   => return { expr := e, proof? := none }
-  | some h,  none    => return { expr := e, proof? := (← Meta.mkCongrFun h r₂.expr) }
-  | none,    some h  => return { expr := e, proof? := (← Meta.mkCongrArg r₁.expr h) }
-  | some h₁, some h₂ => return { expr := e, proof? := (← Meta.mkCongr h₁ h₂) }
-
-private def mkImpCongr (src : Expr) (r₁ r₂ : Result) : MetaM Result := do
-  let e := src.updateForallE! r₁.expr r₂.expr
-  match r₁.proof?, r₂.proof? with
-  | none,     none   => return { expr := e, proof? := none }
-  | _,        _      => return { expr := e, proof? := (← Meta.mkImpCongr (← r₁.getProof) (← r₂.getProof)) } -- TODO specialize if bottleneck
-
 /-- Return true if `e` is of the form `ofNat n` where `n` is a kernel Nat literal -/
 def isOfNatNatLit (e : Expr) : Bool :=
   e.isAppOfArity ``OfNat.ofNat 3 && e.appFn!.appArg!.isNatLit
@@ -306,29 +267,6 @@ def getSimpLetCase (n : Name) (t : Expr) (b : Expr) : MetaM SimpLetCase := do
     else
       return SimpLetCase.dep
 
-/-- Given the application `e`, remove unnecessary casts of the form `Eq.rec a rfl` and `Eq.ndrec a rfl`. -/
-partial def removeUnnecessaryCasts (e : Expr) : MetaM Expr := do
-  let mut args := e.getAppArgs
-  let mut modified := false
-  for i in [:args.size] do
-    let arg := args[i]!
-    if isDummyEqRec arg then
-      args := args.set! i (elimDummyEqRec arg)
-      modified := true
-  if modified then
-    return mkAppN e.getAppFn args
-  else
-    return e
-where
-  isDummyEqRec (e : Expr) : Bool :=
-    (e.isAppOfArity ``Eq.rec 6 || e.isAppOfArity ``Eq.ndrec 6) && e.appArg!.isAppOf ``Eq.refl
-
-  elimDummyEqRec (e : Expr) : Expr :=
-    if isDummyEqRec e then
-      elimDummyEqRec e.appFn!.appFn!.appArg!
-    else
-      e
-
 partial def simp (e : Expr) : M Result := withIncRecDepth do
   checkSystem "simp"
   let cfg ← getConfig
@@ -420,22 +358,7 @@ where
         return { expr := (← dsimp e) }
 
   congrArgs (r : Result) (args : Array Expr) : M Result := do
-    if args.isEmpty then
-      return r
-    else
-      let infos := (← getFunInfoNArgs r.expr args.size).paramInfo
-      let mut r := r
-      let mut i := 0
-      for arg in args do
-        trace[Debug.Meta.Tactic.simp] "app [{i}] {infos.size} {arg} hasFwdDeps: {infos[i]!.hasFwdDeps}"
-        if i < infos.size && !infos[i]!.hasFwdDeps then
-          r ← mkCongr r (← simp arg)
-        else if (← whnfD (← inferType r.expr)).isArrow then
-          r ← mkCongr r (← simp arg)
-        else
-          r ← mkCongrFun r (← dsimp arg)
-        i := i + 1
-      return r
+    Simp.congrArgs simp dsimp r args
 
   visitFn (e : Expr) : M Result := do
     let f := e.getAppFn
@@ -451,112 +374,9 @@ where
         proof ← Meta.mkCongrFun proof arg
       return { expr := eNew, proof? := proof }
 
-  mkCongrSimp? (f : Expr) : M (Option CongrTheorem) := do
-    if f.isConst then if (← isMatcher f.constName!) then
-      -- We always use simple congruence theorems for auxiliary match applications
-      return none
-    let info ← getFunInfo f
-    let kinds ← getCongrSimpKinds f info
-    if kinds.all fun k => match k with | CongrArgKind.fixed => true | CongrArgKind.eq => true | _ => false then
-      /- If all argument kinds are `fixed` or `eq`, then using
-         simple congruence theorems `congr`, `congrArg`, and `congrFun` produces a more compact proof -/
-      return none
-    match (← get).congrCache.find? f with
-    | some thm? => return thm?
-    | none =>
-      let thm? ← mkCongrSimpCore? f info kinds
-      modify fun s => { s with congrCache := s.congrCache.insert f thm? }
-      return thm?
-
   /-- Try to use automatically generated congruence theorems. See `mkCongrSimp?`. -/
   tryAutoCongrTheorem? (e : Expr) : M (Option Result) := do
-    let f := e.getAppFn
-    -- TODO: cache
-    let some cgrThm ← mkCongrSimp? f | return none
-    if cgrThm.argKinds.size != e.getAppNumArgs then return none
-    let mut simplified := false
-    let mut hasProof   := false
-    let mut hasCast    := false
-    let mut argsNew    := #[]
-    let mut argResults := #[]
-    let args := e.getAppArgs
-    for arg in args, kind in cgrThm.argKinds do
-      match kind with
-      | CongrArgKind.fixed => argsNew := argsNew.push (← dsimp arg)
-      | CongrArgKind.cast  => hasCast := true; argsNew := argsNew.push arg
-      | CongrArgKind.subsingletonInst => argsNew := argsNew.push arg
-      | CongrArgKind.eq =>
-        let argResult ← simp arg
-        argResults := argResults.push argResult
-        argsNew    := argsNew.push argResult.expr
-        if argResult.proof?.isSome then hasProof := true
-        if arg != argResult.expr then simplified := true
-      | _ => unreachable!
-    if !simplified then return some { expr := e }
-    /-
-      If `hasProof` is false, we used to return `mkAppN f argsNew` with `proof? := none`.
-      However, this created a regression when we started using `proof? := none` for `rfl` theorems.
-      Consider the following goal
-      ```
-      m n : Nat
-      a : Fin n
-      h₁ : m < n
-      h₂ : Nat.pred (Nat.succ m) < n
-      ⊢ Fin.succ (Fin.mk m h₁) = Fin.succ (Fin.mk m.succ.pred h₂)
-      ```
-      The term `m.succ.pred` is simplified to `m` using a `Nat.pred_succ` which is a `rfl` theorem.
-      The auto generated theorem for `Fin.mk` has casts and if used here at `Fin.mk m.succ.pred h₂`,
-      it produces the term `Fin.mk m (id (Eq.refl m) ▸ h₂)`. The key property here is that the
-      proof `(id (Eq.refl m) ▸ h₂)` has type `m < n`. If we had just returned `mkAppN f argsNew`,
-      the resulting term would be `Fin.mk m h₂` which is type correct, but later we would not be
-      able to apply `eq_self` to
-      ```lean
-      Fin.succ (Fin.mk m h₁) = Fin.succ (Fin.mk m h₂)
-      ```
-      because we would not be able to establish that `m < n` and `Nat.pred (Nat.succ m) < n` are definitionally
-      equal using `TransparencyMode.reducible` (`Nat.pred` is not reducible).
-      Thus, we decided to return here only if the auto generated congruence theorem does not introduce casts.
-    -/
-    if !hasProof && !hasCast then return some { expr := mkAppN f argsNew }
-    let mut proof := cgrThm.proof
-    let mut type  := cgrThm.type
-    let mut j := 0 -- index at argResults
-    let mut subst := #[]
-    for arg in args, kind in cgrThm.argKinds do
-      proof := mkApp proof arg
-      subst := subst.push arg
-      type := type.bindingBody!
-      match kind with
-      | CongrArgKind.fixed => pure ()
-      | CongrArgKind.cast  => pure ()
-      | CongrArgKind.subsingletonInst =>
-        let clsNew := type.bindingDomain!.instantiateRev subst
-        let instNew ← if (← isDefEq (← inferType arg) clsNew) then
-          pure arg
-        else
-          match (← trySynthInstance clsNew) with
-          | LOption.some val => pure val
-          | _ =>
-            trace[Meta.Tactic.simp.congr] "failed to synthesize instance{indentExpr clsNew}"
-            return none
-        proof := mkApp proof instNew
-        subst := subst.push instNew
-        type := type.bindingBody!
-      | CongrArgKind.eq =>
-        let argResult := argResults[j]!
-        let argProof ← argResult.getProof' arg
-        j := j + 1
-        proof := mkApp2 proof argResult.expr argProof
-        subst := subst.push argResult.expr |>.push argProof
-        type := type.bindingBody!.bindingBody!
-      | _ => unreachable!
-    let some (_, _, rhs) := type.instantiateRev subst |>.eq? | unreachable!
-    let rhs ← if hasCast then removeUnnecessaryCasts rhs else pure rhs
-    if hasProof then
-      return some { expr := rhs, proof? := proof }
-    else
-      /- See comment above. This is reachable if `hasCast == true`. The `rhs` is not structurally equal to `mkAppN f argsNew` -/
-      return some { expr := rhs }
+    Simp.tryAutoCongrTheorem? simp dsimp e
 
   congrDefault (e : Expr) : M Result := do
     if let some result ← tryAutoCongrTheorem? e then
@@ -958,19 +778,6 @@ def dsimp (e : Expr) (ctx : Simp.Context)
     (usedSimps : UsedSimps := {}) : MetaM (Expr × UsedSimps) := do profileitM Exception "dsimp" (← getOptions) do
   Simp.dsimpMain e ctx usedSimps (methods := Simp.DefaultMethods.methods)
 
-/--
-  Auxiliary method.
-  Given the current `target` of `mvarId`, apply `r` which is a new target and proof that it is equal to the current one.
--/
-def applySimpResultToTarget (mvarId : MVarId) (target : Expr) (r : Simp.Result) : MetaM MVarId := do
-  match r.proof? with
-  | some proof => mvarId.replaceTargetEq r.expr proof
-  | none =>
-    if target != r.expr then
-      mvarId.replaceTargetDefEq r.expr
-    else
-      return mvarId
-
 /-- See `simpTarget`. This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/
 def simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
     (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do

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

@@ -116,7 +116,7 @@ private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInf
   | some { expr := eNew, proof? := some proof, .. } =>
     let mut proof := proof
     for extraArg in extraArgs do
-      proof ← mkCongrFun proof extraArg
+      proof ← Meta.mkCongrFun proof extraArg
     if (← hasAssignableMVar eNew) then
       trace[Meta.Tactic.simp.rewrite] "{← ppSimpTheorem thm}, resulting expression has unassigned metavariables"
       return none

src/Lean/Meta/Tactic/Simp/Types.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 import Lean.Meta.AppBuilder
 import Lean.Meta.CongrTheorems
+import Lean.Meta.Tactic.Replace
 import Lean.Meta.Tactic.Simp.SimpTheorems
 import Lean.Meta.Tactic.Simp.SimpCongrTheorems
 
@@ -101,8 +102,240 @@ def recordSimpTheorem (thmId : Origin) : SimpM Unit :=
     let n := s.usedTheorems.size
     { s with usedTheorems := s.usedTheorems.insert thmId n }
 
+def Result.getProof (r : Result) : MetaM Expr := do
+  match r.proof? with
+  | some p => return p
+  | none   => mkEqRefl r.expr
+
+/--
+  Similar to `Result.getProof`, but adds a `mkExpectedTypeHint` if `proof?` is `none`
+  (i.e., result is definitionally equal to input), but we cannot establish that
+  `source` and `r.expr` are definitionally when using `TransparencyMode.reducible`. -/
+def Result.getProof' (source : Expr) (r : Result) : MetaM Expr := do
+  match r.proof? with
+  | some p => return p
+  | none   =>
+    if (← isDefEq source r.expr) then
+      mkEqRefl r.expr
+    else
+      /- `source` and `r.expr` must be definitionally equal, but
+         are not definitionally equal at `TransparencyMode.reducible` -/
+      mkExpectedTypeHint (← mkEqRefl r.expr) (← mkEq source r.expr)
+
+def mkCongrFun (r : Result) (a : Expr) : MetaM Result :=
+  match r.proof? with
+  | none   => return { expr := mkApp r.expr a, proof? := none }
+  | some h => return { expr := mkApp r.expr a, proof? := (← Meta.mkCongrFun h a) }
+
+def mkCongr (r₁ r₂ : Result) : MetaM Result :=
+  let e := mkApp r₁.expr r₂.expr
+  match r₁.proof?, r₂.proof? with
+  | none,     none   => return { expr := e, proof? := none }
+  | some h,  none    => return { expr := e, proof? := (← Meta.mkCongrFun h r₂.expr) }
+  | none,    some h  => return { expr := e, proof? := (← Meta.mkCongrArg r₁.expr h) }
+  | some h₁, some h₂ => return { expr := e, proof? := (← Meta.mkCongr h₁ h₂) }
+
+def mkImpCongr (src : Expr) (r₁ r₂ : Result) : MetaM Result := do
+  let e := src.updateForallE! r₁.expr r₂.expr
+  match r₁.proof?, r₂.proof? with
+  | none,     none   => return { expr := e, proof? := none }
+  | _,        _      => return { expr := e, proof? := (← Meta.mkImpCongr (← r₁.getProof) (← r₂.getProof)) } -- TODO specialize if bottleneck
+
+/-- Given the application `e`, remove unnecessary casts of the form `Eq.rec a rfl` and `Eq.ndrec a rfl`. -/
+partial def removeUnnecessaryCasts (e : Expr) : MetaM Expr := do
+  let mut args := e.getAppArgs
+  let mut modified := false
+  for i in [:args.size] do
+    let arg := args[i]!
+    if isDummyEqRec arg then
+      args := args.set! i (elimDummyEqRec arg)
+      modified := true
+  if modified then
+    return mkAppN e.getAppFn args
+  else
+    return e
+where
+  isDummyEqRec (e : Expr) : Bool :=
+    (e.isAppOfArity ``Eq.rec 6 || e.isAppOfArity ``Eq.ndrec 6) && e.appArg!.isAppOf ``Eq.refl
+
+  elimDummyEqRec (e : Expr) : Expr :=
+    if isDummyEqRec e then
+      elimDummyEqRec e.appFn!.appFn!.appArg!
+    else
+      e
+
+/--
+Given a simplified function result `r` and arguments `args`, simplify arguments using `simp` and `dsimp`.
+The resulting proof is built using `congr` and `congrFun` theorems.
+-/
+@[specialize] def congrArgs
+    [Monad m] [MonadLiftT MetaM m] [MonadLiftT IO m] [MonadRef m] [MonadOptions m] [MonadTrace m] [AddMessageContext m]
+    (simp : Expr → m Result)
+    (dsimp : Expr → m Expr)
+    (r : Result) (args : Array Expr) : m Result := do
+  if args.isEmpty then
+    return r
+  else
+    let infos := (← getFunInfoNArgs r.expr args.size).paramInfo
+    let mut r := r
+    let mut i := 0
+    for arg in args do
+      trace[Debug.Meta.Tactic.simp] "app [{i}] {infos.size} {arg} hasFwdDeps: {infos[i]!.hasFwdDeps}"
+      if i < infos.size && !infos[i]!.hasFwdDeps then
+        r ← mkCongr r (← simp arg)
+      else if (← whnfD (← inferType r.expr)).isArrow then
+        r ← mkCongr r (← simp arg)
+      else
+        r ← mkCongrFun r (← dsimp arg)
+      i := i + 1
+    return r
+
+/--
+Helper class for generalizing `mkCongrSimp?`
+-/
+class MonadCongrCache (m : Type → Type) where
+  find? : Expr → m (Option (Option CongrTheorem))
+  save  : Expr → (Option CongrTheorem) → m Unit
+
+instance : MonadCongrCache M where
+  find? f := return (← get).congrCache.find? f
+  save f thm? := modify fun s => { s with congrCache := s.congrCache.insert f thm? }
+
+/--
+Retrieve auto-generated congruence lemma for `f`.
+
+Remark: If all argument kinds are `fixed` or `eq`, it returns `none` because
+using simple congruence theorems `congr`, `congrArg`, and `congrFun` produces a more compact proof.
+-/
+def mkCongrSimp? [Monad m] [MonadLiftT MetaM m] [MonadEnv m] [MonadCongrCache m]
+  (f : Expr) : m (Option CongrTheorem) := do
+  if f.isConst then if (← isMatcher f.constName!) then
+    -- We always use simple congruence theorems for auxiliary match applications
+    return none
+  let info ← getFunInfo f
+  let kinds ← getCongrSimpKinds f info
+  if kinds.all fun k => match k with | CongrArgKind.fixed => true | CongrArgKind.eq => true | _ => false then
+    /- See remark above. -/
+    return none
+  match (← MonadCongrCache.find? f) with
+  | some thm? => return thm?
+  | none =>
+    let thm? ← mkCongrSimpCore? f info kinds
+    MonadCongrCache.save f thm?
+    return thm?
+
+/--
+Try to use automatically generated congruence theorems. See `mkCongrSimp?`.
+-/
+@[specialize] def tryAutoCongrTheorem?
+    [Monad m] [MonadEnv m] [MonadCongrCache m] [MonadLiftT MetaM m]
+    [MonadLiftT IO m] [MonadRef m] [MonadOptions m] [MonadTrace m] [AddMessageContext m]
+    (simp : Expr → m Result)
+    (dsimp : Expr → m Expr)
+    (e : Expr) : m (Option Result) := do
+  let f := e.getAppFn
+  -- TODO: cache
+  let some cgrThm ← mkCongrSimp? f | return none
+  if cgrThm.argKinds.size != e.getAppNumArgs then return none
+  let mut simplified := false
+  let mut hasProof   := false
+  let mut hasCast    := false
+  let mut argsNew    := #[]
+  let mut argResults := #[]
+  let args := e.getAppArgs
+  for arg in args, kind in cgrThm.argKinds do
+    match kind with
+    | CongrArgKind.fixed => argsNew := argsNew.push (← dsimp arg)
+    | CongrArgKind.cast  => hasCast := true; argsNew := argsNew.push arg
+    | CongrArgKind.subsingletonInst => argsNew := argsNew.push arg
+    | CongrArgKind.eq =>
+      let argResult ← simp arg
+      argResults := argResults.push argResult
+      argsNew    := argsNew.push argResult.expr
+      if argResult.proof?.isSome then hasProof := true
+      if arg != argResult.expr then simplified := true
+    | _ => unreachable!
+  if !simplified then return some { expr := e }
+  /-
+    If `hasProof` is false, we used to return `mkAppN f argsNew` with `proof? := none`.
+    However, this created a regression when we started using `proof? := none` for `rfl` theorems.
+    Consider the following goal
+    ```
+    m n : Nat
+    a : Fin n
+    h₁ : m < n
+    h₂ : Nat.pred (Nat.succ m) < n
+    ⊢ Fin.succ (Fin.mk m h₁) = Fin.succ (Fin.mk m.succ.pred h₂)
+    ```
+    The term `m.succ.pred` is simplified to `m` using a `Nat.pred_succ` which is a `rfl` theorem.
+    The auto generated theorem for `Fin.mk` has casts and if used here at `Fin.mk m.succ.pred h₂`,
+    it produces the term `Fin.mk m (id (Eq.refl m) ▸ h₂)`. The key property here is that the
+    proof `(id (Eq.refl m) ▸ h₂)` has type `m < n`. If we had just returned `mkAppN f argsNew`,
+    the resulting term would be `Fin.mk m h₂` which is type correct, but later we would not be
+    able to apply `eq_self` to
+    ```lean
+    Fin.succ (Fin.mk m h₁) = Fin.succ (Fin.mk m h₂)
+    ```
+    because we would not be able to establish that `m < n` and `Nat.pred (Nat.succ m) < n` are definitionally
+    equal using `TransparencyMode.reducible` (`Nat.pred` is not reducible).
+    Thus, we decided to return here only if the auto generated congruence theorem does not introduce casts.
+  -/
+  if !hasProof && !hasCast then return some { expr := mkAppN f argsNew }
+  let mut proof := cgrThm.proof
+  let mut type  := cgrThm.type
+  let mut j := 0 -- index at argResults
+  let mut subst := #[]
+  for arg in args, kind in cgrThm.argKinds do
+    proof := mkApp proof arg
+    subst := subst.push arg
+    type := type.bindingBody!
+    match kind with
+    | CongrArgKind.fixed => pure ()
+    | CongrArgKind.cast  => pure ()
+    | CongrArgKind.subsingletonInst =>
+      let clsNew := type.bindingDomain!.instantiateRev subst
+      let instNew ← if (← isDefEq (← inferType arg) clsNew) then
+        pure arg
+      else
+        match (← trySynthInstance clsNew) with
+        | LOption.some val => pure val
+        | _ =>
+          trace[Meta.Tactic.simp.congr] "failed to synthesize instance{indentExpr clsNew}"
+          return none
+      proof := mkApp proof instNew
+      subst := subst.push instNew
+      type := type.bindingBody!
+    | CongrArgKind.eq =>
+      let argResult := argResults[j]!
+      let argProof ← argResult.getProof' arg
+      j := j + 1
+      proof := mkApp2 proof argResult.expr argProof
+      subst := subst.push argResult.expr |>.push argProof
+      type := type.bindingBody!.bindingBody!
+    | _ => unreachable!
+  let some (_, _, rhs) := type.instantiateRev subst |>.eq? | unreachable!
+  let rhs ← if hasCast then removeUnnecessaryCasts rhs else pure rhs
+  if hasProof then
+    return some { expr := rhs, proof? := proof }
+  else
+    /- See comment above. This is reachable if `hasCast == true`. The `rhs` is not structurally equal to `mkAppN f argsNew` -/
+    return some { expr := rhs }
+
 end Simp
 
 export Simp (SimpM)
 
+/--
+  Auxiliary method.
+  Given the current `target` of `mvarId`, apply `r` which is a new target and proof that it is equal to the current one.
+-/
+def applySimpResultToTarget (mvarId : MVarId) (target : Expr) (r : Simp.Result) : MetaM MVarId := do
+  match r.proof? with
+  | some proof => mvarId.replaceTargetEq r.expr proof
+  | none =>
+    if target != r.expr then
+      mvarId.replaceTargetDefEq r.expr
+    else
+      return mvarId
+
 end Lean.Meta

src/Lean/Meta/Tactic/SymEval.lean

@@ -0,0 +1,14 @@
+/-
+Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.Tactic.SymEval.Types
+import Lean.Meta.Tactic.SymEval.Main
+
+namespace Lean
+
+builtin_initialize registerTraceClass `Meta.Tactic.seval
+builtin_initialize registerTraceClass `Meta.Tactic.seval.visit
+
+end Lean

src/Lean/Meta/Tactic/SymEval/Main.lean

@@ -0,0 +1,133 @@
+/-
+Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.Tactic.Util
+import Lean.Meta.Tactic.Simp.Rewrite
+import Lean.Meta.Tactic.SymEval.Types
+
+namespace Lean.Meta
+namespace SymEval
+
+def cacheResult (e : Expr) (r : Result) : M Result := do
+  let dischargeDepth := (← read).dischargeDepth
+  modify fun s => { s with cache := s.cache.insert e { r with dischargeDepth } }
+  return r
+
+def evalLit (e : Expr) : M Result :=
+  -- TODO
+  return { expr := e }
+
+partial def seval (e : Expr) : M Result := withIncRecDepth do
+  checkSystem "eval"
+  if (← isProof e) then
+    return { expr := e }
+  if let some result := (← get).cache.find? e then
+    if result.dischargeDepth ≤ (← read).dischargeDepth then
+      return result
+  loop { expr := e }
+where
+  loop (r : Result) : M Result := do
+    let cfg ← getConfig
+    if (← get).numSteps > cfg.maxSteps then
+      throwError "'seval' failed, maximum number of steps exceeded"
+    else
+      modify fun s => { s with numSteps := s.numSteps + 1 }
+      let r ← Simp.mkEqTrans r (← step r.expr)
+      cacheResult e r
+
+  step (e : Expr) : M Result := do
+    trace[Meta.Tactic.seval.visit] "{e}"
+    match e with
+    | .mdata _ e   => seval e
+    | .proj ..     => evalProj e
+    | .app ..      => evalApp e
+    | .lam ..      => evalLambda e
+    | .forallE ..  => evalForall e
+    | .letE ..     => evalLet e
+    | .const ..    => evalConst e
+    | .bvar ..     => unreachable!
+    | .sort ..     => return { expr := e }
+    | .lit ..      => evalLit e
+    | .mvar ..     => seval (← instantiateMVars e)
+    | .fvar ..     => evalFVar e
+
+  evalConst (e : Expr) : M Result := do
+    -- TODO
+    return { expr := e }
+
+  evalFVar (e : Expr) : M Result := do
+    -- TODO
+    return { expr := e }
+
+  evalLet (e : Expr) : M Result := do
+    -- TODO
+    return { expr := e }
+
+  evalProj (e : Expr) : M Result := do
+    -- TODO
+    return { expr := e }
+
+  evalLambda (e : Expr) : M Result := do
+    -- TODO
+    return { expr := e }
+
+  evalForall (e : Expr) : M Result := do
+    -- TODO
+    return { expr := e }
+
+  congrArgs (r : Result) (args : Array Expr) : M Result := do
+    Simp.congrArgs seval pure r args
+
+  /-- Try to use automatically generated congruence theorems. See `mkCongrSimp?`. -/
+  tryAutoCongrTheorem? (e : Expr) : M (Option Result) := do
+    Simp.tryAutoCongrTheorem? seval pure e
+
+  congr (e : Expr) : M Result := do
+    if let some result ← tryAutoCongrTheorem? e then
+      return result
+    else
+      e.withApp fun f args => do
+        congrArgs (← seval f) args
+
+  evalApp (e : Expr) : M Result := do
+    -- TODO
+    congr e
+
+def main (e : Expr) (ctx : Context): MetaM Result := do
+  try
+    withoutCatchingRuntimeEx do
+      let (r, _) ← seval e ctx |>.run {}
+      return r
+  catch ex =>
+    if ex.isRuntime then throwNestedTacticEx `seval ex else throw ex
+
+end SymEval
+
+def seval (e : Expr) (ctx : SymEval.Context) : MetaM SymEval.Result := do profileitM Exception "seval" (← getOptions) do
+  SymEval.main e ctx
+
+/-- See `sevalTarget`. This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/
+def sevalTargetCore (mvarId : MVarId) (ctx : SymEval.Context) : MetaM (Option MVarId) := do
+  let target ← instantiateMVars (← mvarId.getType)
+  let r ← seval target ctx
+  if r.expr.consumeMData.isConstOf ``True then
+    match r.proof? with
+    | some proof => mvarId.assign (← mkOfEqTrue proof)
+    | none => mvarId.assign (mkConst ``True.intro)
+    return none
+  else
+    applySimpResultToTarget mvarId target r
+
+/--
+  Symbolic evaluate the given goal target (aka type).
+  Return `none` if the goal was closed. Return `some mvarId'` otherwise,
+  where `mvarId'` is the new reduced goal.
+-/
+def sevalTarget (mvarId : MVarId) (ctx : SymEval.Context := {}) : MetaM (Option MVarId) :=
+  mvarId.withContext do
+    mvarId.checkNotAssigned `seval
+    sevalTargetCore mvarId ctx
+
+end Lean.Meta

src/Lean/Meta/Tactic/SymEval/Types.lean

@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.Tactic.Simp.Types
+
+namespace Lean.Meta.SymEval
+
+/-!
+The `seval` tactic is similar to `simp`, but it is optimized for reducing nested ground
+terms, and performing partial evaluation.
+-/
+
+/--
+Configuration options for `seval` tactic.
+-/
+-- TODO: move to `Init`
+structure Config where
+  maxSteps : Nat := 100000
+  deriving Inhabited
+
+structure Context where
+  config         : Config := {}
+  /-- `ground` is true when visiting a ground term. -/
+  ground         : Bool := false
+  simpTheorems   : SimpTheoremsArray := {}
+  congrTheorems  : SimpCongrTheorems := {}
+  dischargeDepth : Nat := 0
+  deriving Inhabited
+
+export Simp (Cache CongrCache Result)
+
+/--
+State for the `seval` tactic.
+TODO: better support for hash-consing.
+-/
+structure State where
+  cache        : Cache := {}
+  congrCache   : CongrCache := {}
+  numSteps     : Nat := 0
+
+abbrev M := ReaderT Context $ StateRefT State MetaM
+
+instance : Simp.MonadCongrCache M where
+  find? f := return (← get).congrCache.find? f
+  save f thm? := modify fun s => { s with congrCache := s.congrCache.insert f thm? }
+
+def getConfig : M Config :=
+  return (← read).config
+
+def getSimpTheorems : M SimpTheoremsArray :=
+  return (← read).simpTheorems
+
+def getSimpCongrTheorems : M SimpCongrTheorems :=
+  return (← read).congrTheorems
+
+end Lean.Meta.SymEval