# Zulip Chat Archive

## Stream: general

### Topic: simping with instance arguments

#### Paul Reichert (Aug 07 2022 at 15:37):

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 (Aug 07 2022 at 15:49):

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 (Aug 07 2022 at 17:37):

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.

Last updated: Aug 03 2023 at 10:10 UTC