dk_binary_nat.dk

#NAME dk_binary_nat

UNat : Type := dk_nat.Nat.
Bool : Type := dk_bool.Bool.

bNat : cc.uT.
BNat : Type := cc.eT bNat.

O : BNat.
S0 : BNat -> BNat.
S1 : BNat -> BNat.
(; twice zero is zero ;)
[] S0 O --> O.

nat_of_bnat : BNat -> UNat.
[] nat_of_bnat O --> dk_nat.O
[ bn : BNat ]
    nat_of_bnat (S0 bn)
      -->
    dk_nat.mult dk_nat.2 (nat_of_bnat bn)
[ bn : BNat ]
    nat_of_bnat (S1 bn)
      -->
    dk_nat.S (dk_nat.mult dk_nat.2 (nat_of_bnat bn)).

succ : BNat -> BNat.
(; 0 + 1 = 2 * 0 + 1 ;)
[] succ O --> S1 O.
(; 2n + 1 = 2n + 1 ;)
[ n : BNat ] succ (S0 n) --> S1 n
(; 2n + 1 + 1 = 2 (n+1) ;)
[ n : BNat ] succ (S1 n) --> S0 (succ n).

bnat_of_nat : UNat -> BNat.
[] bnat_of_nat dk_nat.O --> O
[ n : UNat ] bnat_of_nat (dk_nat.S n) --> succ (bnat_of_nat n).

(; Order ;)
lt : BNat -> BNat -> Bool.
gt : BNat -> BNat -> Bool.
leq : BNat -> BNat -> Bool.
geq : BNat -> BNat -> Bool.

[ n : BNat ] lt n O --> dk_bool.false
[ m : BNat ] lt O m --> dk_bool.true
[ n : BNat, m : BNat ] lt (S0 n) (S0 m) --> lt n m
[ n : BNat, m : BNat ] lt (S0 n) (S1 m) --> leq n m
[ n : BNat, m : BNat ] lt (S1 n) (S0 m) --> lt n m
[ n : BNat, m : BNat ] lt (S1 n) (S1 m) --> lt n m.

[ n : BNat, m : BNat ] gt n m --> lt m n.

[ m : BNat ] leq O m --> dk_bool.true
[ n : BNat ] leq n O --> dk_bool.false
[ n : BNat, m : BNat ] leq (S0 n) (S0 m) --> leq n m
[ n : BNat, m : BNat ] leq (S0 n) (S1 m) --> leq n m
[ n : BNat, m : BNat ] leq (S1 n) (S0 m) --> lt n m
[ n : BNat, m : BNat ] leq (S1 n) (S1 m) --> leq n m.

[ n : BNat, m : BNat ] geq n m --> leq m n.

(; Equality ;)
eq : BNat -> BNat -> Bool.
[ n : BNat, m : BNat ] eq n m
      --> dk_bool.and (leq n m) (geq n m).

(; Operations ;)

(; Addition ;)
plus : BNat -> BNat -> BNat.
[ m : BNat ] plus O m --> m
[ n : BNat ] plus n O --> n
[ n : BNat, m : BNat ] plus (S0 n) (S0 m) --> S0 (plus n m)
[ n : BNat, m : BNat ] plus (S0 n) (S1 m) --> S1 (plus n m)
[ n : BNat, m : BNat ] plus (S1 n) (S0 m) --> S1 (plus n m)
[ n : BNat, m : BNat ] plus (S1 n) (S1 m) --> S0 (succ (plus n m)).

(; Product ;)
mult : BNat -> BNat -> BNat.
[ m : BNat ] mult O m --> O
[ n : BNat ] mult n O --> O
[ n : BNat, m : BNat ] mult (S0 n) (S0 m) --> S0 (S0 (mult n m))
[ n : BNat, m : BNat ] mult (S0 n) (S1 m) --> S0 (plus m (S0 (mult n m)))
[ n : BNat, m : BNat ] mult (S1 n) (S0 m) --> S0 (plus n (S0 (mult n m)))
[ n : BNat, m : BNat ] mult (S1 n) (S1 m) --> S1 (plus (S0 (mult m n)) (plus n m)).

(; Min and Max ;)
max : BNat -> BNat -> BNat.
[ m : BNat, n : BNat ]
    max m n --> dk_bool.ite bNat (leq m n) n m.

min : BNat -> BNat -> BNat.
[ m : BNat, n : BNat ]
    min m n --> dk_bool.ite bNat (leq m n) m n.

(; Euclidian division ;)
(; by a power of 2 ;)
div2 : BNat -> BNat.
[] div2 O --> O
[ n : BNat ] div2 (S0 n) --> n
[ n : BNat ] div2 (S1 n) --> n.

length : BNat -> UNat.
[] length O --> dk_nat.O
[ n : BNat ] length (S0 n) --> dk_nat.S (length n)
[ n : BNat ] length (S1 n) --> dk_nat.S (length n).

(; quo2 n k = n / 2^k ;)
quo2 : BNat -> UNat -> BNat.
[ n : BNat ] quo2 n dk_nat.O --> n
[ k : UNat ] quo2 O k --> O
[ n : BNat, k : UNat ]
    quo2 (S0 n) (dk_nat.S k) --> quo2 n k
[ n : BNat, k : UNat ]
    quo2 (S1 n) (dk_nat.S k) --> quo2 n k.

(; mod2 n k = n % 2^k ;)
mod2 : BNat -> UNat -> BNat.
[ n : BNat ] mod2 n dk_nat.O --> O
[ k : UNat ] mod2 O k --> O
[ n : BNat, k : UNat ]
    mod2 (S0 n) (dk_nat.S k) --> S0 (mod2 n k)
[ n : BNat, k : UNat ]
    mod2 (S1 n) (dk_nat.S k) --> S1 (mod2 n k).