Zulip Chat Archive

Stream: maths

Topic: add_comm_monoid (set M)


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?
  }

Kevin Buzzard (Nov 16 2019 at 19:52):

PS is this there already?

Johan Commelin (Nov 16 2019 at 20:09):

I guess you are looking for algebra.pointwise?

Johan Commelin (Nov 16 2019 at 20:09):

Or where is that file?

Johan Commelin (Nov 16 2019 at 20:09):

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

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?

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

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

Kevin Buzzard (Nov 16 2019 at 21:14):

gotcha

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?

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

Kevin Buzzard (Nov 16 2019 at 22:17):

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

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

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

Reid Barton (Nov 16 2019 at 22:19):

no...

Reid Barton (Nov 16 2019 at 22:20):

very good

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

Kevin Buzzard (Nov 16 2019 at 22:20):

So what is the magic word?

Reid Barton (Nov 16 2019 at 22:20):

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

Reid Barton (Nov 16 2019 at 22:21):

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

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?

Kevin Buzzard (Nov 16 2019 at 22:22):

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

Kevin Buzzard (Nov 16 2019 at 22:30):

@Yury G. Kudryashov what am I doing wrong?

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

Yury G. Kudryashov (Nov 16 2019 at 22:31):

I guess @Chris Hughes is right.

Chris Hughes (Nov 16 2019 at 22:31):

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

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?

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?

Chris Hughes (Nov 16 2019 at 22:33):

Maybe if you mark pointwise_mul_comm_semiring as to_additive

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 α

Chris Hughes (Nov 16 2019 at 22:34):

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

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.

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

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?

Reid Barton (Nov 16 2019 at 22:37):

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

Kevin Buzzard (Nov 16 2019 at 22:37):

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

Yury G. Kudryashov (Nov 16 2019 at 22:38):

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

Kevin Buzzard (Nov 16 2019 at 22:38):

right. There is no +

Kevin Buzzard (Nov 16 2019 at 22:38):

But I don't care about this semiring

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.

Yury G. Kudryashov (Nov 16 2019 at 22:40):

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

Yury G. Kudryashov (Nov 16 2019 at 22:40):

Not sure if it'll work

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.

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.

Chris Hughes (Nov 16 2019 at 22:41):

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

Kevin Buzzard (Nov 16 2019 at 22:41):

Aah the penny is dropping

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?

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!

Yury G. Kudryashov (Nov 16 2019 at 22:43):

Look at algebra/group/type_tags

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

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

Reid Barton (Nov 16 2019 at 22:46):

is your original definition an instance?

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.

Reid Barton (Nov 16 2019 at 22:49):

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

Kevin Buzzard (Nov 16 2019 at 22:49):

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

Chris Hughes (Nov 16 2019 at 22:51):

I'm betting additive.add_comm_monoid

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.

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.

Kevin Buzzard (Nov 16 2019 at 22:58):

#1696

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.

Kevin Buzzard (Nov 16 2019 at 23:45):

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

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.

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

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

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?

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 }

Kevin Buzzard (Nov 17 2019 at 00:42):

gaargh I broke measure_theory/outer_measure

Kevin Buzzard (Nov 17 2019 at 00:49):

fixed

Kevin Buzzard (Nov 17 2019 at 00:53):

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

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.

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

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: Dec 20 2023 at 11:08 UTC