{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
-- | Some proofs on type-level Peano numbers.
module TypeLevel.Nat.Proofs where
import TypeLevel.Nat
import Data.Type.Equality
import Unsafe.Coerce
-- | Addition is associative.
plusAssoc :: The Nat x -> p y -> q z -> ((x + y) + z) :~: (x + (y + z))
plusAssoc Zy _ _ = Refl
plusAssoc (Sy x) y z = case plusAssoc x y z of
Refl -> Refl
{-# NOINLINE plusAssoc #-}
-- | Zero is the identity of addition.
plusZeroNeutral :: The Nat n -> n + Z :~: n
plusZeroNeutral Zy = Refl
plusZeroNeutral (Sy n) = case plusZeroNeutral n of
Refl -> Refl
{-# NOINLINE plusZeroNeutral #-}
-- | Successor distributes over addition
plusSuccDistrib :: The Nat n -> proxy m -> n + S m :~: S (n + m)
plusSuccDistrib Zy _ = Refl
plusSuccDistrib (Sy n) p = gcastWith (plusSuccDistrib n p) Refl
{-# NOINLINE plusSuccDistrib #-}
{-# RULES
"plusAssoc" forall x y z. plusAssoc x y z = unsafeCoerce (Refl :: 'Z :~: 'Z)
"plusZeroNeutral" forall x. plusZeroNeutral x = unsafeCoerce (Refl :: 'Z :~: 'Z)
"plusSuccDistrib" forall x y. plusSuccDistrib x y = unsafeCoerce (Refl :: 'Z :~: 'Z)
#-}