Fix bug #1899: no more strange notations for Qge and Qgt

In fact, Qge and Ggt disappear, and we only leave notations for > and >=
that map directly to Qlt and Qle. 

We also adopt the same approach for BigN, BigZ, BigQ.

By the way, various clean-up concerning Zeq_bool, Zle_bool and similar
functions for Q. 



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

5 files changed, 11 insertions, 88 deletions

diff --git a/contrib/micromega/QMicromega.v b/contrib/micromega/QMicromega.v
index 9e95f6c493..c054f218aa 100644
--- a/contrib/micromega/QMicromega.v
+++ b/contrib/micromega/QMicromega.v
@@ -16,38 +16,11 @@ Require Import OrderedRing.
 Require Import RingMicromega.
 Require Import Refl.
 Require Import QArith.
-Require Import Qring.
-
-(* Qsrt has been removed from the library ? *)
-Definition Qsrt : ring_theory 0 1 Qplus Qmult Qminus Qopp Qeq.
-Proof.
-  constructor.
-  exact Qplus_0_l.
-  exact Qplus_comm.
-  exact Qplus_assoc.
-  exact Qmult_1_l.
-  exact Qmult_comm.
-  exact Qmult_assoc.
-  exact Qmult_plus_distr_l.
-  reflexivity.
-  exact Qplus_opp_r.
-Qed.
-
-
-Add Ring Qring : Qsrt.
-
-Lemma Qmult_neutral : forall x , 0 * x == 0.
-Proof.
-  intros.
-  compute.
-  reflexivity.
-Qed.
-
-(* Is there any qarith database ? *)
+Require Import Qfield.
 
 Lemma Qsor : SOR 0 1 Qplus Qmult Qminus Qopp Qeq  Qle Qlt.
 Proof.
-  constructor; intros ; subst ; try (intuition (subst; auto  with qarith)).
+  constructor; intros ; subst ; try (intuition (subst; auto with qarith)).
   apply Q_Setoid.
   rewrite H ; rewrite H0 ; reflexivity.
   rewrite H ; rewrite H0 ; reflexivity.
@@ -67,45 +40,12 @@ Proof.
   destruct(Q_dec n m) as [[H1 |H1] | H1 ] ; tauto.
   apply (Qplus_le_compat  p p n m  (Qle_refl p) H).
   generalize (Qmult_lt_compat_r 0 n m H0 H).
-  rewrite Qmult_neutral.
+  rewrite Qmult_0_l.
   auto.
   compute in H.
   discriminate.
 Qed.
 
-Definition Qeq_bool (p q : Q) : bool := Zeq_bool (Qnum p * ' Qden q)%Z  (Qnum q * ' Qden p)%Z.
-
-Definition Qle_bool (x y : Q) : bool := Zle_bool (Qnum x * ' Qden y)%Z (Qnum y * ' Qden x)%Z.
-
-Require ZMicromega.
-
-Lemma Qeq_bool_ok : forall x y, Qeq_bool x y = true -> x == y.
-Proof.
-  intros.
-  unfold Qeq_bool in H.
-  unfold Qeq.
-  apply (Zeqb_ok  _ _ H).
-Qed.
-
-
-Lemma Qeq_bool_neq : forall x y, Qeq_bool x y = false -> ~ x == y.
-Proof.
-  unfold Qeq_bool,Qeq.
-  red ; intros ; subst.
-  rewrite H0 in H.
-  apply  (ZMicromega.Zeq_bool_neq _ _ H).
-  reflexivity.
-Qed.
-
-Lemma Qle_bool_imp_le : forall x y : Q, Qle_bool x y = true -> x <= y.
-Proof.
-  unfold Qle_bool, Qle.
-  intros.
-  apply Zle_bool_imp_le ; auto.
-Qed.
-  
-
-
 
 Lemma QSORaddon :
   SORaddon 0 1 Qplus Qmult Qminus Qopp  Qeq  Qle (* ring elements *)
@@ -115,7 +55,7 @@ Lemma QSORaddon :
 Proof.
   constructor.
   constructor ; intros ; try reflexivity.
-  apply Qeq_bool_ok ; auto.
+  apply Qeq_bool_eq; auto.
   constructor.
   reflexivity.
   intros x y.
@@ -173,9 +113,9 @@ match o with
 | OpEq =>  Qeq
 | OpNEq => fun x y  => ~ x == y
 | OpLe => Qle
