Prelude.Nat

toIntegerNat : Nat -> Integer

Convert a Nat to an Integer

toIntNat : Nat -> Int

Tail recursive cast Nat to Int
Note that this can overflow

succNotLTEzero : Not (LTE (S m) 0)

A successor is never less than or equal zero

succInjective : (left : Nat) -> (right : Nat) -> (p : S left = S right) -> left = right

S is injective

sucMinR : (l : Nat) -> minimum l (S l) = l

sucMinL : (l : Nat) -> minimum (S l) l = l

sucMaxR : (l : Nat) -> maximum l (S l) = S l

sucMaxL : (l : Nat) -> maximum (S l) l = S l

predSucc : (n : Nat) -> pred (S n) = n

pred : Nat -> Nat

The predecessor of a natural number. pred Z is Z.

powerZeroOne : (base : Nat) -> power base (fromInteger 0) = 1

powerSuccSuccMultStepCase : (base : Nat) -> (inductiveHypothesis : power base (fromInteger 2) = mult base base) -> S (plus (mult base 1) (mult base (S (mult base 1)))) = S (plus base (mult base (S base)))

powerSuccSuccMult : (base : Nat) -> power base (fromInteger 2) = mult base base

powerSuccPowerLeft : (base : Nat) -> (exp : Nat) -> power base (S exp) = base * power base exp

