feat: generalize e = x at h

src/Init/Tactics.lean

@@ -573,10 +573,13 @@ syntax (name := induction) "induction " term,+ (" using " ident)?
 syntax generalizeArg := atomic(ident " : ")? term:51 " = " ident
 
 /--
-`generalize ([h :] e = x),+` replaces all occurrences `e`s in the main goal
-with a fresh hypothesis `x`s. If `h` is given, `h : e = x` is introduced as well.
+* `generalize ([h :] e = x),+` replaces all occurrences `e`s in the main goal
+  with a fresh hypothesis `x`s. If `h` is given, `h : e = x` is introduced as well.
+* `generalize e = x at h₁ ... hₙ` also generalizes occurrences of `e`
+  inside `h₁`, ..., `hₙ`.
+* `generalize e = x at *` will generalize occurrences of `e` everywhere.
 -/
-syntax (name := generalize) "generalize " generalizeArg,+ : tactic
+syntax (name := generalize) "generalize " generalizeArg,+ (location)? : tactic
 
 /--
 A `cases` argument, of the form `e` or `h : e` (where `h` asserts that

src/Lean/Elab/Tactic/Generalize.lean

@@ -7,6 +7,7 @@ import Lean.Meta.Tactic.Generalize
 import Lean.Meta.Check
 import Lean.Meta.Tactic.Intro
 import Lean.Elab.Tactic.ElabTerm
+import Lean.Elab.Tactic.Location
 
 namespace Lean.Elab.Tactic
 open Meta
@@ -17,8 +18,11 @@ open Meta
       let hName? := if arg[0].isNone then none else some arg[0][0].getId
       let expr ← elabTerm arg[1] none
       return { hName?, expr, xName? := arg[3].getId : GeneralizeArg }
+    let hyps ← match expandOptLocation stx[2] with
+    | .targets hyps _ => getFVarIds hyps
+    | .wildcard => pure (← getLCtx).getFVarIds
     liftMetaTactic fun mvarId => do
-      let (_, mvarId) ← mvarId.generalize args
+      let (_, _, mvarId) ← mvarId.generalizeHyp args hyps
       return [mvarId]
 
 end Lean.Elab.Tactic

src/Lean/Meta/Tactic/Generalize.lean

@@ -6,6 +6,8 @@ Authors: Leonardo de Moura
 import Lean.Meta.KAbstract
 import Lean.Meta.Tactic.Util
 import Lean.Meta.Tactic.Intro
+import Lean.Meta.Tactic.FVarSubst
+import Lean.Meta.Tactic.Revert
 
 namespace Lean.Meta
 
@@ -26,8 +28,8 @@ private partial def generalizeCore (mvarId : MVarId) (args : Array GeneralizeArg
     let tag ← mvarId.getTag
     let target ← instantiateMVars (← mvarId.getType)
     let rec go (i : Nat) : MetaM Expr := do
-      if i < args.size then
-        let arg := args[i]!
+      if _h : i < args.size then
+        let arg := args[i]
         let e ← instantiateMVars arg.expr
         let eType ← instantiateMVars (← inferType e)
         let type ← go (i+1)
@@ -46,16 +48,16 @@ private partial def generalizeCore (mvarId : MVarId) (args : Array GeneralizeArg
     else
       let (rfls, targetNew) ← forallBoundedTelescope targetNew args.size fun xs type => do
         let rec go' (i : Nat) : MetaM (List Expr × Expr) := do
-          if i < xs.size then
+          if _h : i < xs.size then
             let arg := args[i]!
             if let some hName := arg.hName? then
-              let xType ← inferType xs[i]!
+              let xType ← inferType xs[i]
               let e ← instantiateMVars arg.expr
               let eType ← instantiateMVars (← inferType e)
               let (hType, r) ← if (← isDefEq xType eType) then
-                pure (← mkEq e xs[i]!, ← mkEqRefl e)
+                pure (← mkEq e xs[i], ← mkEqRefl e)
               else
-                pure (← mkHEq e xs[i]!, ← mkHEqRefl e)
+                pure (← mkHEq e xs[i], ← mkHEqRefl e)
               let (rs, type) ← go' (i+1)
               return (r :: rs, mkForall hName BinderInfo.default hType type)
             else
@@ -68,15 +70,36 @@ private partial def generalizeCore (mvarId : MVarId) (args : Array GeneralizeArg
       mvarId.assign (mkAppN (mkAppN mvarNew es) rfls.toArray)
       mvarNew.mvarId!.introNP (args.size + rfls.length)
 
-/--
-Telescopic `generalize` tactic. It can simultaneously generalize many terms.
-It uses `kabstract` to occurrences of the terms that need to be generalized.
--/
+@[inheritDoc generalizeCore]
 def _root_.Lean.MVarId.generalize (mvarId : MVarId) (args : Array GeneralizeArg) : MetaM (Array FVarId × MVarId) :=
   generalizeCore mvarId args
 
-@[deprecated MVarId.generalize]
+@[inheritDoc generalizeCore, deprecated MVarId.generalize]
 def generalize (mvarId : MVarId) (args : Array GeneralizeArg) : MetaM (Array FVarId × MVarId) :=
   generalizeCore mvarId args
 
+/--
+Extension of `generalize` to support generalizing within specified hypotheses.
+The `hyps` array contains the list of hypotheses within which to look for occurrences
+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
+  if hyps.isEmpty then
+    -- trivial case
+    return (fvarSubst, ← mvarId.generalize args)
+  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
+  let (reverted, mvarId) ← mvarId.revert hyps true
+  let (newVars, mvarId) ← mvarId.generalize args
+  let (reintros, mvarId) ← mvarId.introNP reverted.size
+  let fvarSubst := Id.run do
+    let mut subst : FVarSubst := fvarSubst
+    for h in reverted, reintro in reintros do
+      subst := subst.insert h (mkFVar reintro)
+    pure subst
+  return (fvarSubst, newVars, mvarId)
+
 end Lean.Meta