Peano's Axioms in Haskell

peano-nats.hs

-- A straightforward implementation of Peano's Axioms for the Natural Numbers in Haskell.
-- This is intended as a demonstration of similarity between functional code and its equivalent in (informal) first order logic 

import Prelude hiding ( (+), (*) )

-- There exists a set Nat with the distinguished element Zero and the function Suc, such that if n is in Nat, then Suc(n) is in Nat
data Nat = Zero | Suc Nat deriving (Eq, Show)

-- There exists a binary function + on (Nat x Nat) such that
-- Zero + n = n + Zero = n
-- and 
-- n + Suc(m) = Suc(n) + m
(+) :: Nat -> Nat -> Nat
(+) Zero n = n
(+) n Zero = n
(+) n (Suc m) = (Suc n) + m

-- There exists a binary function * on (Nat x Nat) such that
-- Zero * n = n * Zero = Zero
-- and 
-- n * Suc (m) = n + n * m
(*) :: Nat -> Nat -> Nat
(*) Zero _ = Zero
(*) _ Zero = Zero
(*) n (Suc m) = n + n * m