From 2158c9e96f6f33fb0d263e0fa16413b359f7e935 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sat, 2 Mar 2024 16:13:30 -0800
Subject: [PATCH] fix: `generalize` excessive resource usage

closes #3524
---
 src/Lean/Meta/Tactic/Generalize.lean | 71 ++++++++++++++++++++++++----
 tests/lean/run/3524.lean             |  3 ++
 2 files changed, 64 insertions(+), 10 deletions(-)
 create mode 100644 tests/lean/run/3524.lean

diff --git a/src/Lean/Meta/Tactic/Generalize.lean b/src/Lean/Meta/Tactic/Generalize.lean
index d2a9a0df1f2d..82bb252f5164 100644
--- a/src/Lean/Meta/Tactic/Generalize.lean
+++ b/src/Lean/Meta/Tactic/Generalize.lean
@@ -23,7 +23,8 @@ structure GeneralizeArg where
 Telescopic `generalize` tactic. It can simultaneously generalize many terms.
 It uses `kabstract` to occurrences of the terms that need to be generalized.
 -/
-private partial def generalizeCore (mvarId : MVarId) (args : Array GeneralizeArg) : MetaM (Array FVarId × MVarId) :=
+private partial def generalizeCore (mvarId : MVarId) (args : Array GeneralizeArg)
+    (transparency : TransparencyMode) : MetaM (Array FVarId × MVarId) :=
   mvarId.withContext do
     mvarId.checkNotAssigned `generalize
     let tag ← mvarId.getTag
@@ -35,7 +36,8 @@ private partial def generalizeCore (mvarId : MVarId) (args : Array GeneralizeArg
         let eType ← instantiateMVars (← inferType e)
         let type ← go (i+1)
         let xName ← if let some xName := arg.xName? then pure xName else mkFreshUserName `x
-        return Lean.mkForall xName BinderInfo.default eType (← kabstract type e)
+        return Lean.mkForall xName BinderInfo.default eType
+          (← withTransparency transparency <| kabstract type e)
       else
         return target
     let targetNew ← go 0
@@ -71,13 +73,62 @@ private partial def generalizeCore (mvarId : MVarId) (args : Array GeneralizeArg
       mvarId.assign (mkAppN (mkAppN mvarNew es) rfls.toArray)
       mvarNew.mvarId!.introNP (args.size + rfls.length)
 
+/-
+Remark: we use `TransparencyMode.instances` as the default setting at `generalize`
+and `generalizeHyp` to avoid excessive resource usage.
+
+**Motivation:**
+The `kabstract e p` operation is widely used, for instance, in the `generalize` tactic.
+It operates by taking an expression `e` and a pattern (i.e., an expression containing metavariables)
+and employs keyed-matching to identify and abstract instances of `p` within `e`.
+For example, if `e` is `a + (2 * (b + c))` and `p` is `2 * ?m`, the resultant expression
+would be `a + #0`, where `#0` represents a loose bound variable.
+
+This matching process is not merely syntactic; it also considers reduction. It's impractical
+to attempt matching each sub-term with `p`; therefore, only sub-terms sharing the same "root"
+symbol are evaluated. For instance, with the pattern `2 * ?m`, only sub-terms with the
+root `*` are considered. Matching is executed using the definitionally equality test
+(i.e., `isDefEq`).
+
+The `generalize` tactic employs `kabstract` and defaults to standard reducibility.
+Hence, the `isDefEq` operations invoked by `kabstract` can become highly resource-intensive
+and potentially trigger "max recursion depth reached" errors, as observed in issue #3524.
+This issue was isolated by @**Scott Morrison** with the following example:
+```
+example (a : Nat) : ((2 ^ 7) + a) - 2 ^ 7 = 0 := by
+  generalize 0 - 0 = x
+```
+In this scenario, `kabstract` triggers a "max recursion depth reached" error while
+testing whether `((2 ^ 7) + a) - 2 ^ 7` is definitionally equal to `0 - 0`.
+Note that the term `((2 ^ 7) + a) - 2 ^ 7` is not ground.
+We believe most users find the error message to be uninformative and unexpected.
+To fix this issue, we decided to use `TransparencyMode.instances` as the default setting.
+
+Kyle Miller has performed the following analysis on the potential impact of the
+changes on Mathlib (2024-03-02).
+
+There seem to be just 130 cases of generalize in Mathlib, and after looking through a
+good number of them, they seem to come in just two types:
+
+- Ones where it looks like reducible+instance transparency should work, where in
+  particular there is nothing obvious being reduced, and
+- Ones that don't make use of the `kabstract` feature at all (it's being used like a
+  `have` that introduces an equality for rewriting).
+
+That wasn't a systematic review of generalize though. It's possible changing the
+transparency settings would break things, but in my opinion it would be better
+if generalize weren't used for unfolding things.
+-/
+
 @[inherit_doc generalizeCore]
