# The distance between natural numbers

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Eléonore Mangel and Maša Žaucer.

Created on 2022-01-26.

module elementary-number-theory.distance-natural-numbers where

Imports
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.inequality-natural-numbers
open import elementary-number-theory.multiplication-natural-numbers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.strict-inequality-natural-numbers

open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.identity-types
open import foundation.transport-along-identifications
open import foundation.unit-type
open import foundation.universe-levels


## Idea

The distance function between natural numbers measures how far two natural numbers are apart. In the agda-unimath library we often prefer to work with dist-ℕ over the partially defined subtraction operation.

## Definition

dist-ℕ : ℕ → ℕ → ℕ
dist-ℕ zero-ℕ n = n
dist-ℕ (succ-ℕ m) zero-ℕ = succ-ℕ m
dist-ℕ (succ-ℕ m) (succ-ℕ n) = dist-ℕ m n

dist-ℕ' : ℕ → ℕ → ℕ
dist-ℕ' m n = dist-ℕ n m

ap-dist-ℕ :
{m n m' n' : ℕ} → m ＝ m' → n ＝ n' → dist-ℕ m n ＝ dist-ℕ m' n'
ap-dist-ℕ p q = ap-binary dist-ℕ p q


## Properties

### Two natural numbers are equal if and only if their distance is zero

eq-dist-ℕ : (m n : ℕ) → is-zero-ℕ (dist-ℕ m n) → m ＝ n
eq-dist-ℕ zero-ℕ zero-ℕ p = refl
eq-dist-ℕ (succ-ℕ m) (succ-ℕ n) p = ap succ-ℕ (eq-dist-ℕ m n p)

dist-eq-ℕ' : (n : ℕ) → is-zero-ℕ (dist-ℕ n n)
dist-eq-ℕ' zero-ℕ = refl
dist-eq-ℕ' (succ-ℕ n) = dist-eq-ℕ' n

dist-eq-ℕ : (m n : ℕ) → m ＝ n → is-zero-ℕ (dist-ℕ m n)
dist-eq-ℕ m .m refl = dist-eq-ℕ' m

is-one-dist-succ-ℕ : (x : ℕ) → is-one-ℕ (dist-ℕ x (succ-ℕ x))
is-one-dist-succ-ℕ zero-ℕ = refl
is-one-dist-succ-ℕ (succ-ℕ x) = is-one-dist-succ-ℕ x

is-one-dist-succ-ℕ' : (x : ℕ) → is-one-ℕ (dist-ℕ (succ-ℕ x) x)
is-one-dist-succ-ℕ' zero-ℕ = refl
is-one-dist-succ-ℕ' (succ-ℕ x) = is-one-dist-succ-ℕ' x


### The distance function is symmetric

symmetric-dist-ℕ :
(m n : ℕ) → dist-ℕ m n ＝ dist-ℕ n m
symmetric-dist-ℕ zero-ℕ zero-ℕ = refl
symmetric-dist-ℕ zero-ℕ (succ-ℕ n) = refl
symmetric-dist-ℕ (succ-ℕ m) zero-ℕ = refl
symmetric-dist-ℕ (succ-ℕ m) (succ-ℕ n) = symmetric-dist-ℕ m n


### The distance from zero

left-unit-law-dist-ℕ :
(n : ℕ) → dist-ℕ zero-ℕ n ＝ n
left-unit-law-dist-ℕ zero-ℕ = refl
left-unit-law-dist-ℕ (succ-ℕ n) = refl

right-unit-law-dist-ℕ :
(n : ℕ) → dist-ℕ n zero-ℕ ＝ n
right-unit-law-dist-ℕ zero-ℕ = refl
right-unit-law-dist-ℕ (succ-ℕ n) = refl


## The triangle inequality

