polarity/std/data/nat.pol

use "./bool.pol"
use "./ordering.pol"

/// The type of Peano natural numbers.
data Nat {
    /// The constant zero.
    Z,
    /// The successor of a Peano natural number.
    S(pred: Nat),
}

/// Addition of two natural numbers.
def Nat.add(other: Nat): Nat {
    Z => other,
    S(x) => S(x.add(other)),
}

/// Multiplication of two natural numbers.
def Nat.mul(other: Nat): Nat {
    Z => Z,
    S(x) => other.add(x.mul(other)),
}

/// A saturating version of subtraction.
def Nat.monus(other: Nat): Nat {
    Z => Z,
    S(pred) =>
        other.match {
            Z => S(pred),
            S(pred') => pred.monus(pred'),
        },
}

/// The factorial of a natural number.
def Nat.fact: Nat {
    Z => S(Z),
    S(pred) => S(pred).mul(pred.fact),
}

/// The predecessor of a natural number.
/// The predecessor of `Z` is `Z`.
def Nat.pred: Nat {
    Z => Z,
    S(x) => x,
}

/// Compare two natural numbers.
def Nat.cmp(other: Nat): Ordering {
    Z => other.match {
        Z => EQ,
        S(_) => LT,
    },
    S(x) => other.match {
        Z => GT,
        S(other) => x.cmp(other),
    },
}

/// The lesser-or-equal relation on natural numbers.
data LE(x y: Nat) {
    LERefl(x: Nat): LE(x, x),
    LESucc(x y: Nat, h: LE(x, y)): LE(x, S(y)),
}

/// Z is smaller than any natural number.
def (x: Nat).z_le: LE(Z, x) {
    Z => LERefl(Z),
    S(x) => LESucc(Z, x, x.z_le),
}

/// If x <= y, then S(x) <= S(y)
def LE(x, y).le_succ(x y: Nat): LE(S(x), S(y)) {
    LERefl(_) => LERefl(S(x)),
    LESucc(x, y, h) => LESucc(S(x), S(y), h.le_succ(x, y)),
}

/// If S(x) <= S(y), then x <= y.
def LE(S(x), S(y)).le_unsucc(x y: Nat): LE(x, y) {
    LERefl(_) => LERefl(x),
    LESucc(_, _, h) => h.s_le(x, y),
}

/// If S(x) <= y, then x <= y
def LE(S(x), y).s_le(x y: Nat): LE(x, y) {
    LERefl(_) => LESucc(x, x, LERefl(x)),
    LESucc(_, y', h) => LESucc(x, y', h.s_le(x, y')),
}