Refactor the natural numbers and integers up to present code standards #1568

lowasser · 2025-10-05T05:42:13Z

Maybe I should've done the natural numbers and the integers separately? If so, I'll split it...

Changes include:

more consistent terminology (e.g. irreflexive versus antireflexive, symmetric versus commutative)
updated naming conventions
making most proofs of most propositions abstract
Improved Idea sections: concept links, cross references, fixed missing idea sections entirely
minor code cleanups, especially the use of is-equiv-is-invertible

lowasser · 2025-10-05T05:43:14Z

src/elementary-number-theory/inequality-standard-finite-types.lagda.md

I'll admit it's not obvious to me that these files on the standard finite types belong in elementary-number-theory and not univalent-combinatorics.

It's not obvious to me either

lowasser · 2025-10-05T05:43:42Z

src/elementary-number-theory/semiring-of-natural-numbers.lagda.md


 ```agda
-module elementary-number-theory.commutative-semiring-of-natural-numbers where
+module elementary-number-theory.semiring-of-natural-numbers where


We don't specify commutativity for the ring of integers, so it seemed more consistent.

Fair enough. Could you just also split up the definitions section to have ℕ-Semiring in its own section?

lowasser · 2025-10-05T05:44:26Z

Also, I broke several files down into more separate sections.

src/elementary-number-theory/equality-integers.lagda.md

src/elementary-number-theory/equality-natural-numbers.lagda.md

src/elementary-number-theory/exponentiation-natural-numbers.lagda.md

fredrik-bakke · 2025-10-06T18:25:19Z

I'm a bit worried that these changes will make it considerably harder to get #1211 merged down the road. But since that PR has been stale for a while and there are likely other merged changes that already make this difficult I'm not sure it should be a blocker. I would be incredibly grateful if someone were to comb through that PR and try and get the more finished parts of it merged though, such as the well-ordering principle of the natural numbers and divisibility among many others.

fredrik-bakke · 2025-10-07T10:27:29Z

I'm a bit worried that these changes will make it considerably harder to get #1211 merged down the road. But since that PR has been stale for a while and there are likely other merged changes that already make this difficult I'm not sure it should be a blocker. I would be incredibly grateful if someone were to comb through that PR and try and get the more finished parts of it merged though, such as the well-ordering principle of the natural numbers and divisibility among many others.

I'd like to get some feedback from another maintainer before this PR is potentially merged. Preferrably @EgbertRijke, but otherwise @VojtechStep, since I expect the former will not respond.

From what I've seen so far, this PR mostly abstracts definitions and fixes a few names. Are these changes necessary for your continued process @lowasser, or could we potentially icebox this PR until progress has been made to merge the other one? Otherwise, should we consider #1211 discontinued and not take it into consideration, @VojtechStep? Keep in mind I have not checked exactly how much overlap there are between these two PRs.

VojtechStep · 2025-10-07T12:23:05Z

I don't think #1211 is becoming mergeable any time soon (it never typechecked, it's been stale for 8 months, and in any case a +17k-3k PR would be very hard to review in one go), and I don't think we should freeze elementary-number-theory until it's done. I'm sure it contains good ideas, and I hope the ideas should be rebasable onto this work, if not the actual code.

lowasser · 2025-10-07T14:58:34Z

These are not necessary changes, just things that have irritated me.

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>

…-integers

fredrik-bakke · 2025-10-08T14:02:03Z

src/elementary-number-theory/distance-natural-numbers.lagda.md

+    triangle-inequality-dist-ℕ m n k
 ```

 ### `dist-ℕ x y` is a solution in `z` to `x + z ＝ y`


Suggested change

### `dist-ℕ x y` is a solution in `z` to `x + z ＝ y`

### `dist-ℕ x y` is a solution in `z` to `x + z ＝ y` when `x ≤ y`

fredrik-bakke · 2025-10-08T14:10:34Z

src/elementary-number-theory/multiplication-natural-numbers.lagda.md

