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)
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 (+ 0) _+_
identityˡ -[1+ _ ] = refl
identityˡ (+ _ ) = refl
identityʳ : RightIdentity (+ 0) _+_
identityʳ x rewrite comm x (+ 0) = 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 1 c)
| +-comm a 1
= refl
assoc (+ suc a) (+ suc b) -[1+ c ]
rewrite distribʳ-⊖-+-pos (suc a) b c
| sym (+-assoc a 1 b)
| +-comm a 1
= refl
assoc -[1+ a ] -[1+ b ] -[1+ c ]
rewrite sym (+-assoc a 1 (b ℕ+ c))
| +-comm a 1
| +-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 _≡_ _+_ (+ 0)
isCommutativeMonoid = record
{ isSemigroup = isSemigroup
; identityˡ = identityˡ
; comm = comm
}
commutativeMonoid : CommutativeMonoid _ _
commutativeMonoid = record
{ Carrier = ℤ
; _≈_ = _≡_
; _∙_ = _+_
; ε = + 0
; isCommutativeMonoid = isCommutativeMonoid
}