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

5 files changed, 334 insertions, 221 deletions

diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v
index 6f8a5f127..0f2595b26 100644
--- a/theories/Arith/Compare.v
+++ b/theories/Arith/Compare.v
@@ -52,4 +52,4 @@ Qed.
 
 Require Export Wf_nat.
 
-Require Export Min.
+Require Export Min Max.
\ No newline at end of file
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 *)
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
diff --git a/theories/Arith/MinMax.v b/theories/Arith/MinMax.v
new file mode 100644
index 000000000..784e10455
--- /dev/null
+++ b/theories/Arith/MinMax.v
@@ -0,0 +1,211 @@
+(************************************************************************)
+(*  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 OrderedType2 NatOrderedType GenericMinMax.
+
+(** * Maximum and Minimum 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.
+
+Fixpoint min n m : nat :=
+  match n, m with
+    | O, _ => 0
+    | S n', O => 0
+    | S n', S m' => S (min n' m')
+  end.
+
+(** These functions implement indeed a maximum and a minimum *)
+
+Lemma max_spec : forall x y,
+  (x<y /\ max x y = y)  \/  (y<=x /\ max x y = x).
+Proof.
+ induction x; destruct y; simpl; auto with arith.
+ destruct (IHx y); intuition.
+Qed.
+
+Lemma min_spec : forall x y,
+  (x<y /\ min x y = x)  \/  (y<=x /\ min x y = y).
+Proof.
+ induction x; destruct y; simpl; auto with arith.
+ destruct (IHx y); intuition.
+Qed.
+
+Module NatHasMinMax <: HasMinMax Nat_as_OT.
+ Definition max := max.
+ Definition min := min.
+ Definition max_spec := max_spec.
+ Definition min_spec := min_spec.
+End NatHasMinMax.
+
+(** We obtain hence all the generic properties of max and min. *)
+
+Module Import NatMinMaxProps := MinMaxProperties Nat_as_OT NatHasMinMax.
+
+(** For some generic properties, we can have nicer statements here,
+    since underlying equality is Leibniz. *)
+
+Lemma max_case_strong : forall n m (P:nat -> Type),
+  (m<=n -> P n) -> (n<=m -> P m) -> P (max n m).
+Proof. intros; apply max_case_strong; auto. congruence. Defined.
+
+Lemma max_case : forall n m (P:nat -> Type),
+  P n -> P m -> P (max n m).
+Proof. intros. apply max_case_strong; auto. Defined.
+
+Lemma max_monotone: forall f,
+ (Proper (le ==> le) f) ->
+ forall x y, max (f x) (f y) = f (max x y).
+Proof. intros; apply max_monotone; auto. congruence. Qed.
+
+Lemma min_case_strong : forall n m (P:nat -> Type),
+  (m<=n -> P m) -> (n<=m -> P n) -> P (min n m).
+Proof. intros; apply min_case_strong; auto. congruence. Defined.
+
+Lemma min_case : forall n m (P:nat -> Type),
+  P n -> P m -> P (min n m).
+Proof. intros. apply min_case_strong; auto. Defined.
+
+Lemma min_monotone: forall f,
+ (Proper (le ==> le) f) ->
+ forall x y, min (f x) (f y) = f (min x y).
+Proof. intros; apply min_monotone; auto. congruence. Qed.
+
+Lemma max_min_antimonotone : forall f,
+ Proper (le==>ge) f ->
+ forall x y, max (f x) (f y) == f (min x y).
+Proof.
+ intros. apply max_min_antimonotone. congruence.
+ intros z z' Hz; red; unfold ge in *; auto.
+Qed.
+
+Lemma min_max_antimonotone : forall f,
+ Proper (le==>ge) f ->
+ forall x y, min (f x) (f y) == f (max x y).
+Proof.
+ intros. apply min_max_antimonotone. congruence.
+ intros z z' Hz; red; unfold ge in *; auto.
+Qed.
+
+(** For the other generic properties, we make aliases,
+   since otherwise SearchAbout misses some of them
+   (bad interaction with an Include).
+   See GenericMinMax (or SearchAbout) for the statements. *)
+
+Definition max_spec_le := max_spec_le.
+Definition max_dec := max_dec.
+Definition max_unicity := max_unicity.
+Definition max_unicity_ext := max_unicity_ext.
+Definition max_id := max_id.
+Notation max_idempotent := max_id (only parsing).
+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_le := max_le.
+Definition max_le_iff := max_le_iff.
+Definition max_lt_iff := max_lt_iff.
+Definition max_lub_l := max_lub_l.
+Definition max_lub_r := max_lub_r.
+Definition max_lub := max_lub.
+Definition max_lub_iff := max_lub_iff.
+Definition max_lub_lt := max_lub_lt.
+Definition max_lub_lt_iff := max_lub_lt_iff.
+Definition max_le_compat_l := max_le_compat_l.
+Definition max_le_compat_r := max_le_compat_r.
+Definition max_le_compat := max_le_compat.
+
+Definition min_spec_le := min_spec_le.
+Definition min_dec := min_dec.
+Definition min_unicity := min_unicity.
+Definition min_unicity_ext := min_unicity_ext.
+Definition min_id := min_id.
+Notation min_idempotent := min_id (only parsing).
+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_le := min_le.
+Definition min_le_iff := min_le_iff.
+Definition min_lt_iff := min_lt_iff.
+Definition min_glb_l := min_glb_l.
+Definition min_glb_r := min_glb_r.
+Definition min_glb := min_glb.
+Definition min_glb_iff := min_glb_iff.
+Definition min_glb_lt := min_glb_lt.
+Definition min_glb_lt_iff := min_glb_lt_iff.
+Definition min_le_compat_l := min_le_compat_l.
+Definition min_le_compat_r := min_le_compat_r.
+Definition min_le_compat := min_le_compat.
+
+Definition min_max_absorption := min_max_absorption.
+Definition max_min_absorption := max_min_absorption.
+Definition max_min_distr := max_min_distr.
+Definition min_max_distr := min_max_distr.
+Definition max_min_modular := max_min_modular.
+Definition min_max_modular := min_max_modular.
+Definition max_min_disassoc := max_min_disassoc.
+
+
+(** * Properties specific to the [nat] domain *)
+
+(** Simplifications *)
+
+Lemma max_0_l : forall n, max 0 n = n.
+Proof. reflexivity. Qed.
+
+Lemma max_0_r : forall n, max n 0 = n.
+Proof. destruct n; auto. Qed.
+
+Lemma min_0_l : forall n, min 0 n = 0.
+Proof. reflexivity. Qed.
+
+Lemma min_0_r : forall n, min n 0 = 0.
+Proof. destruct n; auto. Qed.
+
+(** Compatibilities (consequences of monotonicity) *)
+
+Lemma succ_max_distr : forall n m, S (max n m) = max (S n) (S m).
+Proof. auto. Qed.
+
+Lemma succ_min_distr : forall n m, S (min n m) = min (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.
+intros. apply max_monotone. repeat red; auto with arith.
+Qed.
+
+Lemma plus_max_distr_r : forall n m p, max (n + p) (m + p) = max n m + p.
+Proof.
+intros. apply max_monotone with (f:=fun x => x + p).
+repeat red; auto with arith.
+Qed.
+
+Lemma plus_min_distr_l : forall n m p, min (p + n) (p + m) = p + min n m.
+Proof.
+intros. apply min_monotone. repeat red; auto with arith.
+Qed.
+
+Lemma plus_min_distr_r : forall n m p, min (n + p) (m + p) = min n m + p.
+Proof.
+intros. apply min_monotone with (f:=fun x => x + p).
+repeat red; auto with arith.
+Qed.
+
+Hint Resolve
+ max_l max_r le_max_l le_max_r
+ min_l min_r le_min_l le_min_r : arith v62.
diff --git a/theories/Arith/NatOrderedType.v b/theories/Arith/NatOrderedType.v
new file mode 100644
index 000000000..c4e71632c
--- /dev/null
+++ b/theories/Arith/NatOrderedType.v
@@ -0,0 +1,69 @@
+(************************************************************************)
+(*  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 Peano_dec Compare_dec
+ DecidableType2 OrderedType2 OrderedType2Facts.
+
+
+(** * DecidableType structure for Peano numbers *)
+
+Module Nat_as_MiniDT <: MiniDecidableType.
+ Definition t := nat.
+ Definition eq_dec := eq_nat_dec.
+End Nat_as_MiniDT.
+
+Module Nat_as_DT <: UsualDecidableType := Make_UDT Nat_as_MiniDT.
+
+(** Note that [Nat_as_DT] can also be seen as a [DecidableType]
+    and a [DecidableTypeOrig]. *)
+
+
+
+(** * OrderedType structure for Peano numbers *)
+
+Module Nat_as_OT <: OrderedTypeFull.
+ Include Nat_as_DT.
+ Definition lt := lt.
+ Definition le := le.
+ Definition compare := nat_compare.
+
+ Instance lt_strorder : StrictOrder lt.
+ Proof. split; [ exact Lt.lt_irrefl | exact Lt.lt_trans ]. Qed.
+
+ Instance lt_compat : Proper (Logic.eq==>Logic.eq==>iff) lt.
+ Proof. repeat red; intros; subst; auto. Qed.
+
+ Lemma le_lteq : forall x y, x <= y <-> x < y \/ x=y.
+ Proof. intuition; subst; auto using Lt.le_lt_or_eq. Qed.
+
+ Lemma compare_spec : forall x y, Cmp eq lt x y (compare x y).
+ Proof.
+ intros; unfold compare.
+ destruct (nat_compare x y) as [ ]_eqn; constructor.
+ apply nat_compare_eq; auto.
+ apply nat_compare_Lt_lt; auto.
+ apply nat_compare_Gt_gt; auto.
+ Qed.
+
+End Nat_as_OT.
+
+(* Note that [Nat_as_OT] can also be seen as a [UsualOrderedType]
+   and a [OrderedType] (and also as a [DecidableType]). *)
+
+
+
+(** * An [order] tactic for Peano numbers *)
+
+Module NatOrder := OTF_to_OrderTac Nat_as_OT.
+Ltac nat_order :=
+ change (@eq nat) with NatOrder.OrderElts.eq in *;
+ NatOrder.order.
+
+(** Note that [nat_order] is domain-agnostic: it will not prove
+    [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *)
+