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, 24 insertions, 117 deletions

diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index 62250fc33..3d7fe9fc2 100644
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.v
@@ -8,127 +8,34 @@
 
 (*i $Id$ i*)
 
-Require Import Le Plus.
+(** THIS FILE IS DEPRECATED. Use [MinMax] instead. *)
 
-Open Local Scope nat_scope.
+Require Export MinMax.
 
+Local Open Scope nat_scope.
 Implicit Types m n p : nat.
 
-(** * Maximum of two natural numbers *)
-
-Fixpoint max n m : nat :=
-  match n, m with
-    | O, _ => m
-    | S n', O => n
-    | S n', S m' => S (max n' m')
-  end.
-
-(** * Inductive characterization of [max] *)
-
-Lemma max_case_strong : forall n m (P:nat -> Type),
-  (m<=n -> P n) -> (n<=m -> P m) -> P (max n m).
-Proof.
-  induction n; destruct m; simpl in *; auto with arith.
-  intros P H1 H2; apply IHn; intro; [apply H1|apply H2]; auto with arith.
-Qed.
-
-(** Propositional characterization of [max] *)
-
-Lemma max_spec : forall n m, m <= n /\ max n m = n \/ n <= m /\ max n m = m.
-Proof.
-  intros n m; apply max_case_strong; auto.
-Qed.
-
-(** * [max n m] is equal to [n] or [m] *)
-
-Lemma max_dec : forall n m, {max n m = n} + {max n m = m}.
-Proof.
-  induction n; destruct m; simpl; auto.
-  destruct (IHn m) as [-> | ->]; auto.
-Defined.
-
-(** [max n m] is equal to [n] or [m], alternative formulation *)
-
-Lemma max_case : forall n m (P:nat -> Type), P n -> P m -> P (max n m).
-Proof.
-  intros n m; destruct (max_dec n m) as [-> | ->]; auto.
-Defined.
-
-(** * Compatibility properties of [max] *)
-
-Lemma succ_max_distr : forall n m, S (max n m) = max (S n) (S m).
-Proof.
-  auto.
-Qed.
-
-Lemma plus_max_distr_l : forall n m p, max (p + n) (p + m) = p + max n m.
-Proof.
-  induction p; simpl; auto.
-Qed.
-
-Lemma plus_max_distr_r : forall n m p, max (n + p) (m + p) = max n m + p.
-Proof.
-  intros n m p; repeat rewrite (plus_comm _ p).
-  apply plus_max_distr_l.
-Qed.
-
-(** * Semi-lattice algebraic properties of [max] *)
-
-Lemma max_idempotent : forall n, max n n = n.
-Proof.
-  intros; apply max_case; auto.
-Qed.
-
-Lemma max_assoc : forall m n p : nat, max m (max n p) = max (max m n) p.
-Proof.
-  induction m; destruct n; destruct p; trivial.
-  simpl; auto.
-Qed.
-
-Lemma max_comm : forall n m, max n m = max m n.
-Proof.
-  induction n; destruct m; simpl; auto.
-Qed.
-
-(** * Least-upper bound properties of [max] *)
-
-Lemma max_l : forall n m, m <= n -> max n m = n.
-Proof.
-  induction n; destruct m; simpl; auto with arith.
-Qed.
-
-Lemma max_r : forall n m, n <= m -> max n m = m.
-Proof.
-  induction n; destruct m; simpl; auto with arith.
-Qed.
-
-Lemma le_max_l : forall n m, n <= max n m.
-Proof.
-  induction n; simpl; auto with arith.
-  destruct m; simpl; auto with arith.
-Qed.
-
-Lemma le_max_r : forall n m, m <= max n m.
-Proof.
-  induction n; simpl; auto with arith.
-  induction m; simpl; auto with arith.
-Qed.
-Hint Resolve max_r max_l le_max_l le_max_r: arith v62.
-
-Lemma max_lub_l : forall n m p, max n m <= p -> n <= p.
-Proof.
-intros n m p; eapply le_trans. apply le_max_l.
-Qed.
-
-Lemma max_lub_r : forall n m p, max n m <= p -> m <= p.
-Proof.
-intros n m p; eapply le_trans. apply le_max_r.
-Qed.
-
-Lemma max_lub : forall n m p, n <= p -> m <= p -> max n m <= p.
-Proof.
-  intros n m p; apply max_case; auto.
-Qed.
+Notation max := MinMax.max (only parsing).
+
+Definition max_0_l := max_0_l.
+Definition max_0_r := max_0_r.
+Definition succ_max_distr := succ_max_distr.
+Definition plus_max_distr_l := plus_max_distr_l.
+Definition plus_max_distr_r := plus_max_distr_r.
+Definition max_case_strong := max_case_strong.
+Definition max_spec := max_spec.
+Definition max_dec := max_dec.
+Definition max_case := max_case.
+Definition max_idempotent := max_id.
+Definition max_assoc := max_assoc.
+Definition max_comm := max_comm.
+Definition max_l := max_l.
+Definition max_r := max_r.
+Definition le_max_l := le_max_l.
+Definition le_max_r := le_max_r.
+Definition max_lub_l := max_lub_l.
+Definition max_lub_r := max_lub_r.
+Definition max_lub := max_lub.
 
 (* begin hide *)
 (* Compatibility *)