dk_int.dk

#NAME dk_int.
def Nat : Type := dk_nat.Nat.
def O : Nat := dk_nat.O.
def S : Nat -> Nat := dk_nat.S.

def B : Type := cc.eT dk_bool.bool.

(; integers are defined by couples of naturals seen as their difference modulo the rule
   S n - S m --> n - m
 ;)
int : cc.uT.
def I : Type := cc.eT int.
(; the only constructor of Int, make n m builds the integer n - m ;)
def make : Nat -> Nat -> I.
(;
thanks to this rule, intergers reduce to one of the three following normal form :
 make O O which is 0
or
 make (S n) O which is n+1
or
 make O (S n) which is -n-1
;)
[n,m] make (dk_nat.S n) (dk_nat.S m) --> make n m.

def nat_abs : I -> Nat.
[n] nat_abs (make n dk_nat.O) --> n
[m] nat_abs (make dk_nat.O m) --> m.

(; n - m <= p - q iff n + q <= m + p ;)
def leq : I -> I -> B.
[n,m,p,q]
    leq (make n m) (make p q)
      --> dk_nat.leq (dk_nat.plus n q) (dk_nat.plus m p).

(; n - m < p - q iff n + q < m + p ;)
def lt : I -> I -> B.
[n,m,p,q]
    lt (make n m) (make p q)
      --> dk_nat.lt (dk_nat.plus n q) (dk_nat.plus m p).

def geq : I -> I -> B.
[i,j] geq i j --> leq j i.

def gt : I -> I -> B.
[i,j] gt i j --> lt j i.

def eq : I -> I -> B.
[i,j] eq i j --> dk_bool.and (leq i j) (geq i j).

(; (n - m) + (p - q) = (n + p) - (m + q) ;)
def plus : I -> I -> I.
[n,m,p,q]
    plus (make n m) (make p q)
      --> make (dk_nat.plus n p) (dk_nat.plus m q).

def opp : I -> I.
[n,m] opp (make n m) --> make m n.

def sub : I -> I -> I.
[i,j] sub i j --> plus i (opp j).

def mult : I -> I -> I.
[n,m,p,q]
    mult (make n m) (make p q)
      --> make
         (dk_nat.plus (dk_nat.mult n p) (dk_nat.mult m q))
         (dk_nat.plus (dk_nat.mult n q) (dk_nat.mult m p)).

def max : I -> I -> I.
[m,n] max m n --> dk_bool.ite int (leq m n) n m.

def min : I -> I -> I.
[m,n] min m n --> dk_bool.ite int (leq m n) m n.

def abs : I -> I.
[i] abs i --> make (nat_abs i) O.

def mod : I -> I -> I.
[n,m,p]
    mod (make m n) (make p dk_nat.O)
      --> make (dk_nat.mod m p) (dk_nat.mod n p)
[n,m,p]
    mod (make m n) (make dk_nat.O p)
      --> make (dk_nat.mod m p) (dk_nat.mod n p).

def quo : I -> I -> I.
[m,p]
    quo (make m dk_nat.O) (make p dk_nat.O)
      --> make (dk_nat.quo m p) O
[m,p]
    quo (make dk_nat.O m) (make dk_nat.O p)
      --> make (dk_nat.quo m p) O
[m,p]
    quo (make dk_nat.O m) (make p dk_nat.O)
      --> make O (dk_nat.quo m p)
[m,p]
    quo (make m dk_nat.O) (make dk_nat.O p)
      --> make O (dk_nat.quo m p).