Synthetic metavariables in exact

Stream: lean4

[Gabriel Ebner]

I know that in Lean 4, the idea is to use synthetic metavariables so that you can select them by name using case in structured proofs. And that exact should not produce any new unnamed goals. However it seems that many tactics fail if the goal contains named/synthetic metavariables:

example : ∃ n : Nat, n = n := by
  refine ⟨?n, ?h⟩
  case h => rfl -- don't know how to synthesize implicit argument
  case n => exact 3

(I would expect that rfl succeeds here since it doesn't produce any new goals. This example is of course a bit constructed, but I hope it is plausible that you sometimes want to fill in complicated witnesses using unification.)

Using refine instead of rfl succeeds, but the result is surprising:

example : ∃ n : Nat, n = n := by
  refine ⟨?n, ?h⟩
  case h =>
    refine rfl -- moves ?n *inside* the ?h goal!?
    case n => exact 3

(I would expect that the case h goal is finished after rfl, and that case n works on the same indentation.)

The issue also appears if you use nested tactics:

example : ∃ n : Nat, n = n := by
  refine ⟨?n, by rfl⟩ -- don't know how to synthesize implicit argument
  case n => exact 3

(I would expect that the rfl succeeds since it does not produce any new goals.)

[Mac]

Gabriel Ebner said:

Using refine instead of rfl succeeds, but the result is surprising:

example : ∃ n : Nat, n = n := by
  refine ⟨?n, ?h⟩
  case h =>
    refine rfl -- moves ?n *inside* the ?h goal!?
    case n => exact 3

(I would expect that the case h goal is finished after rfl, and that case n works on the same indentation.)

If I'm not mistaken, the reason refine rfl succeeds is because it can produce new unnamed goals and is doing so here. It just so happens that the goal it produces is the same as ?n so it unifies it with that and thus they both get folded into the current proof. Since exact rfl cannot introduce said unnamed goal, it fails.

[Sebastian Ullrich]

I think the issue is that refine and exact work on all mvars of the term, while Gabriel would expect them to regard only newly introduced mvars

[Gabriel Ebner]

Yes, I would expect the check for unassigned metavariables (that exact, rfl, etc. use) to ignore already existing metavariables.

[Sebastian Ullrich]

Interestingly the existing mvars are actually nonassignable during elaboration of the nested term. That would make it simple to distinguish them, except I don't think it is intended that e.g.

example : ∃ n : Nat, n = n := by
  refine ⟨?n, ?h⟩
  exact Eq.refl 3

doesn't work.

[Gabriel Ebner]

You're missing a case h => before the exact, but you're right, I would like the ?n to be assignable.

[Sebastian Ullrich]

Feel free to open issues I'd say :)

[Mario Carneiro]

There are some issues I have found with lean 3 proofs using things like have := bla _; rwa [lem] at this where the first have leaves a lot of metavariables that are unified by the rw and assumption, that may be related to this issue

[Mario Carneiro]

lean 4 likes to give errors up front for that kind of proof

[Sebastien Gouezel]

I think I like the lean 4 behavior on this: this kind of obfuscation is maybe good for writing quick proofs, but it doesn't fare too well on readability.

[Mario Carneiro]

I'm okay with using ?_ for explicitness here, but it should still be possible to write those proofs

[Mario Carneiro]

If we say that some variety of proof just isn't okay anymore this will kill the port, because restructuring a big proof in an area you don't know too well is a huge undertaking

[Mario Carneiro]

In particular have statements that have metavariables in them, sometimes hidden in implicit args, that appear briefly and are unified in the next line happen all the time in mathlib

[Mario Carneiro]

Currently the default is to use _ instead of ?_ for implicit args, so this will usually stop a lean 4 proof in its tracks

[Mario Carneiro]

What about allowing these goals to arise but giving them inaccessible case names? (Is that even a thing?)