module Signs where

open import Preliminaries
open import IntegerAlgebra
open import Doubling
open import Booleans
open import Subtraction

shift-equiv : ℤ + (ℤ + ℤ) ≅ ℤ + (ℤ + ℤ)
shift-equiv = inv-iso +-assoc ∘ₑ +-congr halve-iso (inv-iso halve-iso)

shift-alg : IntAlg (ℤ + (ℤ + ℤ))
shift-alg .IntAlg.S = shift-equiv
shift-alg .IntAlg.Z = inr (inl ℤ.Z)

abstract
  presign : ℤ → ℤ + (ℤ + ℤ)
  presign = ℤ-rec shift-alg

  presign-Z : presign ℤ.Z ≡ inr (inl ℤ.Z)
  presign-Z = ℤ-rec-Z shift-alg

  presign-S : {x : ℤ} → presign (ℤ.S .fun x) ≡ shift-equiv .fun (presign x)
  presign-S = ℤ-rec-S shift-alg _

  presign-inv : {x : ℤ} → presign (ℤ.S .inv x) ≡ shift-equiv .inv (presign x)
  presign-inv = ℤ-rec-inv shift-alg _

right-shift : {x : ℤ + (ℤ + ℤ)} → right x → right (shift-equiv .fun x)
right-shift {inl _} = left-right-disj left-intro
right-shift {inr _} _ = right-intro

left-inv : {x : ℤ + (ℤ + ℤ)} → left x → left (shift-equiv .inv x)
left-inv {inl _} _ = left-intro
left-inv {inr _} t = left-right-disj t right-intro

neg zero pos nonneg : ℤ → Set
neg x = left (presign x)
nonneg x = right (presign x)
zero x = Σ (nonneg x) (λ _ → neg (ℤ.S .inv x))
pos x = nonneg (ℤ.S .inv x)

abstract
  zeroIsZero : zero ℤ.Z
  zeroIsZero .fst = transport right right-intro $ symm presign-Z
  zeroIsZero .snd = transport left left-intro $ symm $ presign-inv • ap (shift-equiv .inv) presign-Z

  nonneg-succ : {x : ℤ} → nonneg x → nonneg (ℤ.S .fun x)
  nonneg-succ {x} h = transport right (right-shift {presign x} h) (symm presign-S)

  nonneg-of-pos : {x : ℤ} → pos x → nonneg x
  nonneg-of-pos h = transport nonneg (nonneg-succ h) (ℤ.S .fun-inv _)

  neg-inv : {x : ℤ} → neg x → neg (ℤ.S .inv x)
  neg-inv {x} h = transport left (left-inv h) (symm presign-inv)

  _<_ : ℤ → ℤ → Set
  x < y = neg (x - y)

  lt-succ-of-lt : {x y : ℤ} → x < y → x < ℤ.S .fun y
  lt-succ-of-lt h = transport neg (neg-inv h) (symm sub-S)

  lt-of-succ-lt-succ : {x y : ℤ} → ℤ.S .fun x < ℤ.S .fun y → x < y
  lt-of-succ-lt-succ h = transport neg h S-sub-S

  lt-succ-self : {x : ℤ} → x < ℤ.S .fun x
  lt-succ-self = transport neg (zeroIsZero .snd) (symm (sub-S • ap (ℤ.S .inv) sub-self))

  lt-zero-nonneg-disj : {x : ℤ} → x < ℤ.Z → nonneg x → ⊥
  lt-zero-nonneg-disj {x} p h = left-right-disj (transport neg p sub-Z) h

  lt-prop : {x y : ℤ} → isProp (x < y)
  lt-prop = left-prop

  zero+pos-iso-nonneg : {x : ℤ} → zero x + pos x ≅ nonneg x
  zero+pos-iso-nonneg = Σ-contr (λ _ → left-or-right _) ∘ₑ +-distrib ∘ₑ +-congr id-iso
                        (×-symm ∘ₑ inv-iso (Σ-contr λ xpos → contr-of-prop right-prop (nonneg-of-pos xpos)))