Examples of metavariables pretty printing without names?

Stream: lean4

[Kyle Miller]

I'm wondering if anyone's recently run into the issue of a metavariable like ?a pretty printing later as ?m.123 x y z. If you know what I'm talking about and can make a mwe, that would be helpful!

I run into this occasionally, but I've been having a hard time reproducing it.

[Leni Aniva]

Does this mean the mvar somehow lost its user name?

[Leni Aniva]

I previously had a problem like this, where there are some goals produced by an apply. e.g. ?a ?b ?c. These are not synthetic opaque.

Later on another tactic comes in and say acts on ?a, then the solution of ?a affects ?b and assigns ?b := ?x. If ?b occurs in ?c it might show up as ?x instead.

I'm not sure if this is the behaviour you're referring to. I had to suppress it by setting the generated mvars to .syntheticOpaque.

[Leni Aniva]

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

[Aaron Liu]

like this?
image.png

[Kyle Miller]

I think that one is different @Leni Aniva.

The issue I'm talking about involves only synthetic opaque metavariables, and I believe it's from chains of them being created (via revert or others).

[Kyle Miller]

I believe that is also different @Aaron Liu, since the type of the ?_ isn't a synthetic opaque metavariable, so it gets reverted differently.

[Leni Aniva]

Could this be related to delay assigned mvars?

[Kyle Miller]

Yes, pretty printing delayed assignment metavariables is the motivation for my question.

[Leni Aniva]

you could probably create these mvars using intro and revert where the descendant mvar has a smaller or larger context than the parent

[Jovan Gerbscheid]

Speaking of pretty printing delay assigned metavariables, here's an example that came up yesterday:

theorem p_imp_p_true (p : Prop) : p → p ∧ True := by
  show_term -- Try this: refine fun h => ?_
    intro h
    constructor

Whereas you'd want this to say refine fun h => ⟨?_, ?_⟩

[Kyle Miller]

Yes, I have that noted (I was on that thread). I'm looking for something specific here, and that's a different issue.

[Jovan Gerbscheid]

Note that if I click on the ?_ in refine fun h => ?_, it expands to ?_ h : p ∧ True. So the ?_ magically became ?_ h

[Kyle Miller]

Yes, that's a feature I implemented so that you don't have to see the fvars in delayed assignments.

[Kyle Miller]

You can turn it off with pp.mvars.delayed true I think. (That means "pretty print the delayed assignment metavariable itself.")

[Aaron Liu]

Then, like this?
image.png

[Kyle Miller]

Ah, yes, that works.

Here's a minimized version of what I'm guessing the principle is:

import Lean

open Lean Elab Term

elab "postpone% " t:term : term => do
  tryPostpone
  elabTerm t none

example : True := by
  let f : Nat → Nat := fun x : Nat => postpone% ?a
  /- second goal:
  f : Nat → Nat := fun x ↦ ?m.439
  ⊢ True
  -/
  sorry
  sorry

[Kyle Miller]

I can't look into it right now, but I think ?m.439 is a synthetic opaque that's been assigned to be an application of a delayed assignment for ?a. The pretty printer isn't following this sort of chain.