exact?%

Stream: mathlib4

[Michael Stoll]

Just had this:

import Mathlib.Data.Nat.Factors

example (p n : ℕ) : p ∈ n.factors → p ≠ 0 := exact?%

produces lots and lots of Try this: fun a => ?_ a (and nothing else).

[Ruben Van de Velde]

Huh, that doesn't seem expected. Workaround:

example (p n : ℕ) : p ∈ n.factors → p ≠ 0 := fun h => exact?%

[Martin Dvořák]

What is exact?% supposed to do?

[Michael Stoll]

exact?% is like apply?, but in term mode.

[Scott Morrison]

#mwe?

[Michael Stoll]

Added a suitable import above.

[Scott Morrison]

Hmm, I'm baffled, some piece of state is being lost.

import Mathlib.Tactic.LibrarySearch

example (p : Nat) : Nat → p ≠ 0 := by apply?

is enough to demonstrate the problem. It prints

Try this: refine fun a ↦ ?_ a
Remaining subgoals:
⊢ Nat → p ≠ 0
⊢ ¬∃ x, p = x

Try this: refine fun a ↦ ?_ a
Remaining subgoals:
⊢ Nat → p ≠ 0
⊢ p = 0 → False

Try this: refine fun a ↦ ?_ a
Remaining subgoals:
⊢ Nat → p ≠ 0
⊢ 0 < p

...

and many more.

[Scott Morrison]

We can see from this that is really is finding solutions, but the instantiateMVarshere isn't seeing the assignment that was made by intros a few lines up.

[Scott Morrison]

We are doing something tricky here: on the previous line we've just used withMCtx, but there must be some other state that is being lost in the shuffle.

[Thomas Murrills]

This was a little tricky, because the mctx shuffling was actually a red herring! The issue is actually that the ?_ appearing in fun a => ?_ a has a delayed assignment to (a function which produces the) goal we've created by intros. You can recreate the issue in traces immediately after intros, before doing any librarySearch logic. (goal is properly assigned down in the withMCtx block.) The relevant info about delayed assignment starts here, I believe.

[Thomas Murrills]

What I'm not sure of is why this is actually an issue in this case and not others—I'm not personally familiar with when delayed assignments are actually meant to be substituted in, or what actually goes wrong in this case.

[Scott Morrison]

So how do we convince Lean that it doesn't need to be delayed further? I'm worried this this might have been lost in the state shuffling?

[Thomas Murrills]

Just a guess at this point, but I think it might be because there are pending goals involved, not because the state shuffling:

[Thomas Murrills]

  A delayed assignment for a metavariable `?m`. It represents an assignment of the form `?m := (fun fvars => (mkMVar mvarIdPending))`.
  `mvarIdPending` is a `syntheticOpaque` metavariable that has not been synthesized yet. The delayed assignment becomes a real one
  as soon as `mvarIdPending` has been fully synthesized.

[Thomas Murrills]

(I'm currently looking around for something like instantiateMVarsNoDelayed)

[Kyle Miller]

Delayed assignment metavariables variables are tricky -- they are not really metavariables themselves (they're never assigned), but the idea is that it's a "lambda" whose arguments are substituted into the fvars of the mvarIdPending. The only time you can really do this is once mvarIdPending itself is completely resolved (i.e., when its instantiateMVars comes up with a term with no mvars), since at that point you can locate all the relevant fvars and directly substitute the values.

As far as I've understood it, this is a fundamental concept and you cannot force the assignment by "abstracting away" the delayed assignment metavariable with a lambda. This mechanism is how metavariables from one metavariable context are sort of transferred into another one. (One source of these, by the way, is mkForallFVars and mkLambdaFVars -- done by the intro tactic for example. These functions turn out to be smart and know how to abstract metavariables, but to do so they need to introduce delayed assignment metavariables to "pass in" the abstracted variables.)

[Scott Morrison]

Maybe the right solution here is just to remove the intros calls from exact?, and require that the user does this first??

[Thomas Murrills]

What if instead of returning refine fun ... => b, apply? returned intros; refine b when necessary? This would avoid the delayed assignments in the body of the fun. (Is intros ever different from MVarId.intros? It looks the same to me :) )

[Scott Morrison]

We could, I guess.

[Scott Morrison]

I think it is better to decide that running intros was actually scope creep for exact?, and we should just not do it.

[Thomas Murrills]

Will exact? still be able to close goals of the form A → B when there's a theorem of type precisely A → B?

[Thomas Murrills]

Hmm, I guess it closed those with funs anyway in the first place...