-| OpGe => Qge
+| OpGe => fun x y => Qle y x
 | OpLt => Qlt
-| OpGt => Qgt
+| OpGt => fun x y => Qlt y x
 end.
 
 Definition Qeval_formula (e:PolEnv Q) (ff : Formula Q) :=
diff --git a/contrib/micromega/RMicromega.v b/contrib/micromega/RMicromega.v
index d98c6d422e..7c6969c2f2 100644
--- a/contrib/micromega/RMicromega.v
+++ b/contrib/micromega/RMicromega.v
@@ -76,12 +76,12 @@ Proof.
   apply mult_IZR.
   apply Ropp_Ropp_IZR.
   apply IZR_eq.
-  apply Zeqb_ok ; auto.
+  apply Zeq_bool_eq ; auto.
   apply R_power_theory.
   intros x y.
   intro.
   apply IZR_neq.
-  apply ZMicromega.Zeq_bool_neq ; auto.
+  apply Zeq_bool_neq ; auto.
   intros. apply IZR_le.  apply Zle_bool_imp_le. auto.
 Qed.
 
diff --git a/contrib/micromega/ZMicromega.v b/contrib/micromega/ZMicromega.v
index 94c83f73d3..0855925a3d 100644
--- a/contrib/micromega/ZMicromega.v
+++ b/contrib/micromega/ZMicromega.v
@@ -39,15 +39,6 @@ Proof.
   apply Zmult_lt_0_compat ; auto.
 Qed.
 
-Lemma Zeq_bool_neq : forall x y, Zeq_bool x y = false -> x <> y.
-Proof.
-  red ; intros.
-  subst.
-  unfold Zeq_bool in H.
-  rewrite Zcompare_refl  in H.
-  discriminate.
-Qed.
-
 Lemma ZSORaddon :
   SORaddon 0 1 Zplus Zmult Zminus Zopp  (@eq Z) Zle (* ring elements *)
   0%Z 1%Z Zplus Zmult Zminus Zopp (* coefficients *)
@@ -56,7 +47,7 @@ Lemma ZSORaddon :
 Proof.
   constructor.
   constructor ; intros ; try reflexivity.
-  apply Zeqb_ok ; auto.
+  apply Zeq_bool_eq ; auto.
   constructor.
   reflexivity.
   intros x y.
diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v
index c1fa963f21..e664b3b767 100644
--- a/contrib/setoid_ring/InitialRing.v
+++ b/contrib/setoid_ring/InitialRing.v
@@ -38,14 +38,6 @@ Proof.
  exact Zmult_plus_distr_l. trivial. exact Zminus_diag.
 Qed.
 
- Lemma Zeqb_ok : forall x y, Zeq_bool x y = true -> x = y.
- Proof.
-  intros x y.
-  assert (H := Zcompare_Eq_eq x y);unfold Zeq_bool;
-  destruct (Zcompare x y);intros H1;auto;discriminate H1.
- Qed.
-
-
 (** Two generic morphisms from Z to (abrbitrary) rings, *)
 (**second one is more convenient for proofs but they are ext. equal*)
 Section ZMORPHISM.
@@ -174,7 +166,7 @@ Section ZMORPHISM.
    Zeq_bool x y = true -> [x] == [y].
  Proof.
   intros x y H.
-  assert (H1 := Zeqb_ok x y H);unfold IDphi in H1.
+  assert (H1 := Zeq_bool_eq x y H);unfold IDphi in H1.
   rewrite H1;rrefl.
  Qed.
   
diff --git a/contrib/setoid_ring/ZArithRing.v b/contrib/setoid_ring/ZArithRing.v
index 4a5b623b43..942915abf2 100644
--- a/contrib/setoid_ring/ZArithRing.v
+++ b/contrib/setoid_ring/ZArithRing.v
@@ -50,7 +50,7 @@ Ltac Zpower_neg :=
   end.   
 
 Add Ring Zr : Zth
-  (decidable Zeqb_ok, constants [Zcst], preprocess [Zpower_neg;unfold Zsucc],
+  (decidable Zeq_bool_eq, constants [Zcst], preprocess [Zpower_neg;unfold Zsucc],
    power_tac Zpower_theory [Zpow_tac],
     (* The two following option are not needed, it is the default chose when the set of 
         coefficiant is usual ring Z *)