Variables introduced in lambda in refine

Stream: general

[uwagjaynoi]

Here's an example:

example (Q: Prop)(x y : ℕ)
  (h : x = y → Q):
    (nat.succ x = nat.succ y → Q) :=
begin
  refine (λh3, _),
  -- intro h3,
  -- change x.succ=y.succ at h3,
  injection h3 with h1,
  exact h h1,
end

It errors

injection tactic failed, argument must be an equality proof where lhs and rhs are of the form (c ...), where c is a constructor

However, replacing the refine line with intro line or adding change line which both I think don't change anything will make it work.

So what's wrong with it, and how can I prevent it?

[Yaël Dillies]

The same happens with simp (in place of injection). Variables that are introduced in a lambda in a refine behave differently to the ones introduced with intros. I have no idea why.

[Eric Wieser]

change _ at h3, is enough to fix it

[Eric Wieser]

As is injection (show _, from h3) with h1,

[Mario Carneiro]

the issue is that the type of h3 when introduced in that way contains an assigned metavariable

[Yaël Dillies]

Is this something that can be fixed in refine?

[Eric Wieser]

Mario Carneiro said:

the issue is that the type of h3 when introduced in that way contains an assigned metavariable

Does "that way" refer to refine or show?

[Mario Carneiro]

lambda with no type annotation inside refine

[Mario Carneiro]

I think it is difficult to fix in refine IIRC, the assignment to the type is in fact determined out-of-band

[Mario Carneiro]

and we don't want to go traversing the whole term or the whole context instantiating everything

[Mario Carneiro]

in lean 4 we are consistently doing the opposite: it is the responsibility of the downstream tactic to call instantiateMVars whenever they need to pattern match on something

[Mario Carneiro]

that is, the blame is pointed at injection for not instantiating mvars before asking if the type of h3 is = of something