fix: remove superfluous Monad constraints from some spec lemmas (#10564)

Author: sgraf812

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,18 +472,25 @@ 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
     return vcs
   -- 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}"

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

src/Std/Do/Triple/SpecLemmas.lean

@@ -399,15 +399,15 @@ 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]
 theorem Spec.throw_StateT [WP m ps] [Monad m] [MonadExceptOf ε m] (Q : PostCond α (.arg σ ps)) :
   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))

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