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

1 files changed, 50 insertions, 140 deletions

diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v
index dd46e885d..e6582a775 100644
--- a/theories/ZArith/Zmax.v
+++ b/theories/ZArith/Zmax.v
@@ -7,190 +7,100 @@
 (************************************************************************)
 (*i $Id$ i*)
 
-Require Import Arith_base.
-Require Import BinInt.
-Require Import Zcompare.
-Require Import Zorder.
+(** THIS FILE IS DEPRECATED. Use [Zminmax] instead. *)
+
+Require Export BinInt Zorder Zminmax.
 
 Open Local Scope Z_scope.
 
-(******************************************)
-(** Maximum of two binary integer numbers *)
+(** [Zmax] is now [Zminmax.Zmax]. Code that do things like
+  [unfold Zmin.Zmin] will have to be adapted, and neither
+  a [Definition] or a [Notation] here can help much. *)
 
-Definition Zmax m n :=
-  match m ?= n with
-    | Eq | Gt => m
-    | Lt => n
-  end.
 
 (** * Characterization of maximum on binary integer numbers *)
 
-Lemma Zmax_case : forall (n m:Z) (P:Z -> Type), P n -> P m -> P (Zmax n m).
-Proof.
-  intros n m P H1 H2; unfold Zmax in |- *; case (n ?= m); auto with arith.
-Qed.
+Definition Zmax_case := Zmax_case.
+Definition Zmax_case_strong := Zmax_case_strong.
 
-Lemma Zmax_case_strong : forall (n m:Z) (P:Z -> Type),
-  (m<=n -> P n) -> (n<=m -> P m) -> P (Zmax n m).
+Lemma Zmax_spec : forall x y,
+  x >= y /\ Zmax x y = x  \/ x < y /\ Zmax x y = y.
 Proof.
-  intros n m P H1 H2; unfold Zmax, Zle, Zge in *.
-  rewrite <- (Zcompare_antisym n m) in H1.
-  destruct (n ?= m); (apply H1|| apply H2); discriminate.
+ intros x y. rewrite Zge_iff_le. destruct (Zmax_spec x y); auto.
 Qed.
 
-Lemma Zmax_spec : forall x y:Z,
-  x >= y /\ Zmax x y = x  \/
-  x < y /\ Zmax x y = y.
-Proof.
- intros; unfold Zmax, Zlt, Zge.
- destruct (Zcompare x y); [ left | right | left ]; split; auto; discriminate.
-Qed.
+Lemma Zmax_left : forall n m, n>=m -> Zmax n m = n.
+Proof. intros x y. rewrite Zge_iff_le. apply Zmax_l. Qed.
 
-Lemma Zmax_left : forall n m:Z, n>=m -> Zmax n m = n.
-Proof.
-  intros n m; unfold Zmax, Zge; destruct (n ?= m); auto.
-  intro H; elim H; auto.
-Qed.
-
-Lemma Zmax_right : forall n m:Z, n<=m -> Zmax n m = m.
-Proof.
-  intros n m; unfold Zmax, Zle.
-  generalize (Zcompare_Eq_eq n m).
-  destruct (n ?= m); auto.
-  intros _ H; elim H; auto.
-Qed.
+Definition Zmax_right : forall n m, n<=m -> Zmax n m = m := Zmax_r.
 
 (** * Least upper bound properties of max *)
 
-Lemma Zle_max_l : forall n m:Z, n <= Zmax n m.
-Proof.
-  intros; apply Zmax_case_strong; auto with zarith.
-Qed.
+Definition Zle_max_l : forall n m, n <= Zmax n m := Zle_max_l.
+Definition Zle_max_r : forall n m, m <= Zmax n m := Zle_max_r.
 
-(* begin hide *)
-Notation Zmax1 := Zle_max_l (only parsing).
-(* end hide *)
+Definition Zmax_lub : forall n m p, n <= p -> m <= p -> Zmax n m <= p
+ := Zmax_lub.
 
-Lemma Zle_max_r : forall n m:Z, m <= Zmax n m.
-Proof.
-  intros; apply Zmax_case_strong; auto with zarith.
-Qed.
-
-(* begin hide *)
-Notation Zmax2 := Zle_max_r (only parsing).
-(* end hide *)
-
-Lemma Zmax_lub : forall n m p:Z, n <= p -> m <= p -> Zmax n m <= p.
-Proof.
-  intros; apply Zmax_case; assumption.
-Qed.
+Definition Zmax_lub_lt : forall n m p:Z, n < p -> m < p -> Zmax n m < p
+ := Zmax_lub_lt.
 
-Lemma Zmax_lub_lt : forall n m p:Z, n < p -> m < p -> Zmax n m < p.
-Proof.
-  intros; apply Zmax_case; assumption.
-Qed.
 
 (** * Compatibility with order *)
 
-Lemma Zle_max_compat_r : forall n m p, n <= m -> Zmax n p <= Zmax m p.
-Proof.
-  intros; do 2 (apply Zmax_case_strong; intro); eauto using Zle_trans, Zle_refl.
-Qed.
-
-Lemma Zle_max_compat_l : forall n m p, n <= m -> Zmax p n <= Zmax p m.
-Proof.
-  intros; do 2 (apply Zmax_case_strong; intro); eauto using Zle_trans, Zle_refl.
-Qed.
+Definition Zle_max_compat_r : forall n m p, n <= m -> Zmax n p <= Zmax m p
+ := Zmax_le_compat_r.
 
-(** * Semi-lattice properties of max *)
+Definition Zle_max_compat_l : forall n m p, n <= m -> Zmax p n <= Zmax p m
+ := Zmax_le_compat_l.
 
