Refactoring positive integers

[malarbol]

WIP https://github.com/UniMath/agda-unimath/issues/1043

[fredrik-bakke]

I quite like your organization of the concepts into their own files + a file about the relations between them. But if I didn't misunderstand @EgbertRijke rather wanted one file for all 5? Maybe he can comment on that.

[fredrik-bakke]

Your work looks pretty good so far by the way!

[malarbol]

I quite like your organization of the concepts into their own files + a file about the relations between them. But if I didn't misunderstand @EgbertRijke rather wanted one file for all 5? Maybe he can comment on that.

yes, I'm the one who suggested the single-file solution but I must say I got to appreciate the 4+1 modules. It gives slightly more room to separate specific-concepts properties and cross-concepts properties.

I don't know the library policy around public imports but maybe the positive-and-negative-integers module could re-export the four others, to avoid having to import the five modules everywhere?

I'll continue cleaning up the rest for a while and we can always merge the five modules when we're sure.

[fredrik-bakke]

I don't know the library policy around public imports but maybe the positive-and-negative-integers module could re-export the four others, to avoid having to import the five modules everywhere?

We usually only publicly import a module if it is to be viewed as a submodule. I don't really think that's what's going on here, so to keep the library consistent on this point I suggest that we don't import them publicly for now.

[fredrik-bakke]

Btw, you'd probably like to know that I'm doing a lot of refactoring of operations on propositions in #1008, and some of the basic notation will change. In case you get confused by that 😄

[malarbol]

Btw, you'd probably like to know that I'm doing a lot of refactoring of operations on propositions in https://github.com/UniMath/agda-unimath/pull/1008, and some of the basic notation will change. In case you get confused by that 😄

ok; I'll update the branch when you merge your changes and fix the conflicts of notations. But if there are any names that I should already change to fit the new notations you can point them out.

Seems like this refactoring is really shaping out! Thank you so much for working on this, and do let me know when you want more comments on your work.

Thanks! I still have a few things to cleanup but I should be ready soon.

[malarbol]

do let me know when you want more comments on your work.

Well, hello again; I think my refactoring is ready for another review. Regarding the points of your issue #1043 :

Factor strict inequality into their own files separate from inequality

I'm not sure I'd advocate for that. As for the positive/negative/etc. It makes functions like leq-le-XX or concatenate-leq-le-XX orphan of a natural module to go to.

Decide on whether to go for the formulation preserves-strict-order or preserves-le

As I said before, I'd go with preserves-le-XX and preserves-le-XX' but that's just my opinion. In that case I think there would be some cleanup to do, especially on natural numbers to unify the notation and the type signatures, e.g.

preserves-order-mul-ℕ :
  (k m n : ℕ) → m ≤-ℕ n → (m *ℕ k) ≤-ℕ (n *ℕ k)

could become

preserves-le-mul-ℕ' : {m n : ℕ} (k : ℕ) → m ≤-ℕ n → (m *ℕ k) ≤-ℕ (n *ℕ k)

and so on. The same goes for the reflects-XXX functions. If you're happy with the naming scheme I suggest, I can try to fix these too. Or maybe we can leave that for another PR. As you wish.

Factor out positive and negative integers into a separate module(s).

This is actually the main point of this PR.

Define the expected implications: strict inequality implies inequality

Done for integers, integers fractions and rationals. Was already done for natural numbers. Did you have any more cases in mind?

Define the expected entries where decidability is claimed.

I think they're still a few gaps I can fill here but maybe we can review a bit my work so far. There is still the "4+1 vs 1" question for positive/etc. integers that is not completely settled.

I know you are already quite busy with other issues/PR/etc. so thank you again a lot for your consideration.

[fredrik-bakke]

Hi again, thank you so much for your work, and apologies for taking so long to get back to you. Indeed, I have been quite busy. I will prioritize writing a proper review of your PR soon. In the meantime, I will try to reply to your comments.

Factor strict inequality into their own files separate from inequality

I'm not sure I'd advocate for that. As for the positive/negative/etc. It makes functions like leq-le-XX or concatenate-leq-le-XX orphan of a natural module to go to.

I guess in my mind, strict inequality comes after non-strict inequality, so all definitions pertaining to their interrelation would go in the file about strict inequality. Do you think that is a bad approach?

Decide on whether to go for the formulation preserves-strict-order or preserves-le

As I said before, I'd go with preserves-le-XX and preserves-le-XX' but that's just my opinion. In that case I think there would be some cleanup to do, especially on natural numbers to unify the notation and the type signatures, e.g.

