DoubleCyclic + NMake : typeclasses, more genericity, less ML macro-generation

 - Records of operations and specs in CyclicAxioms are now
   type classes (under a module ZnZ for qualification).
   We benefit from inference and from generic names:
   (ZnZ.mul x y) instead of (znz_mul (some_ops...) x y).

 - Beware of typeclasses unfolds: the line about
   Typeclasses Opaque w1 w2 ... is critical for decent
   compilation time (x2.5 without it).

 - Functions defined via same_level are now obtained from a
   generic version by (Eval ... in ...) during definition.
   The code obtained this way should be just as before, apart
   from some (minor?) details. Proofs for these functions
   are _way_ simplier and lighter.

 - The macro-generated NMake_gen.v contains only generic iterators
   and compare, mul, div_gt, mod_gt. I hope to be able to adapt
   these functions as well soon.

 - Spec of comparison is now fully done with respect to Zcompare

 - A log2 function has been added.

 - No more unsafe_shiftr, we detect the underflow directly with sub_c

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

2 files changed, 241 insertions, 333 deletions

diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 51df2fa38..af30b0175 100644
--- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -26,352 +26,284 @@ Local Open Scope Z_scope.
 
 (** First, a description via an operator record and a spec record. *)
 
-Section Z_nZ_Op.
+Module ZnZ.
 
- Variable znz : Type.
-
- Record znz_op := mk_znz_op {
+ Class Ops (t:Type) := MkOps {
 
     (* Conversion functions with Z *)
-    znz_digits : positive;
-    znz_zdigits: znz;
-    znz_to_Z   : znz -> Z;
-    znz_of_pos : positive -> N * znz; (* Euclidean division by [2^digits] *)
-    znz_head0  : znz -> znz; (* number of digits 0 in front of the number *)
-    znz_tail0  : znz -> znz; (* number of digits 0 at the bottom of the number *)
+    digits : positive;
+    zdigits: t;
+    to_Z   : t -> Z;
+    of_pos : positive -> N * t; (* Euclidean division by [2^digits] *)
+    head0  : t -> t; (* number of digits 0 in front of the number *)
+    tail0  : t -> t; (* number of digits 0 at the bottom of the number *)
 
     (* Basic numbers *)
-    znz_0   : znz;
-    znz_1   : znz;
-    znz_Bm1 : znz;  (* [2^digits-1], which is equivalent to [-1] *)
+    zero : t;
+    one  : t;
+    minus_one : t;  (* [2^digits-1], which is equivalent to [-1] *)
 
     (* Comparison *)
-    znz_compare     : znz -> znz -> comparison;
-    znz_eq0         : znz -> bool;
+    compare     : t -> t -> comparison;
+    eq0         : t -> bool;
 
     (* Basic arithmetic operations *)
-    znz_opp_c       : znz -> carry znz;
-    znz_opp         : znz -> znz;
-    znz_opp_carry   : znz -> znz; (* the carry is known to be -1 *)
-
-    znz_succ_c      : znz -> carry znz;
-    znz_add_c       : znz -> znz -> carry znz;
-    znz_add_carry_c : znz -> znz -> carry znz;
-    znz_succ        : znz -> znz;
-    znz_add         : znz -> znz -> znz;
-    znz_add_carry   : znz -> znz -> znz;
-
-    znz_pred_c      : znz -> carry znz;
-    znz_sub_c       : znz -> znz -> carry znz;
-    znz_sub_carry_c : znz -> znz -> carry znz;
-    znz_pred        : znz -> znz;
-    znz_sub         : znz -> znz -> znz;
-    znz_sub_carry   : znz -> znz -> znz;
-
-    znz_mul_c       : znz -> znz -> zn2z znz;
-    znz_mul         : znz -> znz -> znz;
-    znz_square_c    : znz -> zn2z znz;
+    opp_c       : t -> carry t;
+    opp         : t -> t;
+    opp_carry   : t -> t; (* the carry is known to be -1 *)
+
+    succ_c      : t -> carry t;
+    add_c       : t -> t -> carry t;
+    add_carry_c : t -> t -> carry t;
+    succ        : t -> t;
+    add         : t -> t -> t;
+    add_carry   : t -> t -> t;
+
+    pred_c      : t -> carry t;
+    sub_c       : t -> t -> carry t;
+    sub_carry_c : t -> t -> carry t;
+    pred        : t -> t;
+    sub         : t -> t -> t;
+    sub_carry   : t -> t -> t;
+
+    mul_c       : t -> t -> zn2z t;
+    mul         : t -> t -> t;
+    square_c    : t -> zn2z t;
 
     (* Special divisions operations *)
-    znz_div21       : znz -> znz -> znz -> znz*znz;
-    znz_div_gt      : znz -> znz -> znz * znz; (* specialized version of [znz_div] *)
-    znz_div         : znz -> znz -> znz * znz;
+    div21       : t -> t -> t -> t*t;
+    div_gt      : t -> t -> t * t; (* specialized version of [div] *)
+    div         : t -> t -> t * t;
 
-    znz_mod_gt      : znz -> znz -> znz; (* specialized version of [znz_mod] *)
-    znz_mod         : znz -> znz -> znz;
+    modulo_gt   : t -> t -> t; (* specialized version of [mod] *)
+    modulo      : t -> t -> t;
 
-    znz_gcd_gt      : znz -> znz -> znz; (* specialized version of [znz_gcd] *)
-    znz_gcd         : znz -> znz -> znz;
-    (* [znz_add_mul_div p i j] is a combination of the [(digits-p)]
+    gcd_gt      : t -> t -> t; (* specialized version of [gcd] *)
+    gcd         : t -> t -> t;
+    (* [add_mul_div p i j] is a combination of the [(digits-p)]
        low bits of [i] above the [p] high bits of [j]:
-       [znz_add_mul_div p i j = i*2^p+j/2^(digits-p)] *)
-    znz_add_mul_div : znz -> znz -> znz -> znz;
-    (* [znz_pos_mod p i] is [i mod 2^p] *)
-    znz_pos_mod     : znz -> znz -> znz;
+       [add_mul_div p i j = i*2^p+j/2^(digits-p)] *)
+    add_mul_div : t -> t -> t -> t;
+    (* [pos_mod p i] is [i mod 2^p] *)
+    pos_mod     : t -> t -> t;
 
-    znz_is_even     : znz -> bool;
+    is_even     : t -> bool;
     (* square root *)
-    znz_sqrt2       : znz -> znz -> znz * carry znz;
-    znz_sqrt        : znz -> znz  }.
-
-End Z_nZ_Op.
-
-Section Z_nZ_Spec.
- Variable w : Type.
- Variable w_op : znz_op w.
-
- Let w_digits      := w_op.(znz_digits).
- Let w_zdigits     := w_op.(znz_zdigits).
- Let w_to_Z        := w_op.(znz_to_Z).
- Let w_of_pos      := w_op.(znz_of_pos).
- Let w_head0       := w_op.(znz_head0).
- Let w_tail0       := w_op.(znz_tail0).
-
- Let w0            := w_op.(znz_0).
- Let w1            := w_op.(znz_1).
- Let wBm1          := w_op.(znz_Bm1).
-
- Let w_compare     := w_op.(znz_compare).
- Let w_eq0         := w_op.(znz_eq0).
-
- Let w_opp_c       := w_op.(znz_opp_c).
- Let w_opp         := w_op.(znz_opp).
- Let w_opp_carry   := w_op.(znz_opp_carry).
-
- Let w_succ_c      := w_op.(znz_succ_c).
- Let w_add_c       := w_op.(znz_add_c).
- Let w_add_carry_c := w_op.(znz_add_carry_c).
- Let w_succ        := w_op.(znz_succ).
- Let w_add         := w_op.(znz_add).
- Let w_add_carry   := w_op.(znz_add_carry).
+    sqrt2       : t -> t -> t * carry t;
+    sqrt        : t -> t  }.
 
