even/odd

Stream: general

[Damiano Testa]

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]

Note that bit0/bit1 are gone in Lean 4.

[Damiano Testa]

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]

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

[Damiano Testa]

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

[Damiano Testa]

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]

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

[Michael Stoll]

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

[Damiano Testa]

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

[Damiano Testa]

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

[Damiano Testa]

(Also, hi Michael!)

[Michael Stoll]

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

[Damiano Testa]

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]

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

[Damiano Testa]

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]

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

[Ruben Van de Velde]

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

[Kyle Miller]

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

[Yaël Dillies]

... to not assume has_mul

[Kyle Miller]

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]

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

[Kyle Miller]

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

[Yaël Dillies]

Yes, so you can still talk about even

[Riccardo Brasca]

Ah sure, I was only thinking about has_smul

[Damiano Testa]

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]

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 $\mathbb{N}$, $\mathbb{Z}$ and, a little artificially, for $\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]

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

[Bolton Bailey]

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

[Bolton Bailey]

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

[Damiano Testa]

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]

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

[Kevin Buzzard]

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]

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]

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

[Damiano Testa]

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]

Okay sure. I quite like this idea.

[Damiano Testa]

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]

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]

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]

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]

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

[Damiano Testa]

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]

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]

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

[Michael Stoll]

Anyway, here is a teaser:

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

[Michael Stoll]

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

[Damiano Testa]

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]

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

[Johan Commelin]

@Michael Stoll Is that Hsymbol_product_formula_finprod sorry-free?

[Michael Stoll]

@Johan Commelin Yes!

[Johan Commelin]

Wow! That's really nice!

[Michael Stoll]

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

[Michael Stoll]

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

[Michael Stoll]

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

[Ruben Van de Velde]

Michael Stoll said:

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

I feel that! :)

[Damiano Testa]

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]

@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]

@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]

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

[Yury G. Kudryashov]

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

[Damiano Testa]

Dear All,

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

Thanks!