Refactor elementary number theory

src/elementary-number-theory.lagda.md

@@ -76,6 +76,7 @@ open import elementary-number-theory.initial-segments-natural-numbers public
 open import elementary-number-theory.integer-fractions public
 open import elementary-number-theory.integer-partitions public
 open import elementary-number-theory.integers public
+open import elementary-number-theory.irrationality-square-root-of-2 public
 open import elementary-number-theory.jacobi-symbol public
 open import elementary-number-theory.kolakoski-sequence public
 open import elementary-number-theory.legendre-symbol public
@@ -112,6 +113,7 @@ open import elementary-number-theory.nonzero-integers public
 open import elementary-number-theory.nonzero-natural-numbers public
 open import elementary-number-theory.nonzero-rational-numbers public
 open import elementary-number-theory.ordinal-induction-natural-numbers public
+open import elementary-number-theory.parity-integers public
 open import elementary-number-theory.parity-natural-numbers public
 open import elementary-number-theory.peano-arithmetic public
 open import elementary-number-theory.pisano-periods public

src/elementary-number-theory/absolute-value-integers.lagda.md

@@ -178,36 +178,36 @@ is-nonzero-abs-ℤ :
 is-nonzero-abs-ℤ (inr (inr x)) H = is-nonzero-succ-ℕ x
 ```
 
-### The absolute value function is multiplicative
+### The absolute value distributes over multiplication
 
 ```agda
-multiplicative-abs-ℤ' :
-  (x y : ℤ) → abs-ℤ (explicit-mul-ℤ x y) ＝ (abs-ℤ x) *ℕ (abs-ℤ y)
-multiplicative-abs-ℤ' (inl x) (inl y) =
+distributive-abs-mul-ℤ' :
+  (x y : ℤ) → abs-ℤ (explicit-mul-ℤ x y) ＝ abs-ℤ x *ℕ abs-ℤ y
+distributive-abs-mul-ℤ' (inl x) (inl y) =
   abs-int-ℕ _
-multiplicative-abs-ℤ' (inl x) (inr (inl star)) =
+distributive-abs-mul-ℤ' (inl x) (inr (inl star)) =
   inv (right-zero-law-mul-ℕ x)
-multiplicative-abs-ℤ' (inl x) (inr (inr y)) =
+distributive-abs-mul-ℤ' (inl x) (inr (inr y)) =
   ( abs-neg-ℤ (inl ((x *ℕ (succ-ℕ y)) +ℕ y))) ∙
   ( abs-int-ℕ ((succ-ℕ x) *ℕ (succ-ℕ y)))
-multiplicative-abs-ℤ' (inr (inl star)) (inl y) =
+distributive-abs-mul-ℤ' (inr (inl star)) (inl y) =
   refl
-multiplicative-abs-ℤ' (inr (inr x)) (inl y) =
+distributive-abs-mul-ℤ' (inr (inr x)) (inl y) =
   ( abs-neg-ℤ (inl ((x *ℕ (succ-ℕ y)) +ℕ y))) ∙
   ( abs-int-ℕ (succ-ℕ ((x *ℕ (succ-ℕ y)) +ℕ y)))
-multiplicative-abs-ℤ' (inr (inl star)) (inr (inl star)) =
+distributive-abs-mul-ℤ' (inr (inl star)) (inr (inl star)) =
   refl
-multiplicative-abs-ℤ' (inr (inl star)) (inr (inr x)) =
+distributive-abs-mul-ℤ' (inr (inl star)) (inr (inr x)) =
   refl
-multiplicative-abs-ℤ' (inr (inr x)) (inr (inl star)) =
+distributive-abs-mul-ℤ' (inr (inr x)) (inr (inl star)) =
   inv (right-zero-law-mul-ℕ (succ-ℕ x))
-multiplicative-abs-ℤ' (inr (inr x)) (inr (inr y)) =
+distributive-abs-mul-ℤ' (inr (inr x)) (inr (inr y)) =
   abs-int-ℕ _
 
-multiplicative-abs-ℤ :
-  (x y : ℤ) → abs-ℤ (x *ℤ y) ＝ (abs-ℤ x) *ℕ (abs-ℤ y)
-multiplicative-abs-ℤ x y =
-  ap abs-ℤ (compute-mul-ℤ x y) ∙ multiplicative-abs-ℤ' x y
+distributive-abs-mul-ℤ :
+  (x y : ℤ) → abs-ℤ (x *ℤ y) ＝ abs-ℤ x *ℕ abs-ℤ y
+distributive-abs-mul-ℤ x y =
+  ap abs-ℤ (compute-mul-ℤ x y) ∙ distributive-abs-mul-ℤ' x y
 ```
 
 ### `|(-x)y| ＝ |xy|`

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

@@ -341,6 +341,25 @@ abstract
       associative-add-ℤ
 ```
 
