From 65906d9ccc6c7cbf75736346039617ca6d2f0efe Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Wed, 6 May 2026 19:58:03 +0200 Subject: [PATCH] test: unfold reducible abbreviations in inline-elaborated invariant values (#13668) This PR fixes an issue in the `mvcgen'` prototype where user-provided invariant values were elaborated against a goal type containing reducible abbreviations like `PostShape.args ps`, baking `(PostShape.args PostShape.pure)` into the assignment instead of `[]`. After `tryInlineInvariant` confirms the user tactic assigned the invariant metavariable, reduce its assignment with `unfoldReducible`. Fixes the `mvcgen'` migration path for several `tests/elab/*` proofs that had been blocked on the entailment-phase apply failure. Co-authored-by: Sebastian Graf --- tests/bench/mvcgen/sym/lib/VCGen/Driver.lean | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/tests/bench/mvcgen/sym/lib/VCGen/Driver.lean b/tests/bench/mvcgen/sym/lib/VCGen/Driver.lean index 4f82b03e40..ac6789bec2 100644 --- a/tests/bench/mvcgen/sym/lib/VCGen/Driver.lean +++ b/tests/bench/mvcgen/sym/lib/VCGen/Driver.lean @@ -68,7 +68,15 @@ private meta def tryInlineInvariant (n : Nat) (mv : MVarId) : VCGenM Bool := do let _ ← Lean.Elab.runTactic mv tac {} {} -- The tactic runs without throwing even when it fails to close the goal; -- check explicitly that the MVar got assigned. - mv.isAssigned + if ← mv.isAssigned then + -- Preprocess the assignment to `mv` because it will interact with the `SymM` world + if let some val ← getExprMVarAssignment? mv then + let val ← unfoldReducible val + let val ← shareCommon val + mv.assign val + return true + else + return false catch _ => return false