2.2. Natural Numbers

2.2.1. Basic Definitions

type Nat :=
    zero: Nat
    succ: Nat -> Nat

one: Nat := succ zero

(+): Nat -> Nat -> Nat := case
    \ zero, b     := b
    \ succ n, b   := succ (n + b)

(*): Nat -> Nat -> Nat := case
    \ zero, _     := zero
    \ succ n, b   := b + n * b

(^): Nat -> Nat -> Nat := case
    \ a,  zero    := one
    \ a,  succ n  := a * a^n


type (<=): Nat -> Nat -> Prop :=
    start {n}: zero <= n
    next  {n m}: n <= m  ->  succ n <= succ m

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

2.2.2. Zero is Different from a Successor

zeroNeSucc: all {n: Nat}: zero = succ n -> False :=
    case        -- no clauses

A potential clause would have the form

case
\ {n}, same {?m} := ?
--      : ?m = ?m

This would require to unify zero = succ n with ?m = ?m which is impossible, because ?m cannot be zero and succ n at the same time (zero and succ n are not unifiable).

2.2.3. Properties of Addition

Having a + succ b it is possible to pull out the successor function getting succ (a + b). This can be proved by induction on a. The base case is proved by reflexivity. The induction step requires to prove the equality of the two expressions

-- expressions                          normal forms
succ n + succ b                         succ (n + succ b)
succ (succ n + b)                       succ (succ (n + b))

This can be done by the induction hypothesis using congruence.

pullSucc: all {a b: Nat}: a + succ b = succ (a + b) := case
    \ {zero},   {_} := refl
    \ {succ n}, {_} := congruence {succ} pullSucc

Zero is the neutral element of addition. The left neutrality doesn’t need a proof. It is evident by normalisation. The right neutrality a + zero = a requires an induction proof.

zeroRightNeutral: all {a: Nat}: a + zero = a := case
    \ {zero}   := refl
    \ {succ n} := congruence {succ} zeroRightNeutral

Addition is commutative i.e. a + b = b + a. We prove this by induction on a. The base case is proved by right neutrality of zero. The induction case requires a proof of the equality of the two left expressions

-- expression                       normal form
succ n + b                          succ (n + b)
b + succ n                          b + succ n

Via the induction hypothesis and congruence we can prove the equality of succ (n + b) and succ (b + n). The flipped version of pullSucc can transform it into b + succ n.

plusCommutes: all {a b: Nat}: a + b = b + a := case
    \ {zero},   {b}   := zeroRightNeutral
    \ {succ n}, {b}   := (congruence {succ} plusCommutes, flip pullSucc)

The associativity of addition

(a + b) + c = a + (b + c)

can be proved by induction on a. The base case is trivial. The proof of the induction step can be done by the equivalences

(succ n + b) + c
=                           -- normalisation
succ ((n + b) + c)
=                           -- induction hypothesis + congruence
succ (n + (b + c))
=                           -- normalisation (bwd)
succ n + (b + c)

plusAssociates: all {a b c: Nat}: (a + b) + c = a + (b + c)
:= case
    \ {zero},   {b}, {c} := same
    \ {succ n}, {b}, {c} := congruence {succ} plusAssociates

2.2.4. Properties of Multiplication

Multiplication distributes over addition. In order to prove this we need a helper theorem.

plusSwap: all {a b c: Nat}: a + (b + c) = b + (a + c)
:=
    ( flip plusAssociates:                    _ = (a + b) + c
    , congruence {\ x := x + c} plusCommutes: _ = (b + a) + c
    , plusAssociates:                         _ = b + (a + c)
    )

Having plusSwap we can prove the distributivity of multiplication

a * (b + c) = a * b + a * c

by induction on a. The base case is trivial. The induction step requires a proof of

succ n * (b + c) = succ n * b + succ n * c

The equality can be proved by the steps

succ n * (b + c)
=                               -- normalisation
(b + c) + n * (b + c)
=                               -- associativity of addition
b + (c + n * (b + c))
=                               -- induction hypothesis + congruence
b + (c + (n * b + n * c))
=                               -- plusSwap + congruence
b + (n * b + (c + n * c))
=                               -- associativity of addition (bwd)
(b + n * b) + (c + b * c)
=                               -- normalization (bwd)
succ n * b + succ n * c