- Let w_pred_c      := w_op.(znz_pred_c).
- Let w_sub_c       := w_op.(znz_sub_c).
- Let w_sub_carry_c := w_op.(znz_sub_carry_c).
- Let w_pred        := w_op.(znz_pred).
- Let w_sub         := w_op.(znz_sub).
- Let w_sub_carry   := w_op.(znz_sub_carry).
+ Section Specs.
+ Context {t : Type}{ops : Ops t}.
 
- Let w_mul_c       := w_op.(znz_mul_c).
- Let w_mul         := w_op.(znz_mul).
- Let w_square_c    := w_op.(znz_square_c).
+ Notation "[| x |]" := (to_Z x)  (at level 0, x at level 99).
 
- Let w_div21       := w_op.(znz_div21).
- Let w_div_gt      := w_op.(znz_div_gt).
- Let w_div         := w_op.(znz_div).
-
- Let w_mod_gt      := w_op.(znz_mod_gt).
- Let w_mod         := w_op.(znz_mod).
-
- Let w_gcd_gt      := w_op.(znz_gcd_gt).
- Let w_gcd         := w_op.(znz_gcd).
-
- Let w_add_mul_div := w_op.(znz_add_mul_div).
-
- Let w_pos_mod     := w_op.(znz_pos_mod).
-
- Let w_is_even     := w_op.(znz_is_even).
- Let w_sqrt2       := w_op.(znz_sqrt2).
- Let w_sqrt        := w_op.(znz_sqrt).
-
- Notation "[| x |]" := (w_to_Z x)  (at level 0, x at level 99).
-
- Let wB := base w_digits.
+ Let wB := base digits.
 
  Notation "[+| c |]" :=
-   (interp_carry 1 wB w_to_Z c)  (at level 0, x at level 99).
+   (interp_carry 1 wB to_Z c)  (at level 0, x at level 99).
 
  Notation "[-| c |]" :=
-   (interp_carry (-1) wB w_to_Z c)  (at level 0, x at level 99).
+   (interp_carry (-1) wB to_Z c)  (at level 0, x at level 99).
 
  Notation "[|| x ||]" :=
-   (zn2z_to_Z wB w_to_Z x)  (at level 0, x at level 99).
+   (zn2z_to_Z wB to_Z x)  (at level 0, x at level 99).
 
