BinNatDef containing all functions of BinNat, misc adaptations in BinPos

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

3 files changed, 375 insertions, 346 deletions

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index b1d62d776..7d9f4d64f 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -9,6 +9,7 @@
 Require Export BinNums.
 Require Import BinPos RelationClasses Morphisms Setoid
  Equalities GenericMinMax Wf_nat Bool NAxioms NProperties.
+Require BinNatDef.
 
 (**********************************************************************)
 (** * Binary natural numbers, operations and properties *)
@@ -17,7 +18,7 @@ Require Import BinPos RelationClasses Morphisms Setoid
 (** The type [N] and its constructors [N0] and [Npos] are now
     defined in [BinNums.v] *)
 
-(** Every definitions and early properties about binary natural numbers
+(** Every definitions and properties about binary natural numbers
     are placed in a module [N] for qualification purpose. *)
 
 Local Open Scope N_scope.
@@ -31,98 +32,18 @@ Module N
  <: UsualDecidableTypeFull
  <: TotalOrder.
 
-Definition t := N.
-Definition eq := @Logic.eq t.
-Definition eq_equiv := @eq_equivalence t.
-
-(** Operation [x -> 2*x+1] *)
-
-Definition succ_double x :=
-  match x with
-  | 0 => Npos 1
-  | Npos p => Npos p~1
-  end.
-
-(** Operation [x -> 2*x] *)
-
-Definition double n :=
-  match n with
-  | 0 => 0
-  | Npos p => Npos p~0
-  end.
-
-(** Successor *)
-
-Definition succ n :=
-  match n with
-  | 0 => 1
-  | Npos p => Npos (Pos.succ p)
-  end.
-
-(** Predecessor *)
-
-Definition pred n :=
-  match n with
-  | 0 => 0
-  | Npos p => Pos.pred_N p
-  end.
-
-(** The successor of a N can be seen as a positive *)
-
-Definition succ_pos (n : N) : positive :=
- match n with
-   | N0 => 1%positive
-   | Npos p => Pos.succ p
- end.
-
-(** Addition *)
-
-Definition add n m :=
-  match n, m with
-  | 0, _ => m
-  | _, 0 => n
-  | Npos p, Npos q => Npos (p + q)
-  end.
-
-Infix "+" := add : N_scope.
+(** Definitions of operations, now in a separate file *)
 
-(** Subtraction *)
+Include BinNatDef.N.
 
-Definition sub n m :=
-match n, m with
-| 0, _ => 0
-| n, 0 => n
-| Npos n', Npos m' =>
-  match Pos.sub_mask n' m' with
-  | IsPos p => Npos p
-  | _ => 0
-  end
-end.
-
-Infix "-" := sub : N_scope.
-
-(** Multiplication *)
-
-Definition mul n m :=
-  match n, m with
-  | 0, _ => 0
-  | _, 0 => 0
-  | Npos p, Npos q => Npos (p * q)
-  end.
-
-Infix "*" := mul : N_scope.
-
-(** Order *)
+(* TODO : fix the location of iter_nat *)
+Definition shiftl_nat (a:N)(n:nat) := iter_nat n _ double a.
+Definition shiftr_nat (a:N)(n:nat) := iter_nat n _ div2 a.
 
-Definition compare n m :=
-  match n, m with
-  | 0, 0 => Eq
-  | 0, Npos m' => Lt
-  | Npos n', 0 => Gt
-  | Npos n', Npos m' => (n' ?= m')%positive
-  end.
+(** Logical predicates *)
 
-Infix "?=" := compare (at level 70, no associativity) : N_scope.
+Definition eq := @Logic.eq t.
+Definition eq_equiv := @eq_equivalence t.
 
 Definition lt x y := (x ?= y) = Lt.
 Definition gt x y := (x ?= y) = Gt.
@@ -139,258 +60,11 @@ Notation "x <= y < z" := (x <= y /\ y < z) : N_scope.
 Notation "x < y < z" := (x < y /\ y < z) : N_scope.
 Notation "x < y <= z" := (x < y /\ y <= z) : N_scope.
 
-(** Boolean equality and comparison *)
-
-(** Nota: this [eqb] is not convertible with the generated [N_beq],
-    since the underlying [Pos.eqb] differs from [positive_beq]
-    (cf BinIntDef). *)
-
-Fixpoint eqb n m :=
-  match n, m with
-    | 0, 0 => true
-    | Npos p, Npos q => Pos.eqb p q
-    | _, _ => 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) : N_scope.
-Infix "<=?" := leb (at level 70, no associativity) : N_scope.
-Infix "<?" := ltb (at level 70, no associativity) : N_scope.
-
-(** Min and max *)
-
-Definition min n n' := match n ?= n' with
- | Lt | Eq => n
- | Gt => n'
- end.
-
-Definition max n n' := match n ?= n' with
- | Lt | Eq => n'
- | Gt => n
- end.
-
-(** Dividing by 2 *)
-
-Definition div2 n :=
-  match n with
-  | 0 => 0
-  | Npos 1 => 0
-  | Npos (p~0) => Npos p
-  | Npos (p~1) => Npos p
-  end.
-
-(** Parity *)
-
-Definition even n :=
-  match n with
-    | 0 => true
-    | Npos (xO _) => true
-    | _ => false
-  end.
-
-Definition odd n := negb (even n).
-
-(** Power *)
-
-Definition pow n p :=
-  match p, n with
-    | 0, _ => Npos 1
-    | _, 0 => 0
-    | Npos p, Npos q => Npos (q^p)
-  end.
-
-Infix "^" := pow : N_scope.
-
-(** Base-2 logarithm *)
-
-Definition log2 n :=
- match n with
-   | 0 => 0
-   | Npos 1 => 0
-   | Npos (p~0) => Npos (Pos.size p)
-   | Npos (p~1) => Npos (Pos.size p)
- end.
-
-(** How many digits in a number ?
-    Number 0 is said to have no digits at all.
-*)
-
-Definition size n :=
- match n with
-  | 0 => 0
-  | Npos p => Npos (Pos.size p)
- end.
-
-Definition size_nat n :=
- match n with
-  | 0 => O
-  | Npos p => Pos.size_nat p
- end.
-
-(** Euclidean division *)
-
-Fixpoint pos_div_eucl (a:positive)(b:N) : N * N :=
-  match a with
-    | xH =>
-       match b with 1 => (1,0) | _ => (0,1) end
-    | xO a' =>
-       let (q, r) := pos_div_eucl a' b in
-       let r' := double r in
-       if b <=? r' then (succ_double q, r' - b)
-        else (double q, r')
-    | xI a' =>
-       let (q, r) := pos_div_eucl a' b in
-       let r' := succ_double r in
-       if b <=? r' then (succ_double q, r' - b)
-        else  (double q, r')
-  end.
-
-Definition div_eucl (a b:N) : N * N :=
-  match a, b with
-   | 0,  _ => (0, 0)
-   | _, 0  => (0, a)
-   | Npos na, _ => pos_div_eucl na b
-  end.
-
-Definition div a b := fst (div_eucl a b).
-Definition modulo a b := snd (div_eucl a b).
-
-Infix "/" := div : N_scope.
-Infix "mod" := modulo (at level 40, no associativity) : N_scope.
-
-(** Greatest common divisor *)
-
 Definition divide p q := exists r, p*r = q.
-
 Notation "( p | q )" := (divide p q) (at level 0) : N_scope.
 
-Definition gcd a b :=
- match a, b with
-  | 0, _ => b
-  | _, 0 => a
-  | Npos p, Npos q => Npos (Pos.gcd p q)
- end.
-
-(** Generalized Gcd, also computing rests of [a] and [b] after
-    division by gcd. *)
-
-Definition ggcd a b :=
- match a, b with
-  | 0, _ => (b,(0,1))
-  | _, 0 => (a,(1,0))
-  | Npos p, Npos q =>
-     let '(g,(aa,bb)) := Pos.ggcd p q in
-     (Npos g, (Npos aa, Npos bb))
- end.
-
-(** Square root *)
-
-Definition sqrtrem n :=
- match n with
-  | 0 => (0, 0)
-  | Npos p =>
-    match Pos.sqrtrem p with
-     | (s, IsPos r) => (Npos s, Npos r)
-     | (s, _) => (Npos s, 0)
-    end
- end.
-
-Definition sqrt n :=
- match n with
-  | 0 => 0
-  | Npos p => Npos (Pos.sqrt p)
- end.
-
-(** Operation over bits of a [N] number. *)
-
-(** Logical [or] *)
-
-Definition lor n m :=
- match n, m with
-   | 0, _ => m
-   | _, 0 => n
-   | Npos p, Npos q => Npos (Pos.lor p q)
- end.
-
-(** Logical [and] *)
-
-Definition land n m :=
- match n, m with
-  | 0, _ => 0
-  | _, 0 => 0
-  | Npos p, Npos q => Pos.land p q
- end.
-
-(** Logical [diff] *)
-
-Fixpoint ldiff n m :=
- match n, m with
-  | 0, _ => 0
-  | _, 0 => n
-  | Npos p, Npos q => Pos.ldiff p q
- end.
-
-(** [xor] *)
-
-Definition lxor n m :=
-  match n, m with
-    | 0, _ => m
-    | _, 0 => n
-    | Npos p, Npos q => Pos.lxor p q
-  end.
-
-(** Shifts *)
-
-Definition shiftl_nat (a:N)(n:nat) := iter_nat n _ double a.
-
-Definition shiftr_nat (a:N)(n:nat) := iter_nat n _ div2 a.
-
-Definition shiftl a n :=
-  match a with
-    | 0 => 0
-    | Npos a => Npos (Pos.shiftl a n)
-  end.
-
-Definition shiftr a n :=
-  match n with
-    | 0 => a
-    | Npos p => Pos.iter p div2 a
-  end.
-
-(** Checking whether a particular bit is set or not *)
-
-Definition testbit_nat (a:N) :=
-  match a with
-    | 0 => fun _ => false
-    | Npos p => Pos.testbit_nat p
-  end.
-
-(** Same, but with index in N *)
-
-Definition testbit a n :=
-  match a with
-    | 0 => false
-    | Npos p => Pos.testbit p n
-  end.
-
-(** Translation from [N] to [nat] and back. *)
-
-Definition to_nat (a:N) :=
-  match a with
-  | N0 => O
-  | Npos p => Pos.to_nat p
-  end.
-
-Definition of_nat (n:nat) :=
-  match n with
-  | O => 0
-  | S n' => Npos (Pos.of_succ_nat n')
-  end.
+Definition Even n := exists m, n = 2*m.
+Definition Odd n := exists m, n = 2*m+1.
 
 (** Decidability of equality. *)
 
