Nat.gr

------
--- Module: Nat
--- Description: Base library for operations on type-indexed natural numbers
--- Authors: Dominic Orchard, Vilem-Benjamin Liepelt
--- License: BSD3
--- Copyright: (c) Authors 2018
--- Issue-tracking: https://github.com/dorchard/granule/issues
--- Repository: https://github.com/dorchard/granule
------

module Nat where

data N (n : Nat) where
  Z : N 0;
  S : N n -> N (n+1)

copyNat : forall {n : Nat} . N n -> (N n, N n)
copyNat Z = (Z, Z);
copyNat (S n) = let (x, y) = copyNat n in (S x, S y)

--- Convert an indexed natural number to an untyped int
natToInt
  : forall {n : Nat}
  . N n -> Int
natToInt Z = 0;
natToInt (S m) = 1 + natToInt m

--- # Arithmetic operations

--- Addition
add
  : forall {m n : Nat}
  . N n -> N m -> N (n + m)
add Z m = m;
add (S n') m = S (add n' m)

-- Cut-off subtraction
monus
  : forall {m n : Nat}
  . N m -> N n -> N (m - n)
monus m Z = m;
monus Z (S n') = monus Z n';
monus (S m') (S n') = monus m' n'

sub
  : forall {m n : Nat}
  . {n .≥ m} => N n -> N m -> N (n - m)
sub m Z = m;
sub (S m') (S n') = sub m' n'

-- less explicit than `sub`, therefore sub-prime (excuse the pun)
-- sub' : forall m n. N (m + n) -> N m -> N n
-- sub' m Z = m;
-- sub' (S m') (S n') = sub' m' n'

--- Right-moded multiplication
mult
  : forall {m n : Nat}
  . N n -> (N m) [n] -> N (n * m)
mult Z [m] = Z;
mult (S n') [m] = add m (mult n' [m])

--- Left-moded multiplication
mult_r
  : forall {m n : Nat}
  . (N n) [m] -> (N m) -> N (n * m)
mult_r [n] Z = Z;
mult_r [n] (S m') = add n (mult_r [n] m')

--- Divide by two
div2
  : forall {n : Nat}
  . N (2 * n) -> N n
div2 Z = Z;
div2 (S (S x)) = S (div2 x)