Zulip Chat Archive

Stream: new members

Topic: mul_right_comm_monoid


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

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

view this post on Zulip Anne Baanen (Apr 09 2021 at 13:21):

docs#left_cancel_comm_monoid, for the lazy like me

view this post on Zulip Damiano Testa (Apr 09 2021 at 13:22):

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

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

view this post on Zulip Damiano Testa (Apr 09 2021 at 13:25):

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

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

view this post on Zulip Damiano Testa (Apr 09 2021 at 13:25):

docs#left_cancel_comm_semigroup may not exist...

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

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

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

view this post on Zulip Damiano Testa (Apr 09 2021 at 13:27):

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

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

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

view this post on Zulip Damiano Testa (Apr 09 2021 at 13:29):

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

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

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

view this post on Zulip Anne Baanen (Apr 09 2021 at 13:32):

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

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

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

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

view this post on Zulip Damiano Testa (Apr 09 2021 at 13:35):

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

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

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

view this post on Zulip Anne Baanen (Apr 09 2021 at 13:40):

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

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

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

view this post on Zulip Eric Wieser (Apr 09 2021 at 13:52):

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

view this post on Zulip Damiano Testa (Apr 09 2021 at 13:56):

What does opt_param mean?

view this post on Zulip Eric Wieser (Apr 09 2021 at 13:58):

I think src#preorder has an example

view this post on Zulip Eric Wieser (Apr 09 2021 at 13:59):

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

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

view this post on Zulip Damiano Testa (Apr 09 2021 at 14:01):

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

view this post on Zulip Damiano Testa (Apr 09 2021 at 14:02):

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

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

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

view this post on Zulip Damiano Testa (Apr 09 2021 at 14:13):

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

view this post on Zulip Damiano Testa (Apr 09 2021 at 14:14):

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

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

view this post on Zulip Mario Carneiro (Apr 09 2021 at 14:29):

You need to add the to_additive after the class

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

view this post on Zulip Mario Carneiro (Apr 09 2021 at 14:30):

Those don't sound like they should be instances

view this post on Zulip Mario Carneiro (Apr 09 2021 at 14:30):

they will loop

view this post on Zulip Damiano Testa (Apr 09 2021 at 14:31):

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?

view this post on Zulip Mario Carneiro (Apr 09 2021 at 14:32):

Don't put to_additive on the class definition

view this post on Zulip Eric Wieser (Apr 09 2021 at 14:32):

Why not on the class definition?

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

view this post on Zulip Eric Wieser (Apr 09 2021 at 14:32):

Don't we do that everywhere?

view this post on Zulip Mario Carneiro (Apr 09 2021 at 14:32):

It has to be done after the definition of the class

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

view this post on Zulip Mario Carneiro (Apr 09 2021 at 14:33):

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

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

view this post on Zulip Eric Wieser (Apr 09 2021 at 14:33):

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

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

attribute [to_additive] group

view this post on Zulip Mario Carneiro (Apr 09 2021 at 14:33):

like this

view this post on Zulip Eric Wieser (Apr 09 2021 at 14:34):

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

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

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

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

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

view this post on Zulip Damiano Testa (Apr 09 2021 at 14:40):

image.png

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

view this post on Zulip Damiano Testa (Apr 09 2021 at 14:43):

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

view this post on Zulip Damiano Testa (Apr 09 2021 at 15:00):

PR #7134

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

view this post on Zulip 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 `(+)`. -/
@[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

view this post on Zulip Damiano Testa (Apr 09 2021 at 15:12):

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

view this post on Zulip Eric Wieser (Apr 09 2021 at 15:13):

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

view this post on Zulip Eric Wieser (Apr 09 2021 at 15:13):

Which is obviously not what you meant!

view this post on Zulip Eric Wieser (Apr 09 2021 at 15:13):

That attribute is only supposed to go on multiplicative things

view this post on Zulip Eric Wieser (Apr 09 2021 at 15:14):

I think you probably meant attribute [to_additive add_left_cancel_monoid] left_cancel_monoid

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

view this post on Zulip Eric Wieser (Apr 09 2021 at 15:14):

(your claim is not really true!)

view this post on Zulip Eric Wieser (Apr 09 2021 at 15:15):

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

view this post on Zulip Eric Wieser (Apr 09 2021 at 15:15):

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

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

view this post on Zulip Damiano Testa (Apr 09 2021 at 15:20):

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

view this post on Zulip Eric Wieser (Apr 09 2021 at 15:24):

No!

view this post on Zulip Eric Wieser (Apr 09 2021 at 15:25):

You've told lean that add_comm_monoid is the multiplicative version

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

view this post on Zulip Eric Wieser (Apr 09 2021 at 15:29):

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

view this post on Zulip 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 `(+)`. -/
@[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

view this post on Zulip Eric Wieser (Apr 09 2021 at 15:30):

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

view this post on Zulip Eric Wieser (Apr 09 2021 at 15:30):

The most recent one is correct

view this post on Zulip Damiano Testa (Apr 09 2021 at 15:30):

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

view this post on Zulip Damiano Testa (Apr 09 2021 at 15:30):

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

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

view this post on Zulip Damiano Testa (Apr 09 2021 at 15:32):

Finally I did something right!

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

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

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

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

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

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

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

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

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

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

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

view this post on Zulip Damiano Testa (Apr 09 2021 at 15:53):

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

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

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

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

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

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

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

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

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

view this post on Zulip Kevin Buzzard (Apr 09 2021 at 16:07):

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)

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

@[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

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

view this post on Zulip Kevin Buzzard (Apr 09 2021 at 16:49):

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

view this post on Zulip Damiano Testa (Apr 09 2021 at 16:57):

Thanks, Kevin!

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

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

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

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