Module Data.Nat

Author
Michael Hanus
Version
December 2021

Library defining natural numbers in Peano representation and some operations on this representation.

Exported Datatypes:
Nat
Exported Functions:
addfromNatleqmulsubtoNat

Data type for natural numbers

data Nat

Natural numbers are defined in Peano representation.

Constructors:

  • Z :: Nat The zero constructor
  • S :: Nat -> Nat The successor constructor

Known instances:

Conversion operations

fromNat :: Nat -> Int  Deterministic 

Transforms a natural number into a standard integer.

Postcondition:
n = fromNat _ satisfies n >= 0(fromNat'post)

toNat :: Int -> Nat  Deterministic 

Transforms a standard integer into a natural number.

Precondition:
(toNat n) requires n >= 0(toNat'pre)
Properties:
toNat (fromNat n) -=- n(fromToNat)
(n >= 0) ==> (fromNat (toNat n) -=- n)(toFromNat)
Further infos:
  • partially defined

Arithmetic operations

add :: Nat -> Nat -> Nat  Deterministic 

Addition on natural numbers.

Properties:
add x y -=- add y x(addIsCommutative)
add (add x y) z -=- add x (add y z)(addIsAssociative)
Further infos:
  • solution complete, i.e., able to compute all solutions

sub :: Nat -> Nat -> Nat  Non-deterministic 

Subtraction defined by reversing addition.

Properties:
sub (add x y) x -=- y(subAddL)
sub (add x y) y -=- x(subAddR)

mul :: Nat -> Nat -> Nat  Deterministic 

Multiplication on natural numbers.

Properties:
mul x y -=- mul y x(mulIsCommutative)
mul (mul x y) z -=- mul x (mul y z)(mulIsAssociative)
mul x (add y z) -=- add (mul x y) (mul x z)(distMulAddL)
mul (add y z) x -=- add (mul y x) (mul z x)(distMulAddR)
Further infos:
  • solution complete, i.e., able to compute all solutions

Comparison predicates

leq :: Nat -> Nat -> Bool  Deterministic 

The less-or-equal predicate on natural numbers.

Properties:
always $ leq x (add x y)(leqAdd)
Further infos:
  • solution complete, i.e., able to compute all solutions