OrderedType implementation for various numerical datatypes + min/max structures

 - A richer OrderedTypeFull interface : OrderedType + predicate "le"
 - Implementations {Nat,N,P,Z,Q}OrderedType.v, also providing "order" tactics
 - By the way: as suggested by S. Lescuyer, specification of compare is
   now inductive
 - GenericMinMax: axiomatisation + properties of min and max out of
    OrderedTypeFull structures.
 - MinMax.v, {Z,P,N,Q}minmax.v are specialization of GenericMinMax,
    with also some domain-specific results, and compatibility layer
    with already existing results.
 - Some ML code of plugins had to be adapted, otherwise wrong "eq",
   "lt" or simimlar constants were found by functions like coq_constant.
 - Beware of the aliasing problems: for instance eq:=@eq t instead of
   eq:=@eq M.t in Make_UDT made (r)omega stopped working (Z_as_OT.t
   instead of Z in statement of Zmax_spec).
 - Some Morphism declaration are now ambiguous: switch to new syntax
   anyway.
 - Misc adaptations of FSets/MSets
 - Classes/RelationPairs.v: from two relations over A and B, we
   inspect relations over A*B and their properties in terms of classes.

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

3 files changed, 260 insertions, 88 deletions

diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index c87c9df9e..70830ad80 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -10,7 +10,7 @@
 
 Require Export ZArith.
 Require Export ZArithRing.
-Require Export Setoid Bool.
+Require Export Morphisms Setoid Bool.
 
 (** * Definition of [Q] and basic properties *)
 
@@ -101,7 +101,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 +110,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}.
@@ -155,18 +164,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 +215,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 +229,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 +259,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 +277,49 @@ Proof.
   Close Scope Z_scope.
 Qed.
 
-Add Morphism Qdiv : Qdiv_comp.
+Instance Qdiv_comp : Proper (Qeq==>Qeq==>Qeq) Qdiv.
 Proof.
-  intros; unfold Qdiv.
-  rewrite H; rewrite H0; auto with qarith.
+  intros x x' Hx y y' Hy; unfold Qdiv.
+  rewrite Hx, Hy; auto with qarith.
 Qed.
 
-Add Morphism Qle with signature Qeq ==> Qeq ==> iff as Qle_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, Qle; simpl.
+  unfold Qeq, Qcompare.
   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.
+  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 Qlt with signature Qeq ==> Qeq ==> iff as  Qlt_comp.
+Instance Qle_comp : Proper (Qeq==>Qeq==>iff) Qle.
 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.
-  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.
-  Close Scope Z_scope.
+  intros p q H r s H'. rewrite 2 Qle_alt, H, H'; auto with *.
 Qed.
 
-Add Morphism Qeq_bool with signature Qeq ==> Qeq ==> (@eq bool) as Qeqb_comp.
+Instance Qlt_compat : Proper (Qeq==>Qeq==>iff) Qlt.
 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 Qlt_alt, H, H'; auto with *.
 Qed.
 
-Add Morphism Qle_bool with signature Qeq ==> Qeq ==> (@eq bool) as Qleb_comp.
+Instance Qeqb_comp : Proper (Qeq==>Qeq==>eq) Qeq_bool.
 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'; apply eq_true_iff_eq.
+ rewrite 2 Qeq_bool_iff, H, H'; split; auto with qarith.
 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 Qleb_comp : Proper (Qeq==>Qeq==>eq) Qle_bool.
 Proof.
