fix: instantiate metavariables in hypotheses in grind (#11315)

This PR fixes an issue affecting `grind -revert`. In this mode, assigned
metavariables in hypotheses were not being instantiated. This issue was
affecting two files in Mathlib.

Author: leodemoura

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/MBTC.lean

@@ -16,6 +16,10 @@ private def getAssignmentExt? (e : Expr) : GoalM (Option Rat) := do
   if let some val ← getAssignment? (← get) e then
     -- Easy case when `e : Int`
     return some val
+  /-
+  **Note**: The following code assumes that instantiated mvars occurring in types
+  have been instantiated.
+  -/
   let type ← inferType e
   if type == Int.mkType then
     -- It should have been handled in the previous getAssignment?

src/Lean/Meta/Tactic/Grind/Main.lean

@@ -270,6 +270,11 @@ See issue #11806 for a motivating example.
 def withProtectedMCtx [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m]
     [MonadExcept Exception m] [MonadRuntimeException m]
     (abstractProof : Bool) (mvarId : MVarId) (k : MVarId → m α) : m α := do
+  /-
+  **Note**: `instantiateGoalMVars` here also instantiates mvars occurring in hypotheses.
+  This is particularly important when using `grind -revert`.
+  -/
+  let mvarId ← mvarId.instantiateGoalMVars
   let mvarId ← mvarId.abstractMVars
   let mvarId ← mvarId.clearImplDetails
   tryCatchRuntimeEx (main mvarId) fun ex => do

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

@@ -19,6 +19,18 @@ def _root_.Lean.MVarId.ensureNoMVar (mvarId : MVarId) : MetaM Unit := do
   if type.hasExprMVar then
     throwTacticEx `grind mvarId "goal contains metavariables"
 
+/--
+Instantiates metavariables occurring in the target and hypotheses.
+-/
+def _root_.Lean.MVarId.instantiateGoalMVars (mvarId : MVarId) : MetaM MVarId := do
+  mvarId.checkNotAssigned `grind
+  let mvarDecl ← mvarId.getDecl
+  let lctx ← instantiateLCtxMVars mvarDecl.lctx
+  let type ← Lean.instantiateMVars mvarDecl.type
+  let mvarNew ← mkFreshExprMVarAt lctx mvarDecl.localInstances type .syntheticOpaque mvarDecl.userName
+  mvarId.assign mvarNew
+  return mvarNew.mvarId!
+
 /-- Abstracts metavariables occurring in the target. -/
 def _root_.Lean.MVarId.abstractMVars (mvarId : MVarId) : MetaM MVarId := do
   mvarId.checkNotAssigned `grind

tests/lean/run/grind_inst_mvars_issue.lean

@@ -0,0 +1,36 @@
+namespace Nat
+
+def ascFactorial (n : Nat) : Nat → Nat
+  | 0 => 1
+  | k + 1 => (n + k) * ascFactorial n k
+
+def descFactorial (n : Nat) : Nat → Nat
+  | 0 => 1
+  | k + 1 => (n - k) * descFactorial n k
+
+theorem descFactorial_of_lt {n : Nat} : ∀ {k : Nat}, n < k → n.descFactorial k = 0 := by sorry
+
+theorem add_descFactorial_eq_ascFactorial' (n : Nat) :
+    ∀ k : Nat, (n + k - 1).descFactorial k = n.ascFactorial k := by sorry
+
+def ascFactorialBinary (n k : Nat) : Nat :=
+  match k with
+  | 0 => 1
+  | 1 => n
+  | k@(_ + 2) => ascFactorialBinary n (k / 2) * ascFactorialBinary (n + k / 2) ((k + 1) / 2)
+
+theorem ascFactorial_eq_ascFactorialBinary : ascFactorial = ascFactorialBinary := sorry
+
+def descFactorialBinary (n k : Nat) : Nat :=
+  if n < k then 0
+  else ascFactorialBinary (n - k + 1) k
+
+theorem descFactorial_eq_descFactorialBinary : descFactorial = descFactorialBinary := by
+  ext n k
+  rw [descFactorialBinary]
+  split <;> rename_i h
+  · rw [descFactorial_of_lt h]
+  · rw [← ascFactorial_eq_ascFactorialBinary, ← add_descFactorial_eq_ascFactorial']
+    grind
+
+end Nat