Nat.Prime vs Prime

Stream: mathlib4

[Jon Eugster]

Following this topic about Nat.Prime I realised I don't fully understand why mathlib has both Nat.Prime and _root_.Prime.

Is there a convenient reason that Nat.Prime works better for something or is this more that the API for _root_.Prime should ideally be improved so that it could fully replace Nat.Prime eventually? And just nobody done that yet?

Originally I thought Nat.Prime helps with decidability, but on first glance it seems that one could transport this decidability to _root_.Prime 3, too:

instance (p : ℕ) : Decidable (_root_.Prime p) :=
  decidable_of_iff' _ Nat.prime_iff.symm

[Ruben Van de Velde]

Historical reasons

[Ruben Van de Velde]

Also, you'd need to choose whether to replace it with Prime or Irreducible

[Riccardo Brasca]

Well, at least we follow the mathematical terminology of defining prime natural numbers via irreducibility and then using the word "prime" in general to denote something else (that of course is equivalent in the case of natural numbers)

[Ruben Van de Velde]

Mathematicians and their terminology are really something to behold :sweat_smile:

[Jon Eugster]

Ruben Van de Velde said:

Also, you'd need to choose whether to replace it with Prime or Irreducible

I mean sure, but since Prime and Irreducible are equivalent on Nat (or generally if there are no zero-divisors) , that's also just a matter of having the API written conveniently, isn't it?

[Jon Eugster]

Does "historical reason" mean a refactor could be appreciated in that case? Assuming it's more convenient to use than the current dual setup.

[Riccardo Brasca]

One should check that to prove stuff about Nat.Prime we would not need a lot of imports from ring theory

[Jon Eugster]

Looks like that should not be that case. At least _root_.Prime is already imported in the file where Nat.Prime is defined.

prime_to_nat_prime.png

[Mario Carneiro]

or rather, that battle was lost long ago

[Riccardo Brasca]

Yes, the definition is surely fine, I was wondering about the theorems. But I didn't check anything

[Jon Eugster]

Indeed, Nat.Prime does have quite a bit of unused transitive imports, but also it's not huge in it's current shape:

nat_prime2.jpg

Haven't really looked into it either, just trying to gauge here whether it would be worth looking at in a free minute or if that would be unreasonable.

[Ruben Van de Velde]

Looking at it a bit, but it seems like your picture is fairly out of date

[Eric Wieser]

Jon Eugster said:

Indeed, Nat.Prime does have quite a bit of unused transitive imports, but also it's not huge in it's current shape:

nat_prime2.jpg

Just as a reminder, optimizing away all gray nodes for the sake of removing gray is a bad metric, and at its extreme leads to total atomization of mathlib (or one single extraordinarily large file)

[Jon Eugster]

Ruben Van de Velde said:

Looking at it a bit, but it seems like your picture is fairly out of date

You're right, I made that from a branch I was reviewing, which is way too old, my bad.

[Ruben Van de Velde]

Eric Wieser said:

Jon Eugster said:

Indeed, Nat.Prime does have quite a bit of unused transitive imports, but also it's not huge in it's current shape:

nat_prime2.jpg

Just as a reminder, optimizing away all gray nodes for the sake of removing gray is a bad metric, and at its extreme leads to total atomization of mathlib (or one single extraordinarily large file)

That's fair, but I think there's some reasonable things that might be done here

[Kim Morrison]

Eric Wieser said:

Just as a reminder, optimizing away all gray nodes for the sake of removing gray is a bad metric, and at its extreme leads to total atomization of mathlib (or one single extraordinarily large file)

That's not really true, is it?

For example, If a file contains a definition F, and then independent lemmas A and B about F (and not requiring any additional imports), and then a lemma C which uses both A and B, I don't think there are even "extreme atomization" strategies that would separate these into different files.

(Except the trivial "total atomization" strategy, of course, e.g. if one were aiming for a content-addressed library.)

[Ruben Van de Velde]

#19342 is one change, though I'd be okay with it if we decided not to take it

[Ruben Van de Velde]

I'll investigate, though probably not today. I'm also looking at some other approaches

[Ruben Van de Velde]

Like #19346

[Ruben Van de Velde]

Also #19375

[Ruben Van de Velde]

Ruben Van de Velde said:

#19342 is one change, though I'd be okay with it if we decided not to take it

This is back up for review now.

Graph before the changes (2bb0410843932d03ff2c12cd9bf2e996f514a36b):

prime-master-0.png

With all the recent changes including #19342:

prime-nat-ring.png

[Johan Commelin]

Mario Carneiro said:

or rather, that battle was lost long ago

Mario, do you have some #assert_not_exists that you wish would be present in Data.Nat.Prime.Basic, based on the graphs above?

[Johan Commelin]

The two graphs seem to me to be roughly equivalent in size. So at the moment I don't feel strongly about merging one or the other.

[metakuntyyy]

May I ask how you are generating the import graphs?
I've figured it's lake exe graph. I have some troubles just getting the dependencies that I need. Currently I use import Mathlib, but I'd just like to use the dependencies that I need

[Kim Morrison]

Use #min_imports at the bottom of your file. It will tell you (sometimes incorrectly) what to replace import Mathlib with.

[Ruben Van de Velde]

Can I have a review on #19342 and #19437?

[Mario Carneiro]

Johan Commelin said:

Mario Carneiro said:

or rather, that battle was lost long ago

Mario, do you have some #assert_not_exists that you wish would be present in Data.Nat.Prime.Basic, based on the graphs above?

I would prefer to have #assert_not_exists Prime in Data.Nat.Prime.Basic

[Mario Carneiro]

we could even upstream Data.Nat.Prime.Basic to batteries, which would basically require this

[Mario Carneiro]

I don't think the definition should be Irreducible and use the algebraic hierarchy to do it

[Ruben Van de Velde]

I'm not convinced that would be better

[Mario Carneiro]

better how? It's a tradeoff, of course