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, 40 insertions, 114 deletions

diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v
index de83af137..0278b604b 100644
--- a/theories/ZArith/Zmin.v
+++ b/theories/ZArith/Zmin.v
@@ -1,4 +1,3 @@
-(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -8,157 +7,84 @@
 (************************************************************************)
 (*i $Id$ i*)
 
-(** Initial version from Pierre Crégut (CNET, Lannion, France), 1996.
-    Further extensions by the Coq development team, with suggestions
-    from Russell O'Connor (Radbout U., Nijmegen, The Netherlands).
- *)
+(** THIS FILE IS DEPRECATED. Use [Zminmax] instead. *)
 
-Require Import Arith_base.
-Require Import BinInt.
-Require Import Zcompare.
-Require Import Zorder.
+Require Import BinInt Zorder Zminmax.
 
 Open Local Scope Z_scope.
 
-(**************************************)
-(** Minimum on binary integer numbers *)
+(** [Zmin] is now [Zminmax.Zmin]. Code that do things like
+  [unfold Zmin.Zmin] will have to be adapted, and neither
+  a [Definition] or a [Notation] here can help much. *)
 
-Unboxed Definition Zmin (n m:Z) :=
-  match n ?= m with
-    | Eq | Lt => n
-    | Gt => m
-  end.
 
 (** * Characterization of the minimum on binary integer numbers *)
 
-Lemma Zmin_case_strong : forall (n m:Z) (P:Z -> Type),
-  (n<=m -> P n) -> (m<=n -> P m) -> P (Zmin n m).
-Proof.
-  intros n m P H1 H2; unfold Zmin, Zle, Zge in *.
-  rewrite <- (Zcompare_antisym n m) in H2.
-  destruct (n ?= m); (apply H1|| apply H2); discriminate.
-Qed.
-
-Lemma Zmin_case : forall (n m:Z) (P:Z -> Type), P n -> P m -> P (Zmin n m).
-Proof.
-  intros n m P H1 H2; unfold Zmin in |- *; case (n ?= m); auto with arith.
-Qed.
+Definition Zmin_case := Zmin_case.
+Definition Zmin_case_strong := Zmin_case_strong.
 
-Lemma Zmin_spec : forall x y:Z,
-  x <= y /\ Zmin x y = x  \/
-  x > y /\ Zmin x y = y.
+Lemma Zmin_spec : forall x y,
+  x <= y /\ Zmin x y = x  \/  x > y /\ Zmin x y = y.
 Proof.
- intros; unfold Zmin, Zle, Zgt.
- destruct (Zcompare x y); [ left | left | right ]; split; auto; discriminate.
+ intros x y. rewrite Zgt_iff_lt, Zmin_comm. destruct (Zmin_spec y x); auto.
 Qed.
 
 (** * Greatest lower bound properties of min *)
 
-Lemma Zle_min_l : forall n m:Z, Zmin n m <= n.
-Proof.
-  intros n m; unfold Zmin in |- *; elim_compare n m; intros E; rewrite E;
-    [ apply Zle_refl
-      | apply Zle_refl
-      | apply Zlt_le_weak; apply Zgt_lt; exact E ].
-Qed.
-
-Lemma Zle_min_r : forall n m:Z, Zmin n m <= m.
-Proof.
-  intros n m; unfold Zmin in |- *; elim_compare n m; intros E; rewrite E;
-    [ unfold Zle in |- *; rewrite E; discriminate
-      | unfold Zle in |- *; rewrite E; discriminate
-      | apply Zle_refl ].
-Qed.
-
-Lemma Zmin_glb : forall n m p:Z, p <= n -> p <= m -> p <= Zmin n m.
-Proof.
-  intros; apply Zmin_case; assumption.
-Qed.
+Definition Zle_min_l : forall n m, Zmin n m <= n := Zle_min_l.
+Definition Zle_min_r : forall n m, Zmin n m <= m := Zle_min_r.
 
-Lemma Zmin_glb_lt : forall n m p:Z, p < n -> p < m -> p < Zmin n m.
-Proof.
-  intros; apply Zmin_case; assumption.
-Qed.
+Definition Zmin_glb : forall n m p, p <= n -> p <= m -> p <= Zmin n m
+ := Zmin_glb.
+Definition Zmin_glb_lt : forall n m p, p < n -> p < m -> p < Zmin n m
+ := Zmin_glb_lt.
 
 (** * Compatibility with order *)
 
-Lemma Zle_min_compat_r : forall n m p, n <= m -> Zmin n p <= Zmin m p.
-Proof.
-  intros; do 2 (apply Zmin_case_strong; intro); eauto using Zle_trans, Zle_refl.
-Qed.
-
-Lemma Zle_min_compat_l : forall n m p, n <= m -> Zmin p n <= Zmin p m.
-Proof.
-  intros; do 2 (apply Zmin_case_strong; intro); eauto using Zle_trans, Zle_refl.
-Qed.
+Definition Zle_min_compat_r : forall n m p, n <= m -> Zmin n p <= Zmin m p
+ := Zmin_le_compat_r.
+Definition Zle_min_compat_l : forall n m p, n <= m -> Zmin p n <= Zmin p m
+ := Zmin_le_compat_l.
 
 (** * Semi-lattice properties of min *)
 
-Lemma Zmin_idempotent : forall n:Z, Zmin n n = n.
-Proof.
-  unfold Zmin in |- *; intros; elim (n ?= n); auto.
-Qed.
-
+Definition Zmin_idempotent : forall n, Zmin n n = n := Zmin_id.
 Notation Zmin_n_n := Zmin_idempotent (only parsing).
-
-Lemma Zmin_comm : forall n m:Z, Zmin n m = Zmin m n.
-Proof.
-  intros n m; unfold Zmin.
-  rewrite <- (Zcompare_antisym n m).
-  assert (H:=Zcompare_Eq_eq n m).
-  destruct (n ?= m); simpl; auto.
-Qed.
-
-Lemma Zmin_assoc : forall n m p:Z, Zmin n (Zmin m p) = Zmin (Zmin n m) p.
-Proof.
-  intros n m p; repeat apply Zmin_case_strong; intros;
-    reflexivity || (try apply Zle_antisym); eauto with zarith.
-Qed.
+Definition Zmin_comm : forall n m, Zmin n m = Zmin m n := Zmin_comm.
+Definition Zmin_assoc : forall n m p, Zmin n (Zmin m p) = Zmin (Zmin n m) p
+ := Zmin_assoc.
 
 (** * Additional properties of min *)
 
-Lemma Zmin_irreducible_inf : forall n m:Z, {Zmin n m = n} + {Zmin n m = m}.
-Proof.
-  unfold Zmin in |- *; intros; elim (n ?= m); auto.
-Qed.
+Lemma Zmin_irreducible_inf : forall n m, {Zmin n m = n} + {Zmin n m = m}.
+Proof. exact Zmin_dec. Qed.
 
-Lemma Zmin_irreducible : forall n m:Z, Zmin n m = n \/ Zmin n m = m.
-Proof.
-  intros n m; destruct (Zmin_irreducible_inf n m); [left|right]; trivial.
-Qed.
+Lemma Zmin_irreducible : forall n m, Zmin n m = n \/ Zmin n m = m.
+Proof. intros; destruct (Zmin_dec n m); auto. Qed.
 
 Notation Zmin_or := Zmin_irreducible (only parsing).
 
-Lemma Zmin_le_prime_inf : forall n m p:Z, Zmin n m <= p -> {n <= p} + {m <= p}.
-Proof.
-  intros n m p; apply Zmin_case; auto.
-Qed.
+Lemma Zmin_le_prime_inf : forall n m p, Zmin n m <= p -> {n <= p} + {m <= p}.
+Proof. intros n m p; apply Zmin_case; auto. Qed.
 
 (** * Operations preserving min *)
 
-Lemma Zsucc_min_distr :
-  forall n m:Z, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m).
-Proof.
-  intros n m; unfold Zmin in |- *; rewrite (Zcompare_succ_compat n m);
-    elim_compare n m; intros E; rewrite E; auto with arith.
-Qed.
+Definition Zsucc_min_distr :
+ forall n m, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m)
+ := Zsucc_min_distr.
 
 Notation Zmin_SS := Zsucc_min_distr (only parsing).
 
-Lemma Zplus_min_distr_r : forall n m p:Z, Zmin (n + p) (m + p) = Zmin n m + p.
-Proof.
-  intros x y n; unfold Zmin in |- *.
-  rewrite (Zplus_comm x n); rewrite (Zplus_comm y n);
-    rewrite (Zcompare_plus_compat x y n).
-  case (x ?= y); apply Zplus_comm.
-Qed.
+Definition Zplus_min_distr_r :
+ forall n m p, Zmin (n + p) (m + p) = Zmin n m + p
+ := Zplus_min_distr_r.
 
 Notation Zmin_plus := Zplus_min_distr_r (only parsing).
 
 (** * Minimum and Zpos *)
 
-Lemma Zpos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q).
-Proof.
-  intros; unfold Zmin, Pmin; simpl; destruct Pcompare; auto.
-Qed.
+Definition Zpos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q)
+ := Zpos_min.
+
+