From 63354ce59483f0126d9d6c1fe0efa2ee9b6b3de6 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Wed, 1 Oct 2025 17:03:09 +0200 Subject: [PATCH] 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`. --- src/Lean/Elab/Tactic/Do/Spec.lean | 11 ++++++++- .../lean/run/mspecInvariantInstantiation.lean | 23 +++++++++++++++++++ 2 files changed, 33 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/mspecInvariantInstantiation.lean diff --git a/src/Lean/Elab/Tactic/Do/Spec.lean b/src/Lean/Elab/Tactic/Do/Spec.lean index 0cf468a43f..e2a58bc79b 100644 --- a/src/Lean/Elab/Tactic/Do/Spec.lean +++ b/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 diff --git a/tests/lean/run/mspecInvariantInstantiation.lean b/tests/lean/run/mspecInvariantInstantiation.lean new file mode 100644 index 0000000000..8454d0a824 --- /dev/null +++ b/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