Zulip Chat Archive

Stream: general

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


view this post on Zulip Scott Morrison (Sep 23 2019 at 10:55):

Can anyone find where add_comm acquires simp?

view this post on Zulip Johan Commelin (Sep 23 2019 at 11:01):

I do find

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

view this post on Zulip Johan Commelin (Sep 23 2019 at 11:01):

Maybe it's in core?

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Sep 23 2019 at 11:01):

in init.algebra.group

view this post on Zulip Johan Commelin (Sep 23 2019 at 11:02):

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

view this post on Zulip Chris Hughes (Sep 23 2019 at 12:20):

I quite like having it as a simp lemma.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Sep 23 2019 at 12:22):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Sep 23 2019 at 15:15):

Chris proposed a diagnosis several posts upstairs

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Sep 23 2019 at 15:26):

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

view this post on Zulip Johan Commelin (Sep 23 2019 at 15:28):

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

view this post on Zulip Edward Ayers (Sep 23 2019 at 15:29):

yep

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Edward Ayers (Sep 23 2019 at 15:56):

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

Aw damn.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Simon Hudon (Sep 23 2019 at 23:55):

Yeah, I think so

view this post on Zulip 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