feat: add generalize and replaceLocalDecl

src/Init/Lean/Meta/AppBuilder.lean

@@ -202,5 +202,11 @@ else do
       pure $ mkAppN (mkConst `Eq.rec [u1, u2]) #[α, a, motive, h1, b, h2]
     | _ => throwEx $ Exception.appBuilder `Eq.rec "invalid motive" #[motive]
 
+def mkEqMP (eqProof pr : Expr) : MetaM Expr :=
+mkAppM `Eq.mp #[eqProof, pr]
+
+def mkEqMPR (eqProof pr : Expr) : MetaM Expr :=
+mkAppM `Eq.mpr #[eqProof, pr]
+
 end Meta
 end Lean

src/Init/Lean/Meta/LevelDefEq.lean

@@ -189,8 +189,7 @@ numPostponed ← getNumPostponed;
 if numPostponed == 0 then pure true
 else traceCtx `Meta.isLevelDefEq.postponed $ processPostponedAux ()
 
-
-private def restore (env : Environment) (mctx : MetavarContext) (postponed : PersistentArray PostponedEntry) : MetaM Unit :=
+def restore (env : Environment) (mctx : MetavarContext) (postponed : PersistentArray PostponedEntry) : MetaM Unit :=
 modify $ fun s => { env := env, mctx := mctx, postponed := postponed, .. s }
 
 /--

src/Init/Lean/Meta/Tactic.lean

@@ -12,3 +12,5 @@ import Init.Lean.Meta.Tactic.Clear
 import Init.Lean.Meta.Tactic.Assert
 import Init.Lean.Meta.Tactic.Target
 import Init.Lean.Meta.Tactic.Rewrite
+import Init.Lean.Meta.Tactic.Generalize
+import Init.Lean.Meta.Tactic.LocalDecl

src/Init/Lean/Meta/Tactic/Generalize.lean

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Lean.Meta.KAbstract
+import Init.Lean.Meta.Tactic.Util
+
+namespace Lean
+namespace Meta
+
+def generalize (mvarId : MVarId) (e : Expr) (x : Name) : MetaM MVarId := do
+withMVarContext mvarId $ do
+  checkNotAssigned mvarId `generalize;
+  tag ← getMVarTag mvarId;
+  target ← getMVarType mvarId;
+  target ← instantiateMVars target;
+  targetAbst ← kabstract target e;
+  unless targetAbst.hasLooseBVars $
+    throwTacticEx `generalize mvarId ("failed to find expression in the target");
+  eType ← inferType e;
+  let targetNew := Lean.mkForall x BinderInfo.default eType targetAbst;
+  unlessM (isTypeCorrect targetNew) $
+    throwTacticEx `generalize mvarId ("result is not type correct");
+  mvarNew ← mkFreshExprSyntheticOpaqueMVar targetNew tag;
+  assignExprMVar mvarId (mkApp mvarNew e);
+  pure mvarNew.mvarId!
+
+end Meta
+end Lean

src/Init/Lean/Meta/Tactic/Intro.lean

@@ -68,8 +68,8 @@ def intro (mvarId : MVarId) (name : Name) : MetaM (FVarId × MVarId) := do
 (fvarIds, mvarId) ← introN mvarId 1 [name];
 pure (fvarIds.get! 0, mvarId)
 
-def intro1 (mvarId : MVarId) : MetaM (FVarId × MVarId) := do
-(fvarIds, mvarId) ← introN mvarId 1 [];
+def intro1 (mvarId : MVarId) (useUnusedNames := true) : MetaM (FVarId × MVarId) := do
+(fvarIds, mvarId) ← introN mvarId 1 [] useUnusedNames;
 pure (fvarIds.get! 0, mvarId)
 
 end Meta

src/Init/Lean/Meta/Tactic/LocalDecl.lean

@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Lean.Meta.AppBuilder
+import Init.Lean.Meta.Tactic.Util
+import Init.Lean.Meta.Tactic.Assert
+import Init.Lean.Meta.Tactic.Intro
+import Init.Lean.Meta.Tactic.Clear
+
+namespace Lean
+namespace Meta
+
+def replaceLocalDecl (mvarId : MVarId) (fvarId : FVarId) (newType : Expr) (eqProof : Expr) : MetaM (FVarId × MVarId) := do
+withMVarContext mvarId $ do
+  localDecl ← getLocalDecl fvarId;
+  newTypePr ← mkEqMP eqProof (mkFVar fvarId);
+  mvarId ← assert mvarId localDecl.userName newType newTypePr;
+  (fvarIdNew, mvarId) ← intro1 mvarId;
+  (do mvarId ← clear mvarId fvarId; pure (fvarIdNew, mvarId)) <|> pure (fvarIdNew, mvarId)
+
+end Meta
+end Lean

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

@@ -40,7 +40,7 @@ withMVarContext mvarId $ do
         eEqE ← mkEq e e;
         let eEqEAbst := mkApp eEqE.appFn! eAbst;
         let motive := Lean.mkLambda `_a BinderInfo.default α eEqEAbst;
-        unlessM (withAtLeastTransparency TransparencyMode.default $ isTypeCorrect motive) $
+        unlessM (isTypeCorrect motive) $
           throwTacticEx `rewrite mvarId ("motive is not type correct");
         eqRefl ← mkEqRefl e;
         eqPrf ← mkEqNDRec motive eqRefl heq;

src/Init/Lean/Meta/Tactic/Util.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Lean.Meta.Basic
+import Init.Lean.Meta.LevelDefEq
 
 namespace Lean
 namespace Meta
@@ -36,6 +37,11 @@ mctx ← getMCtx;
 opts ← getOptions;
 pure $ ppGoal env mctx opts mvarId
 
+@[inline] protected def orelse{α} (x y : MetaM α) : MetaM α := do
+s ← get; catch x (fun _ => do restore s.env s.mctx s.postponed; y)
+
+instance Meta.hasOrelse {α} : HasOrelse (MetaM α) := ⟨Meta.orelse⟩
+
 @[init] private def regTraceClasses : IO Unit :=
 registerTraceClass `Meta.Tactic