naming metavariables after the fact

Stream: metaprogramming / tactics

[Scott Morrison]

Sometimes it is convenient (or good pedagogy) to "leave a metavariable for later" in a proof.

However when we do this in Lean 3 this leaves ?m_i names in the proof state, which are highly confusing to people who haven't thought about metavariables, and unpleasant to read for anyone.

Is there a good way to give names to metavariables after the fact? Here's an example of what I would like:

example : Σ {α : Type}, ℕ → α :=
begin
  fsplit,
  /- The goals are:
  ```
  ⊢ Type

  ⊢ ℕ → ?m_1
  ```

  I would like them to be:
  ```
  ⊢ Type

  α : Type := ?m_1
  ⊢ ℕ → α
  ```
  -/
  exact ℕ, exact id,
end

Lean 4 has a nice mechanism for naming metavariables at the time they are created (i.e. using ?α in place of _ in a refine statement), but I'm interested in Lean 3 solutions for now.

One solution is to replace the fsplit above with

  let α := _,
  refine ⟨α, _⟩,

and this gives me the desired goals.

However I am specifically interested in solutions that work after the fact. I'll post below a more involved example where the let α := _ trick doesn't work, as well.

[Johan Commelin]

I'd be interested in that more involved example!

[Scott Morrison]

Sorry, paused on the more involved example to ask my parallel question about to_expr. Essentially it's implicit there: when you use refine, you can't generate typeclass failures as new goals, while fsplit can. Thus the let trick, which requires refine, will fail if some of the other underscores are typeclasses depending on the named metavariable.

[Johan Commelin]

True. Note that refine @foobar.mk α (id _) (id _) (id _) quux xyzzy would work. But it is of course very ugly.

[Johan Commelin]

The main point being that (id _) will turn a typeclass argument into a new goal.

[Scott Morrison]

So is this some difference between elaborating with an expected type vs without? That when elaborating with an expected type, failed typeclasses searches are just failure. But if we insert (id _) the expect type can't propagate down that far, so the elaboration mode switches, and the typeclass searches instead result in new goals...

[Scott Morrison]

This makes me uncertain whether I should be thinking up some hacky refine' that inserts id in places, or hoping that it is possible or reasonable to change the behaviour of elaboration-with-expected-type so we still get the failed typeclass searches as goals.

[Johan Commelin]

I've never looked under the hood of tactic#apply_with but you can pass it a config option {instances := ff} that turns all typeclass arguments into new goals.

[Scott Morrison]

I don't think that argument for apply is relevant. It's the all in the difference between typeclass failures causing failure in to_expr with an expected type, vs causing new goals in to_expr without an expected type.

[Scott Morrison]

I don't understand why there would be that difference in behaviour.

[Scott Morrison]

And my limited attempts to find it in the C++ have not been very successful. :-)