bug in apply_fun

Stream: mathlib4

[Eric Wieser]

This:

import Mathlib.Tactic.ApplyFun
example {x y : ℕ} (h : x = y) : x = y :=
by
  apply_fun Equiv.refl ℕ using (Equiv.refl ℕ).injective

gives

application type mismatch
  Function.Injective (Equiv.refl ℕ)
argument
  Equiv.refl ℕ
has type
  ℕ ≃ ℕ : Type
but is expected to have type
  ?α → ?β : Sort (imax ?u.32 ?u.33)

It looks like a missing coeFn needs to be inserted somewhere

[Eric Wieser]

Though presumably it would be better to just ask lean to elaborate Injective f rather than build the expr manually

[Kyle Miller]

apply_fun ... at ... is able to do function coercions already; maybe something like what it's doing can be used for apply_fun ... using ...

[Kyle Miller]

@Eric Wieser mathlib4#3582

[Scott Morrison]

I left a comment. Happy to have a go at that refactor if you'd prefer.

[Eric Wieser]

Can we use syntax quotations to construct a q() application, and then evaluatw that Expr to get the real Expr?

[Eric Wieser]

I don't really understand why we could use `(quotes) to do everything automatically here in Lean 3, but somehow have to manually build and match all our expressions in Lean 4

[Kyle Miller]

I feel like it's easier to think through the consequences to each construction when they're done one at a time. You have to worry about metavariables that might be created at different times (perhaps due to coercions), when they're solved for, and who's responsible for collecting them to add to the list of goals. (Aside: I think many (most?) uses of docs4#Lean.Meta.mkAppM in tactic code are incorrect, since expressions from the user can easily have holes, and also this function doesn't do the whole elaboration procedure with coercions. There's docs4#Lean.Elab.Term.elabAppArgs to create applications, but you do have to think about the TermElabM monad.)

[Kyle Miller]

Rather than qq quotations, it's possible to do a lot of these things with syntax quotations, but unlike Lean 3 you have to explicitly run the elaborator on these. You can embed expressions into syntax using docs4#Lean.Elab.Term.exprToSyntax

For individual applications I just find it's easier to do it by hand than having to look at expressions with exprToSyntax in them.

[Kyle Miller]

@Eric Wieser Syntax quotations are like pexpr quotations, and qq quotations are like expr quotations, if you want the Lean 3 analogues. In Lean 4, there's a small hoop you have to jump through to embed an "expr" into a "pexpr", which is this exprToSyntax function. It creates a syntactic representation of a metavariable, embeds that, and assigns the metavariable to your Expr.

[Eric Wieser]

Perhaps I'm misremembering the lean3 src#tactic.interactive.apply_fun implementation

[Kyle Miller]

It's using pexpr quotations and to_expr, which could be translated as Syntax quotations and running the elaborator. The Lean 3 one is not making use of expected types, and it's not collecting any holes like refine would.

[Kyle Miller]

If you want to see a pexpr-like quotation, take a look at this line in the PR.