Deletion of useless Zdigits_def

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

10 files changed, 95 insertions, 432 deletions

diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index cb16e1291e..0142b36bef 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -678,17 +678,17 @@ Module Make (N:NType) <: ZType.
   destruct (norm_pos x) as [x'|x'];
    specialize (H x' (eq_refl _)) || clear H.
 
- Lemma spec_testbit: forall x p, testbit x p = Ztestbit (to_Z x) (to_Z p).
+ Lemma spec_testbit: forall x p, testbit x p = Z.testbit (to_Z x) (to_Z p).
  Proof.
   intros x p. unfold testbit.
   destr_norm_pos p; simpl. destr_norm_pos x; simpl.
   apply N.spec_testbit.
   rewrite N.spec_testbit, N.spec_pred, Zmax_r by auto with zarith.
   symmetry. apply Z.bits_opp. apply N.spec_pos.
-  symmetry. apply Ztestbit_neg_r; auto with zarith.
+  symmetry. apply Z.testbit_neg_r; auto with zarith.
  Qed.
 
- Lemma spec_shiftl: forall x p, to_Z (shiftl x p) = Zshiftl (to_Z x) (to_Z p).
+ Lemma spec_shiftl: forall x p, to_Z (shiftl x p) = Z.shiftl (to_Z x) (to_Z p).
  Proof.
   intros x p. unfold shiftl.
   destr_norm_pos x; destruct p as [p|p]; simpl;
@@ -703,13 +703,13 @@ Module Make (N:NType) <: ZType.
   now rewrite Zlnot_alt1, Z.lnot_shiftr, Zlnot_alt2.
  Qed.
 
- Lemma spec_shiftr: forall x p, to_Z (shiftr x p) = Zshiftr (to_Z x) (to_Z p).
+ Lemma spec_shiftr: forall x p, to_Z (shiftr x p) = Z.shiftr (to_Z x) (to_Z p).
  Proof.
   intros. unfold shiftr. rewrite spec_shiftl, spec_opp.
   apply Z.shiftl_opp_r.
  Qed.
 
- Lemma spec_land: forall x y, to_Z (land x y) = Zand (to_Z x) (to_Z y).
+ Lemma spec_land: forall x y, to_Z (land x y) = Z.land (to_Z x) (to_Z y).
  Proof.
   intros x y. unfold land.
   destr_norm_pos x; destr_norm_pos y; simpl;
@@ -720,7 +720,7 @@ Module Make (N:NType) <: ZType.
   now rewrite Z.lnot_lor, !Zlnot_alt2.
  Qed.
 
- Lemma spec_lor: forall x y, to_Z (lor x y) = Zor (to_Z x) (to_Z y).
+ Lemma spec_lor: forall x y, to_Z (lor x y) = Z.lor (to_Z x) (to_Z y).
  Proof.
   intros x y. unfold lor.
   destr_norm_pos x; destr_norm_pos y; simpl;
@@ -731,7 +731,7 @@ Module Make (N:NType) <: ZType.
   now rewrite Z.lnot_land, !Zlnot_alt2.
  Qed.
 
- Lemma spec_ldiff: forall x y, to_Z (ldiff x y) = Zdiff (to_Z x) (to_Z y).
+ Lemma spec_ldiff: forall x y, to_Z (ldiff x y) = Z.ldiff (to_Z x) (to_Z y).
  Proof.
   intros x y. unfold ldiff.
   destr_norm_pos x; destr_norm_pos y; simpl;
@@ -742,7 +742,7 @@ Module Make (N:NType) <: ZType.
   now rewrite 2 Z.ldiff_land, Zlnot_alt2, Z.land_comm, Zlnot_alt3.
  Qed.
 
- Lemma spec_lxor: forall x y, to_Z (lxor x y) = Zxor (to_Z x) (to_Z y).
+ Lemma spec_lxor: forall x y, to_Z (lxor x y) = Z.lxor (to_Z x) (to_Z y).
  Proof.
   intros x y. unfold lxor.
   destr_norm_pos x; destr_norm_pos y; simpl;
@@ -753,9 +753,9 @@ Module Make (N:NType) <: ZType.
   now rewrite <- Z.lxor_lnot_lnot, !Zlnot_alt2.
  Qed.
 
- Lemma spec_div2: forall x, to_Z (div2 x) = Zdiv2 (to_Z x).
+ Lemma spec_div2: forall x, to_Z (div2 x) = Z.div2 (to_Z x).
  Proof.
-  intros x. unfold div2. now rewrite spec_shiftr, Zdiv2_spec, spec_1.
+  intros x. unfold div2. now rewrite spec_shiftr, Z.div2_spec, spec_1.
  Qed.
 
 End Make.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index f409285669..eaab13c2ad 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -445,77 +445,77 @@ Program Instance testbit_wd : Proper (eq==>eq==>Logic.eq) testbit.
 
 Lemma testbit_odd_0 : forall a, testbit (2*a+1) 0 = true.
 Proof.
- intros. zify. apply Ztestbit_odd_0.
+ intros. zify. apply Z.testbit_odd_0.
 Qed.
 
 Lemma testbit_even_0 : forall a, testbit (2*a) 0 = false.
 Proof.
- intros. zify. apply Ztestbit_even_0.
+ intros. zify. apply Z.testbit_even_0.
 Qed.
 
 Lemma testbit_odd_succ : forall a n, 0<=n ->
  testbit (2*a+1) (succ n) = testbit a n.
 Proof.
- intros a n. zify. apply Ztestbit_odd_succ.
+ intros a n. zify. apply Z.testbit_odd_succ.
 Qed.
 
 Lemma testbit_even_succ : forall a n, 0<=n ->
  testbit (2*a) (succ n) = testbit a n.
 Proof.
- intros a n. zify. apply Ztestbit_even_succ.
+ intros a n. zify. apply Z.testbit_even_succ.
 Qed.
 
 Lemma testbit_neg_r : forall a n, n<0 -> testbit a n = false.
 Proof.
- intros a n. zify. apply Ztestbit_neg_r.
+ intros a n. zify. apply Z.testbit_neg_r.
 Qed.
 
 Lemma shiftr_spec : forall a n m, 0<=m ->
  testbit (shiftr a n) m = testbit a (m+n).
 Proof.
- intros a n m. zify. apply Zshiftr_spec.
+ intros a n m. zify. apply Z.shiftr_spec.
 Qed.
 
 Lemma shiftl_spec_high : forall a n m, 0<=m -> n<=m ->
  testbit (shiftl a n) m = testbit a (m-n).
 Proof.
  intros a n m. zify. intros Hn H.
- now apply Zshiftl_spec_high.
+ now apply Z.shiftl_spec_high.
 Qed.
 
 Lemma shiftl_spec_low : forall a n m, m<n ->
  testbit (shiftl a n) m = false.
 Proof.
- intros a n m. zify. intros H. now apply Zshiftl_spec_low.
+ intros a n m. zify. intros H. now apply Z.shiftl_spec_low.
 Qed.
 
 Lemma land_spec : forall a b n,
  testbit (land a b) n = testbit a n && testbit b n.
 Proof.
- intros a n m. zify. now apply Zand_spec.
+ intros a n m. zify. now apply Z.land_spec.
 Qed.
 
 Lemma lor_spec : forall a b n,
  testbit (lor a b) n = testbit a n || testbit b n.
 Proof.
- intros a n m. zify. now apply Zor_spec.
+ intros a n m. zify. now apply Z.lor_spec.
 Qed.
 
 Lemma ldiff_spec : forall a b n,
  testbit (ldiff a b) n = testbit a n && negb (testbit b n).
 Proof.
- intros a n m. zify. now apply Zdiff_spec.
+ intros a n m. zify. now apply Z.ldiff_spec.
 Qed.
 
 Lemma lxor_spec : forall a b n,
  testbit (lxor a b) n = xorb (testbit a n) (testbit b n).
 Proof.
- intros a n m. zify. now apply Zxor_spec.
+ intros a n m. zify. now apply Z.lxor_spec.
 Qed.
 
 Lemma div2_spec : forall a, div2 a == shiftr a 1.
 Proof.
- intros a. zify. now apply Zdiv2_spec.
+ intros a. zify. now apply Z.div2_spec.
 Qed.
 
 End ZTypeIsZAxioms.
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index 64b8ec844d..a6eb6ae470 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -1330,7 +1330,7 @@ Module Make (W0:CyclicType) <: NType.
   generalize (ZnZ.spec_to_Z d); auto with zarith.
  Qed.
 
- Lemma spec_shiftr: forall x p, [shiftr x p] = Zshiftr [x] [p].
+ Lemma spec_shiftr: forall x p, [shiftr x p] = Z.shiftr [x] [p].
  Proof.
   intros.
   now rewrite spec_shiftr_pow2, Z.shiftr_div_pow2 by apply spec_pos.
@@ -1603,7 +1603,7 @@ Module Make (W0:CyclicType) <: NType.
  apply Zpower_le_monotone2; auto with zarith.
  Qed.
 
- Lemma spec_shiftl: forall x p, [shiftl x p] = Zshiftl [x] [p].
+ Lemma spec_shiftl: forall x p, [shiftl x p] = Z.shiftl [x] [p].
  Proof.
   intros.
   now rewrite spec_shiftl_pow2, Z.shiftl_mul_pow2 by apply spec_pos.
@@ -1613,7 +1613,7 @@ Module Make (W0:CyclicType) <: NType.
 
  Definition testbit x n := odd (shiftr x n).
 
- Lemma spec_testbit: forall x p, testbit x p = Ztestbit [x] [p].
+ Lemma spec_testbit: forall x p, testbit x p = Z.testbit [x] [p].
  Proof.
   intros. unfold testbit. symmetry.
   rewrite spec_odd, spec_shiftr. apply Z.testbit_odd.
@@ -1621,42 +1621,42 @@ Module Make (W0:CyclicType) <: NType.
 
  Definition div2 x := shiftr x one.
 
- Lemma spec_div2: forall x, [div2 x] = Zdiv2 [x].
+ Lemma spec_div2: forall x, [div2 x] = Z.div2 [x].
  Proof.
   intros. unfold div2. symmetry.
-  rewrite spec_shiftr, spec_1. apply Zdiv2_spec.
+  rewrite spec_shiftr, spec_1. apply Z.div2_spec.
  Qed.
 
  (** TODO : provide efficient versions instead of just converting
    from/to N (see with Laurent) *)
 
- Definition lor x y := of_N (Nor (to_N x) (to_N y)).
- Definition land x y := of_N (Nand (to_N x) (to_N y)).
- Definition ldiff x y := of_N (Ndiff (to_N x) (to_N y)).
- Definition lxor x y := of_N (Nxor (to_N x) (to_N y)).
+ Definition lor x y := of_N (N.lor (to_N x) (to_N y)).
+ Definition land x y := of_N (N.land (to_N x) (to_N y)).
+ Definition ldiff x y := of_N (N.ldiff (to_N x) (to_N y)).
+ Definition lxor x y := of_N (N.lxor (to_N x) (to_N y)).
 
- Lemma spec_land: forall x y, [land x y] = Zand [x] [y].
+ Lemma spec_land: forall x y, [land x y] = Z.land [x] [y].
  Proof.
   intros x y. unfold land. rewrite spec_of_N. unfold to_N.
   generalize (spec_pos x), (spec_pos y).
   destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2).
  Qed.
 
