Small refactorings for elementary number theory

[fredrik-bakke]

The elementary-number-theory module is in need of some love and attention. This issue is not aiming for a complete overhaul as one might be tempted to, but I will record some select glaring issues that should be easier to resolve.

This issue is a work in progress

Elementary number theory

• Factor strict inequality into their own files separate from inequality
• Decide on whether to go for the formulation preserves-strict-order or preserves-le
• Factor out positive and negative integers into a separate module(s).
• Define the expected implications: strict inequality implies inequality
• Define the expected entries where decidability is claimed.

[fredrik-bakke]

If I recall correctly, parts of the theory of lower and upper dedekind cuts is an instance of the theory of lower and upper sets of posets. If so, we should also refactor them to use this theory. We have files about upper sets of large posets, so adapting* these to small posets shouldn't be a problem.

[malarbol]

Hello again,
I had a few thoughts about nonnegative, positive, etc. integers.

Regarding,

Factor out new file positive-integers also treating nonpositive integers
Factor out new file negative-integers also treating nonnegative integers

I think it's cleaner to treat the four concepts in a single file. There are a lot of pairwise interesting properties so it's easier to have all of them in the same module. I have pushed a module signed-integers in my repo doing this.
Some name conflicted with the ones in the integers module so I prefixed them with a * to have the module compile (like *nonnegative-ℤ or *int-nonnegative-ℤ).

[fredrik-bakke]

Ah, yes, I see the issue. I'm not so happy with having one file for all four concepts though. We could consider having stub files about nonnegative and nonpositive integers, and then import them in the files about positive integers and negative integers.

By the way, when refactoring like this, I find it's useful to just immediately delete the original entries when I move them elsewhere. That way I don't have to remember it later, and I don't have to get creative with names that will then have to be cleaned up later.

[fredrik-bakke]

Another thing I came across while having another look tonight is that we have files decidable-total-order-natural-numbers and decidable-total-order-standard-finite-types that seem to be a little ill-motivated and out of place. Perhaps we should try to find a different dichotomy for the files about the standard inequalities. Either we can separate the more order-theoretic considerations into a second file, or we can separate out considerations relating to decision procedures.

[fredrik-bakke]

btw I've started doing work in #1048. I'm not sure I will have much time to work on it tomorrow though

[malarbol]

Ah, yes, I see the issue. I'm not so happy with having one file for all four concepts though. We could consider having stub files about nonnegative and nonpositive integers, and then import them in the files about positive integers and negative integers.

I'm not sure what you mean by "stub files", sorry. But you don't like the single file idea, I guess the alternative is to have four files for the definitions, one for each of nonnegative, positive, nonpositive, negative and then a fifth module that would import these four, and treat all the properties between them. Is this what you suggest?

By the way, when refactoring like this, I find it's useful to just immediately delete the original entries when I move them elsewhere. That way I don't have to remember it later, and I don't have to get creative with names that will then have to be cleaned up later.

yes, I agree it would be much cleaner, it was just a proof-of-concept so I went for the easy way. When I remove is-positive stuff from the integers module I'll have to track all the other modules using them and fix the imports and functions so I delayed this step until the structure for new files is settled.

Another thing I came across while having another look tonight is that we have files decidable-total-order-natural-numbers and decidable-total-order-standard-finite-types that seem to be a little ill-motivated and out of place. Perhaps we should try to find a different dichotomy for the files about the standard inequalities. Either we can separate the more order-theoretic considerations into a second file, or we can separate out considerations relating to decision procedures.

I haven't worked a lot with these modules, I'll have to dig up a bit.

[fredrik-bakke]

I haven't worked a lot with these modules, I'll have to dig up a bit.

It seems to me like the main subject of those modules is decision procedures, but I don't know of a good title for such a file yet. Perhaps just

• decision-procedures-inequality-natural-numbers

However, in agda-unimath, we organize files by concepts rather than implementation details, and this title suggests that the file is organized after implementation details to me.

[fredrik-bakke]

I guess decidability-inequality-natural-numbers could work, but that doesn't encapsulate all of the contents I would like to put in the file.

[fredrik-bakke]

I'm not sure what you mean by "stub files", sorry.

By "stub file" I mean a very short file, here I meant that they would only contain the definitions. The terminology comes from wikis, where the word "stub" is used for an incomplete wiki page where only some basic things are established.

But you don't like the single file idea, I guess the alternative is to have four files for the definitions, one for each of nonnegative, positive, nonpositive, negative and then a fifth module that would import these four, and treat all the properties between them. Is this what you suggest?

I guess I can be convinced that they can all be in one file. I think signed-integers is a bad name, however, since every integer is signed, and it may suggest to someone that "integers" are not signed. How about calling it positive-and-negative-integers instead?

[malarbol]

Hello again, sorry for the delay, I've been a bit busy lately.

I guess I can be convinced that they can all be in one file. I think signed-integers is a bad name, however, since every integer is signed, and it may suggest to someone that "integers" are not signed. How about calling it positive-and-negative-integers instead?

