Rational real numbers

[malarbol]

This PR introduces the cannonical map from ℚ to ℝ as well as a characterisation of its image in terms of Dedekind cuts.

To do so, I had to introduce a few properties on (strict) inequalities on the rational numbers, integer fractions and integers.

• modified: elementary-number-theory/addition-integers.lagda.md

  • the sum of a nonnegative and a positive integer is positive

• new file: elementary-number-theory/cross-mul-diff-integer-fractions.lagda.md

  • define the cross-multiplication difference of two integer fractions
  • computing properties (useful to work with comparison of integer fractions)

• modified: elementary-number-theory/inequality-integer-fractions.lagda.md

  • generic properties of the (strict) order on integer fractions
    (asymmetricity, transitivity, etc.)
  • helper functions to construct inequal fractions

• modified: elementary-number-theory/inequality-integers.lagda.md

  • fix the definition of le-ℤ
  • generic properties of le-ℤ
  • preservation/reflection properties of le-ℤ w.r.t add-ℤ

• modified: elementary-number-theory/inequality-rational-numbers.lagda.md

  • generic properties of the (strict) order on rational numbers
  • compatibility between the orderings on integer fractions and
    rational numbers
  • no lower/upper bounds, decidability, trichotomy principle
  • density and of strict inequality on rational numbers

• modified: elementary-number-theory/integers.lagda.md

  • decide positivity of integers

• new file: elementary-number-theory/mediant-integer-fractions.lagda.md

  • define the mediant of two integer fractions
  • the mediant preserves cross-multiplication difference

• modified: elementary-number-theory/multiplication-integers.lagda.md

  • multiplication by a positive integer preserves strict ordering

• modified: elementary-number-theory/rational-numbers.lagda.md

  • accessor functions for rational numbers
  • define the mediant of two rational numbers

• modified: real-numbers/dedekind-real-numbers.lagda.md

  • contructor and accessor functions for real numbers
  • properties of Dedekind cuts
  • real numbers are determined by their lower/upper cuts

• new file: real-numbers/rational-real-numbers.lagda.md

  • define the Dedekind cut given by a rational number
  • define the subtype of rational real numbers
  • ℚ embeds in ℝ as the subtype of rational real numbers

[fredrik-bakke]

Hey, @malarbol! Welcome back, and thank you for submitting the pull request. As you can see, our conventions have changed quite a bit since your last contribution. 😅 You will probably get a review from us by this time tomorrow, so just hang tight in the meanwhile.

[malarbol]

Hi @fredrik-bakke! Thank you for considering it 😊! I hope it's ok to submit a PR like this without warning. if it's not in the guidelines / conventions of the library, I understand.

[fredrik-bakke]

No no, any submission is great! It was only a light-hearted remark :)

[fredrik-bakke]

Apologies for having even more nitpick. Your PR is already really good, and it is immediately ready to be merged after my last comments have been resolved. Thank you so much again for your patience!

[fredrik-bakke]

By the way, we have a file where we record names of contributors. Currently, you're displayed as "malarbol", which is your GitHub display name. There is no pressure, but if you want to go by your given name, you can edit your display name in our file CONTRIBUTORS.toml.

[fredrik-bakke]

I recorded an issue (#1043) about refactoring elementary number theory with what I could think of on the top of my head now. Feel free to have a look and comment about additional issues you find/have found there :)

[malarbol]

Apologies for having even more nitpick. Your PR is already really good, and it is immediately ready to be merged after my last comments have been resolved. Thank you so much again for your patience!

Oh! on the contrary, think you for your patience ; I'm really sorry for all the indentation/parenthesis/etc. problems. I think I understand a bit better now, my next PR will be a lot cleaner, don't worry.

By the way, we have a file where we record names of contributors. Currently, you're displayed as "malarbol", which is your GitHub display name. There is no pressure, but if you want to go by your given name, you can edit your display name in our file CONTRIBUTORS.toml.

I think I'll keep malarbol for the moment if you don't mind; I might add myself later, when I feel more confident or something.

I recorded an issue (#1043) about refactoring elementary number theory with what I could think of on the top of my head now. Feel free to have a look and comment about additional issues you find/have found there :)

Cool! I do have a few ideas / comments / doubts so I'll definitely get in touch with you there to talk about it.

There are still two points to discuss before merging, the skew-commutative-XXX name and whether or not to keep the decide-located-le-ℚ : (x y z : ℚ) → le-ℚ y z → le-ℚ y x + le-ℚ x z function. Once you tell me what you decide, I'll push the last changes and you can merge whenever you want.

Thank you again, for all, and see you for issue (#1043).

[fredrik-bakke]

Awesome! Thank you so much once again.
I'll probably post a PR tomorrow or on Thursday starting some refactoring, so stay on the lookout for that. If you decide to do more work in the meantime, don't hesitate to post a draft PR about it. That way, it is easier for me to avoid duplicating work or stepping on your toes.

Talk to you again soon :)