Output of exact? gives metavariables error

Stream: mathlib4

[Bhavik Mehta]

Here is the example:

import Mathlib.Data.Nat.SuccPred

example {t : Nat → Prop} {m : Nat} (hex : ∀ ⦃a : Nat⦄, t a → a ≤ m) (s : Nat) :
    t s → s < m + 1 := by
  exact?

The output of exact?, when pasted in, gives

typeclass instance problem is stuck, it is often due to metavariables
  NoMaxOrder (?m.1825 a)

What's going on here? What's making exact? produce this weird looking proof term:

exact fun a ↦
    (fun {α} {x y} [LinearOrder α] [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α] ↦
        Order.lt_add_one_iff.mpr)
      (hex a)

[Kevin Buzzard]

Always do as much intro as you can before exact :-) (not that this is an answer, it's just a workaround/rule of think l thumb). Presumably the answer is that without the intro of the typeclass instances, lean can't find them. But if you intro them, they'll be in the local context so things should work.

[Bhavik Mehta]

Indeed doing intro first is what I told the student who came across this! But note that before the intro, the typeclass instances are already present! The intro is only a single implication, no instances or types.

[Bhavik Mehta]

More generally, I'm curious why the proof term makes it look like Lean wants to intro a bunch of typeclass assumptions!

[Kyle Miller]

Try doing set_option pp.funBinderTypes true first. (Likely won't solve the problem, but it'll make the term slightly better.)

[Kyle Miller]

There's a deeper issue that x and y are implicit, so their values aren't being printed.

[Bhavik Mehta]

Indeed that changes it to

  exact fun (a : t s) ↦
    (fun {α : Type} {x y : α} [LinearOrder α] [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α] ↦
        Order.lt_add_one_iff.mpr)
      (hex a)

instead

[Bhavik Mehta]

For the sake of comparison, an answer I would have expected here is

  exact fun h ↦ Order.lt_add_one_iff.mpr (hex h)

[Bhavik Mehta]

Should I make an issue for this? I can't seem to minimise further, but this seems like a pretty strange exact? output to me

[Kyle Miller]

Sure, makes sense to make an issue.

Given what I know about how exact? works I'm not surprised the result looks like this, and it could take some work to address.

[Bhavik Mehta]

Can you suggest why the result looks like this? In other cases I've seen exact? work fine when there's an implication to prove, so I'd like to know what's going on in this case that makes it behave weirdly

[Kyle Miller]

Part of the issue is that the binderinfos aren't being set to explicit when they enter the local context. This causes the pretty printer to not print all of these implicit arguments, which are necessary here.

[Kyle Miller]

I don't know SolveByElim well enough though to know the exact details

[Kyle Miller]

Potentially this could be an artifact of how apply works. (Nevermind, can't reproduce it with apply.)

[Bhavik Mehta]

Does this also explain why α is getting reverted?

[Bhavik Mehta]

Here's another example of the same form (by the same student), where doing more intro first doesn't help

import Mathlib.Algebra.Group.Basic

lemma asdf {G : Type} [Group G] {x : G} :
    1 = x * 1 * x⁻¹ := by
  exact?

The output of exact? here is

Try this: exact Eq.symm ((fun {G} [Group G] {a b} => conj_eq_one_iff.mpr) rfl)

which also doesn't work.

[Bhavik Mehta]

(I did tell them to use rw? instead, but the failure of exact? still seems weird!)

[Edward van de Meent]

removing the fun {...} [...] {...}=> seems to fix it

[Edward van de Meent]

i.e. yes, exact? produces weird output, but it's not complete nonsense

[Edward van de Meent]

and it's an easy fix

[Ruben Van de Velde]

I think the "weird output" was the bug report, yeah

[Edward van de Meent]

i don't think "weird output" was the issue tho? the issue is output which doesn't work

[Bhavik Mehta]

Right, the issue is that the output doesn't work, which is really annoying for a self-replacing tactic, and frustrating to beginners.

[Ruben Van de Velde]

Sure, but the example in the OP is fixable in the exact same way you propose here

[Bhavik Mehta]

I perhaps should have clarified that a self-replacing code action replacing itself with an error is undesirable behaviour to me.

[Bhavik Mehta]

Edward van de Meent said:

and it's an easy fix

It's an easy fix to you and to me, but not to people new to Lean!

[Edward van de Meent]

right... so, reformulating the issue, exact? produces a term which explicitly writes a function with only implicit arguments, leading to a metavariable error...

[Edward van de Meent]

that doesn't sound like a hugely difficult issue

[Bhavik Mehta]

Edward van de Meent said:

that doesn't sound like a hugely difficult issue

It doesn't sound like that to me either, but I trust Kyle's judgement above :)

[Bhavik Mehta]

I removed the mathlib dependence and reported as lean4#6975