odd_gt_zero

Stream: general

[Michael Stoll]

There is docs#nat.odd_gt_zero, which defies naming conventions. (I was looking for something containing pos or perhaps zero_lt.) It would also be nice to have the same statement with the assumption n % 2 = 1 instead of odd n.
It looks like it is not used anywhere in mathlib right now and otherwise only once (in archive/imo/imo1998_q2.lean).
I'd suggest to rename it nat.odd_pos (and add nat.odd_pos' for the variant).

[Alex J. Best]

Oh yeah I started doing this a while back and forgot about it #13040, I'll try and get this merged now lol. Then you can add the variant you want separately if you like.

[Michael Stoll]

OK, sounds good.

[Yaël Dillies]

Actually, you can generalize it quite a bit.

[Violeta Hernández]

Agree with odd_pos

[Ruben Van de Velde]

Can't we do odd.pos for canonically ordered monoids it something?

[Violeta Hernández]

This might be a bit of an offhand comment, but I feel like there should be something more general than canonically ordered monoids for which many of the order results still hold true, including this one

[Violeta Hernández]

I recently ran into the problem of ordinals not being a canonically ordered monoid, just because of the technicality that addition isn't commutative

[Violeta Hernández]

odd.pos would still hold true for ordinals, though

[Mario Carneiro]

ordinals are rather odd as an algebraic structure though. Cardinals too

[Mario Carneiro]

I generally try to avoid introducing a new weak algebraic structure if there is only one example

[Mario Carneiro]

even defining what it means to be an "odd ordinal" is a bit subtle and the definition that works for ordinals isn't necessarily the most natural or correct in other situations

[Mario Carneiro]

and "odd cardinal" is all sorts of broken

[Violeta Hernández]

That's fair

[Violeta Hernández]

Yeah actually, odd and even ordinals would be quite broken under the current definition

[Violeta Hernández]

ω + 1 is both even as (ω + 1) + (ω + 1), and odd as 2 * ω + 1

[Violeta Hernández]

Nevermind my remark then

[Mario Carneiro]

the "correct" definition for ordinals is that an ordinal is odd if its finite part is odd, or equivalently it has the form o * 2 + 1

[Mario Carneiro]

hm, actually you're right, that "or equivalently" definition doesn't work since (ω + 1) * 2 = ω * 2 + 1. I think it works if you use o.nmul 2

[Violeta Hernández]

Ordinals with natural operations aren't canonically ordered though, since there's no ordinal with 1 nadd o = ω

[Violeta Hernández]

Being canonically ordered feels like too strong of a property to state some of the order results like 0 ≤ x and this one, but I don't know what the appropriate generalization would be

[Mario Carneiro]

I mean it's basically just zero_le_order

[Violeta Hernández]

Wait, that's a typeclass?

[Mario Carneiro]

I'm not sure there's really anything else to this kind of structure besides general compatibility of + and <=

[Mario Carneiro]

no it's not

[Johan Commelin]

Can you use bot_le instead? I assume ⊥ is defeq to 0.

[Mario Carneiro]

you need a typeclass that asserts it if you want it to be part of odd.pos

[Violeta Hernández]

A typeclass for has_bot + has_zero with ⊥ = 0 seems like it could be useful

[Violeta Hernández]

I feel like I'm derailing this thread, though...

[Violeta Hernández]

I'll make a new one

[Violeta Hernández]

Here's another mostly unrelated remark, but why does odd require a semiring?

[Violeta Hernández]

Is the definition ∃ k, a = k + k + 1 not good enough?

[Violeta Hernández]

Arguably this might lead to worse def-eq, but if so, why is even defined as ∃ k, a = k + k and not as ∃ k, a = 2 * k?

[Violeta Hernández]

Even then, why not just require has_add, has_mul, and has_one?

[Damiano Testa]

For the even/odd definition, there was a previous thread.

The summary: even is more useful, no one really has strong feelings as to what is a "good" definition of odd.

[Violeta Hernández]

Understandable

[Damiano Testa]

With respect to the "ordinal odd", it seems that in this case, all that you use of "odd" is that the ordinal is a successor and therefore non-zero, right? This might be more useful for ordinals, than defining odd for them.