timesDistributes: all {a b c: Nat}: a * (b + c)  =  a * b + a * c
    -- Multiplication distributes over addition
:= case
    \ {zero},    {b},   {c} := refl
    \ {succ n},  {b},   {c} :=
        -- goal:
        --       succ n * (b + c)
        --       =
        --       succ n * b + succ n * c
        ( plusAssociates:
                succ n * (b + c)
                =
                b + (c + n * (b + c))

        , congruence
                {\ x := b + (c + x)}
                timesDistributes
            :   _
                =
                b + (c + (n * b + n * c))

        , congruence
            {\ x :=  b + x}
            plusSwap
            :  _
               =
               b + (n * b + (c + n * c))

        , flip plusAssociates
            :  _
               =
               succ n * b + succ n * c
               -- (b + n * b) + (c + n * c)
        )

2.2.5. Properties of Order

Reflexivity

leReflexive: all {a: Nat}: a <= a
    -- The less equal relation is reflexive.
:= case
    \ {zero}      :=  start
    \ {succ _}    :=  next leReflexive

-- with implicits made explicit
    \ {zero}      := start {zero}
    \ {succ n}    := next {n} {n} (leReflexive {n})

Inversion

leInvers {a b: Nat}: succ a <= succ b  ->  a <= b
    -- If two successors are less equal then the values are
    -- less equal as well.
:= case
    -- constructor 'start' not possible, its type is 'zero <= .'
    \ next le := le

    -- with implicits
    \ next {a} {b} le := le

Transitivity

(,): all {a b c: Nat}: a <= b -> b <= c -> a <= c
    -- The '<=' relation is transitive
:= case
    \ start,        _           := start
    \ next leAB,    next leBC   := next (leAB, leBC)

    -- with implicits
    \ {zero}, {b}, {c}, start {b}, _ :=

        start {c}

    \ {succ a}, {succ b}, {succ c}, next {a} {b} leAB, next {b} {c} leBC :=

        next {a} {c} ((,) {a} {b} {c} leAB leBC)

Others

ltIrreflexive: all {a: Nat}: a < a -> False
    -- The less than relation is irreflexive.
:= case
    -- The 'start' constructor constructs 'zero <= _' which cannot be
    -- unified with 'succ ?a <= ?a'.
    \ next lt := ltIrreflexive lt


leLtOrEq: all {a b: Nat}: a <= b -> a < b \/ a = b
:= case
    \ {zero},   {zero},     start   := right refl
    \ {zero},   {succ _},   start   := left (next start)
    \ {succ n}, {succ m},   next le :=
        match
            leLtOrEq le: n < m \/ n = m
        case
            \ left  lt  := left  (next lt)
            \ right eq  := right (congruence {succ} eq)


leSucc: all {a: Nat}: a <= succ a
    -- All numbers are less or equal their successors
:= case
    \ {zero}      := start
    \ {succ n}    := next leSucc



zeroLeast: all {a: Nat}: a <= zero  ->  a = zero
    -- All numbers less or equal 'zero' are 'zero'
:= case
    \ start := same
    -- The case 'next' is not possible!


notLtZero: all {a: Nat}: a < zero -> False
    -- No number is less than 'zero'
:= case
    -- neither start nor next can construct an object of
    -- type 'succ a <= zero'


ltSucc {a: Nat}: a < succ a
    -- All numbers are less than their successors
:=
    leReflexive

2.2.6. Order and Predicates

LowerBound (P: Nat -> Prop) (x: Nat): Prop
        -- 'x' is a lower bound for all numbers satisfying 'P'
:=
    all {y}: P y  ->  x <= y


StrictLowerBound (P: Nat -> Prop) (x: Nat): Prop
        -- 'x' is a strict lower bound for all numbers satisfying 'P'
:=
    all {y}: P y  ->  x < y


Least (P: Nat -> Prop) (x: Nat): Prop
    -- 'x' is the smallest number satisfying 'P'
:=
    LowerBound P x /\ P x


lowerBoundSucc
    {n: Nat} (lbN: LowerBound P n) (notPN: Not P n)
    : LowerBound P (succ n)
:=
    \ {y} (pY: P y): succ n <= y :=
        match leLtOrEq (lbN pY) case
            \ left  lt  := lt
            \ right eq  := notPN (replace {P} (flip eq) pY)

2.2.7. Difference

