Zulip Chat Archive

Stream: mathlib4

Topic: data.nat.prime #1156

Ruben Van de Velde (Dec 21 2022 at 20:40):

I'm done for today in case someone wants to work on it

Kevin Buzzard (Dec 21 2022 at 20:48):

mathlib4#1156

Kevin Buzzard (Dec 21 2022 at 20:56):

I'll take on the sorry in Data.Nat.Sqrt

Siddhartha Gadgil (Dec 22 2022 at 07:09):

The PR has cleared CI and is ready for review.

Johan Commelin (Dec 22 2022 at 08:01):

I think Data.Nat.Sqrt still needs some cleaning up.

Johan Commelin (Dec 22 2022 at 08:01):

I don't think AM_GM should stay in that file, etc...

Johan Commelin (Dec 22 2022 at 08:01):

@Scott Morrison what is the philosophy here?

Johan Commelin (Dec 22 2022 at 08:02):

Should we move things to other files? Or leave a -- porting note: move this?

Scott Morrison (Dec 22 2022 at 08:03):

How about a new file, which doesn't correspond to anything in mathlib3, that contains the "new work" that had to be done to put the pieces back together again in the "directly ported" files?

Scott Morrison (Dec 22 2022 at 08:04):

(Thinking that this minimises discrepancies with the mathlib3 files, for ease of understanding what's happened later / verifying everything is in place.)

Johan Commelin (Dec 22 2022 at 08:05):

In other words: Data/Nat/Sqrt_for_mathlib.lean? :wink:

Johan Commelin (Dec 22 2022 at 08:13):

@Anand Rao Do you want to finish this PR? If you have no time, then let me know and I can do it.

Anand Rao (Dec 22 2022 at 08:22):

Yes, I can try polishing the new proofs and clearing out the unused lemmas.

Anand Rao (Dec 22 2022 at 09:54):

I have taken the approach of creating two auxilliary files for Data.Nat.Sqrt:

  • Data.Nat.ForSqrtEssential contains two general lemmas about natural numbers (including the AM-GM inequality) and two facts about the sqrt.iter function (which could be moved to Std.Data.Nat.Basic)
  • Data.Nat.ForSqrtNonEssential contains a few lemmas that we proved while porting the file but never ended up using. Some of these might be useful to have in Mathlib or Std (specifically div_mul_div_le and iter_fp_bound), but the rest can be discarded.

Johan Commelin (Dec 22 2022 at 09:58):

@Anand Rao I think we shouldn't put the NonEssential file in mathlib.

Anand Rao (Dec 22 2022 at 10:00):

I'll remove it then. What do you suggest we do with the lemmas div_mul_div_le and iter_fp_bound? Should I merge the two auxilliary files, keeping only the potentially useful lemmas?

Anand Rao (Dec 22 2022 at 10:05):

I have removed the NonEssential file. There is now just one file - ForSqrt.

Ruben Van de Velde (Dec 22 2022 at 16:49):

mathlib4#1156 is ready for review

Last updated: Dec 20 2023 at 11:08 UTC