## Stream: general

### Topic: bot_eq_zero_class

#### Violeta Hernández (Jun 02 2022 at 05:12):

I'm thinking about a potential new typeclass extending has_bot and has_zero with the single field bot_eq_zero : ⊥ = 0. Such a typeclass would allow us to state a few important theorems on the bottom element, such as ∀ x, ⊥ ≤ x, or max x ⊥ = x, in terms of zero, which is useful for rewriting. A nice consequence is that the lemma zero_le would no longer depend on the overpowered canonically_ordered_add_monoid class

#### Violeta Hernández (Jun 02 2022 at 05:13):

The particular application I'm thinking of are ordinals, which cannot be a canonically_ordered_add_monoid whilst still satisfying zero_le, but I would bet that there's a few others.

#### Violeta Hernández (Jun 02 2022 at 05:16):

I believe that this class, together with partial_order, has_add, and one of the covariant classes, should be enough to prove theorems like one_lt_two and such, which are currently gated behind the overpowered ordered_semiring class

#### Violeta Hernández (Jun 02 2022 at 05:16):

(these lemmas aren't even about multiplication! Why do they require it?)

#### Violeta Hernández (Jun 02 2022 at 05:21):

Well, one_lt_two and friends are true even when 0 isn't a bottom element, so I guess these new variants wouldn't obsolete the semiring ones

#### Violeta Hernández (Jun 02 2022 at 05:23):

I think a new zero_le_one_class + has_add + partial_order + some covariant class should be enough to prove these lemmas though

#### Violeta Hernández (Jun 02 2022 at 05:23):

So that's two proposals

#### Violeta Hernández (Jun 02 2022 at 05:26):

Oh and also, these same conditions would be enough to prove odd.pos

#### Violeta Hernández (Jun 02 2022 at 05:27):

As referenced in this other thread

#### Violeta Hernández (Jun 02 2022 at 05:45):

In fact! These lemmas about one_lt_two and such are all proven in terms of relatively weak typeclasses, with the sole exception of ordered_semiring

#### Violeta Hernández (Jun 02 2022 at 05:48):

Actually, the zero_le_one_class proposal seems simple and uncontroversial enough

#14510

#### Violeta Hernández (Jun 02 2022 at 06:01):

I wonder if a zero_lt_one_class might be useful too. That would lead to an even more general form of the numeric comparison lemmas that doesn't depend on multiplication (since zero_ne_one currently depends on mul_zero_one_class and nontrivial)

#### Violeta Hernández (Jun 02 2022 at 06:03):

The one example I can think of is pgame, which is not a mul_zero_one_class but still satisfies 1 < 2 and all these similar lemmas

#### Violeta Hernández (Jun 02 2022 at 06:03):

Again, I bet there's more

#### Violeta Hernández (Jun 02 2022 at 06:06):

That's three proposals

#### Violeta Hernández (Jun 02 2022 at 06:18):

Darn, it seems like my zero_le_one_class breaks dot notation on zero_le_one

No idea why

#### Violeta Hernández (Jun 02 2022 at 06:33):

Wait, what? This broke dot notation on one_le_two even though I didn't even tweak it

#### Violeta Hernández (Jun 02 2022 at 06:36):

I must have done something wrong

#### Anne Baanen (Jun 02 2022 at 12:57):

Dot notation is elaborated quite early on, so it is quite sensitive to typeclass issues. Probably redefining ordered_semiring meant that you get a (different) diamond issue, and the issue happens too early to be resolved by unfolding the (not yet found?) instances

#### Anne Baanen (Jun 02 2022 at 12:58):

This is a constant annoyance with my refactors too :(

#### Violeta Hernández (Jun 02 2022 at 15:47):

Is there any potential fix?

#### Violeta Hernández (Jun 02 2022 at 16:31):

Wonder if it would be better for zero_le_one class to take has_le as an argument rather than a field. Just a hunch though

#### Violeta Hernández (Jun 02 2022 at 16:31):

I don't really understand the difference between these two approaches

#### Violeta Hernández (Jun 02 2022 at 16:46):

Huh, this approach seems to have fixed the issue

It builds!

#### Violeta Hernández (Jun 03 2022 at 01:02):

Actually, since I'm not using this class to build the hierarchy, I think it might be a better idea to make it take has_zero and has_one as instance arguments

#### Violeta Hernández (Jun 03 2022 at 01:08):

To state zero_le_two, I need both add_zero_class and zero_le_one_class, and since add_zero_class extends has_zero and has_one I can't really take both without this

#### Eric Wieser (Jun 03 2022 at 07:14):

What instances do you have in mind for this new class?

#### Eric Wieser (Jun 03 2022 at 07:19):

Because if the only example you have is "ordinals", why not just make a non-commutative version of the existing typeclasses (i.e. pick the strongest typeclass you can)

#### Yaël Dillies (Jun 03 2022 at 07:47):

Also please don't touch canonically_ordered_whatever, I have a big refactor coming up and I suspect it will fix your problem.

#### Eric Wieser (Jun 03 2022 at 08:15):

I thought I'd come up with docs#submodule as an example of an instance, but it turns out that that's a canonically_ordered_add_monoid (#14529)

#### Damiano Testa (Jun 03 2022 at 08:32):

If you take with_bot of something with zero_le_one_class you should still obtain a zero_le_one_class, but canonically_ordered should not be preserved by the with_bot operation, right?

E.g. with_bot nat has zero_le_one_class, but is not canonically ordered, since docs#bot_eq_zero fails.

Note that with_bot nat is the target of docs#polynomial.degree.

#### Violeta Hernández (Jun 04 2022 at 05:55):

As for zero_le_one_class, I don't really have many examples, other than pgame and ordinal. I just find it a bit silly that:

• there's two classes linear_ordered_comm_monoid_with_zero and ordered_semiring with this assumption, yet only one gets to use the lemma in the root namespace zero_le_one.
• the assumptions for zero_le_two and one_le_two, which are laughably simple statements, are very overpowered.

#### Violeta Hernández (Jun 04 2022 at 05:57):

As for bot_eq_zero_class, I think that should be a much easier sell. There's all sorts of structures like that: natural numbers, non-negative reals, ordinals, cardinals, ...

#### Violeta Hernández (Jun 04 2022 at 06:04):

And I've seen a few certain lemmas, like x ≤ 0 ↔ x = 0 or ¬ x < 0 duplicated throughout these files

#### Violeta Hernández (Jun 04 2022 at 06:10):

I'm doing the zero_le_one_class PR first since bot_eq_zero_class would imply that other one, which I suspect may lead to a bit of extra golfing

#### Violeta Hernández (Jun 04 2022 at 06:11):

@Yaël Dillies I'm not really modifying the canonically_ordered_thing in my PR

#### Violeta Hernández (Jun 04 2022 at 06:12):

May I ask what your refactor is about? Wondering if it will magically fix my issues with ordinals

#### Yaël Dillies (Jun 04 2022 at 07:28):

Still I doubt you will need it once I'm done. My refactor is to create a canonical_order mixin (actually, two, one for addition and one for multiplication), and use that in place of canonically_ordered_..., some of which are missing and creating weirdness.

#### Yaël Dillies (Jun 04 2022 at 07:29):

Those would extend docs#has_exists_add_of_le and docs#has_exists_mul_of_le.

#### Violeta Hernández (Jun 04 2022 at 07:29):

You mean that I won't need canonical_order_thing, or that I won't need zero_le_one_class?

#### Violeta Hernández (Jun 04 2022 at 07:31):

And yeah, your PR seems like it would indeed fix a lot of the current ordinal weirdness!

#### Violeta Hernández (Jun 04 2022 at 07:31):

A huge problem right now is the fact that there's no such thing as a canonically ordered monoid without commutative addition

#### Eric Wieser (Jun 04 2022 at 07:44):

Is that actually a huge problem? I understand it would be nice to be able to use the same lemmas on ordinals and elsewhere; but this feels more like an "annoying papercut" rather than a "problem" that prevents things being formalized

#### Violeta Hernández (Jun 04 2022 at 07:47):

Yeah I might have been a bit hyperbolic, it's really an annoying papercut

#### Violeta Hernández (Jun 04 2022 at 07:47):

But it's one I'm glad to get rid of!

#### Violeta Hernández (Jun 04 2022 at 07:50):

Ordinals have been plagued with these papercuts for the longest time, though a few recent PRs have greatly alleviated the situation

#### Yaël Dillies (Jun 04 2022 at 08:03):

Note that your "sided distributivity" PR broke many rewrites in the sense that there now is a right_distrib_class ... gozl popping up.

#### Violeta Hernández (Jun 04 2022 at 08:06):

Was it really that many? Also, what's up with rw and adding typeclass goals?

#### Eric Wieser (Jun 04 2022 at 10:49):

Yaël Dillies said:

Note that your "sided distributivity" PR broke many rewrites in the sense that there now is a right_distrib_class ... gozl popping up.

Do you have an example of this? This was one of the things I was afraid of.

#### Violeta Hernández (Jun 04 2022 at 16:51):

I guess adding these classes to solve small problems isn't a net good after all :pensive:

#### Violeta Hernández (Jun 04 2022 at 17:02):

I still think bot_eq_zero_class is totally worth it, but given that what I have for zero_le_one_class are just small complaints, I'm not so sure about that one

#### Violeta Hernández (Jun 04 2022 at 17:03):

I'm not quite convinced that the distributivity refactor was a bad idea, though. I find it really surprising that ordinals are the only structure with one-sided distributivity we ever have to deal with. And though it did break a few rws, it wasn't that many either

#### Violeta Hernández (Jun 04 2022 at 17:07):

Do these extra classes actually cause a significant increase in compile time? Or is it just a few seconds and some random breakage here and there? Because if so, I think the sliver of extra convenience would still be a net gain

#### Violeta Hernández (Jun 04 2022 at 17:13):

I should mention that my plan with zero_le_one_class was to follow it up with a zero_lt_one_class. That's a new typeclass giving more potential trouble, but I think it's usefulness should be much more obvious. It would allow to generalize lemmas like 0 < 2 and such, which currently require semirings, even though they're lemmas purely about addition. Once again, I only have ordinal and pgame as examples, but I'm much more confident that there should exist structures without well behaved multiplication where comparing natural numbers still makes sense.

#### Violeta Hernández (Jun 04 2022 at 17:20):

I'm going to wait for feedback before following through with anything, because I don't really understand the negative consequences of these new typeclasses.

#### Yaël Dillies (Jun 04 2022 at 22:14):

Yaël Dillies said:

My refactor is to create a canonical_order mixin (actually, two, one for addition and one for multiplication), and use that in place of canonically_ordered_..., some of which are missing and creating weirdness.

First half in #14556.

#### Mario Carneiro (Jun 05 2022 at 01:52):

Violeta Hernández said:

Do these extra classes actually cause a significant increase in compile time? Or is it just a few seconds and some random breakage here and there? Because if so, I think the sliver of extra convenience would still be a net gain

I think the issue with new classes is not as much about compile time increase as it is about maintainability and general understandability of the library. Ideally we would like mathematicians to actually recognize the mathematics we are doing, and coming up with too many bespoke typeclasses makes things harder to untangle. It's a general problem with increasing abstraction, the code eventually becomes utterly unrecognizable on concrete use cases

#### Mario Carneiro (Jun 05 2022 at 01:55):

although the length of the spine of typeclasses is actually directly relevant to the performance of typeclass inference and elaboration thereafter: if you have A.to_C h before and add an intermediate typeclass B you now have A.to_B (B.to_C h) appearing everywhere instead, which is a bigger term that needs more time to typecheck, rewrite, and otherwise manipulate, in addition to the cost of the larger typeclass search that lead to that term in the first place

#### Violeta Hernández (Jun 05 2022 at 02:26):

I don't think any of the classes I'm proposing significantly increases the complexity of the typeclass hierarchy

#### Violeta Hernández (Jun 13 2022 at 02:13):

I'm thinking about the bot_eq_zero_class idea again

#### Violeta Hernández (Jun 13 2022 at 02:16):

I think that ideally, it would work something like this:

• the class takes in has_bot α and has_zero α, and has a single field bot_eq_zero : ⊥ = 0
• bot_eq_zero is made into a simp lemma
• we come up with some sort of attribute @[to_zero] (?) that can be added on a lemma involving ⊥ and turns it into a lemma on 0, with the same typeclass assumptions and attributes save for an extra bot_eq_zero typeclass assumption

#### Violeta Hernández (Jun 13 2022 at 02:16):

The first two points are super easy to implement, but I have no idea how to do the third one

#### Violeta Hernández (Jun 13 2022 at 02:17):

Although, surely it shouldn't be too hard to implement, we already have to_additive which is way more sophisticated

#### Violeta Hernández (Jun 13 2022 at 02:18):

We may also want to consider a "multiplicative" variant of this idea with a bot_eq_one_class, though that's way more niche I believe

#### Violeta Hernández (Jun 13 2022 at 02:19):

I believe ℕ+ is the only concrete example we have of something like this

#### Violeta Hernández (Jun 13 2022 at 02:20):

Can someone with metaprogramming experience tell me if this is a simple/good idea?

#### Violeta Hernández (Jun 13 2022 at 02:58):

Violeta Hernández said:

I believe ℕ+ is the only concrete example we have of something like this

Actually, on that topic, do we have any concrete example whatsoever of a docs#canonically_ordered_monoid?

#### Violeta Hernández (Jun 13 2022 at 02:59):

The docstring acknowledges that this is rare, and says that some duals of some objects have this property, but there don't seem to be any registered concrete instances

#### Patrick Massot (Jun 13 2022 at 08:41):

I didn't follow the conversation in this thread, but I just tried to bump mathlib in the sphere eversion project, and zero_le_two is now horribly broken. Minimized example:

import analysis.normed.group.basic

example {G : Type*} [normed_group G] (g : G) : (0 : ℝ) ≤ 2*∥g∥ :=
begin
apply mul_nonneg zero_le_two,
/-
type mismatch at application
mul_nonneg zero_le_two
term
zero_le_two
has type
0 ≤ 2
but is expected to have type
0 ≤ ?m_3
state:
G : Type ?,
_inst_1 : normed_group G,
g : G
⊢ 0 ≤ 2 * ∥g∥
-/
sorry
end


This used to work flawlessly. I know how to fix my proof, but I find it really sad.

#### Patrick Massot (Jun 13 2022 at 08:44):

And next build error is about zero_le_one...

#### Yaël Dillies (Jun 13 2022 at 08:44):

Just so that it is written somewhere, I thought we agreed the plan was to not introduce zero_le_one_class until we made the canonical_add_order mixin I was talking about (#14556 and then a PR I have yet to write), and then see whether we even needed it anymore.

#### Yaël Dillies (Jun 13 2022 at 08:45):

So I am more than happy to revert #14510.

#### Patrick Massot (Jun 13 2022 at 08:46):

Fixing the sphere eversion project is rather time consuming so I would prefer if we don't oscillate too much.

#### Yaël Dillies (Jun 13 2022 at 08:47):

Well yeah I'm sorry I wasn't the one hitting merge on #14510.

#### Patrick Massot (Jun 13 2022 at 08:48):

I builds now. It turns out that everything needed was related to either zero_le_one/zero_le_two or set.finite now being protected (I guess this is a side effect of Kyle's work but I have no idea why).

#### Ruben Van de Velde (Jun 13 2022 at 09:08):

refine instead of apply works in your mwe

#### Violeta Hernández (Jun 22 2022 at 06:15):

Ok so... my plan was to follow up the zero_le_one_class PR with a zero_lt_one_class PR, but seeing how controversial that last one is, I'd like to put it on the table first

#### Violeta Hernández (Jun 22 2022 at 06:16):

The main benefit of such a typeclass is that it allows us to generalize lemmas like 0 < 2 or 1 < 2, which right now have the somewhat overpowered assumption of a nontrivial ordered semiring (these lemmas aren't even about multiplication!)

#### Violeta Hernández (Jun 22 2022 at 06:17):

There's also this note on docs#zero_lt_one' about how norm_num can only use 0 < 1 for the even stronger case of a linear ordered semiring, so such a class seems like it could be useful there too

#### Violeta Hernández (Jun 22 2022 at 06:19):

As for concrete types that would benefit from this, I have ordinal and game. The typeclass could be defined on some with_top and with_bot types, though the numeric comparison lemmas wouldn't apply. I'm out of examples but hopeful there's a few more

#### Violeta Hernández (Jun 22 2022 at 06:24):

One of the main complaints of the last refactor was random breakage due to typeclass inference. That could be remedied by just making the type argument explicit on all these lemmas. That would add a few extra characters throughout mathlib, but it would also get rid of the dozens of instances of @zero_lt_two α _ _ and such.

#### Violeta Hernández (Jun 22 2022 at 06:55):

Oh! This instance can also be defined on every linearly ordered commutative group with zero, surely that leads to extra uses?

#### Violeta Hernández (Jun 22 2022 at 06:56):

There's also the example of onote though that's admittedly really niche

#### Yuyang Zhao (Nov 10 2022 at 12:58):

I'm working on generalizing lemmas like zero_ne_one and zero_lt_one by reducing their typeclass assumptions to docs#ne_zero, docs#zero_le_one_class, and docs#partial_order (no new typeclasses are introduced). This also needs to fix a lot of @zero_lt_two α _ _.
Before finishing it I would like to ask if there are any more suggestions.

#### Yaël Dillies (Nov 10 2022 at 13:15):

What new types does it apply to?

#### Yuyang Zhao (Nov 10 2022 at 13:35):

lemma zero_lt_one [has_zero α] [has_one α] [partial_order α]
[zero_le_one_class α] [ne_zero (1 : α)] : (0 : α) < 1

lemma zero_lt_two [has_one α] [add_zero_class α] [partial_order α]
[zero_le_one_class α] [ne_zero (1 : α)] [covariant_class α α (+) (≤)] : (0 : α) < 2


#### Eric Wieser (Nov 10 2022 at 14:00):

@Yaël Dillies's question is about what α you forsee this generalization being useful for

#### Eric Wieser (Nov 10 2022 at 14:53):

Doesn't docs#zero_lt_one already work for part_enat?

#### Yuyang Zhao (Nov 10 2022 at 14:58):

There is no multiplication for part_enat.

#### Yuyang Zhao (Nov 10 2022 at 15:59):

Here is the PR #17465

#### Alex J. Best (Nov 10 2022 at 16:08):

If you define 0* infty = 0 I think that makes enat an ordered_semiring though, so zero_lt_one should in principle apply.

#### Alex J. Best (Nov 10 2022 at 16:13):

Indeed enat is already a canonically_ordered_comm_semiring, do we have a good reason for not doing the same with part_enat

#### Eric Wieser (Nov 11 2022 at 02:07):

I think the reason simply that no one cares much about part_enat

#### Kevin Buzzard (Nov 11 2022 at 08:01):

docs#part_enat I've never even heard of it

#### Kevin Buzzard (Nov 11 2022 at 08:04):

Yeah ok it's constructive enat. Good luck using that. I remember the same thing with ereal, which I made once (reals and +- infinity). I defined neg but was scared to define add because I didn't know what -infty + infty was. Later on I realised I should probably have just made a random decision.

#### Andrew Yang (Nov 11 2022 at 08:07):

It was the old enat until a month ago when it was renamed and replaced by enat := with_top nat.

#### Kevin Buzzard (Nov 11 2022 at 08:10):

Yeah old enat I'm only too familiar with :-(

#### Sebastien Gouezel (Nov 11 2022 at 10:31):

Kevin Buzzard said:

Yeah ok it's constructive enat. Good luck using that. I remember the same thing with ereal, which I made once (reals and +- infinity). I defined neg but was scared to define add because I didn't know what -infty + infty was. Later on I realised I should probably have just made a random decision.

Since then, we have made a decision on what -infty + infty. It's +infty now. And unfortunately it's the bad convention. Indeed, 0 * infty should absolutely by 0 in ennreal (this is really important in measure theory), and you really want log and exp between ennreal and ereal to respect the operations. Yet another refactor that will have to de done some day...

#### Kevin Buzzard (Nov 11 2022 at 11:25):

Oh wow I hadn't expected someone to come up with a plausible argument for one convention being better!

#### Sebastien Gouezel (Nov 11 2022 at 11:27):

This even came up in a concrete application (where entropy does not behave well on the empty space unless you have the good convention on ereal).

#### Eric Wieser (Nov 11 2022 at 13:17):

I assume your claim is that it should be -infty + infty = 0?

#### Kevin Buzzard (Nov 11 2022 at 13:21):

The idea is that exp is an isomorphism between ereal and ennreal, with log as the inverse. So if 0 * infty = 0 in ennreal (which is mathematically useful) then -infty + infty = -infty should be true in ereal.

#### Yuyang Zhao (Nov 11 2022 at 15:27):

I split the generalization of zero_ne_one and made PR #17477. However algebra/ne_zero is ported to mathlib4. Can anyone give me access? My github name is negiizhao.

#### Scott Morrison (Nov 11 2022 at 22:11):

(invitation sent, following a request elsewhere)

Last updated: Dec 20 2023 at 11:08 UTC