------------------------------------------------------------------------
-- Integers
------------------------------------------------------------------------

module Data.Integer where

open import Data.Nat as 
  using () renaming (_+_ to _ℕ+_; _*_ to _ℕ*_)
import Data.Nat.Show as 
open import Data.Sign as Sign using (Sign) renaming (_*_ to _S*_)
open import Data.Product as Prod
open import Data.String using (String; _++_)
open import Function
open import Data.Sum as Sum
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; refl; sym; cong; cong₂)
open PropEq.≡-Reasoning

infix  8 +_ -_
infixl 7 _*_ _⊓_
infixl 6 _+_ _-_ _⊖_ _⊔_
infix  4 _≤_ _≤?_

------------------------------------------------------------------------
-- The types

-- Integers.

data  : Set where
  -[1+_] : (n : )    -- -[1+ n ] stands for - (1 + n).
  +_     : (n : )    -- + n stands for n.

------------------------------------------------------------------------
-- Conversions

-- Absolute value.

∣_∣ :   
 + n       = n
 -[1+ n ]  = .suc n

-- Gives the sign. For zero the sign is arbitrarily chosen to be +.

sign :   Sign
sign (+ _)    = Sign.+
sign -[1+ _ ] = Sign.-

-- Decimal string representation.

show :   String
show i = showSign (sign i) ++ .show  i 
  where
  showSign : Sign  String
  showSign Sign.- = "-"
  showSign Sign.+ = ""

------------------------------------------------------------------------
-- A view of integers as sign + absolute value

infix 5 _◂_ _◃_

_◃_ : Sign    
_       .zero  = + .zero
Sign.+  n       = + n
Sign.-  .suc n = -[1+ n ]

◃-left-inverse :  i  sign i   i   i
◃-left-inverse -[1+ n ]    = refl
◃-left-inverse (+ .zero)  = refl
◃-left-inverse (+ .suc n) = refl

◃-cong :  {i j}  sign i  sign j   i    j   i  j
◃-cong {i} {j} sign-≡ abs-≡ = begin
  i               ≡⟨ sym $ ◃-left-inverse i 
  sign i   i   ≡⟨ cong₂ _◃_ sign-≡ abs-≡ 
  sign j   j   ≡⟨ ◃-left-inverse j 
  j               

data SignAbs :   Set where
  _◂_ : (s : Sign) (n : )  SignAbs (s  n)

signAbs :  i  SignAbs i
signAbs i = PropEq.subst SignAbs (◃-left-inverse i) $
              sign i   i 

------------------------------------------------------------------------
-- Equality is decidable

_≟_ : Decidable {A = } _≡_
i  j with Sign._≟_ (sign i) (sign j) | ._≟_  i   j 
i  j | yes sign-≡ | yes abs-≡ = yes (◃-cong sign-≡ abs-≡)
i  j | no  sign-≢ | _         = no (sign-≢  cong sign)
i  j | _          | no abs-≢  = no (abs-≢   cong ∣_∣)

decSetoid : DecSetoid _ _
decSetoid = PropEq.decSetoid _≟_

------------------------------------------------------------------------
-- Arithmetic

-- Negation.

-_ :   
- (+ .suc n) = -[1+ n ]
- (+ .zero)  = + .zero
- -[1+ n ]    = + .suc n

-- Subtraction of natural numbers.

_⊖_ :     
m        .zero  = + m
.zero   .suc n = -[1+ n ]
.suc m  .suc n = m  n

-- Addition.

_+_ :     
-[1+ m ] + -[1+ n ] = -[1+ .suc (m ℕ+ n) ]
-[1+ m ] + +    n   = n  .suc m
+    m   + -[1+ n ] = m  .suc n
+    m   + +    n   = + (m ℕ+ n)

-- Subtraction.

_-_ :     
-[1+ m ] - -[1+ n ] = n  m
-[1+ m ] - +    n   = -[1+ n ℕ+ m ]
+    m   - -[1+ n ] = + (.suc n ℕ+ m)
+    m   - +    n   = m  n

private

  -- Note that the definition i - j = - j + i evaluates differently
  -- from the definition above. For instance, the following property
  -- would require a nontrivial proof with the alternative definition:

  +-+ :  m n  + m - + n  m  n
  +-+ m n = refl

  -- The proof is still easy, though.

  -++ :  m n  - + n + + m  m  n
  -++ m .zero    = refl
  -++ m (.suc n) = refl

-- Successor.

suc :   
suc i = + 1 + i

