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

2 files changed, 96 insertions, 118 deletions

diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 934fbc428..d2f9b0a02 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -11,50 +11,99 @@
 (*i $Id$ i*)
 
 Require Export BigN.
+Require Import ZTimesOrder.
+Require Import ZSig.
+Require Import ZSigZAxioms.
 Require Import ZMake.
 
+Module BigZ <: ZType := ZMake.Make BigN.
 
-Module BigZ := Make BigN.
+(** Module [BigZ] implements [ZAxiomsSig] *)
 
+Module Export BigZAxiomsMod := ZSig_ZAxioms BigZ.
+Module Export BigZTimesOrderPropMod := ZTimesOrderPropFunct BigZAxiomsMod.
 
-Definition bigZ := BigZ.t.
+(** Notations about [BigZ] *)
+
+Notation bigZ := BigZ.t.
 
 Delimit Scope bigZ_scope with bigZ.
 Bind Scope bigZ_scope with bigZ.
 Bind Scope bigZ_scope with BigZ.t.
 Bind Scope bigZ_scope with BigZ.t_.
 
-Notation " i + j " := (BigZ.add i j) : bigZ_scope.
-Notation " i - j " := (BigZ.sub i j) : bigZ_scope.
-Notation " i * j " := (BigZ.mul i j) : bigZ_scope.
-Notation " i / j " := (BigZ.div i j) : bigZ_scope.
-Notation " i ?= j " := (BigZ.compare i j) : bigZ_scope.
-
-
- Theorem spec_to_Z: 
-  forall n, BigN.to_Z (BigZ.to_N n) = 
-            (Zsgn (BigZ.to_Z n) * BigZ.to_Z n)%Z.
- intros n; case n; simpl; intros p; 
-     generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
- intros p1 H1; case H1; auto.
- intros p1 H1; case H1; auto.
- Qed.
-
- Theorem spec_to_N n: 
-  (BigZ.to_Z n = 
-    Zsgn (BigZ.to_Z n) * (BigN.to_Z (BigZ.to_N n)))%Z.
- intros n; case n; simpl; intros p; 
-     generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
- intros p1 H1; case H1; auto.
- intros p1 H1; case H1; auto.
- Qed.
-
- Theorem spec_to_Z_pos: 
-  forall n, (0 <= BigZ.to_Z n ->
-              BigN.to_Z (BigZ.to_N n) = BigZ.to_Z n)%Z.
- intros n; case n; simpl; intros p; 
-     generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
- intros p1 _  H1; case H1; auto.
- intros p1 H1; case H1; auto.
- Qed.
+Notation Local "0" := BigZ.zero : bigZ_scope.
+Infix "+" := BigZ.add : bigZ_scope.
+Infix "-" := BigZ.sub : bigZ_scope.
+Notation "- x" := (BigZ.opp x) : bigZ_scope.
+Infix "*" := BigZ.mul : bigZ_scope.
+Infix "/" := BigZ.div : bigZ_scope.
+Infix "?=" := BigZ.compare : bigZ_scope.
+Infix "==" := BigZ.eq (at level 70, no associativity) : bigZ_scope.
+Infix "<" := BigZ.lt : bigZ_scope.
+Infix "<=" := BigZ.le : bigZ_scope.
+Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope.
+
+Open Scope bigZ_scope.
+
+(** Some additional results about [BigZ] *)
+
+Theorem spec_to_Z: forall n:bigZ, 
+  BigN.to_Z (BigZ.to_N n) = ((Zsgn [n]) * [n])%Z.
+Proof.
+intros n; case n; simpl; intros p; 
+  generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
+intros p1 H1; case H1; auto.
+intros p1 H1; case H1; auto.
+Qed.
+
+Theorem spec_to_N n: 
+ ([n] = Zsgn [n] * (BigN.to_Z (BigZ.to_N n)))%Z.
+Proof.
+intros n; case n; simpl; intros p; 
+  generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
+intros p1 H1; case H1; auto.
+intros p1 H1; case H1; auto.
+Qed.
+
+Theorem spec_to_Z_pos: forall n, (0 <= [n])%Z ->
+  BigN.to_Z (BigZ.to_N n) = [n].
+Proof.
+intros n; case n; simpl; intros p; 
+  generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
+intros p1 _ H1; case H1; auto.
+intros p1 H1; case H1; auto.
+Qed.
+
+Lemma sub_opp : forall x y : bigZ, x - y == x + (- y).
+Proof.
+red; intros; zsimpl; auto.
+Qed.
+
+Lemma plus_opp : forall x : bigZ, x + (- x) == 0.
+Proof.
+red; intros; zsimpl; auto with zarith.
+Qed.
+
+(** [BigZ] is a ring *)
+
+Lemma BigZring : 
+ ring_theory BigZ.zero BigZ.one BigZ.add BigZ.mul BigZ.sub BigZ.opp BigZ.eq.
+Proof.
+constructor.
+exact Zplus_0_l.
+exact Zplus_comm.
+exact Zplus_assoc.
+exact Ztimes_1_l.
+exact Ztimes_comm.
+exact Ztimes_assoc.
+exact Ztimes_plus_distr_r.
+exact sub_opp.
+exact plus_opp.
+Qed.
+
+Add Ring BigZr : BigZring.
+
+(** Todo: tactic translating from [BigZ] to [Z] + omega *)
 
