Algebra.GroupPower.Lemmas

Stream: mathlib4

[Riccardo Brasca]

I've done a little more than the first half of the port of Algebra.GroupPower.Lemmas in #1055. I am stopping now and I will not work on it until Monday I think. If someone wants to keep working on it no problem, just push to PR.

NB: I didn't change any name, so all of them must be checked.

[Siddhartha Gadgil]

I will probably try a bit tomorrow morning Indian time.

[Riccardo Brasca]

It's not very funny, but nothing too annoying, it's just a long file. Also, I think we should move all lemmas about bit0/bit1 to a single section, maybe at the end.

[Riccardo Brasca]

I mean, lemmas bit0/bit1 in the statement. Their use in proofs should be avoided.

[Yaël Dillies]

I'm not sure why we are hunting bit0 and bit1 down like this. I understand numerals don't use them anymore, but why removing them from proofs?

[Arien Malec]

Because they are proving invariant under an arbitrary binary representation that isn't useful in Lean4?

[Yaël Dillies]

"isn't useful to Lean 4 core" is what you meant to say

[Arien Malec]

My impression is that the reasons these proofs were done is that bit0 and bit1 were central to bitwise operations in Lean 3 and they aren't central to anything in Lean 4. If there's an area of group theory or whatever that finds a + a and a + a + 1 interesting operations, fair enough.

[Yaël Dillies]

Parity is pretty central :sweat_smile:

[Arien Malec]

It's a weird definition of even/odd, and a weird definition of binary parity.

[Yaël Dillies]

What is a non-weird definition of even/odd, then?

[Ruben Van de Velde]

We already have docs#even and docs#odd

[Reid Barton]

https://en.wikipedia.org/wiki/Parity_(mathematics)

[Reid Barton]

https://ncatlab.org/nlab/show/even+number

[Reid Barton]

hope these help :upside_down:

[Yaël Dillies]

This is a bit0 definition at heart :thinking:

[Arien Malec]

bit0/bit1 are even/odd the wrong way round, yeah?

[Reid Barton]

It's weird of course to write 2 * a as a + a. Otherwise the definitions are fine.

[Arien Malec]

even is \exists b, a = b + b, bit0 is just the b + b part

[Riccardo Brasca]

I mean, if we want to remove them is better to avoid using them in untalented statements (bit0 was used in the proof of Bernoulli's inequality)

[Kevin Buzzard]

I don't see any reason to define a new function f(b) for b + b or 2 * b, it just impedes vision. However I can see the argument for just porting everything mindlessly and then considering deleting them later.

[Joseph Myers]

Where the lemmas exist to allow simplification of expressions involving numerals, it would also be a good idea to implement whatever's needed for the equivalent simplification in Lean 4 (i.e. what's needed for simp or norm_num or some such tactic to do the simplification automatically, which may vary from case to case), before deleting them.

[Siddhartha Gadgil]

I have fixed the issues in Algebra/GroupPower/Lemmas (sometimes with roundabout proofs) but this has broken one proof in Tactic/NormNum/Basic' which imports this file. This is a simp` proof perhaps broken by a new simp lemma.

@Scott Morrison or @Mario Carneiro can you take a look?

[Scott Morrison]

Regarding above, please don't move lemmas around, it just makes life harder for reviewers or people who come later to solve problems. We're trying to port as boringly as possible, please. :-)

[Siddhartha Gadgil]

I did not move any lemmas, only fixed proofs. I took this over from @Riccardo Brasca so he may know if any lemmas were moved. I will check with git.

[Siddhartha Gadgil]

It seems that the signatures of a couple of lemmas were changed to use coercion instead of .cast. I don't see any other deletions.

[Siddhartha Gadgil]

@Scott Morrison
It is fixed I believe. A lemma was added in the ad hoc port that was removed in the port. I have restored it with a porting note and things seem fine locally.
For reference, this was the lemma:

@[simp] theorem pow_eq {m : ℤ} {n : ℕ} : m.pow n = m ^ n := rfl

[Riccardo Brasca]

I changed an import to avoid a cycle (caused by the ad hoc port), I didn't move any lemma around.

[Riccardo Brasca]

Also, there is the declaration that is now a tautology that needs to be fixed. See my message in the thread about norm_cast (on my phone, sorry)

[Reid Barton]

Changing imports is also likely to break future ports; did you change the imports of the ad hoc port?

[Siddhartha Gadgil]

Somehow one lemma of the ad hoc port got deleted. I don't know if it was because it was not actually a port or whether it was accidentally deleted while editing (I could have done that).

[Siddhartha Gadgil]

I am running the linter and commenting out tautologies (with porting notes).

[Riccardo Brasca]

No, I only removed a dependency on a norm num and now the imports reflect the mathlib3 situation. Sorry but I don't have a computer today, so I cannot explain better.

[Siddhartha Gadgil]

What I saw finally was that the lemma pow_eq was in the ad hoc version but not in the ported version. I have put it back. I don't know where it went away - it could have been me while editing accidentally deleting it.

[Kevin Buzzard]

If a lemma has become a tautology then this might not be an indication that it needs deleting, but might rather be a consequence of the fact that parsing has changed a little and the statement needs to be changed slightly. See got example Riccardo's n^m lemma in another thread (sorry, on mobile). I think the autoporter is getting these wrong?

[Riccardo Brasca]

The autoport commented that lemma, so it was right. I uncommented it because I didn't see it is a tautology. But Yaël's version seems reasonable

[Siddhartha Gadgil]

@Riccardo Brasca I believe the PR is ready (two rounds of review and I addressed most comments) but one comment of @Kevin Buzzard is regarding code you ported at line 390:
"Do we really want a TODO in a docstring as opposed to just in a comment in the code?"

Can you address this?

[Riccardo Brasca]

That line has nothing to do with the port, it is also in mathlib3. I agree a comment would be better, but maybe we just want to keep it as in mathlib.

[Kevin Buzzard]

I don't mind, I just thought it was odd

[Siddhartha Gadgil]

Hopefully the other comments are addressed (in many cases taking your shorter proofs).