Filename ZnZ (or Z_nZ in a later attempt) is neither pretty nor accurate

(n _must_ in fact be a power of 2). Worse: Z_31Z is just plain wrong
since it is Z/(2^31)Z and not Z/31Z (my fault). 

As a consequence, switch to CyclicAxioms, Cyclic31, DoubleCyclic, etc



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

8 files changed, 35 insertions, 27 deletions

diff --git a/Makefile.common b/Makefile.common
index 48e6dff14..a6596d59b 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -617,15 +617,15 @@ NUMBERSCOMMONVO:=$(addprefix theories/Numbers/, \
  QRewrite.vo	NumPrelude.vo	BigNumPrelude.vo )
 
 CYCLICABSTRACTVO:=$(addprefix theories/Numbers/Cyclic/Abstract/, \
- Z_nZ.vo NZCyclic.vo )
+ CyclicAxioms.vo NZCyclic.vo )
 
 CYCLICINT31VO:=$(addprefix theories/Numbers/Cyclic/Int31/, \
- Int31.vo Z_31Z.vo )
+ Int31.vo Cyclic31.vo )
 
 CYCLICDOUBLECYCLICVO:=$(addprefix theories/Numbers/Cyclic/DoubleCyclic/, \
  DoubleType.vo	DoubleBase.vo	DoubleAdd.vo	DoubleSub.vo	\
  DoubleMul.vo	DoubleDivn1.vo 	DoubleDiv.vo	DoubleSqrt.vo	\
- DoubleLift.vo 	Z_2nZ.vo )
+ DoubleLift.vo 	DoubleCyclic.vo )
 
 CYCLICVO:=$(CYCLICABSTRACTVO) $(CYCLICINT31VO) $(CYCLICDOUBLECYCLICVO)
 
diff --git a/theories/Numbers/Cyclic/Abstract/Z_nZ.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 6d19e6613..ed14cc799 100644
--- a/theories/Numbers/Cyclic/Abstract/Z_nZ.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -12,6 +12,9 @@
 
 (** * Signature and specification of a bounded integer structure *)
 
+(** This file specifies how to represent [Z/nZ] when [n=2^d], 
+    [d] being the number of digits of these bounded integers. *) 
+
 Set Implicit Arguments.
 
 Require Import ZArith.
@@ -30,7 +33,7 @@ Section Z_nZ_Op.
  Record znz_op : Set := mk_znz_op {
 
     (* Conversion functions with Z *)
-    znz_digits : positive;
+    znz_digits : positive;  
     znz_zdigits: znz;
     znz_to_Z   : znz -> Z;
     znz_of_pos : positive -> N * znz;
@@ -40,7 +43,7 @@ Section Z_nZ_Op.
     (* Basic constructors *)
     znz_0   : znz;
     znz_1   : znz;
-    znz_Bm1 : znz;
+    znz_Bm1 : znz;  (* [2^digits-1], which is equivalent to [-1] *)
     znz_WW  : znz -> znz -> zn2z znz;
     znz_W0  : znz -> zn2z znz;
     znz_0W  : znz -> zn2z znz;
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index df3af4b63..2d23a12dd 100644
--- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v
+++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -13,10 +13,15 @@
 Require Export NZAxioms.
 Require Import BigNumPrelude.
 Require Import DoubleType.
-Require Import Z_nZ.
+Require Import CyclicAxioms.
 
-(** * A Z/nZ representation (module type [CyclicType]) implements 
-  [NZAxiomsSig], e.g. the common properties between N and Z. *)
+(** * From [CyclicType] to [NZAxiomsSig] *)
+
+(** A [Z/nZ] representation given by a module type [CyclicType] 
+    implements [NZAxiomsSig], e.g. the common properties between 
+    N and Z with no ordering. Notice that the [n] in [Z/nZ] is 
+    a power of 2.
+*)
 
 Module NZCyclicAxiomsMod (Import Cyclic : CyclicType) <: NZAxiomsSig.
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/Z_2nZ.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
index 26d2393f9..54ff3d354 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/Z_2nZ.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
@@ -23,7 +23,7 @@ Require Import DoubleSqrt.
 Require Import DoubleLift.
 Require Import DoubleDivn1.
 Require Import DoubleDiv. 
-Require Import Z_nZ.
+Require Import CyclicAxioms.
 
 Open Local Scope Z_scope.
 
diff --git a/theories/Numbers/Cyclic/Int31/Z_31Z.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index 3b5944ed3..49a1a0b5b 100644
--- a/theories/Numbers/Cyclic/Int31/Z_31Z.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -8,14 +8,14 @@
 
 (*i $Id$ i*)
 
-(** * Int31 numbers defines indeed a cyclic structure : Z/31Z *)
+(** * Int31 numbers defines indeed a cyclic structure : Z/(2^31)Z *)
 
 (**
 Author: Arnaud Spiwack
 *)
 
 Require Export Int31.
-Require Import Z_nZ.
+Require Import CyclicAxioms.
 
 Open Scope int31_scope.
 
@@ -107,8 +107,8 @@ Definition int31_spec : znz_spec int31_op.
 Admitted.
 
 
-Module Int31_words <: CyclicType.
+Module Int31Cyclic <: CyclicType.
   Definition w := int31.
   Definition w_op := int31_op.
   Definition w_spec := int31_spec.
-End Int31_words.
+End Int31Cyclic.
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 25a39aeba..033364f72 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -15,13 +15,13 @@ Author: Arnaud Spiwack
 *)
 
 Require Export Int31.
-Require Import Z_nZ.
-Require Import Z_31Z.
+Require Import CyclicAxioms.
+Require Import Cyclic31.
 Require Import NMake.
 
 Open Scope int31_scope.
 
