Library Coq.PArith.BinPosDef


Binary positive numbers, operations

Initial development by Pierre Crégut, CNET, Lannion, France
The type positive and its constructors xI and xO and xH are now defined in BinNums.v

Require Export BinNums.

Postfix notation for positive numbers, allowing to mimic the position of bits in a big-endian representation. For instance, we can write 1~1~0 instead of (xO (xI xH)) for the number 6 (which is 110 in binary notation).

Notation "p ~ 1" := (xI p)
 (at level 7, left associativity, format "p '~' '1'") : positive_scope.
Notation "p ~ 0" := (xO p)
 (at level 7, left associativity, format "p '~' '0'") : positive_scope.

Local Open Scope positive_scope.
LocalLocal
Module Pos.

Definition t := positive.

Operations over positive numbers

Successor


Fixpoint succ x :=
  match x with
    | p~1 => (succ p)~0
    | p~0 => p~1
    | 1 => 1~0
  end.

Addition


Fixpoint add x y :=
  match x, y with
    | p~1, q~1 => (add_carry p q)~0
    | p~1, q~0 => (add p q)~1
    | p~1, 1 => (succ p)~0
    | p~0, q~1 => (add p q)~1
    | p~0, q~0 => (add p q)~0
    | p~0, 1 => p~1
    | 1, q~1 => (succ q)~0
    | 1, q~0 => q~1
    | 1, 1 => 1~0
  end

with add_carry x y :=
  match x, y with
    | p~1, q~1 => (add_carry p q)~1
    | p~1, q~0 => (add_carry p q)~0
    | p~1, 1 => (succ p)~1
    | p~0, q~1 => (add_carry p q)~0
    | p~0, q~0 => (add p q)~1
    | p~0, 1 => (succ p)~0
    | 1, q~1 => (succ q)~1
    | 1, q~0 => (succ q)~0
    | 1, 1 => 1~1
  end.

Infix "+" := add : positive_scope.

Operation x -> 2*x-1


Fixpoint pred_double x :=
  match x with
    | p~1 => p~0~1
    | p~0 => (pred_double p)~1
    | 1 => 1
  end.

Predecessor


Definition pred x :=
  match x with
    | p~1 => p~0
    | p~0 => pred_double p
    | 1 => 1
  end.

The predecessor of a positive number can be seen as a N


Definition pred_N x :=
  match x with
    | p~1 => Npos (p~0)
    | p~0 => Npos (pred_double p)
    | 1 => N0
  end.

An auxiliary type for subtraction


Inductive mask : Set :=
| IsNul : mask
| IsPos : positive -> mask
| IsNeg : mask.

Operation x -> 2*x+1


Definition succ_double_mask (x:mask) : mask :=
  match x with
    | IsNul => IsPos 1
    | IsNeg => IsNeg
    | IsPos p => IsPos p~1
  end.

Operation x -> 2*x


Definition double_mask (x:mask) : mask :=
  match x with
    | IsNul => IsNul
    | IsNeg => IsNeg
    | IsPos p => IsPos p~0
  end.

Operation x -> 2*x-2


Definition double_pred_mask x : mask :=
  match x with
    | p~1 => IsPos p~0~0
    | p~0 => IsPos (pred_double p)~0
    | 1 => IsNul
  end.

Predecessor with mask


Definition pred_mask (p : mask) : mask :=
  match p with
    | IsPos 1 => IsNul
    | IsPos q => IsPos (pred q)
    | IsNul => IsNeg
    | IsNeg => IsNeg
  end.

Subtraction, result as a mask


Fixpoint sub_mask (x y:positive) {struct y} : mask :=
  match x, y with
    | p~1, q~1 => double_mask (sub_mask p q)
    | p~1, q~0 => succ_double_mask (sub_mask p q)
    | p~1, 1 => IsPos p~0
    | p~0, q~1 => succ_double_mask (sub_mask_carry p q)
    | p~0, q~0 => double_mask (sub_mask p q)
    | p~0, 1 => IsPos (pred_double p)
    | 1, 1 => IsNul
    | 1, _ => IsNeg
  end

