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

------------------------------------------------------------------------------
--- Library defining natural numbers in Peano representation and
--- some operations on this representation.
---
--- @author Michael Hanus
--- @version May 2017
--- @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
 deriving (Eq,Show)

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