-Module BigN := NMake.Make Int31_words.
+Module BigN := NMake.Make Int31Cyclic.
 
 Definition bigN := BigN.t.
 
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 3d098c755..d15006cb4 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -71,11 +71,11 @@ let _ =
   pr "";
   pr "Require Import BigNumPrelude.";
   pr "Require Import ZArith.";
+  pr "Require Import CyclicAxioms.";
   pr "Require Import DoubleType.";
   pr "Require Import DoubleMul.";
   pr "Require Import DoubleDivn1.";
-  pr "Require Import Z_nZ.";
-  pr "Require Import Z_2nZ.";
+  pr "Require Import DoubleCyclic.";
   pr "Require Import Nbasic.";
   pr "Require Import Wf_nat.";
   pr "Require Import StreamMemo.";
@@ -1776,7 +1776,7 @@ let _ =
   pp "    (spec_zdigits ww_spec)";
   pp "   (spec_0 ww_spec) (spec_WW ww_spec) (spec_head0 ww_spec)";
   pp "   (spec_add_mul_div ww_spec) (spec_div21 ww_spec) ";
-  pp "    (Z_nZ.spec_compare ww_spec) (Z_nZ.spec_sub ww_spec)).";
+  pp "    (CyclicAxioms.spec_compare ww_spec) (CyclicAxioms.spec_sub ww_spec)).";
   pp "";
 
   for i = 0 to size do
@@ -2018,7 +2018,7 @@ let _ =
   pp "    (spec_zdigits ww_spec)";
   pp "   (spec_0 ww_spec) (spec_WW ww_spec) (spec_head0 ww_spec)";
   pp "   (spec_add_mul_div ww_spec) (spec_div21 ww_spec) ";
-  pp "    (Z_nZ.spec_compare ww_spec) (Z_nZ.spec_sub ww_spec)).";
+  pp "    (CyclicAxioms.spec_compare ww_spec) (CyclicAxioms.spec_sub ww_spec)).";
   pp "";
 
   pr " Theorem spec_mod_gt:";
@@ -2576,7 +2576,7 @@ let _ =
   pp "                ).";
   pp "     rewrite (spec_0 Hw).";
   pp "     rewrite Zmult_0_l; rewrite Zplus_0_l.";
-  pp "     rewrite (Z_nZ.spec_sub Hw).";
+  pp "     rewrite (CyclicAxioms.spec_sub Hw).";
   pp "     rewrite Zmod_small; auto with zarith.";
   pp "     rewrite (spec_zdigits Hw).";
   pp "     rewrite F0.";
@@ -2754,7 +2754,7 @@ let _ =
   pp "     assert (F1: znz_to_Z ww1_op (znz_head0 ww1_op xx) <= Zpos (znz_digits ww1_op)).";
   pp "     case (Zle_lt_or_eq _ _ HH1); intros HH5.";
   pp "     apply Zlt_le_weak.";
-  pp "     case (Z_nZ.spec_head0 Hw1 xx).";
+  pp "     case (CyclicAxioms.spec_head0 Hw1 xx).";
   pp "       rewrite <- Hx; auto.";
   pp "     intros _ Hu; unfold base in Hu.";
   pp "     case (Zle_or_lt (Zpos (znz_digits ww1_op))";
@@ -2766,7 +2766,7 @@ let _ =
   pp "       apply Zle_lt_trans with (2 := Hu).";
   pp "       apply Zmult_le_compat_l; auto with zarith.";
   pp "     apply Zpower_le_monotone; auto with zarith.";
-  pp "     rewrite (Z_nZ.spec_head00 Hw1 xx); auto with zarith.";
+  pp "     rewrite (CyclicAxioms.spec_head00 Hw1 xx); auto with zarith.";
   pp "     rewrite Zdiv_0_l; auto with zarith.";
   pp "     rewrite Zplus_0_r.";
   pp "     case (Zle_lt_or_eq _ _ HH1); intros HH5.";
@@ -2779,7 +2779,7 @@ let _ =
   pp "     split; auto with zarith .";
   pp "     apply Zlt_le_trans with (base (znz_digits ww1_op)).";
   pp "     rewrite Hx.";
-  pp "     case (Z_nZ.spec_head0 Hw1 xx); auto.";
+  pp "     case (CyclicAxioms.spec_head0 Hw1 xx); auto.";
   pp "       rewrite <- Hx; auto.";
   pp "     intros _ Hu; rewrite Zmult_comm in Hu.";
   pp "     apply Zle_lt_trans with (2 := Hu).";
@@ -2794,7 +2794,7 @@ let _ =
   pp "     rewrite Zmod_small; auto with zarith.";
   pp "     intros HH; apply HH.";
   pp "     rewrite Hy; apply Zle_trans with (1 := Hl).";
-  pp "     rewrite (Z_nZ.spec_head00 Hw1 xx); auto with zarith.";
+  pp "     rewrite (CyclicAxioms.spec_head00 Hw1 xx); auto with zarith.";
   pp "     rewrite <- (spec_zdigits Hw); auto with zarith.";
   pp "     rewrite <- (spec_zdigits Hw1); auto with zarith.";
   pp "  assert (F5: forall n m, (n <= m)%snat ->" "%";
diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v
index ea472c860..ed7a7871f 100644
--- a/theories/Numbers/Natural/BigN/Nbasic.v
+++ b/theories/Numbers/Natural/BigN/Nbasic.v
@@ -15,8 +15,8 @@ Require Import BigNumPrelude.
 Require Import Max.
 Require Import DoubleType.
 Require Import DoubleBase.
-Require Import Z_nZ.
-Require Import Z_2nZ.
+Require Import CyclicAxioms.
+Require Import DoubleCyclic.
 
 (* To compute the necessary height *)