user-facing metavariable names shared between goals

Stream: lean4

[Floris van Doorn]

Is this error expected? I was surprised that the metavariable name ?h refers to the same metavariable in different subgoals.

example {p q r s : Prop} (h1 : p → q) (h2 : r → s)
    (hp : p) (hr : r) : q ∧ s := by
  constructor
  · refine h1 ?h
    exact hp
  · refine h2 ?h -- error, since `?h` has type `p`.
    exact hr

(note: I generally don't type ?h myself, but ?_. In this case I used apply? in two separate subgoals, and the suggestions of apply? are of the form refine ... ?h)

[Mario Carneiro]

Oh, I was just thinking about opening an RFC about this. Yes, this is a known issue and it is surprising to me that it isn't a higher concern given that we use short goal names all the time

[Mario Carneiro]

The thing is, the tactic state doesn't really have "scoping" in the sense that you are thinking about

[Mario Carneiro]

It's even worse than this: apply and other tactics automatically name their goals, and if you use that name in your ?foo metavariables then you will pick up old assignments

[Mario Carneiro]

example (f : (x y : Nat) → True) : True ∧ True := by
  constructor
  next =>
    apply f
    · exact 0
    · exact 1
  next =>
    let z := ?x + ?y
    -- z := 0 + 1
    exact f 0 z

[Floris van Doorn]

I think this is not a higher concern because we rarely name goals ourselves, and all automatically-named goals generate a fresh name (I think?)

[Mario Carneiro]

No, they are not fresh names, that's the issue

[Mario Carneiro]

they are completely outside the hygiene system

[Mario Carneiro]

unless you write ?a or case a => inside a macro but that's not a very common situation

[Floris van Doorn]

I see. What I meant is that apply will at least not re-use existing metavariables with the same user-facing name.

[Mario Carneiro]

But when you use the metaprogramming API to create a new named mvar, it will not be unified with other mvars with the same user name, it will just "shadow" the original

[Mario Carneiro]

No, it will

[Mario Carneiro]

Er, it can make multiple goals with the same name but the metaprogramming API doesn't try to be smart about this and unify them, unlike the ?a syntax

[Floris van Doorn]

I mean, in this example, the second apply f will generate 2 new subgoals, not reuse the existing ?x and ?y.

example (f : (x y : Nat) → True) : True ∧ True := by
  constructor
  next =>
    apply f
    · exact 0
    · exact 1
  next =>
    apply f
    · exact 2
    · exact 3

[Floris van Doorn]

Oh juicy, I just got a stack overflow

example (f : (x y : Nat) → True) : True ∧ True := by
  constructor
  next =>
    apply f
    · exact ?x

[Mario Carneiro]

yep, that one is fun

[Thomas Murrills]

The exposed mvar names issue was brought up in this thread, which suggests a combinator for hiding goals created during execution of some monad computation

[Mario Carneiro]

this has to do with the fact that lean doesn't really do the occurs check as often as it should

[Mario Carneiro]

Maybe we should just have another syntax like ?=a for reusing an existing metavariable, this is almost impossible to use correctly from a user perspective as currently designed

[Mario Carneiro]

(and I can count on one hand the number of times I actually wanted to reuse a metavariable with named mvar syntax)

[Floris van Doorn]

Fair, although I can personally also count on one hand the number of times I actually gave a metavariable a name manually.

[Mario Carneiro]

True. But that road leads to "?a considered harmful"

[Mario Carneiro]

We could certainly have apply? et al explicitly use ?_ instead of named mvars

[Kyle Miller]

@Floris van Doorn Here's the issue for your last example: bug: exact tactic is missing an occurs check

[Mario Carneiro]

I think you could trace that apply? behavior back to the show_term tactic, which tries to replicate the behavior of the tactic it replaces, including the names of generated goals

[Mario Carneiro]

Although I suppose it won't get the order right regardless

[Floris van Doorn]

Oh, we also have a new version of the "a"-bug :grinning: (although in this case a actually occurs in the definition of And)

example : True ∧ True  := by
  constructor
  · refine ?a -- error