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

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 :=
  simp only [nat.sub_self] at h,

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":

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

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