The distance between integers

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Bryan Lu, Victor Blanchi and malarbol.

Created on 2022-01-26.
Last modified on 2024-03-28.

module elementary-number-theory.distance-integers where
open import elementary-number-theory.absolute-value-integers
open import elementary-number-theory.difference-integers
open import elementary-number-theory.distance-natural-numbers
open import elementary-number-theory.integers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.nonnegative-integers
open import elementary-number-theory.positive-and-negative-integers
open import elementary-number-theory.positive-integers

open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
open import foundation.coproduct-types
open import foundation.identity-types


The distance function between integers measures how far two integers are apart.


dist-ℤ :     
dist-ℤ x y = abs-ℤ (x -ℤ y)

ap-dist-ℤ :
  {x x' y y' : }  x  x'  y  y'  dist-ℤ x y  dist-ℤ x' y'
ap-dist-ℤ p q = ap-binary dist-ℤ p q

left-zero-law-dist-ℤ : (x : )  dist-ℤ zero-ℤ x  abs-ℤ x
left-zero-law-dist-ℤ x = ap abs-ℤ (left-zero-law-diff-ℤ x)  abs-neg-ℤ x

right-zero-law-dist-ℤ : (x : )  dist-ℤ x zero-ℤ  abs-ℤ x
right-zero-law-dist-ℤ x = ap abs-ℤ (right-zero-law-diff-ℤ x)

dist-int-ℕ :
  (x y : )  dist-ℤ (int-ℕ x) (int-ℕ y)  dist-ℕ x y
dist-int-ℕ zero-ℕ zero-ℕ = refl
dist-int-ℕ zero-ℕ (succ-ℕ y) = left-zero-law-dist-ℤ (int-ℕ (succ-ℕ y))
dist-int-ℕ (succ-ℕ x) zero-ℕ = right-zero-law-dist-ℤ (int-ℕ (succ-ℕ x))
dist-int-ℕ (succ-ℕ x) (succ-ℕ y) =
  ( ( ap-dist-ℤ (inv (succ-int-ℕ x)) (inv (succ-int-ℕ y))) 
    ( ap abs-ℤ (diff-succ-ℤ (int-ℕ x) (int-ℕ y)))) 
  ( dist-int-ℕ x y)

dist-abs-ℤ :
  (x y : )  (H : is-nonnegative-ℤ x)  (K : is-nonnegative-ℤ y) 
  dist-ℕ (abs-ℤ x) (abs-ℤ y)  dist-ℤ x y
dist-abs-ℤ (inr (inl _)) y H K =
    dist-ℕ 0 (abs-ℤ y)
     abs-ℤ y
      by left-unit-law-dist-ℕ (abs-ℤ y)
     dist-ℤ (zero-ℤ) y
      by inv (left-zero-law-dist-ℤ y)
dist-abs-ℤ (inr (inr x)) (inr (inl _)) H K =
    dist-ℕ (abs-ℤ (inr (inr x))) 0
     succ-ℕ x
      by right-unit-law-dist-ℕ (abs-ℤ (inr (inr x)))
     dist-ℤ (inr (inr x)) zero-ℤ
      by inv (right-zero-law-dist-ℤ (inr (inr x)))
dist-abs-ℤ (inr (inr x)) (inr (inr y)) H K =
    dist-ℕ (succ-ℕ x) (succ-ℕ y)
     dist-ℤ (int-ℕ (succ-ℕ x)) (int-ℕ (succ-ℕ y))
      by inv (dist-int-ℕ (succ-ℕ x) (succ-ℕ y))

Recent changes