-  intros.
-  do 2 rewrite Qeq_alt in H0.
-  unfold Qeq, Qlt, Qcompare in *.
-  apply Zcompare_egal_dec; auto.
-  omega.
-Qed.
-
-Add Morphism Qcompare : Qcompare_comp.
-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 +516,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 +528,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.
@@ -835,9 +809,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;
@@ -854,8 +828,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 000000000..3d83eac38
--- /dev/null
+++ b/theories/QArith/QOrderedType.v
@@ -0,0 +1,68 @@
+(************************************************************************)
+(*  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
+ DecidableType2 OrderedType2 OrderedType2Facts.
+
+Local Open Scope Q_scope.
+
+(** * DecidableType structure for rational numbers *)
+
+Module Q_as_DT <: DecidableType.
+ Definition t := Q.
+ Definition eq := Qeq.
+ Instance eq_equiv : Equivalence Qeq.
+ Definition eq_dec := Qeq_dec.
+
+ (** The next fields are not mandatory, but allow [Q_as_DT] to be
+     also a [DecidableTypeOrig]. *)
+ Definition eq_refl := Qeq_refl.
+ Definition eq_sym := Qeq_sym.
+ Definition eq_trans := eq_trans.
+End Q_as_DT.
+
+
+(** * 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.
+
+ Lemma Qcompare_antisym : forall x y, CompOpp (x ?= y) = (y ?= x).
+ Proof.
+ unfold "?=". intros. apply Zcompare_antisym.
+ Qed.
+
+ Lemma compare_spec : forall x y, Cmp Qeq Qlt x y (Qcompare x y).
+ Proof.
+ intros.
+ destruct (x ?= y) as [ ]_eqn:H; constructor; auto.
+ rewrite Qeq_alt; auto.
+ rewrite Qlt_alt, <- Qcompare_antisym, H; auto.
+ Qed.
+
+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/Qminmax.v b/theories/QArith/Qminmax.v
new file mode 100644
index 000000000..e9d2f79ab
--- /dev/null
+++ b/theories/QArith/Qminmax.v
@@ -0,0 +1,130 @@
+(************************************************************************)
+(*  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 OrderedType2 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_spec := QMM.max_spec.
+ Definition min_spec := QMM.min_spec.
+End QHasMinMax.
+
+(** We obtain hence all the generic properties of max and min. *)
+
+Module Import QMinMaxProps := MinMaxProperties Q_as_OT QHasMinMax.
+
+Definition Qmax_case_strong := max_case_strong.
+Definition Qmax_case := max_case.
+Definition Qmax_monotone := max_monotone.
+Definition Qmax_spec := max_spec.
+Definition Qmax_spec_le := max_spec_le.
+Definition Qmax_dec := max_dec.
+Definition Qmax_unicity := max_unicity.
+Definition Qmax_unicity_ext := max_unicity_ext.
+Definition Qmax_id := max_id.
+Notation Qmax_idempotent := Qmax_id (only parsing).
+Definition Qmax_assoc := max_assoc.
+Definition Qmax_comm := max_comm.
+Definition Qmax_l := max_l.
+Definition Qmax_r := max_r.
+Definition Nle_max_l := le_max_l.
+Definition Nle_max_r := le_max_r.
+Definition Qmax_le := max_le.
+Definition Qmax_le_iff := max_le_iff.
+Definition Qmax_lt_iff := max_lt_iff.
+Definition Qmax_lub_l := max_lub_l.
+Definition Qmax_lub_r := max_lub_r.
+Definition Qmax_lub := max_lub.
+Definition Qmax_lub_iff := max_lub_iff.
+Definition Qmax_lub_lt := max_lub_lt.
+Definition Qmax_lub_lt_iff := max_lub_lt_iff.
+Definition Qmax_le_compat_l := max_le_compat_l.
+Definition Qmax_le_compat_r := max_le_compat_r.
+Definition Qmax_le_compat := max_le_compat.
+
+Definition Qmin_case_strong := min_case_strong.
+Definition Qmin_case := min_case.
+Definition Qmin_monotone := min_monotone.
+Definition Qmin_spec := min_spec.
+Definition Qmin_spec_le := min_spec_le.
+Definition Qmin_dec := min_dec.
+Definition Qmin_unicity := min_unicity.
+Definition Qmin_unicity_ext := min_unicity_ext.
+Definition Qmin_id := min_id.
+Notation Qmin_idempotent := Qmin_id (only parsing).
+Definition Qmin_assoc := min_assoc.
+Definition Qmin_comm := min_comm.
+Definition Qmin_l := min_l.
+Definition Qmin_r := min_r.
+Definition Nle_min_l := le_min_l.
+Definition Nle_min_r := le_min_r.
+Definition Qmin_le := min_le.
+Definition Qmin_le_iff := min_le_iff.
+Definition Qmin_lt_iff := min_lt_iff.
+Definition Qmin_glb_l := min_glb_l.
+Definition Qmin_glb_r := min_glb_r.
+Definition Qmin_glb := min_glb.
+Definition Qmin_glb_iff := min_glb_iff.
+Definition Qmin_glb_lt := min_glb_lt.
+Definition Qmin_glb_lt_iff := min_glb_lt_iff.
+Definition Qmin_le_compat_l := min_le_compat_l.
+Definition Qmin_le_compat_r := min_le_compat_r.
+Definition Qmin_le_compat := min_le_compat.
+
+Definition Qmin_max_absorption := min_max_absorption.
+Definition Qmax_min_absorption := max_min_absorption.
+Definition Qmax_min_distr := max_min_distr.
+Definition Qmin_max_distr := min_max_distr.
+Definition Qmax_min_modular := max_min_modular.
+Definition Qmin_max_modular := min_max_modular.
+Definition Qmax_min_disassoc := max_min_disassoc.
+Definition Qmax_min_antimonotone := max_min_antimonotone.
+Definition Qmin_max_antimonotone := min_max_antimonotone.
+
+
+
+(** * Properties specific to the [Q] domain *)
+
+(** Compatibilities (consequences of monotonicity) *)
+
+Lemma Qplus_max_distr_l : forall n m p, Qmax (p + n) (p + m) == p + Qmax n m.
+Proof.
+ intros. apply Qmax_monotone.
+ intros x x' Hx; rewrite Hx; auto with qarith.
+ intros x x' Hx. apply Qplus_le_compat; q_order.
+Qed.
+
+Lemma Qplus_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 Qplus_max_distr_l.
+Qed.
+
+Lemma Qplus_min_distr_l : forall n m p, Qmin (p + n) (p + m) == p + Qmin n m.
+Proof.
+ intros. apply Qmin_monotone.
+ intros x x' Hx; rewrite Hx; auto with qarith.
+ intros x x' Hx. apply Qplus_le_compat; q_order.
+Qed.
+
+Lemma Qplus_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 Qplus_min_distr_l.
+Qed.