Zulip Chat Archive

Stream: maths

Topic: add_comm_monoid (set M)


view this post on Zulip Kevin Buzzard (Nov 16 2019 at 19:52):

The constructor for add_comm_monoid is non-canonical because it demands zero_add, which follows from the other axioms. I can fix this up by making my own custom constructor. But if I use my own constructor I lose the luxury of being able to write { add := (+), add_assoc := ..., I have to feed the proofs in without saying what they're proofs of. What I write below is more readable (I want an addition on subsets of the reals), but I can't get it to compile, I want zero_add for free and I can't pull it off. Should I just give in and run the constructor on the proofs?

import tactic.interactive
import data.set.basic

instance (M : Type*) [has_zero M] : has_zero (set M) := {0}

instance (M : Type*) [has_add M] : has_add (set M) :=
⟨λ X Y, {z |  (x  X) (y  Y), z = x + y}

def add_comm_monoid.mk' {M : Type*} [has_add M] [has_zero M]
(add_assoc :  a b c : M, a + b + c = a + (b + c))
(add_zero :  a : M, a + 0 = a)
(add_comm :  a b : M, a + b = b + a) :
add_comm_monoid M :=
{ add := (+),
  add_assoc := add_assoc,
  zero := (0),
  add_zero := add_zero,
  add_comm := add_comm,
  zero_add := λ a, add_comm a 0  add_zero a,
}

instance (M : Type*) [add_comm_monoid M] : add_comm_monoid (set M) :=
{ add := (+),
  add_assoc := λ A B C, set.ext $ λ x,
  
    λ ab, a, ha, b, hb, rfl, c, hc, hx,
      a, ha, b + c, b, hb, c, hc, rfl, hx.symm  add_assoc a b c,
    λ a, ha, bc, b, hb, c, hc, rfl, hx,
      a + b, a, ha, b, hb, rfl, c, hc, hx.symm  (add_assoc a b c).symm
  ,
  zero := (0),
  add_zero := λ A, set.ext $ λ x, 
    begin
      rintro a, ha, O, hO, hxa,
      rw set.mem_singleton_iff at hO,
      rwa [hxa, hO, add_zero],
    end,
    λ hx, x, hx, 0, set.mem_singleton 0, (add_zero x).symm⟩⟩,
  add_comm := λ A B, set.ext $ λ x,
  
    λ a, ha, b, hb, hx,
      b, hb, a, ha, hx.symm  add_comm a b,
    λ b, hb, a, ha, hx,
      a, ha, b, hb, hx.symm  (add_comm a b).symm,
  ,
  zero_add := (@add_comm_monoid.mk' (set M) _ _ _ (_) _).zero_add -- I can't fill in the holes
  -- with the proofs I just did?
  }

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 19:52):

PS is this there already?

view this post on Zulip Johan Commelin (Nov 16 2019 at 20:09):

I guess you are looking for algebra.pointwise?

view this post on Zulip Johan Commelin (Nov 16 2019 at 20:09):

Or where is that file?

view this post on Zulip Johan Commelin (Nov 16 2019 at 20:09):

https://github.com/leanprover-community/mathlib/blob/61ccaf65c4cfc9c6ff103463342e034347eb8b89/src/algebra/pointwise.lean

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 20:42):

So the only mention of comm_monoid is

def pointwise_mul_comm_semiring [comm_monoid α] : comm_semiring (set α) :=
{ mul_comm := λ s t, set.ext $ λ a,
  by split; { rintros ⟨_, _, _, _, rfl, exact ⟨_, _, _, _, mul_comm _ _⟩ },
  ..pointwise_mul_semiring }

But this means that set M is a comm_monoid if M is a comm_monoid. I should be able to magically to_additive this now somehow?

view this post on Zulip Johan Commelin (Nov 16 2019 at 20:53):

No, I don't think that will work, because the conclusion doesn't have an additive version

view this post on Zulip Johan Commelin (Nov 16 2019 at 20:53):

I should just have made a commutative version of https://github.com/leanprover-community/mathlib/blob/61ccaf65c4cfc9c6ff103463342e034347eb8b89/src/algebra/pointwise.lean#L65 but I seem to not have done that

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 21:14):

gotcha

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 21:16):

Why isn't this trivial to make from what you have made? There will be some map from comm_semiring X to comm_monoid X right?

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:16):

In algebra/pointwise.lean:

def pointwise_mul_comm_semiring [comm_monoid α] : comm_semiring (set α) :=
{ mul_comm := λ s t, set.ext $ λ a,
  by split; { rintros ⟨_, _, _, _, rfl, exact ⟨_, _, _, _, mul_comm _ _⟩ },
  ..pointwise_mul_semiring }

local attribute [instance] pointwise_mul_semiring

-- new part here
-- can't get to_additive to work
--@[to_additive]
def foo [comm_monoid α] : comm_monoid (set α) :=
@comm_semiring.to_comm_monoid (set α) pointwise_mul_comm_semiring

