Andrew Sneap, 26th November 2021
\begin{code}
{-# OPTIONS --safe --without-K #-}
open import MLTT.Spartan renaming (_+_ to _∔_)
open import Naturals.AbsoluteDifference using (∣_-_∣)
open import Naturals.Order
open import Notation.Order
open import UF.Base
open import UF.Subsingletons
open import Integers.Abs
open import Integers.Type
open import Integers.Addition
open import Integers.Multiplication
open import Integers.Negation
open import Naturals.Addition renaming (_+_ to _ℕ+_)
module Integers.Order where
\end{code}
First, the definition of < and ≤ for the integers. See the NaturalsOrder import
to see how < is defined similarly to < for the natural numbers. Following the
definitions are the proofs that the relations are propositions, and some simple
proofs for each.
\begin{code}
_≤ℤ_ _≥ℤ_ : (x y : ℤ) → 𝓤₀ ̇
x ≤ℤ y = Σ n ꞉ ℕ , x + pos n ＝ y
x ≥ℤ y = y ≤ℤ x
_<ℤ_ _>ℤ_ : (x y : ℤ) → 𝓤₀ ̇
x <ℤ y = succℤ x ≤ℤ y
x >ℤ y = y <ℤ x
instance
Order-ℤ-ℤ : Order ℤ ℤ
_≤_ {{Order-ℤ-ℤ}} = _≤ℤ_
Strict-Order-ℤ-ℤ : Strict-Order ℤ ℤ
_<_ {{Strict-Order-ℤ-ℤ}} = _<ℤ_
Strict-Order-Chain-ℤ-ℤ-ℤ : Strict-Order-Chain ℤ ℤ ℤ _<_ _<_
_<_<_ {{Strict-Order-Chain-ℤ-ℤ-ℤ}} p q r = (p < q) × (q < r)
Order-Chain-ℤ-ℤ-ℤ : Order-Chain ℤ ℤ ℤ _≤_ _≤_
_≤_≤_ {{Order-Chain-ℤ-ℤ-ℤ}} p q r = (p ≤ q) × (q ≤ r)
ℤ≤-is-prop : (x y : ℤ) → is-prop (x ≤ y)
ℤ≤-is-prop x y (n , p) (m , q) = to-subtype-＝ I II
where
I : (k : ℕ) → (α β : x + pos k ＝ y) → α ＝ β
I _ = ℤ-is-set
II : n ＝ m
II = pos-lc (ℤ+-lc (pos n) (pos m) x γ)
where
γ : x + pos n ＝ x + pos m
γ = x + pos n ＝⟨ p ⟩
y ＝⟨ q ⁻¹ ⟩
x + pos m ∎
ℤ<-is-prop : (x y : ℤ) → is-prop (x < y)
ℤ<-is-prop x = ℤ≤-is-prop (succℤ x)
≤-incrℤ : (x : ℤ) → x ≤ succℤ x
≤-incrℤ x = 1 , refl
<-incrℤ : (x : ℤ) → x < succℤ x
<-incrℤ x = 0 , refl
≤-predℤ : (x : ℤ) → predℤ x ≤ x
≤-predℤ x = 1 , succpredℤ x
≤-predℤ' : (x y : ℤ) → x ≤ y → predℤ x ≤ predℤ y
≤-predℤ' x y (n , e) = n , γ
where
γ : predℤ x + pos n ＝ predℤ y
γ = predℤ x + pos n ＝⟨ ℤ-left-pred x (pos n) ⟩
predℤ (x + pos n) ＝⟨ ap predℤ e ⟩
predℤ y ∎
<-predℤ : (x : ℤ) → predℤ x < x
<-predℤ x = 0 , succpredℤ x
<-is-≤ : (x y : ℤ) → x < y → x ≤ y
<-is-≤ x y (a , p) = succ a , γ
where
γ : succℤ (x + pos a) ＝ y
γ = succℤ (x + pos a) ＝⟨ ℤ-left-succ x (pos a) ⁻¹ ⟩
succℤ x + pos a ＝⟨ p ⟩
y ∎
ℕ-order-respects-ℤ-order : (m n : ℕ) → m < n → pos m < pos n
ℕ-order-respects-ℤ-order m n l = I (subtraction'' m n l)
where
I : (Σ k ꞉ ℕ , succ k ℕ+ m ＝ n) → pos m < pos n
I (k , e) = k , II
where
II : succℤ (pos m) + pos k ＝ pos n
II = succℤ (pos m) + pos k ＝⟨ distributivity-pos-addition (succ m) k ⟩
pos (succ m ℕ+ k) ＝⟨ ap pos (addition-commutativity (succ m) k) ⟩
pos (k ℕ+ succ m) ＝⟨ ap pos (succ-left k m ⁻¹) ⟩
pos (succ k ℕ+ m) ＝⟨ ap pos e ⟩
pos n ∎
ℕ-order-respects-ℤ-order' : (m n : ℕ) → m < n → negsucc n < negsucc m
ℕ-order-respects-ℤ-order' m n l = I (subtraction'' m n l)
where
I : (Σ k ꞉ ℕ , succ k ℕ+ m ＝ n) → negsucc n < negsucc m
I (k , e) = k , γ
where
k' = pos (succ k)
m' = pos (succ m)
n' = pos (succ n)
II : k' + m' ＝ n'
II = k' + m' ＝⟨ i ⟩
pos (succ k ℕ+ succ m) ＝⟨ ii ⟩
n' ∎
where
i = distributivity-pos-addition (succ k) (succ m)
ii = ap (pos ∘ succ) e
γ : succℤ (negsucc n) + pos k ＝ negsucc m
γ = succℤ (negsucc n) + pos k ＝⟨ i ⟩
negsucc n + k' ＝⟨ ii ⟩
k' + negsucc n ＝⟨ iii ⟩
k' + negsucc n + pos 0 ＝⟨ iv ⟩
k' + negsucc n + (m' + negsucc m) ＝⟨ v ⟩
k' + negsucc n + m' + negsucc m ＝⟨ vi ⟩
k' + (negsucc n + m') + negsucc m ＝⟨ vii ⟩
k' + (m' + negsucc n) + negsucc m ＝⟨ viii ⟩
k' + m' + negsucc n + negsucc m ＝⟨ ix ⟩
k' + m' + (negsucc n + negsucc m) ＝⟨ x ⟩
n' + (negsucc n + negsucc m) ＝⟨ xi ⟩
n' + negsucc n + negsucc m ＝⟨ xii ⟩
pos 0 + negsucc m ＝⟨ xiii ⟩
negsucc m ∎
where
ivₐₚ : pos 0 ＝ m' - m'
ivₐₚ = ℤ-sum-of-inverse-is-zero m' ⁻¹
i = ℤ-left-succ (negsucc n) (pos k)
ii = ℤ+-comm (negsucc n) k'
iii = ℤ-zero-right-neutral (k' + negsucc n)
iv = ap ((k' + negsucc n) +_) ivₐₚ
v = ℤ+-assoc (k' + negsucc n) m' (negsucc m) ⁻¹
vi = ap (_+ negsucc m) (ℤ+-assoc k' (negsucc n) m')
vii = ap (λ p → k' + p + negsucc m) (ℤ+-comm (negsucc n) m')
viii = ap (_+ negsucc m) (ℤ+-assoc k' m' (negsucc n) ⁻¹)
ix = ℤ+-assoc (k' + m') (negsucc n) (negsucc m)
x = ap (λ p → p + (negsucc n + negsucc m)) II
xi = ℤ+-assoc n' (negsucc n) (negsucc m) ⁻¹
xii = ap (_+ negsucc m) (ℤ-sum-of-inverse-is-zero n')
xiii = ℤ-zero-left-neutral (negsucc m)
ℤ-bigger-or-equal-not-less : (x y : ℤ) → x ≤ y → ¬ (y < x)
ℤ-bigger-or-equal-not-less x y (α , p) (β , q) = 𝟘-elim γ
where
I : x + succℤ (pos (α ℕ+ β)) ＝ x + pos 0
I = x + succℤ (pos (α ℕ+ β)) ＝⟨ i ⟩
x + succℤ (pos α + pos β) ＝⟨ ii ⟩
succℤ (x + (pos α + pos β)) ＝⟨ iii ⟩
succℤ (x + pos α + pos β) ＝⟨ iv ⟩
succℤ (x + pos α) + pos β ＝⟨ v ⟩
x ＝⟨ by-definition ⟩
x + pos 0 ∎
where
i = ap (λ - → x + succℤ -) (distributivity-pos-addition α β ⁻¹)
ii = ℤ-right-succ x (pos α + pos β)
iii = ap succℤ (ℤ+-assoc x (pos α) (pos β) ⁻¹)
iv = ℤ-left-succ (x + pos α) (pos β) ⁻¹
v = transport (λ - → succℤ - + (pos β) ＝ x) (p ⁻¹) q
II : succℤ (pos (α ℕ+ β)) ＝ pos 0
II = ℤ+-lc (succℤ (pos (α ℕ+ β))) (pos 0) x I
γ : 𝟘
γ = pos-succ-not-zero (α ℕ+ β) II
ℤ≤-split : (x y : ℤ) → x ≤ y → (x < y) ∔ (x ＝ y)
ℤ≤-split x y (zero , p) = inr p
ℤ≤-split x y (succ a , p) = inl (a , (ℤ-left-succ x (pos a) ∙ p))
ℤ≤-trans : (x y z : ℤ) → x ≤ y → y ≤ z → x ≤ z
ℤ≤-trans x y z (a , p) (b , q) = a ℕ+ b , I
where
I : x + pos (a ℕ+ b) ＝ z
I = x + pos (a ℕ+ b) ＝⟨ ap (x +_) (distributivity-pos-addition a b ⁻¹) ⟩
x + (pos a + pos b) ＝⟨ ℤ+-assoc x (pos a) (pos b) ⁻¹ ⟩
x + pos a + pos b ＝⟨ ap (_+ (pos b)) p ⟩
y + (pos b) ＝⟨ q ⟩
z ∎
ℤ<-trans : (x y z : ℤ) → x < y → y < z → x < z
ℤ<-trans x y z l₁ l₂ = ℤ≤-trans (succℤ x) (succℤ y) z I l₂
where
I : succℤ x ≤ succℤ y
I = ℤ≤-trans (succℤ x) y (succℤ y) l₁ (≤-incrℤ y)
ℤ<-≤-trans : (x y z : ℤ) → x < y → y ≤ z → x < z
ℤ<-≤-trans x y z l₁ l₂ = cases γ₁ γ₂ I
where
I : (y < z) ∔ (y ＝ z)
I = ℤ≤-split y z l₂
γ₁ : y < z → x < z
γ₁ l₃ = ℤ<-trans x y z l₁ l₃
γ₂ : y ＝ z → x < z
γ₂ e = transport (x <_) e l₁
ℤ≤-<-trans : (x y z : ℤ) → x ≤ y → y < z → x < z
ℤ≤-<-trans x y z l₁ l₂ = cases γ₁ γ₂ I
where
I : (x < y) ∔ (x ＝ y)
I = ℤ≤-split x y l₁
γ₁ : x < y → x < z
γ₁ l₃ = ℤ<-trans x y z l₃ l₂
γ₂ : x ＝ y → x < z
γ₂ e = transport (_< z) (e ⁻¹) l₂
ℤ≤-refl : (x : ℤ) → x ≤ x
ℤ≤-refl x = 0 , refl
ℤ-equal-not-less-than : (x : ℤ) → ¬ (x < x)
ℤ-equal-not-less-than x (0 , α) = succℤ-no-fp x (α ⁻¹)
ℤ-equal-not-less-than x (succ n , α) = pos-succ-not-zero (n ℕ+ 1) γ
where
I : x + succℤ (succℤ (pos n)) ＝ x + pos 0
I = x + succℤ (succℤ (pos n)) ＝⟨ ℤ-right-succ x (succℤ (pos n)) ⟩
succℤ (x + succℤ (pos n)) ＝⟨ ℤ-left-succ x (succℤ (pos n)) ⁻¹ ⟩
succℤ x + succℤ (pos n) ＝⟨ by-definition ⟩
succℤ x + pos (succ n) ＝⟨ α ⟩
x ＝⟨ ℤ-zero-right-neutral x ⟩
x + pos 0 ∎
γ : succℤ (succℤ (pos n)) ＝ pos 0
γ = ℤ+-lc (succℤ (succℤ (pos n))) (pos 0) x I
ℤ-zero-less-than-pos : (n : ℕ) → pos 0 < pos (succ n)
ℤ-zero-less-than-pos n = ℕ-order-respects-ℤ-order 0 (succ n) (zero-least n)
ℤ-zero-least-pos : (n : ℕ) → pos 0 ≤ pos n
ℤ-zero-least-pos 0 = ℤ≤-refl (pos 0)
ℤ-zero-least-pos (succ n) = γ
where
I : pos 0 ≤ pos n
I = ℤ-zero-least-pos n
II : pos n ≤ pos (succ n)
II = ≤-incrℤ (pos n)
γ : pos 0 ≤ pos (succ n)
γ = ℤ≤-trans (pos 0) (pos n) (pos (succ n)) I II
negative-less-than-positive : (x y : ℕ) → negsucc x < pos y
negative-less-than-positive x y = (x ℕ+ y) , I
where
I : succℤ (negsucc x) + pos (x ℕ+ y) ＝ pos y
I = succℤ (negsucc x) + pos (x ℕ+ y) ＝⟨ i ⟩
succℤ (negsucc x) + (pos x + pos y) ＝⟨ ii ⟩
succℤ (negsucc x) + pos x + pos y ＝⟨ iii ⟩
negsucc x + pos (succ x) + pos y ＝⟨ refl ⟩
(- pos (succ x)) + pos (succ x) + pos y ＝⟨ iv ⟩
pos 0 + pos y ＝⟨ v ⟩
pos y ∎
where
i = ap (succℤ (negsucc x) +_) (distributivity-pos-addition x y ⁻¹)
ii = ℤ+-assoc (succℤ (negsucc x)) (pos x) (pos y) ⁻¹
iii = ap (_+ pos y) (ℤ-left-succ (negsucc x) (pos x))
iv = ap (_+ pos y) (ℤ-sum-of-inverse-is-zero' (pos (succ x)))
v = ℤ-zero-left-neutral (pos y)
ℤ≤-swap : (x y : ℤ) → x ≤ y → - y ≤ - x
ℤ≤-swap x y (k , e) = k , ℤ+-lc ((- y) + pos k) (- x) (y + x) I
where
I : y + x + ((- y) + pos k) ＝ y + x - x
I = y + x + ((- y) + pos k) ＝⟨ i ⟩
x + y + ((- y) + pos k) ＝⟨ ii ⟩
x + y - y + pos k ＝⟨ iii ⟩
x + (y - y) + pos k ＝⟨ iv ⟩
x + pos 0 + pos k ＝⟨ by-definition ⟩
x + pos k ＝⟨ e ⟩
y ＝⟨ by-definition ⟩
y + pos 0 ＝⟨ v ⟩
y + (x - x) ＝⟨ vi ⟩
y + x - x ∎
where
i = ap (_+ ((- y) + pos k)) (ℤ+-comm y x)
ii = ℤ+-assoc (x + y) (- y) (pos k) ⁻¹
iii = ap (_+ pos k) (ℤ+-assoc x y (- y))
iv = ap (λ α → x + α + (pos k)) (ℤ-sum-of-inverse-is-zero y)
v = ap (y +_) (ℤ-sum-of-inverse-is-zero x ⁻¹)
vi = ℤ+-assoc y x (- x) ⁻¹
ℤ≤-swap₂ : (x y z : ℤ) → x ≤ y ≤ z → (- y ≤ - x) × (- z ≤ - y)
ℤ≤-swap₂ x y z (l₁ , l₂) = (ℤ≤-swap x y l₁) , (ℤ≤-swap y z l₂)
ℕ≤-to-ℤ≤ : (x y : ℕ) → x ≤ y → pos x ≤ pos y
ℕ≤-to-ℤ≤ x y l = I (subtraction x y l)
where
I : (Σ k ꞉ ℕ , k ℕ+ x ＝ y) → pos x ≤ pos y
I (k , e) = k , II
where
II : pos x + pos k ＝ pos y
II = pos x + pos k ＝⟨ distributivity-pos-addition x k ⟩
pos (x ℕ+ k) ＝⟨ ap pos (addition-commutativity x k) ⟩
pos (k ℕ+ x) ＝⟨ ap pos e ⟩
pos y ∎
ℤ-dichotomous : (x y : ℤ) → (x ≤ y) ∔ (y ≤ x)
ℤ-dichotomous (pos x) (pos y) = I (≤-dichotomous x y)
where
I : (x ≤ y) ∔ (y ≤ x) → (pos x ≤ pos y) ∔ (pos y ≤ pos x)
I (inl l) = inl (ℕ≤-to-ℤ≤ x y l)
I (inr r) = inr (ℕ≤-to-ℤ≤ y x r)
ℤ-dichotomous (pos x) (negsucc y) = inr (negative-less-than-positive (succ y) x)
ℤ-dichotomous (negsucc x) (pos y) = inl (negative-less-than-positive (succ x) y)
ℤ-dichotomous (negsucc x) (negsucc y) = Cases (≤-dichotomous x y) γ₁ γ₂
where
I : (a b : ℕ) → a ≤ b → negsucc b ≤ negsucc a
I a b l = ℤ≤-swap (pos (succ a)) (pos (succ b)) II
where
II : pos (succ a) ≤ pos (succ b)
II = ℕ≤-to-ℤ≤ (succ a) (succ b) l
γ₁ : x ≤ y → (negsucc x ≤ negsucc y) ∔ (negsucc y ≤ negsucc x)
γ₁ l = inr (I x y l)
γ₂ : y ≤ x → (negsucc x ≤ negsucc y) ∔ (negsucc y ≤ negsucc x)
γ₂ l = inl (I y x l)
trich-locate : (x y : ℤ) → 𝓤₀ ̇
trich-locate x y = (x < y) ∔ (x ＝ y) ∔ (y < x)
ℤ-trichotomous : (x y : ℤ) → trich-locate x y
ℤ-trichotomous x y = I (ℤ-dichotomous x y)
where
I : (x ≤ y) ∔ (y ≤ x) → (x < y) ∔ (x ＝ y) ∔ (y < x)
I (inl l) = II (ℤ≤-split x y l)
where
II : (x < y) ∔ (x ＝ y) → (x < y) ∔ (x ＝ y) ∔ (y < x)
II (inl l) = inl l
II (inr r) = inr (inl r)
I (inr r) = II (ℤ≤-split y x r)
where
II : (y < x) ∔ (y ＝ x) → (x < y) ∔ (x ＝ y) ∔ (y < x)
II (inl l) = inr (inr l)
II (inr r) = inr (inl (r ⁻¹))
ℤ-dichotomous' : (x y : ℤ) → x < y ∔ y ≤ x
ℤ-dichotomous' x y = I (ℤ-trichotomous x y)
where
I : (x < y) ∔ (x ＝ y) ∔ (y < x) → x < y ∔ y ≤ x
I (inl x<y) = inl x<y
I (inr (inl x＝y)) = inr (transport (_≤ x) x＝y (ℤ≤-refl x))
I (inr (inr y<x)) = inr (<-is-≤ y x y<x)
ℤ-trichotomous-is-prop : (x y : ℤ) → is-prop (trich-locate x y)
ℤ-trichotomous-is-prop x y = +-is-prop I II γ
where
I : is-prop (x < y)
I = ℤ<-is-prop x y
II : is-prop ((x ＝ y) ∔ y < x)
II = +-is-prop ℤ-is-set (ℤ<-is-prop y x) III
where
III : x ＝ y → ¬ (y < x)
III e l = ℤ-equal-not-less-than y (transport (y <_) e l)
γ : x < y → ¬ ((x ＝ y) ∔ y < x)
γ l (inl e ) = ℤ-equal-not-less-than x (transport (x <_) (e ⁻¹) l)
γ l (inr l') = ℤ-bigger-or-equal-not-less x y (<-is-≤ x y l) l'
ℤ≤-adding : (a b c d : ℤ) → a ≤ b → c ≤ d → a + c ≤ b + d
ℤ≤-adding a b c d (p , β) (q , β') = (p ℕ+ q) , I
where
I : a + c + pos (p ℕ+ q) ＝ b + d
I = a + c + pos (p ℕ+ q) ＝⟨ i ⟩
a + c + (pos p + pos q) ＝⟨ ii ⟩
a + c + pos p + pos q ＝⟨ iii ⟩
c + a + pos p + pos q ＝⟨ iv ⟩
c + (a + pos p) + pos q ＝⟨ v ⟩
c + b + pos q ＝⟨ vi ⟩
b + c + pos q ＝⟨ vii ⟩
b + (c + pos q) ＝⟨ viii ⟩
b + d ∎
where
i = ap (a + c +_) (distributivity-pos-addition p q ⁻¹)
ii = ℤ+-assoc (a + c) (pos p) (pos q) ⁻¹
iii = ap (λ z → z + pos p + pos q) (ℤ+-comm a c)
iv = ap (_+ pos q) (ℤ+-assoc c a (pos p))
v = ap (λ z → c + z + pos q) β
vi = ap (_+ pos q) (ℤ+-comm c b)
vii = ℤ+-assoc b c (pos q)
viii = ap (b +_) β'
ℤ<-adding : (a b c d : ℤ) → a < b → c < d → a + c < b + d
ℤ<-adding a b c d l₁ l₂ = ℤ<-trans (a + c) (a + succℤ c) (b + d) II III
where
I : succℤ a + succℤ c ≤ b + d
I = ℤ≤-adding (succℤ a) b (succℤ c) d l₁ l₂
II : a + c < a + succℤ c
II = 0 , (ℤ-right-succ a c ⁻¹)
III : a + succℤ c < b + d
III = transport (_≤ b + d) (ℤ-left-succ a (succℤ c)) I
ℤ≤-adding' : (a b c : ℤ) → a ≤ b → a + c ≤ b + c
ℤ≤-adding' a b c (k , p) = k , I
where
I : a + c + pos k ＝ b + c
I = a + c + pos k ＝⟨ ℤ+-assoc a c (pos k) ⟩
a + (c + pos k) ＝⟨ ap (a +_) (ℤ+-comm c (pos k)) ⟩
a + (pos k + c) ＝⟨ ℤ+-assoc a (pos k) c ⁻¹ ⟩
a + pos k + c ＝⟨ ap (_+ c) p ⟩
b + c ∎
ℤ≤-adding-left : (a b c : ℤ) → a ≤ b → c + a ≤ c + b
ℤ≤-adding-left a b c l = transport₂ _≤_ I II III
where
I : a + c ＝ c + a
I = ℤ+-comm a c
II : b + c ＝ c + b
II = ℤ+-comm b c
III : a + c ≤ b + c
III = ℤ≤-adding' a b c l
ℤ≤-adding₂ : (a b c d : ℤ) → a ≤ b ≤ c → (a + d ≤ b + d ≤ c + d)
ℤ≤-adding₂ a b c d (l₁ , l₂) = (ℤ≤-adding' a b d l₁) , (ℤ≤-adding' b c d l₂)
ℤ<-adding' : (a b c : ℤ) → a < b → a + c < b + c
ℤ<-adding' a b c (k , p) = I (ℤ≤-adding' (succℤ a) b c (k , p))
where
I : succℤ a + c ≤ b + c → a + c < b + c
I (h , q) = h , II
where
II : succℤ (a + c) + pos h ＝ b + c
II = succℤ (a + c) + pos h ＝⟨ ap (_+ (pos h)) (ℤ-left-succ a c ⁻¹) ⟩
succℤ a + c + pos h ＝⟨ q ⟩
b + c ∎
ℤ<-adding-left : (a b c : ℤ) → a < b → c + a < c + b
ℤ<-adding-left a b c l = transport₂ _<_ I II III
where
I : a + c ＝ c + a
I = ℤ+-comm a c
II : b + c ＝ c + b
II = ℤ+-comm b c
III : a + c < b + c
III = ℤ<-adding' a b c l
ℤ<-adding'' : (a b c : ℤ) → a < b → c + a < c + b
ℤ<-adding'' a b c l = transport₂ _<_ (ℤ+-comm a c) (ℤ+-comm b c) I
where
I : a + c < b + c
I = ℤ<-adding' a b c l
pmpo-lemma : (a b : ℤ) → (n : ℕ) → a < b → a * pos (succ n) < b * pos (succ n)
pmpo-lemma a b = ℕ-induction base step
where
base : a < b
→ a * pos 1 < b * pos 1
base z = z
step : (k : ℕ)
→ (a < b → a * pos (succ k) < b * pos (succ k))
→ a < b
→ a * pos (succ (succ k)) < b * pos (succ (succ k))
step k IH l = ℤ<-adding a b (a + (a * pos k)) (b + (b * pos k)) l (IH l)
positive-multiplication-preserves-order : (a b c : ℤ)
→ is-pos-succ c
→ a < b
→ a * c < b * c
positive-multiplication-preserves-order a b (negsucc x) p l = 𝟘-elim p
positive-multiplication-preserves-order a b (pos 0) p l = 𝟘-elim p
positive-multiplication-preserves-order a b (pos (succ x)) p l = pmpo-lemma a b x l
positive-multiplication-preserves-order' : (a b c : ℤ)
→ is-pos-succ c
→ a ≤ b
→ a * c ≤ b * c
positive-multiplication-preserves-order' a b c p l = I (ℤ≤-split a b l)
where
I : (a < b) ∔ (a ＝ b) → a * c ≤ b * c
I (inl l) = <-is-≤ (a * c) (b * c) γ
where
γ : a * c < b * c
γ = positive-multiplication-preserves-order a b c p l
I (inr e) = transport (_≤ b * c) γ (ℤ≤-refl (b * c))
where
γ : b * c ＝ a * c
γ = ap (_* c) (e ⁻¹)
ℤ*-multiplication-order : (a b c : ℤ)
→ pos 0 ≤ c
→ a ≤ b
→ a * c ≤ b * c
ℤ*-multiplication-order a b (pos 0) p l = ℤ≤-refl (pos 0)
ℤ*-multiplication-order a b (pos (succ c)) p l
= positive-multiplication-preserves-order' a b (pos (succ c)) ⋆ l
ℤ*-multiplication-order a b (negsucc c) p l = 𝟘-elim γ
where
I : negsucc c < pos 0
I = negative-less-than-positive c 0
γ : 𝟘
γ = ℤ-bigger-or-equal-not-less (pos 0) (negsucc c) p I
nmco-lemma : (a b : ℤ) → (c : ℕ) → a < b → b * (negsucc c) < a * (negsucc c)
nmco-lemma a b = ℕ-induction base step
where
base : a < b → b * negsucc 0 < a * negsucc 0
base (k , γ) = k , I
where
II : (- b) + pos k + (a - a) ＝ a + pos k + ((- b) - a)
II = (- b) + pos k + (a - a) ＝⟨ i ⟩
pos k - b + (a - a) ＝⟨ ii ⟩
pos k - b + a - a ＝⟨ iii ⟩
a + (pos k - b) - a ＝⟨ iv ⟩
a + pos k - b - a ＝⟨ v ⟩
a + pos k + ((- b) - a) ∎
where
i = ap (_+ (a - a)) (ℤ+-comm (- b) (pos k))
ii = ℤ+-assoc (pos k - b) a (- a) ⁻¹
iii = ap (_+ (- a)) (ℤ+-comm (pos k - b) a)
iv = ap (_+ (- a)) (ℤ+-assoc a (pos k) (- b) ⁻¹)
v = ℤ+-assoc (a + pos k) (- b) (- a)
I : succℤ (b * negsucc 0) + pos k ＝ a * negsucc 0
I = succℤ (b * negsucc 0) + pos k ＝⟨ by-definition ⟩
succℤ (- b) + pos k ＝⟨ i ⟩
succℤ ((- b) + pos k) ＝⟨ ii ⟩
succℤ ((- b) + pos k) + pos 0 ＝⟨ iii ⟩
succℤ ((- b) + pos k) + (a - a) ＝⟨ iv ⟩
succℤ ((- b) + pos k + (a - a)) ＝⟨ v ⟩
succℤ (a + pos k + ((- b) - a)) ＝⟨ vi ⟩
succℤ (a + pos k) + ((- b) - a) ＝⟨ vii ⟩
succℤ a + pos k + ((- b) - a) ＝⟨ viii ⟩
b + ((- b) - a) ＝⟨ ix ⟩
b - b - a ＝⟨ x ⟩
pos 0 - a ＝⟨ xi ⟩
- a ＝⟨ by-definition ⟩
a * negsucc 0 ∎
where
i = ℤ-left-succ (- b) (pos k)
ii = ℤ-zero-right-neutral (succℤ ((- b) +pos k))
iii = ap (succℤ ((- b) + pos k) +_) (ℤ-sum-of-inverse-is-zero a ⁻¹)
iv = ℤ-left-succ ((- b) + pos k) (a - a)
v = ap succℤ II
vi = ℤ-left-succ (a + pos k) ((- b) - a) ⁻¹
vii = ap (_+ ((- b) - a)) (ℤ-left-succ a (pos k) ⁻¹)
viii = ap (_+ ((- b) - a)) γ
ix = ℤ+-assoc b (- b) (- a) ⁻¹
x = ap (_+ (- a)) (ℤ-sum-of-inverse-is-zero b)
xi = ℤ-zero-left-neutral (- a)
step : (k : ℕ)
→ (a < b → b * negsucc k < a * negsucc k)
→ a < b → b * negsucc (succ k) < a * negsucc (succ k)
step k IH l = ℤ<-adding (- b) (- a) (b * negsucc k) (a * negsucc k) I II
where
I : - b < - a
I = base l
II : b * negsucc k < a * negsucc k
II = IH l
negative-multiplication-changes-order : (a b c : ℤ)
→ negative c
→ a < b
→ b * c < a * c
negative-multiplication-changes-order a b (pos c) g l = 𝟘-elim g
negative-multiplication-changes-order a b (negsucc c) g l = nmco-lemma a b c l
negative-multiplication-changes-order' : (a b c : ℤ)
→ negative c
→ a ≤ b
→ b * c ≤ a * c
negative-multiplication-changes-order' a b (pos x) g l = 𝟘-elim g
negative-multiplication-changes-order' a b (negsucc x) g l = I (ℤ≤-split a b l)
where
I : a < b ∔ (a ＝ b) → b * negsucc x ≤ a * negsucc x
I (inl a<b) = <-is-≤ (b * negsucc x) (a * negsucc x) γ
where
γ : b * negsucc x < a * negsucc x
γ = negative-multiplication-changes-order a b (negsucc x) ⋆ a<b
I (inr a＝b) = transport (b * negsucc x ≤ℤ_) γ₁ γ₂
where
γ₁ : b * negsucc x ＝ a * negsucc x
γ₁ = ap (_* negsucc x) (a＝b ⁻¹)
γ₂ : b * negsucc x ≤ b * negsucc x
γ₂ = ℤ≤-refl (b * negsucc x)
ℤ-mult-right-cancellable : (x y z : ℤ) → not-zero z → x * z ＝ y * z → x ＝ y
ℤ-mult-right-cancellable x y (pos 0) nz e = 𝟘-elim (nz ⋆)
ℤ-mult-right-cancellable x y (pos (succ z)) nz e = tri-split (ℤ-trichotomous x y)
where
tri-split : (x < y) ∔ (x ＝ y) ∔ (y < x) → x ＝ y
tri-split (inl l) = 𝟘-elim (ℤ-equal-not-less-than (x * pos (succ z)) II)
where
I : x * pos (succ z) < y * pos (succ z)
I = positive-multiplication-preserves-order x y (pos (succ z)) ⋆ l
II : x * pos (succ z) < x * pos (succ z)
II = transport (x * pos (succ z) <_) (e ⁻¹) I
tri-split (inr (inl m)) = m
tri-split (inr (inr r)) = 𝟘-elim (ℤ-equal-not-less-than (y * pos (succ z)) II)
where
I : y * pos (succ z) < x * pos (succ z)
I = positive-multiplication-preserves-order y x (pos (succ z)) ⋆ r
II : y * pos (succ z) < y * pos (succ z)
II = transport (y * pos (succ z) <_) e I
ℤ-mult-right-cancellable x y (negsucc z) nz e = tri-split (ℤ-trichotomous x y)
where
tri-split : (x < y) ∔ (x ＝ y) ∔ (y < x) → x ＝ y
tri-split (inl l) = 𝟘-elim (ℤ-equal-not-less-than (y * negsucc z) II)
where
I : y * negsucc z < x * negsucc z
I = nmco-lemma x y z l
II : y * negsucc z < y * negsucc z
II = transport (y * negsucc z <_) e I
tri-split (inr (inl r)) = r
tri-split (inr (inr r)) = 𝟘-elim (ℤ-equal-not-less-than (x * negsucc z) II)
where
I : (x * negsucc z) < (y * negsucc z)
I = nmco-lemma y x z r
II : x * negsucc z < x * negsucc z
II = transport (x * negsucc z <_) (e ⁻¹) I
ℤ-mult-left-cancellable : (x y z : ℤ) → not-zero z
→ z * x ＝ z * y
→ x ＝ y
ℤ-mult-left-cancellable x y z nz e = ℤ-mult-right-cancellable x y z nz I
where
I : x * z ＝ y * z
I = x * z ＝⟨ ℤ*-comm x z ⟩
z * x ＝⟨ e ⟩
z * y ＝⟨ ℤ*-comm z y ⟩
y * z ∎
non-zero-multiplication : (x y : ℤ) → ¬ (x ＝ pos 0) → ¬ (y ＝ pos 0) → ¬ (x * y ＝ pos 0)
non-zero-multiplication (pos 0) y xnz ynz e = xnz refl
non-zero-multiplication (pos (succ x)) y xnz ynz e = ynz γ
where
γ : y ＝ pos 0
γ = ℤ-mult-left-cancellable y (pos 0) (pos (succ x)) id e
non-zero-multiplication (negsucc x) y xnz ynz e = ynz γ
where
γ : y ＝ pos 0
γ = ℤ-mult-left-cancellable y (pos 0) (negsucc x) id e
orcl : (a b : ℤ) → (n : ℕ) → a * (pos (succ n)) ≤ b * (pos (succ n)) → a ≤ b
orcl a b = ℕ-induction base step
where
base : a * pos 1 ≤ b * pos 1 → a ≤ b
base = id
step : (k : ℕ)
→ (a * pos (succ k) ≤ b * pos (succ k) → a ≤ b)
→ a * pos (succ (succ k)) ≤ b * pos (succ (succ k))
→ a ≤ b
step k IH (α , β) = cases₃ γ₁ γ₂ γ₃ (ℤ-trichotomous a b)
where
k' = pos (succ (succ k))
γ₁ : a < b → a ≤ b
γ₁ = <-is-≤ a b
γ₂ : a ＝ b → a ≤ b
γ₂ e = transport (a ≤_) e (ℤ≤-refl a)
γ₃ : b < a → a ≤ b
γ₃ l = 𝟘-elim III
where
I : a * k' ≤ b * k'
I = α , β
II : b * k' < a * k'
II = positive-multiplication-preserves-order b a k' ⋆ l
III : 𝟘
III = ℤ-bigger-or-equal-not-less (a * k') (b * k') I II
orcl' : (a b : ℤ) → (n : ℕ) → a * (pos (succ n)) < b * (pos (succ n)) → a < b
orcl' a b n l = II (ℤ≤-split a b I)
where
I : a ≤ b
I = orcl a b n (<-is-≤ (a * pos (succ n)) (b * pos (succ n)) l)
II : a < b ∔ (a ＝ b) → a < b
II (inl l) = l
II (inr e) = 𝟘-elim (ℤ-equal-not-less-than (a * pos (succ n)) III)
where
III : a * pos (succ n) < a * pos (succ n)
III = transport (λ - → (a * pos (succ n)) < (- * pos (succ n))) (e ⁻¹) l
ordering-right-cancellable : (a b c : ℤ) → is-pos-succ c → a * c < b * c → a < b
ordering-right-cancellable a b (negsucc x) p l = 𝟘-elim p
ordering-right-cancellable a b (pos 0) p l = 𝟘-elim p
ordering-right-cancellable a b (pos (succ x)) p l = orcl' a b x l
ℤ≤-ordering-right-cancellable : (a b c : ℤ)
→ is-pos-succ c → a * c ≤ b * c → a ≤ b
ℤ≤-ordering-right-cancellable a b (pos zero) p l = 𝟘-elim p
ℤ≤-ordering-right-cancellable a b (pos (succ x)) p l = orcl a b x l
ℤ≤-ordering-right-cancellable a b (negsucc x) p l = 𝟘-elim p
ℤ≤-anti : (x y : ℤ) → x ≤ y → y ≤ x → x ＝ y
ℤ≤-anti x y l₁ l₂ = I (ℤ≤-split x y l₁) (ℤ≤-split y x l₂)
where
I : x < y ∔ (x ＝ y) → y < x ∔ (y ＝ x)
→ x ＝ y
I (inl x<y) (inr e) = e ⁻¹
I (inr e) (inl y<x) = e
I (inr e) (inr e') = e
I (inl x<y) (inl y<x) = 𝟘-elim III
where
II : x < x
II = ℤ<-trans x y x x<y y<x
III : 𝟘
III = ℤ-equal-not-less-than x II
maxℤ : ℤ → ℤ → ℤ
maxℤ x y with ℤ-dichotomous x y
... | inl x≤y = y
... | inr y≤x = x
max₂ : ℤ → ℤ → ℤ → ℤ
max₂ x y z = maxℤ (maxℤ x y) z
max₃ : ℤ → ℤ → ℤ → ℤ → ℤ
max₃ w x y z = maxℤ (max₂ w x y) z
minℤ : ℤ → ℤ → ℤ
minℤ x y with ℤ-dichotomous x y
... | inl x≤y = x
... | inr y≤x = y
min₂ : ℤ → ℤ → ℤ → ℤ
min₂ x y z = minℤ (minℤ x y) z
min₃ : ℤ → ℤ → ℤ → ℤ → ℤ
min₃ w x y z = minℤ (min₂ w x y) z
\end{code}
Added by Todd
\begin{code}
ℤ≤-attach : (x y : ℤ) → (y ＝ x) ∔ (x < y) → x ≤ y
ℤ≤-attach x x (inl refl) = 0 , refl
ℤ≤-attach x y (inr (a , p)) = succ a , (ℤ-left-succ-pos x a ⁻¹ ∙ p)
ℤ≤-same-witness : (x y : ℤ) → ((n , _) (m , _) : x ≤ y) → n ＝ m
ℤ≤-same-witness x y p q = ap pr₁ (ℤ≤-is-prop x y p q)
ℤ≤-add-witness : (x y z : ℤ) → ((n , p) : x ≤ y) ((m , q) : y ≤ z)
→ ((o , r) : x ≤ z)
→ o ＝ n ℕ+ m
ℤ≤-add-witness x y z x≤y y≤z x≤z
= ℤ≤-same-witness x z x≤z (ℤ≤-trans x y z x≤y y≤z)
ℤ-less-not-bigger-or-equal : (x y : ℤ) → x < y → ¬ (y ≤ x)
ℤ-less-not-bigger-or-equal x y x<y y≤x
= ℤ-bigger-or-equal-not-less y x y≤x x<y
\end{code}
Lane Biocini, 07 September 2023
A proof of the triangle inequality in the Integers using the Absolute
Difference operation defined in the Naturals. We first prove a convenience
lemma.
\begin{code}
ℕ-order-respects-ℤ-order'' : (m n : ℕ) → m ≤ n → pos m ≤ pos n
ℕ-order-respects-ℤ-order'' zero n l = ℤ-zero-least-pos n
ℕ-order-respects-ℤ-order'' (succ m) n l = ℕ-order-respects-ℤ-order m n l
triangle-inequality₀ : (x y : ℕ) → abs (pos x +pos y) ≤ℕ abs (pos x) ℕ+ abs (pos y)
triangle-inequality₀ x y = transport (_≤ℕ x ℕ+ y) Γ (≤-refl (x ℕ+ y))
where
Γ : x ℕ+ y ＝ abs (pos x +pos y)
Γ = x ℕ+ y ＝⟨ ap abs (distributivity-pos-addition x y) ⁻¹ ⟩
abs (pos x +pos y) ∎
triangle-inequality₁ : (x y : ℕ) → abs (pos x +negsucc y) ≤ℕ succ (x ℕ+ y)
triangle-inequality₁ x y = transport (_≤ℕ succ (x ℕ+ y)) Γ γ
where
Γ : ∣ x - succ y ∣ ＝ abs (pos x +negsucc y)
Γ = abs-pos-plus-negsucc x y ⁻¹
γ : ∣ x - succ y ∣ ≤ℕ succ (x ℕ+ y)
γ = triangle-inequality x 0 (succ y)
triangle-inequality₂ : (x y : ℕ) → abs (negsucc x +pos y) ≤ℕ (succ x ℕ+ y)
triangle-inequality₂ x y = transport₂ _≤ℕ_ I II (triangle-inequality₁ y x)
where
I : abs (pos y +negsucc x) ＝ abs (negsucc x +pos y)
I = ap abs (ℤ+-comm (pos y) (negsucc x))
II : succ (y ℕ+ x) ＝ succ x ℕ+ y
II = ap succ (addition-commutativity y x) ∙ succ-left x y ⁻¹
triangle-inequality₃ : (x y : ℕ) → abs (negsucc x +negsucc y) ≤ℕ succ (succ x ℕ+ y)
triangle-inequality₃ x y = transport (_≤ℕ succ (succ x ℕ+ y)) Γ γ
where
Γ : abs (pos (succ x) + pos (succ y)) ＝ abs (negsucc x +negsucc y)
Γ = abs (succℤ (pos (succ x) +pos y)) ＝⟨ i ⟩
abs (- succℤ (pos (succ x) +pos y)) ＝⟨ ii ⟩
abs (negsucc x +negsucc y) ∎
where
i = abs-removes-neg-sign (succℤ (pos (succ x) +pos y))
ii = ap abs (negation-dist (pos (succ x)) (pos (succ y))) ⁻¹
γ : abs (pos (succ x) + pos (succ y)) ≤ℕ succ (succ x ℕ+ y)
γ = triangle-inequality₀ (succ x) (succ y)
ℤ-triangle-inequality : (x y : ℤ) → abs (x + y) ≤ℕ abs x ℕ+ abs y
ℤ-triangle-inequality (pos x) (pos y) = triangle-inequality₀ x y
ℤ-triangle-inequality (pos x) (negsucc y) = triangle-inequality₁ x y
ℤ-triangle-inequality (negsucc x) (pos y) = triangle-inequality₂ x y
ℤ-triangle-inequality (negsucc x) (negsucc y) = triangle-inequality₃ x y
ℤ-triangle-inequality' : (x y : ℤ) → absℤ (x + y) ≤ℤ absℤ x + absℤ y
ℤ-triangle-inequality' x y = transport₂ _≤ℤ_ I II γ
where
I : pos (abs (x + y)) ＝ absℤ (x + y)
I = pos-abs-is-absℤ (x + y)
II : pos (abs x ℕ+ abs y) ＝ absℤ x + absℤ y
II = pos (abs x ℕ+ abs y) ＝⟨ i ⟩
(pos (abs x) +pos abs y) ＝⟨ ii ⟩
absℤ x + absℤ y ∎
where
i = distributivity-pos-addition (abs x) (abs y) ⁻¹
ii : (pos (abs x) +pos abs y) ＝ absℤ x + absℤ y
ii = ap₂ (λ x y → x + y) (pos-abs-is-absℤ x) (pos-abs-is-absℤ y)
γ : pos (abs (x + y)) ≤ℤ pos (abs x ℕ+ abs y)
γ = ℕ-order-respects-ℤ-order'' (abs (x + y)) (abs x ℕ+ abs y) (ℤ-triangle-inequality x y)