BinPosDef: a module with all code about positive, later Included in BinPos

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14101 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 583 insertions, 543 deletions

diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 26754690a..67d193a6d 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -11,6 +11,8 @@ Require Export BinNums.
 Require Import Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid
  Equalities Orders GenericMinMax Le Plus Wf_nat.
 
+Require Export BinPosDef.
+
 (**********************************************************************)
 (** * Binary positive numbers, operations and properties *)
 (**********************************************************************)
@@ -20,17 +22,6 @@ Require Import Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid
 (** The type [positive] and its constructors [xI] and [xO] and [xH]
     are now defined in [BinNums.v] *)
 
-(** 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.
 Local Unset Boolean Equality Schemes.
 Local Unset Case Analysis Schemes.
@@ -43,543 +34,17 @@ Module Pos
  <: UsualDecidableTypeFull
  <: TotalOrder.
 
-Definition t := positive.
-Definition eq := @Logic.eq t.
-Definition eq_equiv := @eq_equivalence t.
-Include BackportEq.
-
-(** * 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.
-
-(** ** Division by 2 rounded below but for 1 *)
-
-Definition div2 p :=
-  match p with
-    | 1 => 1
-    | p~0 => p
-    | p~1 => p
-  end.
+(** * The definitions of operations are now in a separate file *)
 
-(** 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 lt x y := (x ?= y) = Lt.
-Definition gt x y := (x ?= y) = Gt.
-Definition le x y := (x ?= y) <> Gt.
-Definition ge x y := (x ?= y) <> Lt.
-
-Infix "<=" := le : positive_scope.
-Infix "<" := lt : positive_scope.
-Infix ">=" := ge : positive_scope.
-Infix ">" := gt : positive_scope.
-
-Notation "x <= y <= z" := (x <= y /\ y <= z) : positive_scope.
-Notation "x <= y < z" := (x <= y /\ y < z) : positive_scope.
-Notation "x < y < z" := (x < y /\ y < z) : positive_scope.
-Notation "x < y <= z" := (x < y /\ y <= z) : 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 *)
-
-(** Nota: this [eqb] is not convertible with the generated [positive_beq], due
-    to a different guard argument. We keep this version for compatibility. *)
-
-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, p*r = q.
-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. *)
+Include BinPosDef.Pos.
 
+(* TODO : fix the location of iter_nat *)
 Definition shiftl_nat (p:positive)(n:nat) := iter_nat n _ xO p.
-
 Definition shiftr_nat (p:positive)(n:nat) := iter_nat 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.
-
-(* Another version that converts [n] into [n+1] *)
-
-Fixpoint of_succ_nat (n:nat) : positive :=
-  match n with
-    | O => 1
-    | S x => succ (of_succ_nat x)
-  end.
-
+Definition eq := @Logic.eq t.
+Definition eq_equiv := @eq_equivalence t.
+Include BackportEq.
 
 (**********************************************************************)
 (** * Properties of operations over positive numbers *)
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v
new file mode 100644
index 000000000..10c882188
--- /dev/null
+++ b/theories/PArith/BinPosDef.v
@@ -0,0 +1,574 @@
+(* -*- coding: utf-8 -*- *)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(**********************************************************************)
+(** * 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.
+Local Unset Boolean Equality Schemes.
+Local Unset Case Analysis Schemes.
+
+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.
+
+(** ** 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 lt x y := (x ?= y) = Lt.
+Definition gt x y := (x ?= y) = Gt.
+Definition le x y := (x ?= y) <> Gt.
+Definition ge x y := (x ?= y) <> Lt.
+
+Infix "<=" := le : positive_scope.
+Infix "<" := lt : positive_scope.
+Infix ">=" := ge : positive_scope.
+Infix ">" := gt : positive_scope.
+
+Notation "x <= y <= z" := (x <= y /\ y <= z) : positive_scope.
+Notation "x <= y < z" := (x <= y /\ y < z) : positive_scope.
+Notation "x < y < z" := (x < y /\ y < z) : positive_scope.
+Notation "x < y <= z" := (x < y /\ y <= z) : 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 *)
+
+(** Nota: this [eqb] is not convertible with the generated [positive_beq], due
+    to a different guard argument. We keep this version for compatibility. *)
+
+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, p*r = q.
+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) := iter_nat n _ xO p.
+
+Definition shiftr_nat (p:positive)(n:nat) := iter_nat 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.
+
+(* Another version that converts [n] into [n+1] *)
+
+Fixpoint of_succ_nat (n:nat) : positive :=
+  match n with
+    | O => 1
+    | S x => succ (of_succ_nat x)
+  end.
+
+End Pos.
\ No newline at end of file
diff --git a/theories/PArith/vo.itarget b/theories/PArith/vo.itarget
index 390200515..73044e2c1 100644
--- a/theories/PArith/vo.itarget
+++ b/theories/PArith/vo.itarget
@@ -1,3 +1,4 @@
+BinPosDef.vo
 BinPos.vo
 Pnat.vo
 POrderedType.vo