Ndigits: a Pshiftl_nat used in BigN (was double_digits there)

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

6 files changed, 80 insertions, 111 deletions

diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
index af113da2b..d92e818ff 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
@@ -10,12 +10,14 @@
 
 Set Implicit Arguments.
 
-Require Import ZArith.
+Require Import ZArith Ndigits.
 Require Import BigNumPrelude.
 Require Import DoubleType.
 
 Local Open Scope Z_scope.
 
+Local Infix "<<" := Pshiftl_nat (at level 30).
+
 Section DoubleBase.
  Variable w : Type.
  Variable w_0   : w.
@@ -68,13 +70,7 @@ Section DoubleBase.
      end
   end.
 
- Fixpoint double_digits (n:nat) : positive :=
-  match n with
-  | O => w_digits
-  | S n => xO (double_digits n)
-  end.
-
- Definition double_wB n := base (double_digits n).
+ Definition double_wB n := base (w_digits << n).
 
  Fixpoint double_to_Z (n:nat) : word w n -> Z :=
   match n return word w n -> Z with
@@ -291,11 +287,10 @@ Section DoubleBase.
   Lemma double_wB_wwB : forall n, double_wB n * double_wB n = double_wB (S n).
   Proof.
    intros n;unfold double_wB;simpl.
-   unfold base;rewrite (Zpos_xO (double_digits n)).
-   replace  (2 * Zpos (double_digits n)) with
-     (Zpos (double_digits n) + Zpos (double_digits n)).
+   unfold base. rewrite Pshiftl_nat_S, (Zpos_xO (_ << _)).
+   replace  (2 * Zpos (w_digits << n)) with
+     (Zpos (w_digits << n) + Zpos (w_digits << n)) by ring.
    symmetry; apply Zpower_exp;intro;discriminate.
-   ring.
   Qed.
 
   Lemma double_wB_pos:
@@ -309,7 +304,7 @@ Section DoubleBase.
   Proof.
   clear spec_w_0 spec_w_1 spec_w_Bm1 w_0 w_1 w_Bm1.
   intros n; elim n; clear n; auto.
-    unfold double_wB, double_digits; auto with zarith.
+    unfold double_wB, "<<"; auto with zarith.
   intros n H1; rewrite <- double_wB_wwB.
   apply Zle_trans with (wB * 1).
     rewrite Zmult_1_r; apply Zle_refl.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
index c6c8e8d99..0cb6848e3 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
@@ -1044,7 +1044,6 @@ Section DoubleDivGt.
    assert (H2:= @spec_double_divn1 w w_digits w_zdigits w_0 w_WW w_head0 w_add_mul_div
     w_div21 w_compare w_sub w_to_Z spec_to_Z spec_w_zdigits spec_w_0 spec_w_WW spec_head0
     spec_add_mul_div spec_div21 spec_compare spec_sub 1 (WW ah al) bl Hpos).
-   unfold double_to_Z,double_wB,double_digits in H2.
    destruct (double_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21
               w_compare w_sub 1
              (WW ah al) bl).
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
index 332def286..bf92bbb98 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
@@ -10,13 +10,15 @@
 
 Set Implicit Arguments.
 
-Require Import ZArith.
+Require Import ZArith Ndigits.
 Require Import BigNumPrelude.
 Require Import DoubleType.
 Require Import DoubleBase.
 
 Local Open Scope Z_scope.
 
+Local Infix "<<" := Pshiftl_nat (at level 30).
+
 Section GENDIVN1.
 
  Variable w             : Type.
@@ -155,14 +157,10 @@ Section GENDIVN1.
    | S n => double_divn1_p_aux n (double_divn1_p n)
    end.
 
-  Lemma p_lt_double_digits : forall n, [|p|] <= Zpos (double_digits w_digits n).
+  Lemma p_lt_double_digits : forall n, [|p|] <= Zpos (w_digits << n).
   Proof.
-(*
-   induction n;simpl. destruct p_bounded;trivial.
-   case (spec_to_Z p); rewrite Zpos_xO;auto with zarith.
-*)
    induction n;simpl. trivial.
-   case (spec_to_Z p); rewrite Zpos_xO;auto with zarith.
+   case (spec_to_Z p); rewrite Pshiftl_nat_S, Zpos_xO;auto with zarith.
   Qed.
 
   Lemma spec_double_divn1_p : forall n r h l,