@@ -863,9 +537,6 @@ Qed.
 
 (** Specification of parity functions *)
 
-Definition Even n := exists m, n = 2*m.
-Definition Odd n := exists m, n = 2*m+1.
-
 Lemma even_spec n : even n = true <-> Even n.
 Proof.
  destruct n.
@@ -1220,11 +891,7 @@ Proof.
  apply pos_ldiff_spec.
 Qed.
 
-(** Some constants *)
-
-Definition zero := 0.
-Definition one := 1.
-Definition two := 2.
+(** Specification of constants *)
 
 Lemma one_succ : 1 = succ 0.
 Proof. reflexivity. Qed.
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
new file mode 100644
index 000000000..cb5cfe7f0
--- /dev/null
+++ b/theories/NArith/BinNatDef.v
@@ -0,0 +1,361 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+Require Export BinNums.
+Require Import BinPos.
+Local Open Scope N_scope.
+
+(**********************************************************************)
+(** * Binary natural numbers, definitions of operations *)
+(**********************************************************************)
+
+Module N.
+
+Definition t := N.
+
+(** ** Constants *)
+
+Definition zero := 0.
+Definition one := 1.
+Definition two := 2.
+
+(** ** Operation [x -> 2*x+1] *)
+
+Definition succ_double x :=
+  match x with
+  | 0 => 1
+  | Npos p => Npos p~1
+  end.
+
+(** ** Operation [x -> 2*x] *)
+
+Definition double n :=
+  match n with
+  | 0 => 0
+  | Npos p => Npos p~0
+  end.
+
+(** ** Successor *)
+
+Definition succ n :=
+  match n with
+  | 0 => 1
+  | Npos p => Npos (Pos.succ p)
+  end.
+
+(** ** Predecessor *)
+
+Definition pred n :=
+  match n with
+  | 0 => 0
+  | Npos p => Pos.pred_N p
+  end.
+
+(** ** The successor of a [N] can be seen as a [positive] *)
+
+Definition succ_pos (n : N) : positive :=
+ match n with
+   | N0 => 1%positive
+   | Npos p => Pos.succ p
+ end.
+
+(** ** Addition *)
+
+Definition add n m :=
+  match n, m with
+  | 0, _ => m
+  | _, 0 => n
+  | Npos p, Npos q => Npos (p + q)
+  end.
+
+Infix "+" := add : N_scope.
+
+(** Subtraction *)
+
+Definition sub n m :=
+match n, m with
+| 0, _ => 0
+| n, 0 => n
+| Npos n', Npos m' =>
+  match Pos.sub_mask n' m' with
+  | IsPos p => Npos p
+  | _ => 0
+  end
+end.
+
+Infix "-" := sub : N_scope.
+
+(** Multiplication *)
+
+Definition mul n m :=
+  match n, m with
+  | 0, _ => 0
+  | _, 0 => 0
+  | Npos p, Npos q => Npos (p * q)
+  end.
+
+Infix "*" := mul : N_scope.
+
+(** Order *)
+
+Definition compare n m :=
+  match n, m with
+  | 0, 0 => Eq
+  | 0, Npos m' => Lt
+  | Npos n', 0 => Gt
+  | Npos n', Npos m' => (n' ?= m')%positive
+  end.
+
+Infix "?=" := compare (at level 70, no associativity) : N_scope.
+
+(** Boolean equality and comparison *)
+
+(** Nota: this [eqb] is not convertible with the generated [N_beq],
+    since the underlying [Pos.eqb] differs from [positive_beq]
+    (cf BinIntDef). *)
+
+Fixpoint eqb n m :=
+  match n, m with
+    | 0, 0 => true
+    | Npos p, Npos q => Pos.eqb p q
+    | _, _ => 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) : N_scope.
+Infix "<=?" := leb (at level 70, no associativity) : N_scope.
+Infix "<?" := ltb (at level 70, no associativity) : N_scope.
+
+(** Min and max *)
+
+Definition min n n' := match n ?= n' with
+ | Lt | Eq => n
+ | Gt => n'
+ end.
+
+Definition max n n' := match n ?= n' with
+ | Lt | Eq => n'
+ | Gt => n
+ end.
+
+(** Dividing by 2 *)
+
+Definition div2 n :=
+  match n with
+  | 0 => 0
+  | 1 => 0
+  | Npos (p~0) => Npos p
+  | Npos (p~1) => Npos p
+  end.
+
+(** Parity *)
+
+Definition even n :=
+  match n with
+    | 0 => true
+    | Npos (xO _) => true
+    | _ => false
+  end.
+
+Definition odd n := negb (even n).
+
+(** Power *)
+
+Definition pow n p :=
+  match p, n with
+    | 0, _ => 1
+    | _, 0 => 0
+    | Npos p, Npos q => Npos (q^p)
+  end.
+
+Infix "^" := pow : N_scope.
+
+(** Base-2 logarithm *)
+
+Definition log2 n :=
+ match n with
+   | 0 => 0
+   | 1 => 0
+   | Npos (p~0) => Npos (Pos.size p)
+   | Npos (p~1) => Npos (Pos.size p)
+ end.
+
+(** How many digits in a number ?
+    Number 0 is said to have no digits at all.
+*)
+
+Definition size n :=
+ match n with
+  | 0 => 0
+  | Npos p => Npos (Pos.size p)
+ end.
+
+Definition size_nat n :=
+ match n with
+  | 0 => O
+  | Npos p => Pos.size_nat p
+ end.
+
+(** Euclidean division *)
+
+Fixpoint pos_div_eucl (a:positive)(b:N) : N * N :=
+  match a with
+    | xH =>
+       match b with 1 => (1,0) | _ => (0,1) end
+    | xO a' =>
+       let (q, r) := pos_div_eucl a' b in
+       let r' := double r in
+       if b <=? r' then (succ_double q, r' - b)
+        else (double q, r')
+    | xI a' =>
+       let (q, r) := pos_div_eucl a' b in
+       let r' := succ_double r in
+       if b <=? r' then (succ_double q, r' - b)
+        else  (double q, r')
+  end.
+
+Definition div_eucl (a b:N) : N * N :=
+  match a, b with
+   | 0,  _ => (0, 0)
+   | _, 0  => (0, a)
+   | Npos na, _ => pos_div_eucl na b
+  end.
+
+Definition div a b := fst (div_eucl a b).
+Definition modulo a b := snd (div_eucl a b).
+
+Infix "/" := div : N_scope.
+Infix "mod" := modulo (at level 40, no associativity) : N_scope.
+
+(** Greatest common divisor *)
+
+Definition gcd a b :=
+ match a, b with
+  | 0, _ => b
+  | _, 0 => a
+  | Npos p, Npos q => Npos (Pos.gcd p q)
+ end.
+
+(** Generalized Gcd, also computing rests of [a] and [b] after
+    division by gcd. *)
+
+Definition ggcd a b :=
+ match a, b with
+  | 0, _ => (b,(0,1))
+  | _, 0 => (a,(1,0))
+  | Npos p, Npos q =>
+     let '(g,(aa,bb)) := Pos.ggcd p q in
+     (Npos g, (Npos aa, Npos bb))
+ end.
+
+(** Square root *)
+
+Definition sqrtrem n :=
+ match n with
+  | 0 => (0, 0)
+  | Npos p =>
+    match Pos.sqrtrem p with
+     | (s, IsPos r) => (Npos s, Npos r)
+     | (s, _) => (Npos s, 0)
+    end
+ end.
+
+Definition sqrt n :=
+ match n with
+  | 0 => 0
+  | Npos p => Npos (Pos.sqrt p)
+ end.
+
+(** Operation over bits of a [N] number. *)
+
+(** Logical [or] *)
+
+Definition lor n m :=
+ match n, m with
+   | 0, _ => m
+   | _, 0 => n
+   | Npos p, Npos q => Npos (Pos.lor p q)
+ end.
+
+(** Logical [and] *)
+
+Definition land n m :=
+ match n, m with
+  | 0, _ => 0
+  | _, 0 => 0
+  | Npos p, Npos q => Pos.land p q
+ end.
+
+(** Logical [diff] *)
+
+Fixpoint ldiff n m :=
+ match n, m with
+  | 0, _ => 0
+  | _, 0 => n
+  | Npos p, Npos q => Pos.ldiff p q
+ end.
+
+(** [xor] *)
+
+Definition lxor n m :=
+  match n, m with
+    | 0, _ => m
+    | _, 0 => n
+    | Npos p, Npos q => Pos.lxor p q
+  end.
+
+(** Shifts *)
+
+Definition shiftl a n :=
+  match a with
+    | 0 => 0
+    | Npos a => Npos (Pos.shiftl a n)
+  end.
+
+Definition shiftr a n :=
+  match n with
+    | 0 => a
+    | Npos p => Pos.iter p div2 a
+  end.
+
+(** Checking whether a particular bit is set or not *)
+
+Definition testbit_nat (a:N) :=
+  match a with
+    | 0 => fun _ => false
+    | Npos p => Pos.testbit_nat p
+  end.
+
+(** Same, but with index in N *)
+
+Definition testbit a n :=
+  match a with
+    | 0 => false
+    | Npos p => Pos.testbit p n
+  end.
+
+(** Translation from [N] to [nat] and back. *)
+
+Definition to_nat (a:N) :=
+  match a with
+  | 0 => O
+  | Npos p => Pos.to_nat p
+  end.
+
+Definition of_nat (n:nat) :=
+  match n with
+  | O => 0
+  | S n' => Npos (Pos.of_succ_nat n')
+  end.
+
+End N.
\ No newline at end of file
diff --git a/theories/NArith/vo.itarget b/theories/NArith/vo.itarget
index 3e285772d..e76033f78 100644
--- a/theories/NArith/vo.itarget
+++ b/theories/NArith/vo.itarget
@@ -1,3 +1,4 @@
+BinNatDef.vo
 BinNat.vo
 NArith.vo
 Ndec.vo