Lower MVar Depth

Stream: lean4

[Marcus Rossel]

Is there some way to allow mvars created at depth $d + 1$ to be used at depth $d$? I'm creating mvars at depth $d + 1$, so they're the only ones assignable during isDefEq. But I would like to turn some of them into subgoals (as a result of calling a tactic) afterwards.

[Kyle Miller]

Could you say a bit more about why you want to only assign certain mvars?

(I'm not aware of any API for letting certain mvars "escape". I've run into situations too where I thought it would be useful.)

[Marcus Rossel]

My situation is the following. I'm writing a tactic which generates sequences of rewrites (based on given equation lemmas) for proving goals of the form lhs = rhs. When the goal contains mvars (e.g. as a result of applying Eq.trans), I do not want to assign those mvars, as that would mean deciding what the proof goal should be.

Unfortunately, if I do not increase mvar depth, I sometimes assign those mvars as follows. Let's say we want to prove x = y based on an equational lemma l : ∀ a b c, x = y. Then I first instantiate a, b and c in l with fresh mvars. Let's call the resulting equality l' : x' = y'. Next, I do isDefEq on x and x', as well as y and y'. Thus, the mvars in l' are assigned to match the values required by the proof goal. The problem now is that if the proof goal contains an mvar ?m, then the isDefEq step might assign one of the fresh mvars in l' to ?m. Thus, I currently increase the mvar depth before instantiating l with fresh mvars, which means that ?m will never be assigned by isDefEq. Until now, this setup works great.

The need for lowering mvar depth now arises when conditional rewrites come into play. Namely, if the equation lemma k has the type (h : p) → ∀ a b c, x = y, then I still instantiate k with fresh mvars to get k' : x' = y'. The isDefEq step then only assigns a, b and c, but h remains unassigned. So now I want to generate a new subgoal for h. But as the fresh mvar for h was created at the increased mvar depth, I can't use it to create the subgoal.

[Marcus Rossel]

Kyle Miller said:

I've run into situations too where I thought it would be useful.

Did you ultimately find that it wasn't really necessary though?

[Jovan Gerbscheid]

For lean4#4225, I think it would be useful to do the opposite: increase the depth of some metavariables when bumping up the depth.

[Eric Wieser]

"increase" meaning "allow assignment despite entering depth $d + 1$"?

[Jovan Gerbscheid]

Exactly, so choose which ones can be and which ones can't be instantiated

[Jovan Gerbscheid]

I suppose both of these things can be achieved by making a copy metavariable at the wanted depth, and assigning this to the old mvar.

[Kyle Miller]

@Marcus Rossel It might seem a bit wasteful, but you can split it into two phases, a query phase and an application phase. During the query, you increase the metavariable depth and do all the isDefEq queries you want. If the query succeeds, then you go ahead and use isDefEq again, but this time for unification purposes. This can be more flexible than trying it all at once.

Marcus Rossel said:

Did you ultimately find that it wasn't really necessary though?

I've usually found some sort of workaround, but the reason I asked was because if there are enough cases where people feel like they need to adjust depths of metavariables then this aspect of metaprogramming could get some more attention. There are some difficulties here though since you need to check that the metavariables at this higher depth are not assigned expressions involving high-depth metavariables — we don't want anything to escape.

[Marcus Rossel]

Jovan Gerbscheid said:

I suppose both of these things can be achieved by making a copy metavariable at the wanted depth, and assigning this to the old mvar.

How would you leave the context of higher depth, without deleting the mvars created at that depth? Naively I would want to do this:

import Lean
open Lean Meta Elab Term Command

elab "#test" : command => liftTermElabM do
  let bool ← elabTerm (← `(Bool)) none
  let m₀ ← mkFreshExprMVar bool (userName := `m₀)
  let m₁ ← withNewMCtxDepth do mkFreshExprMVar bool (userName := `m₁)
  unless ← isDefEq m₀ m₁ do failure

#test -- unknown metavariable '?_uniq.1664'

But that deletes mvar m₁ when returning from withNewMCtxDepth. It would be nice to have something like withNewMCtxDepthKeeping where you also return which mvars you want to keep:

-- based on `withNewMCtxDepthImp`
def withNewMCtxDepthKeeping (allowLevelAssignments := false) (x : MetaM (Array MVarId × α)) : MetaM α := do
  let saved ← get
  modify fun s => { s with mctx := s.mctx.incDepth allowLevelAssignments, postponed := {} }
  let mut keep := #[]
  try
    let (k, a) ← x
    keep := k
    return a
  finally
    -- TODO: Restore everything, but also keep the `keep` mvars.
    modify fun s => { s with mctx := saved.mctx, postponed := saved.postponed }

[Jovan Gerbscheid]

I see, in that case what I suggested probably won't work, since withNewMCtxDepth resets the metavariable context to what it was before.

[Jovan Gerbscheid]

A different solution could be to use Lean.Meta.abstractMVars, to abstract the metavariables out of the expression. Then in the lower depth, you can use Lean.Meta.openAbstractMVarsResult

[Marcus Rossel]

Jovan Gerbscheid said:

A different solution could be to use Lean.Meta.abstractMVars, to abstract the metavariables out of the expression. Then in the lower depth, you can use Lean.Meta.openAbstractMVarsResult

Oh of course :see_no_evil: The doc comment also suggests that this is the intended way of doing things:

This API can be used to "transport" to a different metavariable context.