Enhance the BigN and BigZ infrastructure:

 * Isolate and put forward the interfaces NSig and ZSig that describe
   what should contain structures of natural numbers and integers (specs 
   are done by translation to ZArith).

 * Functors NSigNAxioms and ZSigZAxioms proving that these NSig and 
   ZSig implements the fully-abstract NAxioms and ZAxioms module types.
   
 * BigN and BigZ now contains more notations, plus an export of all 
   abstract results proved by Evgeny instantiated thanks to NSigNAxioms
   and ZSigZAxioms. In addition, BigN and BigZ are declared as 
   (semi/full)-rings.

 * as a consequence, some incompatibities have to be fixed in BigQ: 
   - take care of some name masking (via Import, Open Scope ...)
   - some additionnal constants like BigN.lt to deal with



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

1 files changed, 14 insertions, 3 deletions

diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 22a4b200a..534b680e2 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -79,8 +79,9 @@ let _ =
   pr "Require Import Nbasic.";
   pr "Require Import Wf_nat.";
   pr "Require Import StreamMemo.";
+  pr "Require Import NSig.";
   pr "";
-  pr "Module Make (Import W0:CyclicType).";
+  pr "Module Make (Import W0:CyclicType) <: NType.";
   pr "";
 
   pr " Definition w0 := W0.w.";
@@ -163,8 +164,13 @@ let _ =
 
   pr " Open Scope Z_scope.";
   pr " Notation \"[ x ]\" := (to_Z x).";
-  pr " ";
+  pr "";
 
+  pr " Definition to_N x := Zabs_N (to_Z x).";
+  pr "";
+  
+  pr " Definition eq x y := (to_Z x = to_Z y).";
+  pr "";
 
   pp " (* Regular make op (no karatsuba) *)";
   pp " Fixpoint nmake_op (ww:Type) (ww_op: znz_op ww) (n: nat) : ";
@@ -1315,6 +1321,12 @@ let _ =
   pr "      comparenm).";
   pr "";
 
+  pr " Definition lt n m := compare n m = Lt.";
+  pr " Definition le n m := compare n m <> Gt.";
+  pr " Definition min n m := match compare n m with Gt => m | _ => n end.";
+  pr " Definition max n m := match compare n m with Lt => m | _ => n end.";
+  pr "";
+
   for i = 0 to size do
     pp " Let spec_compare_%i: forall x y," i;
     pp "    match compare_%i x y with " i;
@@ -2396,7 +2408,6 @@ let _ =
   pr "  end.";
   pr "";
 
-
   pr " Theorem spec_of_N: forall x,";
   pr "   [of_N x] = Z_of_N x.";
   pa " Admitted.";