Library Coq.ZArith.BinIntDef


Require Export BinNums.
Require Import BinPos BinNat.

Local Open Scope Z_scope.

Binary Integers, Definitions of Operations

Initial author: Pierre Crégut, CNET, Lannion, France

Module Z.

Definition t := Z.

Constants


Definition zero := 0.
Definition one := 1.
Definition two := 2.

Doubling and variants


Definition double x :=
  match x with
    | 0 => 0
    | Zpos p => Zpos p~0
    | Zneg p => Zneg p~0
  end.

Definition succ_double x :=
  match x with
    | 0 => 1
    | Zpos p => Zpos p~1
    | Zneg p => Zneg (Pos.pred_double p)
  end.

Definition pred_double x :=
  match x with
    | 0 => -1
    | Zneg p => Zneg p~1
    | Zpos p => Zpos (Pos.pred_double p)
  end.

Subtraction of positive into Z


Fixpoint pos_sub (x y:positive) {struct y} : Z :=
  match x, y with
    | p~1, q~1 => double (pos_sub p q)
    | p~1, q~0 => succ_double (pos_sub p q)
    | p~1, 1 => Zpos p~0
    | p~0, q~1 => pred_double (pos_sub p q)
    | p~0, q~0 => double (pos_sub p q)
    | p~0, 1 => Zpos (Pos.pred_double p)
    | 1, q~1 => Zneg q~0
    | 1, q~0 => Zneg (Pos.pred_double q)
    | 1, 1 => Z0
  end%positive.

Addition


Definition add x y :=
  match x, y with
    | 0, y => y
    | x, 0 => x
    | Zpos x', Zpos y' => Zpos (x' + y')
    | Zpos x', Zneg y' => pos_sub x' y'
    | Zneg x', Zpos y' => pos_sub y' x'
    | Zneg x', Zneg y' => Zneg (x' + y')
  end.

Infix "+" := add : Z_scope.

Opposite


Definition opp x :=
  match x with
    | 0 => 0
    | Zpos x => Zneg x
    | Zneg x => Zpos x
  end.

Notation "- x" := (opp x) : Z_scope.

Successor


Definition succ x := x + 1.

Predecessor


Definition pred x := x + -1.

Subtraction


Definition sub m n := m + -n.

Infix "-" := sub : Z_scope.

Multiplication


Definition mul x y :=
  match x, y with
    | 0, _ => 0
    | _, 0 => 0
    | Zpos x', Zpos y' => Zpos (x' * y')
    | Zpos x', Zneg y' => Zneg (x' * y')
    | Zneg x', Zpos y' => Zneg (x' * y')
    | Zneg x', Zneg y' => Zpos (x' * y')
  end.

Infix "*" := mul : Z_scope.

Power function


Definition pow_pos (z:Z) (n:positive) := Pos.iter n (mul z) 1.

Definition pow x y :=
  match y with
    | Zpos p => pow_pos x p
    | 0 => 1
    | Zneg _ => 0
  end.

Infix "^" := pow : Z_scope.

Square


Definition square x :=
  match x with
    | 0 => 0
    | Zpos p => Zpos (Pos.square p)
    | Zneg p => Zpos (Pos.square p)
  end.

Comparison


Definition compare x y :=
  match x, y with
    | 0, 0 => Eq
    | 0, Zpos y' => Lt
    | 0, Zneg y' => Gt
    | Zpos x', 0 => Gt
    | Zpos x', Zpos y' => (x' ?= y')%positive
    | Zpos x', Zneg y' => Gt
    | Zneg x', 0 => Lt
    | Zneg x', Zpos y' => Lt
    | Zneg x', Zneg y' => CompOpp ((x' ?= y')%positive)
  end.

Infix "?=" := compare (at level 70, no associativity) : Z_scope.

Sign function


Definition sgn z :=
  match z with
    | 0 => 0
    | Zpos p => 1
    | Zneg p => -1
  end.

Boolean equality and comparisons

Definition leb x y :=
  match x ?= y with
    | Gt => false
    | _ => true
  end.

Definition ltb x y :=
  match x ?= y with
    | Lt => true
    | _ => false
  end.

Nota: geb and gtb are provided for compatibility, but leb and ltb should rather be used instead, since more results we be available on them.

Definition geb x y :=
  match x ?= y with
    | Lt => false
    | _ => true
  end.

Definition gtb x y :=
  match x ?= y with
    | Gt => true
    | _ => false
  end.