- Lemma spec_lor: forall x y, [lor x y] = Zor [x] [y].
+ Lemma spec_lor: forall x y, [lor x y] = Z.lor [x] [y].
  Proof.
   intros x y. unfold lor. rewrite spec_of_N. unfold to_N.
   generalize (spec_pos x), (spec_pos y).
   destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2).
  Qed.
 
- Lemma spec_ldiff: forall x y, [ldiff x y] = Zdiff [x] [y].
+ Lemma spec_ldiff: forall x y, [ldiff x y] = Z.ldiff [x] [y].
  Proof.
   intros x y. unfold ldiff. rewrite spec_of_N. unfold to_N.
   generalize (spec_pos x), (spec_pos y).
   destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2).
  Qed.
 
- Lemma spec_lxor: forall x y, [lxor x y] = Zxor [x] [y].
+ Lemma spec_lxor: forall x y, [lxor x y] = Z.lxor [x] [y].
  Proof.
   intros x y. unfold lxor. rewrite spec_of_N. unfold to_N.
   generalize (spec_pos x), (spec_pos y).
diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v
index 94f6b32fd8..dec8f1fe4d 100644
--- a/theories/Numbers/Natural/BigN/Nbasic.v
+++ b/theories/Numbers/Natural/BigN/Nbasic.v
@@ -23,6 +23,19 @@ Implicit Arguments mk_zn2z_specs_karatsuba [t ops].
 Implicit Arguments ZnZ.digits [t].
 Implicit Arguments ZnZ.zdigits [t].
 
