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
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132

------------------------------------------------------------------------------
-- | Author : Michael Hanus
--   Version: December 2021
--
-- Library defining natural numbers in Peano representation and
-- some operations on this representation.
------------------------------------------------------------------------------

module Data.Nat (
 -- * Data type for natural numbers
 Nat(..),
 -- * Conversion operations
 fromNat, toNat,
 -- * Arithmetic operations
 add, sub, mul,
 -- * Comparison predicates
 leq
 ) where

import Test.Prop

-- | Natural numbers are defined in Peano representation.
data Nat = Z     -- ^ The zero constructor
         | S Nat -- ^ The successor constructor
 deriving Eq

-- We show natural numbers as traditional integers.
instance Show Nat where
  show n = show (fromNat n)

-- We read natural numbers as traditional integers.
instance Read Nat where
  readsPrec p s = map (\ (n,r) -> (toNat n, r)) (readsPrec p s)

-- | 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)

-- | The less-or-equal predicate 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)

------------------------------------------------------------------------------

-- Peano numbers as a `Num` instance. Since we do not represent
-- negative numbers, computing with negative number simply fails.
instance Num Nat where
  x + y = add x y
  x - y = sub x y
  x * y = mul x y

  negate x = sub Z x

  abs x = x -- trivial since there are no negative numbers

  signum Z = Z
  signum (S _) = S Z

  fromInt x = toNat x

------------------------------------------------------------------------------