rw leaving instance side goal with instance in context

Stream: general

[Michael Stoll]

Consider this:

import number_theory.padics.padic_val

example {p n : ℕ} [fact p.prime] (h : n ≠ 0) : even (padic_val_nat p (n ^ 2)) :=
begin
  rw padic_val_nat.pow 2 h,
  exact even_two_mul _,
  -- leaves goal `fact (nat.prime p)`
  exact ⟨fact.out _⟩,
end

example {p n : ℕ} [hp : fact p.prime] (h : n ≠ 0) : even (padic_val_nat p (n ^ 2)) :=
begin
  rw @padic_val_nat.pow _ _ hp 2 h,
  exact even_two_mul _,
  -- works
end

Why does rw fail to find the instance when it is clearly available in the context?

[Ruben Van de Velde]

Perhaps lean does not know exactly what instance it needs when it's looking for it

[Michael Stoll]

simp_rw works, BTW.

[Eric Wieser]

exact ⟨fact.out _⟩ is a worse way of spelling apply_instance

[Michael Stoll]

I know, buit that's not my point here.

[Eric Wieser]

rw @padic_val_nat.pow p _ _ 2 h also works here

[Eric Wieser]

So the problem is that Lean does not know p in time to look for the instance

[Michael Stoll]

Why is simp_rw smarter than rw in this regard?
I assume rw could basically run try {apply_instance} after the fact on all unresolved instances to deal with this.

[Kevin Buzzard]

If it did this then 99% of the time it would be wasting its time, so it would just make things slower. It's all about the order in which things happen, the typeclass system runs, the unification system runs, some combination works most of the time, that's what we end up with.

[Michael Stoll]

I'd think it would not need to waste time if there are no instance goals left (which is usually the case).

[Kevin Buzzard]

At the end of the day people have thought very hard about rw and it's very unlikely that anyone is changing the algorithm; any changes to the algorithm would have huge ramifications across mathlib I should think. If you asked a computer scientist I should think that they would tell you that the whole fact thing is a code smell anyway, and the typeclass inference shouldn't be being used to carry around hypotheses that aren't actually typeclasses. In fact fact was a hack made up by either the perfectoid project or LTE (I forgot which) but I remember being warned about it at the time. Probably a better solution here is just to make p explicit in the statement of the lemma, to mitigate the code smell.

[Michael Stoll]

Well, these [fact p.prime] assumptions are all over mathlib by now...

[Kevin Buzzard]

Sure -- and I'm saying that perhaps this means that the usual algorithm ("make x implicit in a theorem if it's an iff statement and x is mentioned on both sides of the iff") for figuring out whether an input is implicit or explicit might not apply in this situation.

[Michael Stoll]

Anyway, in the concrete case, would you recommed using rw [... @name p _ _ ...], rw [... name ...], ..., apply_instance, or simp_rw [.... name ...] ? (In my PR #19054, I settled for simp_rw, as this seems the easiest to read.)

[Yury G. Kudryashov]

This happens sometimes in Lean 3 (AFAIR, not in Lean 4) when Lean doesn't know all arguments of the typeclass it needs to generate at some specific moment (not sure which one) of unification of your lemma with the goal.

[Yury G. Kudryashov]

Supplying more arguments in rw [my_lemma _] usually helps. Another standard workaround is to use apply_instance after rw. I remember writing these apply_instances in Lean 3 and removing them while porting.

[Michael Stoll]

As mentioned earlier, simp_rw seems to be an alternative, too (when it can be used).