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, 29 insertions, 103 deletions

diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v
index 62948093f..c52fc0dd0 100644
--- a/theories/Arith/Min.v
+++ b/theories/Arith/Min.v
@@ -8,111 +8,37 @@
 
 (*i $Id$ i*)
 
-Require Import Le.
+(** THIS FILE IS DEPRECATED. Use [MinMax] instead. *)
 
-Open Local Scope nat_scope.
+Require Export MinMax.
 
+Open Local Scope nat_scope.
 Implicit Types m n p : nat.
 
-(** * minimum of two natural numbers *)
-
-Fixpoint min n m : nat :=
-  match n, m with
-    | O, _ => 0
-    | S n', O => 0
-    | S n', S m' => S (min n' m')
-  end.
-
-(** * Simplifications of [min] *)
-
-Lemma min_0_l : forall n : nat, min 0 n = 0.
-Proof.
-  trivial.
-Qed.
-
-Lemma min_0_r : forall n : nat, min n 0 = 0.
-Proof.
-  destruct n; trivial.
-Qed.
-
-Lemma min_SS : forall n m, S (min n m) = min (S n) (S m).
-Proof.
-  auto with arith.
-Qed.
-
-(** * [min n m] is equal to [n] or [m] *)
-
-Lemma min_dec : forall n m, {min n m = n} + {min n m = m}.
-Proof.
-  induction n; induction m; simpl in |- *; auto with arith.
-  elim (IHn m); intro H; elim H; auto.
-Qed.
-
-Lemma min_case : forall n m (P:nat -> Type), P n -> P m -> P (min n m).
-Proof.
-  induction n; simpl in |- *; auto with arith.
-  induction m; intros; simpl in |- *; auto with arith.
-  pattern (min n m) in |- *; apply IHn; auto with arith.
-Qed.
-
-(** * Semi-lattice algebraic properties of [min] *)
-
-Lemma min_idempotent : forall n, min n n = n.
-Proof.
-  induction n; simpl; [|rewrite IHn]; trivial.
-Qed.
-
-Lemma min_assoc : forall m n p : nat, min m (min n p) = min (min m n) p.
-Proof.
-  induction m; destruct n; destruct p; trivial.
-  simpl.
-  auto using (IHm n p).
-Qed.
-
-Lemma min_comm : forall n m, min n m = min m n.
-Proof.
-  induction n; induction m; simpl in |- *; auto with arith.
-Qed.
-
-(** * Least-upper bound properties of [min] *)
-
-Lemma min_l : forall n m, n <= m -> min n m = n.
-Proof.
-  induction n; induction m; simpl in |- *; auto with arith.
-Qed.
-
-Lemma min_r : forall n m, m <= n -> min n m = m.
-Proof.
-  induction n; induction m; simpl in |- *; auto with arith.
-Qed.
-
-Lemma le_min_l : forall n m, min n m <= n.
-Proof.
-  induction n; intros; simpl in |- *; auto with arith.
-  elim m; intros; simpl in |- *; auto with arith.
-Qed.
-
-Lemma le_min_r : forall n m, min n m <= m.
-Proof.
-  induction n; simpl in |- *; auto with arith.
-  induction m; simpl in |- *; auto with arith.
-Qed.
-Hint Resolve min_l min_r le_min_l le_min_r: arith v62.
-
-Lemma min_glb_l : forall n m p, p <= min n m -> p <= n.
-Proof.
-intros; eapply le_trans; [eassumption|apply le_min_l].
-Qed.
-
-Lemma min_glb_r : forall n m p, p <= min n m -> p <= m.
-Proof.
-intros; eapply le_trans; [eassumption|apply le_min_r].
-Qed.
-
-Lemma min_glb : forall n m p, p <= n -> p <= m -> p <= min n m.
-Proof.
-  intros n m p; apply min_case; auto.
-Qed.
-
+Notation min := MinMax.min (only parsing).
+
+Definition min_0_l := min_0_l.
+Definition min_0_r := min_0_r.
+Definition succ_min_distr := succ_min_distr.
+Definition plus_min_distr_l := plus_min_distr_l.
+Definition plus_min_distr_r := plus_min_distr_r.
+Definition min_case_strong := min_case_strong.
+Definition min_spec := min_spec.
+Definition min_dec := min_dec.
+Definition min_case := min_case.
+Definition min_idempotent := min_id.
+Definition min_assoc := min_assoc.
+Definition min_comm := min_comm.
+Definition min_l := min_l.
+Definition min_r := min_r.
+Definition le_min_l := le_min_l.
+Definition le_min_r := le_min_r.
+Definition min_glb_l := min_glb_l.
+Definition min_glb_r := min_glb_r.
+Definition min_glb := min_glb.
+
+(* begin hide *)
+(* Compatibility *)
 Notation min_case2 := min_case (only parsing).
-
+Notation min_SS := succ_min_distr (only parsing).
+(* end hide *)
\ No newline at end of file