-Lemma Zmax_idempotent : forall n:Z, Zmax n n = n.
-Proof.
-  intros; apply Zmax_case; auto.
-Qed.
 
-Lemma Zmax_comm : forall n m:Z, Zmax n m = Zmax m n.
-Proof.
-  intros; do 2 apply Zmax_case_strong; intros;
-    apply Zle_antisym; auto with zarith.
-Qed.
+(** * Semi-lattice properties of max *)
 
-Lemma Zmax_assoc : forall n m p:Z, Zmax n (Zmax m p) = Zmax (Zmax n m) p.
-Proof.
-  intros n m p; repeat apply Zmax_case_strong; intros;
-    reflexivity || (try apply Zle_antisym); eauto with zarith.
-Qed.
+Definition Zmax_idempotent : forall n, Zmax n n = n := Zmax_id.
+Definition Zmax_comm : forall n m, Zmax n m = Zmax m n := Zmax_comm.
+Definition Zmax_assoc : forall n m p, Zmax n (Zmax m p) = Zmax (Zmax n m) p
+ := Zmax_assoc.
 
 (** * Additional properties of max *)
 
-Lemma Zmax_irreducible_dec : forall n m:Z, {Zmax n m = n} + {Zmax n m = m}.
-Proof.
-  intros; apply Zmax_case; auto.
-Qed.
+Lemma Zmax_irreducible_dec : forall n m, {Zmax n m = n} + {Zmax n m = m}.
+Proof. exact Zmax_dec. Qed.
+
+Definition Zmax_le_prime : forall n m p, p <= Zmax n m -> p <= n \/ p <= m
+ := Zmax_le.
 
-Lemma Zmax_le_prime : forall n m p:Z, p <= Zmax n m -> p <= n \/ p <= m.
-Proof.
-  intros n m p; apply Zmax_case; auto.
-Qed.
 
 (** * Operations preserving max *)
 
-Lemma Zsucc_max_distr :
-  forall n m:Z, Zsucc (Zmax n m) = Zmax (Zsucc n) (Zsucc m).
-Proof.
-  intros n m; unfold Zmax in |- *; rewrite (Zcompare_succ_compat n m);
-    elim_compare n m; intros E; rewrite E; auto with arith.
-Qed.
+Definition Zsucc_max_distr :
+  forall n m:Z, Zsucc (Zmax n m) = Zmax (Zsucc n) (Zsucc m)
+ := Zsucc_max_distr.
 
-Lemma Zplus_max_distr_l : forall n m p:Z, Zmax (p + n) (p + m) = p + Zmax n m.
-Proof.
-  intros n m p; unfold Zmax.
-  rewrite (Zcompare_plus_compat n m p).
-  destruct (n ?= m); trivial.
-Qed.
+Definition Zplus_max_distr_l : forall n m p:Z, Zmax (p + n) (p + m) = p + Zmax n m
+ := Zplus_max_distr_l.
 
-Lemma Zplus_max_distr_r : forall n m p:Z, Zmax (n + p) (m + p) = Zmax n m + p.
-Proof.
-  intros n m p; repeat rewrite (Zplus_comm _ p); apply Zplus_max_distr_l.
-Qed.
+Definition Zplus_max_distr_r : forall n m p:Z, Zmax (n + p) (m + p) = Zmax n m + p
+ := Zplus_max_distr_r.
 
 (** * Maximum and Zpos *)
 
-Lemma Zpos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q).
-Proof.
-  intros; unfold Zmax, Pmax; simpl; generalize (Pcompare_Eq_eq p q).
-  destruct Pcompare; auto.
-  intro H; rewrite H; auto.
-Qed.
+Definition Zpos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q)
+ := Zpos_max.
 
-Lemma Zpos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p.
-Proof.
-  intros; unfold Zmax; simpl; destruct p; simpl; auto.
-Qed.
+Definition Zpos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p
+ := Zpos_max_1.
 
 (** * Characterization of Pminus in term of Zminus and Zmax *)
 
-Lemma Zpos_minus : forall p q, Zpos (Pminus p q) = Zmax 1 (Zpos p - Zpos q).
-Proof.
-  intros.
-  case_eq (Pcompare p q Eq).
-  intros H; rewrite (Pcompare_Eq_eq _ _ H).
-  rewrite Zminus_diag.
-  unfold Zmax; simpl.
-  unfold Pminus; rewrite Pminus_mask_diag; auto.
-  intros; rewrite Pminus_Lt; auto.
-  destruct (Zmax_spec 1 (Zpos p - Zpos q)) as [(H1,H2)|(H1,H2)]; auto.
-  exfalso; clear H2.
-  assert (H1':=Zlt_trans 0 1 _ Zlt_0_1 H1).
-  generalize (Zlt_0_minus_lt _ _ H1').
-  unfold Zlt; simpl.
-  rewrite (ZC2 _ _ H); intro; discriminate.
-  intros; simpl; rewrite H.
-  symmetry; apply Zpos_max_1.
-Qed.
+Definition Zpos_minus :
+ forall p q, Zpos (Pminus p q) = Zmax 1 (Zpos p - Zpos q)
+ := Zpos_minus.
 
 (* begin hide *)
 (* Compatibility *)
+Notation Zmax1 := Zle_max_l (only parsing).
+Notation Zmax2 := Zle_max_r (only parsing).
 Notation Zmax_irreducible_inf := Zmax_irreducible_dec (only parsing).
 Notation Zmax_le_prime_inf := Zmax_le_prime (only parsing).
 (* end hide *)