4.5. Module: alba.core.nat

4.5.1. Axioms and Builtin Definitions

Nat: Any

Nat.zero: Nat
Nat.one:  Nat

Nat.toNatural:   Nat -> Nat
Nat.fromNatural: Natural -> Nat

Nat.embed (a: Nat): fromNatural (to natural a) = a

Nat.(+): Nat -> Nat -> Nat
Nat.(*): Nat -> Nat -> Nat

Nat.(=?): all (a b: Nat): Decision (a = b)

Nat.(<=): Nat -> Nat -> Prop
Nat.(<=?): all (a b: Nat): Decision (a <= b)

Nat.zeroDefinition: zero = fromNatural zero
Nat.oneDefinition:  one  = fromNatural one

Nat.plusDefinition {a b: Nat}:
        a + b = fromNatural (toNatural a + toNatural b)

Nat.multDefinition {a b: Nat}:
        a * b = fromNatural (toNatural a * toNatural b)

Nat.leDefinition {a b: Nat}: a <= b <-> toNatural a <= toNatural b

4.5.2. Embedding into Natural Numbers

An embedding is always injective. Therefore we can prove that toNatural is injective by the embedding property and properties of equality.

Nat.injective {a b: Nat}: toNatural a = toNatural b -> a = b
:=
    \ eq :=
        (=).(
            flip (embed {a})            -- a = fromNatural (toNatural a)
            +
            inject fromNatural eq
            +
            embed {b}                   -- fromNatural (toNatural b) = b
        )