preserves-order-mul-ℕ :
  (k m n : ℕ) → m ≤-ℕ n → (m *ℕ k) ≤-ℕ (n *ℕ k)

could become

preserves-le-mul-ℕ' : {m n : ℕ} (k : ℕ) → m ≤-ℕ n → (m *ℕ k) ≤-ℕ (n *ℕ k)

and so on. The same goes for the reflects-XXX functions. If you're happy with the naming scheme I suggest, I can try to fix these too. Or maybe we can leave that for another PR. As you wish.

That seems like a good assessment to me! Note that it should be leq in preserves-leq-mul-ℕ' and in this case a better name is actually preserves-leq-left-mul-ℕ :)

Factor out positive and negative integers into a separate module(s).

This is actually the main point of this PR.

Define the expected implications: strict inequality implies inequality

Done for integers, integers fractions and rationals. Was already done for natural numbers. Did you have any more cases in mind?

Not sure at the moment, but that is good for now. The reason I wanted those was because it opens up reuse of some other proofs, although at the moment I can't seem to remember what exactly. Was it that the relations are decidable?

Define the expected entries where decidability is claimed.

I think they're still a few gaps I can fill here but maybe we can review a bit my work so far. There is still the "4+1 vs 1" question for positive/etc. integers that is not completely settled.

Yes, I will review this ASAP! 🚀

[malarbol]

Hi!

thank you so much for your work, and apologies for taking so long to get back to you. Indeed, I have been quite busy. I will prioritize writing a proper review of your PR soon. In the meantime, I will try to reply to your comments.

no problem, and no rush.

I guess in my mind, strict inequality comes after non-strict inequality, so all definitions pertaining to their interrelation would go in the file about strict inequality. Do you think that is a bad approach?

I don't know if it's a bad idea but it does seem a bit arbitrary. If you don't define one in term of the other, it's not clear to me which one should come first...

I think what you're describing in your last comment is a homomorphism of preorders 😄

Indeed, or maybe even homomorphisms of posets I guess. Do you have a version that would be compatible with the strict ordering?

Note that it should be leq in preserves-leq-mul-ℕ' and in this case a better name is actually preserves-leq-left-mul-ℕ :)

sorry, I messed my exemple up and It should be preserves-leq-mul-ℕ'.

Regarding the left/right vs op-X/op-X', I'll have to give it a few mow thoughts. I'll try to make sense of all of it and I'll get back to you with a new suggestion. For exemple, the two functions

preserves-order-mul-ℕ :
  (k m n : ℕ) → m ≤-ℕ n → (m *ℕ k) ≤-ℕ (n *ℕ k)

preserves-order-mul-ℕ' :
  (k m n : ℕ) → m ≤-ℕ n → (k *ℕ m) ≤-ℕ (k *ℕ n)

are basically

preserves-order-mul-ℕ : (k : ℕ) → preserves-order-Poset ℕ-Poset ℕ-Poset (mul-ℕ' k)
preserves-order-mul-ℕ' : (k : ℕ) → preserves-order-Poset ℕ-Poset ℕ-Poset (mul-ℕ k)

so maybe the names should be swapped, and maybe it's the "good type signature" to adopt for the rest of similar functions.

I'll try to have a clean proposal in the next few days. Again, thanks for your consideration, and we'll be in touch.

[malarbol]

By the way, I may have written my transitivity properties in the wrong order, so as for now defining ℤ-Preorder is a bit weird:

ℤ-Preorder : Preorder lzero lzero
ℤ-Preorder =
  ℤ , leq-ℤ-Prop , refl-leq-ℤ , λ x y z H K → transitive-leq-ℤ x y z K H

Do you want me to rewrite them in the "compositional order" so the transitivity rules for inequalities corresponds to the definition of is-transitive?

[malarbol]

And last question for tonight, do you have something similar to the following?

preserves-rel : {l1 l2 : Level} {A : UU l1}
  (rel : A → A → UU l2) (f : A → A) → UU (l1 ⊔ l2)
preserves-rel {l1} {l2} {A} rel f =
  (x y : A) → rel x y → rel (f x) (f y)

In that case, maybe

preserves-leq-add-ℤ' : (z : ℤ) → preserves-rel leq-ℤ (add-ℤ' z)

could also be a good candidate?

[fredrik-bakke]

By the way, I may have written my transitivity properties in the wrong order, so as for now defining ℤ-Preorder is a bit weird:

