Imported Upstream snapshot 8.3~beta0+13298

12 files changed, 270 insertions, 153 deletions

diff --git a/theories/QArith/QArith.v b/theories/QArith/QArith.v
index 2af65320..f7a28598 100644
--- a/theories/QArith/QArith.v
+++ b/theories/QArith/QArith.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: QArith.v 10739 2008-04-01 14:45:20Z herbelin $ i*)
+(*i $Id$ i*)
 
 Require Export QArith_base.
 Require Export Qring.
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 0b6d1cfe..54d2a295 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -6,11 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: QArith_base.v 13215 2010-06-29 09:31:45Z letouzey $ i*)
+(*i $Id$ i*)
 
 Require Export ZArith.
 Require Export ZArithRing.
-Require Export Setoid Bool.
+Require Export Morphisms Setoid Bool.
 
 (** * Definition of [Q] and basic properties *)
 
@@ -87,6 +87,19 @@ Qed.
 Hint Unfold Qeq Qlt Qle : qarith.
 Hint Extern 5 (?X1 <> ?X2) => intro; discriminate: qarith.
 
+Lemma Qcompare_antisym : forall x y, CompOpp (x ?= y) = (y ?= x).
+Proof.
+ unfold "?=". intros. apply Zcompare_antisym.
+Qed.
+
+Lemma Qcompare_spec : forall x y, CompSpec Qeq Qlt x y (x ?= y).
+Proof.
+ intros.
+ destruct (x ?= y) as [ ]_eqn:H; constructor; auto.
+ rewrite Qeq_alt; auto.
+ rewrite Qlt_alt, <- Qcompare_antisym, H; auto.
+Qed.
+
 (** * Properties of equality. *)
 
 Theorem Qeq_refl : forall x, x == x.
@@ -101,7 +114,7 @@ Qed.
 
 Theorem Qeq_trans : forall x y z, x == y -> y == z -> x == z.
 Proof.
-unfold Qeq in |- *; intros.
+unfold Qeq; intros.
 apply Zmult_reg_l with (QDen y).
 auto with qarith.
 transitivity (Qnum x * QDen y * QDen z)%Z; try ring.
@@ -110,6 +123,15 @@ transitivity (Qnum y * QDen z * QDen x)%Z; try ring.
 rewrite H0; ring.
 Qed.
 
+Hint Resolve Qeq_refl : qarith.
+Hint Resolve Qeq_sym : qarith.
+Hint Resolve Qeq_trans : qarith.
+
+(** In a word, [Qeq] is a setoid equality. *)
+
+Instance Q_Setoid : Equivalence Qeq.
+Proof. split; red; eauto with qarith. Qed.
+
 (** Furthermore, this equality is decidable: *)
 
 Theorem Qeq_dec : forall x y, {x==y} + {~ x==y}.
@@ -120,12 +142,12 @@ Defined.
 Definition Qeq_bool x y :=
   (Zeq_bool (Qnum x * QDen y) (Qnum y * QDen x))%Z.
 
-Definition Qle_bool x y := 
+Definition Qle_bool x y :=
   (Zle_bool (Qnum x * QDen y) (Qnum y * QDen x))%Z.
 
 Lemma Qeq_bool_iff : forall x y, Qeq_bool x y = true <-> x == y.
 Proof.
-  unfold Qeq_bool, Qeq; intros. 
+  unfold Qeq_bool, Qeq; intros.
   symmetry; apply Zeq_is_eq_bool.
 Qed.
 
@@ -155,18 +177,6 @@ Proof.
   intros; rewrite <- Qle_bool_iff; auto.
 Qed.
 
-(** We now consider [Q] seen as a setoid. *)
-
-Add Relation Q Qeq
-  reflexivity proved by Qeq_refl
-  symmetry proved by Qeq_sym
-  transitivity proved by Qeq_trans
-as Q_Setoid.
-
-Hint Resolve Qeq_refl : qarith.
-Hint Resolve Qeq_sym : qarith.
-Hint Resolve Qeq_trans : qarith.
-
 Theorem Qnot_eq_sym : forall x y, ~x == y -> ~y == x.
 Proof.
  auto with qarith.
@@ -218,7 +228,7 @@ Qed.
 
 (** * Setoid compatibility results *)
 
-Add Morphism Qplus : Qplus_comp.
+Instance Qplus_comp : Proper (Qeq==>Qeq==>Qeq) Qplus.
 Proof.
   unfold Qeq, Qplus; simpl.
   Open Scope Z_scope.
@@ -232,24 +242,23 @@ Proof.
   Close Scope Z_scope.
 Qed.
 
