ZArith_base, Zbool, Bool_nat

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

4 files changed, 18 insertions, 60 deletions

diff --git a/contrib/correctness/ProgBool.v b/contrib/correctness/ProgBool.v
index 026390a01d..d618e235a2 100644
--- a/contrib/correctness/ProgBool.v
+++ b/contrib/correctness/ProgBool.v
@@ -10,24 +10,10 @@
 
 (* $Id$ *)
 
-Require Export Compare_dec.
-Require Export Peano_dec.
 Require ZArith.
+Require Bool_nat.
 Require Sumbool.
 
-(* Programs use the booleans of type "bool", so we tranform any decidability
- * proof, in type sumbool, into a function returning a boolean with the
- * correct specification, through the following function:
- *)
-
-Definition bool_of_sumbool : 
-  (A,B:Prop) {A}+{B} -> { b:bool | if b then A else B }.
-Proof.
-Intros A B H.
-Elim H; [ Intro; Exists true; Assumption
-        | Intro; Exists false; Assumption ].
-Save.
-
 Definition annot_bool :
   (b:bool) { b':bool | if b' then b=true else b=false }.
 Proof.
@@ -78,45 +64,3 @@ Case b; Intro.
 Exists false; Auto. Exists true; Auto.
 Save.
 
-
-(* Application: the decidability of equality and order relations over
- * type Z give some boolean functions with the adequate specification.
- * For instance, Z_lt_ge_bool has type:
- * 
- *        (x,y:Z){b:bool | if b then `x < y` else `x >= y`}
- *)
-
-Definition Z_lt_ge_bool := [x,y:Z](bool_of_sumbool ? ? (Z_lt_ge_dec x y)).
-Definition Z_ge_lt_bool := [x,y:Z](bool_of_sumbool ? ? (Z_ge_lt_dec x y)).
-
-Definition Z_le_gt_bool := [x,y:Z](bool_of_sumbool ? ? (Z_le_gt_dec x y)).
-Definition Z_gt_le_bool := [x,y:Z](bool_of_sumbool ? ? (Z_gt_le_dec x y)).
-
-Definition Z_eq_bool := [x,y:Z](bool_of_sumbool ? ? (Z_eq_dec x y)).
-Definition Z_noteq_bool := [x,y:Z](bool_of_sumbool ? ? (Z_noteq_dec x y)).
-
-Definition Zeven_odd_bool := [x:Z](bool_of_sumbool ? ? (Zeven_odd_dec x)).
-
-(* ... and similarly for type nat *)
-
-Definition notzerop := [n:nat] (sumbool_not ? ? (zerop n)).
-Definition lt_ge_dec : (x,y:nat){(lt x y)}+{(ge x y)} := 
-  [n,m:nat] (sumbool_not ? ? (le_lt_dec m n)).
-
-Definition nat_lt_ge_bool := 
-  [x,y:nat](bool_of_sumbool ? ? (lt_ge_dec x y)).
-Definition nat_ge_lt_bool := 
-  [x,y:nat](bool_of_sumbool ? ? (sumbool_not ? ? (lt_ge_dec x y))).
-
-Definition nat_le_gt_bool := 
-  [x,y:nat](bool_of_sumbool ? ? (le_gt_dec x y)).
-Definition nat_gt_le_bool := 
-  [x,y:nat](bool_of_sumbool ? ? (sumbool_not ? ? (le_gt_dec x y))).
-
-Definition nat_eq_bool :=
-  [x,y:nat](bool_of_sumbool ? ? (eq_nat_dec x y)).
-Definition nat_noteq_bool := 
-  [x,y:nat](bool_of_sumbool ? ? (sumbool_not ? ? (eq_nat_dec x y))).
-
-Definition zerop_bool := [x:nat](bool_of_sumbool ? ? (zerop x)).
-Definition notzerop_bool := [x:nat](bool_of_sumbool ? ? (notzerop x)).
diff --git a/contrib/omega/Omega.v b/contrib/omega/Omega.v
index 7da167623c..77906873d1 100755
--- a/contrib/omega/Omega.v
+++ b/contrib/omega/Omega.v
@@ -15,7 +15,21 @@
 
 (* $Id$ *)
 
-Require Export ZArith.
+(* We do not require [ZArith] anymore, but only what's necessary for Omega *)
+Require Export fast_integer.
+Require Export zarith_aux.
+Require Export auxiliary.
+Require Export Zsyntax.
+Require Export ZArith_dec.
+Require Export Zmisc.
+Require Export Wf_Z.
+
+Hints Resolve Zle_n Zplus_sym Zplus_assoc Zmult_sym Zmult_assoc
+  Zero_left Zero_right Zmult_one Zplus_inverse_l Zplus_inverse_r 
+  Zmult_plus_distr_l Zmult_plus_distr_r : zarith.
+
+Require Export Zhints.
+
 (* The constant minus is required in coq_omega.ml *)
 Require Export Minus.
 
diff --git a/contrib/ring/ZArithRing.v b/contrib/ring/ZArithRing.v
index 2de8611764..65fd1bc64a 100644
--- a/contrib/ring/ZArithRing.v
+++ b/contrib/ring/ZArithRing.v
@@ -11,7 +11,7 @@
 (* Instantiation of the Ring tactic for the binary integers of ZArith *)
 
 Require Export ArithRing.
-Require Export ZArith.
+Require Export ZArith_base.
 Require Eqdep_dec.
 
 Definition Zeq := [x,y:Z]
diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v
index 41e29d38e2..f0ccfb886e 100644
--- a/contrib/romega/ReflOmegaCore.v
+++ b/contrib/romega/ReflOmegaCore.v
@@ -9,7 +9,7 @@
 Require Arith.
 Require PolyList.
 Require Bool.
-Require ZArith.
+Require ZArith_base.
 
 (* \subsection{Définition des types} *)