private

  suc-is-lazy⁺ :  n  suc (+ n)  + .suc n
  suc-is-lazy⁺ n = refl

  suc-is-lazy⁻ :  n  suc -[1+ .suc n ]  -[1+ n ]
  suc-is-lazy⁻ n = refl

-- Predecessor.

pred :   
pred i = i - + 1

private

  pred-is-lazy⁺ :  n  pred (+ .suc n)  + n
  pred-is-lazy⁺ n = refl

  pred-is-lazy⁻ :  n  pred -[1+ n ]  -[1+ .suc n ]
  pred-is-lazy⁻ n = refl

-- Multiplication.

_*_ :     
i * j = sign i S* sign j   i  ℕ*  j 

-- Maximum.

_⊔_ :     
-[1+ m ]  -[1+ n ] = -[1+ ._⊓_ m n ]
-[1+ m ]  +    n   = + n
+    m    -[1+ n ] = + m
+    m    +    n   = + (._⊔_ m n)

-- Minimum.

_⊓_ :     
-[1+ m ]  -[1+ n ] = -[1+ ._⊔_ m n ]
-[1+ m ]  +    n   = -[1+ m ]
+    m    -[1+ n ] = -[1+ n ]
+    m    +    n   = + (._⊓_ m n)

------------------------------------------------------------------------
-- Ordering

data _≤_ :     Set where
  -≤+ :  {m n}  -[1+ m ]  + n
  -≤- :  {m n}  (n≤m : ._≤_ n m)  -[1+ m ]  -[1+ n ]
  +≤+ :  {m n}  (m≤n : ._≤_ m n)  + m  + n

drop‿+≤+ :  {m n}  + m  + n  ._≤_ m n
drop‿+≤+ (+≤+ m≤n) = m≤n

drop‿-≤- :  {m n}  -[1+ m ]  -[1+ n ]  ._≤_ n m
drop‿-≤- (-≤- n≤m) = n≤m

_≤?_ : Decidable _≤_
-[1+ m ] ≤? -[1+ n ] = Dec.map′ -≤- drop‿-≤- (._≤?_ n m)
-[1+ m ] ≤? +    n   = yes -≤+
+    m   ≤? -[1+ n ] = no λ ()
+    m   ≤? +    n   = Dec.map′ +≤+ drop‿+≤+ (._≤?_ m n)

decTotalOrder : DecTotalOrder _ _ _
decTotalOrder = record
  { Carrier         = 
  ; _≈_             = _≡_
  ; _≤_             = _≤_
  ; isDecTotalOrder = record
      { isTotalOrder = record
          { isPartialOrder = record
              { isPreorder = record
                  { isEquivalence = PropEq.isEquivalence
                  ; reflexive     = refl′
                  ; trans         = trans
                  }
                ; antisym  = antisym
              }
          ; total          = total
          }
      ; _≟_          = _≟_
      ; _≤?_         = _≤?_
      }
  }
  where
  module ℕO = DecTotalOrder .decTotalOrder

  refl′ : _≡_  _≤_
  refl′ { -[1+ n ]} refl = -≤- ℕO.refl
  refl′ {+ n}       refl = +≤+ ℕO.refl

  trans : Transitive _≤_
  trans -≤+       (+≤+ n≤m) = -≤+
  trans (-≤- n≤m) -≤+       = -≤+
  trans (-≤- n≤m) (-≤- k≤n) = -≤- (ℕO.trans k≤n n≤m)
  trans (+≤+ m≤n) (+≤+ n≤k) = +≤+ (ℕO.trans m≤n n≤k)

  antisym : Antisymmetric _≡_ _≤_
  antisym -≤+       ()
  antisym (-≤- n≤m) (-≤- m≤n) = cong -[1+_] $ ℕO.antisym m≤n n≤m
  antisym (+≤+ m≤n) (+≤+ n≤m) = cong +_     $ ℕO.antisym m≤n n≤m

  total : Total _≤_
  total (-[1+ m ]) (-[1+ n ]) = [ inj₂ ∘′ -≤- , inj₁ ∘′ -≤- ]′ $ ℕO.total m n
  total (-[1+ m ]) (+    n  ) = inj₁ -≤+
  total (+    m  ) (-[1+ n ]) = inj₂ -≤+
  total (+    m  ) (+    n  ) = [ inj₁ ∘′ +≤+ , inj₂ ∘′ +≤+ ]′ $ ℕO.total m n

poset : Poset _ _ _
poset = DecTotalOrder.poset decTotalOrder

import Relation.Binary.PartialOrderReasoning as POR
module ≤-Reasoning = POR poset
  renaming (_≈⟨_⟩_ to _≡⟨_⟩_)