MVar disappearing from list of goals after a `subst`

Stream: lean4

[Yann Herklotz]

Hi, I had a question about the expected behaviour of metavariables in Lean, as there are situations when MVars can get assigned with new MVars, where the new MVars are not added to the goal, making them disappear from the list of goals. This leads to us losing track of MVars, and results in:

(kernel) declaration has metavariables '_example'

because there are unassigned MVars in the proof term. Is this something others have encountered? In Coq there is a "shelf", and evars have to be unshelved at the end of the proof if they remained unassigned. I'll post a detailed example below.

[Yann Herklotz]

In the example below we create a small tactic called createMVar, which doesn't do anything useful but just shows the problem. We have other tactics that do useful things with the MVar that exhibit the same problem. The tactic creates a natural or syntheticOpaque MVar in the context, as part of the type of an equality hypothesis, where the proof is rfl.

h : ?m = 0 (:= rfl)

It then returns the modified goal MVar with the updated context, as well as a new goal for ?m.

import Lean

open Lean Meta Elab Tactic

syntax naturalOrSynthetic := "natural" <|> "synthetic"

elab "createMVar" i:naturalOrSynthetic : tactic => withMainContext do
  let mvarKind ←
    match i with | `(naturalOrSynthetic| natural) => pure MetavarKind.natural
                 | `(naturalOrSynthetic| synthetic) => pure MetavarKind.syntheticOpaque
                 | _ => unreachable!
  let l ← mkFreshExprMVar (some (mkConst ``Nat)) (kind := mvarKind)
  let app ← mkAppOptM ``Eq #[mkConst ``Nat, l, mkConst ``Nat.zero]
  let proof ← mkAppM ``Eq.refl #[mkConst ``Nat.zero]
  liftMetaTactic λ mvarId => do
    let newMVar ← mvarId.assert `HR app proof
    let (_, newMVar) ← newMVar.intro1P
    return [newMVar, l.mvarId!]

example (s : Nat) (h : s = 0) : True := by
  -- Create a natural MVar in an hypothesis and add it as a goal
  createMVar natural
  -- Substitution assigns the MVar with a new MVar, making the goal disappear
  subst s
  -- Solve the only remaining goal
  constructor
-- (kernel) declaration has metavariables '_example'

Creating a natural MVar, which is the behaviour we want because eventually we would like to unify the MVar through isDefEq results in the MVar goal disappearing. This means that if we happen to not unify the MVar naturally, there won't be any references left that we could use to assign it explicitly.

Using a syntheticOpaque MVar exhibits the behaviour we are looking for, where the goal is still left open after the substitution, and we can fill it using exact 0.

example (s : Nat) (h : s = 0) : True := by
  createMVar synthetic
  subst s
  construction
  exact 0

Digging down further, the real issue seems to be in the revert function. It assigns any natural MVar that is encountered, which makes sense for the main goal, but for other MVar it will assign them but won't return the new MVar reference.

The code below shows that revert will remove the second goal associated with the MVar.

example (s : Nat) (h : s = 0) : True := by
  createMVar natural
  run_tac withMainContext do
    let s ← getFVarId (mkIdent `s)
    liftMetaTactic λ mvarId => do
      let (_, mvarId) ← mvarId.revert #[s] true
      return [mvarId]
  intros; constructor

revert seems to eventually call elimMVar on the main goal, but eventually also applies elimMVar on the MVar we introduced (through elimApp), resulting in an assignment of the MVar. It is therefore removed from the list of goals, but it is never substituted by a new goal for the newly introduced MVar.

The main questions I had were the following:

• Is it expected that all MVar should have an associated goal (if these are not assigned or used within a tactic internally)? In this case, it would seem like the interface of the revert function is not expressive enough, and it might have to return a list of new goals instead of just the main new MVar.

• Otherwise, is there a Shelf, similar to Coq? Coq doesn't try and keep track of all the MVar as goals, instead they are saved and at the end of the proof the MVar that are present in the proof but are not assigned can be Unshelved and assigned explicitly.

• We are thinking of implementing a tactic which will check the proof term and "unshelve" all the unassigned MVar that are left in the proof term. This would essentially be a wrapper around by, which then produces new goals for all the MVar that were unassigned in the proof.

Finally, we may also be misusing MVar, and currently we have a few cases where we actually don't care about the exact value of the MVar. Instead, we partially assign them until we find a contradiction. But this fails because they remain unassigned even though there are no goals to assign them anymore (because subst eliminates them). However, we also think that we have found cases where MVar introduced by apply disappear and lead to the same issue.

[Mario Carneiro]

that situation is considered a bug in the tactic that lost track of the goals

[Yann Herklotz]

Yeah that makes sense, I posted the detailed example, and subst, or more precisely revert assigns the MVar with a new MVar without adding it to the goal.

[Mario Carneiro]

in your example, I think createMVar is also misbehaving, because proof does not have the same type as app, which I'm guessing MVarId.assert assumes

[Mario Carneiro]

you need to unify app with the type of proof and this process will end up solving the metavariable l you have created

[Yann Herklotz]

Hmm, I was just trying to write a tactic which leaves unassigned MVars in the context. I think that this proof should still type-check at the end if we ever assign the MVar.

[Yann Herklotz]

Of course if we assign it correctly, so it should always be assigned to 0, otherwise we get a panic during the final term type checking.

[Mario Carneiro]

you could create a metavariable for proof instead of using Eq.refl

