fix: spurious invariant instantiation in mspec by rfl (#10641)

This PR ensures that the `mspec` and `mvcgen` tactics no longer
spuriously instantiate loop invariants by `rfl`.

Author: sgraf812

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

@@ -159,7 +159,16 @@ def mSpec (goal : MGoal) (elabSpecAtWP : Expr → n SpecTheorem) (goalTag : Name
   mTryFrame goal fun goal => do
 
   -- Fully instantiate the specThm without instantiating its MVars to `wp` yet
-  let (_, _, spec, specTy) ← specThm.proof.instantiate
+  let (mvars, _, spec, specTy) ← specThm.proof.instantiate
+
+  -- Instantiation creates `.natural` MVars, which possibly get instantiated by the def eq checks
+  -- below when they occur in `P` or `Q`.
+  -- That's good for many such as MVars ("schematic variables"), but problematic for MVars
+  -- corresponding to `Invariant`s, which should end up as user goals.
+  -- To prevent accidental instantiation, we mark all `Invariant` MVars as synthetic opaque.
+  for mvar in mvars do
+    let ty ← mvar.mvarId!.getType
+    if ty.isAppOf ``Invariant then mvar.mvarId!.setKind .syntheticOpaque
 
   -- Apply the spec to the excess arguments of the `wp⟦e⟧ Q` application
   let T := goal.target.consumeMData

tests/lean/run/mspecInvariantInstantiation.lean

@@ -0,0 +1,23 @@
+import Std.Tactic.Do
+import Std.Do.WP.Basic
+
+def tst (n : Nat) : Vector Bool n := Id.run do
+  let mut res : Vector Bool n := .ofFn fun _ ↦ false
+  for i in [:n] do
+    for j in [:n] do
+      if i = j ∧ i % 2 = 0 then
+        res := res.set! i true
+  return res
+
+set_option warn.sorry false in
+open Std.Do in
+example (n i : Nat) (h : i < n) : (tst n)[i] = (i % 2 == 0) := by
+  generalize h : tst n = bs
+  apply Std.Do.Id.of_wp_run_eq h
+  mvcgen
+  -- We should see `inv1` and `inv2` here as separate goals.
+  -- `inv2` should not have been spuriously instantiated in terms of `inv1`.
+  -- Used to happen because `inv2` was born natural and got instantiated in a .rfl test.
+  case inv1 => sorry
+  case inv2 => sorry
+  all_goals sorry