IEEE754.RationalOrder

module IEEE754.RationalOrder where

open import IEEE754.Prelude
open import IEEE754.Exact
open import IEEE754.FiniteSpec

import Cubical.Data.Int as ℤ
import Cubical.Data.Int.Order as ℤOrder
import Cubical.Data.Nat.Order as ℕOrder
import Cubical.Data.Rationals as ℚ
import Cubical.Data.Rationals.Order as ℚOrder

infix 4 _≤ℚ_ _<ℚ_ _≥ℚ_ _>ℚ_

_≤ℚ_ : ℚ.ℚ → ℚ.ℚ → Type₀
_≤ℚ_ = ℚOrder._≤_

_<ℚ_ : ℚ.ℚ → ℚ.ℚ → Type₀
_<ℚ_ = ℚOrder._<_

_≥ℚ_ : ℚ.ℚ → ℚ.ℚ → Type₀
left ≥ℚ right = right ≤ℚ left

_>ℚ_ : ℚ.ℚ → ℚ.ℚ → Type₀
left >ℚ right = right <ℚ left

isProp≤ℚ :
  (left right : ℚ.ℚ) →
  isProp (left ≤ℚ right)
isProp≤ℚ = ℚOrder.isProp≤

≤ℚ-refl :
  (value : ℚ.ℚ) →
  value ≤ℚ value
≤ℚ-refl = ℚOrder.isRefl≤

≤ℚ-trans :
  (left middle right : ℚ.ℚ) →
  left ≤ℚ middle →
  middle ≤ℚ right →
  left ≤ℚ right
≤ℚ-trans = ℚOrder.isTrans≤

≤ℚ-antisym :
  (left right : ℚ.ℚ) →
  left ≤ℚ right →
  right ≤ℚ left →
  left ≡ right
≤ℚ-antisym = ℚOrder.isAntisym≤

<ℚ-weaken :
  (left right : ℚ.ℚ) →
  left <ℚ right →
  left ≤ℚ right
<ℚ-weaken = ℚOrder.<Weaken≤

≤ℚ-subst-left :
  ∀ {left middle right} →
  left ≡ middle →
  middle ≤ℚ right →
  left ≤ℚ right
≤ℚ-subst-left {right = right} path proof =
  subst (λ value → value ≤ℚ right) (sym path) proof

≤ℚ-subst-right :
  ∀ {left middle right} →
  middle ≡ right →
  left ≤ℚ middle →
  left ≤ℚ right
≤ℚ-subst-right {left = left} path proof =
  subst (λ value → left ≤ℚ value) path proof

record ℚInterval (lower upper value : ℚ.ℚ) : Type₀ where
  constructor in-ℚ-interval
  field
    lower≤value : lower ≤ℚ value
    value≤upper : value ≤ℚ upper

ℚInterval-refl :
  (value : ℚ.ℚ) →
  ℚInterval value value value
ℚInterval-refl value =
  in-ℚ-interval (≤ℚ-refl value) (≤ℚ-refl value)

ℚInterval-transport :
  ∀ {lower upper value newValue} →
  value ≡ newValue →
  ℚInterval lower upper value →
  ℚInterval lower upper newValue
ℚInterval-transport {lower = lower} {upper = upper} path interval =
  in-ℚ-interval
    (subst
      (λ value → lower ≤ℚ value)
      path
      (ℚInterval.lower≤value interval))
    (subst
      (λ value → value ≤ℚ upper)
      path
      (ℚInterval.value≤upper interval))

zeroMagnitude-nonnegative :
  rationalZero ≤ℚ rationalZero
zeroMagnitude-nonnegative = ≤ℚ-refl rationalZero

natℚ-monotone :
  (m n : ℕ) →
  m ℕOrder.≤ n →
  natℚ m ≤ℚ natℚ n
natℚ-monotone m n m≤n =
  subst2
    ℤOrder._≤_
    (sym (ℤ.·IdR (ℤ.pos m)))
    (sym (ℤ.·IdR (ℤ.pos n)))
    (ℤOrder.m≤n→posm≤posn m≤n)

natℚ-nonnegative :
  (n : ℕ) →
  rationalZero ≤ℚ natℚ n
natℚ-nonnegative n =
  natℚ-monotone 0 n ℕOrder.zero-≤

scaleNatByPowerOfTwo-nonnegative :
  (n : ℕ) →
  (exponent : ℤ.ℤ) →
  rationalZero ≤ℚ scaleNatByPowerOfTwo n exponent
scaleNatByPowerOfTwo-nonnegative n (ℤ.pos exponent) =
  subst2
    ℤOrder._≤_
    (sym (ℤ.·IdR (ℤ.pos 0)))
    (sym (ℤ.·IdR (ℤ.pos (n · (2 ^ exponent)))))
    (ℤOrder.zero-≤pos {l = n · (2 ^ exponent)})
scaleNatByPowerOfTwo-nonnegative n (ℤ.negsuc exponent) =
  subst2
    ℤOrder._≤_
    (sym (ℤ.·AnnihilL
      (ℚ.ℕ₊₁→ℤ (powerOfTwoDenominator (suc exponent)))))
    (sym (ℤ.·IdR (ℤ.pos n)))
    (ℤOrder.zero-≤pos {l = n})

pow2ℚ-nonnegative :
  (exponent : ℤ.ℤ) →
  rationalZero ≤ℚ pow2ℚ exponent
pow2ℚ-nonnegative (ℤ.pos exponent) =
  natℚ-nonnegative (2 ^ exponent)
pow2ℚ-nonnegative (ℤ.negsuc exponent) =
  scaleNatByPowerOfTwo-nonnegative 1 (ℤ.negsuc exponent)

scaleNatByPowerOfTwo-monotone :
  (m n : ℕ) →
  (exponent : ℤ.ℤ) →
  m ℕOrder.≤ n →
  scaleNatByPowerOfTwo m exponent ≤ℚ
  scaleNatByPowerOfTwo n exponent
scaleNatByPowerOfTwo-monotone m n exponent m≤n =
  subst2
    _≤ℚ_
    (scaleNatByPowerOfTwo-product m exponent)
    (scaleNatByPowerOfTwo-product n exponent)
    (ℚOrder.≤-·o
      (natℚ m)
      (natℚ n)
      (pow2ℚ exponent)
      (pow2ℚ-nonnegative exponent)
      (natℚ-monotone m n m≤n))

≤ℚ-mul-right-nonnegative :
  (left right factor : ℚ.ℚ) →
  rationalZero ≤ℚ factor →
  left ≤ℚ right →
  (left ℚ.· factor) ≤ℚ (right ℚ.· factor)
≤ℚ-mul-right-nonnegative = ℚOrder.≤-·o