triangle-inequality-dist-ℕ :
(m n k : ℕ) → (dist-ℕ m n) ≤-ℕ ((dist-ℕ m k) +ℕ (dist-ℕ k n))
triangle-inequality-dist-ℕ zero-ℕ zero-ℕ zero-ℕ = star
triangle-inequality-dist-ℕ zero-ℕ zero-ℕ (succ-ℕ k) = star
triangle-inequality-dist-ℕ zero-ℕ (succ-ℕ n) zero-ℕ =
tr
( leq-ℕ (succ-ℕ n))
( refl-leq-ℕ (succ-ℕ n))
triangle-inequality-dist-ℕ zero-ℕ (succ-ℕ n) (succ-ℕ k) =
concatenate-eq-leq-eq-ℕ
( inv (ap succ-ℕ (left-unit-law-dist-ℕ n)))
( triangle-inequality-dist-ℕ zero-ℕ n k)
( ( ap (succ-ℕ ∘ (_+ℕ (dist-ℕ k n))) (left-unit-law-dist-ℕ k)) ∙
( inv (left-successor-law-add-ℕ k (dist-ℕ k n))))
triangle-inequality-dist-ℕ (succ-ℕ m) zero-ℕ zero-ℕ = refl-leq-ℕ (succ-ℕ m)
triangle-inequality-dist-ℕ (succ-ℕ m) zero-ℕ (succ-ℕ k) =
concatenate-eq-leq-eq-ℕ
( inv (ap succ-ℕ (right-unit-law-dist-ℕ m)))
( triangle-inequality-dist-ℕ m zero-ℕ k)
( ap (succ-ℕ ∘ ((dist-ℕ m k) +ℕ_)) (right-unit-law-dist-ℕ k))
triangle-inequality-dist-ℕ (succ-ℕ m) (succ-ℕ n) zero-ℕ =
concatenate-leq-eq-ℕ
( dist-ℕ m n)
( transitive-leq-ℕ
( dist-ℕ m n)
( succ-ℕ ((dist-ℕ m zero-ℕ) +ℕ (dist-ℕ zero-ℕ n)))
( succ-ℕ (succ-ℕ ((dist-ℕ m zero-ℕ) +ℕ (dist-ℕ zero-ℕ n))))
( succ-leq-ℕ (succ-ℕ ((dist-ℕ m zero-ℕ) +ℕ (dist-ℕ zero-ℕ n))))
( transitive-leq-ℕ
( dist-ℕ m n)
( (dist-ℕ m zero-ℕ) +ℕ (dist-ℕ zero-ℕ n))
( succ-ℕ ((dist-ℕ m zero-ℕ) +ℕ (dist-ℕ zero-ℕ n)))
( succ-leq-ℕ ((dist-ℕ m zero-ℕ) +ℕ (dist-ℕ zero-ℕ n)))
( triangle-inequality-dist-ℕ m n zero-ℕ)))
( ( ap
( succ-ℕ ∘ succ-ℕ)
( ap-add-ℕ (right-unit-law-dist-ℕ m) (left-unit-law-dist-ℕ n))) ∙
( inv (left-successor-law-add-ℕ m (succ-ℕ n))))
triangle-inequality-dist-ℕ (succ-ℕ m) (succ-ℕ n) (succ-ℕ k) =
triangle-inequality-dist-ℕ m n k


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

is-additive-right-inverse-dist-ℕ :
(x y : ℕ) → x ≤-ℕ y → x +ℕ (dist-ℕ x y) ＝ y
is-additive-right-inverse-dist-ℕ zero-ℕ zero-ℕ H = refl
is-additive-right-inverse-dist-ℕ zero-ℕ (succ-ℕ y) star =
is-additive-right-inverse-dist-ℕ (succ-ℕ x) (succ-ℕ y) H =
( left-successor-law-add-ℕ x (dist-ℕ x y)) ∙
( ap succ-ℕ (is-additive-right-inverse-dist-ℕ x y H))

