From c14c850a5dbe21979112b52038af9c5c51ab5b29 Mon Sep 17 00:00:00 2001
From: Lane Biocini <lane@mailbox.org>
Date: Tue, 17 Oct 2023 17:09:16 -0400
Subject: [PATCH] Natural Order definition utilizing an identity type

---
 source/Naturals/IdOrder.lagda | 400 ++++++++++++++++++++++++++++++++++
 source/Naturals/index.lagda   |   1 +
 2 files changed, 401 insertions(+)
 create mode 100644 source/Naturals/IdOrder.lagda

diff --git a/source/Naturals/IdOrder.lagda b/source/Naturals/IdOrder.lagda
new file mode 100644
index 000000000..2f7d19246
--- /dev/null
+++ b/source/Naturals/IdOrder.lagda
@@ -0,0 +1,400 @@
+Lane Biocini, 12 October 2023
+
+Following the equality case of the triangle inequality, we can define a
+partial order on ℕ directly with an identity type, namely by considering
+the fixed points of the family of functions indexed by x of the form (λ y
+→ ∣ y - x ∣ + x). This is because the only inhabitants of these fixed
+point equalities are identities where x is less than or equal to y. And
+because ℕ is a set, each term of this identity type thereby becomes a
+proposition, although in contrast to the standard order definition based
+on 𝟙 each inhabitant of our order type is its own distinct refl term and
+hence distinct inequalities will not be equal terms.
+
+In hindsight it is obvious a type such as this ought to be possible,
+because the definition for the standard order module essentially
+calculates the inhabitation of its type by the same recursion algorithm as
+absolute difference, with the provision that the succ x ≤ zero case is
+defined as the empty type. Our definition leads to a partial order type
+with interesting properties. As opposed to the one generated by a function
+from ℕ to 𝟙, we are able to work directly with the identifications that
+specify the order relation, so 'succ-lc' for example will translate an
+inequality of 'succ m ≼ succ n' to 'm ≼ n', and likewise with 'ap succ'
+for the other direction. Negation is directly handled by the standard
+negation proofs for the Naturals. The use of transport is ergonomic as
+each term is directly an identity term. Our type definition also has
+strong computational properties that assist Agda's case matching as
+opposed to the standard definition; you will never see it attempt to match
+for the case 'succ x ≼ zero' as Agda can automatically detect this type
+is uninhabited.
+
+We use the curly order '≼' so as not to conflict with the one already
+defined for the Naturals. Although the early portions of this module were
+written myself, after I translated Escardo's definition of ≤-induction to
+this type I decided to go further and have begun translating all the Order
+lemmas in the standard module to accommodate this definition. For the most
+part, I have attempted to preserve the titles and type definitions
+exactly, but in the earlier sections of the modules I took some liberties
+as I wanted to tailor the most fundamental lemmas to the character of this
+type, and also to make certain operations more ergonomic and reduce the
+character count of proofs. Notably, 'equal-gives-less-than-or-equal' is
+simply '≼-＝' here.
+
+Aside from the fundamental lemmas as well as ones concerning absolute
+difference the credit for most of the type definitions that will be listed
+here goes to the efforts of Martin Escardo, Tom de Jong, and Andrew Sneap.
+Sometimes I needed to tailor their proofs to fit our order definition, but
+in many cases I was able to use essentially the same principles from
+proofs in the other module to guide the equivalent proofs here.
+
+\begin{code}
+
+{-# OPTIONS --safe --without-K --exact-split #-}
+
+module Naturals.IdOrder where
+
+open import MLTT.Spartan renaming (_+_ to _∔_)
+open import MLTT.Plus-Properties using (+functor)
+
+open import Naturals.Addition using (_+_; zero-left-neutral; succ-left;
+ addition-commutativity; addition-right-cancellable)
+open import Naturals.AbsoluteDifference
+open import Naturals.Order using (_≤ℕ_)
+open import Naturals.Properties using (positive-not-zero; succ-lc)
+open import Naturals.Multiplication using (_*_)
+
+open import Notation.General
+open import Notation.Order
+open import NotionsOfDecidability.Decidable
+
+open import UF.Base using (transport₂)
+open import UF.DiscreteAndSeparated using (discrete-types-are-sets;
+ is-discrete; ℕ-is-set; props-are-discrete)
+open import UF.Equiv using (_≅_)
+open import UF.Sets using (is-set)
+open import UF.Subsingletons using (is-prop)
+
+_≼ℕ_ : ℕ → ℕ → 𝓤₀ ̇
+x ≼ℕ y = ∣ y - x ∣ + x ＝ y
+
+infix 30 _≼ℕ_
+
+instance
+ Curly-Order-ℕ-ℕ : Curly-Order ℕ ℕ
+ _≼_ {{Curly-Order-ℕ-ℕ}} = _≼ℕ_
+
+private
+ example : 0 ≼ 2
+ example = refl
+
+ example2 : ¬ (1 ≼ 0)
+ example2 = positive-not-zero 1
+
+≼-is-prop-valued : (x y : ℕ) → is-prop (x ≼ y)
+≼-is-prop-valued x y p q = ℕ-is-set p q
+
+≼-is-discrete : (x y : ℕ) → is-discrete (x ≼ y)
+≼-is-discrete x y = props-are-discrete (≼-is-prop-valued x y)
+
+≼-is-set : (x y : ℕ) → is-set (x ≼ y)
+≼-is-set x y p q = discrete-types-are-sets (≼-is-discrete x y) p q
+
+≼-dichotomous : (x y : ℕ) → (x ≼ y) ∔ (y ≼ x)
+≼-dichotomous x y = +functor (_⁻¹) (_⁻¹) (diff-cancellable x y)
+
+zero-least : (x : ℕ) → zero ≼ x
+zero-least x = refl
+
+unique-least : (x : ℕ) → x ≼ zero → x ＝ zero
+unique-least zero p = refl
+
+≼-intro : (x y m n : ℕ)
+        → (x ＝ succ m)
+        → (y ＝ succ (succ (m + n)))
+        → x ≼ y
+≼-intro x y zero zero p q = transport₂ (_≼ℕ_) (p ⁻¹) (q ⁻¹) refl
+≼-intro x y zero (succ n) p q = transport₂ (_≼ℕ_) (p ⁻¹) (q ⁻¹)
+ (ap succ (zero-least (succ (succ (0 + n)))))
+≼-intro (succ x) (succ y) (succ m) n p q = ap succ
+ (≼-intro x y m n (succ-lc p)
+  (succ-lc (q ∙ ap (succ ^ 2) (succ-left m n))))
+
+≼-refl : reflexive _≼ℕ_
+≼-refl x = ap (_+ x) (difference-is-zero x) ∙ zero-left-neutral x
+
+≼-anti : antisymmetric _≼ℕ_
+≼-anti x zero p q = unique-least x p
+≼-anti (succ x) (succ y) p q = ap succ
+ (≼-anti x y (succ-lc p) (succ-lc q))
+
+≼-trans : transitive _≼ℕ_
+≼-trans zero y z p q = zero-least z
+≼-trans (succ x) (succ y) (succ z) p q =
+ ap succ (≼-trans x y z (succ-lc p) (succ-lc q))
+
+≼-trans₂ : (x y z w : ℕ) → x ≼ y → y ≼ z → z ≼ w → x ≼ w
+≼-trans₂ x y z w p q r = ≼-trans x y w p (≼-trans y z w q r )
+
+≼-transport₂ : {x y z w : ℕ} → x ＝ z → y ＝ w → x ≼ y → z ≼ w
+≼-transport₂ p q i = transport₂ (_≼ℕ_) p q i
+
+≼-＝ : (x y : ℕ) → x ＝ y → x ≼ y
+≼-＝ x y p = transport (x ≼ℕ_) p (≼-refl x)
+
+_≼⟨_⟩_ : (x : ℕ) {y z : ℕ} → x ≼ y → y ≼ z → x ≼ z
+(_≼⟨_⟩_) x {y} {z} p q = ≼-trans x y z p q
+
+_◻ : (x : ℕ) → x ≼ x
+_◻ = ≼-refl
+
+infixr 0 _≼⟨_⟩_
+infix  1 _◻
+
+private instance
+ Reasoning-Chain-≼ℕ : Reasoning-Chain ℕ ℕ ℕ (_≼ℕ_) (_≼ℕ_) (_≼ℕ_)
+ _⸴_⊢_ {{Reasoning-Chain-≼ℕ}} = _≼⟨_⟩_
+
+ Reflexive-Order-≼ℕ : Reflexive-Order ℕ (_≼ℕ_)
+ _▨ {{Reflexive-Order-≼ℕ}} = ≼-refl
+
+\end{code}
+
+Order lemmas for the successor constructor
+
+\begin{code}
+
+≼-succ : (x : ℕ) → x ≼ succ x
+≼-succ zero = refl
+≼-succ (succ x) = ap succ (≼-succ x)
+
+≼-succ^ : (n x : ℕ) → x ≼ (succ ^ n) x
+≼-succ^ zero x = ≼-refl x
+≼-succ^ (succ n) x = ≼-trans x (succ x) (succ (rec x succ n))
+ (≼-succ x) (ap succ (≼-succ^ n x))
+
+≼-close-left : (x y : ℕ) → succ x ≼ y → x ≼ y
+≼-close-left x y i = ≼-trans x (succ x) y (≼-succ x) i
+
+≼-close-right : (x y : ℕ) → x ≼ y → x ≼ succ y
+≼-close-right x y i = ≼-trans x y (succ y) i (≼-succ y)
+
+succ-monotone : (x y : ℕ) → x ≼ y → succ x ≼ succ y
+succ-monotone x y = ap succ
+
+succ-order-injective : (x y : ℕ) → succ x ≼ succ y → x ≼ y
+succ-order-injective x y = succ-lc
+
+¬≼-succ-lc : (x y : ℕ) → ¬ (succ x ≼ succ y) → ¬ (x ≼ y)
+¬≼-succ-lc x y l = l ∘ ap succ
+
+succ-not-less-than-zero : (x : ℕ) → ¬ (succ x ≼ℕ zero)
+succ-not-less-than-zero x = positive-not-zero (succ x + x)
+
+\end{code}
+
+Some general properties of _≼_, notably we prove the induction principle
+for it as well as the equivalence of our definition to the standard order
+definition.
+
+\begin{code}
+
+≼-induction : (A : (x y : ℕ) (i : x ≼ y) → 𝓤 ̇ )
+            → ((y : ℕ) → A zero y (zero-least y))
+            → ((x y : ℕ) (i : x ≼ y)
+                    → A x y i
+                    → A (succ x) (succ y) (succ-monotone x y i))
+            → (x y : ℕ) (i : x ≼ y) → A x y i
+≼-induction A b f zero y i = transport (A zero y)
+ (ℕ-is-set refl i) (b y)
+≼-induction A b f (succ x) (succ y) i = transport (A (succ x) (succ y))
+ (ℕ-is-set (ap succ (succ-lc i)) i)
+ (f x y (succ-lc i) (≼-induction A b f x y (succ-lc i)))
+
+≼-decidable : (x y : ℕ) → is-decidable (x ≼ y)
+≼-decidable zero y = inl refl
+≼-decidable (succ x) zero = inr (succ-not-less-than-zero x)
+≼-decidable (succ x) (succ y) =
+ +functor (ap succ) (λ u v → u (succ-lc v)) (≼-decidable x y)
+
+≤-≅-≼ : (x y : ℕ) → (x ≤ y) ≅ (x ≼ y)
+≤-≅-≼ x y = α x y , β x y , γ x y , δ x y
+ where
+  α : (x y : ℕ) → x ≤ℕ y → x ≼ℕ y
+  α zero y i = zero-least y
+  α (succ x) (succ y) i = ap succ (α x y i)
+
+  β : (x y : ℕ) → x ≼ℕ y → x ≤ℕ y
+  β zero y i = ⋆
+  β (succ x) (succ y) i = β x y (succ-lc i)
+
+  γ : (x y : ℕ) → (λ i → β x y (α x y i)) ∼ id
+  γ zero y i = refl
+  γ (succ x) (succ y) i = I ∙ γ x y i
+   where
+    f : (m n : ℕ) → (p : m ＝ n) → succ-lc (ap succ p) ＝ p
+    f m n p = ℕ-is-set (succ-lc (ap succ p)) p
+
+    I : β x y (succ-lc (ap succ (α x y i))) ＝ β x y (α x y i)
+    I = ap (β x y) (f (∣ y - x ∣ + x) y (α x y i))
+
+  δ : (x y : ℕ) → (λ i → α x y (β x y i)) ∼ id
+  δ zero y i = ℕ-is-set refl i
+  δ (succ x) (succ y) i = ℕ-is-set (ap succ (α x y (β x y (succ-lc i)))) i
+
+≼-split : (x y : ℕ) → x ≼ succ y → (x ≼ y) ∔ (x ＝ succ y)
+≼-split zero y i = inl refl
+≼-split (succ x) zero i = inr (ap succ (unique-least x (succ-lc i)))
+≼-split (succ x) (succ y) i =
+ +functor (ap succ) (ap succ) (≼-split x y (succ-lc i))
+
+≼-join : (x y : ℕ) → (x ≼ y) ∔ (x ＝ succ y) → x ≼ succ y
+≼-join x y (inl i) = ≼-close-right x y i
+≼-join x y (inr l) = ≼-＝ x (succ y) l
+
+≼-down : (x y : ℕ) → x ≼ succ y → (x ≠ succ y) → (x ≼ y)
+≼-down x y i l = cases id (𝟘-elim ∘ l) (≼-split x y i)
+
+\end{code}
+
+Here we define the strict order and its associated lemmas. As above,
+many of the proofs here are heavily guided by the equivalent ones
+in the other module, and type definitions and names are preserved
+for compatibility.
+
+\begin{code}
+
+_≺ℕ_ : ℕ → ℕ → 𝓤₀ ̇
+x ≺ℕ y = succ x ≼ y
+
+infix 30 _≺ℕ_
+
+instance
+ Strict-Curly-Order-ℕ-ℕ : Strict-Curly-Order ℕ ℕ
+ _≺_ {{Strict-Curly-Order-ℕ-ℕ}} = _≺ℕ_
+
+not-less-than-itself : (x : ℕ) → ¬ (x ≺ x)
+not-less-than-itself x e = 𝟘-elim (positive-not-zero ∣ x - succ x ∣
+ (addition-right-cancellable (succ ∣ x - succ x ∣) 0 x
+  (succ-left ∣ x - succ x ∣ x  ∙ e ∙ zero-left-neutral x ⁻¹)))
+
+not-less-bigger-or-equal : (x y : ℕ) → ¬ (y ≺ x) → y ≽ x
+not-less-bigger-or-equal zero y l = zero-least y
+not-less-bigger-or-equal (succ x) zero l = 𝟘-elim (l (zero-least (succ x)))
+not-less-bigger-or-equal (succ x) (succ y) l =
+ ap succ (not-less-bigger-or-equal x y (¬≼-succ-lc (succ y) x l))
+
+bigger-or-equal-not-less : (x y : ℕ) → y ≽ x → ¬ (y ≺ x)
+bigger-or-equal-not-less x y i l =
+ not-less-than-itself y (≼-trans (succ y) x y l i)
+
+less-not-bigger-or-equal : (x y : ℕ) → x ≺ y → ¬ (y ≼ x)
+less-not-bigger-or-equal x y i l = bigger-or-equal-not-less y x l i
+
+bounded-∀-next : (A : ℕ → 𝓤 ̇ ) (n : ℕ)
+               → A n
+               → ((k : ℕ) → k ≺ n → A k)
+               → (x : ℕ) → x ≺ succ n → A x
+bounded-∀-next A n a φ x i =
+ cases (φ x) (λ u → transport⁻¹ A (succ-lc u) a) (≼-split (succ x) n i)
+
+\end{code}
+
+Order lemmas for addition
+
+\begin{code}
+
+≼-+ : (x y : ℕ) → x ≼ x + y
+≼-+ zero y = zero-least (zero + y)
+≼-+ (succ x) y =
+ transport (λ u → succ x ≼ℕ u) (succ-left x y ⁻¹) (ap succ (≼-+ x y))
+
+≼-add-right : (x y z : ℕ) → x ≼ y → x + z ≼ y + z
+≼-add-right x y zero p = p
+≼-add-right x y (succ z) p = ap succ (≼-add-right x y z p)
+
+≼-add-left : (x y z : ℕ) → x ≼ y → z + x ≼ z + y
+≼-add-left zero y z p = ≼-+ z y
+≼-add-left (succ x) y z p =
+ transport₂ (_≼ℕ_) (addition-commutativity (succ x) z)
+  (addition-commutativity y z)
+  (≼-add-right (succ x) y z p)
+
+\end{code}
+
+Order lemmas for absolute difference. It is an interesting result
+that we can use an order defined by absolute difference to prove lemmas
+regarding this same operation, or to put it another way, that lemmas about
+absolute difference are directly lemmas about how terms are ordered in ℕ.
+
+\begin{code}
+
+≼-diff-split : (x y : ℕ)
+             → ∣ x - y ∣ ≼ ∣ x - succ y ∣
+             ∔ ∣ x - y ∣ ≼ ∣ succ x - y ∣
+≼-diff-split zero y = inl (transport (λ u → u ≼ succ y)
+ (minus-nothing y ⁻¹) (≼-succ y))
+≼-diff-split (succ x) zero = inr (ap succ (≼-succ x))
+≼-diff-split (succ x) (succ y) = ≼-diff-split x y
+
+≼-succ-pred-split : (x y : ℕ)
+                  → ∣ x - succ y ∣ ≼ ∣ succ x - y ∣
+                  ∔ ∣ succ x - y ∣ ≼ ∣ x - succ y ∣
+≼-succ-pred-split zero zero = inl refl
+≼-succ-pred-split zero (succ y) = inr (transport (_≼ℕ succ (succ y))
+ (minus-nothing y ⁻¹) (≼-succ^ 2 y))
+≼-succ-pred-split (succ x) zero = inl (≼-succ^ 2 x)
+≼-succ-pred-split (succ x) (succ y) = ≼-succ-pred-split x y
+
+≼-diff-sum-left : (x y : ℕ) → x ≼ y + ∣ y - x ∣
+≼-diff-sum-left zero y = zero-least (y + y)
+≼-diff-sum-left (succ x) zero =
+ ap succ (≼-＝ x (zero + x) (zero-left-neutral x ⁻¹))
+≼-diff-sum-left (succ x) (succ y) =
+ ≼-trans (succ x) (succ (y + ∣ y - x ∣)) (succ y + ∣ y - x ∣)
+  (ap succ (≼-diff-sum-left x y))
+  (≼-＝ (succ (y + ∣ y - x ∣)) (succ y + ∣ y - x ∣)
+   (succ-left y ∣ y - x ∣ ⁻¹))
+
+≼-diff-sum-right : (x y : ℕ) → x ≼ ∣ x - y ∣ + y
+≼-diff-sum-right x zero = ≼-refl x
+≼-diff-sum-right zero (succ y) = zero-least (succ (succ y + y))
+≼-diff-sum-right (succ x) (succ y) = ap succ (≼-diff-sum-right x y)
+
+diff-succ-less-than-succ-diff : (x y : ℕ) → ∣ succ x - y ∣ ≼ℕ succ ∣ x - y ∣
+diff-succ-less-than-succ-diff zero zero = refl
+diff-succ-less-than-succ-diff zero (succ y) =
+ transport⁻¹ (λ u → u ≼ succ (succ y)) (minus-nothing y) (≼-succ^ 2 y)
+diff-succ-less-than-succ-diff (succ x) zero = ≼-refl (succ (succ x))
+diff-succ-less-than-succ-diff (succ x) (succ y) =
+ diff-succ-less-than-succ-diff x y
+
+diff-pred-less-than-succ-diff : (x y : ℕ)
+                              →  ∣ x - succ y ∣ ≼ℕ succ ∣ x - y ∣
+diff-pred-less-than-succ-diff zero y = transport⁻¹ (λ u → succ y ≼ succ u)
+ (minus-nothing y)
+ (ap succ (≼-refl y))
+diff-pred-less-than-succ-diff (succ x) zero = ≼-succ^ 2 x
+diff-pred-less-than-succ-diff (succ x) (succ y) =
+ diff-pred-less-than-succ-diff x y
+
+diff-less-than-succ-diff-pred : (x y : ℕ) → ∣ x - y ∣ ≼ succ ∣ x - succ y ∣
+diff-less-than-succ-diff-pred zero y = transport⁻¹ (_≼ℕ succ (succ y))
+ (minus-nothing y)
+ (≼-succ^ 2 y)
+diff-less-than-succ-diff-pred (succ x) y =
+ diff-succ-less-than-succ-diff x y
+
+diff-less-than-sum : (x y : ℕ) → ∣ x - y ∣ ≼ x + y
+diff-less-than-sum x zero = ≼-refl x
+diff-less-than-sum x (succ y) =
+ ≼-trans ∣ x - succ y ∣ (succ ∣ x - y ∣) (succ (x + y))
+ (diff-pred-less-than-succ-diff x y) (ap succ (diff-less-than-sum x y))
+
+triangle-inequality : (x y z : ℕ) → ∣ x - z ∣ ≼ ∣ x - y ∣ + ∣ y - z ∣
+triangle-inequality x zero z = transport⁻¹ (λ u → ∣ x - z ∣ ≼ℕ x + u)
+ (minus-nothing z) (diff-less-than-sum x z)
+triangle-inequality x (succ y) zero = ≼-diff-sum-right x (succ y)
+triangle-inequality zero (succ y) (succ z) =
+ ≼-diff-sum-left (succ z) (succ y)
+triangle-inequality (succ x) (succ y) (succ z) = triangle-inequality x y z
+
+\end{code}
diff --git a/source/Naturals/index.lagda b/source/Naturals/index.lagda
index 7546566fa..070d2e456 100644
--- a/source/Naturals/index.lagda
+++ b/source/Naturals/index.lagda
@@ -9,6 +9,7 @@ import Naturals.Addition
 import Naturals.Binary
 import Naturals.Division
 import Naturals.Exponentiation
+import Naturals.IdOrder
 import Naturals.HCF
 import Naturals.Multiplication
 import Naturals.Order