Zulip Chat Archive

Stream: general

Topic: even/odd


Damiano Testa (Mar 15 2022 at 18:03):

Dear All,

currently, even and odd are defined as follow:

variables {α : Type*} [semiring α]

/-- An element `a` of a semiring is even if there exists `k` such `a = 2*k`. -/
def even (a : α) : Prop :=  k, a = 2*k

/-- An element `a` of a semiring is odd if there exists `k` such `a = 2*k + 1`. -/
def odd (a : α) : Prop :=  k, a = 2*k + 1

What would everyone think of redefining them in terms of bit0 and bit1? (Recall that bit0 a = a + a and bit1 a = a + a + 1).

variables {α : Type*}

--  new version
/-- An element `a` of a type with addition is even if there exists `k` such `a = k + k`. -/
def even [has_add α] (a : α) : Prop :=  k, a = bit0 k

/-- An element `a` of a semiring is odd if there exists `k` such `a = k + k + 1`. -/
def odd [semiring α] (a : α) : Prop :=  k, a = bit1 k

This means that some of the lemmas in data.nat/int.parity can be proven more generally and only once, e.g. even.add_even, even.add_odd...

Gabriel Ebner (Mar 15 2022 at 18:08):

Note that bit0/bit1 are gone in Lean 4.

Damiano Testa (Mar 15 2022 at 18:10):

Ok, so maybe I am changing to using

/-- An element `a` of a type with addition is even if there exists `k` such `a = k + k`. -/
def even [has_add α] (a : α) : Prop :=  k, a = k + k

/-- An element `a` of a semiring is odd if there exists `k` such `a = k + k + 1`. -/
def odd [semiring α] (a : α) : Prop :=  k, a = k + k + 1

:wink:

Johan Commelin (Mar 15 2022 at 18:30):

You only need [has_add α] [has_one] for odd :wink:

Damiano Testa (Mar 15 2022 at 18:31):

That's what I had, I'm not sure how I could have gone so much overboard with the assumptions! :lol:

Damiano Testa (Mar 15 2022 at 22:33):

As an experiment, I created a new file and proved the four lemmas about adding two elements of a semiring, with all combinations of even odd assumptions.

I then removed the duplicates in data.nat/int.parity and realized that these lemmas were not actually used!

Damiano Testa (Mar 15 2022 at 22:34):

The PR is #12718. The definition of even/has not changed.

Michael Stoll (Mar 19 2022 at 13:12):

... which broke some of my code upon updating mathlib; it was using some nat.even. stuff.

Damiano Testa (Mar 19 2022 at 13:16):

Oh, what is it? Probably, removing a nat. or int. prefix might fix the issue?

Damiano Testa (Mar 19 2022 at 13:16):

I'm not at a computer, though, so I will have limited possibilities of fixing this soon...

Damiano Testa (Mar 19 2022 at 13:17):

(Also, hi Michael!)

Michael Stoll (Mar 19 2022 at 13:39):

@Damiano Testa Hi! Yes, I just had to remove the nat. prefix.

Damiano Testa (Mar 19 2022 at 13:40):

I have tried being careful to only generalize statements, and not removing anything that was there, even if unused in master.

Glad that this was easy!

Michael Stoll (Mar 19 2022 at 14:02):

In fact, in one of the lemmas, the order of arguments had to be switched, but it was no big deal.

Damiano Testa (Mar 19 2022 at 14:08):

Ok. I would have probably picked up on this, if the even/odd side of the library was more used. As is, very few files use even/odd, so it is difficult to know if I made some "big" changes. The most visible for me was the change in namespace.

Yaël Dillies (Mar 21 2022 at 11:43):

Actually, why weren't even and odd using 2 • instead of 2 *?

Ruben Van de Velde (Mar 21 2022 at 11:59):

I'm guessing that would mean inserting smul_eq_mul rewrites in a lot of places

Kyle Miller (Mar 21 2022 at 12:05):

What would the motivation be to use smul instead of mul?

Yaël Dillies (Mar 21 2022 at 12:25):

... to not assume has_mul

Kyle Miller (Mar 21 2022 at 12:43):