(x y z : ℕ) → x +ℕ y ＝ z → x ＝ dist-ℕ y z
rewrite-left-add-dist-ℕ zero-ℕ zero-ℕ .zero-ℕ refl = refl
rewrite-left-add-dist-ℕ zero-ℕ (succ-ℕ y) .(succ-ℕ (zero-ℕ +ℕ y)) refl =
( inv (dist-eq-ℕ' y)) ∙
( inv (ap (dist-ℕ (succ-ℕ y)) (left-unit-law-add-ℕ (succ-ℕ y))))
rewrite-left-add-dist-ℕ (succ-ℕ x) zero-ℕ .(succ-ℕ x) refl = refl
rewrite-left-add-dist-ℕ (succ-ℕ x) (succ-ℕ y) ._ refl =
rewrite-left-add-dist-ℕ (succ-ℕ x) y ((succ-ℕ x) +ℕ y) refl

(x y z : ℕ) → y ≤-ℕ z → x ＝ dist-ℕ y z → x +ℕ y ＝ z
rewrite-left-dist-add-ℕ .(dist-ℕ y z) y z H refl =
( commutative-add-ℕ (dist-ℕ y z) y) ∙

(x y z : ℕ) → x +ℕ y ＝ z → y ＝ dist-ℕ x z
rewrite-right-add-dist-ℕ x y z p =

(x y z : ℕ) → x ≤-ℕ z → y ＝ dist-ℕ x z → x +ℕ y ＝ z
rewrite-right-dist-add-ℕ x .(dist-ℕ x z) z H refl =

is-difference-dist-ℕ :
(x y : ℕ) → x ≤-ℕ y → x +ℕ (dist-ℕ x y) ＝ y
is-difference-dist-ℕ zero-ℕ zero-ℕ H = refl
is-difference-dist-ℕ zero-ℕ (succ-ℕ y) H = left-unit-law-add-ℕ (succ-ℕ y)
is-difference-dist-ℕ (succ-ℕ x) (succ-ℕ y) H =
( left-successor-law-add-ℕ x (dist-ℕ x y)) ∙
( ap succ-ℕ (is-difference-dist-ℕ x y H))

is-difference-dist-ℕ' :
(x y : ℕ) → x ≤-ℕ y → (dist-ℕ x y) +ℕ x ＝ y
is-difference-dist-ℕ' x y H =
( commutative-add-ℕ (dist-ℕ x y) x) ∙
( is-difference-dist-ℕ x y H)


### The distance from n to n + m is m

dist-add-ℕ : (x y : ℕ) → dist-ℕ x (x +ℕ y) ＝ y
dist-add-ℕ x y = inv (rewrite-right-add-dist-ℕ x y (x +ℕ y) refl)

dist-add-ℕ' : (x y : ℕ) → dist-ℕ (x +ℕ y) x ＝ y
dist-add-ℕ' x y = symmetric-dist-ℕ (x +ℕ y) x ∙ dist-add-ℕ x y


### If three elements are ordered linearly, then their distances add up

triangle-equality-dist-ℕ :
(x y z : ℕ) → (x ≤-ℕ y) → (y ≤-ℕ z) →
(dist-ℕ x y) +ℕ (dist-ℕ y z) ＝ dist-ℕ x z
triangle-equality-dist-ℕ zero-ℕ zero-ℕ zero-ℕ H1 H2 = refl
triangle-equality-dist-ℕ zero-ℕ zero-ℕ (succ-ℕ z) star star =
triangle-equality-dist-ℕ zero-ℕ (succ-ℕ y) (succ-ℕ z) star H2 =
left-successor-law-add-ℕ y (dist-ℕ y z) ∙
ap succ-ℕ (is-additive-right-inverse-dist-ℕ y z H2)
triangle-equality-dist-ℕ (succ-ℕ x) (succ-ℕ y) (succ-ℕ z) H1 H2 =
triangle-equality-dist-ℕ x y z H1 H2

cases-dist-ℕ :
(x y z : ℕ) → UU lzero
cases-dist-ℕ x y z =
( (dist-ℕ x y) +ℕ (dist-ℕ y z) ＝ dist-ℕ x z) +
( ( (dist-ℕ y z) +ℕ (dist-ℕ x z) ＝ dist-ℕ x y) +
( (dist-ℕ x z) +ℕ (dist-ℕ x y) ＝ dist-ℕ y z))

is-total-dist-ℕ :
(x y z : ℕ) → cases-dist-ℕ x y z
is-total-dist-ℕ x y z with order-three-elements-ℕ x y z
is-total-dist-ℕ x y z | inl (inl (pair H1 H2)) =
inl (triangle-equality-dist-ℕ x y z H1 H2)
is-total-dist-ℕ x y z | inl (inr (pair H1 H2)) =
inr
( inl
( ( commutative-add-ℕ (dist-ℕ y z) (dist-ℕ x z)) ∙
( ( ap ((dist-ℕ x z) +ℕ_) (symmetric-dist-ℕ y z)) ∙
( triangle-equality-dist-ℕ x z y H1 H2))))
is-total-dist-ℕ x y z | inr (inl (inl (pair H1 H2))) =
inr
( inl
( ( ap ((dist-ℕ y z) +ℕ_) (symmetric-dist-ℕ x z)) ∙
( ( triangle-equality-dist-ℕ y z x H1 H2) ∙
( symmetric-dist-ℕ y x))))
is-total-dist-ℕ x y z | inr (inl (inr (pair H1 H2))) =
inr
( inr
( ( ap ((dist-ℕ x z) +ℕ_) (symmetric-dist-ℕ x y)) ∙
( ( commutative-add-ℕ (dist-ℕ x z) (dist-ℕ y x)) ∙
( triangle-equality-dist-ℕ y x z H1 H2))))
is-total-dist-ℕ x y z | inr (inr (inl (pair H1 H2))) =
inr
( inr
( ( ap (_+ℕ (dist-ℕ x y)) (symmetric-dist-ℕ x z)) ∙
( ( triangle-equality-dist-ℕ z x y H1 H2) ∙
( symmetric-dist-ℕ z y))))
is-total-dist-ℕ x y z | inr (inr (inr (pair H1 H2))) =
inl
( ( ap-add-ℕ (symmetric-dist-ℕ x y) (symmetric-dist-ℕ y z)) ∙
( ( commutative-add-ℕ (dist-ℕ y x) (dist-ℕ z y)) ∙
( ( triangle-equality-dist-ℕ z y x H1 H2) ∙
( symmetric-dist-ℕ z x))))


### If x ≤ y then the distance between x and y is less than y

leq-dist-ℕ :
(x y : ℕ) → x ≤-ℕ y → dist-ℕ x y ≤-ℕ y
leq-dist-ℕ zero-ℕ zero-ℕ H = refl-leq-ℕ zero-ℕ
leq-dist-ℕ zero-ℕ (succ-ℕ y) H = refl-leq-ℕ y
leq-dist-ℕ (succ-ℕ x) (succ-ℕ y) H =
transitive-leq-ℕ (dist-ℕ x y) y (succ-ℕ y) (succ-leq-ℕ y) (leq-dist-ℕ x y H)


### If x < b and y < b, then dist-ℕ x y < b

strict-upper-bound-dist-ℕ :
(b x y : ℕ) → le-ℕ x b → le-ℕ y b → le-ℕ (dist-ℕ x y) b
strict-upper-bound-dist-ℕ (succ-ℕ b) zero-ℕ y H K = K
strict-upper-bound-dist-ℕ (succ-ℕ b) (succ-ℕ x) zero-ℕ H K = H
strict-upper-bound-dist-ℕ (succ-ℕ b) (succ-ℕ x) (succ-ℕ y) H K =
preserves-le-succ-ℕ (dist-ℕ x y) b (strict-upper-bound-dist-ℕ b x y H K)


### If x < y then dist-ℕ x (succ-ℕ y) = succ-ℕ (dist-ℕ x y)

right-successor-law-dist-ℕ :
(x y : ℕ) → leq-ℕ x y → dist-ℕ x (succ-ℕ y) ＝ succ-ℕ (dist-ℕ x y)
right-successor-law-dist-ℕ zero-ℕ zero-ℕ star = refl
right-successor-law-dist-ℕ zero-ℕ (succ-ℕ y) star = refl
right-successor-law-dist-ℕ (succ-ℕ x) (succ-ℕ y) H =
right-successor-law-dist-ℕ x y H

left-successor-law-dist-ℕ :
(x y : ℕ) → leq-ℕ y x → dist-ℕ (succ-ℕ x) y ＝ succ-ℕ (dist-ℕ x y)
left-successor-law-dist-ℕ zero-ℕ zero-ℕ star = refl
left-successor-law-dist-ℕ (succ-ℕ x) zero-ℕ star = refl
left-successor-law-dist-ℕ (succ-ℕ x) (succ-ℕ y) H =
left-successor-law-dist-ℕ x y H


### dist-ℕ is translation invariant

translation-invariant-dist-ℕ :
(k m n : ℕ) → dist-ℕ (k +ℕ m) (k +ℕ n) ＝ dist-ℕ m n
translation-invariant-dist-ℕ zero-ℕ m n =
translation-invariant-dist-ℕ (succ-ℕ k) m n =
( translation-invariant-dist-ℕ k m n)

translation-invariant-dist-ℕ' :
(k m n : ℕ) → dist-ℕ (m +ℕ k) (n +ℕ k) ＝ dist-ℕ m n
translation-invariant-dist-ℕ' k m n =
( translation-invariant-dist-ℕ k m n)


### dist-ℕ is linear with respect to scalar multiplication

left-distributive-mul-dist-ℕ :
(m n k : ℕ) → k *ℕ (dist-ℕ m n) ＝ dist-ℕ (k *ℕ m) (k *ℕ n)
left-distributive-mul-dist-ℕ zero-ℕ zero-ℕ zero-ℕ = refl
left-distributive-mul-dist-ℕ zero-ℕ zero-ℕ (succ-ℕ k) =
left-distributive-mul-dist-ℕ zero-ℕ zero-ℕ k
left-distributive-mul-dist-ℕ zero-ℕ (succ-ℕ n) zero-ℕ = refl
left-distributive-mul-dist-ℕ zero-ℕ (succ-ℕ n) (succ-ℕ k) =
ap
( dist-ℕ' ((succ-ℕ k) *ℕ (succ-ℕ n)))
( inv (right-zero-law-mul-ℕ (succ-ℕ k)))
left-distributive-mul-dist-ℕ (succ-ℕ m) zero-ℕ zero-ℕ = refl
left-distributive-mul-dist-ℕ (succ-ℕ m) zero-ℕ (succ-ℕ k) =
ap
( dist-ℕ ((succ-ℕ k) *ℕ (succ-ℕ m)))
( inv (right-zero-law-mul-ℕ (succ-ℕ k)))
left-distributive-mul-dist-ℕ (succ-ℕ m) (succ-ℕ n) zero-ℕ = refl
left-distributive-mul-dist-ℕ (succ-ℕ m) (succ-ℕ n) (succ-ℕ k) =
inv
( ( 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)))))

right-distributive-mul-dist-ℕ :
(x y k : ℕ) → (dist-ℕ x y) *ℕ k ＝ dist-ℕ (x *ℕ k) (y *ℕ k)
right-distributive-mul-dist-ℕ x y k =
( commutative-mul-ℕ (dist-ℕ x y) k) ∙
( ( left-distributive-mul-dist-ℕ x y k) ∙
( ap-dist-ℕ (commutative-mul-ℕ k x) (commutative-mul-ℕ k y)))