[Mario Carneiro]

Yann Herklotz said:

Of course if we assign it correctly, so it should always be assigned to 0, otherwise we get a panic during the final term type checking.

Well there is nothing that is keeping track of this fact, that it should not be assigned to anything other than 0, which is why this is considered an invariant violation

[Yann Herklotz]

But this doesn't lead to inconsistencies right? If you ever use the hypothesis the MVar will be unified, and the expression will be present in the term, and it will be type checked, at which point the user has to ensure that they unified correctly (otherwise it results in a panic which makes sense). I'm trying to see if adding it as the proof goal leads to the same issue though.

[Mario Carneiro]

Here's a version that creates another metavariable for proof

import Lean

open Lean Meta Elab Tactic

syntax naturalOrSynthetic := "natural" <|> "synthetic"

elab "createMVar" i:naturalOrSynthetic : tactic => withMainContext do
  let mvarKind ←
    match i with | `(naturalOrSynthetic| natural) => pure MetavarKind.natural
                 | `(naturalOrSynthetic| synthetic) => pure MetavarKind.syntheticOpaque
                 | _ => unreachable!
  let l ← mkFreshExprMVar (some (mkConst ``Nat)) (kind := mvarKind)
  let app ← mkAppOptM ``Eq #[mkConst ``Nat, l, mkConst ``Nat.zero]
  let proof ← mkFreshExprMVar app
  liftMetaTactic λ mvarId => do
    let newMVar ← mvarId.assert `HR app proof
    let (_, newMVar) ← newMVar.intro1P
    return [newMVar, l.mvarId!, proof.mvarId!]

example (s : Nat) (h : s = 0) (x : False) : True := by
  -- Create a natural MVar in an hypothesis and add it as a goal
  createMVar natural
  -- Substitution assigns the MVar with a new MVar, making the goal disappear
  · subst s
    cases x
  · cases x

[Mario Carneiro]

Yann Herklotz said:

and it will be type checked

Terms are not eagerly typechecked multiple times during elaboration for performance reasons. So each tactic and elaborator is responsible for contributing only well-typed-ly to the goal

[Mario Carneiro]

if a tactic fails to uphold its part of the bargain, the kernel will catch the typing error and this is a tactic bug

[Yann Herklotz]

Interesting, would you expect the goal associated with the MVar in the context to disappear? It will be assigned when providing the proof to the hypothesis I guess.

[Mario Carneiro]

I think some of the guidance around this is mixed, but I think the prevailing opinion is that dependent mvars should be goals, because otherwise you can contrive situations where they are not solved, as in my example here where I used cases x to avoid solving the mvar in the goal en passant

[Mario Carneiro]

meaning that this behavior is a bug in subst

[Mario Carneiro]

although I guess tactics will not normally use natural mvars in this situation

[Mario Carneiro]

and subst does not have the same behavior on synthetic mvars

[Yann Herklotz]

Ah I didn't see the x, OK that makes sense. Do the questions I added at the end make sense as possible solutions? I would guess that revert needs to be a bit more expressive and return a list of fresh MVars that it introduced.

We use natural mvars so that we can already unify them in the main goal if we can, instead of having to explicitly assign them. This seems to be similar to the behaviour of apply right?

[Yann Herklotz]

And I think we found similar behaviour in apply, but haven't quite reduced it yet. We have to be very careful about using apply explicitly with the right number of _, otherwise it leads to mvars also disappearing that were introduced by apply.

[Yann Herklotz]

But it's true, subst behaves correctly on synthetic mvars.

[Mario Carneiro]

there is a tactic along the lines of your last bullet, called recover, but it's basically only for debugging purposes

[Yann Herklotz]

Ah interesting thank you, I'll have a look at that, but yes it doesn't seem like the best solution. We essentially just have some cases in our proof where we can prove a contradiction without assigning some mvars, and currently they completely disappear, leading to a kernel panic. And I'm not sure how our tactic can keep track of them other than adding them to the goal, which doesn't seem to work when they are natural and we use subst or revert.

[Mario Carneiro]

why not make them synthetic?

[Yann Herklotz]

We would like tactics like apply in the main goal to be able to assign the mvars through unification. And I believe that some new mvars introduced by apply will also be natural.

[Yann Herklotz]

There are just some cases where we prove a contradiction without having to unify all mvars, in which case we don't actually care about their value. Maybe these mvars should never have been created in the first place, but they make finding the contradiction much easier.

[Yann Herklotz]

Is it a rule that goals should be synthetic mvars? Tactics like apply seem to manage not to do this though, because they create goals for mvars that can be assigned by unification.

[Kyle Miller]

The fact that apply isn't creating synthetic mvar goals might be an oversight. Tactics seem to be inconsistent about this.

The concept behind synthetic metavariables is that defeq inside of elaboration shouldn't be able to assign certain metavariables. Instead, all of these unifications can happen in a separate stage post-elaboration where synthetic metavariables become assignable, using the withAssignableSyntheticOpaque combinator. (Tactics seem to be inconsistent about using this combinator too.)

[Yann Herklotz]

Ah thanks, I was under the impression that having to use withAssignableSyntheticOpaque in our tactics was a bit of a hack, but it's interesting to know that it's deliberate and the reasoning behind it. That makes sense, and we'll try using synthetic mvars then.

Should apply be using withAssignableSyntheticOpaque as well? Because when one is using apply one often wants to force unification.