Hide intermediate goals from user?

Stream: metaprogramming / tactics

[Thomas Murrills]

Often a tactic involves creating some "intermediate" metavariable, which is both created and assigned over the course of the tactic. E.g., the tactic might involve something like this:

open Lean Meta Elab Tactic Term
elab "make_intermediate_goal" t:term : tactic => withMainContext do
  let a ← mkFreshExprMVar (← elabType t) .syntheticOpaque `a
  let b ← mkFreshExprMVar (← elabType t) .syntheticOpaque `b
  a.mvarId!.assign b
  appendGoals [b.mvarId!]

The mvar a gets created and assigned over the course of the tactic, and we shouldn't even know about it when calling the tactic.

Of course, if you have control over the names of the intermediate mvars, you can just give them inaccessible names in the first place. But sometimes names are created automatically, such as in forallMetaTelescope.

Consider the following example of this "in the wild", which can cause confusing behavior if you're naming a new metavariable during e.g. refine' after constructor, where the type has named parameters (in this case And (a b : Prop)):

def f (n : Nat) : True := True.intro

example : True ∧ True := by
  constructor
  · refine' f ?a -- application type mismatch
    -- f True / argument / True / has type / Prop : Type / but is expected to have type / Nat : Type

Here, the metavariable ?a got created for And and assigned to True during constructor, unbeknownst to the user, who would probably assume it was free to use.

---

I was wondering what the best way to deal with this is, in general. You can of course rename everything by hand, but that seems very low-level. Is there (or should there be) some kind of combinator that would render all metavariables created during a monadic computation inaccessible? Something roughly along the lines of

def withInaccessibleAssignedMVars (k : MetaM α) : MetaM α := do
  let mvarCounterSaved := (← getMCtx).mvarCounter
  let val ← k
  for (mvarId, decl) in (← getMCtx).decls do
    if decl.index >= mvarCounterSaved
        && !decl.userName.isInaccessibleUserName
        && (← mvarId.isAssigned)
    then
      mvarId.setUserName (decl.userName.appendAfter "✝")
  return val

(but with a more careful way of rendering usernames inaccessible).

Or maybe elaboration should as a matter of principle consider assigned mvars "dead" and should clean up the mctx on the fly (making the old mvar with that username inaccessible one way or another, and creating a new mvar with the same username).

This might be a bad idea, as then you couldn't refer to metavariables again once they were assigned without some special tool to do so—however, it would be one less responsibility to manage during metaprogramming (and there are already a few), and makes a kind of intuitive sense (assignment ~ replacement).

Or maybe there's already a standard way to deal with this issue. :)

[Thomas Murrills]

Also, here’s a slightly refined version of the code:

code

import Lean

open Lean

set_option autoImplicit true in
/-- Executes `k`, and makes all of the metavariables created during `k` inaccessible to the user by
acting on their username with `mkFreshUserName`.

By default, only assigned metavariables are made inaccessible.

The argument `shouldHide : MVarId → m Bool` can be specified to hide metavariable names using a
condition other than assignment status; when `← shouldHide mvarId` is `true`, `mvarId` will be
renamed with an inaccessible name. -/
def withoutCreatingAccessibleGoals [Monad m] [MonadLiftT CoreM m] [MonadMCtx m] (k : m α)
    (shouldHide : MVarId → m Bool := MVarId.isAssigned) : m α := do
  let initialMVarCounter := (← getMCtx).mvarCounter
  let val ← k
  for (mvarId, decl) in (← getMCtx).decls do
    if decl.index >= initialMVarCounter
        && !decl.userName.isInaccessibleUserName
        && (← shouldHide mvarId)
    then
      let newUserName ← mkFreshUserName decl.userName
      modifyMCtx fun mctx => mctx.setMVarUserName mvarId newUserName
  return val

[Thomas Murrills]

(Though, thinking about it now, we should also be able to hide goals on the basis of the value we obtain from the computation, so that we can e.g. return a list of goals that should not be user-facing.)