fix: try synthesizing synthetic MVars in mspec (#10644)

This PR explicitly tries to synthesize synthetic MVars in `mspec`. Doing
so resolves a bug triggered by use of the loop invariant lemma for
`Std.PRange`.

src/Lean/Elab/Tactic/Do/Spec.lean

@@ -14,15 +14,13 @@ public import Lean.Elab.Tactic.Do.ProofMode.Assumption
 public import Lean.Elab.Tactic.Do.Attr
 public import Std.Do.Triple
 
-public section
-
 namespace Lean.Elab.Tactic.Do
 open Lean Elab Tactic Meta
 open Std.Do Do.SpecAttr Do.ProofMode
 
 builtin_initialize registerTraceClass `Elab.Tactic.Do.spec
 
-def findSpec (database : SpecTheorems) (wp : Expr) : MetaM SpecTheorem := do
+public def findSpec (database : SpecTheorems) (wp : Expr) : MetaM SpecTheorem := do
   let_expr c@WP.wp _m _ps _instWP _α prog := wp | throwError "target not a wp application {wp}"
   let prog ← instantiateMVarsIfMVarApp prog
   let prog := prog.headBeta
@@ -139,7 +137,7 @@ def dischargeMGoal (goal : MGoal) (goalTag : Name) : n Expr := do
 /--
   Returns the proof and the list of new unassigned MVars.
 -/
-def mSpec (goal : MGoal) (elabSpecAtWP : Expr → n SpecTheorem) (goalTag : Name) : n Expr := do
+public def mSpec (goal : MGoal) (elabSpecAtWP : Expr → n SpecTheorem) (goalTag : Name) : n Expr := do
   -- First instantiate `fun s => ...` in the target via repeated `mintro ∀s`.
   mIntroForallN goal goal.target.consumeMData.getNumHeadLambdas fun goal => do
   -- Elaborate the spec for the wp⟦e⟧ app in the target
@@ -177,11 +175,25 @@ def mSpec (goal : MGoal) (elabSpecAtWP : Expr → n SpecTheorem) (goalTag : Name
   let excessArgs := (args.extract 4 args.size).reverse
 
   -- Actually instantiate the specThm using the expected type computed from `wp`.
-  let_expr f@Triple m ps instWP α prog P Q := specTy | do liftMetaM (throwError "target not a Triple application {specTy}")
+  let_expr f@Triple m ps instWP α prog P Q := specTy
+    | liftMetaM <| throwError "target not a Triple application {specTy}"
   let wp' := mkApp5 (mkConst ``WP.wp f.constLevels!) m ps instWP α prog
   unless (← withAssignableSyntheticOpaque <| isDefEq wp wp') do
     Term.throwTypeMismatchError none wp wp' spec
 
+  -- Try synthesizing synthetic MVars. We don't have the convenience of `TermElabM`, hence
+  -- this poor man's version of `TermElabM.synthesizeSyntheticMVars`.
+  -- We do so after the def eq call so that instance resolution is likely to succeed.
+  -- If it _doesn't_ succeed now, then the spec theorem leaves behind an additional subgoal.
+  -- We'll add a trace message if that happens.
+  for mvar in mvars do
+    let mvar := mvar.mvarId!
+    if (← mvar.getKind) matches .synthetic && !(← liftMetaM <| mvar.isAssigned) then
+      match ← trySynthInstance (← mvar.getType) with
+      | .some prf => liftMetaM <| mvar.assign prf
+      | .none => continue
+      | .undef => liftMetaM <| do trace[Elab.Tactic.Do.spec] "Failed to synthesize synthetic MVar {mvar} from unifying {specTy} against {prog}.\nThis likely leaves behind an additional subgoal."
+
   let P ← instantiateMVarsIfMVarApp P
   let Q ← instantiateMVarsIfMVarApp Q
 

src/Lean/Elab/Tactic/Do/VCGen.lean

@@ -64,41 +64,25 @@ where
     -- trace[Elab.Tactic.Do.vcgen] "fail {goal.toExpr}"
     emitVC goal.toExpr name
 
-  tryGoal (goal : Expr) (name : Name) : VCGenM Expr := do
-    -- trace[Elab.Tactic.Do.vcgen] "tryGoal: {goal}"
-    forallTelescope goal fun xs body => do
-      let res ← try mStart body catch _ =>
-        -- trace[Elab.Tactic.Do.vcgen] "not an MGoal: {body}"
-        return ← mkLambdaFVars xs (← emitVC body name)
+  tryGoal (mvar : MVarId) : OptionT VCGenM Expr := mvar.withContext do
+    -- The type might contain more `P ⊢ₛ wp⟦prog⟧ Q` apps. Try and prove it!
+    forallTelescope (← mvar.getType) fun xs body => do
+      let res ← try mStart body catch _ => OptionT.fail
       -- trace[Elab.Tactic.Do.vcgen] "an MGoal: {res.goal.toExpr}"
-      let mut prf ← onGoal res.goal name
+      let mut prf ← onGoal res.goal (← mvar.getTag)
       -- res.goal.checkProof prf
       if let some proof := res.proof? then
         prf := mkApp proof prf
-      mkLambdaFVars xs prf
+      return ← mkLambdaFVars xs prf
 
   assignMVars (mvars : List MVarId) : VCGenM PUnit := do
     for mvar in mvars do
       if ← mvar.isAssigned then continue
-      mvar.withContext <| do
       -- trace[Elab.Tactic.Do.vcgen] "assignMVars {← mvar.getTag}, isDelayedAssigned: {← mvar.isDelayedAssigned},\n{mvar}"
-      let ty ← mvar.getType
-      if ← isProp ty then
-        -- Might contain more `P ⊢ₛ wp⟦prog⟧ Q` apps. Try and prove it!
-        let prf ← tryGoal ty (← mvar.getTag)
-        if ← mvar.isAssigned then
-          throwError "Tried to assign already assigned metavariable `{← mvar.getTag}` while `tryGoal`. MVar: {mvar}\nAssignment: {mkMVar mvar}\nNew assignment: {prf}"
-        mvar.assign prf
-        return
-      if ty.isAppOf ``PostCond || ty.isAppOf ``Invariant || ty.isAppOf ``SPred then
-        -- Here we make `mvar` a synthetic opaque goal upon discharge failure.
-        -- This is the right call for (previously natural) holes such as loop invariants, which
-        -- would otherwise lead to spurious instantiations and unwanted renamings (when leaving the
-        -- scope of a local).
-        -- But it's wrong for, e.g., schematic variables. The latter should never be PostConds,
-        -- Invariants or SPreds, hence the condition.
-        mvar.setKind .syntheticOpaque
-      addSubGoalAsVC mvar
+      let some prf ← (tryGoal mvar).run | addSubGoalAsVC mvar
+      if ← mvar.isAssigned then
+        throwError "Tried to assign already assigned metavariable `{← mvar.getTag}`. MVar: {mvar}\nAssignment: {mkMVar mvar}\nNew assignment: {prf}"
+      mvar.assign prf
 
   onGoal goal name : VCGenM Expr := do
     let T := goal.target

src/Lean/Elab/Tactic/Do/VCGen/Basic.lean

@@ -94,6 +94,14 @@ def ifOutOfFuel (x : VCGenM α) (k : VCGenM α) : VCGenM α := do
 def addSubGoalAsVC (goal : MVarId) : VCGenM PUnit := do
   goal.freshenLCtxUserNamesSinceIdx (← read).initialCtxSize
   let ty ← goal.getType
+  if ty.isAppOf ``Std.Do.PostCond || ty.isAppOf ``Std.Do.SPred then
+    -- Here we make `mvar` a synthetic opaque goal upon discharge failure.
+    -- This is the right call for (previously natural) holes such as loop invariants, which
+    -- would otherwise lead to spurious instantiations and unwanted renamings (when leaving the
+    -- scope of a local).
+    -- But it's wrong for, e.g., schematic variables. The latter should never be PostConds,
+    -- Invariants or SPreds, hence the condition.
+    goal.setKind .syntheticOpaque
   if ty.isAppOf ``Std.Do.Invariant then
     modify fun s => { s with invariants := s.invariants.push goal }
   else

tests/lean/run/mvcgenPRangeInst.lean

@@ -0,0 +1,61 @@
+import Std.Tactic.Do
+
+open Std.Do
+
+set_option warn.sorry false
+set_option mvcgen.warning false
+
+def foo (l : List Nat) : Nat := Id.run do
+  let mut out := 0
+  for _ in l do
+    out := out + 1
+  return out
+
+def bar (n : Nat) : Nat := Id.run do
+  let mut out := 0
+  for _ in 0...n do
+    out := out + 1
+  return out
+
+/-- This works as expected: -/
+theorem foo_eq (l : List Nat) : foo l = l.length := by
+  generalize h : foo l = x
+  apply Id.of_wp_run_eq h
+  mvcgen
+  case inv1 =>
+    exact ⇓⟨xs, out⟩ => ⌜True⌝
+  case vc1 => sorry
+  case vc2 => sorry
+  case vc3 => sorry
+
+/-- This used to fail in `inv1` due to an unresolved `HasFiniteRanges` instance: -/
+theorem bar_eq (n : Nat) : bar n = n := by
+  generalize h : bar n = x
+  apply Id.of_wp_run_eq h
+  mvcgen
+  case inv1 =>
+    -- Invalid match expression: The type of pattern variable 'xs' contains metavariables:
+    -- (0...n).toList.Cursor
+    exact ⇓⟨xs, out⟩ => ⌜True⌝
+  case vc1 => sorry
+  case vc2 => sorry
+  case vc3 => sorry
+
+theorem bar_eq' (n : Nat) : bar n = n := by
+  generalize h : bar n = x
+  apply Id.of_wp_run_eq h
+  mvcgen
+  case inv1 =>
+    exact ⇓⟨xs, out⟩ => ⌜True⌝
+  case vc1 => sorry
+  case vc2 => sorry
+  case vc3 => sorry
+
+/-- Check the same for `mspec` -/
+theorem bar_eq_mspec (n : Nat) : bar n = n := by
+  generalize h : bar n = x
+  apply Id.of_wp_run_eq h
+  mspec
+  -- should not produce a goal for `Std.PRange.HasFiniteRanges Std.PRange.BoundShape.open Nat`
+  fail_if_success case inst => exact inferInstance
+  all_goals sorry