- Record znz_spec := mk_znz_spec {
+ Class Specs := MkSpecs {
 
     (* Conversion functions with Z *)
     spec_to_Z   : forall x, 0 <= [| x |] < wB;
     spec_of_pos : forall p,
-           Zpos p = (Z_of_N (fst (w_of_pos p)))*wB + [|(snd (w_of_pos p))|];
-    spec_zdigits : [| w_zdigits |] = Zpos w_digits;
-    spec_more_than_1_digit: 1 < Zpos w_digits;
+           Zpos p = (Z_of_N (fst (of_pos p)))*wB + [|(snd (of_pos p))|];
+    spec_zdigits : [| zdigits |] = Zpos digits;
+    spec_more_than_1_digit: 1 < Zpos digits;
 
     (* Basic numbers *)
-    spec_0   : [|w0|] = 0;
-    spec_1   : [|w1|] = 1;
-    spec_Bm1 : [|wBm1|] = wB - 1;
+    spec_0   : [|zero|] = 0;
+    spec_1   : [|one|] = 1;
+    spec_m1 : [|minus_one|] = wB - 1;
 
     (* Comparison *)
-    spec_compare :
-     forall x y,
-       match w_compare x y with
-       | Eq => [|x|] = [|y|]
-       | Lt => [|x|] < [|y|]
-       | Gt => [|x|] > [|y|]
-       end;
-    spec_eq0 : forall x, w_eq0 x = true -> [|x|] = 0;
+    spec_compare : forall x y, compare x y = ([|x|] ?= [|y|]);
+    (* NB: the spec of [eq0] is deliberately partial,
+       see DoubleCyclic where [eq0 x = true <-> x = W0] *)
+    spec_eq0 : forall x, eq0 x = true -> [|x|] = 0;
     (* Basic arithmetic operations *)
-    spec_opp_c : forall x, [-|w_opp_c x|] = -[|x|];
-    spec_opp : forall x, [|w_opp x|] = (-[|x|]) mod wB;
-    spec_opp_carry : forall x, [|w_opp_carry x|] = wB - [|x|] - 1;
-
-    spec_succ_c : forall x, [+|w_succ_c x|] = [|x|] + 1;
-    spec_add_c  : forall x y, [+|w_add_c x y|] = [|x|] + [|y|];
-    spec_add_carry_c : forall x y, [+|w_add_carry_c x y|] = [|x|] + [|y|] + 1;
-    spec_succ : forall x, [|w_succ x|] = ([|x|] + 1) mod wB;
-    spec_add : forall x y, [|w_add x y|] = ([|x|] + [|y|]) mod wB;
+    spec_opp_c : forall x, [-|opp_c x|] = -[|x|];
+    spec_opp : forall x, [|opp x|] = (-[|x|]) mod wB;
+    spec_opp_carry : forall x, [|opp_carry x|] = wB - [|x|] - 1;
+
+    spec_succ_c : forall x, [+|succ_c x|] = [|x|] + 1;
+    spec_add_c  : forall x y, [+|add_c x y|] = [|x|] + [|y|];
+    spec_add_carry_c : forall x y, [+|add_carry_c x y|] = [|x|] + [|y|] + 1;
+    spec_succ : forall x, [|succ x|] = ([|x|] + 1) mod wB;
+    spec_add : forall x y, [|add x y|] = ([|x|] + [|y|]) mod wB;
     spec_add_carry :
-	 forall x y, [|w_add_carry x y|] = ([|x|] + [|y|] + 1) mod wB;
+	 forall x y, [|add_carry x y|] = ([|x|] + [|y|] + 1) mod wB;
 
-    spec_pred_c : forall x, [-|w_pred_c x|] = [|x|] - 1;
-    spec_sub_c : forall x y, [-|w_sub_c x y|] = [|x|] - [|y|];
-    spec_sub_carry_c : forall x y, [-|w_sub_carry_c x y|] = [|x|] - [|y|] - 1;
-    spec_pred : forall x, [|w_pred x|] = ([|x|] - 1) mod wB;
-    spec_sub : forall x y, [|w_sub x y|] = ([|x|] - [|y|]) mod wB;
+    spec_pred_c : forall x, [-|pred_c x|] = [|x|] - 1;
+    spec_sub_c : forall x y, [-|sub_c x y|] = [|x|] - [|y|];
+    spec_sub_carry_c : forall x y, [-|sub_carry_c x y|] = [|x|] - [|y|] - 1;
+    spec_pred : forall x, [|pred x|] = ([|x|] - 1) mod wB;
+    spec_sub : forall x y, [|sub x y|] = ([|x|] - [|y|]) mod wB;
     spec_sub_carry :
-	 forall x y, [|w_sub_carry x y|] = ([|x|] - [|y|] - 1) mod wB;
+	 forall x y, [|sub_carry x y|] = ([|x|] - [|y|] - 1) mod wB;
 
-    spec_mul_c : forall x y, [|| w_mul_c x y ||] = [|x|] * [|y|];
-    spec_mul : forall x y, [|w_mul x y|] = ([|x|] * [|y|]) mod wB;
-    spec_square_c : forall x, [|| w_square_c x||] = [|x|] * [|x|];
+    spec_mul_c : forall x y, [|| mul_c x y ||] = [|x|] * [|y|];
+    spec_mul : forall x y, [|mul x y|] = ([|x|] * [|y|]) mod wB;
+    spec_square_c : forall x, [|| square_c x||] = [|x|] * [|x|];
 
     (* Special divisions operations *)
     spec_div21 : forall a1 a2 b,
       wB/2 <= [|b|] ->
       [|a1|] < [|b|] ->
-      let (q,r) := w_div21 a1 a2 b in
+      let (q,r) := div21 a1 a2 b in
       [|a1|] *wB+ [|a2|] = [|q|] * [|b|] + [|r|] /\
       0 <= [|r|] < [|b|];
     spec_div_gt : forall a b, [|a|] > [|b|] -> 0 < [|b|] ->
-      let (q,r) := w_div_gt a b in
+      let (q,r) := div_gt a b in
       [|a|] = [|q|] * [|b|] + [|r|] /\
       0 <= [|r|] < [|b|];
     spec_div : forall a b, 0 < [|b|] ->
-      let (q,r) := w_div a b in
+      let (q,r) := div a b in
       [|a|] = [|q|] * [|b|] + [|r|] /\
       0 <= [|r|] < [|b|];
 
-    spec_mod_gt : forall a b, [|a|] > [|b|] -> 0 < [|b|] ->
-      [|w_mod_gt a b|] = [|a|] mod [|b|];
-    spec_mod :  forall a b, 0 < [|b|] ->
-      [|w_mod a b|] = [|a|] mod [|b|];
+    spec_modulo_gt : forall a b, [|a|] > [|b|] -> 0 < [|b|] ->
+      [|modulo_gt a b|] = [|a|] mod [|b|];
+    spec_modulo :  forall a b, 0 < [|b|] ->
+      [|modulo a b|] = [|a|] mod [|b|];
 
     spec_gcd_gt : forall a b, [|a|] > [|b|] ->
-      Zis_gcd [|a|] [|b|] [|w_gcd_gt a b|];
-    spec_gcd : forall a b, Zis_gcd [|a|] [|b|] [|w_gcd a b|];
+      Zis_gcd [|a|] [|b|] [|gcd_gt a b|];
+    spec_gcd : forall a b, Zis_gcd [|a|] [|b|] [|gcd a b|];
 
 
     (* shift operations *)
-    spec_head00:  forall x, [|x|] = 0 -> [|w_head0 x|] = Zpos w_digits;
+    spec_head00:  forall x, [|x|] = 0 -> [|head0 x|] = Zpos digits;
     spec_head0  : forall x,  0 < [|x|] ->
-	 wB/ 2 <= 2 ^ ([|w_head0 x|]) * [|x|] < wB;
-    spec_tail00:  forall x, [|x|] = 0 -> [|w_tail0 x|] = Zpos w_digits;
+	 wB/ 2 <= 2 ^ ([|head0 x|]) * [|x|] < wB;
+    spec_tail00:  forall x, [|x|] = 0 -> [|tail0 x|] = Zpos digits;
     spec_tail0  : forall x, 0 < [|x|] ->
-         exists y, 0 <= y /\ [|x|] = (2 * y + 1) * (2 ^ [|w_tail0 x|]) ;
+         exists y, 0 <= y /\ [|x|] = (2 * y + 1) * (2 ^ [|tail0 x|]) ;
     spec_add_mul_div : forall x y p,
-       [|p|] <= Zpos w_digits ->
-       [| w_add_mul_div p x y |] =
+       [|p|] <= Zpos digits ->
+       [| add_mul_div p x y |] =
          ([|x|] * (2 ^ [|p|]) +
-          [|y|] / (2 ^ ((Zpos w_digits) - [|p|]))) mod wB;
+          [|y|] / (2 ^ ((Zpos digits) - [|p|]))) mod wB;
     spec_pos_mod : forall w p,
-       [|w_pos_mod p w|] = [|w|] mod (2 ^ [|p|]);
+       [|pos_mod p w|] = [|w|] mod (2 ^ [|p|]);
     (* sqrt *)
     spec_is_even : forall x,
-      if w_is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1;
+      if is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1;
     spec_sqrt2 : forall x y,
        wB/ 4 <= [|x|] ->
-       let (s,r) := w_sqrt2 x y in
+       let (s,r) := sqrt2 x y in
           [||WW x y||] = [|s|] ^ 2 + [+|r|] /\
           [+|r|] <= 2 * [|s|];
     spec_sqrt : forall x,
-       [|w_sqrt x|] ^ 2 <= [|x|] < ([|w_sqrt x|] + 1) ^ 2
+       [|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2
   }.
 
-End Z_nZ_Spec.
+ End Specs.
+
+ Implicit Arguments Specs [[t]].
 
-(** Generic construction of double words *)
+ (** Generic construction of double words *)
 
-Section WW.
+ Section WW.
 
- Variable w : Type.
- Variable w_op : znz_op w.
- Variable op_spec : znz_spec w_op.
+ Context {t : Type}{ops : Ops t}{specs : Specs ops}.
 
- Let wB := base w_op.(znz_digits).
- Let w_to_Z := w_op.(znz_to_Z).
- Let w_eq0 := w_op.(znz_eq0).
- Let w_0 := w_op.(znz_0).
+ Let wB := base digits.
 
- Definition znz_W0 h :=
-  if w_eq0 h then W0 else WW h w_0.
+ Definition WO h :=
+  if eq0 h then W0 else WW h zero.
 
- Definition znz_0W l :=
-  if w_eq0 l then W0 else WW w_0 l.
+ Definition OW l :=
+  if eq0 l then W0 else WW zero l.
 
- Definition znz_WW h l :=
-  if w_eq0 h then znz_0W l else WW h l.
+ Definition WW h l :=
+  if eq0 h then OW l else WW h l.
 
- Lemma spec_W0 : forall h,
-   zn2z_to_Z wB w_to_Z (znz_W0 h) = (w_to_Z h)*wB.
+ Lemma spec_WO : forall h,
+   zn2z_to_Z wB to_Z (WO h) = (to_Z h)*wB.
  Proof.
- unfold zn2z_to_Z, znz_W0, w_to_Z; simpl; intros.
- case_eq (w_eq0 h); intros.
- rewrite (op_spec.(spec_eq0) _ H); auto.
- unfold w_0; rewrite op_spec.(spec_0); auto with zarith.
+ unfold zn2z_to_Z, WO; simpl; intros.
+ case_eq (eq0 h); intros.
+ rewrite (spec_eq0 _ H); auto.
+ rewrite spec_0; auto with zarith.
  Qed.
 
- Lemma spec_0W : forall l,
-   zn2z_to_Z wB w_to_Z (znz_0W l) = w_to_Z l.
+ Lemma spec_OW : forall l,
+   zn2z_to_Z wB to_Z (OW l) = to_Z l.
  Proof.
- unfold zn2z_to_Z, znz_0W, w_to_Z; simpl; intros.
- case_eq (w_eq0 l); intros.
- rewrite (op_spec.(spec_eq0) _ H); auto.
- unfold w_0; rewrite op_spec.(spec_0); auto with zarith.
+ unfold zn2z_to_Z, OW; simpl; intros.
+ case_eq (eq0 l); intros.
+ rewrite (spec_eq0 _ H); auto.
+ rewrite spec_0; auto with zarith.
  Qed.
 
  Lemma spec_WW : forall h l,
-  zn2z_to_Z wB w_to_Z (znz_WW h l) = (w_to_Z h)*wB + w_to_Z l.
+  zn2z_to_Z wB to_Z (WW h l) = (to_Z h)*wB + to_Z l.
  Proof.
- unfold znz_WW, w_to_Z; simpl; intros.
- case_eq (w_eq0 h); intros.
- rewrite (op_spec.(spec_eq0) _ H); auto.
- rewrite spec_0W; auto.
+ unfold WW; simpl; intros.
+ case_eq (eq0 h); intros.
+ rewrite (spec_eq0 _ H); auto.
+ rewrite spec_OW; auto.
  simpl; auto.
  Qed.
 
-End WW.
+ End WW.
 
-(** Injecting [Z] numbers into a cyclic structure *)
+ (** Injecting [Z] numbers into a cyclic structure *)
 
-Section znz_of_pos.
+ Section Of_Z.
 
- Variable w : Type.
- Variable w_op : znz_op w.
- Variable op_spec : znz_spec w_op.
+ Context {t : Type}{ops : Ops t}{specs : Specs ops}.
 
- Notation "[| x |]" := (znz_to_Z w_op x)  (at level 0, x at level 99).
+ Notation "[| x |]" := (to_Z x)  (at level 0, x at level 99).
 
- Definition znz_of_Z (w:Type) (op:znz_op w) z :=
- match z with
- | Zpos p => snd (op.(znz_of_pos) p)
- | _ => op.(znz_0)
- end.
-
- Theorem znz_of_pos_correct:
-   forall p, Zpos p < base (znz_digits w_op) -> [|(snd (znz_of_pos w_op p))|] = Zpos p.
+ Theorem of_pos_correct:
+   forall p, Zpos p < base digits -> [|(snd (of_pos p))|] = Zpos p.
+ Proof.
  intros p Hp.
- generalize (spec_of_pos op_spec p).
- case (znz_of_pos w_op p); intros n w1; simpl.
+ generalize (spec_of_pos p).
+ case (of_pos p); intros n w1; simpl.
  case n; simpl Npos; auto with zarith.
  intros p1 Hp1; contradict Hp; apply Zle_not_lt.
- rewrite Hp1; auto with zarith.
- match goal with |- _ <= ?X + ?Y =>
-  apply Zle_trans with X; auto with zarith
- end.
- match goal with |- ?X <= _ =>
-  pattern X at 1; rewrite <- (Zmult_1_l);
-  apply Zmult_le_compat_r; auto with zarith
- end.
+ replace (base digits) with (1 * base digits + 0) by auto with zarith.
+ rewrite Hp1.
+ apply Zplus_le_compat.
+ apply Zmult_le_compat; auto with zarith.
  case p1; simpl; intros; red; simpl; intros; discriminate.
  unfold base; auto with zarith.
- case (spec_to_Z op_spec w1); auto with zarith.
+ case (spec_to_Z w1); auto with zarith.
  Qed.
 
- Theorem znz_of_Z_correct:
-   forall p, 0 <= p < base (znz_digits w_op) -> [|znz_of_Z w_op p|] = p.
+ Definition of_Z z :=
+ match z with
+ | Zpos p => snd (of_pos p)
+ | _ => zero
+ end.
+
+ Theorem of_Z_correct:
+   forall p, 0 <= p < base digits -> [|of_Z p|] = p.
+ Proof.
  intros p; case p; simpl; try rewrite spec_0; auto.
- intros; rewrite znz_of_pos_correct; auto with zarith.
+ intros; rewrite of_pos_correct; auto with zarith.
  intros p1 (H1, _); contradict H1; apply Zlt_not_le; red; simpl; auto.
  Qed.
-End znz_of_pos.
 
+ End Of_Z.
+
+End ZnZ.
 
 (** A modular specification grouping the earlier records. *)
 
 Module Type CyclicType.
- Parameter w : Type.
- Parameter w_op : znz_op w.
- Parameter w_spec : znz_spec w_op.
+ Parameter t : Type.
+ Declare Instance ops : ZnZ.Ops t.
+ Declare Instance specs : ZnZ.Specs ops.
 End CyclicType.
 
 
@@ -379,38 +311,29 @@ End CyclicType.
 
 Module CyclicRing (Import Cyclic : CyclicType).
 
-Definition t := w.
-
-Local Notation "[| x |]" := (w_op.(znz_to_Z) x) (at level 0, x at level 99).
+Local Notation "[| x |]" := (ZnZ.to_Z x) (at level 0, x at level 99).
 
 Definition eq (n m : t) := [| n |] = [| m |].
-Definition zero : t := w_op.(znz_0).
-Definition one := w_op.(znz_1).
-Definition add := w_op.(znz_add).
-Definition sub := w_op.(znz_sub).
-Definition mul := w_op.(znz_mul).
-Definition opp := w_op.(znz_opp).
 
 Local Infix "=="  := eq (at level 70).
-Local Notation "0" := zero.
-Local Notation "1" := one.
-Local Infix "+" := add.
-Local Infix "-" := sub.
-Local Infix "*" := mul.
-Local Notation "!!" := (base (znz_digits w_op)).
-
-Hint Rewrite
- w_spec.(spec_0) w_spec.(spec_1)
- w_spec.(spec_add) w_spec.(spec_mul) w_spec.(spec_opp) w_spec.(spec_sub)
+Local Notation "0" := ZnZ.zero.
+Local Notation "1" := ZnZ.one.
+Local Infix "+" := ZnZ.add.
+Local Infix "-" := ZnZ.sub.
+Local Notation "- x" := (ZnZ.opp x).
+Local Infix "*" := ZnZ.mul.
+Local Notation wB := (base ZnZ.digits).
+
+Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_add ZnZ.spec_mul
+ ZnZ.spec_opp ZnZ.spec_sub
  : cyclic.
 
-Ltac zify :=
- unfold eq, zero, one, add, sub, mul, opp in *; autorewrite with cyclic.
+Ltac zify := unfold eq in *; autorewrite with cyclic.
 
 Lemma add_0_l : forall x, 0 + x == x.
 Proof.
 intros. zify. rewrite Zplus_0_l.
-apply Zmod_small. apply w_spec.(spec_to_Z).
+apply Zmod_small. apply ZnZ.spec_to_Z.
 Qed.
 
 Lemma add_comm : forall x y, x + y == y + x.
@@ -426,7 +349,7 @@ Qed.
 Lemma mul_1_l : forall x, 1 * x == x.
 Proof.
 intros. zify. rewrite Zmult_1_l.
-apply Zmod_small. apply w_spec.(spec_to_Z).
+apply Zmod_small. apply ZnZ.spec_to_Z.
 Qed.
 
 Lemma mul_comm : forall x y, x * y == y * x.
@@ -444,22 +367,22 @@ Proof.
 intros. zify. now rewrite <- Zplus_mod, Zmult_mod_idemp_l, Zmult_plus_distr_l.
 Qed.
 
-Lemma add_opp_r : forall x y, x + opp y == x-y.
+Lemma add_opp_r : forall x y, x + - y == x-y.
 Proof.
 intros. zify. rewrite <- Zminus_mod_idemp_r. unfold Zminus.
-destruct (Z_eq_dec ([|y|] mod !!) 0) as [EQ|NEQ].
+destruct (Z_eq_dec ([|y|] mod wB) 0) as [EQ|NEQ].
 rewrite Z_mod_zero_opp_full, EQ, 2 Zplus_0_r; auto.
 rewrite Z_mod_nz_opp_full by auto.
 rewrite <- Zplus_mod_idemp_r, <- Zminus_mod_idemp_l.
 rewrite Z_mod_same_full. simpl. now rewrite Zplus_mod_idemp_r.
 Qed.
 
-Lemma add_opp_diag_r : forall x, x + opp x == 0.
+Lemma add_opp_diag_r : forall x, x + - x == 0.
 Proof.
 intros. red. rewrite add_opp_r. zify. now rewrite Zminus_diag, Zmod_0_l.
 Qed.
 
-Lemma CyclicRing : ring_theory 0 1 add mul sub opp eq.
+Lemma CyclicRing : ring_theory 0 1 ZnZ.add ZnZ.mul ZnZ.sub ZnZ.opp eq.
 Proof.
 constructor.
 exact add_0_l. exact add_comm. exact add_assoc.
@@ -470,13 +393,24 @@ exact add_opp_diag_r.
 Qed.
 
 Definition eqb x y :=
- match w_op.(znz_compare) x y with Eq => true | _ => false end.
+ match ZnZ.compare x y with Eq => true | _ => false end.
+
+Lemma eqb_eq : forall x y, eqb x y = true <-> x == y.
+Proof.
+ intros. unfold eqb, eq.
+ rewrite ZnZ.spec_compare.
+ case Zcompare_spec; intuition; try discriminate.
+Qed.
 
+(* POUR HUGO:
 Lemma eqb_eq : forall x y, eqb x y = true <-> x == y.
 Proof.
- intros. unfold eqb, eq. generalize (w_spec.(spec_compare) x y).
- destruct (w_op.(znz_compare) x y); intuition; try discriminate.
+ intros. unfold eqb, eq. generalize (ZnZ.spec_compare x y).
+ case (ZnZ.compare x y); intuition; try discriminate.
+ (* BUG ?! using destruct instead of case won't work:
+   it gives 3 subcases, but ZnZ.compare x y is still there in them! *)
 Qed.
+*)
 
 Lemma eqb_correct : forall x y, eqb x y = true -> x==y.
 Proof. now apply eqb_eq. Qed.
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index 517e48ad9..b68e89560 100644
--- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v
+++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -27,21 +27,17 @@ Module NZCyclicAxiomsMod (Import Cyclic : CyclicType) <: NZAxiomsSig.
 
 Local Open Scope Z_scope.
 
-Definition t := w.
+Local Notation wB := (base ZnZ.digits).
 
-Definition NZ_to_Z : t -> Z := znz_to_Z w_op.
-Definition Z_to_NZ : Z -> t := znz_of_Z w_op.
-Local Notation wB := (base w_op.(znz_digits)).
-
-Local Notation "[| x |]" := (w_op.(znz_to_Z) x) (at level 0, x at level 99).
+Local Notation "[| x |]" := (ZnZ.to_Z x) (at level 0, x at level 99).
 
 Definition eq (n m : t) := [| n |] = [| m |].
-Definition zero := w_op.(znz_0).
-Definition succ := w_op.(znz_succ).
-Definition pred := w_op.(znz_pred).
-Definition add := w_op.(znz_add).
-Definition sub := w_op.(znz_sub).
-Definition mul := w_op.(znz_mul).
+Definition zero := ZnZ.zero.
+Definition succ := ZnZ.succ.
+Definition pred := ZnZ.pred.
+Definition add := ZnZ.add.
+Definition sub := ZnZ.sub.
+Definition mul := ZnZ.mul.
 
 Local Infix "=="  := eq (at level 70).
 Local Notation "0" := zero.
@@ -51,41 +47,25 @@ Local Infix "+" := add.
 Local Infix "-" := sub.
 Local Infix "*" := mul.
 
-Hint Rewrite w_spec.(spec_0) w_spec.(spec_succ) w_spec.(spec_pred)
- w_spec.(spec_add) w_spec.(spec_mul) w_spec.(spec_sub) : w.
-Ltac wsimpl :=
- unfold eq, zero, succ, pred, add, sub, mul; autorewrite with w.
-Ltac wcongruence := repeat red; intros; wsimpl; congruence.
+Hint Rewrite ZnZ.spec_0 ZnZ.spec_succ ZnZ.spec_pred
+ ZnZ.spec_add ZnZ.spec_mul ZnZ.spec_sub : cyclic.
+Ltac zify :=
+ unfold eq, zero, succ, pred, add, sub, mul in *;
+ autorewrite with cyclic.
+Ltac zcongruence := repeat red; intros; zify; congruence.
 
 Instance eq_equiv : Equivalence eq.
 Proof.
 unfold eq. firstorder.
 Qed.
 
-Instance succ_wd : Proper (eq ==> eq) succ.
-Proof.
-wcongruence.
-Qed.
-
-Instance pred_wd : Proper (eq ==> eq) pred.
-Proof.
-wcongruence.
-Qed.
+Local Obligation Tactic := zcongruence.
 
-Instance add_wd : Proper (eq ==> eq ==> eq) add.
-Proof.
-wcongruence.
-Qed.
-
-Instance sub_wd : Proper (eq ==> eq ==> eq) sub.
-Proof.
-wcongruence.
-Qed.
-
-Instance mul_wd : Proper (eq ==> eq ==> eq) mul.
-Proof.
-wcongruence.
-Qed.
+Program Instance succ_wd : Proper (eq ==> eq) succ.
+Program Instance pred_wd : Proper (eq ==> eq) pred.
+Program Instance add_wd : Proper (eq ==> eq ==> eq) add.
+Program Instance sub_wd : Proper (eq ==> eq ==> eq) sub.
+Program Instance mul_wd : Proper (eq ==> eq ==> eq) mul.
 
 Theorem gt_wB_1 : 1 < wB.
 Proof.
@@ -115,23 +95,16 @@ Qed.
 
 Lemma NZ_to_Z_mod : forall n, [| n |] mod wB = [| n |].
 Proof.
-intro n; rewrite Zmod_small. reflexivity. apply w_spec.(spec_to_Z).
+intro n; rewrite Zmod_small. reflexivity. apply ZnZ.spec_to_Z.
 Qed.
 
 Theorem pred_succ : forall n, P (S n) == n.
 Proof.
-intro n. wsimpl.
+intro n. zify.
 rewrite <- pred_mod_wB.
 replace ([| n |] + 1 - 1)%Z with [| n |] by auto with zarith. apply NZ_to_Z_mod.
 Qed.
 
-Lemma Z_to_NZ_0 : Z_to_NZ 0%Z == 0.
-Proof.
-unfold NZ_to_Z, Z_to_NZ. wsimpl.
-rewrite znz_of_Z_correct; auto.
-exact w_spec. split; [auto with zarith |apply gt_wB_0].
-Qed.
-
 Section Induction.
 
 Variable A : t -> Prop.
@@ -140,21 +113,22 @@ Hypothesis A0 : A 0.
 Hypothesis AS : forall n, A n <-> A (S n).
  (* Below, we use only -> direction *)
 
-Let B (n : Z) := A (Z_to_NZ n).
+Let B (n : Z) := A (ZnZ.of_Z n).
 
 Lemma B0 : B 0.
 Proof.
-unfold B. now rewrite Z_to_NZ_0.
+unfold B.
+setoid_replace (ZnZ.of_Z 0) with zero. assumption.
+red; zify. apply ZnZ.of_Z_correct. auto using gt_wB_0 with zarith.
 Qed.
 
 Lemma BS : forall n : Z, 0 <= n -> n < wB - 1 -> B n -> B (n + 1).
 Proof.
 intros n H1 H2 H3.
 unfold B in *. apply -> AS in H3.
-setoid_replace (Z_to_NZ (n + 1)) with (S (Z_to_NZ n)). assumption.
-wsimpl.
-unfold NZ_to_Z, Z_to_NZ.
-do 2 (rewrite znz_of_Z_correct; [ | exact w_spec | auto with zarith]).
+setoid_replace (ZnZ.of_Z (n + 1)) with (S (ZnZ.of_Z n)). assumption.
+zify.
+rewrite 2 ZnZ.of_Z_correct; auto with zarith.
 symmetry; apply Zmod_small; auto with zarith.
 Qed.
 
@@ -167,25 +141,23 @@ Qed.
 
 Theorem bi_induction : forall n, A n.
 Proof.
-intro n. setoid_replace n with (Z_to_NZ (NZ_to_Z n)).
-apply B_holds. apply w_spec.(spec_to_Z).
-unfold eq, NZ_to_Z, Z_to_NZ; rewrite znz_of_Z_correct.
-reflexivity.
-exact w_spec.
-apply w_spec.(spec_to_Z).
+intro n. setoid_replace n with (ZnZ.of_Z (ZnZ.to_Z n)).
+apply B_holds. apply ZnZ.spec_to_Z.
+red. symmetry. apply ZnZ.of_Z_correct.
+apply ZnZ.spec_to_Z.
 Qed.
 
 End Induction.
 
 Theorem add_0_l : forall n, 0 + n == n.
 Proof.
-intro n. wsimpl.
-rewrite Zplus_0_l. rewrite Zmod_small; [reflexivity | apply w_spec.(spec_to_Z)].
+intro n. zify.
+rewrite Zplus_0_l. apply Zmod_small. apply ZnZ.spec_to_Z.
 Qed.
 
 Theorem add_succ_l : forall n m, (S n) + m == S (n + m).
 Proof.
-intros n m. wsimpl.
+intros n m. zify.
 rewrite succ_mod_wB. repeat rewrite Zplus_mod_idemp_l; try apply gt_wB_0.
 rewrite <- (Zplus_assoc ([| n |] mod wB) 1 [| m |]). rewrite Zplus_mod_idemp_l.
 rewrite (Zplus_comm 1 [| m |]); now rewrite Zplus_assoc.
@@ -193,25 +165,27 @@ Qed.
 
 Theorem sub_0_r : forall n, n - 0 == n.
 Proof.
-intro n. wsimpl. rewrite Zminus_0_r. apply NZ_to_Z_mod.
+intro n. zify. rewrite Zminus_0_r. apply NZ_to_Z_mod.
 Qed.
 
 Theorem sub_succ_r : forall n m, n - (S m) == P (n - m).
 Proof.
-intros n m. wsimpl. rewrite Zminus_mod_idemp_r, Zminus_mod_idemp_l.
+intros n m. zify. rewrite Zminus_mod_idemp_r, Zminus_mod_idemp_l.
 now replace ([|n|] - ([|m|] + 1))%Z with ([|n|] - [|m|] - 1)%Z
      by auto with zarith.
 Qed.
 
 Theorem mul_0_l : forall n, 0 * n == 0.
 Proof.
-intro n. wsimpl. now rewrite Zmult_0_l.
+intro n. now zify.
 Qed.
 
 Theorem mul_succ_l : forall n m, (S n) * m == n * m + m.
 Proof.
-intros n m. wsimpl. rewrite Zplus_mod_idemp_l, Zmult_mod_idemp_l.
+intros n m. zify. rewrite Zplus_mod_idemp_l, Zmult_mod_idemp_l.
 now rewrite Zmult_plus_distr_l, Zmult_1_l.
 Qed.
 
+Definition t := t.
+
 End NZCyclicAxiomsMod.