Eliminating intermediate metavariables

Stream: lean4

[Eric Wieser]

What can I do to replace f_old with f_new here?

import Lean

open Lean Meta Elab Tactic

theorem foo : ∃ f : Nat → Nat, f 1 = 1 := by
  refine ⟨?f_old, ?hf⟩
  intro x
  revert x
  refine ?f_new
  /-- Goal state is

  case f_new
  ⊢ Nat → Nat

  case hf
  ⊢ (fun x ↦ ?f_old) 1 = 1
  -/

[Eric Wieser]

(Note that this is hard to debug in the web editor since it doesn't show case names)

[Aaron Liu]

I think ?f_old is delay-assigned, so you just have to solve the goal.

[Eric Wieser]

Can it be un-delayed?

[Aaron Liu]

no idea

[Eric Wieser]

I've filed lean4#7883 for a related issue

[Kyle Miller]

Aaron is correct that ?f_old is involved in a delayed assignment, but ?f_old is not delayed assigned itself. Also, it's worth being very careful here, since the initial ?f_old is different from the ?f_old in the end. Here's the sequence:

• refine creates the ?f_old : Nat -> Nat metavariable
• intro creates a new metavariable ?m with context x : Nat ⊢ Nat and a new metavariable ?m.37 : Nat -> Nat, then assigns ?f_old := fun x => ?m.37 x, then records the delayed assignment ?m.37 x := ?m, and then renames ?m to ?f_old.
• revert creates a metavariable ?m : Nat -> Nat, assigns ?f_old := ?m x, then renames ?m to ?f_old. (Note: I think there is a pretty printing oversight here: there are two metavariables named ?f_old now, since MetavarDecl contains the name, so they both print as ?f_old, but only the newest ?f_old is what can be referred to, since that's what's in the MetavarContext.userNames table. As such, you can see ?f_old in the hf goal, but it's not the f_old goal.)
• Then refine ?f_new renames the newest ?f_old to ?f_new.

In the end, after instantiating metavariables, this is what we have:

• an ?hf metavariable whose type is (fun x => ?m.37 x) 1 = 1
• the delayed assignment ?m.37 x := ?f_new x

Delayed assignments don't instantiate until their value contains no metavariables.

In this case, we could safely instantiate the delayed assignment since the metavariable it depends on (?f_new) has a local context that's a sublist of the ?m.37 context. (Indeed, the local contexts are the same.) If that's something that's fast to check for, maybe instantiateMVars could be changed to go ahead and instantiate.

We could also write a metaprogram to force that kind of delayed assignment to instantiate.

Something that's also possible is writing a metaprogram to "push" delayed assignments, at the cost of creating new delayed assignments for every metavariable in the expression. It might be worth having it as a tactic, at least for debugging purposes.