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)))