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