add_comm_monoid (set M)

Stream: maths

[Kevin Buzzard]

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]

PS is this there already?

[Johan Commelin]

I guess you are looking for algebra.pointwise?

[Johan Commelin]

Or where is that file?

[Johan Commelin]

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

[Kevin Buzzard]

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]

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

[Johan Commelin]

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]

gotcha

[Kevin Buzzard]

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]

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]

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

[Reid Barton]

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]

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]

no...

[Reid Barton]

very good

[Kevin Buzzard]

#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]

So what is the magic word?

[Reid Barton]

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

[Reid Barton]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

@Yury G. Kudryashov what am I doing wrong?

[Chris Hughes]

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]

I guess @Chris Hughes is right.

[Chris Hughes]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

Maybe if you mark pointwise_mul_comm_semiring as to_additive

[Kevin Buzzard]

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]

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

[Chris Hughes]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Yury G. Kudryashov]

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

[Kevin Buzzard]

right. There is no +

[Kevin Buzzard]

But I don't care about this semiring

[Kevin Buzzard]

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]

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

[Yury G. Kudryashov]

Not sure if it'll work

[Kevin Buzzard]

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]

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

[Chris Hughes]

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

[Kevin Buzzard]

Aah the penny is dropping

[Kevin Buzzard]

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]

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

There should be an equiv!

[Yury G. Kudryashov]

Look at algebra/group/type_tags

[Yury G. Kudryashov]

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]

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]

is your original definition an instance?

[Kevin Buzzard]

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

[Reid Barton]

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

[Kevin Buzzard]

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

[Chris Hughes]

I'm betting additive.add_comm_monoid

[Kevin Buzzard]

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

[Chris Hughes]

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]

#1696

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

gaargh I broke measure_theory/outer_measure

[Kevin Buzzard]

fixed

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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