From 76403367baa8b3c8a4448c383febe845c37933da Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Mon, 29 Sep 2025 17:02:43 +0200 Subject: [PATCH] fix: remove superfluous `Monad` instances from some spec lemmas (#10564) (#10618) This PR removes superfluous `Monad` instances from the spec lemmas of the `MonadExceptOf` lifting framework. It also adds a bit of documentation and more tracing to `mvcgen`. Fixes #10564. --- src/Lean/Elab/Tactic/Do/VCGen.lean | 78 +++++++++++++++++------------- src/Lean/MetavarContext.lean | 10 ++++ src/Std/Do/Triple/SpecLemmas.lean | 10 ++-- tests/lean/run/10564.lean | 32 ++++++++++++ 4 files changed, 91 insertions(+), 39 deletions(-) create mode 100644 tests/lean/run/10564.lean diff --git a/src/Lean/Elab/Tactic/Do/VCGen.lean b/src/Lean/Elab/Tactic/Do/VCGen.lean index 8b952bb58f..0410b6b3bb 100644 --- a/src/Lean/Elab/Tactic/Do/VCGen.lean +++ b/src/Lean/Elab/Tactic/Do/VCGen.lean @@ -57,7 +57,7 @@ partial def genVCs (goal : MVarId) (ctx : Context) (fuel : Fuel) : MetaM Result mv.setTag (Name.mkSimple ("inv" ++ toString (idx + 1))) for h : idx in [:state.vcs.size] do let mv := state.vcs[idx] - mv.setTag (Name.mkSimple ("vc" ++ toString (idx + 1)) ++ (← mv.getTag)) + mv.setTag (Name.mkSimple ("vc" ++ toString (idx + 1)) ++ (← mv.getTag).eraseMacroScopes) return { invariants := state.invariants, vcs := state.vcs } where onFail (goal : MGoal) (name : Name) : VCGenM Expr := do @@ -85,9 +85,11 @@ where let ty ← mvar.getType if ← isProp ty then -- Might contain more `P ⊢ₛ wp⟦prog⟧ Q` apps. Try and prove it! - mvar.assign (← tryGoal ty (← mvar.getTag)) + 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 @@ -124,7 +126,7 @@ where let e ← instantiateMVarsIfMVarApp e let e := e.headBeta let goal := goal.withNewProg e -- to persist the instantiation of `e` and `trans` - trace[Elab.Tactic.Do.vcgen] "Program: {e}" + withTraceNode `Elab.Tactic.Do.vcgen (msg := fun _ => return m!"Program: {e}") do -- let-expressions if let .letE x ty val body _nonDep := e.getAppFn' then @@ -179,6 +181,7 @@ where let res ← Simp.mkCongrArg context res return ← res.mkEqMPR prf assignMVars specHoles.toList + trace[Elab.Tactic.Do.vcgen] "Unassigned specHoles: {(← specHoles.filterM (not <$> ·.isAssigned)).map fun m => (m.name, mkMVar m)}" return prf return ← onFail goal name @@ -373,36 +376,36 @@ def elabInvariants (stx : Syntax) (invariants : Array MVarId) (suggestInvariant let mut dotOrCase := LBool.undef -- .true => dot for h : n in 0...alts.size do - let alt := alts[n] - match alt with - | `(invariantDotAlt| · $rhs) => - if dotOrCase matches .false then - logErrorAt alt m!"Alternation between labelled and bulleted invariants is not supported." - break - dotOrCase := .true - let some mv := invariants[n]? | do - logErrorAt alt m!"More invariants have been defined ({alts.size}) than there were unassigned invariants goals `inv` ({invariants.size})." - continue - withRef rhs do - discard <| evalTacticAt (← `(tactic| exact $rhs)) mv - | `(invariantCaseAlt| | $tag $args* => $rhs) => - if dotOrCase matches .true then - logErrorAt alt m!"Alternation between labelled and bulleted invariants is not supported." - break - dotOrCase := .false - let n? : Option Nat := do - let `(binderIdent| $tag:ident) := tag | some n -- fall back to ordinal - let .str .anonymous s := tag.getId | none - s.dropPrefix? "inv" >>= Substring.toNat? - let some mv := do invariants[(← n?) - 1]? | do - logErrorAt alt m!"No invariant with label {tag} {repr tag}." - continue - if ← mv.isAssigned then - logErrorAt alt m!"Invariant {n?.get!} is already assigned." - continue - withRef rhs do - discard <| evalTacticAt (← `(tactic| rename_i $args*; exact $rhs)) mv - | _ => logErrorAt alt m!"Expected `invariantDotAlt`, got {alt}" + let alt := alts[n] + match alt with + | `(invariantDotAlt| · $rhs) => + if dotOrCase matches .false then + logErrorAt alt m!"Alternation between labelled and bulleted invariants is not supported." + break + dotOrCase := .true + let some mv := invariants[n]? | do + logErrorAt alt m!"More invariants have been defined ({alts.size}) than there were unassigned invariants goals `inv` ({invariants.size})." + continue + withRef rhs do + discard <| evalTacticAt (← `(tactic| exact $rhs)) mv + | `(invariantCaseAlt| | $tag $args* => $rhs) => + if dotOrCase matches .true then + logErrorAt alt m!"Alternation between labelled and bulleted invariants is not supported." + break + dotOrCase := .false + let n? : Option Nat := do + let `(binderIdent| $tag:ident) := tag | some n -- fall back to ordinal + let .str .anonymous s := tag.getId | none + s.dropPrefix? "inv" >>= Substring.toNat? + let some mv := do invariants[(← n?) - 1]? | do + logErrorAt alt m!"No invariant with label {tag} {repr tag}." + continue + if ← mv.isAssigned then + logErrorAt alt m!"Invariant {n?.get!} is already assigned." + continue + withRef rhs do + discard <| evalTacticAt (← `(tactic| rename_i $args*; exact $rhs)) mv + | _ => logErrorAt alt m!"Expected `invariantDotAlt`, got {alt}" if let `(invariantsKW| invariants) := invariantsKW then if alts.size < invariants.size then @@ -469,12 +472,16 @@ def elabMVCGen : Tactic := fun stx => withMainContext do let goal ← getMainGoal let goal ← if ctx.config.elimLets then elimLets goal else pure goal let { invariants, vcs } ← VCGen.genVCs goal ctx fuel + trace[Elab.Tactic.Do.vcgen] "after genVCs {← (invariants ++ vcs).mapM fun m => m.getTag}" let runOnVCs (tac : TSyntax `tactic) (vcs : Array MVarId) : TermElabM (Array MVarId) := vcs.flatMapM fun vc => List.toArray <$> Term.withSynthesize do Tactic.run vc (Tactic.evalTactic tac *> Tactic.pruneSolvedGoals) let invariants ← Term.TermElabM.run' do let invariants ← if ctx.config.leave then runOnVCs (← `(tactic| try mleave)) invariants else pure invariants + trace[Elab.Tactic.Do.vcgen] "before elabInvariants {← (invariants ++ vcs).mapM fun m => m.getTag}" elabInvariants stx[3] invariants (suggestInvariant vcs) + let invariants ← invariants.filterM (not <$> ·.isAssigned) + trace[Elab.Tactic.Do.vcgen] "before trying trivial VCs {← (invariants ++ vcs).mapM fun m => m.getTag}" let vcs ← Term.TermElabM.run' do let vcs ← if ctx.config.trivial then runOnVCs (← `(tactic| try mvcgen_trivial)) vcs else pure vcs let vcs ← if ctx.config.leave then runOnVCs (← `(tactic| try mleave)) vcs else pure vcs @@ -482,5 +489,8 @@ def elabMVCGen : Tactic := fun stx => withMainContext do -- Eliminating lets here causes some metavariables in `mkFreshPair_triple` to become nonassignable -- so we don't do it. Presumably some weird delayed assignment thing is going on. -- let vcs ← if ctx.config.elimLets then liftMetaM <| vcs.mapM elimLets else pure vcs + trace[Elab.Tactic.Do.vcgen] "before elabVCs {← (invariants ++ vcs).mapM fun m => m.getTag}" let vcs ← elabVCs stx[4] vcs + trace[Elab.Tactic.Do.vcgen] "before replacing main goal {← (invariants ++ vcs).mapM fun m => m.getTag}" replaceMainGoal (invariants ++ vcs).toList + -- trace[Elab.Tactic.Do.vcgen] "replaced main goal, new: {← getGoals}" diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index d79cae6eda..9bee3b41c6 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -596,6 +596,16 @@ run_meta do let e' ← instantiateMVars e -- e' is `Nat.succ 42`, `?m.773` is assigned to `42` ``` + +There are a few gotchas concerning delayed assignments. + +* Regular assignments take precedence over delayed ones. This happens when an error occurs, in which + case Lean assigns `sorry` to all unassigned metavariables, delayed assigned or not. +* Unless a delayed assigned metavariable `?m := fun fvars => ?pending` is fully applied to its free + variables `fvars`, it will not be instantiated to `?pending`. +* A delayed assigned metavariable `?m := fun fvars => ?pending` that occurs fully applied `?m fvars` + will not be instantiated to `?pending` unless (1) `?pending` is assigned, and (2) the + assignment to `?pending` is ground (i.e., does not contain unassigned metavariables). -/ def instantiateMVars [Monad m] [MonadMCtx m] (e : Expr) : m Expr := do if !e.hasMVar then diff --git a/src/Std/Do/Triple/SpecLemmas.lean b/src/Std/Do/Triple/SpecLemmas.lean index b16c75d800..6280a3ae79 100644 --- a/src/Std/Do/Triple/SpecLemmas.lean +++ b/src/Std/Do/Triple/SpecLemmas.lean @@ -399,7 +399,7 @@ theorem Spec.tryCatch_MonadExcept [MonadExceptOf ε m] [WP m ps] (Q : PostCond Triple (tryCatch x h : m α) (spred(wp⟦MonadExceptOf.tryCatch x h : m α⟧ Q)) spred(Q) := SPred.entails.rfl @[spec] -theorem Spec.throw_ReaderT [WP m sh] [Monad m] [MonadExceptOf ε m] : +theorem Spec.throw_ReaderT [WP m sh] [MonadExceptOf ε m] : Triple (MonadExceptOf.throw e : ReaderT ρ m α) (spred(wp⟦MonadLift.monadLift (MonadExceptOf.throw (ε:=ε) e : m α) : ReaderT ρ m α⟧ Q)) spred(Q) := SPred.entails.rfl @[spec] @@ -407,7 +407,7 @@ theorem Spec.throw_StateT [WP m ps] [Monad m] [MonadExceptOf ε m] (Q : PostCond Triple (MonadExceptOf.throw e : StateT σ m α) (spred(wp⟦MonadLift.monadLift (MonadExceptOf.throw (ε:=ε) e : m α) : StateT σ m α⟧ Q)) spred(Q) := SPred.entails.rfl @[spec] -theorem Spec.throw_ExceptT_lift [WP m ps] [Monad m] [MonadExceptOf ε m] (Q : PostCond α (.except ε' ps)) : +theorem Spec.throw_ExceptT_lift [WP m ps] [MonadExceptOf ε m] (Q : PostCond α (.except ε' ps)) : Triple (ps:=.except ε' ps) (MonadExceptOf.throw e : ExceptT ε' m α) (wp⟦MonadExceptOf.throw (ε:=ε) e : m (Except ε' α)⟧ (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2)) @@ -419,7 +419,7 @@ theorem Spec.throw_ExceptT_lift [WP m ps] [Monad m] [MonadExceptOf ε m] (Q : Po split <;> rfl @[spec] -theorem Spec.tryCatch_ReaderT [WP m ps] [Monad m] [MonadExceptOf ε m] (Q : PostCond α (.arg ρ ps)) : +theorem Spec.tryCatch_ReaderT [WP m ps] [MonadExceptOf ε m] (Q : PostCond α (.arg ρ ps)) : Triple (MonadExceptOf.tryCatch x h : ReaderT ρ m α) (spred(fun r => wp⟦MonadExceptOf.tryCatch (ε:=ε) (x.run r) (fun e => (h e).run r) : m α⟧ (fun a => Q.1 a r, Q.2))) spred(Q) := SPred.entails.rfl @[spec] @@ -427,13 +427,13 @@ theorem Spec.tryCatch_StateT [WP m ps] [Monad m] [MonadExceptOf ε m] (Q : PostC Triple (MonadExceptOf.tryCatch x h : StateT σ m α) (spred(fun s => wp⟦MonadExceptOf.tryCatch (ε:=ε) (x.run s) (fun e => (h e).run s) : m (α × σ)⟧ (fun xs => Q.1 xs.1 xs.2, Q.2))) spred(Q) := SPred.entails.rfl @[spec] -theorem Spec.tryCatch_ExceptT_lift [WP m ps] [Monad m] [MonadExceptOf ε m] (Q : PostCond α (.except ε' ps)) : +theorem Spec.tryCatch_ExceptT_lift [WP m ps] [MonadExceptOf ε m] (Q : PostCond α (.except ε' ps)) : Triple (ps:=.except ε' ps) (MonadExceptOf.tryCatch x h : ExceptT ε' m α) (wp⟦MonadExceptOf.tryCatch (ε:=ε) x h : m (Except ε' α)⟧ (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2)) Q := by - simp only [Triple, WP.tryCatch_lift_ExceptT] + simp only [Triple] apply (wp _).mono simp intro x diff --git a/tests/lean/run/10564.lean b/tests/lean/run/10564.lean new file mode 100644 index 0000000000..85df9aa64b --- /dev/null +++ b/tests/lean/run/10564.lean @@ -0,0 +1,32 @@ +import Std.Tactic.Do +open Std.Do + +set_option mvcgen.warning false + +structure Supply where + counter : Nat + limit : Nat + property : counter ≤ limit + +def mkFreshN2 (n : Nat) : ExceptT Char (EStateM String Supply) (List Nat) := do + let mut acc := #[] + for _ in [:n] do + let supply ← get + if h : supply.counter = supply.limit then + throwThe String s!"Supply exhausted: {supply.counter} = {supply.limit}" + else + let n := supply.counter + have := supply.property + set {supply with counter := n + 1, property := by omega} + acc := acc.push n + pure acc.toList + +theorem mkFreshN2_spec2 (n : Nat) : + ⦃⌜True⌝⦄ + mkFreshN2 n + ⦃post⟨fun r => ⌜r.Nodup⌝, fun _ => ⌜False⌝, fun _msg state => ⌜state.counter = state.limit⌝⟩⦄ := by + mvcgen [mkFreshN2] invariants + · post⟨fun ⟨xs, acc⟩ state => ⌜(∀ n ∈ acc, n < state.counter) ∧ acc.toList.Nodup⌝, + fun _ => ⌜False⌝, + fun _msg state => ⌜state.counter = state.limit⌝⟩ + with grind