with sub_mask_carry (x y:positive) {struct y} : mask :=
  match x, y with
    | p~1, q~1 => succ_double_mask (sub_mask_carry p q)
    | p~1, q~0 => double_mask (sub_mask p q)
    | p~1, 1 => IsPos (pred_double p)
    | p~0, q~1 => double_mask (sub_mask_carry p q)
    | p~0, q~0 => succ_double_mask (sub_mask_carry p q)
    | p~0, 1 => double_pred_mask p
    | 1, _ => IsNeg
  end.

Subtraction, result as a positive, returning 1 if x<=y


Definition sub x y :=
  match sub_mask x y with
    | IsPos z => z
    | _ => 1
  end.

Infix "-" := sub : positive_scope.

Multiplication


Fixpoint mul x y :=
  match x with
    | p~1 => y + (mul p y)~0
    | p~0 => (mul p y)~0
    | 1 => y
  end.

Infix "*" := mul : positive_scope.

Iteration over a positive number


Fixpoint iter (n:positive) {A} (f:A -> A) (x:A) : A :=
  match n with
    | xH => f x
    | xO n´ => iter n´ f (iter n´ f x)
    | xI n´ => f (iter n´ f (iter n´ f x))
  end.

Power


Definition pow (x y:positive) := iter y (mul x) 1.

Infix "^" := pow : positive_scope.

Square


Fixpoint square p :=
  match p with
    | p~1 => (square p + p)~0~1
    | p~0 => (square p)~0~0
    | 1 => 1
  end.

Division by 2 rounded below but for 1


Definition div2 p :=
  match p with
    | 1 => 1
    | p~0 => p
    | p~1 => p
  end.

Division by 2 rounded up

Definition div2_up p :=
 match p with
   | 1 => 1
   | p~0 => p
   | p~1 => succ p
 end.

Number of digits in a positive number


Fixpoint size_nat p : nat :=
  match p with
    | 1 => S O
    | p~1 => S (size_nat p)
    | p~0 => S (size_nat p)
  end.

Same, with positive output

Fixpoint size p :=
  match p with
    | 1 => 1
    | p~1 => succ (size p)
    | p~0 => succ (size p)
  end.

Comparison on binary positive numbers


Fixpoint compare_cont (x y:positive) (r:comparison) {struct y} : comparison :=
  match x, y with
    | p~1, q~1 => compare_cont p q r
    | p~1, q~0 => compare_cont p q Gt
    | p~1, 1 => Gt
    | p~0, q~1 => compare_cont p q Lt
    | p~0, q~0 => compare_cont p q r
    | p~0, 1 => Gt
    | 1, q~1 => Lt
    | 1, q~0 => Lt
    | 1, 1 => r
  end.

Definition compare x y := compare_cont x y Eq.

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

Definition min p p´ :=
 match p ?= p´ with
 | Lt | Eq => p
 | Gt => p´
 end.

Definition max p p´ :=
 match p ?= p´ with
 | Lt | Eq => p´
 | Gt => p
 end.

Boolean equality and comparisons


Fixpoint eqb p q {struct q} :=
  match p, q with
    | p~1, q~1 => eqb p q
    | p~0, q~0 => eqb p q
    | 1, 1 => true
    | _, _ => false
  end.

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

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

Infix "=?" := eqb (at level 70, no associativity) : positive_scope.
Infix "<=?" := leb (at level 70, no associativity) : positive_scope.
Infix "<?" := ltb (at level 70, no associativity) : positive_scope.

A Square Root function for positive numbers

