Natural.order

-- Order on ℕ as DATA: a ≤ b is a CODE inhabited by a difference and
-- the Id-witness that it closes the gap — the OnlyZ pattern of
-- Core/id.nova, scaled to a theory. Everything downstream (ℤ order, ℚ
-- order, the reals' moduli and bounds) consumes these as Σ-data, so
-- no choice principle is ever needed: a bound IS its witness.

import Natural (+, *, plusZeroId, zeroPlusId, sucPlus, plusComm, plusAssoc, plusCongL, plusCongR, sucInj, plusCancel, multDistrib, multComm)
import Natural.eq (zNotS)
import Core.equality (trans, sym, cong)
import Core.id (Id, idToEq, eqToId)

infixl 4 ≤
≤ : ℕ → ℕ → 𝕌
(≤) = λa b. (k : ℕ) × Id _ (a + k) b

-- ===== basics =====
leRefl : (a : ℕ) → a ≤ a using (Natural.order.≤.unfold)
leRefl = λa. Z, eqToId _ _ (plusZeroId a)

leOfEq : {a b : ℕ} → (a ≡ b) → a ≤ b using (Natural.order.≤.unfold)
leOfEq = λa b h. Z, eqToId _ _ (trans _ _ _ (plusZeroId a) h)

leZero : (a : ℕ) → Z ≤ a using (Natural.order.≤.unfold)
leZero = λa. a, eqToId _ _ (zeroPlusId a)

-- a + S Z unwinds to S a by computation alone
leSucSelf : (a : ℕ) → a ≤ S a using (Natural.+.eq, Natural.order.≤.unfold)
leSucSelf = λa. S Z, eqToId _ _ ⋆

leStep : {a b : ℕ} → a ≤ b → a ≤ S b
  using (+.eq, Natural.order.≤.eq, Core.id.Id.unfold, Core.id.idToEq.eq, Natural.order.≤.unfold)
leStep = λa b le. S (le .π₁), eqToId _ _ (let h = idToEq _ _ _ (le .π₂) in ⋆)

-- ===== transitivity, antisymmetry =====
leTrans : (a b c : ℕ) → a ≤ b → b ≤ c → a ≤ c using (Core.id.Id.unfold, Natural.order.≤.unfold)
leTrans =
  λa b c l1 l2. (,)
    l1 .π₁ + l2 .π₁
    eqToId
      _
      _
      let h1 = idToEq _ _ _ (l1 .π₂)
          h2 = idToEq _ _ _ (l2 .π₂)
          a + (l1 .π₁ + l2 .π₁)
            ≡⟨ sym _ _ (plusAssoc a (l1 .π₁) (l2 .π₁)) ⟩ a + l1 .π₁ + l2 .π₁
            ≡⟨ plusCongL (l2 .π₁) h1 ⟩ b + l2 .π₁
            ≡⟨ h2 ⟩ c

-- a summand of zero is zero (both sides)
sumZeroR : (x y : ℕ) → (x + y ≡ Z) → y ≡ Z using (Natural.plusSucId)
sumZeroR = λx y. ℕ-elim (λh. ⋆) (j ih. λh. 𝟘-elim (zNotS {x + j} (sym (x + S j) _ h))) y

sumZeroL : (x y : ℕ) → (x + y ≡ Z) → x ≡ Z
sumZeroL = λx y h. sumZeroR _ _ (trans _ _ _ (plusComm x y) h)

leZeroInv : {a : ℕ} → a ≤ Z → a ≡ Z using (Natural.order.≤.unfold)
leZeroInv = λa le. sumZeroL _ _ (trans _ _ Z (idToEq _ _ _ (le .π₂)) ⋆)

leAntisym : (a b : ℕ) → a ≤ b → b ≤ a → a ≡ b using (Core.id.Id.unfold, Natural.order.≤.unfold)
leAntisym =
  λa b l1 l2. let h1 = idToEq _ _ _ (l1 .π₂)
                  h2 = idToEq _ _ _ (l2 .π₂)
                  loop : a + (l1 .π₁ + l2 .π₁) ≡ a
                    = a + (l1 .π₁ + l2 .π₁)
                      ≡⟨ sym _ _ (plusAssoc a (l1 .π₁) (l2 .π₁)) ⟩ a + l1 .π₁ + l2 .π₁
                      ≡⟨ plusCongL (l2 .π₁) h1 ⟩ b + l2 .π₁
                      ≡⟨ h2 ⟩ a
                  kz = plusCancel
                    l1 .π₁ + l2 .π₁
                    Z
                    a
                    l1 .π₁ + l2 .π₁ + a
                      ≡⟨ plusComm a (l1 .π₁ + l2 .π₁) ⟩ a + (l1 .π₁ + l2 .π₁)
                      ≡⟨ loop ⟩ a
                      ≡⟨ sym _ _ (zeroPlusId a) ⟩ Z + a
                  k1z = sumZeroL _ _ kz
                  a
                    ≡⟨ sym _ _ (plusZeroId a) ⟩ a + Z
                    ≡⟨ plusCongR a (sym _ _ k1z) ⟩ a + l1 .π₁
                    ≡⟨ h1 ⟩ b

-- ===== monotonicity =====
leSucMono : {a b : ℕ} → a ≤ b → S a ≤ S b using (Core.id.Id.unfold, Natural.order.≤.unfold)
leSucMono =
  λa b le. (,)
    le .π₁
    eqToId
      _
      _
      let h = idToEq _ _ _ (le .π₂)
          S a + le .π₁ ≡⟨ sucPlus a (le .π₁) ⟩ S (a + le .π₁) ≡⟨ cong (λu. ℕ) (λu. S u) h ⟩ S b

leSucInv : (a b : ℕ) → S a ≤ S b → a ≤ b using (Core.id.Id.unfold, Natural.order.≤.unfold)
leSucInv =
  λa b le. (,)
    le .π₁
    eqToId
      _
      _
      sucInj
        a + le .π₁
        b
        let h = idToEq _ _ _ (le .π₂)
            S (a + le .π₁) ≡⟨ sym _ _ (sucPlus a (le .π₁)) ⟩ S a + le .π₁ ≡⟨ h ⟩ S b

lePlusMonoR : {a : ℕ} (b c : ℕ) → a ≤ b → a + c ≤ b + c
  using (Core.id.Id.unfold, Natural.order.≤.unfold)
lePlusMonoR =
  λa b c le. (,)
    le .π₁
    eqToId
      _
      _
      let h = idToEq _ _ _ (le .π₂)
          a + c + le .π₁
            ≡⟨ plusAssoc a c (le .π₁) ⟩ a + (c + le .π₁)
            ≡⟨ plusCongR a (plusComm (le .π₁) c) ⟩ a + (le .π₁ + c)
            ≡⟨ sym _ _ (plusAssoc a (le .π₁) c) ⟩ a + le .π₁ + c
            ≡⟨ plusCongL c h ⟩ b + c

lePlusMonoL : {a b : ℕ} (c : ℕ) → a ≤ b → c + a ≤ c + b using (Natural.order.≤.unfold)
lePlusMonoL =
  λa b c le. leTrans
    _
    _
    _
    leOfEq (plusComm a c)
    leTrans _ _ _ (lePlusMonoR _ c le) (leOfEq (plusComm c b))

leMultMonoR : {a b : ℕ} (c : ℕ) → a ≤ b → a * c ≤ b * c
  using (Core.id.Id.unfold, Natural.order.≤.unfold)
leMultMonoR =
  λa b c le. (,)
    le .π₁ * c
    eqToId
      _
      _
      let h = idToEq _ _ _ (le .π₂)
          a * c + le .π₁ * c
            ≡⟨ plusCongL (le .π₁ * c) (multComm c a) ⟩ c * a + le .π₁ * c
            ≡⟨ plusCongR (c * a) (multComm c (le .π₁)) ⟩ c * a + c * le .π₁
            ≡⟨ sym _ _ (multDistrib c a (le .π₁)) ⟩ c * (a + le .π₁)
            ≡⟨ multComm (a + le .π₁) c ⟩ (a + le .π₁) * c
            ≡⟨ cong (λu. ℕ) (λu. u * c) h ⟩ b * c

-- ===== totality: the DECISION, as data =====
leTotal : (a b : ℕ) → a ≤ b ⊎ b ≤ a
leTotal =
  λa. ℕ-elim
    λb. inj₁ (leZero _)
    j ih. λb. ℕ-elim
      inj₂ (leZero _)
      i ih2. ⊎-elim (u. inj₁ (leSucMono u)) (u. inj₂ (leSucMono u)) (ih i)
      b
    a