If you want the reason, it's that a little over a year ago Patrick Massot defined them so that they can replace nat.even/nat.odd and int.even/int.odd.

Curious if there are any situations where you'd have has_add and has_one, have no has_mul, and want to know which elements are even or odd.

Riccardo Brasca (Mar 21 2022 at 12:46):

For abelian groups aka -modules it seems a reasonable concept.

Kyle Miller (Mar 21 2022 at 12:50):

Those have has_add and has_zero, but no has_one, right?

Yaël Dillies (Mar 21 2022 at 12:50):

Yes, so you can still talk about even

Riccardo Brasca (Mar 21 2022 at 12:51):

Ah sure, I was only thinking about has_smul

Damiano Testa (Mar 21 2022 at 13:57):

I was thinking of doing the change with \smul. However, it seems a little bit of work, which eventually is almost entirely used in nat, int, zmod 2.

If you think that having even for abelian add_monoids, then I can go ahead and refactor.

Damiano Testa (Mar 22 2022 at 07:14):

I have a proposal about this.

First a little bit of motivation.
I feel that even is much more useful for a general type than odd. The usefulness of odd is mostly for N\mathbb{N}, Z\mathbb{Z} and, a little artificially, for Z/2Z\mathbb{Z}/2\mathbb{Z}.

Moreover, even is the additive version of square. Btw, I did not find square or is_square in mathlib.

What do people think of the following?

import algebra.group.to_additive