How do I get @[to_additive] to buy that? The error is

to_additive: can't transport set.foo to itself

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:17):

Don't you love it when Kevin tries to edit mathlib

view this post on Zulip Reid Barton (Nov 16 2019 at 22:18):

I think the problem is that the name it would produce is the same, because foo doesn't contain any of the magic words

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:18):

Did you see you get a mention in the natural number game within the context of magic words? Oh actually that might still be in the beta

view this post on Zulip Reid Barton (Nov 16 2019 at 22:19):

no...

view this post on Zulip Reid Barton (Nov 16 2019 at 22:20):

very good

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:20):

#where -- namespace set

@[to_additive]
def comm_monoid [comm_monoid α] : comm_monoid (set α) :=
@comm_semiring.to_comm_monoid (set α) pointwise_mul_comm_semiring

/-
to_additive: can't transport set.comm_monoid to itself
-/

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:20):

So what is the magic word?

view this post on Zulip Reid Barton (Nov 16 2019 at 22:20):

I think you can put the name you want it to transform to after to_additive

view this post on Zulip Reid Barton (Nov 16 2019 at 22:21):

I don't know the whole list... usually things like mul or one

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:22):

Progress:

@[to_additive set.add_comm_monoid]
def comm_monoid [comm_monoid α] : comm_monoid (set α) :=
@comm_semiring.to_comm_monoid (set α) pointwise_mul_comm_semiring

/-
type mismatch at application
  @pointwise_mul_comm_semiring α _inst_1
term
  _inst_1
has type
  add_comm_monoid α
but is expected to have type
  comm_monoid α
-/

Does to_additive not move me from comm_monoid to add_comm_monoid?

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:22):

This is the sort of error that you get when to_additive needs more hints

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:30):

@Yury G. Kudryashov what am I doing wrong?

view this post on Zulip Chris Hughes (Nov 16 2019 at 22:30):

I'm guessing comm_semiring.to_comm_monoid doesn't have a to_additive attribute with comm_semiring.to_add_comm_monoid

view this post on Zulip Yury G. Kudryashov (Nov 16 2019 at 22:31):

I guess @Chris Hughes is right.

view this post on Zulip Chris Hughes (Nov 16 2019 at 22:31):

Which makes sense, because they're distinguished by more than just notation

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:32):

But the fact that this correctly doesn't exist doesn't help me, because I'm trying to do something sensible, right?

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:33):

I have a map comm_monoid α -> comm_monoid (set α) and now I want my map add_comm_monoid α -> add_comm_monoid (set α) for free. Isn't that how life works?

view this post on Zulip Chris Hughes (Nov 16 2019 at 22:33):

Maybe if you mark pointwise_mul_comm_semiring as to_additive

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:34):

type mismatch at application
  @pointwise_mul_semiring α (@add_comm_monoid.to_add_monoid α _inst_1)
term
  @add_comm_monoid.to_add_monoid α _inst_1
has type
  add_monoid α
but is expected to have type
  monoid α

view this post on Zulip Chris Hughes (Nov 16 2019 at 22:34):

But then it's not obvious to me which add_comm_monoid, structure you want.

view this post on Zulip Chris Hughes (Nov 16 2019 at 22:35):

Because there are two that makes sense, the additive one from the semiring and the multiplicative one from the semiring.

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:35):

Yeah I don't think that I want a to_additive version of pointwise_mul_comm_semiring

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:36):

I know what the additive version of comm_monoid is but I don't know what the additive version of comm_semiring is. Can I just manufacture this easily manually with ease using additive and multiplicative somehow and then sort out the attributes afterwards?

view this post on Zulip Reid Barton (Nov 16 2019 at 22:37):

Yeah, I think additive/multiplicative might be the way to go

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:37):

attribute [to_additive set.add_comm_monoid] set.comm_monoid or something?

view this post on Zulip Yury G. Kudryashov (Nov 16 2019 at 22:38):

pointwise_mul_semiring uses sup for addition, not pointwise (+).

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:38):

right. There is no +

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:38):

But I don't care about this semiring

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:39):

I can make set.comm_monoid and now I want set.add_comm_monoid for free but I'm going to have to make it I think.

view this post on Zulip Yury G. Kudryashov (Nov 16 2019 at 22:40):

You can try to define set.comm_monoid using { .. pointwise_mul_semiring }

view this post on Zulip Yury G. Kudryashov (Nov 16 2019 at 22:40):

Not sure if it'll work

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:40):

As you can see, I already made the function in the first post in this thread. But I don't understand if this is a mathlib-acceptable approach.

view this post on Zulip Yury G. Kudryashov (Nov 16 2019 at 22:41):

Another way is to split the definition of pointwise_mul_semiring into two steps: first define the multiplicative monoid, then the semiring.