-Add Morphism Qopp : Qopp_comp.
+Instance Qopp_comp : Proper (Qeq==>Qeq) Qopp.
 Proof.
   unfold Qeq, Qopp; simpl.
   Open Scope Z_scope.
-  intros.
+  intros x y H; simpl.
   replace (- Qnum x * ' Qden y) with (- (Qnum x * ' Qden y)) by ring.
-  rewrite H in |- *;  ring.
+  rewrite H;  ring.
   Close Scope Z_scope.
 Qed.
 
-Add Morphism Qminus : Qminus_comp.
+Instance Qminus_comp : Proper (Qeq==>Qeq==>Qeq) Qminus.
 Proof.
-  intros.
-  unfold Qminus.
-  rewrite H; rewrite H0; auto with qarith.
+  intros x x' Hx y y' Hy.
+  unfold Qminus. rewrite Hx, Hy; auto with qarith.
 Qed.
 
-Add Morphism Qmult : Qmult_comp.
+Instance Qmult_comp : Proper (Qeq==>Qeq==>Qeq) Qmult.
 Proof.
   unfold Qeq; simpl.
   Open Scope Z_scope.
@@ -263,7 +272,7 @@ Proof.
   Close Scope Z_scope.
 Qed.
 
-Add Morphism Qinv : Qinv_comp.
+Instance Qinv_comp : Proper (Qeq==>Qeq) Qinv.
 Proof.
   unfold Qeq, Qinv; simpl.
   Open Scope Z_scope.
@@ -281,83 +290,49 @@ Proof.
   Close Scope Z_scope.
 Qed.
 
-Add Morphism Qdiv : Qdiv_comp.
-Proof.
-  intros; unfold Qdiv.
-  rewrite H; rewrite H0; auto with qarith.
-Qed.
-
-Add Morphism Qle with signature Qeq ==> Qeq ==> iff as Qle_comp.
+Instance Qdiv_comp : Proper (Qeq==>Qeq==>Qeq) Qdiv.
 Proof.
-  cut (forall x1 x2, x1==x2 -> forall x3 x4, x3==x4 -> x1<=x3 -> x2<=x4).
-  split; apply H; assumption || (apply Qeq_sym ; assumption).
-
-  unfold Qeq, Qle; simpl.
-  Open Scope Z_scope.
-  intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0 H1; simpl in *.
-  apply Zmult_le_reg_r with ('p2).
-  unfold Zgt; auto.
-  replace (q1 * 's2 * 'p2) with (q1 * 'p2 * 's2) by ring.
-  rewrite <- H.
-  apply Zmult_le_reg_r with ('r2).
-  unfold Zgt; auto.
-  replace (s1 * 'q2 * 'p2 * 'r2) with (s1 * 'r2 * 'q2 * 'p2) by ring.
-  rewrite <- H0.
-  replace (p1 * 'q2 * 's2 * 'r2) with ('q2 * 's2 * (p1 * 'r2)) by ring.
-  replace (r1 * 's2 * 'q2 * 'p2) with ('q2 * 's2 * (r1 * 'p2)) by ring.
-  auto with zarith.
-  Close Scope Z_scope.
+  intros x x' Hx y y' Hy; unfold Qdiv.
+  rewrite Hx, Hy; auto with qarith.
 Qed.
 
-Add Morphism Qlt with signature Qeq ==> Qeq ==> iff as  Qlt_comp.
+Instance Qcompare_comp : Proper (Qeq==>Qeq==>eq) Qcompare.
 Proof.
-  cut (forall x1 x2, x1==x2 -> forall x3 x4, x3==x4 -> x1<x3 -> x2<x4).
-  split; apply H; assumption || (apply Qeq_sym ; assumption).
-
-  unfold Qeq, Qlt; simpl.
+  unfold Qeq, Qcompare.
   Open Scope Z_scope.
