The absolute value function on the integers
Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Bryan Lu and malarbol.
Created on 2022-01-26.
Last modified on 2024-03-28.
module elementary-number-theory.absolute-value-integers where
Imports
open import elementary-number-theory.addition-integers open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.inequality-natural-numbers open import elementary-number-theory.integers open import elementary-number-theory.multiplication-integers open import elementary-number-theory.multiplication-natural-numbers open import elementary-number-theory.natural-numbers open import elementary-number-theory.nonnegative-integers open import elementary-number-theory.positive-integers open import foundation.action-on-identifications-functions open import foundation.coproduct-types open import foundation.function-types open import foundation.identity-types open import foundation.unit-type
Idea
The absolute value of an integer is the natural number with the same distance
from 0
.
Definition
abs-ℤ : ℤ → ℕ abs-ℤ (inl x) = succ-ℕ x abs-ℤ (inr (inl star)) = zero-ℕ abs-ℤ (inr (inr x)) = succ-ℕ x int-abs-ℤ : ℤ → ℤ int-abs-ℤ = int-ℕ ∘ abs-ℤ
Properties
The absolute value of int-ℕ n
is n
itself
abs-int-ℕ : (n : ℕ) → abs-ℤ (int-ℕ n) = n abs-int-ℕ zero-ℕ = refl abs-int-ℕ (succ-ℕ n) = refl
|-x| = |x|
abs-neg-ℤ : (x : ℤ) → abs-ℤ (neg-ℤ x) = abs-ℤ x abs-neg-ℤ (inl x) = refl abs-neg-ℤ (inr (inl star)) = refl abs-neg-ℤ (inr (inr x)) = refl
If x
is nonnegative, then int-abs-ℤ x = x
int-abs-is-nonnegative-ℤ : (x : ℤ) → is-nonnegative-ℤ x → int-abs-ℤ x = x int-abs-is-nonnegative-ℤ (inr (inl star)) h = refl int-abs-is-nonnegative-ℤ (inr (inr x)) h = refl
|x| = 0
if and only if x = 0
eq-abs-ℤ : (x : ℤ) → is-zero-ℕ (abs-ℤ x) → is-zero-ℤ x eq-abs-ℤ (inr (inl star)) p = refl abs-eq-ℤ : (x : ℤ) → is-zero-ℤ x → is-zero-ℕ (abs-ℤ x) abs-eq-ℤ .zero-ℤ refl = refl
|x - 1| ≤ |x| + 1
predecessor-law-abs-ℤ : (x : ℤ) → (abs-ℤ (pred-ℤ x)) ≤-ℕ (succ-ℕ (abs-ℤ x)) predecessor-law-abs-ℤ (inl x) = refl-leq-ℕ (succ-ℕ x) predecessor-law-abs-ℤ (inr (inl star)) = refl-leq-ℕ zero-ℕ predecessor-law-abs-ℤ (inr (inr zero-ℕ)) = star predecessor-law-abs-ℤ (inr (inr (succ-ℕ x))) = preserves-leq-succ-ℕ x (succ-ℕ x) (succ-leq-ℕ x)
|x + 1| ≤ |x| + 1
successor-law-abs-ℤ : (x : ℤ) → (abs-ℤ (succ-ℤ x)) ≤-ℕ (succ-ℕ (abs-ℤ x)) successor-law-abs-ℤ (inl zero-ℕ) = star successor-law-abs-ℤ (inl (succ-ℕ x)) = preserves-leq-succ-ℕ x (succ-ℕ x) (succ-leq-ℕ x) successor-law-abs-ℤ (inr (inl star)) = refl-leq-ℕ zero-ℕ successor-law-abs-ℤ (inr (inr x)) = refl-leq-ℕ (succ-ℕ x)
The absolute value function is subadditive
subadditive-abs-ℤ : (x y : ℤ) → (abs-ℤ (x +ℤ y)) ≤-ℕ ((abs-ℤ x) +ℕ (abs-ℤ y)) subadditive-abs-ℤ x (inl zero-ℕ) = concatenate-eq-leq-eq-ℕ ( ap abs-ℤ (right-add-neg-one-ℤ x)) ( predecessor-law-abs-ℤ x) ( refl) subadditive-abs-ℤ x (inl (succ-ℕ y)) = concatenate-eq-leq-eq-ℕ ( ap abs-ℤ (right-predecessor-law-add-ℤ x (inl y))) ( transitive-leq-ℕ ( abs-ℤ (pred-ℤ (x +ℤ (inl y)))) ( succ-ℕ (abs-ℤ (x +ℤ (inl y)))) ( (abs-ℤ x) +ℕ (succ-ℕ (succ-ℕ y))) ( subadditive-abs-ℤ x (inl y)) ( predecessor-law-abs-ℤ (x +ℤ (inl y)))) ( refl) subadditive-abs-ℤ x (inr (inl star)) = concatenate-eq-leq-eq-ℕ ( ap abs-ℤ (right-unit-law-add-ℤ x)) ( refl-leq-ℕ (abs-ℤ x)) ( refl) subadditive-abs-ℤ x (inr (inr zero-ℕ)) = concatenate-eq-leq-eq-ℕ ( ap abs-ℤ (right-add-one-ℤ x)) ( successor-law-abs-ℤ x) ( refl) subadditive-abs-ℤ x (inr (inr (succ-ℕ y))) = concatenate-eq-leq-eq-ℕ ( ap abs-ℤ (right-successor-law-add-ℤ x (inr (inr y)))) ( transitive-leq-ℕ ( abs-ℤ (succ-ℤ (x +ℤ (inr (inr y))))) ( succ-ℕ (abs-ℤ (x +ℤ (inr (inr y))))) ( succ-ℕ ((abs-ℤ x) +ℕ (succ-ℕ y))) ( subadditive-abs-ℤ x (inr (inr y))) ( successor-law-abs-ℤ (x +ℤ (inr (inr y))))) ( refl)
|-x| = |x|
negative-law-abs-ℤ : (x : ℤ) → abs-ℤ (neg-ℤ x) = abs-ℤ x negative-law-abs-ℤ (inl x) = refl negative-law-abs-ℤ (inr (inl star)) = refl negative-law-abs-ℤ (inr (inr x)) = refl
If x
is positive then |x|
is positive
is-positive-abs-ℤ : (x : ℤ) → is-positive-ℤ x → is-positive-ℤ (int-abs-ℤ x) is-positive-abs-ℤ (inr (inr x)) H = star
If x
is nonzero then |x|
is nonzero
is-nonzero-abs-ℤ : (x : ℤ) → is-positive-ℤ x → is-nonzero-ℕ (abs-ℤ x) is-nonzero-abs-ℤ (inr (inr x)) H = is-nonzero-succ-ℕ x
The absolute value function is multiplicative
multiplicative-abs-ℤ' : (x y : ℤ) → abs-ℤ (explicit-mul-ℤ x y) = (abs-ℤ x) *ℕ (abs-ℤ y) multiplicative-abs-ℤ' (inl x) (inl y) = abs-int-ℕ _ multiplicative-abs-ℤ' (inl x) (inr (inl star)) = inv (right-zero-law-mul-ℕ x) multiplicative-abs-ℤ' (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) = refl multiplicative-abs-ℤ' (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)) = refl multiplicative-abs-ℤ' (inr (inl star)) (inr (inr x)) = refl multiplicative-abs-ℤ' (inr (inr x)) (inr (inl star)) = inv (right-zero-law-mul-ℕ (succ-ℕ x)) multiplicative-abs-ℤ' (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
|(-x)y| = |xy|
left-negative-law-mul-abs-ℤ : (x y : ℤ) → abs-ℤ (x *ℤ y) = abs-ℤ ((neg-ℤ x) *ℤ y) left-negative-law-mul-abs-ℤ x y = equational-reasoning abs-ℤ (x *ℤ y) = abs-ℤ (neg-ℤ (x *ℤ y)) by (inv (negative-law-abs-ℤ (x *ℤ y))) = abs-ℤ ((neg-ℤ x) *ℤ y) by (ap abs-ℤ (inv (left-negative-law-mul-ℤ x y)))
|x(-y)| = |xy|
right-negative-law-mul-abs-ℤ : (x y : ℤ) → abs-ℤ (x *ℤ y) = abs-ℤ (x *ℤ (neg-ℤ y)) right-negative-law-mul-abs-ℤ x y = equational-reasoning abs-ℤ (x *ℤ y) = abs-ℤ (neg-ℤ (x *ℤ y)) by (inv (negative-law-abs-ℤ (x *ℤ y))) = abs-ℤ (x *ℤ (neg-ℤ y)) by (ap abs-ℤ (inv (right-negative-law-mul-ℤ x y)))
|(-x)(-y)| = |xy|
double-negative-law-mul-abs-ℤ : (x y : ℤ) → abs-ℤ (x *ℤ y) = abs-ℤ ((neg-ℤ x) *ℤ (neg-ℤ y)) double-negative-law-mul-abs-ℤ x y = (right-negative-law-mul-abs-ℤ x y) ∙ (left-negative-law-mul-abs-ℤ x (neg-ℤ y))
Recent changes
- 2024-03-28. malarbol and Fredrik Bakke. Refactoring positive integers (#1059).
- 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).
- 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).
- 2023-05-13. Fredrik Bakke. Refactor to use infix binary operators for arithmetic (#620).
- 2023-05-13. Fredrik Bakke. Define binary operator notations for
mul-ℕ
,mul-ℤ
, andexp-ℕ
. (#618).