nameclash: add_idem already exists

Stream: mathlib4

[Pieter Cuijpers]

I'm introducing AddIdemQuantale to define idempotent additive quantales and try to follow what is standard in other parts of the library. I first define the class:

class AddIdemQuantale (α : Type*) extends AddQuantale α where
  /- addition is idempotent in an idempotent quantale -/
  protected add_idem (x : α) : x + x = x

And after that, I try to make the add_item theorem available:

section AddIdemQuantale
variable (α : Type _)
variable [IdemQuantale α]

theorem add_idem : ∀ x : α, x + x = x := IdemQuantale.add_idem

end AddIdemQuantale

But now, continuous integration complains, because add_idem is also defined in Algebra.Order.Kleene (on IdemSemirings).

What is the best way to go about such a clash?

[Eric Wieser]

One option would be to add an IdemAddCommMonoid class, and change IdemSemiring and your class to extend it

[Eric Wieser]

Another would be to change add_idem to assume Std.IsIdempotent instead

[Yaël Dillies]

I think the AddIdemCommMonoid solution is the best

[Eric Wieser]

I fear that Pieter also wants IsdemAddCommGroup or more

[Pieter Cuijpers]

I would propose to extend Algebra.Groups.Defs with AddIdemSemigroup and IdemSemigroup and work from there.
Not sure yet how many of the combined variants would come in, but it may indeed build up a bit.

[Yaël Dillies]

I would suggest not putting them in Algebra.Group.Defs as then the majority of the library, not needing them, won't import them

[Eric Wieser]

Pieter, in your context is the stronger a + b = a ⊔ b requirement that IdemSemiring uses ok?

[Pieter Cuijpers]

Not exactly, but... an alternative definition for quantales in general is:

A quantale, or complete dioid, Q, is a dioid in which the underlying sup-semilattice has arbitrary suprema over which the multiplication distributes.

with dioid simply being another word for semiring... so maybe taking a different starting point for the definition may solve the issue. However, it may lead to notational confusion as well.

If I view a quantale as a semigroup combined with a complete lattice, which is the more usual view, either the $+$ or $*$ can be used to denote the semigroup, and $\sqcup$ is used for the lattice. When presented as a semiring, I would be forced to write $*$ for the semigroup and use $+$ for the join.

[Pieter Cuijpers]

(How do you manage to write the \sqcup in this: a + b = a ⊔ b? I can only do it by copy-paste now... Newbie...)

[Yaël Dillies]

Type \sup in vscode

[Pieter Cuijpers]

Ah, that's not what I meant. I meant within Zulip. The webinterface eludes me on how to write this.

[Pieter Cuijpers]

Yaël Dillies said:

I would suggest not putting them in Algebra.Group.Defs as then the majority of the library, not needing them, won't import them

What would be a good place? Make a separate file on idempotence Algebra.Group.Idem or so?

[Pieter Cuijpers]

Eric Wieser said:

Pieter, in your context is the stronger a + b = a ⊔ b requirement that IdemSemiring uses ok?

I'm trying to go by the first approach, extending the definition of IdemSemiring, but I have trouble with the original definition. It goes like this:

/-- An idempotent semiring is a semiring with the additional property that addition is idempotent.
-/
class IdemSemiring (α : Type u) extends Semiring α, SemilatticeSup α where
  protected sup := (· + ·)
  protected add_eq_sup : ∀ a b : α, a + b = a ⊔ b := by
    intros
    rfl
  /-- The bottom element of an idempotent semiring: `0` by default -/
  protected bot : α := 0
  protected bot_le : ∀ a, bot ≤ a

Thing is... the definition never explicitly mentions idempotence? Instead it mentions a SemilatticeSup?
From the textual description, I would have expected something along the lines of:

class IdemSemiring (α : Type u) extends Semiring α where
   add_idem (x : α) : x + x = x

and subsequently a theorem saying
instance [IdemSemiring α] : SemilatticeSup α

@Yaël Dillies am I missing something here? Do you know why the original definition is the way it is?

[Yaël Dillies]

Eric Wieser said:

Pieter, in your context is the stronger a + b = a ⊔ b requirement that IdemSemiring uses ok?

That's what Eric was trying to get you to understand with this :point_of_information: message: There are several definitions of idempotence

[Yaël Dillies]

An idempotent semiring assumes that addition is the same as supremum, so in particular it is idempotent (a + a = a ⊔ a = a). Your idempotency requirement seems to just be a + a = a, with no mention of an order. There is a mismatch

[Pieter Cuijpers]

From what I've been reading in some papers at least, an idempotent semiring is usually defined as "a semiring with and idempotent addition", just like the comment says in the Mathlib definition. No assumptions regarding any ordering are made. Instead, given that definition, literature usually argues that one can define a natural/canonical order on idempotent semirings through $x \leq y$ iff $x + y = y$, in which case $+$ coincides with $sup$. Reversely, it can then be shown that any idempotent semiring can only be ordered in this way if one wants both + and * to be order preserving, and so an idempotent semiring can also be thought of as a semiring on a Sup-semilattice with + defined as sup. This latter viewpoint was apparently taken as a definition Mathlib, rather than being a result.

I don't see an actual mismatch, really, just a different starting point. In fact, the quantales that I'm defining can also be described as:

class Quantale extends IdemSemiring, CompleteLattice

But an additive quantale AddQuantale could not be defined in the same way unless we introduce AddIdemSemiring (i.e. a semiring in which * and + are reversed).

The solution of the AddIdemCommMonoid class (or similar) still seems best. I'll try to make that work.

[Pieter Cuijpers]

Eric Wieser said:

