## Stream: new members

### Topic: mul_right_comm_monoid

#### Damiano Testa (Apr 09 2021 at 13:08):

I could not find the instances below: am I missing some import? Does it make sense to PR it? Or should the solution be to have only a single cancel_comm_monoid class, instead of cancel_left_comm_monoid,cancel_right_comm_monoid and cancel_comm_monoid, with crossed instances relating them?

instance right_of_left {R : Type*} [left_cancel_comm_monoid R] : right_cancel_comm_monoid R :=
{ mul_right_cancel := λ a b c ac, begin
repeat { rw mul_comm _ b at ac},
exact mul_left_cancel ac,
end,
..(infer_instance : left_cancel_comm_monoid R) }

instance left_of_right {R : Type*} [right_cancel_comm_monoid R] : left_cancel_comm_monoid R :=
by apply_instance  -- fails

#### Damiano Testa (Apr 09 2021 at 13:18):

Here are a bunch of (missing?/unneeded) instances:

variable {R : Type*}

instance right_of_left [left_cancel_comm_monoid R] : right_cancel_comm_monoid R :=
{ mul_right_cancel := λ a b c ac, by { repeat { rw mul_comm _ b at ac}, exact mul_left_cancel ac },
..(infer_instance : left_cancel_comm_monoid R) }

instance left_of_right [right_cancel_comm_monoid R] : left_cancel_comm_monoid R :=
{ mul_left_cancel := λ a b c bc, by { repeat { rw mul_comm a at bc}, exact mul_right_cancel bc },
..(infer_instance : right_cancel_comm_monoid R) }

instance cancel_of_left [left_cancel_comm_monoid R] : cancel_comm_monoid R :=
{ ..(infer_instance : left_cancel_comm_monoid R),
..(infer_instance : right_cancel_comm_monoid R) }

instance cancel_of_right [right_cancel_comm_monoid R] : cancel_comm_monoid R :=
{ ..(infer_instance : left_cancel_comm_monoid R),
..(infer_instance : right_cancel_comm_monoid R) }

#### Anne Baanen (Apr 09 2021 at 13:21):

docs#left_cancel_comm_monoid, for the lazy like me

#### Damiano Testa (Apr 09 2021 at 13:22):

docs#left_cancel_comm_monoid ← Sorry, simply my attempt at seeing how to generate the link!

#### Damiano Testa (Apr 09 2021 at 13:24):

Unless there is a reason for preferring these typeclasses, I would opt for having a single cancel_comm_monoid typeclass, with "asymmetric" fields, choosing, say, mul_left_cancel.

#### Damiano Testa (Apr 09 2021 at 13:25):

And, if such a thing exist, also cancel_semigroup...

#### Anne Baanen (Apr 09 2021 at 13:25):

Looks like they were added in #3688 and we didn't realize left + comm is exactly the same as right + comm.

#### Damiano Testa (Apr 09 2021 at 13:25):

docs#left_cancel_comm_semigroup may not exist...

#### Anne Baanen (Apr 09 2021 at 13:26):

So yes, defining cancel_comm_monoid extends left_cancel_monoid, comm_monoid and then proving right_cancel as well, looks like the best option.

#### Anne Baanen (Apr 09 2021 at 13:26):

(i.e. provide instances cancel_comm_monoid.to_right_cancel_monoid and cancel_comm_monoid.to_cancel_monoid.)

#### Anne Baanen (Apr 09 2021 at 13:27):

Actually, judging from the number of instances, let's promote right_cancel_comm_monoid to be the one true typeclass.

#### Damiano Testa (Apr 09 2021 at 13:27):

...and there are the add versions as well.

#### Anne Baanen (Apr 09 2021 at 13:29):

Unfortunately @[to_additive] can't autogenerate structures (like typeclasses), so we have to write out the class twice :(

#### Damiano Testa (Apr 09 2021 at 13:29):

for the left version, there is this comment in the code:
-- TODO: I found 1 (one) lemma assuming [add_left_cancel_monoid].
-- Should we port more lemmas to this typeclass?
I guess that I am going to be the one taking, at least in part, this to completion!

#### Damiano Testa (Apr 09 2021 at 13:29):

Anne, or rather, in this case, remove them twice! :upside_down:

#### Damiano Testa (Apr 09 2021 at 13:31):

Ok, so I am going to keep the right_comm code, except that I remove the word right from it. Then, I change the left_comm classes to instance, correct?

#### Damiano Testa (Apr 09 2021 at 13:32):

Finally, I remove what is now comm with no indication of left/right.

From a procedural point of view, I would begin with removing the comm [no left/right], then promote right_comm to comm only and finally instance the left.