+Lemma Pshiftl_nat_Zpower : forall n p,
+  Zpos (Pos.shiftl_nat p n) = Zpos p * 2 ^ Z.of_nat n.
+Proof.
+ intros.
+ rewrite Z.mul_comm.
+ induction n. simpl; auto.
+ transitivity (2 * (2 ^ Z.of_nat n * Zpos p)).
+ rewrite <- IHn. auto.
+ rewrite Z.mul_assoc.
+ rewrite inj_S.
+ rewrite <- Z.pow_succ_r; auto with zarith.
+Qed.
+
 (* To compute the necessary height *)
 
 Fixpoint plength (p: positive) : positive :=
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 225c0853ec..a1f4ea9a26 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -11,7 +11,7 @@ Require Import ZArith OrdersFacts Nnat Ndigits NAxioms NDiv NSig.
 
 (** * The interface [NSig.NType] implies the interface [NAxiomsSig] *)
 
-Module NTypeIsNAxioms (Import N : NType').
+Module NTypeIsNAxioms (Import NN : NType').
 
 Hint Rewrite
  spec_0 spec_1 spec_2 spec_succ spec_add spec_mul spec_pred spec_sub
@@ -54,7 +54,7 @@ Definition N_of_Z z := of_N (Zabs_N z).
 
 Section Induction.
 
-Variable A : N.t -> Prop.
+Variable A : NN.t -> Prop.
 Hypothesis A_wd : Proper (eq==>iff) A.
 Hypothesis A0 : A 0.
 Hypothesis AS : forall n, A n <-> A (succ n).
@@ -161,7 +161,7 @@ Proof.
  intros. zify. apply Z.compare_antisym.
 Qed.
 
-Include BoolOrderFacts N N N [no inline].
+Include BoolOrderFacts NN NN NN [no inline].
 
 Instance compare_wd : Proper (eq ==> eq ==> Logic.eq) compare.
 Proof.
@@ -371,83 +371,83 @@ Program Instance testbit_wd : Proper (eq==>eq==>Logic.eq) testbit.
 
 Lemma testbit_odd_0 : forall a, testbit (2*a+1) 0 = true.
 Proof.
- intros. zify. apply Ztestbit_odd_0.
+ intros. zify. apply Z.testbit_odd_0.
 Qed.
 
 Lemma testbit_even_0 : forall a, testbit (2*a) 0 = false.
 Proof.
- intros. zify. apply Ztestbit_even_0.
+ intros. zify. apply Z.testbit_even_0.
 Qed.
 
 Lemma testbit_odd_succ : forall a n, 0<=n ->
  testbit (2*a+1) (succ n) = testbit a n.
 Proof.
- intros a n. zify. apply Ztestbit_odd_succ.
+ intros a n. zify. apply Z.testbit_odd_succ.
 Qed.
 
 Lemma testbit_even_succ : forall a n, 0<=n ->
  testbit (2*a) (succ n) = testbit a n.
 Proof.
- intros a n. zify. apply Ztestbit_even_succ.
+ intros a n. zify. apply Z.testbit_even_succ.
 Qed.
 
 Lemma testbit_neg_r : forall a n, n<0 -> testbit a n = false.
 Proof.
- intros a n. zify. apply Ztestbit_neg_r.
+ intros a n. zify. apply Z.testbit_neg_r.
 Qed.
 
 Lemma shiftr_spec : forall a n m, 0<=m ->
  testbit (shiftr a n) m = testbit a (m+n).
 Proof.
- intros a n m. zify. apply Zshiftr_spec.
+ intros a n m. zify. apply Z.shiftr_spec.
 Qed.
 
 Lemma shiftl_spec_high : forall a n m, 0<=m -> n<=m ->
  testbit (shiftl a n) m = testbit a (m-n).
 Proof.
- intros a n m. zify. intros Hn H. rewrite Zmax_r by auto with zarith.
- now apply Zshiftl_spec_high.
+ intros a n m. zify. intros Hn H. rewrite Z.max_r by auto with zarith.
+ now apply Z.shiftl_spec_high.
 Qed.
 
 Lemma shiftl_spec_low : forall a n m, m<n ->
  testbit (shiftl a n) m = false.
 Proof.
- intros a n m. zify. intros H. now apply Zshiftl_spec_low.
+ intros a n m. zify. intros H. now apply Z.shiftl_spec_low.
 Qed.
 
 Lemma land_spec : forall a b n,
  testbit (land a b) n = testbit a n && testbit b n.
 Proof.
- intros a n m. zify. now apply Zand_spec.
+ intros a n m. zify. now apply Z.land_spec.
 Qed.
 
 Lemma lor_spec : forall a b n,
  testbit (lor a b) n = testbit a n || testbit b n.
 Proof.
- intros a n m. zify. now apply Zor_spec.
+ intros a n m. zify. now apply Z.lor_spec.
 Qed.
 
 Lemma ldiff_spec : forall a b n,
  testbit (ldiff a b) n = testbit a n && negb (testbit b n).
 Proof.
- intros a n m. zify. now apply Zdiff_spec.
+ intros a n m. zify. now apply Z.ldiff_spec.
 Qed.
 
 Lemma lxor_spec : forall a b n,
  testbit (lxor a b) n = xorb (testbit a n) (testbit b n).
 Proof.
- intros a n m. zify. now apply Zxor_spec.
+ intros a n m. zify. now apply Z.lxor_spec.
 Qed.
 
 Lemma div2_spec : forall a, div2 a == shiftr a 1.
 Proof.
- intros a. zify. now apply Zdiv2_spec.
+ intros a. zify. now apply Z.div2_spec.
 Qed.
 
 (** Recursion *)
 
-Definition recursion (A : Type) (a : A) (f : N.t -> A -> A) (n : N.t) :=
-  Nrect (fun _ => A) a (fun n a => f (N.of_N n) a) (N.to_N n).
+Definition recursion (A : Type) (a : A) (f : NN.t -> A -> A) (n : NN.t) :=
+  Nrect (fun _ => A) a (fun n a => f (NN.of_N n) a) (NN.to_N n).
 Implicit Arguments recursion [A].
 
 Instance recursion_wd (A : Type) (Aeq : relation A) :
@@ -456,7 +456,7 @@ Proof.
 unfold eq.
 intros a a' Eaa' f f' Eff' x x' Exx'.
 unfold recursion.
-unfold N.to_N.
+unfold NN.to_N.
 rewrite <- Exx'; clear x' Exx'.
 replace (Zabs_N [x]) with (N_of_nat (Zabs_nat [x])).
 induction (Zabs_nat [x]).
@@ -468,30 +468,30 @@ change (nat_of_P p) with (nat_of_N (Npos p)); apply N_of_nat_of_N.
 Qed.
 
 Theorem recursion_0 :
-  forall (A : Type) (a : A) (f : N.t -> A -> A), recursion a f 0 = a.
+  forall (A : Type) (a : A) (f : NN.t -> A -> A), recursion a f 0 = a.
 Proof.
-intros A a f; unfold recursion, N.to_N; rewrite N.spec_0; simpl; auto.
+intros A a f; unfold recursion, NN.to_N; rewrite NN.spec_0; simpl; auto.
 Qed.
 
 Theorem recursion_succ :
-  forall (A : Type) (Aeq : relation A) (a : A) (f : N.t -> A -> A),
+  forall (A : Type) (Aeq : relation A) (a : A) (f : NN.t -> A -> A),
     Aeq a a -> Proper (eq==>Aeq==>Aeq) f ->
       forall n, Aeq (recursion a f (succ n)) (f n (recursion a f n)).
 Proof.
-unfold N.eq, recursion; intros A Aeq a f EAaa f_wd n.
-replace (N.to_N (succ n)) with (Nsucc (N.to_N n)).
+unfold NN.eq, recursion; intros A Aeq a f EAaa f_wd n.
+replace (NN.to_N (succ n)) with (N.succ (NN.to_N n)).
 rewrite Nrect_step.
 apply f_wd; auto.
-unfold N.to_N.
-rewrite N.spec_of_N, Z_of_N_abs, Zabs_eq; auto.
- apply N.spec_pos.
+unfold NN.to_N.
+rewrite NN.spec_of_N, Z_of_N_abs, Zabs_eq; auto.
+ apply NN.spec_pos.
 
 fold (recursion a f n).
 apply recursion_wd; auto.
 red; auto.
-unfold N.to_N.
+unfold NN.to_N.
 
-rewrite N.spec_succ.
+rewrite NN.spec_succ.
 change ([n]+1)%Z with (Zsucc [n]).
 apply Z_of_N_eq_rev.
 rewrite Z_of_N_succ.
@@ -503,6 +503,6 @@ Qed.
 
 End NTypeIsNAxioms.
 
-Module NType_NAxioms (N : NType)
- <: NAxiomsSig <: OrderFunctions N <: HasMinMax N
- := N <+ NTypeIsNAxioms.
+Module NType_NAxioms (NN : NType)
+ <: NAxiomsSig <: OrderFunctions NN <: HasMinMax NN
+ := NN <+ NTypeIsNAxioms.
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 379e68544a..9e559b68cf 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -992,12 +992,7 @@ Proof.
   rewrite ?Pos.pred_N_succ; now destruct n.
 Qed.
 
-Lemma div2_of_N n : of_N (N.div2 n) = div2 (of_N n).
-Proof.
- now destruct n as [|[ | | ]].
-Qed.
-
-(** Correctness proofs about [Zshiftr] and [Zshiftl] *)
+(** Correctness proofs about [Z.shiftr] and [Z.shiftl] *)
 
 Lemma shiftr_spec_aux a n m : 0<=n -> 0<=m ->
  testbit (shiftr a n) m = testbit a (m+n).
@@ -1016,7 +1011,7 @@ Proof.
  now rewrite 2 testbit_0_l.
  (* a > 0 *)
  change (Zpos a) with (of_N (Npos a)) at 1.
- rewrite <- (Pos.iter_swap_gen _ _ _ Ndiv2) by exact div2_of_N.
+ rewrite <- (Pos.iter_swap_gen _ _ _ Ndiv2) by now intros [|[ | | ]].
  rewrite testbit_Zpos, testbit_of_N', H; trivial.
  exact (N.shiftr_spec' (Npos a) (Npos n) (to_N m)).
  (* a < 0 *)
@@ -1155,23 +1150,6 @@ Proof.
  now rewrite N.lxor_spec, xorb_negb_negb.
 Qed.
 
-(** An additionnal proof concerning [Pos.shiftl_nat], used in BigN *)
-
-Lemma pos_shiftl_nat_pow n p :
-  Zpos (Pos.shiftl_nat p n) = Zpos p * 2 ^ Z.of_nat n.
-Proof.
- intros.
- rewrite mul_comm.
- induction n. simpl; auto.
- transitivity (2 * (2 ^ Z.of_nat n * Zpos p)).
- rewrite <- IHn. auto.
- rewrite mul_assoc.
- replace (of_nat (S n)) with (succ (of_nat n)).
- rewrite <- pow_succ_r. trivial.
- now destruct n.
- destruct n. trivial. simpl. now rewrite Pos.add_1_r.
-Qed.
-
 (** ** Induction principles based on successor / predecessor *)
 
 Lemma peano_ind (P : Z -> Prop) :
diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v
index abd735de5a..265e62f065 100644
--- a/theories/ZArith/ZArith.v
+++ b/theories/ZArith/ZArith.v
@@ -12,7 +12,7 @@ Require Export ZArith_base.
 
 (** Extra definitions *)
 
-Require Export Zpow_def Zdigits_def.
+Require Export Zpow_def.
 
 (** Extra modules using [Omega] or [Ring]. *)
 
diff --git a/theories/ZArith/Zdigits_def.v b/theories/ZArith/Zdigits_def.v
deleted file mode 100644
index 1fff96dd1a..0000000000
--- a/theories/ZArith/Zdigits_def.v
+++ /dev/null
@@ -1,337 +0,0 @@
-(************************************************************************)
-(*  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        *)
-(************************************************************************)
-
-(** Bitwise operations for ZArith *)
-
-Require Import Bool BinPos BinNat BinInt Znat Zeven Zpow_def
- Zorder Zcompare.
-
-Local Open Scope Z_scope.
-
-Notation Ztestbit := Z.testbit (only parsing).
-Notation Zshiftr := Z.shiftr (only parsing).
-Notation Zshiftl := Z.shiftl (only parsing).
-Notation Zor := Z.lor (only parsing).
-Notation Zand := Z.land (only parsing).
-Notation Zdiff := Z.ldiff (only parsing).
-Notation Zxor := Z.lxor (only parsing).
-
-
-(** Conversions between [Ztestbit] and [Ntestbit] *)
-
-Lemma Ztestbit_of_N : forall a n,
- Ztestbit (Z_of_N a) (Z_of_N n) = N.testbit a n.
-Proof.
- intros [ |a] [ |n]; simpl; trivial. now destruct a.
-Qed.
-
-Lemma Ztestbit_of_N' : forall a n, 0<=n ->
- Ztestbit (Z_of_N a) n = N.testbit a (Zabs_N n).
-Proof.
- intros. now rewrite <- Ztestbit_of_N, Z_of_N_abs, Zabs_eq.
-Qed.
-
-Lemma Ztestbit_Zpos : forall a n, 0<=n ->
- Ztestbit (Zpos a) n = N.testbit (Npos a) (Zabs_N n).
-Proof.
- intros. now rewrite <- Ztestbit_of_N'.
-Qed.
-
-Lemma Ztestbit_Zneg : forall a n, 0<=n ->
- Ztestbit (Zneg a) n = negb (N.testbit (Pos.pred_N a) (Zabs_N n)).
-Proof.
- intros a n Hn.
- rewrite <- Ztestbit_of_N' by trivial.
- destruct n as [ |n|n];
-  [ | simpl; now destruct (Ppred_N a) | now destruct Hn].
- unfold Ztestbit.
- replace (Z_of_N (Pos.pred_N a)) with (Zpred (Zpos a))
-  by (destruct a; trivial).
- now rewrite Zodd_bool_pred, <- Zodd_even_bool.
-Qed.
-
-(** Proofs of specifications *)
-
-Lemma Zdiv2_spec : forall a, Zdiv2 a = Zshiftr a 1.
-Proof.
- reflexivity.
-Qed.
-
-Lemma Ztestbit_0_l : forall n, Ztestbit 0 n = false.
-Proof.
- now destruct n.
-Qed.
-
-Lemma Ztestbit_neg_r : forall a n, n<0 -> Ztestbit a n = false.
-Proof.
- now destruct n.
-Qed.
-
-Lemma Ztestbit_odd_0 a : Ztestbit (2*a+1) 0 = true.
-Proof.
- now destruct a as [|a|[a|a|]].
-Qed.
-
-Lemma Ztestbit_even_0 a : Ztestbit (2*a) 0 = false.
-Proof.
- now destruct a.
-Qed.
-
-Lemma Ztestbit_odd_succ a n : 0<=n ->
- Ztestbit (2*a+1) (Zsucc n) = Ztestbit a n.
-Proof.
- destruct n as [|n|n]; (now destruct 1) || intros _.
- destruct a as [|[a|a|]|[a|a|]]; simpl; trivial. now destruct a.
- unfold Ztestbit. rewrite <- Zpos_succ_morphism.
- destruct a as [|a|[a|a|]]; simpl; trivial;
-  rewrite ?Pos.pred_N_succ; now destruct n.
-Qed.
-
-Lemma Ztestbit_even_succ a n : 0<=n ->
- Ztestbit (2*a) (Zsucc n) = Ztestbit a n.
-Proof.
- destruct n as [|n|n]; (now destruct 1) || intros _.
- destruct a as [|[a|a|]|[a|a|]]; simpl; trivial. now destruct a.
- unfold Ztestbit. rewrite <- Zpos_succ_morphism.
- destruct a as [|a|[a|a|]]; simpl; trivial;
-  rewrite ?Pos.pred_N_succ; now destruct n.
-Qed.
-
-Lemma Ppred_div2_up : forall p,
- Pos.pred_N (Pos.div2_up p) = N.div2 (Pos.pred_N p).
-Proof.
- intros [p|p| ]; trivial.
- simpl. apply Pos.pred_N_succ.
- destruct p; simpl; trivial.
-Qed.
-
-Lemma Z_of_N_div2 : forall n, Z_of_N (N.div2 n) = Zdiv2 (Z_of_N n).
-Proof.
- intros [|p]; trivial. now destruct p.
-Qed.
-
-Lemma Z_of_N_quot2 : forall n, Z_of_N (N.div2 n) = Zquot2 (Z_of_N n).
-Proof.
- intros [|p]; trivial. now destruct p.
-Qed.
-
-(** Auxiliary results about right shift on positive numbers *)
-
-Lemma Ppred_Pshiftl_low : forall p n m, (m<n)%N ->
- N.testbit (Pos.pred_N (Pos.shiftl p n)) m = true.
-Proof.
- induction n using N.peano_ind.
- now destruct m.
- intros m H. unfold Pos.shiftl.
- destruct n as [|n]; simpl in *.
- destruct m. now destruct p. elim (Pos.nlt_1_r _ H).
- rewrite Pos.iter_succ. simpl.
- set (u:=Pos.iter n xO p) in *; clearbody u.
- destruct m as [|m]. now destruct u.
- rewrite <- (IHn (Pos.pred_N m)).
- rewrite <- (N.testbit_odd_succ _ (Pos.pred_N m)).
- rewrite N.succ_pos_pred. now destruct u.
- apply N.le_0_l.
- apply N.succ_lt_mono. now rewrite N.succ_pos_pred.
-Qed.
-
-Lemma Ppred_Pshiftl_high : forall p n m, (n<=m)%N ->
- N.testbit (Pos.pred_N (Pos.shiftl p n)) m =
- N.testbit (N.shiftl (Pos.pred_N p) n) m.
-Proof.
- induction n using N.peano_ind; intros m H.
- unfold N.shiftl. simpl. now destruct (Pos.pred_N p).
- rewrite N.shiftl_succ_r.
- destruct n as [|n].
- destruct m as [|m]. now destruct H. now destruct p.
- destruct m as [|m]. now destruct H.
- rewrite <- (N.succ_pos_pred m).
- rewrite N.double_spec, N.testbit_even_succ by apply N.le_0_l.
- rewrite <- IHn.
- rewrite N.testbit_succ_r_div2 by apply N.le_0_l.
- f_equal. simpl. rewrite Pos.iter_succ.
- now destruct (Pos.iter n xO p).
- apply N.succ_le_mono. now rewrite N.succ_pos_pred.
-Qed.
-
-(** Correctness proofs about [Zshiftr] and [Zshiftl] *)
-
-Lemma Zshiftr_spec_aux : forall a n m, 0<=n -> 0<=m ->
- Ztestbit (Zshiftr a n) m = Ztestbit a (m+n).
-Proof.
- intros a n m Hn Hm. unfold Zshiftr.
- destruct n as [ |n|n]; (now destruct Hn) || clear Hn; simpl.
- now rewrite Zplus_0_r.
- destruct a as [ |a|a].
- (* a = 0 *)
- replace (iter_pos n _ Zdiv2 0) with 0
-  by (apply iter_pos_invariant; intros; subst; trivial).
- now rewrite 2 Ztestbit_0_l.
- (* a > 0 *)
- rewrite <- (Z_of_N_pos a) at 1.
- rewrite <- (iter_pos_swap_gen _ _ _ Ndiv2) by exact Z_of_N_div2.
- rewrite Ztestbit_Zpos, Ztestbit_of_N'; trivial.
- rewrite Zabs_N_plus; try easy. simpl Zabs_N.
- exact (N.shiftr_spec' (Npos a) (Npos n) (Zabs_N m)).
- now apply Zplus_le_0_compat.
- (* a < 0 *)
- rewrite <- (iter_pos_swap_gen _ _ _ Pdiv2_up) by trivial.
- rewrite 2 Ztestbit_Zneg; trivial. f_equal.
- rewrite Zabs_N_plus; try easy. simpl Zabs_N.
- rewrite (iter_pos_swap_gen _ _ _ _ Ndiv2) by exact Ppred_div2_up.
- exact (N.shiftr_spec' (Ppred_N a) (Npos n) (Zabs_N m)).
- now apply Zplus_le_0_compat.
-Qed.
-
-Lemma Zshiftl_spec_low : forall a n m, m<n ->
- Ztestbit (Zshiftl a n) m = false.
-Proof.
- intros a [ |n|n] [ |m|m] H; try easy; simpl Zshiftl.
- rewrite iter_nat_of_P.
- destruct (nat_of_P_is_S n) as (n' & ->).
- simpl. now destruct (iter_nat n' _  (Zmult 2) a).
- destruct a as [ |a|a].
- (* a = 0 *)
- replace (iter_pos n _ (Zmult 2) 0) with 0
-  by (apply iter_pos_invariant; intros; subst; trivial).
- apply Ztestbit_0_l.
- (* a > 0 *)
- rewrite <- (iter_pos_swap_gen _ _ _ xO) by trivial.
- rewrite Ztestbit_Zpos by easy.
- exact (N.shiftl_spec_low (Npos a) (Npos n) (Npos m) H).
- (* a < 0 *)
- rewrite <- (iter_pos_swap_gen _ _ _ xO) by trivial.
- rewrite Ztestbit_Zneg by easy.
- now rewrite (Ppred_Pshiftl_low a (Npos n)).
-Qed.
-
-Lemma Zshiftl_spec_high : forall a n m, 0<=m -> n<=m ->
- Ztestbit (Zshiftl a n) m = Ztestbit a (m-n).
-Proof.
- intros a n m Hm H.
- destruct n as [ |n|n]. simpl. now rewrite Zminus_0_r.
- (* n > 0 *)
- destruct m as [ |m|m]; try (now destruct H).
- assert (0 <= Zpos m - Zpos n) by (now apply Zle_minus_le_0).
- assert (EQ : Zabs_N (Zpos m - Zpos n) =  (Npos m - Npos n)%N).
-  apply Z_of_N_eq_rev. rewrite Z_of_N_abs, Zabs_eq by trivial.
-  now rewrite Z_of_N_minus, !Z_of_N_pos, Zmax_r.
- destruct a; unfold Zshiftl.
- (* ... a = 0 *)
- replace (iter_pos n _ (Zmult 2) 0) with 0
-  by (apply iter_pos_invariant; intros; subst; trivial).
- now rewrite 2 Ztestbit_0_l.
- (* ... a > 0 *)
- rewrite <- (iter_pos_swap_gen _ _ _ xO) by trivial.
- rewrite 2 Ztestbit_Zpos, EQ by easy.
- exact (N.shiftl_spec_high' (Npos p) (Npos n) (Npos m) H).
- (* ... a < 0 *)
- rewrite <- (iter_pos_swap_gen _ _ _ xO) by trivial.
- rewrite 2 Ztestbit_Zneg, EQ by easy. f_equal.
- simpl Zabs_N.
- rewrite <- N.shiftl_spec_high by easy.
- now apply (Ppred_Pshiftl_high p (Npos n)).
- (* n < 0 *)
- unfold Zminus. simpl.
- now apply (Zshiftr_spec_aux a (Zpos n) m).
-Qed.
-
-Lemma Zshiftr_spec : forall a n m, 0<=m ->
- Ztestbit (Zshiftr a n) m = Ztestbit a (m+n).
-Proof.
- intros a n m Hm.
- destruct (Zle_or_lt 0 n).
- now apply Zshiftr_spec_aux.
- destruct (Zle_or_lt (-n) m).
- unfold Zshiftr.
- rewrite (Zshiftl_spec_high a (-n) m); trivial.
- unfold Zminus. now rewrite Zopp_involutive.
- unfold Zshiftr.
- rewrite (Zshiftl_spec_low a (-n) m); trivial.
- rewrite Ztestbit_neg_r; trivial.
- now apply Zlt_plus_swap.
-Qed.
-
-(** Correctness proofs for bitwise operations *)
-
-Lemma Zor_spec : forall a b n,
- Ztestbit (Zor a b) n = Ztestbit a n || Ztestbit b n.
-Proof.
- intros a b n.
- destruct (Zle_or_lt 0 n) as [Hn|Hn]; [|now rewrite !Ztestbit_neg_r].
- destruct a as [ |a|a], b as [ |b|b];
-  rewrite ?Ztestbit_0_l, ?orb_false_r; trivial; unfold Zor;
-  rewrite ?Ztestbit_Zpos, ?Ztestbit_Zneg, ?Ppred_Nsucc
-   by trivial.
- now rewrite <- N.lor_spec.
- now rewrite N.ldiff_spec, negb_andb, negb_involutive, orb_comm.
- now rewrite N.ldiff_spec, negb_andb, negb_involutive.
- now rewrite N.land_spec, negb_andb.
-Qed.
-
-Lemma Zand_spec : forall a b n,
- Ztestbit (Zand a b) n = Ztestbit a n && Ztestbit b n.
-Proof.
- intros a b n.
- destruct (Zle_or_lt 0 n) as [Hn|Hn]; [|now rewrite !Ztestbit_neg_r].
- destruct a as [ |a|a], b as [ |b|b];
-  rewrite ?Ztestbit_0_l, ?andb_false_r; trivial; unfold Zand;
-  rewrite ?Ztestbit_Zpos, ?Ztestbit_Zneg, ?Ztestbit_of_N', ?Ppred_Nsucc
-   by trivial.
- now rewrite <- N.land_spec.
- now rewrite N.ldiff_spec.
- now rewrite N.ldiff_spec, andb_comm.
- now rewrite N.lor_spec, negb_orb.
-Qed.
-
-Lemma Zdiff_spec : forall a b n,
- Ztestbit (Zdiff a b) n = Ztestbit a n && negb (Ztestbit b n).
-Proof.
- intros a b n.
- destruct (Zle_or_lt 0 n) as [Hn|Hn]; [|now rewrite !Ztestbit_neg_r].
- destruct a as [ |a|a], b as [ |b|b];
-  rewrite ?Ztestbit_0_l, ?andb_true_r; trivial; unfold Zdiff;
-  rewrite ?Ztestbit_Zpos, ?Ztestbit_Zneg, ?Ztestbit_of_N', ?Ppred_Nsucc
-   by trivial.
- now rewrite <- N.ldiff_spec.
- now rewrite N.land_spec, negb_involutive.
- now rewrite N.lor_spec, negb_orb.
- now rewrite N.ldiff_spec, negb_involutive, andb_comm.
-Qed.
-
-Lemma Zxor_spec : forall a b n,
- Ztestbit (Zxor a b) n = xorb (Ztestbit a n) (Ztestbit b n).
-Proof.
- intros a b n.
- destruct (Zle_or_lt 0 n) as [Hn|Hn]; [|now rewrite !Ztestbit_neg_r].
- destruct a as [ |a|a], b as [ |b|b];
-  rewrite ?Ztestbit_0_l, ?xorb_false_l, ?xorb_false_r; trivial; unfold Zxor;
-  rewrite ?Ztestbit_Zpos, ?Ztestbit_Zneg, ?Ztestbit_of_N', ?Ppred_Nsucc
-   by trivial.
- now rewrite <- N.lxor_spec.
- now rewrite N.lxor_spec, negb_xorb_r.
- now rewrite N.lxor_spec, negb_xorb_l.
- now rewrite N.lxor_spec, xorb_negb_negb.
-Qed.
-
-(** An additionnal proof concerning [Pshiftl_nat], used in BigN *)
-
-
-Lemma Pshiftl_nat_Zpower : forall n p,
-  Zpos (Pos.shiftl_nat p n) = Zpos p * 2 ^ Z_of_nat n.
-Proof.
- intros.
- rewrite Zmult_comm.
- induction n. simpl; auto.
- transitivity (2 * (2 ^ Z_of_nat n * Zpos p)).
- rewrite <- IHn. auto.
- rewrite Zmult_assoc.
- rewrite inj_S.
- rewrite <- Zpower_succ_r; auto with zarith.
- apply Zle_0_nat.
-Qed.
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index 84262469b3..0ae5dea818 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -212,6 +212,16 @@ Proof.
  case N.compare_spec; intros; subst; trivial.
 Qed.
 
+Lemma inj_div2 n : Z.of_N (N.div2 n) = Z.div2 (Z.of_N n).
+Proof.
+ destruct n as [|p]; trivial. now destruct p.
+Qed.
+
+Lemma inj_quot2 n : Z.of_N (N.div2 n) = Z.quot2 (Z.of_N n).
+Proof.
+ destruct n as [|p]; trivial. now destruct p.
+Qed.
+
 End N2Z.
 
 Module Z2N.
diff --git a/theories/ZArith/vo.itarget b/theories/ZArith/vo.itarget
index 767ba4f1b4..9c1e69ac7c 100644
--- a/theories/ZArith/vo.itarget
+++ b/theories/ZArith/vo.itarget
@@ -30,4 +30,3 @@ Zpow_facts.vo
 Zsqrt_compat.vo
 Zwf.vo
 Zeuclid.vo
-Zdigits_def.vo
\ No newline at end of file