-  intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0 H1; simpl in *.
-  apply Zgt_lt.
-  generalize (Zlt_gt _ _ H1); clear H1; intro H1.
-  apply Zmult_gt_reg_r with ('p2); auto with zarith.
-  replace (q1 * 's2 * 'p2) with (q1 * 'p2 * 's2) by ring.
-  rewrite <- H.
-  apply Zmult_gt_reg_r with ('r2); auto with zarith.
-  replace (s1 * 'q2 * 'p2 * 'r2) with (s1 * 'r2 * 'q2 * 'p2) by ring.
-  rewrite <- H0.
-  replace (p1 * 'q2 * 's2 * 'r2) with ('q2 * 's2 * (p1 * 'r2)) by ring.
-  replace (r1 * 's2 * 'q2 * 'p2) with ('q2 * 's2 * (r1 * 'p2)) by ring.
-  apply Zlt_gt.
-  apply Zmult_gt_0_lt_compat_l; auto with zarith.
+  intros (p1,p2) (q1,q2) H (r1,r2) (s1,s2) H'; simpl in *.
+  rewrite <- (Zcompare_mult_compat (q2*s2) (p1*'r2)).
+  rewrite <- (Zcompare_mult_compat (p2*r2) (q1*'s2)).
+  change ('(q2*s2)) with ('q2 * 's2).
+  change ('(p2*r2)) with ('p2 * 'r2).
+  replace ('q2 * 's2 * (p1*'r2)) with ((p1*'q2)*'r2*'s2) by ring.
+  rewrite H.
+  replace ('q2 * 's2 * (r1*'p2)) with ((r1*'s2)*'q2*'p2) by ring.
+  rewrite H'.
+  f_equal; ring.
   Close Scope Z_scope.
 Qed.
 
-Add Morphism Qeq_bool with signature Qeq ==> Qeq ==> (@eq bool) as Qeqb_comp.
+Instance Qle_comp : Proper (Qeq==>Qeq==>iff) Qle.
 Proof.
- intros; apply eq_true_iff_eq.
- rewrite 2 Qeq_bool_iff, H, H0; split; auto with qarith.
+  intros p q H r s H'. rewrite 2 Qle_alt, H, H'; auto with *.
 Qed.
 
-Add Morphism Qle_bool with signature Qeq ==> Qeq ==> (@eq bool) as Qleb_comp.
+Instance Qlt_compat : Proper (Qeq==>Qeq==>iff) Qlt.
 Proof.
- intros; apply eq_true_iff_eq.
- rewrite 2 Qle_bool_iff, H, H0.
- split; auto with qarith.
+  intros p q H r s H'. rewrite 2 Qlt_alt, H, H'; auto with *.
 Qed.
 
-Lemma Qcompare_egal_dec: forall n m p q : Q,
-  (n<m -> p<q) -> (n==m -> p==q) -> (n>m -> p>q) -> ((n?=m) = (p?=q)).
+Instance Qeqb_comp : Proper (Qeq==>Qeq==>eq) Qeq_bool.
 Proof.
-  intros.
-  do 2 rewrite Qeq_alt in H0.
-  unfold Qeq, Qlt, Qcompare in *.
-  apply Zcompare_egal_dec; auto.
-  omega.
+ intros p q H r s H'; apply eq_true_iff_eq.
+ rewrite 2 Qeq_bool_iff, H, H'; split; auto with qarith.
 Qed.
 
-Add Morphism Qcompare : Qcompare_comp.
+Instance Qleb_comp : Proper (Qeq==>Qeq==>eq) Qle_bool.
 Proof.
-  intros; apply Qcompare_egal_dec; rewrite H; rewrite H0; auto.
+ intros p q H r s H'; apply eq_true_iff_eq.
+ rewrite 2 Qle_bool_iff, H, H'; split; auto with qarith.
 Qed.
 
 
@@ -554,6 +529,11 @@ Qed.
 
 Hint Resolve Qle_trans : qarith.
 
+Lemma Qlt_irrefl : forall x, ~x<x.
+Proof.
+ unfold Qlt. auto with zarith.
+Qed.
+
 Lemma Qlt_not_eq : forall x y, x<y -> ~ x==y.
 Proof.
   unfold Qlt, Qeq; auto with zarith.
@@ -561,6 +541,13 @@ Qed.
 
 (** Large = strict or equal *)
 
+Lemma Qle_lteq : forall x y, x<=y <-> x<y \/ x==y.
+Proof.
+ intros.
+ rewrite Qeq_alt, Qle_alt, Qlt_alt.
+ destruct (x ?= y); intuition; discriminate.
+Qed.
+
 Lemma Qlt_le_weak : forall x y, x<y -> x<=y.
 Proof.
   unfold Qle, Qlt; auto with zarith.
@@ -632,15 +619,8 @@ Proof.
   unfold Qle, Qlt, Qeq; intros; apply Zle_lt_or_eq; auto.
 Qed.
 
-(** These hints were meant to be added to the qarith database,
-    but a typo prevented that. This will be fixed in 8.3.
-    Concerning 8.2, for maximal compatibility , we
-    leave them in a separate database, in order to preserve
-    the strength of both [auto with qarith] and [auto with *].
-    (see bug #2346). *)
-
 Hint Resolve Qle_not_lt Qlt_not_le Qnot_le_lt Qnot_lt_le
- Qlt_le_weak Qlt_not_eq Qle_antisym Qle_refl: qarith_extra.
+ Qlt_le_weak Qlt_not_eq Qle_antisym Qle_refl: qarith.
 
 (** Some decidability results about orders. *)
 
@@ -842,9 +822,9 @@ Qed.
 Definition Qpower_positive (q:Q)(p:positive) : Q :=
  pow_pos Qmult q p.
 
-Add Morphism Qpower_positive with signature Qeq ==> @eq _ ==> Qeq as Qpower_positive_comp.
+Instance Qpower_positive_comp : Proper (Qeq==>eq==>Qeq) Qpower_positive.
 Proof.
-intros x1 x2 Hx y.
+intros x x' Hx y y' Hy. rewrite <-Hy; clear y' Hy.
 unfold Qpower_positive.
 induction y; simpl;
 try rewrite IHy;
@@ -861,8 +841,8 @@ Definition Qpower (q:Q) (z:Z) :=
 
 Notation " q ^ z " := (Qpower q z) : Q_scope.
 
-Add Morphism Qpower with signature Qeq ==> @eq _ ==> Qeq as Qpower_comp.
+Instance Qpower_comp : Proper (Qeq==>eq==>Qeq) Qpower.
 Proof.
-intros x1 x2 Hx [|y|y]; try reflexivity;
-simpl; rewrite Hx; reflexivity.
+intros x x' Hx y y' Hy. rewrite <- Hy; clear y' Hy.
+destruct y; simpl; rewrite ?Hx; auto with *.
 Qed.
diff --git a/theories/QArith/QOrderedType.v b/theories/QArith/QOrderedType.v
new file mode 100644
index 00000000..692bfd92
--- /dev/null
+++ b/theories/QArith/QOrderedType.v
@@ -0,0 +1,58 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import QArith_base Equalities Orders OrdersTac.
+
+Local Open Scope Q_scope.
+
+(** * DecidableType structure for rational numbers *)
+
+Module Q_as_DT <: DecidableTypeFull.
+ Definition t := Q.
+ Definition eq := Qeq.
+ Definition eq_equiv := Q_Setoid.
+ Definition eqb := Qeq_bool.
+ Definition eqb_eq := Qeq_bool_iff.
+
+ Include BackportEq. (** eq_refl, eq_sym, eq_trans *)
+ Include HasEqBool2Dec. (** eq_dec *)
+
+End Q_as_DT.
+
+(** Note that the last module fulfills by subtyping many other
+    interfaces, such as [DecidableType] or [EqualityType]. *)
+
+
+
+(** * OrderedType structure for rational numbers *)
+
+Module Q_as_OT <: OrderedTypeFull.
+ Include Q_as_DT.
+ Definition lt := Qlt.
+ Definition le := Qle.
+ Definition compare := Qcompare.
+
+ Instance lt_strorder : StrictOrder Qlt.
+ Proof. split; [ exact Qlt_irrefl | exact Qlt_trans ]. Qed.
+
+ Instance lt_compat : Proper (Qeq==>Qeq==>iff) Qlt.
+ Proof. auto with *. Qed.
+
+ Definition le_lteq := Qle_lteq.
+ Definition compare_spec := Qcompare_spec.
+
+End Q_as_OT.
+
+
+(** * An [order] tactic for [Q] numbers *)
+
+Module QOrder := OTF_to_OrderTac Q_as_OT.
+Ltac q_order := QOrder.order.
+
+(** Note that [q_order] is domain-agnostic: it will not prove
+    [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x==y]. *)
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v
index 42522468..34d6267e 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.v
@@ -6,14 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Qcanon.v 10739 2008-04-01 14:45:20Z herbelin $ i*)
+(*i $Id$ i*)
 
 Require Import Field.
 Require Import QArith.
 Require Import Znumtheory.
 Require Import Eqdep_dec.
 
-(** [Qc] : A canonical representation of rational numbers. 
+(** [Qc] : A canonical representation of rational numbers.
    based on the setoid representation [Q]. *)
 
 Record Qc : Set := Qcmake { this :> Q ; canon : Qred this = this }.
@@ -23,7 +23,7 @@ Bind Scope Qc_scope with Qc.
 Arguments Scope Qcmake [Q_scope].
 Open Scope Qc_scope.
 
-Lemma Qred_identity : 
+Lemma Qred_identity :
   forall q:Q, Zgcd (Qnum q) (QDen q) = 1%Z -> Qred q = q.
 Proof.
   unfold Qred; intros (a,b); simpl.
@@ -36,7 +36,7 @@ Proof.
   subst; simpl; auto.
 Qed.
 
-Lemma Qred_identity2 : 
+Lemma Qred_identity2 :
   forall q:Q, Qred q = q -> Zgcd (Qnum q) (QDen q) = 1%Z.
 Proof.
   unfold Qred; intros (a,b); simpl.
@@ -50,7 +50,7 @@ Proof.
   destruct g as [|g|g]; destruct bb as [|bb|bb]; simpl in *; try discriminate.
   f_equal.
   apply Pmult_reg_r with bb.
-  injection H2; intros. 
+  injection H2; intros.
   rewrite <- H0.
   rewrite H; simpl; auto.
   elim H1; auto.
@@ -70,7 +70,7 @@ Proof.
   apply Qred_correct.
 Qed.
 
-Definition Q2Qc (q:Q) : Qc := Qcmake (Qred q) (Qred_involutive q). 
+Definition Q2Qc (q:Q) : Qc := Qcmake (Qred q) (Qred_involutive q).
 Arguments Scope Q2Qc [Q_scope].
 Notation " !! " := Q2Qc : Qc_scope.
 
@@ -82,7 +82,7 @@ Proof.
   assert (H0:=Qred_complete _ _ H).
   assert (q = q') by congruence.
   subst q'.
-  assert (proof_q = proof_q'). 
+  assert (proof_q = proof_q').
   apply eq_proofs_unicity; auto; intros.
   repeat decide equality.
   congruence.
@@ -98,8 +98,8 @@ Notation Qcgt := (fun x y : Qc => Qlt y x).
 Notation Qcge := (fun x y : Qc => Qle y x).
 Infix "<" := Qclt : Qc_scope.
 Infix "<=" := Qcle : Qc_scope.
-Infix ">" := Qcgt : Qc_scope. 
-Infix ">=" := Qcge : Qc_scope. 
+Infix ">" := Qcgt : Qc_scope.
+Infix ">=" := Qcge : Qc_scope.
 Notation "x <= y <= z" := (x<=y/\y<=z) : Qc_scope.
 Notation "x < y < z" := (x<y/\y<z) : Qc_scope.
 
@@ -141,9 +141,9 @@ Proof.
   intros.
   destruct (Qeq_dec x y) as [H|H]; auto.
   right; contradict H; subst; auto with qarith.
-Defined. 
+Defined.
 
-(** The addition, multiplication and opposite are defined 
+(** The addition, multiplication and opposite are defined
    in the straightforward way: *)
 
 Definition Qcplus (x y : Qc) := !!(x+y).
@@ -155,9 +155,9 @@ Notation "- x" := (Qcopp x) : Qc_scope.
 Definition Qcminus (x y : Qc) := x+-y.
 Infix "-" := Qcminus : Qc_scope.
 Definition Qcinv (x : Qc) := !!(/x).
-Notation "/ x" := (Qcinv x) : Qc_scope. 
+Notation "/ x" := (Qcinv x) : Qc_scope.
 Definition Qcdiv (x y : Qc) := x*/y.
-Infix "/" := Qcdiv : Qc_scope. 
+Infix "/" := Qcdiv : Qc_scope.
 
 (** [0] and [1] are apart *)
 
@@ -167,8 +167,8 @@ Proof.
   intros H; discriminate H.
 Qed.
 
-Ltac qc := match goal with 
- | q:Qc |- _ => destruct q; qc 
+Ltac qc := match goal with
+ | q:Qc |- _ => destruct q; qc
  | _ => apply Qc_is_canon; simpl; repeat rewrite Qred_correct
 end.
 
@@ -191,7 +191,7 @@ Qed.
 Lemma Qcplus_0_r : forall x, x+0 = x.
 Proof.
   intros; qc; apply Qplus_0_r.
-Qed. 
+Qed.
 
 (** Commutativity of addition: *)
 
@@ -265,13 +265,13 @@ Qed.
 Theorem Qcmult_integral_l : forall x y, ~ x = 0 -> x*y = 0 -> y = 0.
 Proof.
   intros; destruct (Qcmult_integral _ _ H0); tauto.
-Qed. 
+Qed.
 
-(** Inverse and division. *) 
+(** Inverse and division. *)
 
 Theorem Qcmult_inv_r : forall x, x<>0 -> x*(/x) = 1.
 Proof.
-  intros; qc; apply Qmult_inv_r; auto. 
+  intros; qc; apply Qmult_inv_r; auto.
 Qed.
 
 Theorem Qcmult_inv_l : forall x, x<>0 -> (/x)*x = 1.
@@ -436,24 +436,24 @@ Qed.
 Lemma Qcmult_lt_0_le_reg_r : forall x y z, 0 <  z  -> x*z <= y*z -> x <= y.
 Proof.
   unfold Qcmult, Qcle, Qclt; intros; simpl in *.
-  repeat progress rewrite Qred_correct in * |-. 
+  repeat progress rewrite Qred_correct in * |-.
   eapply Qmult_lt_0_le_reg_r; eauto.
 Qed.
 
 Lemma Qcmult_lt_compat_r : forall x y z, 0 < z  -> x < y -> x*z < y*z.
 Proof.
   unfold Qcmult, Qclt; intros; simpl in *.
-  repeat progress rewrite Qred_correct in *. 
+  repeat progress rewrite Qred_correct in *.
   eapply Qmult_lt_compat_r; eauto.
 Qed.
 
 (** Rational to the n-th power *)
 
-Fixpoint Qcpower (q:Qc)(n:nat) { struct n } : Qc := 
-  match n with 
+Fixpoint Qcpower (q:Qc)(n:nat) : Qc :=
+  match n with
     | O => 1
     | S n => q * (Qcpower q n)
-  end. 
+  end.
 
 Notation " q ^ n " := (Qcpower q n) : Qc_scope.
 
@@ -467,7 +467,7 @@ Lemma Qcpower_0 : forall n, n<>O -> 0^n = 0.
 Proof.
   destruct n; simpl.
   destruct 1; auto.
-  intros. 
+  intros.
   apply Qc_is_canon.
   simpl.
   compute; auto.
@@ -537,7 +537,7 @@ Proof.
   intros (q, Hq) (q', Hq'); simpl; intros H.
   assert (H1 := H Hq Hq').
   subst q'.
-  assert (Hq = Hq'). 
+  assert (Hq = Hq').
   apply Eqdep_dec.eq_proofs_unicity; auto; intros.
   repeat decide equality.
   congruence.
diff --git a/theories/QArith/Qfield.v b/theories/QArith/Qfield.v
index 9841ef89..fbfae55c 100644
--- a/theories/QArith/Qfield.v
+++ b/theories/QArith/Qfield.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Qfield.v 11208 2008-07-04 16:57:46Z letouzey $ i*)
+(*i $Id$ i*)
 
 Require Export Field.
 Require Export QArith_base.
@@ -73,15 +73,15 @@ Ltac Qpow_tac t :=
   | _ => NotConstant
   end.
 
-Add Field Qfield : Qsft 
- (decidable Qeq_bool_eq, 
+Add Field Qfield : Qsft
+ (decidable Qeq_bool_eq,
   completeness Qeq_eq_bool,
-  constants [Qcst], 
+  constants [Qcst],
   power_tac Qpower_theory [Qpow_tac]).
 
 (** Exemple of use: *)
 
-Section Examples. 
+Section Examples.
 
 Let ex1 : forall x y z : Q, (x+y)*z ==  (x*z)+(y*z).
   intros.
@@ -89,7 +89,7 @@ Let ex1 : forall x y z : Q, (x+y)*z ==  (x*z)+(y*z).
 Qed.
 
 Let ex2 : forall x y : Q, x+y == y+x.
-  intros. 
+  intros.
   ring.
 Qed.
 
diff --git a/theories/QArith/Qminmax.v b/theories/QArith/Qminmax.v
new file mode 100644
index 00000000..d05a8594
--- /dev/null
+++ b/theories/QArith/Qminmax.v
@@ -0,0 +1,67 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import QArith_base Orders QOrderedType GenericMinMax.
+
+(** * Maximum and Minimum of two rational numbers *)
+
+Local Open Scope Q_scope.
+
+(** [Qmin] and [Qmax] are obtained the usual way from [Qcompare]. *)
+
+Definition Qmax := gmax Qcompare.
+Definition Qmin := gmin Qcompare.
+
+Module QHasMinMax <: HasMinMax Q_as_OT.
+ Module QMM := GenericMinMax Q_as_OT.
+ Definition max := Qmax.
+ Definition min := Qmin.
+ Definition max_l := QMM.max_l.
+ Definition max_r := QMM.max_r.
+ Definition min_l := QMM.min_l.
+ Definition min_r := QMM.min_r.
+End QHasMinMax.
+
+Module Q.
+
+(** We obtain hence all the generic properties of max and min. *)
+
+Include MinMaxProperties Q_as_OT QHasMinMax.
+
+
+(** * Properties specific to the [Q] domain *)
+
+(** Compatibilities (consequences of monotonicity) *)
+
+Lemma plus_max_distr_l : forall n m p, Qmax (p + n) (p + m) == p + Qmax n m.
+Proof.
+ intros. apply max_monotone.
+ intros x x' Hx; rewrite Hx; auto with qarith.
+ intros x x' Hx. apply Qplus_le_compat; q_order.
+Qed.
+
+Lemma plus_max_distr_r : forall n m p, Qmax (n + p) (m + p) == Qmax n m + p.
+Proof.
+ intros. rewrite (Qplus_comm n p), (Qplus_comm m p), (Qplus_comm _ p).
+ apply plus_max_distr_l.
+Qed.
+
+Lemma plus_min_distr_l : forall n m p, Qmin (p + n) (p + m) == p + Qmin n m.
+Proof.
+ intros. apply min_monotone.
+ intros x x' Hx; rewrite Hx; auto with qarith.
+ intros x x' Hx. apply Qplus_le_compat; q_order.
+Qed.
+
+Lemma plus_min_distr_r : forall n m p, Qmin (n + p) (m + p) == Qmin n m + p.
+Proof.
+ intros. rewrite (Qplus_comm n p), (Qplus_comm m p), (Qplus_comm _ p).
+ apply plus_min_distr_l.
+Qed.
+
+End Q.
\ No newline at end of file
diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v
index efaefbb7..fa341dd9 100644
--- a/theories/QArith/Qpower.v
+++ b/theories/QArith/Qpower.v
@@ -59,7 +59,7 @@ Qed.
 
 Lemma Qmult_power : forall a b n, (a*b)^n == a^n*b^n.
 Proof.
-  intros a b [|n|n]; simpl; 
+  intros a b [|n|n]; simpl;
   try rewrite Qmult_power_positive;
   try rewrite Qinv_mult_distr;
   reflexivity.
@@ -73,7 +73,7 @@ Qed.
 
 Lemma Qinv_power : forall a n, (/a)^n == /a^n.
 Proof.
-  intros a [|n|n]; simpl; 
+  intros a [|n|n]; simpl;
   try rewrite Qinv_power_positive;
   reflexivity.
 Qed.
@@ -173,8 +173,8 @@ Qed.
 
 Lemma Qpower_mult : forall a n m, a^(n*m) ==  (a^n)^m.
 Proof.
-intros a [|n|n] [|m|m]; simpl; 
- try rewrite Qpower_positive_1; 
+intros a [|n|n] [|m|m]; simpl;
+ try rewrite Qpower_positive_1;
  try rewrite Qpower_mult_positive;
  try rewrite Qinv_power_positive;
  try rewrite Qinv_involutive;
diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v
index c98cef3f..12e371ee 100644
--- a/theories/QArith/Qreals.v
+++ b/theories/QArith/Qreals.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Qreals.v 10739 2008-04-01 14:45:20Z herbelin $ i*)
+(*i $Id$ i*)
 
 Require Export Rbase.
 Require Export QArith_base.
@@ -173,7 +173,7 @@ unfold Qinv, Q2R, Qeq in |- *; intros (x1, x2); unfold Qden, Qnum in |- *.
 case x1.
 simpl in |- *; intros; elim H; trivial.
 intros; field; auto.
-intros; 
+intros;
   change (IZR (Zneg x2)) with (- IZR (' x2))%R in |- *;
   change (IZR (Zneg p)) with (- IZR (' p))%R in |- *;
   field; (*auto 8 with real.*)
@@ -193,8 +193,8 @@ Hint Rewrite Q2R_plus Q2R_mult Q2R_opp Q2R_minus Q2R_inv Q2R_div : q2r_simpl.
 Section LegacyQField.
 
 (** In the past, the field tactic was not able to deal with setoid datatypes,
-    so translating from Q to R and applying field on reals was a workaround. 
-    See now Qfield for a direct field tactic on Q. *) 
+    so translating from Q to R and applying field on reals was a workaround.
+    See now Qfield for a direct field tactic on Q. *)
 
 Ltac QField := apply eqR_Qeq; autorewrite with q2r_simpl; try field; auto.
 
diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v
index 9c522f09..27e3c4e0 100644
--- a/theories/QArith/Qreduction.v
+++ b/theories/QArith/Qreduction.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Qreduction.v 10739 2008-04-01 14:45:20Z herbelin $ i*)
+(*i $Id$ i*)
 
 (** Normalisation functions for rational numbers. *)
 
@@ -35,15 +35,15 @@ Qed.
 (** Simplification of fractions using [Zgcd].
   This version can compute within Coq. *)
 
-Definition Qred (q:Q) := 
-  let (q1,q2) := q in 
-  let (r1,r2) := snd (Zggcd q1 ('q2)) 
+Definition Qred (q:Q) :=
+  let (q1,q2) := q in
+  let (r1,r2) := snd (Zggcd q1 ('q2))
   in r1#(Z2P r2).
 
 Lemma Qred_correct : forall q, (Qred q) == q.
 Proof.
   unfold Qred, Qeq; intros (n,d); simpl.
-  generalize (Zggcd_gcd n ('d)) (Zgcd_is_pos n ('d)) 
+  generalize (Zggcd_gcd n ('d)) (Zgcd_is_pos n ('d))
     (Zgcd_is_gcd n ('d)) (Zggcd_correct_divisors n ('d)).
   destruct (Zggcd n (Zpos d)) as (g,(nn,dd)); simpl.
   Open Scope Z_scope.
@@ -52,7 +52,7 @@ Proof.
   rewrite H3; rewrite H4.
   assert (0 <> g).
   intro; subst g; discriminate.
-  
+
   assert (0 < dd).
   apply Zmult_gt_0_lt_0_reg_r with g.
   omega.
@@ -68,10 +68,10 @@ Proof.
   intros (a,b) (c,d).
   unfold Qred, Qeq in *; simpl in *.
   Open Scope Z_scope.
-  generalize (Zggcd_gcd a ('b)) (Zgcd_is_gcd a ('b)) 
+  generalize (Zggcd_gcd a ('b)) (Zgcd_is_gcd a ('b))
     (Zgcd_is_pos a ('b)) (Zggcd_correct_divisors a ('b)).
   destruct (Zggcd a (Zpos b)) as (g,(aa,bb)).
-  generalize (Zggcd_gcd c ('d)) (Zgcd_is_gcd c ('d)) 
+  generalize (Zggcd_gcd c ('d)) (Zgcd_is_gcd c ('d))
     (Zgcd_is_pos c ('d)) (Zggcd_correct_divisors c ('d)).
   destruct (Zggcd c (Zpos d)) as (g',(cc,dd)).
   simpl.
@@ -136,7 +136,7 @@ Proof.
   Close Scope Z_scope.
 Qed.
 
-Add Morphism Qred : Qred_comp. 
+Add Morphism Qred : Qred_comp.
 Proof.
   intros q q' H.
   rewrite (Qred_correct q); auto.
@@ -144,7 +144,7 @@ Proof.
 Qed.
 
 Definition Qplus' (p q : Q) := Qred (Qplus p q).
-Definition Qmult' (p q : Q) := Qred (Qmult p q). 
+Definition Qmult' (p q : Q) := Qred (Qmult p q).
 Definition Qminus' x y := Qred (Qminus x y).
 
 Lemma Qplus'_correct : forall p q : Q, (Qplus' p q)==(Qplus p q).
diff --git a/theories/QArith/Qring.v b/theories/QArith/Qring.v
index 2d45d537..8c9e2dfa 100644
--- a/theories/QArith/Qring.v
+++ b/theories/QArith/Qring.v
@@ -6,6 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Qring.v 10739 2008-04-01 14:45:20Z herbelin $ i*)
+(*i $Id$ i*)
 
 Require Export Qfield.
diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v
index 3f191c75..8162a702 100644
--- a/theories/QArith/Qround.v
+++ b/theories/QArith/Qround.v
@@ -122,7 +122,7 @@ Qed.
 
 Hint Resolve Qceiling_resp_le : qarith.
 
-Add Morphism Qfloor with signature Qeq ==> @eq _ as Qfloor_comp.
+Add Morphism Qfloor with signature Qeq ==> eq as Qfloor_comp.
 Proof.
 intros x y H.
 apply Zle_antisym.
@@ -130,7 +130,7 @@ apply Zle_antisym.
 symmetry in H; auto with *.
 Qed.
 
-Add Morphism Qceiling with signature Qeq ==> @eq _ as Qceiling_comp.
+Add Morphism Qceiling with signature Qeq ==> eq as Qceiling_comp.
 Proof.
 intros x y H.
 apply Zle_antisym.
diff --git a/theories/QArith/vo.itarget b/theories/QArith/vo.itarget
new file mode 100644
index 00000000..b3faef88
--- /dev/null
+++ b/theories/QArith/vo.itarget
@@ -0,0 +1,12 @@
+Qabs.vo
+QArith_base.vo
+QArith.vo
+Qcanon.vo
+Qfield.vo
+Qpower.vo
+Qreals.vo
+Qreduction.vo
+Qring.vo
+Qround.vo
+QOrderedType.vo
+Qminmax.vo
\ No newline at end of file