We procede by blocks of two digits : if p is written qbb' then sqrt(p) will be sqrt(q)~0 or sqrt(q)~1. For deciding easily in which case we are, we store the remainder (as a mask, since it can be null). Instead of copy-pasting the following code four times, we factorize as an auxiliary function, with f and g being either xO or xI depending of the initial digits. NB: (sub_mask (g (f 1)) 4) is a hack, morally it's g (f 0).

Definition sqrtrem_step (f g:positive->positive) p :=
 match p with
  | (s, IsPos r) =>
    let s´ := s~0~1 in
    let r´ := g (f r) in
    if s´ <=? r´ then (s~1, sub_mask r´ s´)
    else (s~0, IsPos r´)
  | (s,_) => (s~0, sub_mask (g (f 1)) 4)
 end.

Fixpoint sqrtrem p : positive * mask :=
 match p with
  | 1 => (1,IsNul)
  | 2 => (1,IsPos 1)
  | 3 => (1,IsPos 2)
  | p~0~0 => sqrtrem_step xO xO (sqrtrem p)
  | p~0~1 => sqrtrem_step xO xI (sqrtrem p)
  | p~1~0 => sqrtrem_step xI xO (sqrtrem p)
  | p~1~1 => sqrtrem_step xI xI (sqrtrem p)
 end.

Definition sqrt p := fst (sqrtrem p).

Greatest Common Divisor


Definition divide p q := exists r, q = r*p.
Notation "( p | q )" := (divide p q) (at level 0) : positive_scope.

Instead of the Euclid algorithm, we use here the Stein binary algorithm, which is faster for this representation. This algorithm is almost structural, but in the last cases we do some recursive calls on subtraction, hence the need for a counter.

Fixpoint gcdn (n : nat) (a b : positive) : positive :=
  match n with
    | O => 1
    | S n =>
      match a,b with
        | 1, _ => 1
        | _, 1 => 1
        | a~0, b~0 => (gcdn n a b)~0
        | _ , b~0 => gcdn n a b
        | a~0, _ => gcdn n a b
        | a´~1, b´~1 =>
          match a´ ?= b´ with
            | Eq => a
            | Lt => gcdn n (b´-a´) a
            | Gt => gcdn n (a´-b´) b
          end
      end
  end.

We'll show later that we need at most (log2(a.b)) loops

Definition gcd (a b : positive) := gcdn (size_nat a + size_nat b)%nat a b.

Generalized Gcd, also computing the division of a and b by the gcd

Fixpoint ggcdn (n : nat) (a b : positive) : (positive*(positive*positive)) :=
  match n with
    | O => (1,(a,b))
    | S n =>
      match a,b with
        | 1, _ => (1,(1,b))
        | _, 1 => (1,(a,1))
        | a~0, b~0 =>
           let (g,p) := ggcdn n a b in
           (g~0,p)
        | _, b~0 =>
           let ´(g,(aa,bb)) := ggcdn n a b in
           (g,(aa, bb~0))
        | a~0, _ =>
           let ´(g,(aa,bb)) := ggcdn n a b in
           (g,(aa~0, bb))
        | a´~1, b´~1 =>
           match a´ ?= b´ with
             | Eq => (a,(1,1))
             | Lt =>
                let ´(g,(ba,aa)) := ggcdn n (b´-a´) a in
                (g,(aa, aa + ba~0))
             | Gt =>
                let ´(g,(ab,bb)) := ggcdn n (a´-b´) b in
                (g,(bb + ab~0, bb))
           end
      end
  end.

Definition ggcd (a b: positive) := ggcdn (size_nat a + size_nat b)%nat a b.

Local copies of the not-yet-available N.double and N.succ_double

Definition Nsucc_double x :=
  match x with
  | N0 => Npos 1
  | Npos p => Npos p~1
  end.

Definition Ndouble n :=
  match n with
  | N0 => N0
  | Npos p => Npos p~0
  end.

Operation over bits.
Logical or