(-): all (a b: Nat) {le: b <= a}: Nat
:= case
    \ (a := zero)    zero       start     := a
    \ (a := succ _)  zero       start     := a
    \ (succ n)       (succ m)   (next le) := n - m

   -- or better
   case
     a        zero     {start}    := a
     (succ n) (succ m) {next le}  := (n - m) {le}

Note that the pattern match on b <= a is allowed in the case clauses, because only one constructor is possible. Therefore no decision is made on the propositional pattern match.

minusPlusInvers: all {a b: Nat}: b <= a -> a - b + b = a
:= case
    \ {zero},       {zero},     _       := zeroRightNeutral
    \ {succ n},     {zero},     _       := zeroRightNeutral
    \ {succ n},     {succ m},   next le :=
        -- goal: (succ n - succ m) + succ m = succ n
        -- i.e.: (n - m) + succ m = succ n
        (
            pullSucc: _ = succ ((n - m) + m)
        ,
            mapEquals (minusPlusInvers le)
        )

minusLe: all {a b: Nat}: b <= a -> a - b <= a
    -- Substraction makes a number less equal.
:= case
    \ {zero},   {zero},   start     := start
    \ {succ n}, {zero},   start     := leReflexive
    \ {succ n}, {succ m}, next le   :=
        -- goal: succ n - succ m <= succ n
        -- i.e.: n - m  <= succ n
        (
            minusLe le: n - m <= n
        ,
            leSucc:     n <= succ n
        )

From a < b we can infer c - b < c - a provided that b <= c is valid.

minusLt: all {a b c: Nat}: a <= c  ->  b <= c  ->  a < b  ->  c - b < c - a
    -- The preconditions 'a <= c'  and 'b <= c' are needed for '-'
:= case
    \ start,        next leBC,      next ltAB   :=
        -- goal: succ c - succ b < succ c - zero
        -- i.e.: succ (c - b) <= succ c
        next (minusLe leBC)
    \ next leAC,    next leBC,      next ltAB   :=
        -- goal: succ c - succ b < succ c - succ a
        -- i.e.: c - b < c - a
        minusLt leAC leBC ltAB

2.2.8. Wellfounded Recursion

Clearly all natural numbers are finite, because each number is constructed by finitely many applications of the successor function. But here we invent another way to express the finiteness of natural numbers.

We say that a number is finite, if all numbers below it are finite.

type Finite: Nat -> Prop :=
    fin {x}: (all {y}: y < x -> Finite y) -> Finite x

We can prove that all natural numbers are finite by an induction proof.

natFinite: all {n: Nat}: Finite n
:= case
    \ {zero} :=
        fin notLtZero

    \ {succ n} :=
        -- goal: Finite (succ n)
        let
            aux: all {n}: Finite n -> all {y}: y < succ n -> Finite y
            := case
                -- no match for
                --      {_} _ {_} start
                -- because
                --      succ y <= x
                -- cannot be unified with
                --      zero <= x

                {n} (finN := fin f) {y} (next le) :=
                    match
                        leLtOrEq (le: y <= n): y < n \/ y = n
                    case
                        left  lt  :=
                            (f: all {y}: y < n -> Finite y)
                                lt

                        right eq  :=
                            cast (flip eq) finN
        :=
            fin (aux natFinite: all {y}: y < succ n -> Finite y)
            : Finite (succ n)

Unbounded search:

find {P: Nat -> Prop} (d: Decider P): Exist P -> Refine (Least P)
:= case
    \ (w, pW) :=
        let
            aux: all n:
                    n <= w  ->              -- invariant 1
                    LowerBound P n ->       -- invariant 2
                    Finite (w - n) ->       -- bound function
                    Decision P n   ->
                    Refine (Least P)
            := case
                n _ lbN _ (true pN) :=
                    (n, lbN, pN)

                n leNW lbN (fin f) (false notPN) :=
                    let
                        lbSN: LowerBound P (succ n) :=
                            lowerBoundSucc lbN notPN

                        leSNW: succ n <= w :=
                            lbSN pW

                        ltWmSN: w - succ n < w - n :=
                            minusLt leNW leSNW leReflexive
                    :=
                        aux (succ n) leSNW lbSN (f ltWnSN) (d (succ n))
        :=
            aux zero start (\ _ := start) natFinite (d zero)