Natural numbers - simple formal proofs in Agda & Haskell

Naturals.agda

module Naturals where

-- based on https://plfa.github.io/

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym; trans)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}

_+_ : ℕ → ℕ → ℕ
zero    + n = n
(suc m) + n = suc (m + n)

-- zero is right identity
--
+-identity : ∀ (m : ℕ) → m + zero ≡ m
+-identity zero    = refl
+-identity (suc m) = cong suc (+-identity m)

+-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc zero    n = refl
+-suc (suc m) n = cong suc (+-suc m n)
    
-- Addition of Peano natural numbers is commutative
--
+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm zero    n = sym (+-identity n)
-- +-comm (suc m) n = trans (cong suc (+-comm m n)) (sym (+-suc n m))
+-comm (suc m) n =
  begin
    suc m + n
  ≡⟨⟩
    suc (m + n)
  ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m)
  ≡⟨ sym (+-suc n m) ⟩
    n + suc m
  ∎

-- Associativity of addition
--
+-assoc : ∀ (m n o : ℕ) -> m + (n + o) ≡ (m + n) + o
+-assoc zero    n o = refl
-- +-assoc (suc m) n o = cong suc (+-assoc m n o)
+-assoc (suc m) n o =
  begin
    suc m + (n + o)
  ≡⟨⟩
    suc (m + (n + o))
  ≡⟨ cong suc (+-assoc m n o) ⟩
    suc ((m + n) + o)
  ≡⟨⟩
    suc (m + n) + o
  ≡⟨⟩
    (suc m + n) + o
  ∎

Naturals.hs

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE ConstraintKinds     #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE PolyKinds           #-}
{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Naturals where

import           Prelude hiding (Eq)
import           Data.Proxy (Proxy (..))
import           Data.Kind (Type, Constraint)

data Dict :: Constraint -> Type where
     Dict :: a => Dict a

data N where
     Z :: N
     S :: N -> N

type family Add (n :: N) (m :: N) :: N where
  Add 'Z m     = m
  Add ('S n) m = 'S (Add n m)

-- We need the singletons, since we cannot pattern match on types in Haskell.
data SNat (n :: N) where
     SZero :: SNat 'Z
     SSuc  :: SNat n -> SNat ('S n)


-- | kind homogenous equalitiy
--
data Eq (a :: k) (b :: k) where
     Refl :: Eq a a

eq :: Dict (a ~ b) -> Eq a b
eq Dict = Refl

eqInv :: Eq a b -> Dict (a ~ b)
eqInv Refl = Dict

cong :: Proxy f -> Eq a b -> Eq (f a) (f b)
cong _ Refl = Refl

sym :: Eq (a :: k) (b :: k) -> Eq b a
sym Refl = Refl

trans :: Eq a b -> Eq b c -> Eq a c
trans Refl Refl = Refl

type IdentityLaw (m :: N) = Eq (Add m 'Z) m

identityLaw :: SNat m -> IdentityLaw (m :: N)
identityLaw SZero    = Refl
identityLaw (SSuc m) = cong (Proxy :: Proxy 'S) (identityLaw m)


type SucLaw (m :: N) (n :: N) = Eq (Add m ('S n)) ('S (Add m n))

sucLaw :: forall (n :: N) (m :: N). SNat m -> SNat n -> SucLaw m n
sucLaw SZero    _n = Refl
sucLaw (SSuc m) n  = cong (Proxy :: Proxy 'S) (sucLaw m n)


type CommLaw (m :: N) (n :: N) = Eq (Add m n) (Add n m)

commLaw :: forall (n :: N) (m :: N).
           SNat m
        -> SNat n
        -> CommLaw m n
commLaw SZero    n = sym (identityLaw n)
commLaw (SSuc m) n = trans (cong (Proxy :: Proxy 'S) (commLaw m n))
                           (sym (sucLaw n m))


type AssocLaw (m :: N) (n :: N) (o :: N) = Eq (Add (Add m n) o) (Add m (Add n o))

assocLaw :: forall (n :: N) (m :: N) (o :: N).
            SNat m
         -> SNat n
         -> SNat o
         -> AssocLaw m n o
assocLaw SZero    _n _o = Refl
assocLaw (SSuc m) n  o  = cong (Proxy :: Proxy 'S) (assocLaw m n o)