triangle inequality for naturals and integers (#177)

source/Integers/Abs.lagda

@@ -9,7 +9,9 @@ of abs, along with positive and negative properties of integers.
 
 open import MLTT.Spartan renaming (_+_ to _∔_)
 
+open import Naturals.AbsoluteDifference
 open import Naturals.Multiplication renaming (_*_ to _ℕ*_)
+open import Integers.Addition
 open import Integers.Multiplication
 open import Integers.Negation
 open import Integers.Type
@@ -169,3 +171,29 @@ abs-over-mult' (negsucc x) (negsucc y) = I
     iii = pos-multiplication-equiv-to-ℕ (succ x) (succ y) ⁻¹
 
 \end{code}
+
+Lane Biocini 2023
+
+In this section I prove a convenience lemma about the Absolute Value operation,
+then go on to prove a lemma regarding the equivalence of the addition of a positive
+and negative Integer to the Absolute Difference operation in the Naturals, which
+will help us when we prove the triangle inequality in the Integers.
+
+\begin{code}
+
+pos-abs-is-absℤ : (x : ℤ) → pos (abs x) ＝ absℤ x
+pos-abs-is-absℤ (pos x) = refl
+pos-abs-is-absℤ (negsucc x) = refl
+
+abs-pos-plus-negsucc : (x y : ℕ) → abs (pos x +negsucc y) ＝ ∣ x - succ y ∣
+abs-pos-plus-negsucc zero y = ap abs (ℤ+-comm (pos 0) (negsucc y))
+abs-pos-plus-negsucc (succ x) zero = refl
+abs-pos-plus-negsucc (succ x) (succ y) =
+  abs (predℤ (pos (succ x) +negsucc y)) ＝⟨ i ⟩
+  abs (pos x +negsucc y) ＝⟨ abs-pos-plus-negsucc x y ⟩
+  ∣ x - succ y ∣ ∎
+    where
+      i : abs (predℤ (pos (succ x) +negsucc y)) ＝ abs (pos x +negsucc y)
+      i = ap abs (ℤ-left-pred (pos (succ x)) (negsucc y)) ⁻¹
+
+\end{code}

source/Integers/Order.lagda

@@ -6,6 +6,7 @@ Andrew Sneap, 26th November 2021
 
 open import MLTT.Spartan renaming (_+_ to _∔_)
 
+open import Naturals.AbsoluteDifference using (∣_-_∣)
 open import Naturals.Order
 open import Notation.Order
 open import UF.Base
@@ -786,3 +787,77 @@ Added by Todd
  = ℤ-bigger-or-equal-not-less y x y≤x x<y
 
 \end{code}
+
+Lane Biocini 2023
+
+A proof of the triangle inequality in the Integers using the Absolute Difference
+operation defined in the Naturals. We first define 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 ∣ ≤ℕ succ (x ℕ+ y)
+    Γ = triangle-inequality x 0 (succ y)
+
+    γ : ∣ x - succ y ∣ ＝ abs (pos x +negsucc y)
+    γ = abs-pos-plus-negsucc x 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)) ≤ℕ succ (succ x ℕ+ y)
+  Γ = triangle-inequality₀ (succ x) (succ y)
+
+  γ : 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))) ⁻¹
+
+ℤ-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
+    Γ : pos (abs (x + y)) ≤ℤ pos (abs x ℕ+ abs y)
+    Γ = ℕ-order-respects-ℤ-order'' (abs (x + y)) (abs x ℕ+ abs y) (ℤ-triangle-inequality x y)
+
+    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)

source/Naturals/AbsoluteDifference.lagda

