mul_right_comm_monoid

Stream: new members

[Damiano Testa]

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]

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]

docs#left_cancel_comm_monoid, for the lazy like me

[Damiano Testa]

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

[Damiano Testa]

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]

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

[Anne Baanen]

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

[Damiano Testa]

docs#left_cancel_comm_semigroup may not exist...

[Anne Baanen]

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]

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

[Anne Baanen]

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

[Damiano Testa]

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

[Anne Baanen]

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

[Damiano Testa]

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]

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

[Damiano Testa]

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]

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]

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

[Damiano Testa]

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]

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

[Damiano Testa]

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

[Damiano Testa]

What does ancestor mean below?

@[protect_proj, ancestor add_left_cancel_comm_monoid add_right_cancel_comm_monoid]
class add_cancel_comm_monoid (M : Type u)
  extends add_left_cancel_comm_monoid M, add_right_cancel_comm_monoid M

Should this become

@[protect_proj, ancestor add_right_cancel_comm_monoid]
class add_cancel_comm_monoid (M : Type u)
  extends add_right_cancel_comm_monoid M

[Anne Baanen]

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]

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]

So add_cancel_comm_monoid would look something like:

@[protect_proj, ancestor add_comm_monoid add_right_cancel_monoid]
class add_cancel_comm_monoid (M : Type u)
  extends add_comm_monoid M, add_right_cancel_monoid M

[Damiano Testa]

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

[Anne Baanen]

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]

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

[Damiano Testa]

What does opt_param mean?

[Eric Wieser]

I think src#preorder has an example

[Eric Wieser]

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

[Damiano Testa]

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]

also, when I do this

/-- Commutative version of cancel_monoid. -/
@[protect_proj, ancestor right_cancel_monoid left_cancel_monoid comm_monoid, to_additive add_cancel_comm_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]

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

[Damiano Testa]

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

[Damiano Testa]

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]

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

[Damiano Testa]

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

[Damiano Testa]

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

[Mario Carneiro]

You need to add the to_additive after the class

[Damiano Testa]

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]

Those don't sound like they should be instances

[Mario Carneiro]

they will loop

[Damiano Testa]

Mario, right now, this works:

/-- Commutative version of add_cancel_monoid. -/
@[protect_proj, ancestor add_right_cancel_monoid add_left_cancel_monoid add_comm_monoid]
class add_cancel_comm_monoid (M : Type u) extends
  add_right_cancel_monoid M, add_left_cancel_monoid M, add_comm_monoid M

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

/-- An add_cancel_comm_monoid. -/
instance add_left_cancel_comm_monoid (M : Type u) [add_cancel_comm_monoid M] :
  add_left_cancel_monoid M := by apply_instance

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

[Mario Carneiro]

Don't put to_additive on the class definition

[Eric Wieser]

Why not on the class definition?

[Damiano Testa]

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

[Eric Wieser]

Don't we do that everywhere?

[Mario Carneiro]

It has to be done after the definition of the class

[Damiano Testa]

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

[Mario Carneiro]

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

[Eric Wieser]

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]

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

[Mario Carneiro]

/-- 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)

attribute [to_additive] group

[Mario Carneiro]

like this

[Eric Wieser]

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

[Eric Wieser]

My guess would be that

@[foo, bar]
class X

and

@[foo]
class X

attribute [bar] X

are indistinguishable to lean

[Mario Carneiro]

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]

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

[Damiano Testa]

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?

[Damiano Testa]

image.png

[Anne Baanen]

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

[Damiano Testa]

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

@[protect_proj, ancestor left_cancel_semigroup monoid, to_additive add_left_cancel_monoid]
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
attribute [to_additive] add_left_cancel_monoid

[Damiano Testa]

PR #7134

[Damiano Testa]

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]

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 `(+)`. -/
@[protect_proj, ancestor add_monoid add_comm_semigroup]
class add_comm_monoid (M : Type u) extends add_monoid M, add_comm_semigroup M
attribute [to_additive] comm_monoid

[Damiano Testa]

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

[Eric Wieser]

attribute [to_additive] add_left_cancel_monoid means "add_left_cancel_monoid is the multiplicative version of some additive lemma"

[Eric Wieser]

Which is obviously not what you meant!

[Eric Wieser]

That attribute is only supposed to go on multiplicative things

[Eric Wieser]

I think you probably meant attribute [to_additive add_left_cancel_monoid] left_cancel_monoid

[Damiano Testa]

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]

(your claim is not really true!)

[Eric Wieser]

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

[Eric Wieser]

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

[Damiano Testa]

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]

Is this the correct form, then?

/-- An additive commutative monoid is an additive monoid with commutative `(+)`. -/
@[protect_proj, ancestor add_monoid add_comm_semigroup]
class add_comm_monoid (M : Type u) extends add_monoid M, add_comm_semigroup M

/-- 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
attribute [to_additive] add_comm_monoid

[Eric Wieser]

No!

[Eric Wieser]

You've told lean that add_comm_monoid is the multiplicative version

[Damiano Testa]

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]

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

[Damiano Testa]

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

/-- An additive commutative monoid is an additive monoid with commutative `(+)`. -/
@[protect_proj, ancestor add_monoid add_comm_semigroup]
class add_comm_monoid (M : Type u) extends add_monoid M, add_comm_semigroup M

/-- 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
attribute [to_additive] comm_monoid

[Eric Wieser]

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

[Eric Wieser]

The most recent one is correct

[Damiano Testa]

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

[Damiano Testa]

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

[Eric Wieser]

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]

Finally I did something right!

[Damiano Testa]

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

[Damiano Testa]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

oh also the docstring trick

/-- multiplicative docstring -/
@[to_additive "additive docstring"] def gi : galois_insertion...

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

@[to_additive ordered_add_comm_group.add_lt_add_left]
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]

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

@[simp] lemma add_order_of_zero : add_order_of (0 : H) = 1 :=
by simp [← order_of_of_add_eq_add_order_of]

attribute [to_additive add_order_of_zero] order_of_one

[Damiano Testa]

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]

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

[Damiano Testa]

Thanks, Kevin!

[Damiano Testa]

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]

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]

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]

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