{-# language DataKinds #-}
{-# language TypeOperators #-}
{-# language KindSignatures #-}
{-# language ExplicitForAll #-}
{-# language AllowAmbiguousTypes #-}

module Arithmetic.Plus
  ( zeroL
  , zeroR
  , commutative
  , associative
  ) where

import Arithmetic.Unsafe (type (:=:)(Eq))
import GHC.TypeNats (type (+))

-- | Any number plus zero is equal to the original number.
zeroR :: m :=: (m + 0)
zeroR :: forall (m :: Nat). m :=: (m + 0)
zeroR = forall (a :: Nat) (b :: Nat). a :=: b
Eq

-- | Zero plus any number is equal to the original number.
zeroL :: m :=: (0 + m)
zeroL :: forall (m :: Nat). m :=: (0 + m)
zeroL = forall (a :: Nat) (b :: Nat). a :=: b
Eq

-- | Addition is commutative.
commutative :: forall a b. a + b :=: b + a
commutative :: forall (a :: Nat) (b :: Nat). (a + b) :=: (b + a)
commutative = forall (a :: Nat) (b :: Nat). a :=: b
Eq

-- | Addition is associative.
associative :: forall a b c. (a + b) + c :=: a + (b + c)
associative :: forall (a :: Nat) (b :: Nat) (c :: Nat).
((a + b) + c) :=: (a + (b + c))
associative = forall (a :: Nat) (b :: Nat). a :=: b
Eq