Additive/multiplicative split in Lean 4

Stream: lean4

[Sebastian Ullrich]

Splitting this off from the OfNat thread in #general: reading that one made me wonder if a more local solution to the issue in the title has been considered so far, something in the veins of

class Monoid (α : Type) where
  neut : α
  op : α → α → α

namespace Additive

local instance [Monoid α] : OfNat α 0 where
  ofNat := Monoid.neut

local instance [Monoid α] : Add α where
  add := Monoid.op

end Additive

example [Monoid α] (x : α) : open Additive in (0 + x) = x + 0 := _

Granted, this doesn't currently seem to work, probably because the term open does not register the new instances... but eventually it should, I assume? @Leonardo de Moura

[Sebastian Ullrich]

Another missing ingredient here might be a binder variant of open that can be used with variable to avoid repetition

[Floris van Doorn]

Should local instance be scoped instance in your example?

[Floris van Doorn]

One problem is that we mix additive notation and multiplicative notation a lot in the same statement... Either on different types with two different monoids, or on the same type if we have a ring.

[Sebastian Ullrich]

Hah, that sure explains the failure! Thanks. OfNat still fails, but that's a detail...

[Sebastian Ullrich]

Floris van Doorn said:

One problem is that we mix additive notation and multiplicative notation a lot in the same statement... Either on different types with two different monoids, or on the same type if we have a ring.

Thanks, I feared so. In fact, my first approach was a custom macro that would be more selective in this regard

class Additive (α : Type) extends OfNat α 0, Add α

def Additive.ofMonoid [Monoid α] : Additive α where
  ofNat := Monoid.neut
  add   := Monoid.op

set_option quotPrecheck false in
notation "with_additive " α "; " e => let i : Additive α := Additive.ofMonoid; e

example [Monoid α] (x : α) : with_additive α; (0 + x) = x + 0 := _

[Sebastian Ullrich]

For rings and higher where there is no split, I assume there is no reason not to define the notation instances globally, just like in Lean 3

[Yury G. Kudryashov]

How do you suggest to combine additive group and multiplicative monoid instances into a ring?

[Sebastian Ullrich]

Do you have a problematic instance in mind? There are many possible definitions of Ring, but the simplest one would start with

class Ring (A : Type) where
  additive : Group A
  multiplicative : Monoid A

and then you would set these fields explicitly when constructing a specific ring. Note that for types with multiple monoidal/... structures, you would use the name of the "instance" (which should be a regular def in this case to avoid ambiguity) explicitly as well when accessing theorems. For example, if there exist Monoid.foo [Monoid A] ... and Nat.multiplicative : Monoid Nat, you could access the multiplicative instance via Nat.multiplicative.foo.

[Gabriel Ebner]

but the simplest one would start with

You're missing the distributivity axioms here. Practically speaking, Ring already extends two mixed additive/multiplicative structures: MonoidWithZero and Distrib. Also, further extending this kind of construction seems hard, you can't do class CommRing (A) extends Ring A, CommMonoid A anymore.

[Sebastian Ullrich]

Oh, I'm sure I'm missing many things here. But that the structure merging only works with parents and not with explicit fields is a good point, thanks.

[Gabriel Ebner]

The distributivity axioms are interesting because they mention both + and *, so they'd probably be annoying to state in the proposed Ring definition.

[Sebastian Ullrich]

I guess that depends on whether the hypothetical binder macro for activating the additive/multiplicative interpretation can also be used in class/structure. But, uh, that's getting a little too hypothetical.

[Sebastian Ullrich]

Just to get a better feeling for the issue at hand, do mathlib people even mind the split? Or is it something set up once with metaprogramming and then everyone forgets about it?

[Gabriel Ebner]

I think some people even like it.

[Sebastian Ullrich]

Haha, then I have no intention to change that

[Gabriel Ebner]

One thing that is still annoying is that we need to define class monoid and class add_monoid manually, because you can't programmatically declare structures in Lean 3. In Lean 4, we'll hopefully be able to say @[toAdditive] class Monoid.

[Kevin Buzzard]

When I arrived here I thought that treating multiplicative groups and additive groups as different objects was totally crazy because they're obviously the same and this just underlined how weirdly computer scientists thought about mathematics. Four years on I think it's a really insightful idea because it has shown me how mathematicians treat multiplication and addition as different objects in some kind of hierarchy that I didn't understand beforehand (which also contains the binary operators \bub and [x,y]).

Semirings are a natural example where a type has two monoid structures and our current solution works really well. A mathematician might in theory come along demanding that semirings with random different notation instead of + and * should exist but in practice nobody uses such a thing.

[Eric Wieser]

One thing I haven't seen mentioned before would be to generate additive and multiplicative definitions from a more abstract monoid definition. That might at least look less weird to outsiders, although maybe has little else going for it