+### Swapping the order of iterated addition
+
+```agda
+abstract
+  right-swap-add-ℤ :
+    (x y z : ℤ) → (x +ℤ y) +ℤ z ＝ (x +ℤ z) +ℤ y
+  right-swap-add-ℤ x y z =
+    associative-add-ℤ x y z ∙
+    ap (x +ℤ_) (commutative-add-ℤ y z) ∙
+    inv (associative-add-ℤ x z y)
+
+  left-swap-add-ℤ :
+    (x y z : ℤ) → x +ℤ (y +ℤ z) ＝ y +ℤ (x +ℤ z)
+  left-swap-add-ℤ x y z =
+    inv (associative-add-ℤ x y z) ∙
+    ap (_+ℤ z) (commutative-add-ℤ x y) ∙
+    associative-add-ℤ y x z
+```
+
 ### Addition by `x` is a binary equivalence
 
 ```agda

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

@@ -138,6 +138,25 @@ abstract
       associative-add-ℕ
 ```
 
+### Swapping iterated addition
+
+```agda
+abstract
+  right-swap-add-ℕ :
+    (x y z : ℕ) → (x +ℕ y) +ℕ z ＝ (x +ℕ z) +ℕ y
+  right-swap-add-ℕ x y z =
+    associative-add-ℕ x y z ∙
+    ap (add-ℕ x) (commutative-add-ℕ y z) ∙
+    inv (associative-add-ℕ x z y)
+
+  left-swap-add-ℕ :
+    (x y z : ℕ) → x +ℕ (y +ℕ z) ＝ y +ℕ (x +ℕ z)
+  left-swap-add-ℕ x y z =
+    inv (associative-add-ℕ x y z) ∙
+    ap (add-ℕ' z) (commutative-add-ℕ x y) ∙
+    associative-add-ℕ y x z
+```
+
 ### Addition by a fixed element on either side is injective
 
 ```agda

src/elementary-number-theory/bezouts-lemma-integers.lagda.md

@@ -117,7 +117,7 @@ bezouts-lemma-eqn-to-int x y H =
                     ( minimal-positive-distance-y-coeff (abs-ℤ x) (abs-ℤ y) H)))
                 ( abs-ℤ y)))
           ( inv
-            ( multiplicative-abs-ℤ
+            ( distributive-abs-mul-ℤ
               ( int-ℕ (minimal-positive-distance-x-coeff (abs-ℤ x) (abs-ℤ y) H))
               ( x))))
     ＝ dist-ℕ
@@ -138,7 +138,7 @@ bezouts-lemma-eqn-to-int x y H =
                   ( minimal-positive-distance-x-coeff (abs-ℤ x) (abs-ℤ y) H))
                 ( x))))
           ( inv
-            ( multiplicative-abs-ℤ
+            ( distributive-abs-mul-ℤ
               ( int-ℕ (minimal-positive-distance-y-coeff (abs-ℤ x) (abs-ℤ y) H))
               ( y))))
 

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

@@ -350,11 +350,11 @@ left-distributive-mul-dist-ℕ (succ-ℕ m) (succ-ℕ n) (succ-ℕ k) =
     ( ( ap-dist-ℕ
         ( right-successor-law-mul-ℕ (succ-ℕ k) m)
         ( right-successor-law-mul-ℕ (succ-ℕ k) n)) ∙
-      ( ( translation-invariant-dist-ℕ
-          ( succ-ℕ k)
-          ( (succ-ℕ k) *ℕ m)
-          ( (succ-ℕ k) *ℕ n)) ∙
-        ( inv (left-distributive-mul-dist-ℕ m n (succ-ℕ k)))))
+      ( translation-invariant-dist-ℕ'
+        ( succ-ℕ k)
+        ( succ-ℕ k *ℕ m)
+        ( succ-ℕ k *ℕ n)) ∙
+      ( inv (left-distributive-mul-dist-ℕ m n (succ-ℕ k))))
 
 right-distributive-mul-dist-ℕ :
   (x y k : ℕ) → (dist-ℕ x y) *ℕ k ＝ dist-ℕ (x *ℕ k) (y *ℕ k)

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

@@ -202,16 +202,6 @@ is-zero-is-zero-div-ℤ : (x k : ℤ) → div-ℤ k x → is-zero-ℤ k → is-z
 is-zero-is-zero-div-ℤ x .zero-ℤ k-div-x refl = is-zero-div-zero-ℤ x k-div-x
 ```
 