view this post on Zulip Chris Hughes (Nov 16 2019 at 22:41):

Is there a function comm_monoid X -> add_comm_monoid X in mathlib

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:41):

Aah the penny is dropping

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:42):

The point is that the algorithm can't handle the translation the way I want to do it because it goes via the semiring and the algorithm gets stuck?

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:42):

Is there a function comm_monoid X -> add_comm_monoid X in mathlib

There should be an equiv!

view this post on Zulip Yury G. Kudryashov (Nov 16 2019 at 22:43):

Look at algebra/group/type_tags

view this post on Zulip Yury G. Kudryashov (Nov 16 2019 at 22:44):

You can do a trick like add_comm_monoid (set M) := show @add_comm_monoid (additive (set (multiplicative M))), by apply_instance; didn't test

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:45):

tactic.mk_instance failed to generate instance for
  add_comm_monoid (additive (set (multiplicative α)))
state:
α : Type u_1,
_inst_1 : add_comm_monoid α
⊢ add_comm_monoid (additive (set (multiplicative α)))

view this post on Zulip Reid Barton (Nov 16 2019 at 22:46):

is your original definition an instance?

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:46):

My original definition isn't even in the file. I thought this was what we were trying to avoid.

view this post on Zulip Reid Barton (Nov 16 2019 at 22:49):

I mean def comm_monoid [comm_monoid α] : comm_monoid (set α) :=

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:49):

How do I figure out the name of this instance painlessly?

view this post on Zulip Chris Hughes (Nov 16 2019 at 22:51):

I'm betting additive.add_comm_monoid

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:51):

I don't need to know, I've finally got there thanks to the extensive help from the three of you.

view this post on Zulip Chris Hughes (Nov 16 2019 at 22:52):

I don't know of a general method for finding that out painlessly. The best I know it to make a def of the same type, prove it with apply_instance and #print it.

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:58):

#1696

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 22:59):

Thanks @Johan Commelin @Reid Barton @Chris Hughes @Yury G. Kudryashov for eventually getting me over the line.

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 23:45):

updated #1696 after conversation which for some reason ended up in another thread

view this post on Zulip Kevin Buzzard (Nov 17 2019 at 00:04):

Is there room for this

def add_comm_monoid.mk' {M : Type*} [has_add M] [has_zero M]
(add_assoc :  a b c : M, a + b + c = a + (b + c))
(add_zero :  a : M, a + 0 = a)
(add_comm :  a b : M, a + b = b + a) :
add_comm_monoid M :=
{ add := (+),
  add_assoc := add_assoc,
  zero := (0),
  add_zero := add_zero,
  add_comm := add_comm,
  zero_add := λ a, add_comm a 0  add_zero a,
}

in mathlib? It's the correct constructor for add_comm_monoid where we don't ask for axioms which can be deduced from other axioms.

view this post on Zulip Mario Carneiro (Nov 17 2019 at 00:07):

Yes, I've wanted to see these sort of things for a while. As you've pointed out, it's a bit sad that you lose constructor notation. One way to fix that is to make a new structure with only these fields and a function to take it to add_comm_monoid. Compare with nonneg_group for making ordered groups

view this post on Zulip Mario Carneiro (Nov 17 2019 at 00:08):

However, I think it is a bad idea to make this auxiliary structure a class, because it just makes the instance hierarchy bigger

view this post on Zulip Kevin Buzzard (Nov 17 2019 at 00:09):

I see. So the user makes an auxiliary structure and then they register the resulting add_comm_monoid term with type class inference afterwards?

view this post on Zulip Mario Carneiro (Nov 17 2019 at 00:11):

right, they get a proof that looks like

instance : add_comm_monoid foo :=
add_comm_monoid.mk' {
  zero := ...,
  add_zero := ...,
  add_comm := ...,
  ..foo.add_semigroup }

view this post on Zulip Kevin Buzzard (Nov 17 2019 at 00:42):

gaargh I broke measure_theory/outer_measure

view this post on Zulip Kevin Buzzard (Nov 17 2019 at 00:49):

fixed

view this post on Zulip Kevin Buzzard (Nov 17 2019 at 00:53):

Where does add_comm_monoid.mk' go? It seems to want to go in core.

view this post on Zulip Kevin Buzzard (Nov 17 2019 at 00:58):

Is there an argument which says that these auxiliary structures should go in some new file? I remember now making such a better constructor for group and I bet I never PR'ed that.

view this post on Zulip Kevin Buzzard (Nov 17 2019 at 00:59):

I seem to use class has_group_notation (G : Type) extends has_mul G, has_one G, has_inv G

view this post on Zulip Mario Carneiro (Nov 17 2019 at 01:12):

Stuff about the algebraic hierarchy which "should go in core" is generally in the algebra folder. Missing theorems about groups and monoids are in algebra.group


Last updated: May 19 2021 at 02:10 UTC