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.
2025-09-29 17:02:43 +02:00 · 2025-09-29 17:02:43 +02:00 · 76403367ba
commit 76403367ba
parent c016bb9434
4 changed files with 91 additions and 39 deletions
--- 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<n>` ({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<n>` ({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}"
--- 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
--- 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
--- a/tests/lean/run/10564.lean
+++ 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