proved_nat.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE NoStarIsType #-}

import Data.Type.Equality ((:~:) (..))
import qualified GHC.TypeLits as GHC (Nat, type (+), type (-))

-- Equality

type (==) = (:~:)

infix 4 ==

type Reverse :: a == b -> b == a
type family Reverse p where
  Reverse Refl = Refl

type (>>) :: a == b -> b == c -> a == c
type family a >> b where
  Refl >> Refl = Refl

infixr 9 >>

type (<<) :: b == a -> b == c -> a == c
type a << b = Reverse a >> b

infixr 9 <<

type Cong :: forall a b f. a == b -> f a == f b
type family Cong p where
  Cong Refl = Refl

type (@@) :: forall a b. forall f -> a == b -> f a == f b
type f @@ (p :: a == b) = Cong @a @b @f p

infixr 0 @@

-- Nat

data Nat where
  Zero :: Nat
  Succ :: Nat -> Nat

type FromNat :: GHC.Nat -> Nat
type family FromNat n where
  FromNat 0 = Zero
  FromNat n = Succ (FromNat (n GHC.- 1))

type ToNat :: Nat -> GHC.Nat
type family ToNat n where
  ToNat Zero = 0
  ToNat (Succ x) = ToNat x GHC.+ 1

type (+) :: Nat -> Nat -> Nat
type family a + b where
  Zero + b = b
  Succ a + b = Succ (a + b)

infixl 6 +

type (*) :: Nat -> Nat -> Nat
type family a * b where
  Zero * _ = Zero
  Succ a * b = b + (a * b)

infixl 7 *

-- Nat properties

type Plus_Zero_Right :: forall a -> a + Zero == a
type family Plus_Zero_Right a where
  Plus_Zero_Right Zero = Refl
  Plus_Zero_Right (Succ n) = Succ @@ Plus_Zero_Right n

type Plus_Shift_Right :: forall a b -> Succ a + b == a + Succ b
type family Plus_Shift_Right a b where
  Plus_Shift_Right Zero _ = Refl
  Plus_Shift_Right (Succ a) b = Succ @@ Plus_Shift_Right a b

type Plus_Left :: forall a b. forall c -> a == b -> c + a == c + b
type family Plus_Left c p where
  Plus_Left _ Refl = Refl

type Plus_Right :: forall a b. forall c -> a == b -> a + c == b + c
type family Plus_Right c p where
  Plus_Right _ Refl = Refl

type Plus_Assoc :: forall a b c -> (a + b) + c == a + (b + c)
type family Plus_Assoc a b c where
  Plus_Assoc Zero _ _ = Refl
  Plus_Assoc (Succ a) b c = Succ @@ Plus_Assoc a b c

type Plus_Commute :: forall a b -> a + b == b + a
type family Plus_Commute a b where
  Plus_Commute Zero b = Reverse (Plus_Zero_Right b)
  Plus_Commute (Succ a) b = (Succ @@ Plus_Commute a b) >> Plus_Shift_Right b a

type Mult_Zero_Right :: forall a -> a * Zero == Zero
type family Mult_Zero_Right a where
  Mult_Zero_Right Zero = Refl
  Mult_Zero_Right (Succ a) = Mult_Zero_Right a

type Plus_Mult :: forall a b -> a + a * b == a * Succ b
type family Plus_Mult a b where
  Plus_Mult Zero _ = Refl
  Plus_Mult (Succ a) b = Succ @@ Plus_Assoc a b (a * b) << Plus_Right (a * b) (Plus_Commute a b) >> Plus_Assoc b a (a * b) >> Plus_Left b (Plus_Mult a b)

type Mult_Commute :: forall a b -> a * b == b * a
type family Mult_Commute a b where
  Mult_Commute Zero b = Reverse (Mult_Zero_Right b)
  Mult_Commute (Succ a) b = Plus_Left b (Mult_Commute a b) >> Plus_Mult b a