open import 1Lab.Prelude

open import Data.Int

import Data.Nat as Nat

module Data.Int.Order where

Ordering integersπŸ”—

private
  le-lemma
    : βˆ€ a b x y
    β†’ Path (n-Type lzero 1)
      (el (a + y Nat.≀ b + x) Nat.≀-is-prop)
      (el (a + suc y Nat.≀ b + suc x) Nat.≀-is-prop)
  le-lemma a b x y = n-ua
    (prop-ext Nat.≀-is-prop Nat.≀-is-prop
      (Ξ» p β†’ transport (apβ‚‚ Nat._≀_ (sym (Nat.+-sucr a y)) (sym (Nat.+-sucr b x))) (Nat.s≀s p))
      (Ξ» p β†’ Nat.≀-peel (transport (apβ‚‚ Nat._≀_ (Nat.+-sucr a y) (Nat.+-sucr b x)) p)))

  le-lemmaβ€²
    : βˆ€ a b x y
    β†’ Path (n-Type lzero 1)
      (el (a + x Nat.≀ b + y) Nat.≀-is-prop)
      (el (suc (a + x) Nat.≀ suc (b + y)) Nat.≀-is-prop)
  le-lemmaβ€² a b x y = n-ua
    (prop-ext Nat.≀-is-prop Nat.≀-is-prop Nat.s≀s Ξ» { (Nat.s≀s x) β†’ x })

Int-le-prop : Int β†’ Int β†’ Prop lzero
Int-le-prop (diff a b) (diff c d)     = el (a + d Nat.≀ b + c) Nat.≀-is-prop
Int-le-prop (diff a b) (quot x y i)   = le-lemma a b x y i
Int-le-prop (quot m n i) (diff x y)   = le-lemmaβ€² m n y x i
Int-le-prop (quot a b i) (quot c d j) =
  is-set→squarep (λ _ _ → n-Type-is-hlevel 1)
    (Ξ» i β†’ le-lemmaβ€² a b d c i)
    (Ξ» i β†’ le-lemma a b c d i)
    (n-ua
      (prop-ext Nat.≀-is-prop Nat.≀-is-prop
      (Ξ» p β†’
          transport
          (apβ‚‚ Nat._≀_ (sym (ap suc (Nat.+-sucr a d)))
          (sym (ap suc (Nat.+-sucr b c))))
          (Nat.s≀s p))
      (Ξ» p β†’
          Nat.≀-peel
          (transport
          (apβ‚‚ Nat._≀_ (ap suc (Nat.+-sucr a d)) (ap suc (Nat.+-sucr b c)))
          p))))
    (Ξ» i β†’ le-lemmaβ€² a b (suc d) (suc c) i)
    i j

_≀_ : Int β†’ Int β†’ Type
x ≀ y = ∣ Int-le-prop x y ∣

≀-refl : βˆ€ {x} β†’ x ≀ x
≀-refl {x} = Int-elim-prop {P = Ξ» x β†’ x ≀ x} (Ξ» _ β†’ hlevel!)
  (Ξ» a b β†’ subst (a + b Nat.≀_) (Nat.+-commutative a b) Nat.≀-refl)
  x

private
  sum≀0-l : βˆ€ x y β†’ (x + y) Nat.≀ 0 β†’ x ≑ 0
  sum≀0-l zero zero p = refl

  sum≀0-r : βˆ€ x y β†’ (x + y) Nat.≀ 0 β†’ y ≑ 0
  sum≀0-r zero zero p = refl

≀-trans : βˆ€ {x y z} β†’ x ≀ y β†’ y ≀ z β†’ x ≀ z
≀-trans {x} {y} {z} p q with by-sign x | by-sign y | by-sign z
... | negv x | posv y | posv z = Nat.0≀x
... | negv x | negv y | posv z = Nat.0≀x
... | posv x | posv y | posv z = Nat.≀-trans p (subst (Nat._≀ z) (Nat.+-zeror y) q)
... | negv x | negv y | negv z = Nat.≀-trans q (subst (Ξ» e β†’ suc e Nat.≀ suc (x + 0)) (sym (Nat.+-zeror y)) p)
... | posv x | posv y | negv z = absurd (Nat.zeroβ‰ suc (sym (sum≀0-r y (suc z) q)))
... | posv x | negv y | posv z = absurd (Nat.zeroβ‰ suc (sym (sum≀0-r x (suc y) p)))
... | posv x | negv y | negv z = absurd (Nat.zeroβ‰ suc (sym (sum≀0-r x (suc y) p)))
... | negv x | posv y | negv z = absurd (Nat.zeroβ‰ suc (sym (sum≀0-r y (suc z) q)))

≀-antisym : βˆ€ {x y} β†’ x ≀ y β†’ y ≀ x β†’ x ≑ y
≀-antisym {x} {y} p q with by-sign x | by-sign y
... | posv x | negv y = absurd (Nat.zeroβ‰ suc (sym (sum≀0-r x (suc y) p)))
... | negv x | posv y = absurd (Nat.zeroβ‰ suc (sym (sum≀0-r y (suc x) q)))
... | negv x | negv y = ap (Ξ» e β†’ diff 0 (suc e)) $
  Nat.≀-antisym
    (subst (x Nat.≀_) (Nat.+-zeror y) (Nat.≀-peel q))
    (subst (y Nat.≀_) (Nat.+-zeror x) (Nat.≀-peel p))
... | posv x | posv y = ap (Ξ» e β†’ diff e 0) $
  Nat.≀-antisym
    (subst (Nat._≀ y) (Nat.+-zeror x) p)
    (subst (Nat._≀ x) (Nat.+-zeror y) q)