bot_eq_zero_class

Stream: general

[Violeta Hernández]

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]

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]

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]

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

[Violeta Hernández]

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]

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]

So that's two proposals

[Violeta Hernández]

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

[Violeta Hernández]

As referenced in this other thread

[Violeta Hernández]

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]

Actually, the zero_le_one_class proposal seems simple and uncontroversial enough

[Violeta Hernández]

#14510

[Violeta Hernández]

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]

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]

Again, I bet there's more

[Violeta Hernández]

That's three proposals

[Violeta Hernández]

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

[Violeta Hernández]

No idea why

[Violeta Hernández]

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

[Violeta Hernández]

I must have done something wrong

[Anne Baanen]

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]

This is a constant annoyance with my refactors too :(

[Violeta Hernández]

Is there any potential fix?

[Violeta Hernández]

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]

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

[Violeta Hernández]

Huh, this approach seems to have fixed the issue

[Violeta Hernández]

It builds!

[Violeta Hernández]

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]

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]

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

[Eric Wieser]

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]

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]

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]

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]

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]

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]

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

[Violeta Hernández]

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]

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

[Violeta Hernández]

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

[Yaël Dillies]

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]

Those would extend docs#has_exists_add_of_le and docs#has_exists_mul_of_le.

[Violeta Hernández]

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

[Violeta Hernández]

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

[Violeta Hernández]

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

[Eric Wieser]

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]

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

[Violeta Hernández]

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

[Violeta Hernández]

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

[Yaël Dillies]

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]

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

[Eric Wieser]

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]

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

[Violeta Hernández]

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]

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]

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]

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]

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]

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]

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]

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]

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

[Violeta Hernández]

I'm thinking about the bot_eq_zero_class idea again

[Violeta Hernández]

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]

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

[Violeta Hernández]

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

[Violeta Hernández]

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]

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

[Violeta Hernández]

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

[Violeta Hernández]

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]

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]

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]

And next build error is about zero_le_one...

[Yaël Dillies]

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]

So I am more than happy to revert #14510.

[Patrick Massot]

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

[Yaël Dillies]

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

[Patrick Massot]

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]

refine instead of apply works in your mwe

[Violeta Hernández]

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]

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]

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]

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]

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]

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

[Violeta Hernández]

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

[Yuyang Zhao]

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]

What new types does it apply to?

[Yuyang Zhao]

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]

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

[Yuyang Zhao]

It generalizes docs#ordinal.zero_lt_one, docs#cardinal.zero_lt_one, docs#zero_lt_one₀, and docs#part_enat.zero_lt_one.

[Eric Wieser]

Doesn't docs#zero_lt_one already work for part_enat?

[Yuyang Zhao]

There is no multiplication for part_enat.

[Yuyang Zhao]

Here is the PR #17465

[Alex J. Best]

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]

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]

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

[Kevin Buzzard]

docs#part_enat I've never even heard of it

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Sebastien Gouezel]

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]

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

[Sebastien Gouezel]

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]

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

[Kevin Buzzard]

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]

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]

(invitation sent, following a request elsewhere)