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

4 files changed, 25 insertions, 28 deletions

diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index bb2c01437d..5189a33efa 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -42,25 +42,27 @@ 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 "x > y" := (BigZ.lt y x)(only parsing) : bigZ_scope.
+Notation "x >= y" := (BigZ.le y x)(only parsing) : 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, 
+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; 
+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: 
+Theorem spec_to_N n:
  ([n] = Zsgn [n] * (BigN.to_Z (BigZ.to_N n)))%Z.
 Proof.
-intros n; case n; simpl; intros p; 
+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.
@@ -69,7 +71,7 @@ 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; 
+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.
@@ -87,7 +89,7 @@ Qed.
 
 (** [BigZ] is a ring *)
 
-Lemma BigZring : 
+Lemma BigZring :
  ring_theory BigZ.zero BigZ.one BigZ.add BigZ.mul BigZ.sub BigZ.opp BigZ.eq.
 Proof.
 constructor.
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 1e0b45cd2c..653170e348 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -47,6 +47,8 @@ Infix "?=" := BigN.compare : bigN_scope.
 Infix "==" := BigN.eq (at level 70, no associativity) : bigN_scope.
 Infix "<" := BigN.lt : bigN_scope.
 Infix "<=" := BigN.le : bigN_scope.
+Notation "x > y" := (BigN.lt y x)(only parsing) : bigN_scope.
+Notation "x >= y" := (BigN.le y x)(only parsing) : bigN_scope.
 Notation "[ i ]" := (BigN.to_Z i) : bigN_scope.
 
 Open Scope bigN_scope.
@@ -62,7 +64,7 @@ Qed.
 
 (** [BigN] is a semi-ring *)
 
-Lemma BigNring : 
+Lemma BigNring :
  semi_ring_theory BigN.zero BigN.one BigN.add BigN.mul BigN.eq.
 Proof.
 constructor.
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index 11c945f4ee..4177fc202f 100644
--- a/theories/Numbers/Rational/BigQ/BigQ.v
+++ b/theories/Numbers/Rational/BigQ/BigQ.v
@@ -54,7 +54,9 @@ Infix "?=" := BigQ.compare : bigQ_scope.
 Infix "==" := BigQ.eq : bigQ_scope.
 Infix "<" := BigQ.lt : bigQ_scope.
 Infix "<=" := BigQ.le : bigQ_scope.
-Notation "[ q ]" := (BigQ.to_Q q) : bigQ_scope. 
+Notation "x > y" := (BigQ.lt y x)(only parsing) : bigQ_scope.
+Notation "x >= y" := (BigQ.le y x)(only parsing) : bigQ_scope.
+Notation "[ q ]" := (BigQ.to_Q q) : bigQ_scope.
 
 Open Scope bigQ_scope.
 
@@ -97,16 +99,16 @@ Proof.
 Qed.
 
 (* TODO : fix this. For the moment it's useless (horribly slow)
-Hint Rewrite 
+Hint Rewrite
  BigQ.spec_0 BigQ.spec_1 BigQ.spec_m1 BigQ.spec_compare
- BigQ.spec_red BigQ.spec_add BigQ.spec_sub BigQ.spec_opp 
+ BigQ.spec_red BigQ.spec_add BigQ.spec_sub BigQ.spec_opp
  BigQ.spec_mul BigQ.spec_inv BigQ.spec_div BigQ.spec_power_pos
  BigQ.spec_square : bigq. *)
 
 
 (** [BigQ] is a field *)
 
-Lemma BigQfieldth : 
+Lemma BigQfieldth :
  field_theory BigQ.zero BigQ.one BigQ.add BigQ.mul BigQ.sub BigQ.opp BigQ.div BigQ.inv BigQ.eq.
 Proof.
 constructor.
@@ -128,7 +130,7 @@ rewrite BigQ.spec_mul, BigQ.spec_inv, BigQ.spec_1; field.
 rewrite <- BigQ.spec_0; auto.
 Qed.
 
-Lemma BigQpowerth : 
+Lemma BigQpowerth :
  power_theory BigQ.one BigQ.mul BigQ.eq Z_of_N BigQ.power.
 Proof.
 constructor.
@@ -141,13 +143,13 @@ induction p; simpl; auto; try rewrite !BigQ.spec_mul, !IHp; apply Qeq_refl.
 destruct n; reflexivity.
 Qed.
 
-Lemma BigQ_eq_bool_correct : 
+Lemma BigQ_eq_bool_correct :
  forall x y, BigQ.eq_bool x y = true -> x==y.
 Proof.
 intros; generalize (BigQ.spec_eq_bool x y); rewrite H; auto.
 Qed.
 
-Lemma BigQ_eq_bool_complete : 
+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).
@@ -156,16 +158,16 @@ Qed.
 
 (* TODO : improve later the detection of constants ... *)
 
-Ltac BigQcst t := 
- match t with 
+Ltac BigQcst t :=
+ match t with
    | BigQ.zero => BigQ.zero
    | BigQ.one => BigQ.one
    | BigQ.minus_one => BigQ.minus_one
-   | _ => NotConstant 
+   | _ => NotConstant
  end.
 
-Add Field BigQfield : BigQfieldth 
- (decidable BigQ_eq_bool_correct, 
+Add Field BigQfield : BigQfieldth
+ (decidable BigQ_eq_bool_correct,
   completeness BigQ_eq_bool_complete,
   constants [BigQcst],
   power_tac BigQpowerth [Qpow_tac]).
diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v
index bfed32f9d8..82d65dafb1 100644
--- a/theories/Numbers/Rational/BigQ/QMake.v
+++ b/theories/Numbers/Rational/BigQ/QMake.v
@@ -155,15 +155,6 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
    generalize (Z.spec_eq_bool x y); case Z.eq_bool
   end).
 
- Ltac destr_zcompare := 
- match goal with |- context [Zcompare ?x ?y] => 
-  let H := fresh "H" in 
-  case_eq (Zcompare x y); intro H;
-   [generalize (Zcompare_Eq_eq _ _ H); clear H; intro H |
-    change (x<y)%Z in H | 
-    change (x>y)%Z in H ]
- end.
-
  Ltac simpl_ndiv := rewrite N.spec_div by (nzsimpl; romega).
  Tactic Notation "simpl_ndiv" "in" "*" := 
    rewrite N.spec_div in * by (nzsimpl; romega).