Fixpoint lor (p q : positive) : positive :=
  match p, q with
    | 1, q~0 => q~1
    | 1, _ => q
    | p~0, 1 => p~1
    | _, 1 => p
    | p~0, q~0 => (lor p q)~0
    | p~0, q~1 => (lor p q)~1
    | p~1, q~0 => (lor p q)~1
    | p~1, q~1 => (lor p q)~1
  end.

Logical and

Fixpoint land (p q : positive) : N :=
  match p, q with
    | 1, q~0 => N0
    | 1, _ => Npos 1
    | p~0, 1 => N0
    | _, 1 => Npos 1
    | p~0, q~0 => Ndouble (land p q)
    | p~0, q~1 => Ndouble (land p q)
    | p~1, q~0 => Ndouble (land p q)
    | p~1, q~1 => Nsucc_double (land p q)
  end.

Logical diff

Fixpoint ldiff (p q:positive) : N :=
  match p, q with
    | 1, q~0 => Npos 1
    | 1, _ => N0
    | _~0, 1 => Npos p
    | p~1, 1 => Npos (p~0)
    | p~0, q~0 => Ndouble (ldiff p q)
    | p~0, q~1 => Ndouble (ldiff p q)
    | p~1, q~1 => Ndouble (ldiff p q)
    | p~1, q~0 => Nsucc_double (ldiff p q)
  end.

xor

Fixpoint lxor (p q:positive) : N :=
  match p, q with
    | 1, 1 => N0
    | 1, q~0 => Npos (q~1)
    | 1, q~1 => Npos (q~0)
    | p~0, 1 => Npos (p~1)
    | p~0, q~0 => Ndouble (lxor p q)
    | p~0, q~1 => Nsucc_double (lxor p q)
    | p~1, 1 => Npos (p~0)
    | p~1, q~0 => Nsucc_double (lxor p q)
    | p~1, q~1 => Ndouble (lxor p q)
  end.

Shifts. NB: right shift of 1 stays at 1.

Definition shiftl_nat (p:positive)(n:nat) := nat_iter n xO p.
Definition shiftr_nat (p:positive)(n:nat) := nat_iter n div2 p.

Definition shiftl (p:positive)(n:N) :=
  match n with
    | N0 => p
    | Npos n => iter n xO p
  end.

Definition shiftr (p:positive)(n:N) :=
  match n with
    | N0 => p
    | Npos n => iter n div2 p
  end.

Checking whether a particular bit is set or not

Fixpoint testbit_nat (p:positive) : nat -> bool :=
  match p with
    | 1 => fun n => match n with
                      | O => true
                      | S _ => false
                    end
    | p~0 => fun n => match n with
                        | O => false
                        | S n´ => testbit_nat p n´
                      end
    | p~1 => fun n => match n with
                        | O => true
                        | S n´ => testbit_nat p n´
                      end
  end.

Same, but with index in N

Fixpoint testbit (p:positive)(n:N) :=
  match p, n with
    | p~0, N0 => false
    | _, N0 => true
    | 1, _ => false
    | p~0, Npos n => testbit p (pred_N n)
    | p~1, Npos n => testbit p (pred_N n)
  end.

From binary positive numbers to Peano natural numbers


Definition iter_op {A}(op:A->A->A) :=
  fix iter (p:positive)(a:A) : A :=
  match p with
    | 1 => a
    | p~0 => iter p (op a a)
    | p~1 => op a (iter p (op a a))
  end.

Definition to_nat (x:positive) : nat := iter_op plus x (S O).

From Peano natural numbers to binary positive numbers

A version preserving positive numbers, and sending 0 to 1.

Fixpoint of_nat (n:nat) : positive :=
 match n with
   | O => 1
   | S O => 1
   | S x => succ (of_nat x)
 end.


Fixpoint of_succ_nat (n:nat) : positive :=
  match n with
    | O => 1
    | S x => succ (of_succ_nat x)
  end.

End Pos.