## Stream: general

### Topic: where does the @[simp] on add_comm come from?

#### Scott Morrison (Sep 23 2019 at 10:55):

Can anyone find where add_comm acquires simp?

#### Johan Commelin (Sep 23 2019 at 11:01):

I do find

git grep "attri.*simp.*add_comm"


#### Johan Commelin (Sep 23 2019 at 11:01):

Maybe it's in core?

#### Chris Hughes (Sep 23 2019 at 11:01):

mul_comm is locally simp when the run_cmd transport_multiplicative_to_additive defining add_comm is defined, so I guess that's where it gets the attribute.

#### Chris Hughes (Sep 23 2019 at 11:01):

in init.algebra.group

#### Johan Commelin (Sep 23 2019 at 11:02):

Maybe that line from set_theory.lists should move to logic.basic and become global?

#### Chris Hughes (Sep 23 2019 at 12:20):

I quite like having it as a simp lemma.

#### Scott Morrison (Sep 23 2019 at 12:22):

It frustrates me to no end. I get everything all lined up so simp will work, but then simp uses add_comm and arbitrarily jumbles up terms.

#### Scott Morrison (Sep 23 2019 at 12:22):

I think you can't globally remove an attribute anyway.

#### Patrick Massot (Sep 23 2019 at 12:54):

To me it sounds like automatic invocations of add_comm should be done by ring, abel and similar tactics.

#### Floris van Doorn (Sep 23 2019 at 15:06):

I think add_comm is the declaration that I most often have to remove from a simp set (simp [-add_comm]). I would also have preferred it to not have simp by default.

#### Simon Hudon (Sep 23 2019 at 15:09):

We should remove it from core. I don't know where the attribute is added. I'm wondering if it's through meta programming

#### Johan Commelin (Sep 23 2019 at 15:15):

Chris proposed a diagnosis several posts upstairs

#### Edward Ayers (Sep 23 2019 at 15:26):

A theory: I think it's in group.lean.

local attribute [simp] mul_comm mul_assoc mul_left_comm
-- ... later

meta def transport_with_dict (dict : name_map name) (src : name) (tgt : name) : command :=
copy_decl_using dict src tgt
>> copy_attribute reducible src tt tgt
>> copy_attribute simp src tt tgt
>> copy_attribute instance src tt tgt


The local on local attribute means that the attribute is only present inside the section right? But maybe this localness gets clobbered when it does the copy_attribute.

#### Patrick Massot (Sep 23 2019 at 15:26):

I have simp [-sub_eq_add_neg] much more often than simp [-add_comm]

#### Johan Commelin (Sep 23 2019 at 15:28):

@Edward Ayers Isn't that what Chris also said?

yep

#### Edward Ayers (Sep 23 2019 at 15:31):

But mul_comm isn't a simp lemma I think. So this is a bug in transport_with_dict?

#### Edward Ayers (Sep 23 2019 at 15:40):

I'm wondering if setting that tt flag on copy_attribute will cause it to be local

#### Edward Ayers (Sep 23 2019 at 15:48):

Ok so copy_attribute simp src ff tgt will set it as a local attribute. But I can't see a tactic that tells you whether an attribute is local or not so I think the best fix is to just unset the attribute in the group.lean file.

#### Edward Ayers (Sep 23 2019 at 15:56):

I think you can't globally remove an attribute anyway.

Aw damn.

#### Edward Ayers (Sep 23 2019 at 16:13):

You can actually remove mul_comm as a local simp attr and thegroup.lean file still checks, so that might be the best way to fix it.

#### Edward Ayers (Sep 23 2019 at 22:15):

PRed a change to remove add_comm and add_left_comm from simp lemmas. https://github.com/leanprover-community/lean/pull/65

#### Scott Morrison (Sep 23 2019 at 23:46):

I suspect this might be a change that makes it hard to keep mathlib in sync with both 3.4.2 and 3.5c?

Yeah, I think so

#### Marc Huisinga (Sep 29 2019 at 22:39):

ne.def is another simp lemma that i frequently remove from my simp only set

Last updated: May 14 2021 at 23:14 UTC