+(** Todo: micromega *)
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 83171388d..cbf6f701f 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -12,94 +12,18 @@
 
 Require Import ZArith.
 Require Import BigNumPrelude.
+Require Import NSig.
+Require Import ZSig.
 
 Open Scope Z_scope.
 
-Module Type NType.
-
- Parameter t : Type.
- 
- Parameter zero : t.
- Parameter one : t.
-
- Parameter of_N : N -> t.
- Parameter to_Z : t -> Z.
- Parameter spec_pos: forall x, 0 <= to_Z x.
- Parameter spec_0: to_Z zero = 0.
- Parameter spec_1: to_Z one = 1.
- Parameter spec_of_N: forall x, to_Z (of_N x) = Z_of_N x.
-
- Parameter compare : t -> t -> comparison.
-
- Parameter spec_compare: forall x y,
-    match compare x y with
-      Eq => to_Z x = to_Z y
-    | Lt => to_Z x < to_Z y
-    | Gt => to_Z x > to_Z y
-    end.
-
- Parameter eq_bool : t -> t -> bool.
-
- Parameter spec_eq_bool: forall x y,
-    if eq_bool x y then to_Z x = to_Z y else to_Z x <> to_Z y.
- 
- Parameter succ : t -> t.
-
- Parameter spec_succ: forall n, to_Z (succ n) = to_Z n + 1.
-
- Parameter add  : t -> t -> t.
-
- Parameter spec_add: forall x y, to_Z (add x y) = to_Z x +  to_Z y.
-
- Parameter pred : t -> t.
-
- Parameter spec_pred: forall x, 0 < to_Z x -> to_Z (pred x) = to_Z x - 1.
-
- Parameter sub  : t -> t -> t.
-
- Parameter spec_sub: forall x y, to_Z y <= to_Z x ->
-   to_Z (sub x y) = to_Z x - to_Z y.
-
- Parameter mul       : t -> t -> t.
-
- Parameter spec_mul: forall x y, to_Z (mul x y) = to_Z x * to_Z y.
-
- Parameter square    : t -> t.
-
- Parameter spec_square: forall x, to_Z (square x) = to_Z x *  to_Z x.
-
- Parameter power_pos : t -> positive -> t.
-
- Parameter spec_power_pos: forall x n, to_Z (power_pos x n) = to_Z x ^ Zpos n.
-
- Parameter sqrt      : t -> t.
-
- Parameter spec_sqrt: forall x, to_Z (sqrt x) ^ 2 <= to_Z x < (to_Z (sqrt x) + 1) ^ 2.
-
- Parameter div_eucl : t -> t -> t * t.
-
- Parameter spec_div_eucl: forall x y,
-      0 < to_Z y ->
-      let (q,r) := div_eucl x y in (to_Z q, to_Z r) = (Zdiv_eucl (to_Z x) (to_Z y)).
+(** * ZMake 
  
- Parameter div      : t -> t -> t.
-
- Parameter spec_div: forall x y,
-      0 < to_Z y -> to_Z (div x y) = to_Z x / to_Z y.
-
- Parameter modulo   : t -> t -> t.
-
- Parameter spec_modulo:
-   forall x y, 0 < to_Z y -> to_Z (modulo x y) = to_Z x mod to_Z y.
-
- Parameter gcd      : t -> t -> t.
-
- Parameter spec_gcd: forall a b, to_Z (gcd a b) = Zgcd (to_Z a) (to_Z b).
-
-
-End NType.
+  A generic transformation from a structure of natural numbers 
+  [NSig.NType] to a structure of integers [ZSig.ZType].
+*)
 
-Module Make (N:NType).
+Module Make (N:NType) <: ZType.
  
  Inductive t_ := 
   | Pos : N.t -> t_
@@ -131,6 +55,7 @@ Module Make (N:NType).
    intros; rewrite N.spec_of_N; auto.
  Qed.
 
+ Definition eq x y := (to_Z x = to_Z y).
 
  Theorem spec_0: to_Z zero = 0.
  exact N.spec_0.
@@ -160,6 +85,10 @@ Module Make (N:NType).
   | Neg nx, Neg ny => N.compare ny nx
   end.
 
+ Definition lt n m := compare n m = Lt.
+ Definition le n m := compare n m <> Gt.
+ Definition min n m := match compare n m with Gt => m | _ => n end.
+ Definition max n m := match compare n m with Lt => m | _ => n end.
 
  Theorem spec_compare: forall x y,
     match compare x y with