@@ -0,0 +1,43 @@
+Lane Biocini 2023
+
+This module defines the Absolute Difference operation, where we take two numbers
+and return the absolute value of the remainder left over after subtracting one
+from the other. It also defines some useful lemmas that will come in handy when
+we tackle the triangle inequality in the Integers, and also to prove the
+Natural Number analog for the triangle inequality.
+
+\begin{code}
+
+{-# OPTIONS --safe --without-K --exact-split #-}
+
+module Naturals.AbsoluteDifference where
+
+open import MLTT.Spartan hiding (_+_)
+open import Naturals.Addition renaming (_+_ to _+_)
+
+∣_-_∣ : ℕ → ℕ → ℕ
+∣ x - zero ∣ = x
+∣ zero - succ y ∣ = succ y
+∣ succ x - succ y ∣ = ∣ x - y ∣
+
+minus-nothing : (x : ℕ) → ∣ 0 - x ∣ ＝ x
+minus-nothing zero = refl
+minus-nothing (succ x) = refl
+
+exact-difference-is-zero : (x : ℕ) → ∣ x - x ∣ ＝ 0
+exact-difference-is-zero zero = refl
+exact-difference-is-zero (succ x) = exact-difference-is-zero x
+
+diff-commutative : (x y : ℕ) → ∣ x - y ∣ ＝ ∣ y - x ∣
+diff-commutative zero y = minus-nothing y
+diff-commutative (succ x) zero = refl
+diff-commutative (succ x) (succ y) = diff-commutative x y
+
+diff-sum : (x y : ℕ) → ∣ x + y - y ∣ ＝ x
+diff-sum zero zero = refl
+diff-sum zero (succ y) = ap (λ u → ∣ u - y ∣) (zero-left-neutral y)
+                         ∙ exact-difference-is-zero y
+diff-sum (succ x) zero = refl
+diff-sum (succ x) (succ y) = diff-sum (succ x) y
+
+\end{code}

source/Naturals/Order.lagda

@@ -9,6 +9,7 @@ module Naturals.Order where
 open import MLTT.Spartan
 
 open import Naturals.Addition renaming (_+_ to _+'_)
+open import Naturals.AbsoluteDifference
 open import Naturals.Properties
 open import Notation.Order
 open import Ordinals.Notions
@@ -804,3 +805,74 @@ less-than-pos-mult : (x y z : ℕ) → x < y → x < y * succ z
 less-than-pos-mult x y z l = <-+ x y (y * z) l
 
 \end{code}
+
+Lane Biocini 2023
+
+Here we define some order lemmas for the Absolute Difference operation and then
+prove the analog of the triangle inequality for the Natural Numbers under it.
+
+\begin{code}
+
+≤-diff : (x y : ℕ) → ∣ x - y ∣ ≤ x +' y
+≤-diff x zero = ≤-refl x
+≤-diff zero (succ y) = ≤-+' zero y
+≤-diff (succ x) (succ y) = γ
+  where
+    Γ : (x +' y) ≤ℕ (succ x +' y)
+    Γ = ≤-trans (x +' y) (succ (x +' y)) (succ x +' y)
+                (≤-succ (x +' y))
+                (equal-gives-less-than-or-equal (succ (x +' y)) (succ x +' y)
+                                                (succ-left x y ⁻¹))
+
+    γ : ∣ x - y ∣ ≤ℕ succ (succ x +' y)
+    γ = ≤-trans₂ ∣ x - y ∣ (x +' y) (succ x +' y) (succ (succ x +' y))
+                 (≤-diff x y) Γ (≤-succ (succ x +' y))
+
+≤-diff-minus : (x y : ℕ) → x ≤ y +' ∣ y - x ∣
+≤-diff-minus zero y = ⋆
+≤-diff-minus (succ x) zero = ≤-+' zero x
+≤-diff-minus (succ x) (succ y) = γ
+  where
+    Γ : x ≤ℕ (y +' ∣ y - x ∣)
+    Γ = ≤-diff-minus x y
+
+    γ : succ x ≤ℕ (succ y +' ∣ y - x ∣)
+    γ = ≤-trans (succ x) (succ (y +' ∣ y - x ∣)) (succ y +' ∣ y - x ∣)
+                 (succ-monotone x (y +' ∣ y - x ∣) Γ)
+                 (equal-gives-less-than-or-equal
+                   (succ (y +' ∣ y - x ∣)) (succ y +' ∣ y - x ∣)
+                   (succ-left y ∣ y - x ∣ ⁻¹))
+
+≤-diff-plus : (x y : ℕ) → x ≤ℕ (∣ x - y ∣ +' y)
+≤-diff-plus zero y = ⋆
+≤-diff-plus (succ x) zero = ≤-refl x
+≤-diff-plus (succ x) (succ y) = ≤-diff-plus x y
+
+triangle-inequality : (x y z : ℕ) → ∣ x - z ∣ ≤ ∣ x - y ∣ +' ∣ y - z ∣
+triangle-inequality zero y z =
+  ≤-trans₂ ∣ zero - z ∣ z (y +' ∣ y - z ∣) (∣ zero - y ∣ +' ∣ y - z ∣) Γ α γ
+    where
+      Γ : ∣ zero - z ∣ ≤ℕ z
+      Γ = equal-gives-less-than-or-equal ∣ zero - z ∣ z
+                                         (minus-nothing z)
+
+      α : z ≤ℕ (y +' ∣ y - z ∣)
+      α = ≤-diff-minus z y
+
+      β : y ≤ℕ ∣ zero - y ∣
+      β = equal-gives-less-than-or-equal y ∣ zero - y ∣ (minus-nothing y ⁻¹)
+
+      γ : (y +' ∣ y - z ∣) ≤ℕ (∣ zero - y ∣ +' ∣ y - z ∣)
+      γ = ≤-adding y ∣ zero - y ∣ ∣ y - z ∣ ∣ y - z ∣ β (≤-refl ∣ y - z ∣)
+triangle-inequality (succ x) zero zero = ≤-refl x
+triangle-inequality (succ x) zero (succ z) =
+  ≤-trans₂ ∣ x - z ∣ (x +' z) (succ (x +' z)) (succ (succ x +' z))
+           (≤-diff x z)
+           (≤-succ (x +' z))
+           (≤-trans (x +' z) (succ (x +' z)) (succ x +' z) (≤-succ (x +' z)) α )
+    where
+      α = equal-gives-less-than-or-equal (succ (x +' z)) (succ x +' z) (succ-left x z ⁻¹)
+triangle-inequality (succ x) (succ y) zero = ≤-diff-plus x y
+triangle-inequality (succ x) (succ y) (succ z) = triangle-inequality x y z
+
+\end{code}