@@ -170,14 +168,14 @@ Section GENDIVN1.
     let (q,r') := double_divn1_p n r h l in
     [|r|] * double_wB w_digits n +
       ([!n|h!]*2^[|p|] +
-        [!n|l!] / (2^(Zpos(double_digits w_digits n) - [|p|])))
+        [!n|l!] / (2^(Zpos(w_digits << n) - [|p|])))
         mod double_wB w_digits n = [!n|q!] * [|b2p|] + [|r'|] /\
     0 <= [|r'|] < [|b2p|].
   Proof.
    case (spec_to_Z p); intros HH0 HH1.
    induction n;intros.
    simpl (double_divn1_p 0 r h l).
-   unfold double_to_Z, double_wB, double_digits.
+   unfold double_to_Z, double_wB, "<<".
    rewrite <- spec_add_mul_divp.
    exact (spec_div21 (w_add_mul_div p h l) b2p_le H).
    simpl (double_divn1_p (S n) r h l).
@@ -189,24 +187,24 @@ Section GENDIVN1.
    replace ([|r|] * (double_wB w_digits n * double_wB w_digits n) +
     (([!n|hh!] * double_wB w_digits n + [!n|hl!]) * 2 ^ [|p|] +
     ([!n|lh!] * double_wB w_digits n + [!n|ll!]) /
-     2^(Zpos (double_digits w_digits (S n)) - [|p|])) mod
+     2^(Zpos (w_digits << (S n)) - [|p|])) mod
       (double_wB w_digits n * double_wB w_digits n)) with
     (([|r|] * double_wB w_digits n + ([!n|hh!] * 2^[|p|] +
-      [!n|hl!] / 2^(Zpos (double_digits w_digits n) - [|p|])) mod
+      [!n|hl!] / 2^(Zpos (w_digits << n) - [|p|])) mod
                       double_wB w_digits n) * double_wB w_digits n +
      ([!n|hl!] * 2^[|p|] +
-      [!n|lh!] / 2^(Zpos (double_digits w_digits n) - [|p|])) mod
+      [!n|lh!] / 2^(Zpos (w_digits << n) - [|p|])) mod
               double_wB w_digits n).
    generalize (IHn r hh hl H);destruct (double_divn1_p n r hh hl) as (qh,rh);
    intros (H3,H4);rewrite H3.
    assert ([|rh|] < [|b2p|]). omega.
    replace (([!n|qh!] * [|b2p|] + [|rh|]) * double_wB w_digits n +
      ([!n|hl!] * 2 ^ [|p|] +
-      [!n|lh!] / 2 ^ (Zpos (double_digits w_digits n) - [|p|])) mod
+      [!n|lh!] / 2 ^ (Zpos (w_digits << n) - [|p|])) mod
       double_wB w_digits n)  with
     ([!n|qh!] * [|b2p|] *double_wB w_digits n + ([|rh|]*double_wB w_digits n +
       ([!n|hl!] * 2 ^ [|p|] +
-       [!n|lh!] / 2 ^ (Zpos (double_digits w_digits n) - [|p|])) mod
+       [!n|lh!] / 2 ^ (Zpos (w_digits << n) - [|p|])) mod
       double_wB w_digits n)). 2:ring.
    generalize (IHn rh hl lh H0);destruct (double_divn1_p n rh hl lh) as (ql,rl);
    intros (H5,H6);rewrite H5.
@@ -222,52 +220,52 @@ Section GENDIVN1.
    unfold double_wB,base.
    assert (UU:=p_lt_double_digits n).
    rewrite Zdiv_shift_r;auto with zarith.
-   2:change (Zpos (double_digits w_digits (S n)))
-     with (2*Zpos (double_digits w_digits n));auto with zarith.
-   replace (2 ^ (Zpos (double_digits w_digits (S n)) - [|p|])) with
-    (2^(Zpos (double_digits w_digits n) - [|p|])*2^Zpos (double_digits w_digits n)).
+   2:change (Zpos (w_digits << (S n)))
+     with (2*Zpos (w_digits << n));auto with zarith.
+   replace (2 ^ (Zpos (w_digits << (S n)) - [|p|])) with
+    (2^(Zpos (w_digits << n) - [|p|])*2^Zpos (w_digits << n)).
    rewrite Zdiv_mult_cancel_r;auto with zarith.
    rewrite Zmult_plus_distr_l with (p:=  2^[|p|]).
    pattern  ([!n|hl!] * 2^[|p|]) at 2;
