Zulip Chat Archive

Stream: mathlib4

Topic: Algebra.GroupPower.Order


Siddhartha Gadgil (Dec 15 2022 at 11:01):

I have started porting Algebra.GroupPower.Order, and everything is ported except for a theorem pow_bit0_pos_iff which depends on an unported result in Lean core, as everything to do with bit0 seems deprecated.

I was going to ask if this should be commented out, but I see that this has an important corollary: theorem sq_pos_iff (a : R) : 0 < a ^ 2 ↔ a ≠ 0.
What would be a good policy:

  • port the results on bit0
  • port a modification using doubles and prove only the result about squares and the lemmas along the way.

I feel the second has the advantage that if the deprecated bit0 is removed we can have the other results still.

Yaël Dillies (Dec 15 2022 at 11:25):

The bit0 and bit1 lemmas have (/had?) the avantage that they apply to numerals.

Siddhartha Gadgil (Dec 15 2022 at 11:42):

Do you think they are worth porting then (at least the ones that are used)?

Yaël Dillies (Dec 15 2022 at 11:43):

I don't know how numerals work in Lean 4, but if there is a way of seeing whether a numeral is even or odd from the head symbol, yes definitely.

Floris van Doorn (Dec 15 2022 at 11:48):

No, the head symbol of numerals is not bit0/bit1 anymore, so I expect that simp and rw will not be able to deal well with lemmas about bit0 and bit1 anymore.

Kevin Buzzard (Dec 15 2022 at 11:50):

This is really a result about even and odd -- the fact that in lean 3 we chose to express them via bit0 is now a historical coincidence. Are we in a position to port data.nat.parity? If not then we could make data.nat.parity.defs and that would be a nice way forward

Floris van Doorn (Dec 15 2022 at 11:54):

We can still state lemmas about bit0/bit1, but I don't know if that will be nicer than 2 * _ or 2 * _ + 1. I think both forms will not easily match the numerals 16 or 17 (but I might be wrong, I didn't check).

Siddhartha Gadgil (Dec 15 2022 at 11:57):

As they are marked as deprecated, a file with lemmas about them is rejected.

Siddhartha Gadgil (Dec 15 2022 at 11:59):

I should also add that the PR is mathlib4#1043 and given my timezone if anyone wants to take over they are welcome.

Yaël Dillies (Dec 15 2022 at 12:00):

Kevin Buzzard said:

This is really a result about even and odd -- the fact that in lean 3 we chose to express them via bit0 is now a historical coincidence. Are we in a position to port data.nat.parity? If not then we could make data.nat.parity.defs and that would be a nice way forward

It's not a historical coincidence at all. I made sure that all lemmas were available in both spellings.

Ruben Van de Velde (Dec 15 2022 at 12:23):

Please port the bit lemmas, even though they won't apply directly to numerals. You'll need a set_option - see all other declarations about bit in the tree for examples

Yaël Dillies (Dec 15 2022 at 12:27):

Also, Kevin, why data.nat.parity? Everything is in file#algebra/parity which is very low import now.

Kevin Buzzard (Dec 15 2022 at 12:36):

Yael I'm sure you know a lot more about parity than me :-)

Siddhartha Gadgil (Dec 15 2022 at 12:41):

Sure. I will port the bit lemmas

Siddhartha Gadgil (Dec 15 2022 at 13:08):

Actually some of this has been ported either for Positivity or Linarithmetic. I will deduplicated and clean up.

Siddhartha Gadgil (Dec 15 2022 at 13:34):

Just to confirm mathlib4#1043 is ready for review


Last updated: Dec 20 2023 at 11:08 UTC