------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to addition of integers
------------------------------------------------------------------------

module Data.Integer.Addition.Properties where

open import Algebra
import Algebra.FunctionProperties
open import Algebra.Structures
open import Data.Integer hiding (suc)
open import Data.Nat using (suc; zero) renaming (_+_ to _ℕ+_)
import Data.Nat.Properties as ℕ
open import Relation.Binary.PropositionalEquality

open Algebra.FunctionProperties (_≡_ {A = ℤ})
open CommutativeSemiring ℕ.commutativeSemiring
  using (+-comm; +-assoc; +-identity)

------------------------------------------------------------------------
-- Addition and zero form a commutative monoid

private

  comm : Commutative _+_
  comm -[1+ a ] -[1+ b ] rewrite +-comm a b = refl
  comm (+   a ) (+   b ) rewrite +-comm a b = refl
  comm -[1+ _ ] (+   _ ) = refl
  comm (+   _ ) -[1+ _ ] = refl

  identityˡ : LeftIdentity (+ ) _+_
  identityˡ -[1+ _ ] = refl
  identityˡ (+   _ ) = refl

  identityʳ : RightIdentity (+ ) _+_
  identityʳ x rewrite comm x (+ ) = identityˡ x

  distribˡ-⊖-+-neg : ∀ a b c → b ⊖ c + -[1+ a ] ≡ b ⊖ (suc c ℕ+ a)
  distribˡ-⊖-+-neg _ zero    zero    = refl
  distribˡ-⊖-+-neg _ zero    (suc _) = refl
  distribˡ-⊖-+-neg _ (suc _) zero    = refl
  distribˡ-⊖-+-neg a (suc b) (suc c) = distribˡ-⊖-+-neg a b c

  distribʳ-⊖-+-neg : ∀ a b c → -[1+ a ] + (b ⊖ c) ≡ b ⊖ (suc a ℕ+ c)
  distribʳ-⊖-+-neg a b c
    rewrite comm -[1+ a ] (b ⊖ c)
          | distribˡ-⊖-+-neg a b c
          | +-comm a c
          = refl

  distribˡ-⊖-+-pos : ∀ a b c → b ⊖ c + + a ≡ b ℕ+ a ⊖ c
  distribˡ-⊖-+-pos _ zero    zero    = refl
  distribˡ-⊖-+-pos _ zero    (suc _) = refl
  distribˡ-⊖-+-pos _ (suc _) zero    = refl
  distribˡ-⊖-+-pos a (suc b) (suc c) = distribˡ-⊖-+-pos a b c

  distribʳ-⊖-+-pos : ∀ a b c → + a + (b ⊖ c) ≡ a ℕ+ b ⊖ c
  distribʳ-⊖-+-pos a b c
    rewrite comm (+ a) (b ⊖ c)
          | distribˡ-⊖-+-pos a b c
          | +-comm a b
          = refl

  assoc : Associative _+_
  assoc (+ zero) y z rewrite identityˡ      y  | identityˡ (y + z) = refl
  assoc x (+ zero) z rewrite identityʳ  x      | identityˡ      z  = refl
  assoc x y (+ zero) rewrite identityʳ (x + y) | identityʳ  y      = refl
  assoc -[1+ a ]  -[1+ b ]  (+ suc c) = sym (distribʳ-⊖-+-neg a c b)
  assoc -[1+ a ]  (+ suc b) (+ suc c) = distribˡ-⊖-+-pos (suc c) b a
  assoc (+ suc a) -[1+ b ]  -[1+ c ]  = distribˡ-⊖-+-neg c a b
  assoc (+ suc a) -[1+ b ] (+ suc c)
    rewrite distribˡ-⊖-+-pos (suc c) a b
          | distribʳ-⊖-+-pos (suc a) c b
          | sym (+-assoc a  c)
          | +-comm a 
          = refl
  assoc (+ suc a) (+ suc b) -[1+ c ]
    rewrite distribʳ-⊖-+-pos (suc a) b c
          | sym (+-assoc a  b)
          | +-comm a 
          = refl
  assoc -[1+ a ] -[1+ b ] -[1+ c ]
    rewrite sym (+-assoc a  (b ℕ+ c))
          | +-comm a 
          | +-assoc a b c
          = refl
  assoc -[1+ a ] (+ suc b) -[1+ c ]
    rewrite distribʳ-⊖-+-neg a b c
          | distribˡ-⊖-+-neg c b a
          = refl
  assoc (+ suc a) (+ suc b) (+ suc c)
    rewrite +-assoc (suc a) (suc b) (suc c)
          = refl

  isSemigroup : IsSemigroup _≡_ _+_
  isSemigroup = record
    { isEquivalence = isEquivalence
    ; assoc         = assoc
    ; ∙-cong        = cong₂ _+_
    }

  isCommutativeMonoid : IsCommutativeMonoid _≡_ _+_ (+ )
  isCommutativeMonoid = record
    { isSemigroup = isSemigroup
    ; identityˡ   = identityˡ
    ; comm        = comm
    }

commutativeMonoid : CommutativeMonoid _ _
commutativeMonoid = record
  { Carrier             = ℤ
  ; _≈_                 = _≡_
  ; _∙_                 = _+_
  ; ε                   = + 
  ; isCommutativeMonoid = isCommutativeMonoid
  }