------------------------------------------------------------------------
-- Some properties about integers
------------------------------------------------------------------------

module Data.Integer.Properties where

open import Algebra
import Algebra.Morphism as Morphism
open import Data.Empty
open import Function
open import Data.Integer hiding (suc)
open import Data.Nat as  renaming (_*_ to _ℕ*_)
import Data.Nat.Properties as 
open import Data.Sign as Sign using () renaming (_*_ to _S*_)
import Data.Sign.Properties as SignProp
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

open Morphism.Definitions   _≡_

-- Some properties relating sign and ∣_∣ to _◃_.

sign-◃ :  s n  sign (s  suc n)  s
sign-◃ Sign.- _ = refl
sign-◃ Sign.+ _ = refl

sign-cong :  {s₁ s₂ n₁ n₂} 
            s₁  suc n₁  s₂  suc n₂  s₁  s₂
sign-cong {s₁} {s₂} {n₁} {n₂} eq = begin
  s₁                  ≡⟨ sym $ sign-◃ s₁ n₁ 
  sign (s₁  suc n₁)  ≡⟨ cong sign eq 
  sign (s₂  suc n₂)  ≡⟨ sign-◃ s₂ n₂ 
  s₂                  

abs-◃ :  s n   s  n   n
abs-◃ _      zero    = refl
abs-◃ Sign.- (suc n) = refl
abs-◃ Sign.+ (suc n) = refl

abs-cong :  {s₁ s₂ n₁ n₂} 
           s₁  n₁  s₂  n₂  n₁  n₂
abs-cong {s₁} {s₂} {n₁} {n₂} eq = begin
  n₁           ≡⟨ sym $ abs-◃ s₁ n₁ 
   s₁  n₁   ≡⟨ cong ∣_∣ eq 
   s₂  n₂   ≡⟨ abs-◃ s₂ n₂ 
  n₂           

-- ∣_∣ commutes with multiplication.

abs-*-commute : Homomorphic₂ ∣_∣ _*_ _ℕ*_
abs-*-commute i j = abs-◃ _ _

-- Multiplication is right cancellative for non-zero integers.

cancel-*-right :  i j k 
                 k  + 0  i * k  j * k  i  j
cancel-*-right i j k            ≢0 eq with signAbs k
cancel-*-right i j .(+ 0)       ≢0 eq | s  zero  = ⊥-elim (≢0 refl)
cancel-*-right i j .(s  suc n) ≢0 eq | s  suc n
  with  s  suc n  | abs-◃ s (suc n) | sign (s  suc n) | sign-◃ s n
...  | .(suc n)      | refl            | .s               | refl =
  ◃-cong (sign-i≡sign-j i j eq) $
         .cancel-*-right  i   j  $ abs-cong eq
  where
  sign-i≡sign-j :  i j 
                  sign i S* s   i  ℕ* suc n 
                  sign j S* s   j  ℕ* suc n 
                  sign i  sign j
  sign-i≡sign-j i              j              eq with signAbs i | signAbs j
  sign-i≡sign-j .(+ 0)         .(+ 0)         eq | s₁  zero   | s₂  zero   = refl
  sign-i≡sign-j .(+ 0)         .(s₂  suc n₂) eq | s₁  zero   | s₂  suc n₂
    with  s₂  suc n₂  | abs-◃ s₂ (suc n₂)
  ... | .(suc n₂) | refl
    with abs-cong {s₁} {sign (s₂  suc n₂) S* s} {0} {suc n₂ ℕ* suc n} eq
  ...   | ()
  sign-i≡sign-j .(s₁  suc n₁) .(+ 0)         eq | s₁  suc n₁ | s₂  zero
    with  s₁  suc n₁  | abs-◃ s₁ (suc n₁)
  ... | .(suc n₁) | refl
    with abs-cong {sign (s₁  suc n₁) S* s} {s₁} {suc n₁ ℕ* suc n} {0} eq
  ...   | ()
  sign-i≡sign-j .(s₁  suc n₁) .(s₂  suc n₂) eq | s₁  suc n₁ | s₂  suc n₂
    with  s₁  suc n₁  | abs-◃ s₁ (suc n₁)
       | sign (s₁  suc n₁) | sign-◃ s₁ n₁
       |  s₂  suc n₂  | abs-◃ s₂ (suc n₂)
       | sign (s₂  suc n₂) | sign-◃ s₂ n₂
  ... | .(suc n₁) | refl | .s₁ | refl | .(suc n₂) | refl | .s₂ | refl =
    SignProp.cancel-*-right s₁ s₂ (sign-cong eq)