IsBotZeroClass

Stream: mathlib4

[Violeta Hernández]

I recall having brought this up back in 2022 or so. But I'd like to bring it up again, because it keeps pestering me.

Mathlib does not currently have a typeclass to express that the bottom element of a type and its zero element are equal. The closest thing we have is docs#CanonicallyOrderedAdd, which is a relatively minimal, somewhat common typeclass that implies it. Multiple order structures with the ⊥ = 0 property such as ℕ, Ordinal, or Cardinal, do satisfy the canonically ordered add typeclass.

There are various convenience lemmas that are gated behind this typeclass. The basic examples would be docs#zero_le, docs#LT.lt.pos, docs#eq_zero_or_pos, docs#le_self_add and docs#le_add_self, docs#le_add_of_le_left and docs#le_add_of_le_right. There's also some more "advanced" examples, such as docs#List.sum_eq_zero_iff or docs#Finsupp.Lex.wellFoundedLT.

However, working within the combinatorial-games repository, there are various structures that satisfy ⊥ = 0 but not this predicate. The main one would be NatOrdinal. Although it's just a type alias for Ordinal, it has completely different (and quite interesting) arithmetic. In fact, it's a strictly ordered semiring with ⊥ = 0, which means all the aforementioned convenience lemmas apply to it, even though they all have to be reproved, since it is not CanonicallyOrderedAdd (e.g. there's no x with ω = 1 + x).

There's also Nimber, which is another mathematically interesting type alias of Ordinal. Its order is quite borked up with respect to its arithmetic, which means it only satisfies the direct consequences of ⊥ = 0, though it's still a bit annoying having to reprove all of them. The same applies to Nimber[X], which the repository endows with a lexicographic order structure, which is quite important for the simplest extension theorems.

The problems I describe still apply to some extent to Ordinal itself. Since ordinal addition isn't commutative, it gets cut off (in a seemingly arbitrarily way) from about half of the CanonicallyOrderedAdd API. For instance, ordinals satisfy both a ≤ a + b and a ≤ b + a, but the latter (docs#le_add_self) is proven assuming commutativity from the former.

My proposal is to create the following typeclass:

class IsBotZero [LE α] [Zero α] (α : Type*) : Prop where
  isBot_zero : IsBot (0 : α)

This would allow many of the theorems currently stated with CanonicallyOrderedAdd to be stated in terms of even weaker assumptions. Some combination of IsBotZero + AddZeroClass + AddLeftMono + AddRightMono should be sufficient for a large portion of these theorems, and would apply to my cases. We could then show (via a low-priority instance) that CanonicallyOrderedAdd + AddZeroClass → IsBotZero.

[Violeta Hernández]

The blocker last time I tried this was whether docs#bot_eq_zero should be a simp lemma. The thing is, not all types with the ⊥ = 0 property prefer the 0 spelling, with a notable counterexample being ideals over a semiring (see docs#Ideal.zero_eq_bot). I think we can keep the current design, where the base lemma is not made simp, whereas the specialization docs#bot_eq_zero' to linearly ordered monoids is.

[Aaron Liu]

Probably don't assume Bot

[Yaël Dillies]

Violeta Hernández said:

it only satisfies the direct consequences of ⊥ = 0

What lemmas are we talking about?

[Violeta Hernández]

Yaël Dillies said:

Violeta Hernández said:

it only satisfies the direct consequences of ⊥ = 0

What lemmas are we talking about?

0 ≤ x, x < y → 0 < y, x = 0 ∨ 0 < x, those are the main three.

[Violeta Hernández]

Though I'd also like to call out docs#Finsupp.Lex.wellFoundedLT which truly only needs ⊥ = 0 (as the primed version above it shows).

[Yaël Dillies]

Is this really that painful to have three extra lemmas Nimber.zero_le, Nimber.pos_of_lt, Nimber.eq_zero_or_pos?

[Yaël Dillies]

Violeta Hernández said:

Though I'd also like to call out docs#Finsupp.Lex.wellFoundedLT which truly only needs ⊥ = 0 (as the primed version above it shows).

About this, you might be interested in the proposal Sky and I have had for a few years of decoupling Finsupp from Zero, since there are some use cases where we would instead want the support according to 1, or the support according to ⊥

[Yaël Dillies]

Until recently it was difficult to actually implement this proposal, but now we have clearly-separated files for the "data properties" vs algebraic properties of Finsupp

[Violeta Hernández]

Yaël Dillies said:

Is this really that painful to have three extra lemmas Nimber.zero_le, Nimber.pos_of_lt, Nimber.eq_zero_or_pos?

It's not, but it is a slight inconvenience piled up on the other larger inconveniences I mentioned. (Note also that we can't enable dot notation on Nimber.pos_of_lt in the same way as with LT.lt.pos).

[Jireh Loreaux]

I'm not sure if this works, but can you do Nimber.LT.lt.pos and then when you open Nimber you can use it for dot notation?

[Violeta Hernández]

Yaël Dillies said:

Violeta Hernández said:

Though I'd also like to call out docs#Finsupp.Lex.wellFoundedLT which truly only needs ⊥ = 0 (as the primed version above it shows).

About this, you might be interested in the proposal Sky and I have had for a few years of decoupling Finsupp from Zero, since there are some use cases where we would instead want the support according to 1, or the support according to ⊥

I think said proposal is quite reasonable, but I do worry that in my particular case it might create two different ways to spell the same thing (finsupp with ⊥, finsupp with 0)

[Violeta Hernández]

Jireh Loreaux said:

I'm not sure if this works, but can you do Nimber.LT.lt.pos and then when you open Nimber you can use it for dot notation?

No, this doesn't work.

import Mathlib

def Nimber' := Ordinal
instance : Zero Nimber' := inferInstanceAs (Zero Ordinal)
instance : LT Nimber' := inferInstanceAs (LT Ordinal)

theorem Nimber'.LT.lt.pos {x y : Nimber'} (h : x < y) : 0 < y := pos_of_gt (α := Ordinal) h

open Nimber'

 -- failed to synthesize AddZeroClass Nimber'
example {x y : Nimber'} (h : x < y) : 0 < y := h.pos

[Yaël Dillies]

Violeta Hernández said:

I do worry that in my particular case it might create two different ways to spell the same thing (finsupp with ⊥, finsupp with 0)

My idea is that they will be defeq, so you needn't worry

[Violeta Hernández]

Fair enough!

[Violeta Hernández]

I do still think that the List.sum theorems (e.g. docs#List.le_sum_of_mem, docs#List.sum_eq_zero_iff) assuming commutativity are quite unfortunate. Working with the Cantor normal form I've had to use List.sum precisely because it allows for noncommutative sums. and the only reason these theorems assume commutativity is for the same reason a ≤ b + a does.

[Aaron Liu]

maybe CanonicallyOrderedAdd should also have an le_add_self field

[Violeta Hernández]

That seems like a reasonable middle-ground solution. Looking through the instances of docs#CanonicallyOrderedAdd it seems like Ordinal is the only one without commutative addition.

[Violeta Hernández]

On a tangentially related note... why do we have both docs#le_self_add and docs#self_le_add_right ?

[Violeta Hernández]

The only difference is the former has explicit arguments

[Violeta Hernández]

Notably, neither of these match docs#Nat.le_add_right or docs#Multiset.le_add_right

[Violeta Hernández]

PR is ready! Surprised by how smoothly it went. #29084