feat: add congrConsts

Author: leodemoura

src/Init/MetaTypes.lean

@@ -240,15 +240,23 @@ structure Config where
   -/
   implicitDefEqProofs : Bool := true
   /--
-  When `true` (default : `true`), then simps will remove unused let-declarations:
+  When `true` (default : `true`), `simp` removes unused let-declarations:
   `let x := v; e` simplifies to `e` when `x` does not occur in `e`.
   -/
   zetaUnused : Bool := true
   /--
-  When `true` (default : `true`), then simps will catch runtime exceptions and
-  convert them into `simp` exceptions.
+  When `true` (default : `true`), `simp` catches runtime exceptions and
+  converts them into `simp` exceptions.
   -/
   catchRuntime : Bool := true
+  /--
+  When `true` (default : `true`), `simp` tries to realize constant `f.congr_simp`
+  when constructing an auxiliary congruence proof for `f`.
+  This option exists because the termination prover uses `simp` and `withoutModifyingEnv`
+  while constructing the termination proof. Thus, any constant realized by `simp`
+  is deleted.
+  -/
+  congrConsts : Bool := true
   deriving Inhabited, BEq
 
 -- Configuration object for `simp_all`

src/Lean/Elab/PreDefinition/WF/Preprocess.lean

@@ -73,7 +73,9 @@ private def getSimpContext : MetaM Simp.Context := do
   Simp.mkContext
     (simpTheorems  := #[simpTheorems])
     (congrTheorems := {})
-    (config        := { Simp.neutralConfig with dsimp := true })
+    -- Remark: we use `congrConsts` because this module uses `withoutModifyingEnv`
+    -- which would erase any congruence lemmas realized in the `withoutModifyingEnv` block.
+    (config        := { Simp.neutralConfig with dsimp := true, congrConsts := false })
 
 def isWfParam? (e : Expr) : Option Expr :=
   if e.isAppOfArity ``wfParam 2 then

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

@@ -650,7 +650,9 @@ def mkCongrSimp? (f : Expr) : SimpM (Option CongrTheorem) := do
   match (← get).congrCache[f]? with
   | some thm? => return thm?
   | none =>
-    let thm? ← if let .const declName us := f then
+    let thm? ← if !(← getConfig).congrConsts then
+      mkCongrSimpCore? f info kinds
+    else if let .const declName us := f then
       mkCongrSimpForConst? declName us
     else
       mkCongrSimpCore? f info kinds