-### If `x` divides both `y` and `z`, then it divides `y + z`
-
-```agda
-div-add-ℤ : (x y z : ℤ) → div-ℤ x y → div-ℤ x z → div-ℤ x (y +ℤ z)
-pr1 (div-add-ℤ x y z (pair d p) (pair e q)) = d +ℤ e
-pr2 (div-add-ℤ x y z (pair d p) (pair e q)) =
-  ( right-distributive-mul-add-ℤ d e x) ∙
-  ( ap-add-ℤ p q)
-```
-
 ### If `x` divides `y` then `x` divides any multiple of `y`
 
 ```agda
@@ -246,6 +236,40 @@ pr2 (neg-div-ℤ x y (pair d p)) =
       by p
 ```
 
+### If `x` divides both `y` and `z`, then it divides `y + z`
+
+```agda
+div-add-ℤ : (x y z : ℤ) → div-ℤ x y → div-ℤ x z → div-ℤ x (y +ℤ z)
+pr1 (div-add-ℤ x y z (pair d p) (pair e q)) = d +ℤ e
+pr2 (div-add-ℤ x y z (pair d p) (pair e q)) =
+  ( right-distributive-mul-add-ℤ d e x) ∙
+  ( ap-add-ℤ p q)
+
+div-right-summand-ℤ :
+  (x y z : ℤ) → div-ℤ x y → div-ℤ x (y +ℤ z) → div-ℤ x z
+div-right-summand-ℤ x y z H K =
+  tr
+    ( div-ℤ x)
+    ( is-retraction-left-add-neg-ℤ y z)
+    ( div-add-ℤ x
+      ( neg-ℤ y)
+      ( y +ℤ z)
+      ( div-neg-ℤ x y H)
+      ( K))
+
+div-left-summand-ℤ :
+  (x y z : ℤ) → div-ℤ x z → div-ℤ x (y +ℤ z) → div-ℤ x y
+div-left-summand-ℤ x y z H K =
+  tr
+    ( div-ℤ x)
+    ( is-retraction-right-add-neg-ℤ z y)
+    ( div-add-ℤ x
+      ( y +ℤ z)
+      ( neg-ℤ z)
+      ( K)
+      ( div-neg-ℤ x z H))
+```
+
 ### Multiplication preserves divisibility
 
 ```agda

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

@@ -206,15 +206,12 @@ convert-based-succ-based-ℕ
         ( succ-ℕ (convert-based-ℕ (succ-ℕ k) (succ-based-ℕ (succ-ℕ k) n))))
           +ℕ_)
     ( is-zero-nat-zero-Fin {k})) ∙
-  ( ( ap
-      ( ((succ-ℕ k) *ℕ_) ∘ succ-ℕ)
-      ( convert-based-succ-based-ℕ (succ-ℕ k) n)) ∙
-    ( ( right-successor-law-mul-ℕ
-        ( succ-ℕ k)
-        ( succ-ℕ (convert-based-ℕ (succ-ℕ k) n))) ∙
-      ( commutative-add-ℕ
-        ( succ-ℕ k)
-        ( (succ-ℕ k) *ℕ (succ-ℕ (convert-based-ℕ (succ-ℕ k) n))))))
+  ( ap
+    ( ((succ-ℕ k) *ℕ_) ∘ succ-ℕ)
+    ( convert-based-succ-based-ℕ (succ-ℕ k) n)) ∙
+  ( ( right-successor-law-mul-ℕ
+      ( succ-ℕ k)
+      ( succ-ℕ (convert-based-ℕ (succ-ℕ k) n))))
 
 is-section-inv-convert-based-ℕ :
   (k n : ℕ) → convert-based-ℕ (succ-ℕ k) (inv-convert-based-ℕ k n) ＝ n

src/elementary-number-theory/integer-fractions.lagda.md

@@ -10,6 +10,7 @@ module elementary-number-theory.integer-fractions where
 open import elementary-number-theory.greatest-common-divisor-integers
 open import elementary-number-theory.integers
 open import elementary-number-theory.multiplication-integers
+open import elementary-number-theory.natural-numbers
 open import elementary-number-theory.nonzero-integers
 open import elementary-number-theory.positive-and-negative-integers
 open import elementary-number-theory.positive-integers
@@ -64,6 +65,10 @@ denominator-fraction-ℤ x = pr1 (positive-denominator-fraction-ℤ x)
 is-positive-denominator-fraction-ℤ :
   (x : fraction-ℤ) → is-positive-ℤ (denominator-fraction-ℤ x)
 is-positive-denominator-fraction-ℤ x = pr2 (positive-denominator-fraction-ℤ x)
+
+nat-denominator-fraction-ℤ : fraction-ℤ → ℕ
+nat-denominator-fraction-ℤ x =
+  nat-positive-ℤ (positive-denominator-fraction-ℤ x)
 ```
 
 ### Inclusion of the integers