After giving it a few more thoughts, I went for the 4+1 modules solution. It's all in my branch master...malarbol:agda-unimath:signed-integers, I'd be happy to have your feedback if you have time.

I also followed your advice

to just immediately delete the original entries when I move them elsewhere.

trying to keep all that seemed relevant. There are still a few things to cleanup, for exemple these two functions used in the Bezout's modules

decide-is-nonnegative-ℤ :
  {x : ℤ} → (is-nonnegative-ℤ x) + (is-nonnegative-ℤ (neg-ℤ x))

is-zero-is-nonnegative-neg-is-nonnegative-ℤ :
  (x : ℤ) → is-nonnegative-ℤ x → is-nonnegative-ℤ (neg-ℤ x) → is-zero-ℤ x

seem a bit artificial, so to speak, and maybe we could replace their uses with some combinations of decide-is-negative-is-nonnegative-ℤ, is-zero-is-nonnegative-is-nonpositive-ℤ, etc.

[fredrik-bakke]

No worries! Do let me know if you would rather move on to formalize more math instead. It is not much fun to do this sort of refactoring after all.

[fredrik-bakke]

Regarding the files on Bezout's lemma, it is best not to spend your time on them currently, as they are in need of a very thorough refactoring

[malarbol]

I think it would also be nice to remove the "positive/nonnegative stuff" from the addition-integers and multiplication-integers modules. What do you think about two more modules addition-positive-and-negative-integers and multiplication-positive-and-negative-integers that would treat all the combinations rules for addition/multiplication of positive, etc. integers ?

I was thinking something like this :

p	q	p +ℤ q	operation
positive	positive	positive	add-positive-ℤ
positive	nonnegative	positive
positive	negative	??
positive	nonpositive	??
nonnegative	nonnegative	nonnegative	add-nonnegative-ℤ
nonnegative	negative	??
nonnegative	nonpositive	??
negative	negative	negative	add-negative-ℤ
negative	nonpositive	negative
nonpositive	nonpositive	nonpositive	add-nonpositive-ℤ

p	q	p *ℤ q	operation
positive	positive	positive	mul-positive-ℤ
positive	nonnegative	nonnegative
positive	negative	negative
positive	nonpositive	nonpositive
nonnegative	nonnegative	nonnegative	mul-nonnegative-ℤ
nonnegative	negative	nonpositive
nonnegative	nonpositive	nonpositive
negative	negative	positive	mul-negative-ℤ
negative	nonpositive	nonnegative
nonpositive	nonpositive	nonnegative	mul-nonpositive-ℤ

Maybe it's a bit too much, but if you/we go for the four concepts of (non)positive and (non)negative why not be exhaustive.

[fredrik-bakke]

Hmm, I do like that suggestion. I'm afraid I am not so intimate with the module that I can immediately say if it's good or bad, but a priori it sounds good to me.

[fredrik-bakke]

Btw, if you want feedback on your current work, it is very useful if you post a pull request, because then I can comment directly on your code with suggestions and the likes. Your coding style seems to be very good as far as I can tell by skimming the changes though.

[malarbol]

No worries! Do let me know if you would rather move on to formalize more math instead. It is not much fun to do this sort of refactoring after all.

I'm still learning Agda/HoTT so it's easier to go with basic maths. But I'd be more than happy to contribute to other parts of the library.

[malarbol]

Regarding the files on Bezout's lemma, it is best not to spend your time on them currently, as they are in need of a very thorough refactoring

yeah, they look a bit scary. I just made the minimal changes to have them compile with the new modules for positive-integers etc.
Maybe we should can keep the

decide-is-nonnegative-ℤ :
  {x : ℤ} → (is-nonnegative-ℤ x) + (is-nonnegative-ℤ (neg-ℤ x))

is-zero-is-nonnegative-neg-is-nonnegative-ℤ :
  (x : ℤ) → is-nonnegative-ℤ x → is-nonnegative-ℤ (neg-ℤ x) → is-zero-ℤ x

functions after all.

[EgbertRijke]

Hi!

Thanks to both of you for picking up this issue

I think I actually like the idea of a file for signed integers best, treating all four concepts in one place. A lot of things about signed integers is about the interaction between the (non)positive and (non)negative integers.

If you make separate files for (non)positive and (non)negative integers, don't you create the problem of where to put something that is about the interaction of both of them? For example, where would the property that every positive integer is nonnegative go if we have a file positive-integers also treating nonpositive integers and a file negative-integers also treating nonnegative integers?

A good refactoring of the files would make it obvious where to expect code to be.

May I also suggest that the refactorings of the real numbers should be a completely separate issue?

[fredrik-bakke]

Yeah, I'm starting to agree that one file for all the versions of signing an integer is best. However, how do you feel about positive-and-negative-integers vs. signed-integers?

[EgbertRijke]

That name is ok with me

[fredrik-bakke]

May I also suggest that the refactorings of the real numbers should be a completely separate issue?

This is now #1060.