feat: congr_simp as realizable constant

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/CongrTheorems.lean

@@ -366,42 +366,53 @@ def congrSimpSuffix := "congr_simp"
 
 builtin_initialize congrKindsExt : MapDeclarationExtension (Array CongrArgKind) ← mkMapDeclarationExtension
 
-builtin_initialize registerReservedNamePredicate fun env n =>
-  match n with
-  | .str p s => (isHCongrReservedNameSuffix s || s == congrSimpSuffix) && env.isSafeDefinition p
-  | _ => false
+private def deriveHCongrConst (declName : Name) (congrDeclName : Name) (numArgs : Nat) : MetaM Bool := do
+  try
+    realizeConst declName congrDeclName do
+      let info ← getConstInfo declName
+      let f := mkConst declName (info.levelParams.map mkLevelParam)
+      let congrThm ← mkHCongrWithArity f numArgs
+      addDecl <| Declaration.thmDecl {
+          name := congrDeclName, type := congrThm.type, value := congrThm.proof
+          levelParams := info.levelParams
+      }
+      modifyEnv fun env => congrKindsExt.insert env congrDeclName congrThm.argKinds
+    return true
+  catch _ =>
+    return false
+
+private def deriveSimpCongr (declName : Name) (congrDeclName : Name) : MetaM Bool := do
+  try
+    realizeConst declName congrDeclName do
+      let cinfo ← getConstInfo declName
+      let f := mkConst declName (cinfo.levelParams.map mkLevelParam)
+      let info ← getFunInfo f
+      let some congrThm ← mkCongrSimpCore? f info (← getCongrSimpKinds f info)
+        | throwError "`mkCongrSimpCore?` failed at {f}"
+      addDecl <| Declaration.thmDecl {
+          name := congrDeclName, type := congrThm.type, value := congrThm.proof
+          levelParams := cinfo.levelParams
+      }
+      modifyEnv fun env => congrKindsExt.insert env congrDeclName congrThm.argKinds
+    return true
+  catch _ =>
+    return false
+
+builtin_initialize
+  registerReservedNamePredicate fun env n =>
+    match n with
+    | .str p s => (isHCongrReservedNameSuffix s || s == congrSimpSuffix) && env.isSafeDefinition p
+    | _ => false
 
 builtin_initialize
   registerReservedNameAction fun name => do
     let .str p s := name | return false
     unless (← getEnv).isSafeDefinition p do return false
     if isHCongrReservedNameSuffix s then
       let numArgs := (s.drop 7).toNat!
-      try MetaM.run' do
-        let info ← getConstInfo p
-        let f := mkConst p (info.levelParams.map mkLevelParam)
-        let congrThm ← mkHCongrWithArity f numArgs
-        addDecl <| Declaration.thmDecl {
-           name, type := congrThm.type, value := congrThm.proof
-           levelParams := info.levelParams
-        }
-        modifyEnv fun env => congrKindsExt.insert env name congrThm.argKinds
-        return true
-      catch _ => return false
+      MetaM.run' do deriveHCongrConst p name numArgs
     else if s == congrSimpSuffix then
-      try MetaM.run' do
-        let cinfo ← getConstInfo p
-        let f := mkConst p (cinfo.levelParams.map mkLevelParam)
-        let info ← getFunInfo f
-        let some congrThm ← mkCongrSimpCore? f info (← getCongrSimpKinds f info)
-          | return false
-        addDecl <| Declaration.thmDecl {
-           name, type := congrThm.type, value := congrThm.proof
-           levelParams := cinfo.levelParams
-        }
-        modifyEnv fun env => congrKindsExt.insert env name congrThm.argKinds
-        return true
-      catch _ => return false
+      MetaM.run' do deriveSimpCongr p name
     else
       return false
 
@@ -413,8 +424,7 @@ def mkHCongrWithArityForConst? (declName : Name) (levels : List Level) (numArgs
   try
     let suffix := hcongrThmSuffixBasePrefix ++ toString numArgs
     let thmName := Name.str declName suffix
-    unless (← getEnv).contains thmName do
-      let _ ← executeReservedNameAction thmName
+    discard <| realizeGlobalConstNoOverloadCore thmName
     let proof := mkConst thmName levels
     let type ← inferType proof
     let some argKinds := congrKindsExt.find? (← getEnv) thmName
@@ -430,8 +440,7 @@ same congruence theorem over and over again.
 def mkCongrSimpForConst? (declName : Name) (levels : List Level) : MetaM (Option CongrTheorem) := do
   try
     let thmName := Name.str declName congrSimpSuffix
-    unless (← getEnv).contains thmName do
-      let _ ← executeReservedNameAction thmName
+    discard <| realizeGlobalConstNoOverloadCore thmName
     let proof := mkConst thmName levels
     let type ← inferType proof
     let some argKinds := congrKindsExt.find? (← getEnv) thmName

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

@@ -650,7 +650,12 @@ def mkCongrSimp? (f : Expr) : SimpM (Option CongrTheorem) := do
   match (← get).congrCache[f]? with
   | some thm? => return thm?
   | none =>
-    let thm? ← mkCongrSimpCore? f info kinds
+    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
     modify fun s => { s with congrCache := s.congrCache.insert f thm? }
     return thm?