Collect mvars during a tactic

Stream: lean4

[Leni Aniva]

Sometimes when you invoke MVarId.revert (the low-level MetaM version), additional mvars can be generated.

Is there a function that can collect the generated mvars from this tactic? The simplest way I can think of is to record the mvar counter and used filterOldMVars to filter all mvars in the current MetaM context.

This function would take place of the ?? in

def invokeRevertAndCollect (mvarId: MVarId) (fvarId: FVarId): MetaM (List MVarId) := do
  let (nextGoal, moreMVars) := ?? do
    let (_, nextGoal) := mvarId.revert #[fvarId]
    pure nextGoal
  return [nextGoal] ++ moreMVars

[Kyle Miller]

Do you have an example where you need to collect these mvars? If it's generating mvars, they should be delayed assigned, so they are not your responsibility.

[Leni Aniva]

Kyle Miller said:

Do you have an example where you need to collect these mvars? If it's generating mvars, they should be delayed assigned, so they are not your responsibility.

There are some cases when the generated mvars are not delayed assigned. Consider this example:

| n : Nat
?snd : Eq ?alpha ?lhs ?rhs
| n : Nat
?alpha : Sort u
| n : Nat
?lhs : ?alpha
| n : Nat
?rhs : ?alpha

Now suppose you execute .revert #[fvarId] where fvarId is the id of this n, on ?snd, you get

?snd : forall (n: Nat), Eq ?alpha' ?lhs' ?rhs'

(the actual generated mvar names are not as clean as this. I annotated this for clarity)

In this case instead of having ?lhs' being delayed assigned with some expr dependent on ?lhs, we get

| n : Nat
?lhs := ?lhs' n

This is a pretty peculiar case, but if it occurs I don't even have a way of detecting that it happened, hence the question

[Kyle Miller]

I see. I was noticing this issue recently, and it can pop up whenever you have natural metavariables, and there are lots of tactics that seem to accidentally create natural metavariables for new goals.

Can you make sure these metavariables are synthetic opaque instead?

[Leni Aniva]

Kyle Miller said:

I see. I was noticing this issue recently, and it can pop up whenever you have natural metavariables, and there are lots of tactics that seem to accidentally create natural metavariables for new goals.

Can you make sure these metavariables are synthetic opaque instead?

do you mean the automatically generated ones?

I have no control over the mvars ?alpha, ?lhs, ?rhs because they could be generated from other tactics.

As long as I can detect when this problem occurs, I can deal with it. My only question is about detecting this problem and collecting the resulting mvars.

[Kyle Miller]

If revert causes goals to disappear, this is a bug. Please report these bugs. Can you give mwe's of this phenomenon?

A workaround you could try is to change all the goal metavariables to be synthetic opaque yourself with docs#Lean.MetavarContext.setMVarKind before doing revert. I think this should work.

[Leni Aniva]

Kyle Miller said:

If revert causes goals to disappear, this is a bug. Please report these bugs. Can you give mwe's of this phenomenon?

A workaround you could try is to change all the goal metavariables to be synthetic opaque yourself with docs#Lean.MetavarContext.setMVarKind before doing revert. I think this should work.

it doesn't cause goals to disappear. I'm operating on the MetaM level where there's no concept of goals like TacticM. I just need to capture the generated mvars from a revert

[Kyle Miller]

I am pretty sure that revert should not be assigning metavariables like this. You shouldn't need to capture generated mvars.

[Leni Aniva]

Kyle Miller said:

I am pretty sure that revert should not be assigning metavariables like this. You shouldn't need to capture generated mvars.

so it should just fail in this case? even if the assigned mvars are .natural?

[Kyle Miller]

Another workaround you could try is to use withNewMCtxDepth to prevent pre-existing mvars to be assigned.

[Kyle Miller]

so it should just fail in this case?

No. My understanding of this issue is that the assignment is happening in the wrong direction. It would be very helpful having some mwes to properly report it.

[Leni Aniva]

Kyle Miller said:

so it should just fail in this case?

No. My understanding of this issue is that the assignment is happening in the wrong direction. It would be very helpful having some mwes to properly report it.

I can try producing one.

[Leni Aniva]

Its done:

import Lean
open Lean

def showMVar (name: String) (mvarId: MVarId): MetaM Unit := do
  if let .some expr ← getExprMVarAssignment? mvarId then
    IO.println s!"{name} := {← Meta.ppExpr expr}"
  else if let .some a ← getDelayedMVarAssignment? mvarId then
    IO.println s!"{name} ::= {a.mvarIdPending.name}"
  else
    IO.println s!"{name} is not assigned"

def metaM: MetaM Unit := do
  let α: Expr := .sort 0
  let nat: Expr := .const `Nat []
  Meta.withLocalDecl `x .default nat $ λ fvar => do
    let lhs: Expr ← Meta.mkFreshExprMVar (type? := .some α)
    let rhs ← Meta.mkFreshExprSyntheticOpaqueMVar α
    let goalType ← Meta.mkEq lhs rhs
    let goal ← Meta.mkFreshExprSyntheticOpaqueMVar goalType
    IO.println s!"goal: {← Meta.ppExpr $ ← goal.mvarId!.getType}"
    let (_, goal2) ← goal.mvarId!.revert #[fvar.fvarId!]
    IO.println s!"goal2 : {← Meta.ppExpr $ ← goal2.getType}"
    let .forallE _ _ body _ ← goal2.getType | panic! "This must be a ∀"
    let .some (_, .app lhs' (.bvar _), .app rhs' (.bvar _)) := body.eq? | panic! "Wrong type"
    showMVar "lhs" lhs.mvarId!
    showMVar "rhs" rhs.mvarId!
    showMVar "lhs'" lhs'.mvarId!
    showMVar "rhs'" rhs'.mvarId!