-   rewrite (shift_unshift_mod (Zpos(double_digits w_digits n))([|p|])([!n|hl!]));
+   rewrite (shift_unshift_mod (Zpos(w_digits << n))([|p|])([!n|hl!]));
     auto with zarith.
    rewrite Zplus_assoc.
    replace
-    ([!n|hh!] * 2^Zpos (double_digits w_digits n)* 2^[|p|] +
-      ([!n|hl!] / 2^(Zpos (double_digits w_digits n)-[|p|])*
-       2^Zpos(double_digits w_digits n)))
+    ([!n|hh!] * 2^Zpos (w_digits << n)* 2^[|p|] +
+      ([!n|hl!] / 2^(Zpos (w_digits << n)-[|p|])*
+       2^Zpos(w_digits << n)))
    with
     (([!n|hh!] *2^[|p|] + double_to_Z w_digits w_to_Z n hl /
-       2^(Zpos (double_digits w_digits n)-[|p|]))
-      * 2^Zpos(double_digits w_digits n));try (ring;fail).
+       2^(Zpos (w_digits << n)-[|p|]))
+      * 2^Zpos(w_digits << n));try (ring;fail).
    rewrite <- Zplus_assoc.
    rewrite <- (Zmod_shift_r ([|p|]));auto with zarith.
    replace
-     (2 ^ Zpos (double_digits w_digits n) * 2 ^ Zpos (double_digits w_digits n)) with
-     (2 ^ (Zpos (double_digits w_digits n) + Zpos (double_digits w_digits n))).
-   rewrite (Zmod_shift_r (Zpos (double_digits w_digits n)));auto with zarith.
-   replace (2 ^ (Zpos (double_digits w_digits n) + Zpos (double_digits w_digits n)))
-   with (2^Zpos(double_digits w_digits n) *2^Zpos(double_digits w_digits n)).
+     (2 ^ Zpos (w_digits << n) * 2 ^ Zpos (w_digits << n)) with
+     (2 ^ (Zpos (w_digits << n) + Zpos (w_digits << n))).
+   rewrite (Zmod_shift_r (Zpos (w_digits << n)));auto with zarith.
+   replace (2 ^ (Zpos (w_digits << n) + Zpos (w_digits << n)))
+   with (2^Zpos(w_digits << n) *2^Zpos(w_digits << n)).
    rewrite (Zmult_comm (([!n|hh!] * 2 ^ [|p|] +
-      [!n|hl!] / 2 ^ (Zpos (double_digits w_digits n) - [|p|])))).
+      [!n|hl!] / 2 ^ (Zpos (w_digits << n) - [|p|])))).
    rewrite  Zmult_mod_distr_l;auto with zarith.
    ring.
    rewrite Zpower_exp;auto with zarith.
-   assert (0 < Zpos (double_digits w_digits n)). unfold Zlt;reflexivity.
+   assert (0 < Zpos (w_digits << n)). unfold Zlt;reflexivity.
    auto with zarith.
    apply Z_mod_lt;auto with zarith.
    rewrite Zpower_exp;auto with zarith.
    split;auto with zarith.
    apply Zdiv_lt_upper_bound;auto with zarith.
    rewrite <- Zpower_exp;auto with zarith.
-   replace ([|p|] + (Zpos (double_digits w_digits n) - [|p|])) with
-     (Zpos(double_digits w_digits n));auto with zarith.
+   replace ([|p|] + (Zpos (w_digits << n) - [|p|])) with
+     (Zpos(w_digits << n));auto with zarith.
    rewrite <- Zpower_exp;auto with zarith.
