0🔶 ("zero diamond")

Stream: mathlib4

[Gabriel Ebner]

In his last week here in Amsterdam, Aurélien ran into an exciting diamond in the algebra type classes.

As you probably know, Lean 4 introduced in the OfNat α n type class with an ofNat : α member. This type class is used to elaborate the numeral n, if you write 0 then you get e.g. OfNat.ofNat 0. This type class only allows us to embed one single specific numeral n. Typically we want a function Nat → α (cf nat.cast in mathlib3), so we define Numeric α := ∀ n, OfNat α n.

However currently mathlib4 also contains a Zero type class ported from mathlib3, and e.g. AddMonoid extends Zero. This means that there are two non-defeq ways to write 0 in a ring: OfNat.ofNat 0 and Zero.zero. (Since a ring should both have an embedding Nat → R as well as a zero from the monoid).

I can think of some solutions, but all of them have some downsides.

1. Make AddMonoid extend Numeric. But then there are AddMonoid instances which are isomorphic (as monoids) but not equal (in Lean).
2. Adopt the convention that the zero field is always defeq to ofNat 0 for concrete instances. This means that Ring no longer extends AddMonoid, instead we need to write the instance manually.
3. Learn to live with the diamond, so far it wasn't outrageously painful in mathlib4.

[Gabriel Ebner]

After writing this up, I think option 2 is actually pretty okay. Any opinions?

[Mario Carneiro]

Why would Ring not be able to extend AddMonoid?

[Gabriel Ebner]

By "extend" I mean extend. Because then Ring would have two fields: zero and ofNat. And no guarantee that zero and ofNat 0 are defeq.

[Mario Carneiro]

For general rings, this is true, but it could have both fields and an equality proof

[Gabriel Ebner]

With the equality proof you get a diamond. That is, you could have R : Type, inst : Ring R ⊢ 0 = 0 which is not provable by rfl.

[Gabriel Ebner]

https://github.com/leanprover-community/mathlib4/pull/72
The main downside is that we get a bit of duplication. That is, the fields of AddGroup, etc., are duplicated in Ring. But otherwise this works quite nicely, it could replace a few proofs by rfl.

[Johan Commelin]

Can't Zero be effectively replaced by OfNat _ 0?

[Gabriel Ebner]

Unfortunately no. The reason is that this doesn't work:

class A (n : Nat) where
  a : String

class B extends A 1, A 2

Here B will only extend A 1 and not A 2. Now set B := MonoidWithZero and A := OfNat.

[Jakob von Raumer]

Sebastian and me had a similar problem in our Lean class (boolean equality of decidable equality of products versus boolean equality of products of types with decidable equality), and we solved it with a further type class equating the two...

[Gabriel Ebner]

@Jakob von Raumer That's the standard approach we take for diamonds, never defining fields in term of each other and always include proofs that they are equal instead. (The typical example in mathlib is the topology of product spaces: the topology induced by the product metric is not defeq to the product of the topologies induced by the metrics). However this rule is precisely what we're not doing here.

The difference is that concrete instances of 0 and 0 are always supposed to be defeq (in contrast to the product example where the two topologies are not defeq). Therefore we define 0 in terms of 0 instead of adding a proof that 0 = 0.