```1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 ``` ```------------------------------------------------------------------------------ --- Library defining natural numbers in Peano representation and --- some operations on this representation. --- --- @author Michael Hanus --- @version May 2016 --- @category general ------------------------------------------------------------------------------ module Nat ( Nat(..), fromNat, toNat, add, sub, mul, leq ) where import Test.Prop --- Natural numbers defined in Peano representation. data Nat = Z | S Nat --- Transforms a natural number into a standard integer. fromNat :: Nat -> Int fromNat Z = 0 fromNat (S n) = 1 + fromNat n -- Postcondition: the result of `fromNat` is not negative fromNat'post :: Nat -> Int -> Bool fromNat'post _ n = n >= 0 --- Transforms a standard integer into a natural number. toNat :: Int -> Nat toNat n | n == 0 = Z | n > 0 = S (toNat (n-1)) -- Precondition: `toNat` must be called with non-negative numbers toNat'pre :: Int -> Bool toNat'pre n = n >= 0 -- Property: transforming natural numbers into integers and back is the identity fromToNat :: Nat -> Prop fromToNat n = toNat (fromNat n) -=- n toFromNat :: Int -> Prop toFromNat n = n>=0 ==> fromNat (toNat n) -=- n --- Addition on natural numbers. add :: Nat -> Nat -> Nat add Z n = n add (S m) n = S(add m n) -- Property: addition is commutative addIsCommutative :: Nat -> Nat -> Prop addIsCommutative x y = add x y -=- add y x -- Property: addition is associative addIsAssociative :: Nat -> Nat -> Nat -> Prop addIsAssociative x y z = add (add x y) z -=- add x (add y z) --- Subtraction defined by reversing addition. sub :: Nat -> Nat -> Nat sub x y | add y z == x = z where z free -- Properties: subtracting a value which was added yields the same value subAddL :: Nat -> Nat -> Prop subAddL x y = sub (add x y) x -=- y subAddR :: Nat -> Nat -> Prop subAddR x y = sub (add x y) y -=- x --- Multiplication on natural numbers. mul :: Nat -> Nat -> Nat mul Z _ = Z mul (S m) n = add n (mul m n) -- Property: multiplication is commutative mulIsCommutative :: Nat -> Nat -> Prop mulIsCommutative x y = mul x y -=- mul y x -- Property: multiplication is associative mulIsAssociative :: Nat -> Nat -> Nat -> Prop mulIsAssociative x y z = mul (mul x y) z -=- mul x (mul y z) -- Properties: multiplication is distributive over addition distMulAddL :: Nat -> Nat -> Nat -> Prop distMulAddL x y z = mul x (add y z) -=- add (mul x y) (mul x z) distMulAddR :: Nat -> Nat -> Nat -> Prop distMulAddR x y z = mul (add y z) x -=- add (mul y x) (mul z x) -- less-or-equal predicated on natural numbers: leq :: Nat -> Nat -> Bool leq Z _ = True leq (S _) Z = False leq (S x) (S y) = leq x y -- Property: adding a number yields always a greater-or-equal number leqAdd :: Nat -> Nat -> Prop leqAdd x y = always \$ leq x (add x y) ```