-   replace (Zpos (double_digits w_digits (S n)) - [|p|]) with
-       (Zpos (double_digits w_digits n) - [|p|] +
-         Zpos (double_digits w_digits n));trivial.
-   change (Zpos (double_digits w_digits (S n))) with
-    (2*Zpos (double_digits w_digits n)). ring.
+   replace (Zpos (w_digits << (S n)) - [|p|]) with
+       (Zpos (w_digits << n) - [|p|] +
+         Zpos (w_digits << n));trivial.
+   change (Zpos (w_digits << (S n))) with
+    (2*Zpos (w_digits << n)). ring.
   Qed.
 
   Definition double_modn1_p_aux n (modn1 : w -> word w n -> word w n -> w) r h l:=
@@ -304,20 +302,21 @@ Section GENDIVN1.
      end
   end.
 
- Lemma spec_double_digits:forall n, Zpos w_digits <= Zpos (double_digits w_digits n).
+ Lemma spec_double_digits:forall n, Zpos w_digits <= Zpos (w_digits << n).
  Proof.
   induction n;simpl;auto with zarith.
-  change (Zpos (xO (double_digits w_digits n))) with
-    (2*Zpos (double_digits w_digits n)).
-  assert (0 < Zpos w_digits);auto with zarith.
-  exact (refl_equal Lt).
+  rewrite Pshiftl_nat_S.
+  change (Zpos (xO (w_digits << n))) with
+    (2*Zpos (w_digits << n)).
+  assert (0 < Zpos w_digits) by reflexivity.
+  auto with zarith.
  Qed.
 
  Lemma spec_high : forall n (x:word w n),
-   [|high n x|] = [!n|x!] / 2^(Zpos (double_digits w_digits n) - Zpos w_digits).
+   [|high n x|] = [!n|x!] / 2^(Zpos (w_digits << n) - Zpos w_digits).
  Proof.
   induction n;intros.
-  unfold high,double_digits,double_to_Z.
+  unfold high,double_to_Z. rewrite Pshiftl_nat_0.
   replace (Zpos w_digits - Zpos w_digits) with 0;try ring.
   simpl. rewrite <- (Zdiv_unique [|x|] 1 [|x|] 0);auto with zarith.
   assert (U2 := spec_double_digits n).
@@ -329,18 +328,18 @@ Section GENDIVN1.
    assert (U1 := spec_double_to_Z w_digits w_to_Z spec_to_Z n w1).
   simpl [!S n|WW w0 w1!].
   unfold double_wB,base;rewrite Zdiv_shift_r;auto with zarith.
-  replace (2 ^ (Zpos (double_digits w_digits (S n)) - Zpos w_digits)) with
-   (2^(Zpos (double_digits w_digits n) - Zpos w_digits) *
-        2^Zpos (double_digits w_digits n)).
+  replace (2 ^ (Zpos (w_digits << (S n)) - Zpos w_digits)) with
+   (2^(Zpos (w_digits << n) - Zpos w_digits) *
+        2^Zpos (w_digits << n)).
   rewrite Zdiv_mult_cancel_r;auto with zarith.
   rewrite <- Zpower_exp;auto with zarith.
-  replace (Zpos (double_digits w_digits n) - Zpos w_digits +
-    Zpos (double_digits w_digits n)) with
-   (Zpos (double_digits w_digits (S n)) - Zpos w_digits);trivial.
-  change (Zpos (double_digits w_digits (S n))) with
-     (2*Zpos (double_digits w_digits n));ring.
-  change (Zpos (double_digits w_digits (S n))) with
-  (2*Zpos (double_digits w_digits n)); auto with zarith.
+  replace (Zpos (w_digits << n) - Zpos w_digits +
+    Zpos (w_digits << n)) with
+   (Zpos (w_digits << (S n)) - Zpos w_digits);trivial.
+  change (Zpos (w_digits << (S n))) with
+     (2*Zpos (w_digits << n));ring.
+  change (Zpos (w_digits << (S n))) with
+  (2*Zpos (w_digits << n)); auto with zarith.
  Qed.
 
  Definition double_divn1 (n:nat) (a:word w n) (b:w) :=
