Nat.fm

// Nat.fm
// ======
//
// Natural numbers.

import Bool
import Empty
import Equal
import Pair
import The
import Unit

// Definition
// ----------

T Nat
| zero
| succ(pred: Nat)

T Comparison
| less_than
| equal_to
| greater_than

// Functions
// ---------

// Predecessor
pred(n: Nat) : Nat
  case n
  | zero => zero
  | succ => n.pred

// Copies a Nat
copy_nat(n: Nat) : Pair(Nat, Nat)
  case n
  | zero => pair(__ zero, zero)
  | succ => case copy_nat(n.pred) as pred
    | pair => pair(__ succ(pred.fst), succ(pred.snd))

// Addition
add(n: Nat, m: Nat) : Nat
  case n
  with m : Nat
  | zero => m
  | succ => case m
    with n.pred : Nat
    | zero => succ(n.pred)
    | succ => succ(succ(add(n.pred, m.pred)))

// Left-hand addition
addl(n: Nat, m: Nat) : Nat
  case n
  with m : Nat
  | zero => m
  | succ => succ(addl(n.pred, m))

// Subtraction
sub(n: Nat, m: Nat) : Nat
  case m
  with n : Nat
  | zero => n
  | succ => case n
    | zero => zero
    | succ => sub(n.pred, m.pred)

// Multiplication by 2
double(n: Nat) : Nat
  case n
  | zero => zero
  | succ => succ(succ(double(n.pred)))

// Helper for the multiplication below
mul.go(k: Nat, n: Nat, m: Nat) : Nat
  let f = mul.go
  case k
  with n: Nat
  with m: Nat
  with f: Nat -> Nat -> Nat -> Nat
  | zero => case m
    | zero => zero
    | succ => f(n, zero, m.pred)
  | succ => succ(f(k.pred, succ(n), m))

// Multiplication
mul(n: Nat, m: Nat) : Nat
  mul.go(zero, n, m)

// Comparison
nat_compare(n: Nat, m: Nat) : Comparison
  case n
  with m: Nat
  | zero => case m
    | zero => equal_to
    | succ => less_than
  | succ => case m
    | zero => greater_than
    | succ => nat_compare(n.pred, m.pred)

// Equality
nat_equal(n: Nat, m: Nat) : Bool
  case nat_compare(n, m) as cmp
  | less_than    => false
  | equal_to     => true
  | greater_than => false

// Theorems
// --------

// Proof that `1 != 0`
succ_isnt_zero(n : Nat;) : succ(n) != zero
  let P = (n: Nat) =>
    case n
    | zero => Empty
    | succ => Unit
  (e) => unit :: rewrite P(.) with e

// Proof that `0 != 1`
zero_isnt_succ(n: Nat;): zero != succ(n)
  let P = (n: Nat) =>
    case n
    | zero => Unit
    | succ => Empty
  (e) => unit :: rewrite P(.) with e

// Proof that `n == m` implies `succ(n) == succ(m)`
apply_succ(n: Nat; m; e: n == m) : succ(n) == succ(m)
  apply(_____ e)

addl.succ(n: Nat, m: Nat) : succ(addl(n,m)) == addl(n,succ(m))
  case n
  with m : Nat
  | zero => equal(__)
  | succ => apply(____ succ; addl.succ(n.pred,m))
  : succ(addl(n,m)) == addl(n,succ(m))

addl.commute(n: Nat, m: Nat) : addl(n,m) == addl(m,n)
  case n
  with m : Nat
  | zero =>
    case m
    | zero => equal(__)
    | succ => apply(____ succ; addl.commute(zero,m.pred))
    : addl(zero,m) == addl(m,zero)
  | succ => 
    let e = apply(____ succ; addl.commute(n.pred,m))
    rewrite(___ addl.succ(m,n.pred), Equal(Nat,addl(succ(n.pred),m)); e)
  : addl(n,m) == addl(m,n)

add.commute(n: Nat, m: Nat) : add(n,m) == add(m,n)
  case n
  with m : Nat
  | zero =>
    case m
    | zero => equal(__)
    | succ => equal(__)
    : add(zero,m) == add(m,zero)
  | succ =>
    case m
    | zero => equal(__)
    | succ => apply(____ (x) => succ(succ(x)); add.commute(n.pred,m.pred))
    : add(succ(n.pred),m) == add(m,succ(n.pred))
  : add(n,m) == add(m,n)

addl.succ_succ(n: Nat, m: Nat) : succ(succ(addl(n,m))) == addl(succ(n),succ(m))
  case n
  with m : Nat
  | zero => equal(__)
  | succ => apply(____ succ; addl.succ_succ(n.pred,m))
  : succ(succ(addl(n,m))) == addl(succ(n),succ(m))

add.addl(n: Nat, m: Nat) : add(n,m) == addl(n,m)
  case n
  with m : Nat
  | zero =>
    case m
    | zero => equal(__)
    | succ => equal(__)
    : add(zero,m) == addl(zero,m)
  | succ =>
    case m
    | zero => 
      let P = (x) => Equal(Nat,x,addl(zero,succ(n.pred)))
      let e = rewrite(___ add.commute(zero,succ(n.pred)),P; equal(__))
      let addl_zn = addl.commute(zero,succ(n.pred))
      rewrite(___ addl_zn,Equal(Nat,add(succ(n.pred),zero)); e)
    | succ => 
      let e = apply(____ (x) => succ(succ(x)); add.addl(n.pred,m.pred))
      let addl_ss = addl.succ_succ(n.pred,m.pred)
      rewrite(___ addl_ss, Equal(Nat,succ(succ(add(n.pred,m.pred)))); e)
    : add(succ(n.pred),m) == addl(succ(n.pred),m)
  : add(n,m) == addl(n,m)

// Tests
// -----

nat.test0: The(Nat, 6n)
  the(_ add(3n, 3n))

nat.test1: The(Nat, 6n)
  the(_ mul(2n, 3n))