4.3. Module: alba.core.natural

There are arbitrary sized natural numbers and integer numbers. Both are given a definition as an inductive type. However they are compiled to more efficient types in the runtime.

Therefore the basic arithmetic functions and decision procedures are also defined in terms of the inductive types. But these arithmetic functions and decision procedures are compiled to more efficient runtime representations.

4.3.1. Builtin Definitions

class Natural: Any :=
    zero: Natural
    succ: Natural -> Natural

class (<=): Natural -> Natural -> Prop :=
    start {n}: 0 <= n
    next {n m}: n <= m -> succ n <= succ m


(<) (a b: Natural): Prop :=
    succ a <= b

(>=) (a b: Natural): Prop :=
    b <= a

(>) (a b: Natural): Prop :=
    b < a


pred: Natural -> Natural
:= case
    \ zero :=
        zero
    \ (succ n) :=
        n

zeroNotSucc: all {a: Natural}: zero /= succ a
:= case
    -- not unifiable


succInjective: all {a b: Natural}: succ a = succ b -> a = b
:=
    \ eqSucc := (=).inject pred eqSucc


(=?): (a b: Natural): Decision (a = b)
:= case
    λ zero      zero        :=
        true identical

    λ (succ n)  (succ m)    :=
        inspect n =? m case
            \ true eq :=
                true (=).inject succ eq
            \ (false notEq) :=
                false (\ eqSuccs := notEq (succInjective eqSuccs))

    λ zero (succ m) :=
        false zeroNotSucc

    \ (succ n) zero :=
        false (\ eq := zeroNotSucc ((=).flip eq))


(<?): Natural -> Natural -> Bool := case
    λ _         zero        := false
    λ zero      (succ _)    := true
    λ (succ n)  (succ m)    := n <? m

(+): Natural -> Natural -> Natural := case
    λ n zero        := n
    λ n (succ m)    := succ (n + m)

(-): Natural -> Natural -> Natural := case
    λ n         zero        :=  n
    λ n         (succ _)    :=  zero
    λ (succ n)  (succ m)    :=  n - m

(*): Natural -> Natural -> Natural := case
    λ zero      m           :=  zero
    λ (succ n)  m           :=  n * m + m

(^): Natural -> Natural -> Natural := case
    λ n         zero        := succ zero
    λ n         (succ m)    := n * (n ^ m)

divAux: Natural -> Natural -> Natural -> Natural -> Natural := case
        -- n / (succ m) = divAux 0 m n m
    λ k m   zero        j       :=  k
    λ k m   (succ n)    zero    :=  divAux (succ k) m n m
    λ k m   (succ n)    (succ j):=  divAux k m n j

modAux: Natural -> Natural -> Natural -> Natural -> Natural := case
        -- n % (succ m) = modAux 0 m n m
    λ k m   zero        j       :=  k
    λ k m   (succ n)    zero    :=  modAux 0 m n m
    λ k m   (succ n)    (succ j):=  modAux (succ k) m n j

Key idea in divAux and modAux: The number k is initialized to zero and incremented in some cases such that at the end it is either the quotient or the remainder. Both are total functions have efficient runtime representations.

4.3.2. Recursion and Induction

recurse
    {F: Natural -> Any}
    (start: F zero)
    (next: all i: F i -> F (succ i))
    : all n: F n
:= case
    \ zero :=
        start
    \ (succ n) :=
        next n (recurse n)


induce
    {P: Predicate Natural}
    (start: P zero)
    (next: all {i}: P i -> P (succ i))
    : all {n}: P n
:= case
    \ {zero} :=
        start
    \ {succ n} :=
        next (induce {n})

4.3.3. Addition

4.3.3.1. Helper Functions

pullSucc:
    all {a b: Natural}:
        succ a + b = succ (a + b)
:= case
    \ {a} {zero} :=
        identical
    \ {a} {succ n} :=
        (=).inject succ (pullSucc {a} {n})


pushSucc {a b: Natural}:
        succ (a + b) = succ a + b
:=
    (=).flip pullSucc


zeroLeftNeutral:
    all {a: Natural}
        zero + a = a
:= case
    \ {zero} :=
        identical
    \ {succ n} :=
        (=).inject succ (zeroLeftNeutral {n})

4.3.3.2. Associativity

associate:
    all {a b c: Natural}:
        a + b + c = a + (b + c)
:= case
    \ {a} {b} {zero} :=
        identical
    \ {a} {b} {succ n} :=
        (=).inject succ (associate {a} {b} {n})

4.3.3.3. Commutativity

commute:
    all {a b: Natural}:
        a + b = b + a
:= case
    \ {a} {zero} :=
        (=).flip zeroLeftNeutral
    \ {a} {succ n} :=
        (=).(
            inject succ (commute {a} {n})   -- a + succ n = succ (n + a)
            +
            pushSucc {n} {a}                --            = succ n + a
        )

4.3.4. Multiplication

4.3.5. Exponentiation

4.3.6. Order Relation