@@ -129,12 +134,35 @@ fraction-ℤ-Set : Set lzero
 fraction-ℤ-Set = fraction-ℤ , is-set-fraction-ℤ
 ```
 
+### The standard equivalence relation on integer fractions
+
+Two integer fractions `a/b` and `c/d` are said to be equivalent if they satisfy
+the equation
+
+```text
+  ad ＝ cb.
+```
+
+This relation is obviously reflexive and symmetric. To see that it is
+transitive, suppose that `a/b ~ c/d` and that `c/d ~ e/f`. Since `d` is
+positive, we have the implication
+
+```text
+  (af)d ＝ (eb)d → af ＝ eb.
+```
+
+Therefore it suffices to show that `(af)d ＝ (eb)d`. To see this, we calculate
+
+```text
+  (af)d ＝ (ad)f ＝ (cb)f ＝ (cf)b ＝ (ed)b ＝ (eb)d.
+```
+
 ```agda
 sim-fraction-ℤ-Prop : fraction-ℤ → fraction-ℤ → Prop lzero
 sim-fraction-ℤ-Prop x y =
   Id-Prop ℤ-Set
-    ((numerator-fraction-ℤ x) *ℤ (denominator-fraction-ℤ y))
-    ((numerator-fraction-ℤ y) *ℤ (denominator-fraction-ℤ x))
+    ( numerator-fraction-ℤ x *ℤ denominator-fraction-ℤ y)
+    ( numerator-fraction-ℤ y *ℤ denominator-fraction-ℤ x)
 
 sim-fraction-ℤ : fraction-ℤ → fraction-ℤ → UU lzero
 sim-fraction-ℤ x y = type-Prop (sim-fraction-ℤ-Prop x y)
@@ -150,54 +178,11 @@ symmetric-sim-fraction-ℤ x y r = inv r
 
 abstract
   transitive-sim-fraction-ℤ : is-transitive sim-fraction-ℤ
-  transitive-sim-fraction-ℤ x y z s r =
-    is-injective-right-mul-ℤ
-      ( denominator-fraction-ℤ y)
+  transitive-sim-fraction-ℤ (a , b , pb) y@(c , d , pd) (e , f , pf) s r =
+    is-injective-right-mul-ℤ d
       ( is-nonzero-denominator-fraction-ℤ y)
-      ( ( associative-mul-ℤ
-          ( numerator-fraction-ℤ x)
-          ( denominator-fraction-ℤ z)
-          ( denominator-fraction-ℤ y)) ∙
-        ( ap
-          ( (numerator-fraction-ℤ x) *ℤ_)
-          ( commutative-mul-ℤ
-            ( denominator-fraction-ℤ z)
-            ( denominator-fraction-ℤ y))) ∙
-        ( inv
-          ( associative-mul-ℤ
-            ( numerator-fraction-ℤ x)
-            ( denominator-fraction-ℤ y)
-            ( denominator-fraction-ℤ z))) ∙
-        ( ap ( _*ℤ (denominator-fraction-ℤ z)) r) ∙
-        ( associative-mul-ℤ
-          ( numerator-fraction-ℤ y)
-          ( denominator-fraction-ℤ x)
-          ( denominator-fraction-ℤ z)) ∙
-        ( ap
-          ( (numerator-fraction-ℤ y) *ℤ_)
-          ( commutative-mul-ℤ
-            ( denominator-fraction-ℤ x)
-            ( denominator-fraction-ℤ z))) ∙
-        ( inv
-          ( associative-mul-ℤ
-            ( numerator-fraction-ℤ y)
-            ( denominator-fraction-ℤ z)
-            ( denominator-fraction-ℤ x))) ∙
-        ( ap (_*ℤ (denominator-fraction-ℤ x)) s) ∙
-        ( associative-mul-ℤ
-          ( numerator-fraction-ℤ z)
-          ( denominator-fraction-ℤ y)
-          ( denominator-fraction-ℤ x)) ∙
-        ( ap
-          ( (numerator-fraction-ℤ z) *ℤ_)
-          ( commutative-mul-ℤ
-            ( denominator-fraction-ℤ y)
-            ( denominator-fraction-ℤ x))) ∙
-        ( inv
-          ( associative-mul-ℤ
-            ( numerator-fraction-ℤ z)
-            ( denominator-fraction-ℤ x)
-            ( denominator-fraction-ℤ y))))
+      ( right-swap-mul-ℤ a f d ∙ ap (_*ℤ f) r ∙
+        right-swap-mul-ℤ c b f ∙ ap (_*ℤ b) s ∙ right-swap-mul-ℤ e d b)
 
 equivalence-relation-sim-fraction-ℤ : equivalence-relation lzero fraction-ℤ
 pr1 equivalence-relation-sim-fraction-ℤ = sim-fraction-ℤ-Prop