One option would be to add an IdemAddCommMonoid class, and change IdemSemiring and your class to extend it

Okay... so I'm trying this out, and now run into the next thing...
If I extend IdemSemiring like this:

class AddIdemSemigroup (G : Type _) extends AddSemigroup G where
  protected add_idem : ∀ x : G, x + x = x

class IdemSemiring (α : Type u) extends Semiring α, SemilatticeSup α, AddIdemSemigroup α where
  protected le a b := a + b = b
  protected sup := (· + ·)
  protected add_eq_sup : ∀ a b : α, a + b = a ⊔ b := by
    intros
    rfl
  /-- The bottom element of an idempotent semiring: `0` by default -/
  protected bot : α := 0
  protected bot_le : ∀ a, bot ≤ a

then I will have to add the add_idem field everytime an instance of IdemSemiring is being made.
There is a default solution, which comes down to applying add_eq_sup and sup_idem, but I don't know
how to add this in such a way that I don't need to change anything downstream anymore. (It seems there
is a lot of theory already built on IdemSemiring, so I'm getting in a bit of a mess for my first PR...)

Other solution would be to give up on the desire to have both Quantale and AddQuantale, but that sounds like creating problems in the future.

[Jireh Loreaux]

Pieter Cuijpers said:

This latter viewpoint was apparently taken as a definition Mathlib, rather than being a result.

This is because you generally don't want to define instances that build new data from existing instances. It can pretty easily lead to diamonds.

[Eric Wieser]

Pieter Cuijpers said:

then I will have to add the add_idem field everytime an instance of IdemSemiring is being made.

You can resolve this by not extending AddIdemSemigroup , and writing a IdemSemiring.toAddIdemSemigroup instance manually.

[Pieter Cuijpers]

Jireh Loreaux said:

Pieter Cuijpers said:

This latter viewpoint was apparently taken as a definition Mathlib, rather than being a result.

This is because you generally don't want to define instances that build new data from existing instances. It can pretty easily lead to diamonds.

Thanks. I need to chew on that one a bit, I think. Is there a book or videolecture that goes into this a bit more?

[Jireh Loreaux]

#mil

[Jireh Loreaux]

specifically: https://leanprover-community.github.io/mathematics_in_lean/C07_Hierarchies.html#basics

But the diamond we created with modules is definitely bad. The offending piece is the smul field which is data, not a proof, and we have two constructions that are not definitionally equal. The robust way of fixing this issue is to make sure that going from a rich structure to a poor structure is always done by forgetting data, not by defining data. This well-known pattern as been named “forgetful inheritance” and extensively discussed in https://inria.hal.science/hal-02463336.

Although there is much more in this section worth reading (and the rest of the book!)

[Jireh Loreaux]

Also: @Pieter Cuijpers I'm worried that the discussion of quantales is too disjointed. I've seen several threads about your issues on Zulip, not to mention your PR and the back-and-forth we've had there. I think you need a single thread in which we converge on the correct design, as well as the correct prerequisites. A key thing to understand in formalization is that proofs are easy, definitions are hard. So getting the right definition(s) of quantales is important to make later use as straightforward as possible.

[Yaël Dillies]

Jireh Loreaux said:

proofs are easy, definitions are hard

:raised_hand: Combinatorics would like to object :grinning: But more seriously, yes I agree with Jireh that you should stop fragmenting the discussion. In fact, if someone could merge all the threads together in one thread called "Quantales" under #maths, that would be great.

[Pieter Cuijpers]

Agreed. I'm not proficient enough on Zulip yet to comply to the merge request, but if someone can do it or show me how, let's go.

[Jireh Loreaux]

@Pieter Cuijpers , if you provide links here to all the threads, and then ping me, I can try to do something appropriate later.

[Pieter Cuijpers]

@Jireh Loreaux Thanks for the offer!

There are four threads that I recently started to get help related to my efforts to formalize the Quantale definitions.

The first one, I used to ask for help on to_additive, after I couldn't find out how to use it from reading example code on semigroups. (I'm not sure if that would belong in a "Quantale" group, as it is more about how to use to_additive.)
#mathlib4 > to_additive gives error "can't transport XYZ to itself"

The second one also came up in the use of to_additive, because I felt uncertain about adding anything to a part of the library that I'm really not involved in developing. Turns out that would be okay. (Again, I feel this has nothing to do with Quantales really, and therefore it was okay for it to have its own thread. Maybe I should not have mentioned what I was working on, but I felt that may be relevant context for the answer.)
#mathlib4 > adding items to fixAbbreviation in to_additive

The third may actually be more important for the Quantale definition than I originally figured. I thought it would be a more generic question about semigroups, but perhaps the context is more important. I figured I needed to understand how to define an idempotent semigroup, and based on that would define an idempotent quantale in a similar manner. As it turns out, the choice becomes more whether I should use a parameterized definition of quantale and then indeed have a definition of idempotent semigroup, or have a definition of idempotent quantale (perhaps even without having a def. of idempotent semigroup). As I'm not completely decided on this yet, a discussion in the "Quantale" topic would be good.
#mathlib4 > Two ways of defining an idempotent semigroup

The last one is derived from this. I added it because, while working on the idempotent semigroup, I discovered a dependency with kleene algebras. Ultimately, we worked out that it is probably best to replace the lemma in the kleene algebra file with a lemma that proves that and idempotent semiring is an instance of an idempotent semigroup, replacing the lemma that is currently there (and says exactly the same). I also got that to work fine, but if we go for a parameterized quantale definition, it should probably be done in a separate PR, while if we go for an integrated quantale definition, it may be done in this PR.
#mathlib4 > nameclash: add_idem already exists

I hope this gives you enough information.