## Stream: maths

#### 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}⟩

⟨λ X Y, {z | ∃ (x ∈ X) (y ∈ Y), z = x + y}⟩

(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) :
zero := (0),
}

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

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

no...

very good

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

#where -- namespace set

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
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
term
has type
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: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
state:
α : Type u_1,


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

#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) :
zero := (0),
}


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 :=
zero := ...,


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

gaargh I broke measure_theory/outer_measure

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: May 19 2021 at 02:10 UTC