Nota: this eqb is not convertible with the generated Z_beq, since the underlying Pos.eqb differs from positive_beq (cf BinIntDef).

Fixpoint eqb x y :=
  match x, y with
    | 0, 0 => true
    | Zpos p, Zpos q => Pos.eqb p q
    | Zneg p, Zneg q => Pos.eqb p q
    | _, _ => false
  end.

Infix "=?" := eqb (at level 70, no associativity) : Z_scope.
Infix "<=?" := leb (at level 70, no associativity) : Z_scope.
Infix "<?" := ltb (at level 70, no associativity) : Z_scope.
Infix ">=?" := geb (at level 70, no associativity) : Z_scope.
Infix ">?" := gtb (at level 70, no associativity) : Z_scope.

Minimum and maximum


Definition max n m :=
  match n ?= m with
    | Eq | Gt => n
    | Lt => m
  end.

Definition min n m :=
  match n ?= m with
    | Eq | Lt => n
    | Gt => m
  end.

Absolute value


Definition abs z :=
  match z with
    | 0 => 0
    | Zpos p => Zpos p
    | Zneg p => Zpos p
  end.

Conversions

From Z to nat via absolute value

Definition abs_nat (z:Z) : nat :=
  match z with
    | 0 => 0%nat
    | Zpos p => Pos.to_nat p
    | Zneg p => Pos.to_nat p
  end.

From Z to N via absolute value

Definition abs_N (z:Z) : N :=
  match z with
    | Z0 => 0%N
    | Zpos p => Npos p
    | Zneg p => Npos p
  end.

From Z to nat by rounding negative numbers to 0

Definition to_nat (z:Z) : nat :=
  match z with
    | Zpos p => Pos.to_nat p
    | _ => O
  end.

From Z to N by rounding negative numbers to 0

Definition to_N (z:Z) : N :=
  match z with
    | Zpos p => Npos p
    | _ => 0%N
  end.

From nat to Z

Definition of_nat (n:nat) : Z :=
  match n with
   | O => 0
   | S n => Zpos (Pos.of_succ_nat n)
  end.

From N to Z

Definition of_N (n:N) : Z :=
  match n with
    | N0 => 0
    | Npos p => Zpos p
  end.

Iteration of a function

By convention, iterating a negative number of times is identity.

Definition iter (n:Z) {A} (f:A -> A) (x:A) :=
  match n with
    | Zpos p => Pos.iter p f x
    | _ => x
  end.

Euclidean divisions for binary integers

Concerning the many possible variants of integer divisions, see the headers of the generic files ZDivFloor, ZDivTrunc, ZDivEucl, and the article by R. Boute mentioned there. We provide here two flavours, Floor and Trunc, while the Euclid convention can be found in file Zeuclid.v For non-zero b, they all satisfy a = b*(a/b) + (a mod b) and |a mod b| < |b| , but the sign of the modulo will differ when a<0 and/or b<0.

Floor division

div_eucl provides a Truncated-Toward-Bottom (a.k.a Floor) Euclidean division. Its projections are named div (noted "/") and modulo (noted with an infix "mod"). These functions correspond to the `div` and `mod` of Haskell. This is the historical convention of Coq.
The main properties of this convention are :
  • we have sgn (a mod b) = sgn (b)
  • div a b is the greatest integer smaller or equal to the exact fraction a/b.
  • there is no easy sign rule.
In addition, note that we arbitrary take a/0 = 0 and a mod 0 = 0.
First, a division for positive numbers. Even if the second argument is a Z, the answer is arbitrary is it isn't a Zpos.

Fixpoint pos_div_eucl (a:positive) (b:Z) : Z * Z :=
  match a with
    | xH => if 2 <=? b then (0, 1) else (1, 0)
    | xO a' =>
      let (q, r) := pos_div_eucl a' b in
      let r' := 2 * r in
      if r' <? b then (2 * q, r') else (2 * q + 1, r' - b)
    | xI a' =>
      let (q, r) := pos_div_eucl a' b in
      let r' := 2 * r + 1 in
      if r' <? b then (2 * q, r') else (2 * q + 1, r' - b)
  end.

Then the general euclidean division

Definition div_eucl (a b:Z) : Z * Z :=
  match a, b with
    | 0, _ => (0, 0)
    | _, 0 => (0, 0)
    | Zpos a', Zpos _ => pos_div_eucl a' b
    | Zneg a', Zpos _ =>
      let (q, r) := pos_div_eucl a' b in
        match r with
          | 0 => (- q, 0)
          | _ => (- (q + 1), b - r)
        end
    | Zneg a', Zneg b' =>
      let (q, r) := pos_div_eucl a' (Zpos b') in (q, - r)
    | Zpos a', Zneg b' =>
      let (q, r) := pos_div_eucl a' (Zpos b') in
        match r with
          | 0 => (- q, 0)
          | _ => (- (q + 1), b + r)
        end
  end.