/--  An element `a` of a type `α` with multiplication satisfies `square a` if `a = r * r`,
for some `r : α`. -/
@[to_additive even
"An element `a` of a type `α` with addition satisfies `even a` if `a = r + r`,
for some `r : α`."]
def square {α : Type*} [has_mul α] (a : α) : Prop :=  r, a = r * r

Damiano Testa (Mar 22 2022 at 07:15):

Then, the "general theory" would use \not even, rather than odd.

Bolton Bailey (Mar 22 2022 at 07:21):

I think square is generally rendered in mathlib as sq, did you try searching for that?

Bolton Bailey (Mar 22 2022 at 07:23):

In any case, making even the to_additive of a new is_sq seems clever and a good idea.

Damiano Testa (Mar 22 2022 at 07:38):

I just tried with sq and is_sq: with the former, there are several hits, but they all seem to be referring to lemmas describing a ^ 2 appearing in the type.

I could still not find a definition of a square. It may very well be that it is not there.

Damiano Testa (Mar 22 2022 at 07:39):

I also tried the more general is_pow and again I could not find it.

Kevin Buzzard (Mar 22 2022 at 08:00):

I personally think that all this is abstraction for abstraction's sake. Where is the application? Of course we use it for \N and \Z. Do we ever use the concept of oddness elsewhere?

Damiano Testa (Mar 22 2022 at 08:06):

I agree with you on odd: I do not think that odd is used except for nat and int.

However, square/even seem much more ubiquitous and that is the definition that I am proposing.

Yaël Dillies (Mar 22 2022 at 08:28):

Do you then want to define odd a as ¬ even a?

Damiano Testa (Mar 22 2022 at 08:29):

I am not even sure that I would define odd generally. I would delay defining odd for as long as possible. I think that¬ even a is good in general. For nat, int it is possible that + 1 is a good choice.

Yaël Dillies (Mar 22 2022 at 08:31):

Okay sure. I quite like this idea.

Damiano Testa (Mar 22 2022 at 08:32):

Let me clarify: I am proposing to change the definition of even so that it is the to_additive version of square.

With respect to odd I am currently proposing no change: whatever is already in mathlib, stays as is.

Possibly, odd will be revamped later on, but for the moment I was concerning myself only with even.

Yaël Dillies (Mar 22 2022 at 08:33):

The main point we have to remember is that even/square really is a very basic property that we use to simplify very elementary arguments.

Michael Stoll (Mar 22 2022 at 09:46):

In the code I have written so far to deal with the Hilbert symbol (over ℚ), I use even and odd a lot (of naturals), since it is very relevant if the p-adic valuation of something is even or odd. So I would hope that my squeezed simps will continue to work...

Damiano Testa (Mar 22 2022 at 09:50):

I hope so too! In any case, I have not started this yet. Once there is a PR, you can "test it out" by merging it into your branch and seeing if something breaks.

If/when it does, simply let me know and I will try to see what is going on. I will attempt to only change the definition and replace it with an equivalent one, so that all "old" lemmas still hold. What happened earlier was that some lemmas changed namespace, since they were no longer specific to nat/int but applied more generally. This is, I hope, the largest change to be expected for the existing lemmas!

Damiano Testa (Mar 22 2022 at 09:50):

Even the reordering of assumptions with which you had problems should not have happened.

Damiano Testa (Mar 22 2022 at 09:55):

By the way, if you PR your lemmas and they make it to mathlib before the revamping of even takes place, then it is not your responsibility to make sure that it still compiles, but mine! :wink:

Damiano Testa (Mar 22 2022 at 09:57):

In fact, what you are describing is a great testing ground for the change in even/square. Knowing that something has even valuation is not equivalent to it being a square and it would be kind of cool to see the interaction between these two "identical concepts in additive/multiplicative groups" playing out in Lean!

Michael Stoll (Mar 22 2022 at 09:59):

It will take a while until my stuff will get into mathlib, so don't hold your breath.

Michael Stoll (Mar 22 2022 at 10:00):

Anyway, here is a teaser:

theorem Hsymbol_product_formula_finprod (a b : ) : ∏ᶠ v, [a, b | v]_H = 1 := ...

Michael Stoll (Mar 22 2022 at 10:01):

I'll open a thread on this and the questions I have related to getting it into mathlib at some later point...

Damiano Testa (Mar 22 2022 at 10:04):

Ok, in any case, once this gets going, I may ask you if I can merge your branch into mine, as a test. At the moment, even/odd is not so used in mathlib and squares do not appear to even exist!

Yaël Dillies (Mar 22 2022 at 10:06):

Pretty sure they do, but the condition is written out.

Johan Commelin (Mar 22 2022 at 10:29):

@Michael Stoll Is that Hsymbol_product_formula_finprod sorry-free?

Michael Stoll (Mar 22 2022 at 10:29):

@Johan Commelin Yes!

Johan Commelin (Mar 22 2022 at 10:30):

Wow! That's really nice!

Michael Stoll (Mar 22 2022 at 10:30):

As it stands, it is ~3000 lines of code.

Michael Stoll (Mar 22 2022 at 10:31):

And some stuff is still missing, like the characterization via solvability of ternary quadratic forms...

Michael Stoll (Mar 22 2022 at 10:36):

When I embarked on that project, I did not anticipate that it would grow so large.

Ruben Van de Velde (Mar 22 2022 at 10:37):

Michael Stoll said:

When I embarked on that project, I did not anticipate that it would grow so large.

I feel that! :)

Damiano Testa (Mar 22 2022 at 18:01):

If you are interested, I started preparing the refactor of even. The relevant PR is #12882.

This PR is only moving (many) lemmas involving even/odd to a single file. The change in definition will happen in a separate PR.

Scott Morrison (Mar 22 2022 at 22:52):

@Michael Stoll, if you've got 3000 lines of code, you think some things are still missing, but substantial results are already sorry-free, I'd really encourage you to start PRing material. It's going to require many PRs to get your work into mathlib, and starting early is good for everyone. (mathlib gets the early content even if the content you still want to work on takes much longer, you get feedback that may require changes to the later work as early as possible, and reviewers get more time!)

Michael Stoll (Mar 23 2022 at 19:29):

@Scott Morrison You are probably right, but I'm a bit afraid that doing all this will develop into an enormous time sink... (And first I have to learn how this all works.) So I'm planning to do it slowly.

Patrick Massot (Mar 23 2022 at 20:29):

There is no doubt it will be an enormous time sink. But you'll learn a lot.

Yury G. Kudryashov (Mar 23 2022 at 21:02):

And this way your code will not rot (especially after migration to Lean 4).

Damiano Testa (Mar 30 2022 at 06:50):

Dear All,

PR #13037 now has oleans! Any comment would be greatly appreciated!

Thanks!


Last updated: Dec 20 2023 at 11:08 UTC