aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.common6
-rw-r--r--theories/Numbers/Cyclic/Abstract/CyclicAxioms.v (renamed from theories/Numbers/Cyclic/Abstract/Z_nZ.v)7
-rw-r--r--theories/Numbers/Cyclic/Abstract/NZCyclic.v11
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v (renamed from theories/Numbers/Cyclic/DoubleCyclic/Z_2nZ.v)2
-rw-r--r--theories/Numbers/Cyclic/Int31/Cyclic31.v (renamed from theories/Numbers/Cyclic/Int31/Z_31Z.v)8
-rw-r--r--theories/Numbers/Natural/BigN/BigN.v6
-rw-r--r--theories/Numbers/Natural/BigN/NMake_gen.ml18
-rw-r--r--theories/Numbers/Natural/BigN/Nbasic.v4
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 *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 19:39:49 +0000