+  is-nonzero-right-factor-mul-ℕ x .zero-ℕ H refl = H (right-zero-law-mul-ℕ x)
+```
+
+### If `(x+1)y = x+1`, then `y = 1`


I'd just like to reiterate that, until #1235 is resolved, using code guards over latex rendered text in headers should not generally be considered an improvement.

fredrik-bakke · 2025-10-08T14:13:44Z

src/elementary-number-theory/poset-of-natural-numbers-ordered-by-divisibility.lagda.md

+The **[poset](order-theory.posets.md) of natural numbers ordered by
+divisibility** consists of the


Suggested change

The **[poset](order-theory.posets.md) of natural numbers ordered by

divisibility** consists of the

The {{#concept "poset of natural numbers ordered by divisibility" Agda=ℕ-Div-Poset}} consists of the

fredrik-bakke · 2025-10-08T14:16:04Z

src/elementary-number-theory/relatively-prime-natural-numbers.lagda.md

+{{#concept "relatively prime" WDID=Q104752 WD="coprime" Disambiguation="natural numbers" Agda=is-relatively-prime-ℕ}}
+if their


Suggested change

{{#concept "relatively prime" WDID=Q104752 WD="coprime" Disambiguation="natural numbers" Agda=is-relatively-prime-ℕ}}

if their

{{#concept "relatively prime" WDID=Q104752 WD="coprime" Disambiguation="natural numbers" Agda=is-relatively-prime-ℕ}},

or **coprime**, if their

fredrik-bakke · 2025-10-08T14:16:37Z

src/elementary-number-theory/relatively-prime-integers.lagda.md

+{{#concept "relatively prime" Disambiguation="integers" Agda=is-relatively-prime-ℤ}}
+if their


Suggested change

{{#concept "relatively prime" Disambiguation="integers" Agda=is-relatively-prime-ℤ}}

if their

{{#concept "relatively prime" Disambiguation="integers" WDID=Q104752 WD="coprime" Agda=is-relatively-prime-ℤ}},

or **coprime**, if their

fredrik-bakke · 2025-10-08T14:30:01Z

src/elementary-number-theory/strong-induction-natural-numbers.lagda.md

-The strong induction principle allows one to assume in the inductive step that
-the inductive hypothesis is satisfied at all smaller values.
+The
+{{#concept "strong induction principle" WDID=Q54506667 WD="principle of complete induction" Agda=strong-ind-ℕ}}


Looking at the wikidata page, I wonder if this identifier also refers to well-founded induction á la https://unimath.github.io/agda-unimath/order-theory.well-founded-relations.html. Maybe we should point both to this identifier

fredrik-bakke · 2025-10-08T14:32:44Z

src/literature/introduction-to-homotopy-type-theory.lagda.md

 open import elementary-number-theory.inequality-natural-numbers using
  ( preserves-leq-left-mul-ℕ
-  ; reflects-order-mul-ℕ)
+  ; reflects-leq-mul-ℕ)


This renaming is fine by me as a temporary solution. See #1575 however.

fredrik-bakke · 2025-10-08T14:48:59Z

src/elementary-number-theory/divisibility-natural-numbers.lagda.md

+    leq-quotient-div-ℕ d (succ-ℕ x) (is-nonzero-succ-ℕ x) H
 ```

 ### If `x` is nonzero, if `d | x` and `d ≠ x`, then `d < x`


Suggested change

### If `x` is nonzero, if `d | x` and `d ≠ x`, then `d < x`

### If `x` is nonzero, `d | x`, and `d ≠ x`, then `d < x`

fredrik-bakke · 2025-10-08T14:56:25Z

I guess I'm just struggling to accept that #1211 is again not going to get merged, and this PR puts a final nail in its coffin. I'll okay these changes for merging.

lowasser added 4 commits October 4, 2025 22:28

Refactor the natural numbers and integers up to present code standards

d13056f

Unabstract divisibility

1133c5d

Unabstract divisibility

7cd6e07

Unabstract deciding if a natural number is prime

9ac8536

lowasser commented Oct 5, 2025

View reviewed changes

Fix link

53bd6e8

lowasser added documentation Improvements or additions to documentation elementary-number-theory refactoring improve naming and removed documentation Improvements or additions to documentation labels Oct 5, 2025

fredrik-bakke reviewed Oct 6, 2025

View reviewed changes

src/elementary-number-theory/equality-integers.lagda.md Outdated Show resolved Hide resolved

fredrik-bakke reviewed Oct 6, 2025

View reviewed changes

src/elementary-number-theory/equality-natural-numbers.lagda.md Outdated Show resolved Hide resolved

fredrik-bakke reviewed Oct 6, 2025

View reviewed changes

src/elementary-number-theory/exponentiation-natural-numbers.lagda.md Show resolved Hide resolved

fredrik-bakke reviewed Oct 6, 2025

View reviewed changes

src/elementary-number-theory/exponentiation-natural-numbers.lagda.md Outdated Show resolved Hide resolved

lowasser and others added 5 commits October 7, 2025 07:59

Apply suggestions from code review

bb96777

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>

Respond to review comment

cd12463

Merge remote-tracking branch 'origin/abstract-integers' into abstract…

d156d96

…-integers

Merge branch 'master' into abstract-integers

7ac5cd0

make pre-commit

168b1c7

fredrik-bakke reviewed Oct 8, 2025

View reviewed changes

fredrik-bakke approved these changes Oct 8, 2025

View reviewed changes

	### `dist-ℕ x y` is a solution in `z` to `x + z ＝ y`
	### `dist-ℕ x y` is a solution in `z` to `x + z ＝ y` when `x ≤ y`

		The **[poset](order-theory.posets.md) of natural numbers ordered by
		divisibility** consists of the

	The **[poset](order-theory.posets.md) of natural numbers ordered by
	divisibility** consists of the
	The {{#concept "poset of natural numbers ordered by divisibility" Agda=ℕ-Div-Poset}} consists of the

		{{#concept "relatively prime" WDID=Q104752 WD="coprime" Disambiguation="natural numbers" Agda=is-relatively-prime-ℕ}}
		if their

		{{#concept "relatively prime" Disambiguation="integers" Agda=is-relatively-prime-ℤ}}
		if their

	### If `x` is nonzero, if `d \| x` and `d ≠ x`, then `d < x`
	### If `x` is nonzero, `d \| x`, and `d ≠ x`, then `d < x`

Refactor the natural numbers and integers up to present code standards #1568

Are you sure you want to change the base?

Refactor the natural numbers and integers up to present code standards #1568

Uh oh!

Conversation

lowasser commented Oct 5, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

lowasser commented Oct 5, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

fredrik-bakke commented Oct 6, 2025

Uh oh!

fredrik-bakke commented Oct 7, 2025

Uh oh!

VojtechStep commented Oct 7, 2025

Uh oh!

lowasser commented Oct 7, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

fredrik-bakke Oct 8, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

fredrik-bakke Oct 8, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

fredrik-bakke commented Oct 8, 2025

Uh oh!

Uh oh!

fredrik-bakke Oct 8, 2025 •

edited

Loading

fredrik-bakke Oct 8, 2025 •

edited

Loading