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

Stream: general

[Scott Morrison]

Can anyone find where add_comm acquires simp?

[Johan Commelin]

I do find

git grep "attri.*simp.*add_comm"
src/set_theory/lists.lean:local attribute [-simp] add_comm add_assoc

[Johan Commelin]

Maybe it's in core?

[Chris Hughes]

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]

in init.algebra.group

[Johan Commelin]

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

[Chris Hughes]

I quite like having it as a simp lemma.

[Scott Morrison]

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]

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

[Patrick Massot]

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

[Floris van Doorn]

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]

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]

Chris proposed a diagnosis several posts upstairs

[Edward Ayers]

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]

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

[Johan Commelin]

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

[Edward Ayers]

yep

[Edward Ayers]

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

[Edward Ayers]

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

[Edward Ayers]

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]

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

Aw damn.

[Edward Ayers]

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]

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

[Scott Morrison]

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

[Simon Hudon]

Yeah, I think so

[Marc Huisinga]

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