Definition div (a b:Z) : Z := let (q, _) := div_eucl a b in q.
Definition modulo (a b:Z) : Z := let (_, r) := div_eucl a b in r.

Infix "/" := div : Z_scope.
Infix "mod" := modulo (at level 40, no associativity) : Z_scope.

Trunc Division

quotrem provides a Truncated-Toward-Zero Euclidean division. Its projections are named quot (noted "÷") and rem. These functions correspond to the `quot` and `rem` of Haskell. This division convention is used in most programming languages, e.g. Ocaml.
With this convention:
  • we have sgn(a rem b) = sgn(a)
  • sign rule for division: quot (-a) b = quot a (-b) = -(quot a b)
  • and for modulo: a rem (-b) = a rem b and (-a) rem b = -(a rem b)
Note that we arbitrary take here quot a 0 = 0 and a rem 0 = a.

Definition quotrem (a b:Z) : Z * Z :=
  match a, b with
   | 0, _ => (0, 0)
   | _, 0 => (0, a)
   | Zpos a, Zpos b =>
     let (q, r) := N.pos_div_eucl a (Npos b) in (of_N q, of_N r)
   | Zneg a, Zpos b =>
     let (q, r) := N.pos_div_eucl a (Npos b) in (-of_N q, - of_N r)
   | Zpos a, Zneg b =>
     let (q, r) := N.pos_div_eucl a (Npos b) in (-of_N q, of_N r)
   | Zneg a, Zneg b =>
     let (q, r) := N.pos_div_eucl a (Npos b) in (of_N q, - of_N r)
  end.

Definition quot a b := fst (quotrem a b).
Definition rem a b := snd (quotrem a b).

Infix "÷" := quot (at level 40, left associativity) : Z_scope.
No infix notation for rem, otherwise it becomes a keyword

Parity functions


Definition even z :=
  match z with
    | 0 => true
    | Zpos (xO _) => true
    | Zneg (xO _) => true
    | _ => false
  end.

Definition odd z :=
  match z with
    | 0 => false
    | Zpos (xO _) => false
    | Zneg (xO _) => false
    | _ => true
  end.

Division by two

div2 performs rounding toward bottom, it is hence a particular case of div, and for all relative number n we have: n = 2 * div2 n + if odd n then 1 else 0.

Definition div2 z :=
 match z with
   | 0 => 0
   | Zpos 1 => 0
   | Zpos p => Zpos (Pos.div2 p)
   | Zneg p => Zneg (Pos.div2_up p)
 end.

quot2 performs rounding toward zero, it is hence a particular case of quot, and for all relative number n we have: n = 2 * quot2 n + if odd n then sgn n else 0.

Definition quot2 (z:Z) :=
  match z with
    | 0 => 0
    | Zpos 1 => 0
    | Zpos p => Zpos (Pos.div2 p)
    | Zneg 1 => 0
    | Zneg p => Zneg (Pos.div2 p)
  end.

NB: Z.quot2 used to be named Zdiv2 in Coq <= 8.3

Base-2 logarithm


Definition log2 z :=
  match z with
    | Zpos (p~1) => Zpos (Pos.size p)
    | Zpos (p~0) => Zpos (Pos.size p)
    | _ => 0
  end.

Square root


Definition sqrtrem n :=
 match n with
  | 0 => (0, 0)
  | Zpos p =>
    match Pos.sqrtrem p with
     | (s, IsPos r) => (Zpos s, Zpos r)
     | (s, _) => (Zpos s, 0)
    end
  | Zneg _ => (0,0)
 end.

Definition sqrt n :=
 match n with
  | Zpos p => Zpos (Pos.sqrt p)
  | _ => 0
 end.

Greatest Common Divisor


Definition gcd a b :=
  match a,b with
    | 0, _ => abs b
    | _, 0 => abs a
    | Zpos a, Zpos b => Zpos (Pos.gcd a b)
    | Zpos a, Zneg b => Zpos (Pos.gcd a b)
    | Zneg a, Zpos b => Zpos (Pos.gcd a b)
    | Zneg a, Zneg b => Zpos (Pos.gcd a b)
  end.