powerPowerMultPowerStepCase : (base : Nat) -> (exp : Nat) -> (exp' : Nat) -> (inductiveHypothesis : power (power base exp) exp' = power base (exp * exp')) -> mult (power base exp) (power (power base exp) exp') = power base (mult exp (S exp'))

powerPowerMultPowerBaseCase : (base : Nat) -> (exp : Nat) -> 1 = power base (mult exp 0)

powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) -> power (power base exp) exp' = power base (exp * exp')

powerOneSuccOneStepCase : (exp : Nat) -> (inductiveHypothesis : power (fromInteger 1) exp = 1) -> plus (power 1 exp) 0 = 1

powerOneSuccOne : (exp : Nat) -> power (fromInteger 1) exp = 1

powerOneNeutralStepCase : (base : Nat) -> (inductiveHypothesis : power base (fromInteger 1) = base) -> S (mult base 1) = S base

powerOneNeutral : (base : Nat) -> power base (fromInteger 1) = base

power : Nat -> Nat -> Nat

Exponentiation of natural numbers

plusZeroRightNeutralStepCase : (n : Nat) -> (inductiveHypothesis : n + fromInteger 0 = n) -> S (plus n 0) = S n

plusZeroRightNeutral : (left : Nat) -> left + fromInteger 0 = left

plusZeroLeftNeutral : (right : Nat) -> fromInteger 0 + right = right

plusSuccRightSuccStepCase : (left : Nat) -> (right : Nat) -> (inductiveHypothesis : S (left + right) = left + S right) -> S (S (plus left right)) = S (plus left (S right))

plusSuccRightSucc : (left : Nat) -> (right : Nat) -> S (left + right) = left + S right

plusRightCancelStepCase : (left : Nat) -> (left' : Nat) -> (right : Nat) -> (p : left + S right = left' + S right) -> (inductiveHypothesis : (left + right = left' + right) -> left = left') -> left = left'

plusRightCancelBaseCase : (left : Nat) -> (left' : Nat) -> (p : left + 0 = left' + 0) -> left = left'

plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) -> (p : left + right = left' + right) -> left = left'

plusOneSucc : (right : Nat) -> fromInteger 1 + right = S right

plusMinusLeftCancelStepCase : (left : Nat) -> (right : Nat) -> (right' : Nat) -> (inductiveHypothesis : left + right - (left + right') = right - right') -> minus (plus left right) (plus left right') = minus right right'

plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) -> left + right - (left + right') = right - right'

plusLeftLeftRightZeroStepCase : (left : Nat) -> (right : Nat) -> (p : S left + right = S left) -> (inductiveHypothesis : (left + right = left) -> right = 0) -> right = 0

plusLeftLeftRightZeroBaseCase : (right : Nat) -> (p : 0 + right = 0) -> right = 0

plusLeftLeftRightZero : (left : Nat) -> (right : Nat) -> (p : left + right = left) -> right = 0

plusLeftCancelStepCase : (left : Nat) -> (right : Nat) -> (right' : Nat) -> (p : S left + right = S left + right') -> (inductiveHypothesis : (left + right = left + right') -> right = right') -> right = right'

plusLeftCancelBaseCase : (right : Nat) -> (right' : Nat) -> (p : 0 + right = 0 + right') -> right = right'

plusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) -> (p : left + right = left + right') -> right = right'

plusConstantRight : (left : Nat) -> (right : Nat) -> (c : Nat) -> (p : left = right) -> left + c = right + c

plusConstantLeft : (left : Nat) -> (right : Nat) -> (c : Nat) -> (p : left = right) -> c + left = c + right

plusCommutativeStepCase : (left : Nat) -> (right : Nat) -> (inductiveHypothesis : left + right = right + left) -> S (plus left right) = plus right (S left)

plusCommutativeBaseCase : (right : Nat) -> right = plus right 0

plusCommutative : (left : Nat) -> (right : Nat) -> left + right = right + left

plusAssociativeStepCase : (left : Nat) -> (centre : Nat) -> (right : Nat) -> (inductiveHypothesis : left + (centre + right) = left + centre + right) -> S (plus left (plus centre right)) = S (plus (plus left centre) right)

plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) -> left + (centre + right) = left + centre + right

plus : (n : Nat) -> (m : Nat) -> Nat

Add two natural numbers.

n

the number to case-split on

m

the other number

multZeroRightZeroStepCase : (left : Nat) -> (inductiveHypothesis : left * 0 = 0) -> mult left 0 = 0

multZeroRightZero : (left : Nat) -> left * 0 = 0

multZeroLeftZero : (right : Nat) -> 0 * right = 0

multRightSuccPlusStepCase : (left : Nat) -> (right : Nat) -> (inductiveHypothesis : left * S right = left + left * right) -> S (plus right (mult left (S right))) = S (plus left (plus right (mult left right)))

multRightSuccPlus : (left : Nat) -> (right : Nat) -> left * S right = left + left * right

multPowerPowerPlusStepCase : (base : Nat) -> (exp : Nat) -> (exp' : Nat) -> (inductiveHypothesis : power base exp * power base exp' = power base (exp + exp')) -> mult (mult base (power base exp)) (power base exp') = mult base (power base (plus exp exp'))

multPowerPowerPlusBaseCase : (base : Nat) -> (exp' : Nat) -> plus (power base exp') 0 = power base exp'

multPowerPowerPlus : (base : Nat) -> (exp : Nat) -> (exp' : Nat) -> power base exp * power base exp' = power base (exp + exp')

multOneRightNeutralStepCase : (left : Nat) -> (inductiveHypothesis : left * fromInteger 1 = left) -> S (mult left 1) = S left

multOneRightNeutral : (left : Nat) -> left * fromInteger 1 = left

multOneLeftNeutralStepCase : (right : Nat) -> (inductiveHypothesis : fromInteger 1 * right = right) -> S (plus right 0) = S right

multOneLeftNeutral : (right : Nat) -> fromInteger 1 * right = right

multLeftSuccPlus : (left : Nat) -> (right : Nat) -> S left * right = right + left * right

multDistributesOverPlusRightStepCase : (left : Nat) -> (centre : Nat) -> (right : Nat) -> (inductiveHypothesis : left * (centre + right) = left * centre + left * right) -> plus (plus centre right) (mult left (plus centre right)) = plus (plus centre (mult left centre)) (plus right (mult left right))

multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) -> left * (centre + right) = left * centre + left * right

multDistributesOverPlusLeftStepCase : (left : Nat) -> (centre : Nat) -> (right : Nat) -> (inductiveHypothesis : (left + centre) * right = left * right + centre * right) -> plus right (mult (plus left centre) right) = plus (plus right (mult left right)) (mult centre right)

multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) -> (left + centre) * right = left * right + centre * right

multDistributesOverMinusRightBody : (left : Nat) -> (centre : Nat) -> (right : Nat) -> mult left (minus centre right) = minus (mult left centre) (mult left right)

multDistributesOverMinusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) -> left * (centre - right) = left * centre - left * right

multDistributesOverMinusLeftStepCase : (left : Nat) -> (centre : Nat) -> (right : Nat) -> (inductiveHypothesis : (left - centre) * right = left * right - centre * right) -> mult (minus left centre) right = minus (plus right (mult left right)) (plus right (mult centre right))

multDistributesOverMinusLeftBaseCase : (left : Nat) -> (right : Nat) -> plus right (mult left right) = minus (plus right (mult left right)) 0

multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) -> (left - centre) * right = left * right - centre * right

multCommutativeStepCase : (left : Nat) -> (right : Nat) -> (inductiveHypothesis : left * right = right * left) -> plus right (mult left right) = mult right (S left)

multCommutativeBaseCase : (right : Nat) -> 0 = mult right 0

multCommutative : (left : Nat) -> (right : Nat) -> left * right = right * left

multAssociativeStepCase : (left : Nat) -> (centre : Nat) -> (right : Nat) -> (inductiveHypothesis : left * (centre * right) = left * centre * right) -> plus (mult centre right) (mult left (mult centre right)) = mult (plus centre (mult left centre)) right

multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) -> left * (centre * right) = left * centre * right

mult : Nat -> Nat -> Nat

Multiply natural numbers

modNatNZ : Nat -> (y : Nat) -> Not (y = 0) -> Nat

modNat : Nat -> Nat -> Nat

minusZeroRight : (left : Nat) -> left - fromInteger 0 = left

minusZeroN : (n : Nat) -> 0 = n - n

minusZeroLeft : (right : Nat) -> fromInteger 0 - right = 0

minusSuccSucc : (left : Nat) -> (right : Nat) -> S left - S right = left - right

minusSuccPredStepCase' : (left : Nat) -> (right : Nat) -> (inductiveHypothesis : left - S right = pred (left - right)) -> minus left (S right) = pred (minus left right)

minusSuccPredStepCase : (left : Nat) -> (inductiveHypothesis : left - 1 = pred (left - 0)) -> minus left 0 = left

minusSuccPred : (left : Nat) -> (right : Nat) -> left - S right = pred (left - right)

minusSuccOne : (n : Nat) -> S n - fromInteger 1 = n

minusPlusZero : (n : Nat) -> (m : Nat) -> n - (n + m) = 0

minusOneSuccN : (n : Nat) -> 1 = S n - n

minusMinusMinusPlusStepCase : (left : Nat) -> (centre : Nat) -> (right : Nat) -> (inductiveHypothesis : left - centre - right = left - (centre + right)) -> minus (minus left centre) right = minus left (plus centre right)

minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) -> left - centre - right = left - (centre + right)