ℤ-Preorder : Preorder lzero lzero
ℤ-Preorder =
  ℤ , leq-ℤ-Prop , refl-leq-ℤ , λ x y z H K → transitive-leq-ℤ x y z K H

Do you want me to rewrite them in the "compositional order" so the transitivity rules for inequalities corresponds to the definition of is-transitive?

Yes. Note that every other definition of transitivity in the library uses the compositional order. It is also useful to define a trans-leq-ℤ that takes x y z as implicit arguments

[fredrik-bakke]

And last question for tonight, do you have something similar to the following?

preserves-rel : {l1 l2 : Level} {A : UU l1}
  (rel : A → A → UU l2) (f : A → A) → UU (l1 ⊔ l2)
preserves-rel {l1} {l2} {A} rel f =
  (x y : A) → rel x y → rel (f x) (f y)

Ah, yes, sorry. This would be a morphism of directed graphs. 😅

[fredrik-bakke]

I still think your definitions should be preserves-leq-(left/right)-mul-bN The map preserves-leq-mul-bN I would expect to take an inequality for both the left and right hand side of the operator.

[malarbol]

Sorry for writing so many comments.

Don't need to; on the contrary. Your comments are really helpful to me and I'm the one who started with all my questions and doubts!

Your work is already very good, and looks ready to be merged soon!

Thanks. I'll be a bit busy in the next few days but I'll try to address all your comments and suggestions (and the few remaining doubts) for next week.

[malarbol]

I think this covers #1043 I've got a few more things for the elementary-number-theory module (e.g. additive inverse of rational numbers, properties for addition/multiplication of rational numbers, etc.) Do you want me to include them in this PR or do you want to merge this first and leave my new code for the next one? I think this is already quite much so it would be better to merge this now, close #1043, and keep going with a clean slate.

[fredrik-bakke]

I think this covers #1043 I've got a few more things for the elementary-number-theory module (e.g. additive inverse of rational numbers, properties for addition/multiplication of rational numbers, etc.) Do you want me to include them in this PR or do you want to merge this first and leave my new code for the next one? I think this is already quite much so it would be better to merge this now, close #1043, and keep going with a clean slate.

Congrats! Yes, I think it is best to open a new PR for new additions.

[malarbol]

In the library, I believe "inequality" is the name we use for the standard ordering on integers and so on. We shouldn't introduce "standard inequality" as an extra term for the same thing.

Ok. I chose inequality over order(ing) to stick with the names of the files ; maybe this was an error and I should have kept a bit of both? And I just stuck standard in a few places because of your comment on the many orderings of ℤ but we can drop them if you prefer.

[fredrik-bakke]

In the library, I believe "inequality" is the name we use for the standard ordering on integers and so on. We shouldn't introduce "standard inequality" as an extra term for the same thing.

Ok. I chose inequality over order(ing) to stick with the names of the files ; maybe this was an error and I should have kept a bit of both? And I just stuck standard in a few places because of your comment on the many orderings of ℤ but we can drop them if you prefer.

I think your choice is very sensible, and I can't see why it is a mistake. It seemed rather arbitrary how the prose kept switching between the two terms before.

[fredrik-bakke]

I like the current version of things, so I think this PR should be merged after my final suggestions have been implemented

[malarbol]

It seemed rather arbitrary how the prose kept switching between the two terms before.

well, each contributor will have its own prose and preferred terms so I guess this is bound to happen somehow. But it does give a kind of "organic" touch. As a reader, it's nice to feel that this was written by humans and that it's not just a juxtaposition of automatically derived proofs and generated text.

I like the current version of things, so I think this PR should be merged after my final suggestions have been implemented

thx. I also quite liked how it all turned out. Thank you again for all your time and dedication.

[fredrik-bakke]

Thank you!

If you don't mind, may I keep myself as co-author of this contribution? Reviewers are automatically added as co-authors when you accept one of their suggestions, but we have a policy that we do not preserve co-authorship status in these cases unless the submitter agrees to it. Normally I wouldn't even ask, but given that we've worked so closely on this one it seems fitting to keep my name on it. I do not mean to take any credit away from you though, you definitely deserve most of it for your hard work!

[malarbol]

If you don't mind, may I keep myself as co-author of this contribution?

Of course! I wouldn't have it any other way. I may have written most of the new code but I definitely consider we worked together on this. (and this goes for any future collaborations; I trust your judgment on your level of contribution).

[fredrik-bakke]

Merged!