simping with instance arguments

Stream: general

[Paul Reichert]

I just stumbled over a situation where I wanted to simp a term like in the following mwe:

import algebra.group.defs group_theory.submonoid.basic
  group_theory.submonoid.operations

def p (V : Type) [add_monoid V] : Prop := sorry

example {V : Type}
  [add_monoid V]
  (k : ℕ → add_submonoid V)
  (h : p (k (0 - 0))) : false :=
begin
  simp only [nat.sub_self] at h,
end

I would expect that simp replaces 0 - 0 with 0. However, it seems that the [add_monoid V] instance that is expected by p prevents simp from doing so. It works after replacing simp only by rw. I know that those tactics work somehow differently but I cannot explain this phenomenon. Is this just a situation that should be avoided or solved with rw or is there another trick to make simp work?

[Kyle Miller]

If you look at the output of set_option pp.implicit true, you can see there are two places that simp would need to rewrite simultaneously. That's not something it can do without some more help, but rw can do it because it works by generalizing an expression and substituting everywhere simultaneously.

The way you can help simp out is via congr lemmas. Here's one that says "yes you can rewrite V, and here's how to construct a new instance":

@[congr]
lemma congr_p {V V' : Type} [add_monoid V] (h : V = V') : p V = @p V' (by { subst h, apply_instance }) :=
begin
  subst h,
end

The downside to this is that it inserts an eq.rec around the add_monoid instance.

[Paul Reichert]

Thanks for the explanation, the example and also the behavior of rw and simp make a lot more sense now!
And set_option pp.implicit true is also worth keeping in mind.