BigN, BigZ, BigQ: presentation via unique module with both ops and props

 We use the <+ operation to regroup all known facts about BigN
 (resp BigZ, ...) in a unique module. This uses also the new ! feature
 for controling inlining. By the way, we also make sure that these
 new BigN and BigZ modules implements OrderedTypeFull and TotalOrder,
 and also contains facts about min and max (cf. GenericMinMax).

 Side effects:
 - In NSig and ZSig, specification of compare and eq_bool is now
   done with respect to Zcompare and Zeq_bool, as for other ops.
   The order <= and < are also defined via Zle and Zlt, instead
   of using compare. Min and max are axiomatized instead of being
   macros.
 - Some proofs rework in QMake
 - QOrderedType and Qminmax were in fact not compiled by make world

 Still todo: OrderedType + MinMax for BigQ, etc etc

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

1 files changed, 11 insertions, 10 deletions

diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index fcfb5d7e75..15abaaa42b 100644
--- a/theories/Numbers/Rational/BigQ/BigQ.v
+++ b/theories/Numbers/Rational/BigQ/BigQ.v
@@ -5,10 +5,10 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
-(************************************************************************)
 
-(*i $Id$ i*)
+(** * BigQ: an efficient implementation of rational numbers *)
+
+(** Initial authors: Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
 
 Require Export BigZ.
 Require Import Field Qfield QSig QMake.
@@ -178,18 +178,19 @@ induction p; simpl; auto; try rewrite !BigQ.spec_mul, !IHp; apply Qeq_refl.
 destruct n; reflexivity.
 Qed.
 
-Lemma BigQ_eq_bool_correct :
- forall x y, BigQ.eq_bool x y = true -> x==y.
+Lemma BigQ_eq_bool_iff :
+ forall x y, BigQ.eq_bool x y = true <-> x==y.
 Proof.
-intros; generalize (BigQ.spec_eq_bool x y); rewrite H; auto.
+intros. rewrite BigQ.spec_eq_bool. apply Qeq_bool_iff.
 Qed.
 
+Lemma BigQ_eq_bool_correct :
+ forall x y, BigQ.eq_bool x y = true -> x==y.
+Proof. now apply BigQ_eq_bool_iff. Qed.
+
 Lemma BigQ_eq_bool_complete :
  forall x y, x==y -> BigQ.eq_bool x y = true.
-Proof.
-intros; generalize (BigQ.spec_eq_bool x y).
-destruct BigQ.eq_bool; auto.
-Qed.
+Proof. now apply BigQ_eq_bool_iff. Qed.
 
 (* TODO : improve later the detection of constants ... *)