Nat.hs

module Nat where

data Nat = O | S Nat deriving (Eq,Show)

instance Ord Nat where compare = cmpNat

cmpNat O O = EQ
cmpNat (S a) (S b) = cmpNat a b
cmpNat O (S b) = LT
cmpNat (S a) O = GT

instance Num Nat where
  O   + b = b
  S a + b = S (a + b)

len [] = O
len (_:xs) = S (len xs)

index [] _ = error "index [] _"
index (x:xs) O = x
index (x:xs) (S n) = index xs n

{-P:
assert NatEq = All a . All b . True {a `eqNat` b} <==> a===b {-#cert:NatEq#-}
assert CongSucc = All a . All b . a===b ==> {S a}==={S b}   {-#cert:CongSucc#-}
assert EqNatRefl = All a . True {a `eqNat` a}               {-#cert:EqNatRefl#-}
assert NotLtZero = All a . False {a `ltNat` O}              {-#cert:NotLtZero#-}
assert AddSucc = All a . All b . {S a + b}==={a + S b}      {-#cert:AddSucc#-}
assert AddZero = All a . a==={a + O}                        {-#cert:AddZero#-}
assert Peano4    = All a . -/ {S a}==={O}                   {-#cert:Peano4#-}
assert Peano4b   = All a . All b . -/ {S a + b}===b         {-#cert:Peano4b#-}

assert LeNatRefl = All a . True {a `leNat` a}		    {-#cert:LeNatRefl#-}
assert LtNatSucc = All a . All b . True {a `ltNat` S b + a} {-#cert:LtNatSucc#-}
assert LeNatSucc = All a . All b . True {a `leNat` S b + a} {-#cert:LeNatSucc#-}
assert LtNatPlus =					    {-#cert:LtNatPlus#-}
  All a . All b . All c .
  True {a `ltNat` b} ==> True {a + c `ltNat` b + c}
-}

infixl 6 `plus`
plus :: Nat->Nat->Nat
plus = (+)

infix 4 `ltNat`, `leNat`, `eqNat`

eqNat :: Nat->Nat->Bool
eqNat = (==)

ltNat a b = oLt (cmpNat a b)
leNat a b = oLe (cmpNat a b)


oLt LT = True
oLt _ = False
oLe GT = False
oLe _ = True