#### Anne Baanen (Apr 09 2021 at 13:32):

Sounds good. Don't we have docs#cancel_comm_monoid already?

#### Damiano Testa (Apr 09 2021 at 13:33):

Yes, but it extends both. Ah, I could make it extend only right, erase right and instance left. This is simpler, you are right!

#### Anne Baanen (Apr 09 2021 at 13:33):

So make sure that the "new" cancel_comm_monoid has the same lemmas and instances as the "old" cancel_comm_monoid.

#### Damiano Testa (Apr 09 2021 at 13:34):

I will get down to it! I am sure that lean will let me know if I mess something up...

#### Damiano Testa (Apr 09 2021 at 13:35):

What does ancestor mean below?

class add_cancel_comm_monoid (M : Type u)

Should this become

class add_cancel_comm_monoid (M : Type u)

#### Anne Baanen (Apr 09 2021 at 13:38):

I am not exactly sure to be honest! I think protect_proj will give the protected attribute to the fields of the structure (so that cancel_comm_monoid.mul doesn't become mul when the cancel_comm_monoid namespace is open).

#### Anne Baanen (Apr 09 2021 at 13:39):

And ancestor is used by the subtype_instance tactic to copy over fields, it looks like. So just copy over what comes after the extends.

#### Anne Baanen (Apr 09 2021 at 13:40):

So add_cancel_comm_monoid would look something like:

class add_cancel_comm_monoid (M : Type u)

#### Damiano Testa (Apr 09 2021 at 13:47):

Hence, the ancestor thing will be "forgotten" in the instance from cancel_comm to cancel_left, right?

#### Anne Baanen (Apr 09 2021 at 13:48):

Yes, it is just to keep track of which fields to copy and which ones to add when declaring a new instance via tactics.

#### Eric Wieser (Apr 09 2021 at 13:52):

Why not extend both but fill out the redundant axiom with opt_param?

#### Damiano Testa (Apr 09 2021 at 13:56):

What does opt_param mean?

#### Eric Wieser (Apr 09 2021 at 13:58):

I think src#preorder has an example

#### Eric Wieser (Apr 09 2021 at 13:59):

The (lt := ...) parameter fills that field automatically

#### Damiano Testa (Apr 09 2021 at 13:59):

I had seen this and I remember having been happy that it "just worked". I guess that now is my time to make it "just work", right? :wink:

#### Damiano Testa (Apr 09 2021 at 14:01):

also, when I do this

/-- Commutative version of cancel_monoid. -/
class cancel_comm_monoid (M : Type u) extends
left_cancel_monoid M, right_cancel_monoid M, comm_monoid M

class complains:

Failed to map fields of cancel_comm_monoid

#### Damiano Testa (Apr 09 2021 at 14:02):

This disappears, though, if I remove the line with @

#### Damiano Testa (Apr 09 2021 at 14:12):

In fact, simply erasing to_additive add_cancel_comm_monoid is enough to make the error go away.

#### Damiano Testa (Apr 09 2021 at 14:13):

Since the class just above cancel_comm_monoid is add_cancel_comm_monoid, maybe the to_additive is not needed? I would have guessed that to_additive would have created exactly the class that is defined above, right?

#### Damiano Testa (Apr 09 2021 at 14:13):

Ah, Anne said that to_additive does not work with classes...

#### Damiano Testa (Apr 09 2021 at 14:14):

So, I probably need it, but I am not able to make it work.

#### Damiano Testa (Apr 09 2021 at 14:18):

Sorry about the noise: I think that I am making progress! Ignore the previous comments, for the moment!

#### Damiano Testa (Apr 09 2021 at 14:30):

If the proof of an instance is by apply_instance, then that instance is not needed, correct?

This means that I will want to prove instances [left_cancel] + [comm] => [cancel] + [comm] and similarly for right and then same again for add.

#### Mario Carneiro (Apr 09 2021 at 14:30):

Those don't sound like they should be instances

they will loop

#### Damiano Testa (Apr 09 2021 at 14:31):

Mario, right now, this works:

/-- Commutative version of add_cancel_monoid. -/
class add_cancel_comm_monoid (M : Type u) extends

/-- Commutative version of cancel_monoid. -/
@[protect_proj, ancestor right_cancel_monoid left_cancel_monoid comm_monoid,
class cancel_comm_monoid (M : Type u) extends
right_cancel_monoid M, left_cancel_monoid M, comm_monoid M

I imagine that the last instance can be removed. Is the rest looking good?

#### Mario Carneiro (Apr 09 2021 at 14:32):

Don't put to_additive on the class definition

#### Eric Wieser (Apr 09 2021 at 14:32):

Why not on the class definition?

#### Damiano Testa (Apr 09 2021 at 14:32):

Ok, no instances [left_cancel] + [comm] => [cancel] + [comm]. Should there be defs instead? Or simply not there at all?

#### Eric Wieser (Apr 09 2021 at 14:32):

Don't we do that everywhere?

#### Mario Carneiro (Apr 09 2021 at 14:32):

It has to be done after the definition of the class

#### Damiano Testa (Apr 09 2021 at 14:32):

I copied the to_additive adapting what was already there. Still, I am happy to keep it or remove it, as needed-

#### Mario Carneiro (Apr 09 2021 at 14:33):

although maybe my info is out of date, it used to be a lot more annoying

#### Eric Wieser (Apr 09 2021 at 14:33):

Are you sure? I thought that's just because you can't put to_additive on the mul version until the add version is defined

#### Eric Wieser (Apr 09 2021 at 14:33):

And for some reason lots of files define the add version after the mul version

#### Mario Carneiro (Apr 09 2021 at 14:33):

/-- A group is a monoid with an operation ⁻¹ satisfying a⁻¹ * a = 1.

There is also a division operation / such that a / b = a * b⁻¹,
with a default so that a / b = a * b⁻¹ holds by definition.
-/
@[protect_proj, ancestor div_inv_monoid]
class group (G : Type u) extends div_inv_monoid G :=
(mul_left_inv :  a : G, a⁻¹ * a = 1)

/-- An add_group is an add_monoid with a unary - satisfying -a + a = 0.

There is also a binary operation - such that a - b = a + -b,
with a default so that a - b = a + -b holds by definition.
-/
@[protect_proj, ancestor sub_neg_monoid]
class add_group (A : Type u) extends sub_neg_monoid A :=
(add_left_neg :  a : A, -a + a = 0)

like this

#### Eric Wieser (Apr 09 2021 at 14:34):

Yes, exactly - the attribute is only separate because the definitions are in the wrong order

#### Eric Wieser (Apr 09 2021 at 14:34):

My guess would be that

@[foo, bar]
class X

and

@[foo]
class X

attribute [bar] X

are indistinguishable to lean

#### Mario Carneiro (Apr 09 2021 at 14:36):

No, they have different effects, because in the first one bar can act while X is still being constructed, so it can influence the constructors and such

#### Mario Carneiro (Apr 09 2021 at 14:36):

for example @[class] structure foo := (a : nat) vs structure foo := (a : nat) attribute [class] foo have different types for foo.a

#### Damiano Testa (Apr 09 2021 at 14:40):

Ok, I feel like the dog playing cards of the memes... the conclusion is that I should put the to additive after the definition as an attribute, right?

image.png

#### Anne Baanen (Apr 09 2021 at 14:42):

I think so: define class add_cancel_comm_monoid, then class cancel_comm_monoid, then attribute [to_additive] cancel_comm_monoid.

#### Damiano Testa (Apr 09 2021 at 14:43):

While I am at it, should the second be the preferred form, then?

class left_cancel_monoid (M : Type u) extends left_cancel_semigroup M, monoid M

--better as follows than above?
@[protect_proj, ancestor left_cancel_semigroup monoid]
class left_cancel_monoid (M : Type u) extends left_cancel_semigroup M, monoid M

PR #7134

#### Damiano Testa (Apr 09 2021 at 15:01):

It already has an error. I will try to fix it, but may need further assistance. Sorry for opening this can of worms and not being able to clean up my own mess...

#### Damiano Testa (Apr 09 2021 at 15:11):

Given my very superficial understanding of the discussion above, what is below seem to be in the wrong order: should the two definitions be swapped around?

/-- A commutative monoid is a monoid with commutative (*). -/
@[protect_proj, ancestor monoid comm_semigroup]
class comm_monoid (M : Type u) extends monoid M, comm_semigroup M

/-- An additive commutative monoid is an additive monoid with commutative (+). -/

#### Damiano Testa (Apr 09 2021 at 15:12):

(This is the order in which they appear in the file algebra/group/defs.)

#### Eric Wieser (Apr 09 2021 at 15:13):

Which is obviously not what you meant!

#### Eric Wieser (Apr 09 2021 at 15:13):

That attribute is only supposed to go on multiplicative things

#### Damiano Testa (Apr 09 2021 at 15:14):

Ok, but I think that I did not change this: this is what already was in the file before I touched it!
(Let me check that this is really true!)

#### Eric Wieser (Apr 09 2021 at 15:14):

(your claim is not really true!)

#### Eric Wieser (Apr 09 2021 at 15:15):

@[to_additive x] def y means "x is the additive version of y"

#### Eric Wieser (Apr 09 2021 at 15:15):

Usually you can omit x and lean works it out from the name

#### Damiano Testa (Apr 09 2021 at 15:17):

Ok, I will change this, but looking at the file in git, I do not think that I wrote this. Still, I am happy to change it! :smile:

#### Damiano Testa (Apr 09 2021 at 15:20):

Is this the correct form, then?

/-- An additive commutative monoid is an additive monoid with commutative (+). -/

/-- A commutative monoid is a monoid with commutative (*). -/
@[protect_proj, ancestor monoid comm_semigroup]
class comm_monoid (M : Type u) extends monoid M, comm_semigroup M

No!

#### Eric Wieser (Apr 09 2021 at 15:25):

You've told lean that add_comm_monoid is the multiplicative version

#### Damiano Testa (Apr 09 2021 at 15:28):

I'm sorry, I am trying to understand and keep everything straight, but I am clearly failing. I will try to produce a better version!

#### Eric Wieser (Apr 09 2021 at 15:29):

That example above isn't copied from group/basic, is assume?

#### Damiano Testa (Apr 09 2021 at 15:29):

This works in this case, right? Or am I still confused?

/-- An additive commutative monoid is an additive monoid with commutative (+). -/

/-- A commutative monoid is a monoid with commutative (*). -/
@[protect_proj, ancestor monoid comm_semigroup]
class comm_monoid (M : Type u) extends monoid M, comm_semigroup M

#### Eric Wieser (Apr 09 2021 at 15:30):

Your last line is different between that snippet and the previous one

#### Eric Wieser (Apr 09 2021 at 15:30):

The most recent one is correct

#### Damiano Testa (Apr 09 2021 at 15:30):

The very first one was, the one with the comm_monoid before the `add_comm_monoid*.

#### Damiano Testa (Apr 09 2021 at 15:30):

Yes, I changed the last line, since I imagine that that would fix the issue...

#### Eric Wieser (Apr 09 2021 at 15:31):

That most recent one looks fine, and it doesn't care what order the two classes go in as long as the attribute is after both

#### Damiano Testa (Apr 09 2021 at 15:32):

Finally I did something right!

#### Damiano Testa (Apr 09 2021 at 15:33):

So, as a "generic rule", the name not inside the square brackets should not had add, correct?

#### Damiano Testa (Apr 09 2021 at 15:35):

To be honest, I had completely missed the distinction between inside and outside the square brackets. I hope that I have it straight now.

#### Kevin Buzzard (Apr 09 2021 at 15:44):

@[to_additive x] def y attaches the attribute to y. attribute [to_additive] x attaches the attribute to x.

#### Kevin Buzzard (Apr 09 2021 at 15:45):

You either attach the tag when you're making the definition (e.g. @[simp] theorem blah...) or you attach the tag afterwards (e.g. theorem blah... and then later attribute [simp] blah).

#### Damiano Testa (Apr 09 2021 at 15:46):

Ah, Kevin, one more "subtlety" that I had missed! Anyway, the PR has been building for over 5s now, so it must all be correct... :upside_down:

#### Kevin Buzzard (Apr 09 2021 at 15:47):

You can use #print blah to see all the tags attached to the definition/theorem called blah -- they appear at the very top of the output.

#### Damiano Testa (Apr 09 2021 at 15:48):

Also, from the discussion above, I gathered that @[to_additive] and attribute [to_additive] are not equivalent and the latter seems to be preferred.

#### Kevin Buzzard (Apr 09 2021 at 15:49):

I think they are equivalent. I think you're confused because the to_additive attribute can take other inputs.

#### Kevin Buzzard (Apr 09 2021 at 15:50):

here is an example in mathlib where the to_additive attribute is actually taking an input -- a string, which is the docstring for the additive version. to_additive is a very flexible attribute and I completely agree that there is right now no good place to read about how it works.

#### Damiano Testa (Apr 09 2021 at 15:50):

Kevin, this is what made me say what I did: honestly, I do not understand what the difference is/might be/isn't!
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/mul_right_comm_monoid/near/233831681

#### Kevin Buzzard (Apr 09 2021 at 15:51):

The things you wrote above are equivalent, because you didn't give to_additive any inputs. The fun starts when you add other attributes at the same time, or add attributes which do funky stuff.

#### Damiano Testa (Apr 09 2021 at 15:53):

I am confused on so many levels that I do not even make sense to myself...

#### Kevin Buzzard (Apr 09 2021 at 15:54):

For example @[simp, to_additive] def x... is different to @[to_additive, simp] def x... because in the first one the additivised version of x will also get the simp attribute.

#### Kevin Buzzard (Apr 09 2021 at 15:57):

some attributes are quite powerful and subtle things, and to_additive is one of them. The way I learnt how it worked was just by looking at files like submonoid.basic and making sure I understood what was going on and why things were done the way they were done. But I guess what really taught me was writing some code like this myself, and being forced to learn it (like you are now).

#### Kevin Buzzard (Apr 09 2021 at 15:59):

I think that when I was at your stage (a competent Lean programmer and a mathematician) I started to ask myself whether I could actually completely understand random Lean files in mathlib, as opposed to just "basically understanding what was going on". I still ignore pretty much all meta and do code, but everything else I decided that I should probably be able to get to the bottom of it (and of course there are mathematicians who decide to understand meta code too...)

#### Damiano Testa (Apr 09 2021 at 16:00):

Ok, thanks for the encouragement! I think that the PR is building now, so I must have learned something! :upside_down:

#### Bryan Gin-ge Chen (Apr 09 2021 at 16:01):

Custom attributes like to_additive and simps (but not simp, I think) are basically metaprograms like tactics that run as Lean processes a declaration. We should expand the documentation if the way to use one isn't completely clear.

#### Kevin Buzzard (Apr 09 2021 at 16:03):

You should write some to_additive doc before you forget everything. The basic things are: (1) basic usage (it makes an additive version of a multiplicative lemma) (2) add the attribute after simp if you want the simp to apply to the additive version (3) for structures (rather than theorems) you have to make the structure yourself and then tag it later (your confusion about adding the attribute at the same time or afterwards) (4) link to the "dictionary" which auto-generates things like theorem names (5) how to override docstrings e.g. with add_decl_doc (see for example line 279 of submonoid.basic, I linked to the file above) (6) the gotcha with g^n vs n smul g and how it breaks everything.

#### Damiano Testa (Apr 09 2021 at 16:03):

Well, at the moment, I am having difficulty even keeping track of whether something is inside or outside some brackets, so my issues are probably at a more fundamental level than what the documentation might say.

That and having to keep track of whether there was an add or not, a right + comm or not really crossed my eyes!

#### Damiano Testa (Apr 09 2021 at 16:04):

Ok, I might give this a shot! Actually, your summary is already clearer than what is in my mind...

#### Kevin Buzzard (Apr 09 2021 at 16:07):

oh also the docstring trick

/-- multiplicative docstring -/

and the "choose another name rather than the auto-generated one" trick e.g.

lemma ordered_comm_group.mul_lt_mul_left' (a b : α) (h : a < b) (c : α) : c * a < c * b :=

(remove the prime, because there will be some ring version which doesn't have an additive counterpart)

#### Yakov Pechersky (Apr 09 2021 at 16:09):

The final aspect is tagging something with to_additive "out of band", that is, via an attribute ... line like at

@[simp] lemma order_of_one : order_of (1 : α) = 1 :=
begin
apply le_antisymm,
{ exact order_of_le_of_pow_eq_one (nat.one_pos) (pow_one 1) },
{ exact nat.succ_le_of_lt ( order_of_pos' 1, nat.one_pos, pow_one 1⟩⟩) }
end

#### Damiano Testa (Apr 09 2021 at 16:41):

Is there a way to get Lean to list the attributes of a given lemma? Say that I want to discover whether an autogenerated lemma is or isn't simp: chan I #check or #print or something like this to find out?

#### Kevin Buzzard (Apr 09 2021 at 16:49):

#print and look at the very top of the output.

Thanks, Kevin!

#### Damiano Testa (Apr 09 2021 at 19:47):

To my surprise, once I fixed the silly errors that I introduced, PR #7134 "just worked"! The 4 typeclasses (add_)left_cancel_comm_monoid, (add_)right_cancel_comm_monoid can leave mathlib and no one would notice...

#### Damiano Testa (Apr 09 2021 at 20:22):

I also just noticed that this might be the first time that a PR of mine actually has a net negative effect on the number of lines of code in mathlib.

#### Anne Baanen (Apr 09 2021 at 21:19):

Damiano Testa said:

I also just noticed that this might be the first time that a PR of mine actually has a net negative effect on the number of lines of code in mathlib.

"Fools ignore complexity. Pragmatists suffer it. Some can avoid it. Geniuses remove it." Congratulations, you are now a genius :)

#### Notification Bot (Apr 10 2021 at 00:05):

This topic was moved by Scott Morrison to #Is there code for X? > mul_right_comm_monoid

Last updated: May 11 2021 at 23:11 UTC