From 784a0630922923f3ab8bb7b3b91ad59bf54e0178 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Wed, 1 Oct 2025 18:29:12 +0200 Subject: [PATCH] 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 | 22 +++++++-- src/Lean/Elab/Tactic/Do/VCGen.lean | 36 ++++---------- src/Lean/Elab/Tactic/Do/VCGen/Basic.lean | 8 ++++ tests/lean/run/mvcgenPRangeInst.lean | 61 ++++++++++++++++++++++++ 4 files changed, 96 insertions(+), 31 deletions(-) create mode 100644 tests/lean/run/mvcgenPRangeInst.lean diff --git a/src/Lean/Elab/Tactic/Do/Spec.lean b/src/Lean/Elab/Tactic/Do/Spec.lean index e2a58bc79b..5194ba8550 100644 --- a/src/Lean/Elab/Tactic/Do/Spec.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/Do/VCGen.lean b/src/Lean/Elab/Tactic/Do/VCGen.lean index dc12594dc7..9881eae2a8 100644 --- a/src/Lean/Elab/Tactic/Do/VCGen.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean b/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean index 9ae57f06cc..83782aad54 100644 --- a/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean +++ b/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 diff --git a/tests/lean/run/mvcgenPRangeInst.lean b/tests/lean/run/mvcgenPRangeInst.lean new file mode 100644 index 0000000000..a5ef7934d5 --- /dev/null +++ b/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