A generalized gcd, also computing division of a and b by gcd.

Definition ggcd a b : Z*(Z*Z) :=
  match a,b with
    | 0, _ => (abs b,(0, sgn b))
    | _, 0 => (abs a,(sgn a, 0))
    | Zpos a, Zpos b =>
       let '(g,(aa,bb)) := Pos.ggcd a b in (Zpos g, (Zpos aa, Zpos bb))
    | Zpos a, Zneg b =>
       let '(g,(aa,bb)) := Pos.ggcd a b in (Zpos g, (Zpos aa, Zneg bb))
    | Zneg a, Zpos b =>
       let '(g,(aa,bb)) := Pos.ggcd a b in (Zpos g, (Zneg aa, Zpos bb))
    | Zneg a, Zneg b =>
       let '(g,(aa,bb)) := Pos.ggcd a b in (Zpos g, (Zneg aa, Zneg bb))
  end.

Bitwise functions

When accessing the bits of negative numbers, all functions below will use the two's complement representation. For instance, -1 will correspond to an infinite stream of true bits. If this isn't what you're looking for, you can use abs first and then access the bits of the absolute value.
testbit : accessing the n-th bit of a number a. For negative n, we arbitrarily answer false.

Definition testbit a n :=
 match n with
   | 0 => odd a
   | Zpos p =>
     match a with
       | 0 => false
       | Zpos a => Pos.testbit a (Npos p)
       | Zneg a => negb (N.testbit (Pos.pred_N a) (Npos p))
     end
   | Zneg _ => false
 end.

Shifts
Nota: a shift to the right by -n will be a shift to the left by n, and vice-versa.
For fulfilling the two's complement convention, shifting to the right a negative number should correspond to a division by 2 with rounding toward bottom, hence the use of div2 instead of quot2.

Definition shiftl a n :=
 match n with
   | 0 => a
   | Zpos p => Pos.iter p (mul 2) a
   | Zneg p => Pos.iter p div2 a
 end.

Definition shiftr a n := shiftl a (-n).

Bitwise operations lor land ldiff lxor

Definition lor a b :=
 match a, b with
   | 0, _ => b
   | _, 0 => a
   | Zpos a, Zpos b => Zpos (Pos.lor a b)
   | Zneg a, Zpos b => Zneg (N.succ_pos (N.ldiff (Pos.pred_N a) (Npos b)))
   | Zpos a, Zneg b => Zneg (N.succ_pos (N.ldiff (Pos.pred_N b) (Npos a)))
   | Zneg a, Zneg b => Zneg (N.succ_pos (N.land (Pos.pred_N a) (Pos.pred_N b)))
 end.

Definition land a b :=
 match a, b with
   | 0, _ => 0
   | _, 0 => 0
   | Zpos a, Zpos b => of_N (Pos.land a b)
   | Zneg a, Zpos b => of_N (N.ldiff (Npos b) (Pos.pred_N a))
   | Zpos a, Zneg b => of_N (N.ldiff (Npos a) (Pos.pred_N b))
   | Zneg a, Zneg b => Zneg (N.succ_pos (N.lor (Pos.pred_N a) (Pos.pred_N b)))
 end.

Definition ldiff a b :=
 match a, b with
   | 0, _ => 0
   | _, 0 => a
   | Zpos a, Zpos b => of_N (Pos.ldiff a b)
   | Zneg a, Zpos b => Zneg (N.succ_pos (N.lor (Pos.pred_N a) (Npos b)))
   | Zpos a, Zneg b => of_N (N.land (Npos a) (Pos.pred_N b))
   | Zneg a, Zneg b => of_N (N.ldiff (Pos.pred_N b) (Pos.pred_N a))
 end.

Definition lxor a b :=
 match a, b with
   | 0, _ => b
   | _, 0 => a
   | Zpos a, Zpos b => of_N (Pos.lxor a b)
   | Zneg a, Zpos b => Zneg (N.succ_pos (N.lxor (Pos.pred_N a) (Npos b)))
   | Zpos a, Zneg b => Zneg (N.succ_pos (N.lxor (Npos a) (Pos.pred_N b)))
   | Zneg a, Zneg b => of_N (N.lxor (Pos.pred_N a) (Pos.pred_N b))
 end.

End Z.