minus : Nat -> Nat -> Nat

Subtract natural numbers. If the second number is larger than the first, return 0.

minimumZeroZeroRight : (right : Nat) -> minimum (fromInteger 0) right = 0

minimumZeroZeroLeft : (left : Nat) -> minimum left (fromInteger 0) = 0

minimumSuccSuccStepCase : (left : Nat) -> (right : Nat) -> (inductiveHypothesis : minimum (S left) (S right) = S (minimum left right)) -> S (S (minimum left right)) = S (S (minimum left right))

minimumSuccSucc : (left : Nat) -> (right : Nat) -> minimum (S left) (S right) = S (minimum left right)

minimumIdempotent : (n : Nat) -> minimum n n = n

minimumCommutative : (l : Nat) -> (r : Nat) -> minimum l r = minimum r l

minimumAssociative : (l : Nat) -> (c : Nat) -> (r : Nat) -> minimum l (minimum c r) = minimum (minimum l c) r

minimum : Nat -> Nat -> Nat

Find the least of two natural numbers

maximumZeroNRight : (right : Nat) -> maximum 0 right = right

maximumZeroNLeft : (left : Nat) -> maximum left 0 = left

maximumSuccSuccStepCase : (left : Nat) -> (right : Nat) -> (inductiveHypothesis : S (maximum left right) = maximum (S left) (S right)) -> S (S (maximum left right)) = S (S (maximum left right))