def main : IO Unit := do
  let env: Environment ← importModules
    (imports := #[`Init])
    (opts := {})
    (trustLevel := 1)
  let options: Options := {}
  let options := options.setBool `pp.all true
  let coreM := Meta.MetaM.run' metaM
  let coreContext: Lean.Core.Context := {
    options,
    currNamespace := `Example
    openDecls := [],     -- No 'open' directives needed
    fileName := "<stdin>",
    fileMap := { source := "", positions := #[0] }
  }
  match ← (coreM.run' coreContext { env }).toBaseIO with
  | .error exception =>
    IO.println s!"{← exception.toMessageData.toString}"
  | .ok _ => return ()

RHS is set to .syntheticOpaque so it wasn't modified by revert (edit: However the generated mvar in goal2 corresponding to rhs was modified). Should I file a bug in Lean4 repo?

In summary:

• lhs: Assigned to lhs? x
• rhs: Not assigned
• lhs': Not assigned
• rhs': Delayed assigned to rhs with fvar. (IMO correct behaviour)

[Leni Aniva]

Moreover, if you run the tactic with withNewMCtxDepth, you get

goal: @Eq.{1} Prop ?m.2 ?m.3
unknown metavariable '?_uniq.7'

The unknown mvar occurs at ← goal2.getType.

[Leni Aniva]

https://github.com/leanprover/lean4/issues/5279

[Leni Aniva]

I came up with a way to fix it. If we can have a function

def withOpaqueOldMVars (mvarCount: Nat) (m: MetaM a): MetaM a := ...

which overrides the kind of mvars older than mvarCount to be .syntheticOpaque. Then we can call it before MetavarContext.revert to prevent the elimination function from assigning to these mvars.

If people are fine with this solution, I'll open a PR. It requires adding a new field to Meta.Context and modifications to elim

[Kevin Buzzard]

I love it when people in this community persevere to understand a problem. Thanks a lot for minimising and thinking about a fix! I'm well aware that it's time-consuming.

[Leni Aniva]

Kevin Buzzard said:

I love it when people in this community persevere to understand a problem. Thanks a lot for minimising and thinking about a fix! I'm well aware that it's time-consuming.

My main research project is blocked on this bug I may as well fix it asap

[Yann Herklotz]

I just wanted to note that this looks similar to a previous discussion on MVar assignments, we've been working around this with an MVar collection tactic and being careful about where MVars are assingned.

[Kyle Miller]

Thanks @Yann Herklotz, I was trying to remember that thread. I've linked to it on the issue (lean4#5279).

[Leni Aniva]

Yann Herklotz said:

I just wanted to note that this looks similar to a previous discussion on MVar assignments, we've been working around this with an MVar collection tactic and being careful about where MVars are assingned.

I came up with a workaround which is to intercept all MVars during Tactic.setGoals and force them to be .syntheticOpaque. It seems to be working for now, but if a tactic runs things with withAssignableSyntheticOpaque we could potentially lose track of the goals

[Leni Aniva]

There's a problem with this workaround. I sometimes rely on the fact that apply can unify metavariables. For example, I can apply le_of_eq to 2 <= ?m and this will induce ?m := 2. With all mvars set to .syntheticOpaque, this is no longer possible. I think having this sort of unification is fine as long as no goals are lost

[Kyle Miller]

Yann suggested in the other thread that apply might need to be doing its unifications using withSyntheticOpaque — this might be justified.

[Leni Aniva]

Kyle Miller said:

Yann suggested in the other thread that apply might need to be doing its unifications using withSyntheticOpaque — this might be justified.

do you mean withAssignableSyntheticOpaque?

[Yann Herklotz]

Yeah I think so, as far as I understand, one should use synthetic MVars when creating MVars that one wants to keep around, and that tactics that want to unify those MVars should use withAssignableSyntheticOpaque to explicitly assign them.

[Thomas Murrills]

Leni Aniva said:

Moreover, if you run the tactic with withNewMCtxDepth, you get

goal: @Eq.{1} Prop ?m.2 ?m.3

unknown metavariable '?_uniq.7'

The unknown mvar occurs at ← goal2.getType.

Relatedly, I’d love if there were a version of withNewMCtxDepth that didn’t revert the entire mctx at the end, but instead raised the depth of the newly-created mvars inside back up to the depth outside. That would prevent unknown mvar errors like these and imo provide more intuitive behavior (intuitively, I wouldn’t expect that increasing the depth would affect anything besides assignability). 

I’ve run into this situation a few times, and collecting/returning the necessary information from within withNewMCtxDepth in a stateless fashion can be frustrating. (I would be in favor of withNewMCtxDepth itself changing if it didn’t break anything!)

It’s not hard to write a combinator which manages the depths like this yourself, but it does feel “risky”! :) (And a little inefficient.)

(Note: an alternative, cheaper implementation that I think achieves the same effect (but might require a core change) is to not actually change the depth of any mvars upon closing out withNewMCtxDepth', but to simply say that any mvars with the current mctx depth or greater are assignable. However, to ensure that you can always create a fresh depth easily when entering subsequent (non-nested) withNewMCtxDepth's (i.e. to avoid re-entering a previously-used depth), we could maintain the maximum encountered mctx depth in the MetaM state, and increase the depth based on that.)