@@ -425,13 +424,13 @@ Section GENDIVN1.
    rewrite spec_add_mul_div in H7;auto with zarith.
    rewrite spec_0 in H7;rewrite Zmult_0_l in H7;rewrite Zplus_0_l in H7.
    assert (([|high n a|] / 2 ^ (Zpos w_digits - [|w_head0 b|])) mod wB
-     = [!n|a!] / 2^(Zpos (double_digits w_digits n) - [|w_head0 b|])).
+     = [!n|a!] / 2^(Zpos (w_digits << n) - [|w_head0 b|])).
    rewrite Zmod_small;auto with zarith.
    rewrite spec_high. rewrite Zdiv_Zdiv;auto with zarith.
    rewrite <- Zpower_exp;auto with zarith.
-   replace (Zpos (double_digits w_digits n) - Zpos w_digits +
+   replace (Zpos (w_digits << n) - Zpos w_digits +
                        (Zpos w_digits - [|w_head0 b|]))
-    with (Zpos (double_digits w_digits n) - [|w_head0 b|]);trivial;ring.
+    with (Zpos (w_digits << n) - [|w_head0 b|]);trivial;ring.
    assert (H8 := Zpower_gt_0 2  (Zpos w_digits - [|w_head0 b|]));auto with zarith.
    split;auto with zarith.
    apply Zle_lt_trans with ([|high n a|]);auto with zarith.
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index 105cf0620..23cfec5e9 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -64,7 +64,7 @@ Module Make (W0:CyclicType) <: NType.
  Proof.
  intros.
  change (Zpos (ZnZ.digits (dom_op n)) <= Zpos (ZnZ.digits (dom_op m))).
- rewrite !digits_dom_op, !Pshiftl_Zpower.
+ rewrite !digits_dom_op, !Pshiftl_nat_Zpower.
  apply Zmult_le_compat_l; auto with zarith.
  apply Zpower_le_monotone2; auto with zarith.
  Qed.
@@ -1050,7 +1050,7 @@ Module Make (W0:CyclicType) <: NType.
  unfold base.
  apply Zlt_le_trans with (1 := pheight_correct x).
  apply Zpower_le_monotone2; auto with zarith.
- rewrite (digits_dom_op (_ _)), Pshiftl_Zpower. auto with zarith.
+ rewrite (digits_dom_op (_ _)), Pshiftl_nat_Zpower. auto with zarith.
  Qed.
 
  Definition of_N (x:N) : t :=
@@ -1392,7 +1392,7 @@ Module Make (W0:CyclicType) <: NType.
    forall x, Zpos (digits (double_size x)) = 2 * (Zpos (digits x)).
  Proof.
  intros x. rewrite ! digits_level, double_size_level.
- rewrite 2 digits_dom_op, 2 Pshiftl_Zpower,
+ rewrite 2 digits_dom_op, 2 Pshiftl_nat_Zpower,
          inj_S, Zpower_Zsucc; auto with zarith.
  ring.
  Qed.
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 8779f4be3..b5cc4c51d 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -49,7 +49,7 @@ pr
 
 (** Remark: File automatically generated by NMake_gen.ml, DO NOT EDIT ! *)
 
-Require Import BigNumPrelude ZArith CyclicAxioms
+Require Import BigNumPrelude ZArith Ndigits CyclicAxioms
  DoubleType DoubleMul DoubleDivn1 DoubleCyclic Nbasic
  Wf_nat StreamMemo.
 
@@ -248,10 +248,10 @@ pr
  Qed.
 
  Theorem digits_nmake : forall n ww (w_op: ZnZ.Ops ww),
-    ZnZ.digits (nmake_op _ w_op n) = Pshiftl (ZnZ.digits w_op) n.
+    ZnZ.digits (nmake_op _ w_op n) = Pshiftl_nat (ZnZ.digits w_op) n.
  Proof.
  induction n. auto.
- intros ww ww_op; simpl Pshiftl. rewrite <- IHn; auto.
+ intros ww ww_op. rewrite Pshiftl_nat_S, <- IHn; auto.
  Qed.
 
  Theorem nmake_double: forall n ww (w_op: ZnZ.Ops ww),
@@ -331,7 +331,7 @@ pr "
  (** * Digits *)
 
  Lemma digits_make_op_0 : forall n,
-  ZnZ.digits (make_op n) = Pshiftl (ZnZ.digits (dom_op Size)) (S n).
+  ZnZ.digits (make_op n) = Pshiftl_nat (ZnZ.digits (dom_op Size)) (S n).
  Proof.
  induction n.
  auto.
@@ -341,15 +341,15 @@ pr "
  Qed.
 
  Lemma digits_make_op : forall n,
-  ZnZ.digits (make_op n) = Pshiftl (ZnZ.digits w0_op) (SizePlus (S n)).
+  ZnZ.digits (make_op n) = Pshiftl_nat (ZnZ.digits w0_op) (SizePlus (S n)).
  Proof.
  intros. rewrite digits_make_op_0.
  replace (SizePlus (S n)) with (S n + Size) by (rewrite <- plus_comm; auto).
- rewrite Pshiftl_plus. auto.
+ rewrite Pshiftl_nat_plus. auto.
  Qed.
 
  Lemma digits_dom_op : forall n,
-  ZnZ.digits (dom_op n) = Pshiftl (ZnZ.digits w0_op) n.
+  ZnZ.digits (dom_op n) = Pshiftl_nat (ZnZ.digits w0_op) n.
  Proof.
  do_size (destruct n; try reflexivity).
  exact (digits_make_op n).
@@ -358,7 +358,7 @@ pr "
  Lemma digits_dom_op_nmake : forall n m,
   ZnZ.digits (dom_op (m+n)) = ZnZ.digits (nmake_op _ (dom_op n) m).
  Proof.
- intros. rewrite digits_nmake, 2 digits_dom_op. apply Pshiftl_plus.
+ intros. rewrite digits_nmake, 2 digits_dom_op. apply Pshiftl_nat_plus.
  Qed.
 
  (** * Conversion between [zn2z (dom_t n)] and [dom_t (S n)].
diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v
index 552002e44..94f6b32fd 100644
--- a/theories/Numbers/Natural/BigN/Nbasic.v
+++ b/theories/Numbers/Natural/BigN/Nbasic.v
@@ -8,7 +8,7 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-Require Import ZArith.
+Require Import ZArith Ndigits.
 Require Import BigNumPrelude.
 Require Import Max.
 Require Import DoubleType.
@@ -358,8 +358,8 @@ Section CompareRec.
  intros n (H0, H); split; auto.
  apply Zlt_le_trans with (1:= H).
  unfold double_wB, DoubleBase.double_wB; simpl.
- rewrite base_xO.
- set (u := base (double_digits wm_base n)).
+ rewrite Pshiftl_nat_S, base_xO.
+ set (u := base (Pshiftl_nat wm_base n)).
  assert (0 < u).
   unfold u, base; auto with zarith.
  replace (u^2) with (u * u); simpl; auto with zarith.
@@ -480,30 +480,6 @@ End AddS.
 
  End SimplOp.
 
-(** TODO : to migrate in NArith *)
-
- Notation Pshiftl := DoubleBase.double_digits.
-
- Lemma Pshiftl_plus : forall n m p,
-  Pshiftl p (m + n) = Pshiftl (Pshiftl p n) m.
- Proof.
- induction m; simpl; congruence.
- Qed.
-
- Lemma Pshiftl_Zpower : forall n d,
-  Zpos (Pshiftl d n) = (Zpos d * 2 ^ Z_of_nat n)%Z.
- Proof.
- intros.
- rewrite Zmult_comm.
- induction n. simpl; auto.
- transitivity (2 * (2 ^ Z_of_nat n * Zpos d))%Z.
- rewrite <- IHn. auto.
- rewrite Zmult_assoc.
- rewrite <- Zpower_Zsucc, inj_S; auto with zarith.
- Qed.
-
-(** END TODO *)
-
 (** Abstract vision of a datatype of arbitrary-large numbers.
     Concrete operations can be derived from these generic
     fonctions, in particular from [iter_t] and [same_level].
@@ -518,7 +494,7 @@ Declare Instance dom_op n : ZnZ.Ops (dom_t n).
 Declare Instance dom_spec n : ZnZ.Specs (dom_op n).
 
 Axiom digits_dom_op : forall n,
-  ZnZ.digits (dom_op n) = Pshiftl (ZnZ.digits (dom_op 0)) n.
+  ZnZ.digits (dom_op n) = Pshiftl_nat (ZnZ.digits (dom_op 0)) n.
 
 (** The type [t] of arbitrary-large numbers, with abstract constructor [mk_t]
     and destructor [destr_t] and iterator [iter_t] *)