maximumSuccSucc : (left : Nat) -> (right : Nat) -> S (maximum left right) = maximum (S left) (S right)

maximumIdempotent : (n : Nat) -> maximum n n = n

maximumCommutative : (l : Nat) -> (r : Nat) -> maximum l r = maximum r l

maximumAssociative : (l : Nat) -> (c : Nat) -> (r : Nat) -> maximum l (maximum c r) = maximum (maximum l c) r

maximum : Nat -> Nat -> Nat

Find the greatest of two natural numbers

lteSuccRight : LTE n m -> LTE n (S m)

n < m implies n < m + 1

lteRefl : LTE n n

LTE is reflexive.

lteNTrue : (n : Nat) -> lte n n = True

lte : Nat -> Nat -> Bool

Boolean test than one Nat is less than or equal to another

lt : Nat -> Nat -> Bool

Boolean test than one Nat is strictly less than another

log2NZ : (x : Nat) -> Not (x = 0) -> Nat

log2 : Nat -> Nat

lcm : Nat -> Nat -> Nat

isZero : Nat -> Bool

isSucc : Nat -> Bool

isLTE : (m : Nat) -> (n : Nat) -> Dec (LTE m n)

A decision procedure for LTE

ifThenElseSuccSucc : (cond : Bool) -> (t : Nat) -> (f : Nat) -> S if cond then t else f = if cond then S t else S f

ifThenElsePlusPlusRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) -> if cond then t else f + right = if cond then t + right else f + right

ifThenElsePlusPlusLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) -> left + if cond then t else f = if cond then left + t else left + f

ifThenElseMultMultRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) -> if cond then t else f * right = if cond then t * right else f * right

ifThenElseMultMultLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) -> left * if cond then t else f = if cond then left * t else left * f

hyper : Nat -> Nat -> Nat -> Nat

gte : Nat -> Nat -> Bool

Boolean test than one Nat is greater than or equal to another

gt : Nat -> Nat -> Bool

Boolean test than one Nat is strictly greater than another

gcd : Nat -> Nat -> Nat

fromLteSucc : LTE (S m) (S n) -> LTE m n

If two numbers are ordered, their predecessors are too

fromIntegerNat : Integer -> Nat

Convert an Integer to a Nat, mapping negative numbers to 0

fib : Nat -> Nat

Fibonacci numbers

fact : Nat -> Nat

Factorial function

eqSucc : (left : Nat) -> (right : Nat) -> (p : left = right) -> S left = S right

S preserves equality

divNatNZ : Nat -> (y : Nat) -> Not (y = 0) -> Nat

divNat : Nat -> Nat -> Nat

divCeilNZ : Nat -> (y : Nat) -> Not (y = fromInteger 0) -> Nat

divCeil : Nat -> Nat -> Nat

cmp : (x : Nat) -> (y : Nat) -> CmpNat x y

SIsNotZ : (S x = 0) -> Void

data Nat : Type

Unary natural numbers

Z : Nat

Zero

S : Nat -> Nat

Successor

data Multiplicative : Type

A wrapper for Nat that specifies the semigroup and monad instances that use (+)

getMultiplicative : Nat -> Multiplicative

LTESuccZeroFalse : (n : Nat) -> lte (S n) 0 = False

data LTE : (n : Nat) -> (m : Nat) -> Type

Proofs that n is less than or equal to m

n

the smaller number

m

the larger number

LTEZero : LTE 0 right

Zero is the smallest Nat

LTESucc : LTE left right -> LTE (S left) (S right)

If n <= m, then n + 1 <= m + 1

LT : Nat -> Nat -> Type

Strict less than

GTE : Nat -> Nat -> Type

Greater than or equal to

GT : Nat -> Nat -> Type

Strict greater than

data CmpNat : Nat -> Nat -> Type

CmpLT : (y : Nat) -> CmpNat x (plus x (S y))

CmpEQ : CmpNat x x

CmpGT : (x : Nat) -> CmpNat (plus y (S x)) y

data Additive : Type

A wrapper for Nat that specifies the semigroup and monad instances that use (*)

getAdditive : Nat -> Additive