-def _root_.Lean.MVarId.generalize (mvarId : MVarId) (args : Array GeneralizeArg) : MetaM (Array FVarId × MVarId) :=
-  generalizeCore mvarId args
+def _root_.Lean.MVarId.generalize (mvarId : MVarId) (args : Array GeneralizeArg)
+    (transparency := TransparencyMode.instances) : MetaM (Array FVarId × MVarId) :=
+  generalizeCore mvarId args transparency
 
 @[inherit_doc generalizeCore, deprecated MVarId.generalize]
-def generalize (mvarId : MVarId) (args : Array GeneralizeArg) : MetaM (Array FVarId × MVarId) :=
-  generalizeCore mvarId args
+def generalize (mvarId : MVarId) (args : Array GeneralizeArg)
+    (transparency := TransparencyMode.instances) : MetaM (Array FVarId × MVarId) :=
+  generalizeCore mvarId args transparency
 
 /--
 Extension of `generalize` to support generalizing within specified hypotheses.
@@ -85,16 +136,16 @@ The `hyps` array contains the list of hypotheses within which to look for occurr
 of the generalizing expressions.
 -/
 def _root_.Lean.MVarId.generalizeHyp (mvarId : MVarId) (args : Array GeneralizeArg) (hyps : Array FVarId := #[])
-    (fvarSubst : FVarSubst := {}) : MetaM (FVarSubst × Array FVarId × MVarId) := do
+    (fvarSubst : FVarSubst := {}) (transparency := TransparencyMode.instances) : MetaM (FVarSubst × Array FVarId × MVarId) := do
   if hyps.isEmpty then
     -- trivial case
-    return (fvarSubst, ← mvarId.generalize args)
+    return (fvarSubst, ← mvarId.generalize args transparency)
   let args ← args.mapM fun arg => return { arg with expr := ← instantiateMVars arg.expr }
   let hyps ← hyps.filterM fun h => do
     let type ← instantiateMVars (← h.getType)
-    args.anyM fun arg => return (← kabstract type arg.expr).hasLooseBVars
+    args.anyM fun arg => return (← withTransparency transparency <| kabstract type arg.expr).hasLooseBVars
   let (reverted, mvarId) ← mvarId.revert hyps true
-  let (newVars, mvarId) ← mvarId.generalize args
+  let (newVars, mvarId) ← mvarId.generalize args transparency
   let (reintros, mvarId) ← mvarId.introNP reverted.size
   let fvarSubst := Id.run do
     let mut subst : FVarSubst := fvarSubst
diff --git a/tests/lean/run/3524.lean b/tests/lean/run/3524.lean
new file mode 100644
index 000000000000..e63efe1b9d2b
--- /dev/null
+++ b/tests/lean/run/3524.lean
@@ -0,0 +1,3 @@
+example (a : Nat) : ((2 ^ 7) + a) - 2 ^ 7 = 0 := by
+  generalize 0 - 0 = x
+  sorry