Rework of GenericMinMax: new axiomatic, split logical/decidable parts, Leibniz part

 Moreover, instantiation like MinMax are now made without redefining
 generic properties (easier maintenance). We start using inner modules
 for qualifying (e.g. Z.max_comm).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12638 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 305 insertions, 151 deletions

diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v
index f5ff27888..f45e43b44 100644
--- a/theories/Structures/GenericMinMax.v
+++ b/theories/Structures/GenericMinMax.v
@@ -6,28 +6,25 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-Require Import OrderedType2 OrderedType2Facts Setoid Morphisms Basics.
+Require Import OrderTac OrderedType2 OrderedType2Facts Setoid Morphisms Basics.
 
-(** * A Generic construction of min and max based on OrderedType *)
+(** * A Generic construction of min and max *)
 
 (** ** First, an interface for types with [max] and/or [min] *)
 
-Module Type HasMax (Import O:OrderedTypeFull).
+Module Type HasMax (Import E:EqLe').
  Parameter Inline max : t -> t -> t.
- Parameter max_spec : forall x y,
-   (lt x y /\ eq (max x y) y)  \/  (le y x /\ eq (max x y) x).
+ Parameter max_l : forall x y, y<=x -> max x y == x.
+ Parameter max_r : forall x y, x<=y -> max x y == y.
 End HasMax.
 
-Module Type HasMin (Import O:OrderedTypeFull).
+Module Type HasMin (Import E:EqLe').
  Parameter Inline min : t -> t -> t.
- Parameter min_spec : forall x y,
-   (lt x y /\ eq (min x y) x)  \/  (le y x /\ eq (min x y) y).
+ Parameter min_l : forall x y, x<=y -> min x y == x.
+ Parameter min_r : forall x y, y<=x -> min x y == y.
 End HasMin.
 
-Module Type HasMinMax (Import O:OrderedTypeFull).
- Include Type HasMax O.
- Include Type HasMin O.
-End HasMinMax.
+Module Type HasMinMax (E:EqLe) := HasMax E <+ HasMin E.
 
 
 (** ** Any [OrderedTypeFull] can be equipped by [max] and [min]
@@ -38,23 +35,42 @@ Definition gmax {A} (cmp : A->A->comparison) x y :=
 Definition gmin {A} (cmp : A->A->comparison) x y :=
  match cmp x y with Gt => y | _ => x end.
 
-Module GenericMinMax (Import O:OrderedTypeFull) <: HasMinMax O.
+Module GenericMinMax (Import O:OrderedTypeFull') <: HasMinMax O.
 
  Definition max := gmax O.compare.
  Definition min := gmin O.compare.
 
- Lemma max_spec : forall x y,
-   (lt x y /\ eq (max x y) y)  \/  (le y x /\ eq (max x y) x).
+ Lemma ge_not_lt : forall x y, y<=x -> x<y -> False.
  Proof.
-  intros. rewrite le_lteq. unfold max, gmax.
-  destruct (compare_spec x y); auto with relations.
+ intros x y H H'.
+ apply (StrictOrder_Irreflexive x).
+ rewrite le_lteq in *; destruct H as [H|H].
+ transitivity y; auto.
+ rewrite H in H'; auto.
  Qed.
 
- Lemma min_spec : forall x y,
-   (lt x y /\ eq (min x y) x)  \/  (le y x /\ eq (min x y) y).
+ Lemma max_l : forall x y, y<=x -> max x y == x.
  Proof.
-  intros. rewrite le_lteq. unfold min, gmin.
-  destruct (compare_spec x y); auto with relations.
+ intros. unfold max, gmax. destruct (compare_spec x y); auto with relations.
+ elim (ge_not_lt x y); auto.
+ Qed.
+
+ Lemma max_r : forall x y, x<=y -> max x y == y.
+ Proof.
+ intros. unfold max, gmax. destruct (compare_spec x y); auto with relations.
+ elim (ge_not_lt y x); auto.
+ Qed.
+
+ Lemma min_l : forall x y, x<=y -> min x y == x.
+ Proof.
+ intros. unfold min, gmin. destruct (compare_spec x y); auto with relations.
+ elim (ge_not_lt y x); auto.
+ Qed.
+
+ Lemma min_r : forall x y, y<=x -> min x y == y.
+ Proof.
+ intros. unfold min, gmin. destruct (compare_spec x y); auto with relations.
+ elim (ge_not_lt x y); auto.
  Qed.
 
 End GenericMinMax.
@@ -62,26 +78,21 @@ End GenericMinMax.
 
 (** ** Consequences of the minimalist interface: facts about [max]. *)
 
-Module MaxProperties (Import O:OrderedTypeFull)(Import M:HasMax O).
- Module Import OF := OrderedTypeFullFacts O.
- Infix "<" := lt.
- Infix "==" := eq (at level 70).
- Infix "<=" := le.
-
-Instance max_compat : Proper (eq==>eq==>eq) max.
-Proof.
-intros x x' Hx y y' Hy.
-assert (H1 := max_spec x y). assert (H2 := max_spec x' y').
-set (m := max x y) in *; set (m' := max x' y') in *; clearbody m m'.
-rewrite <- Hx, <- Hy in *.
-destruct (compare_spec x y); intuition; order.
-Qed.
+Module MaxLogicalProperties (Import O:TotalOrder')(Import M:HasMax O).
+ Module Import T := MakeOrderTac O.
 
-(** An alias to the [max_spec] of the interface. *)
+(** An alternative caracterisation of [max], equivalent to
+    [max_l /\ max_r] *)
 
 Lemma max_spec : forall n m,
   (n < m /\ max n m == m)  \/ (m <= n /\ max n m == n).
-Proof. exact max_spec. Qed.
+Proof.
+ intros n m.
+ destruct (lt_total n m); [left|right].
+ split; auto. apply max_r. rewrite le_lteq; auto.
+ assert (m <= n) by (rewrite le_lteq; intuition).
+ split; auto. apply max_l; auto.
+Qed.
 
 (** A more symmetric version of [max_spec], based only on [le].
     Beware that left and right alternatives overlap. *)
@@ -92,13 +103,26 @@ Proof.
  intros. destruct (max_spec n m); [left|right]; intuition; order.
 Qed.
 
-(** Another function satisfying the same specification is equal to [max]. *)
+Instance : Proper (eq==>eq==>iff) le.
+Proof. repeat red. intuition order. Qed.
+
+Instance max_compat : Proper (eq==>eq==>eq) max.
+Proof.
+intros x x' Hx y y' Hy.
+assert (H1 := max_spec x y). assert (H2 := max_spec x' y').
+set (m := max x y) in *; set (m' := max x' y') in *; clearbody m m'.
+rewrite <- Hx, <- Hy in *.
+destruct (lt_total x y); intuition order.
+Qed.
+
+
+(** A function satisfying the same specification is equal to [max]. *)
 
 Lemma max_unicity : forall n m p,
  ((n < m /\ p == m)  \/ (m <= n /\ p == n)) ->  p == max n m.
 Proof.
  intros. assert (Hm := max_spec n m).
- destruct (compare_spec n m); intuition; order.
+ destruct (lt_total n m); intuition; order.
 Qed.
 
 Lemma max_unicity_ext : forall f,
@@ -108,45 +132,16 @@ Proof.
  intros. apply max_unicity; auto.
 Qed.
 
-(** Induction principles for [max]. *)
-
-Lemma max_case_strong : forall n m (P:t -> Type),
-  (forall x y, x==y -> P x -> P y) ->
-  (m<=n -> P n) -> (n<=m -> P m) -> P (max n m).
-Proof.
-intros n m P Compat Hl Hr.
-assert (H:=compare_spec n m). assert (H':=max_spec n m).
-destruct (compare n m).
-apply (Compat m), Hr; inversion_clear H; intuition; order.
-apply (Compat m), Hr; inversion_clear H; intuition; order.
-apply (Compat n), Hl; inversion_clear H; intuition; order.
-Qed.
-
-Lemma max_case : forall n m (P:t -> Type),
-  (forall x y, x == y -> P x -> P y) ->
-  P n -> P m -> P (max n m).
-Proof.
- intros. apply max_case_strong; auto.
-Defined.
-
-(** [max] returns one of its arguments. *)
-
-Lemma max_dec : forall n m, {max n m == n} + {max n m == m}.
-Proof.
- intros n m. apply max_case; auto with relations.
- intros x y H [E|E]; [left|right]; order.
-Defined.
-
 (** [max] commutes with monotone functions. *)
 
-Lemma max_monotone: forall f,
+Lemma max_mono: forall f,
  (Proper (eq ==> eq) f) ->
  (Proper (le ==> le) f) ->
  forall x y, max (f x) (f y) == f (max x y).
 Proof.
  intros f Eqf Lef x y.
- destruct (M.max_spec x y) as [(H,E)|(H,E)]; rewrite E;
-  destruct (M.max_spec (f x) (f y)) as [(H',E')|(H',E')]; auto.
+ destruct (max_spec x y) as [(H,E)|(H,E)]; rewrite E;
+  destruct (max_spec (f x) (f y)) as [(H',E')|(H',E')]; auto.
  assert (f x <= f y) by (apply Lef; order). order.
  assert (f y <= f x) by (apply Lef; order). order.
 Qed.
@@ -155,101 +150,106 @@ Qed.
 
 Lemma max_id : forall n, max n n == n.
 Proof.
- intros. destruct (M.max_spec n n); intuition.
+ intros. destruct (max_spec n n); intuition.
 Qed.
 
+Notation max_idempotent := max_id (only parsing).
+
 Lemma max_assoc : forall m n p, max m (max n p) == max (max m n) p.
 Proof.
  intros.
- destruct (M.max_spec n p) as [(H,Eq)|(H,Eq)]; rewrite Eq.
- destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'.
+ destruct (max_spec n p) as [(H,Eq)|(H,Eq)]; rewrite Eq.
+ destruct (max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'.
  destruct (max_spec m p); intuition; order. order.
- destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'. order.
+ destruct (max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'. order.
  destruct (max_spec m p); intuition; order.
 Qed.
 
 Lemma max_comm : forall n m, max n m == max m n.
 Proof.
  intros.
- destruct (M.max_spec n m) as [(H,Eq)|(H,Eq)]; rewrite Eq.
- destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; order.
- destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; order.
+ destruct (max_spec n m) as [(H,Eq)|(H,Eq)]; rewrite Eq.
+ destruct (max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; order.
+ destruct (max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; order.
 Qed.
 
 (** *** Least-upper bound properties of [max] *)
 
-Lemma max_l : forall n m, m <= n -> max n m == n.
+Definition max_l := max_l.
+Definition max_r := max_r.
+
+Lemma le_max_l : forall n m, n <= max n m.
 Proof.
- intros. destruct (M.max_spec n m); intuition; order.
+ intros; destruct (max_spec n m); intuition; order.
 Qed.
 
-Lemma max_r : forall n m, n <= m -> max n m == m.
+Lemma le_max_r : forall n m, m <= max n m.
 Proof.
- intros. destruct (M.max_spec n m); intuition; order.
+ intros; destruct (max_spec n m); intuition; order.
 Qed.
 
-Lemma le_max_l : forall n m, n <= max n m.
+Lemma max_l_iff : forall n m, max n m == n <-> m <= n.
 Proof.
- intros; destruct (M.max_spec n m); intuition; order.
+ split. intro H; rewrite <- H. apply le_max_r. apply max_l.
 Qed.
 
-Lemma le_max_r : forall n m, m <= max n m.
+Lemma max_r_iff : forall n m, max n m == m <-> n <= m.
 Proof.
- intros; destruct (M.max_spec n m); intuition; order.
+ split. intro H; rewrite <- H. apply le_max_l. apply max_r.
 Qed.
 
 Lemma max_le : forall n m p, p <= max n m -> p <= n \/ p <= m.
 Proof.
- intros n m p H; destruct (M.max_spec n m);
+ intros n m p H; destruct (max_spec n m);
   [right|left]; intuition; order.
 Qed.
 
 Lemma max_le_iff : forall n m p, p <= max n m <-> p <= n \/ p <= m.
 Proof.
  intros. split. apply max_le.
- destruct (M.max_spec n m); intuition; order.
+ destruct (max_spec n m); intuition; order.
 Qed.
 
 Lemma max_lt_iff : forall n m p, p < max n m <-> p < n \/ p < m.
 Proof.
- intros. destruct (M.max_spec n m); intuition;
+ intros. destruct (max_spec n m); intuition;
   order || (right; order) || (left; order).
 Qed.
 
 Lemma max_lub_l : forall n m p, max n m <= p -> n <= p.
 Proof.
- intros; destruct (M.max_spec n m); intuition; order.
+ intros; destruct (max_spec n m); intuition; order.
 Qed.
 
 Lemma max_lub_r : forall n m p, max n m <= p -> m <= p.
 Proof.
- intros; destruct (M.max_spec n m); intuition; order.
+ intros; destruct (max_spec n m); intuition; order.
 Qed.
 
 Lemma max_lub : forall n m p, n <= p -> m <= p -> max n m <= p.
 Proof.
- intros; destruct (M.max_spec n m); intuition; order.
+ intros; destruct (max_spec n m); intuition; order.
 Qed.
 
 Lemma max_lub_iff : forall n m p, max n m <= p <-> n <= p /\ m <= p.
 Proof.
- intros; destruct (M.max_spec n m); intuition; order.
+ intros; destruct (max_spec n m); intuition; order.
 Qed.
 
 Lemma max_lub_lt : forall n m p, n < p -> m < p -> max n m < p.
 Proof.
- intros; destruct (M.max_spec n m); intuition; order.
+ intros; destruct (max_spec n m); intuition; order.
 Qed.
 
 Lemma max_lub_lt_iff : forall n m p, max n m < p <-> n < p /\ m < p.
 Proof.
- intros; destruct (M.max_spec n m); intuition; order.
+ intros; destruct (max_spec n m); intuition; order.
 Qed.
 
 Lemma max_le_compat_l : forall n m p, n <= m -> max p n <= max p m.
 Proof.
  intros.
- destruct (M.max_spec p n) as [(LT,E)|(LE,E)]; rewrite E.
+ destruct (max_spec p n) as [(LT,E)|(LE,E)]; rewrite E.
  assert (LE' := le_max_r p m). order.
  apply le_max_l.
 Qed.
@@ -269,57 +269,44 @@ Proof.
  order.
 Qed.
 
-End MaxProperties.
+End MaxLogicalProperties.
 
 
 (** ** Properties concernant [min], then both [min] and [max].
 
-   To avoid duplication of code, we exploit that [min] can be
+   To avoid too much code duplication, we exploit that [min] can be
    seen as a [max] of the reversed order.
 *)
 
-Module MinMaxProperties (Import O:OrderedTypeFull)(Import M:HasMinMax O).
- Include MaxProperties O M.
+Module MinMaxLogicalProperties (Import O:TotalOrder')(Import M:HasMinMax O).
+ Include MaxLogicalProperties O M.
+ Import T.
 
- Module ORev := OrderedTypeRev O.
+ Module ORev := TotalOrderRev O.
  Module MRev <: HasMax ORev.
   Definition max x y := M.min y x.
-  Definition max_spec x y := M.min_spec y x.
+  Definition max_l x y := M.min_r y x.
+  Definition max_r x y := M.min_l y x.
  End MRev.
- Module MPRev := MaxProperties ORev MRev.
+ Module MPRev := MaxLogicalProperties ORev MRev.
 
 Instance min_compat : Proper (eq==>eq==>eq) min.
 Proof. intros x x' Hx y y' Hy. apply MPRev.max_compat; assumption. Qed.
 
 Lemma min_spec : forall n m,
  (n < m /\ min n m == n) \/ (m <= n /\ min n m == m).
-Proof. exact min_spec. Qed.
+Proof. intros. exact (MPRev.max_spec m n). Qed.
 
 Lemma min_spec_le : forall n m,
  (n <= m /\ min n m == n) \/ (m <= n /\ min n m == m).
 Proof. intros. exact (MPRev.max_spec_le m n). Qed.
 
-Lemma min_case_strong : forall n m (P:O.t -> Type),
- (forall x y, x == y -> P x -> P y) ->
- (n<=m -> P n) -> (m<=n -> P m) -> P (min n m).
-Proof. intros. apply (MPRev.max_case_strong m n P); auto. Qed.
-
-Lemma min_case : forall n m (P:O.t -> Type),
-  (forall x y, x == y -> P x -> P y) ->
-  P n -> P m -> P (min n m).
-Proof. intros. apply min_case_strong; auto. Defined.
-
-Lemma min_dec : forall n m, {min n m == n} + {min n m == m}.
-Proof.
- intros. destruct (MPRev.max_dec m n); [right|left]; assumption.
-Defined.
-
-Lemma min_monotone: forall f,
+Lemma min_mono: forall f,
  (Proper (eq ==> eq) f) ->
  (Proper (le ==> le) f) ->
  forall x y, min (f x) (f y) == f (min x y).
 Proof.
- intros. apply MPRev.max_monotone; auto. compute in *; eauto.
+ intros. apply MPRev.max_mono; auto. compute in *; eauto.
 Qed.
 
 Lemma min_unicity : forall n m p,
@@ -334,17 +321,16 @@ Proof. intros f H n m. apply MPRev.max_unicity, H; auto. Qed.
 Lemma min_id : forall n, min n n == n.
 Proof. intros. exact (MPRev.max_id n). Qed.
 
+Notation min_idempotent := min_id (only parsing).
+
 Lemma min_assoc : forall m n p, min m (min n p) == min (min m n) p.
 Proof. intros. symmetry; apply MPRev.max_assoc. Qed.
 
 Lemma min_comm : forall n m, min n m == min m n.
 Proof. intros. exact (MPRev.max_comm m n). Qed.
 
-Lemma min_l : forall n m, n <= m -> min n m == n.
-Proof. intros n m. exact (MPRev.max_r m n). Qed.
-
-Lemma min_r : forall n m, m <= n -> min n m == m.
-Proof. intros n m. exact (MPRev.max_l m n). Qed.
+Definition min_l := min_l.
+Definition min_r := min_r.
 
 Lemma le_min_r : forall n m, min n m <= m.
 Proof. intros. exact (MPRev.le_max_l m n). Qed.
@@ -352,6 +338,12 @@ Proof. intros. exact (MPRev.le_max_l m n). Qed.
 Lemma le_min_l : forall n m, min n m <= n.
 Proof. intros. exact (MPRev.le_max_r m n). Qed.
 
+Lemma min_l_iff : forall n m, min n m == n <-> n <= m.
+Proof. intros n m. exact (MPRev.max_r_iff m n). Qed.
+
+Lemma min_r_iff : forall n m, min n m == m <-> m <= n.
+Proof. intros n m. exact (MPRev.max_l_iff m n). Qed.
+
 Lemma min_le : forall n m p, min n m <= p -> n <= p \/ m <= p.
 Proof. intros n m p H. destruct (MPRev.max_le _ _ _ H); auto. Qed.
 
@@ -395,17 +387,17 @@ Proof. intros. apply MPRev.max_le_compat; auto. Qed.
 Lemma min_max_absorption : forall n m, max n (min n m) == n.
 Proof.
  intros.
- destruct (M.min_spec n m) as [(C,E)|(C,E)]; rewrite E.
- apply max_l. OF.order.
- destruct (M.max_spec n m); intuition; OF.order.
+ destruct (min_spec n m) as [(C,E)|(C,E)]; rewrite E.
+ apply max_l. order.
+ destruct (max_spec n m); intuition; order.
 Qed.
 
 Lemma max_min_absorption : forall n m, min n (max n m) == n.
 Proof.
  intros.
- destruct (M.max_spec n m) as [(C,E)|(C,E)]; rewrite E.
- destruct (M.min_spec n m) as [(C',E')|(C',E')]; auto. OF.order.
- apply min_l; auto. OF.order.
+ destruct (max_spec n m) as [(C,E)|(C,E)]; rewrite E.
+ destruct (min_spec n m) as [(C',E')|(C',E')]; auto. order.
+ apply min_l; auto. order.
 Qed.
 
 (** Distributivity *)
@@ -413,7 +405,7 @@ Qed.
 Lemma max_min_distr : forall n m p,
  max n (min m p) == min (max n m) (max n p).
 Proof.
- intros. symmetry. apply min_monotone.
+ intros. symmetry. apply min_mono.
  eauto with *.
  repeat red; intros. apply max_le_compat_l; auto.
 Qed.
@@ -421,7 +413,7 @@ Qed.
 Lemma min_max_distr : forall n m p,
  min n (max m p) == max (min n m) (min n p).
 Proof.
- intros. symmetry. apply max_monotone.
+ intros. symmetry. apply max_mono.
  eauto with *.
  repeat red; intros. apply min_le_compat_l; auto.
 Qed.
@@ -432,20 +424,20 @@ Lemma max_min_modular : forall n m p,
  max n (min m (max n p)) == min (max n m) (max n p).
 Proof.
  intros. rewrite <- max_min_distr.
- destruct (max_spec n p) as [(C,E)|(C,E)]; rewrite E. reflexivity.
+ destruct (max_spec n p) as [(C,E)|(C,E)]; rewrite E; auto with *.
  destruct (min_spec m n) as [(C',E')|(C',E')]; rewrite E'.
- rewrite 2 max_l; try OF.order. rewrite min_le_iff; auto.
- rewrite 2 max_l; try OF.order. rewrite min_le_iff; auto.
+ rewrite 2 max_l; try order. rewrite min_le_iff; auto.
+ rewrite 2 max_l; try order. rewrite min_le_iff; auto.
 Qed.
 
 Lemma min_max_modular : forall n m p,
  min n (max m (min n p)) == max (min n m) (min n p).
 Proof.
  intros. rewrite <- min_max_distr.
- destruct (min_spec n p) as [(C,E)|(C,E)]; rewrite E.
+ destruct (min_spec n p) as [(C,E)|(C,E)]; rewrite E; auto with *.
  destruct (max_spec m n) as [(C',E')|(C',E')]; rewrite E'.
- rewrite 2 min_l; try OF.order. rewrite max_le_iff; right; OF.order.
- rewrite 2 min_l; try OF.order. rewrite max_le_iff; auto. reflexivity.
+ rewrite 2 min_l; try order. rewrite max_le_iff; right; order.
+ rewrite 2 min_l; try order. rewrite max_le_iff; auto.
 Qed.
 
 (** Disassociativity *)
@@ -459,34 +451,196 @@ Qed.
 
 (** Anti-monotonicity swaps the role of [min] and [max] *)
 
-Lemma max_min_antimonotone : forall f,
+Lemma max_min_antimono : forall f,
  Proper (eq==>eq) f ->
  Proper (le==>inverse le) f ->
  forall x y, max (f x) (f y) == f (min x y).
 Proof.
  intros f Eqf Lef x y.
- destruct (M.min_spec x y) as [(H,E)|(H,E)]; rewrite E;
-  destruct (M.max_spec (f x) (f y)) as [(H',E')|(H',E')]; auto.
- assert (f y <= f x) by (apply Lef; OF.order). OF.order.
- assert (f x <= f y) by (apply Lef; OF.order). OF.order.
+ destruct (min_spec x y) as [(H,E)|(H,E)]; rewrite E;
+  destruct (max_spec (f x) (f y)) as [(H',E')|(H',E')]; auto.
+ assert (f y <= f x) by (apply Lef; order). order.
+ assert (f x <= f y) by (apply Lef; order). order.
 Qed.
 
-
-Lemma min_max_antimonotone : forall f,
+Lemma min_max_antimono : forall f,
  Proper (eq==>eq) f ->
  Proper (le==>inverse le) f ->
  forall x y, min (f x) (f y) == f (max x y).
 Proof.
  intros f Eqf Lef x y.
- destruct (M.max_spec x y) as [(H,E)|(H,E)]; rewrite E;
-  destruct (M.min_spec (f x) (f y)) as [(H',E')|(H',E')]; auto.
- assert (f y <= f x) by (apply Lef; OF.order). OF.order.
- assert (f x <= f y) by (apply Lef; OF.order). OF.order.
+ destruct (max_spec x y) as [(H,E)|(H,E)]; rewrite E;
+  destruct (min_spec (f x) (f y)) as [(H',E')|(H',E')]; auto.
+ assert (f y <= f x) by (apply Lef; order). order.
+ assert (f x <= f y) by (apply Lef; order). order.
 Qed.
 
+End MinMaxLogicalProperties.
+
+
+(** ** Properties requiring a decidable order *)
+
+Module MinMaxDecProperties (Import O:OrderedTypeFull')(Import M:HasMinMax O).
+
+(** Induction principles for [max]. *)
+
+Lemma max_case_strong : forall n m (P:t -> Type),
+  (forall x y, x==y -> P x -> P y) ->
+  (m<=n -> P n) -> (n<=m -> P m) -> P (max n m).
+Proof.
+intros n m P Compat Hl Hr.
+assert (H:=compare_spec n m). destruct (compare n m).
+assert (n<=m) by (inversion H; rewrite le_lteq; auto).
+apply (Compat m), Hr; auto. symmetry; apply max_r; auto.
+assert (n<=m) by (inversion H; rewrite le_lteq; auto).
+apply (Compat m), Hr; auto. symmetry; apply max_r; auto.
+assert (m<=n) by (inversion H; rewrite le_lteq; auto).
+apply (Compat n), Hl; auto. symmetry; apply max_l; auto.
+Defined.
+
+Lemma max_case : forall n m (P:t -> Type),
+  (forall x y, x == y -> P x -> P y) ->
+  P n -> P m -> P (max n m).
+Proof. intros. apply max_case_strong; auto. Defined.
+
+(** [max] returns one of its arguments. *)
+
+Lemma max_dec : forall n m, {max n m == n} + {max n m == m}.
+Proof.
+ intros n m. apply max_case; auto with relations.
+ intros x y H [E|E]; [left|right]; rewrite <-H; auto.
+Defined.
+
+(** Idem for [min] *)
+
+Lemma min_case_strong : forall n m (P:O.t -> Type),
+ (forall x y, x == y -> P x -> P y) ->
+ (n<=m -> P n) -> (m<=n -> P m) -> P (min n m).
+Proof.
+intros n m P Compat Hl Hr.
+assert (H:=compare_spec n m). destruct (compare n m).
+assert (n<=m) by (inversion H; rewrite le_lteq; auto).
+apply (Compat n), Hl; auto. symmetry; apply min_l; auto.
+assert (n<=m) by (inversion H; rewrite le_lteq; auto).
+apply (Compat n), Hl; auto. symmetry; apply min_l; auto.
+assert (m<=n) by (inversion H; rewrite le_lteq; auto).
+apply (Compat m), Hr; auto. symmetry; apply min_r; auto.
+Defined.
+
+Lemma min_case : forall n m (P:O.t -> Type),
+  (forall x y, x == y -> P x -> P y) ->
+  P n -> P m -> P (min n m).
+Proof. intros. apply min_case_strong; auto. Defined.
+
+Lemma min_dec : forall n m, {min n m == n} + {min n m == m}.
+Proof.
+ intros. apply min_case; auto with relations.
+ intros x y H [E|E]; [left|right]; rewrite <- E; auto with relations.
+Defined.
+
+End MinMaxDecProperties.
+
+Module MinMaxProperties (Import O:OrderedTypeFull')(Import M:HasMinMax O).
+ Module OT := OTF_to_TotalOrder O.
+ Include MinMaxLogicalProperties OT M.
+ Include MinMaxDecProperties O M.
+ Notation max_monotone := max_mono.
+ Notation min_monotone := min_mono.
+ Notation max_min_antimonotone := max_min_antimono.
+ Notation min_max_antimonotone := min_max_antimono.
 End MinMaxProperties.
 
 
+(** ** When the equality is Leibniz, we can skip a few [Proper] precondition. *)
+
+Module UsualMinMaxLogicalProperties
+ (Import O:UsualTotalOrder')(Import M:HasMinMax O).
+
+ Include MinMaxLogicalProperties O M.
+
+ 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_mono; auto. congruence. Qed.
+
+ 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_mono; auto. congruence. Qed.
+
+ Lemma min_max_antimonotone : forall f, Proper (le ==> inverse le) f ->
+  forall x y, min (f x) (f y) = f (max x y).
+ Proof. intros; apply min_max_antimono; auto. congruence. Qed.
+
+ Lemma max_min_antimonotone : forall f, Proper (le ==> inverse le) f ->
+  forall x y, max (f x) (f y) = f (min x y).
+ Proof. intros; apply max_min_antimono; auto. congruence. Qed.
+
+End UsualMinMaxLogicalProperties.
+
+
+Module UsualMinMaxDecProperties
+ (Import O:UsualOrderedTypeFull')(Import M:HasMinMax O).
+
+ Module P := MinMaxDecProperties O M.
+
+ Lemma max_case_strong : forall n m (P:t -> Type),
+  (m<=n -> P n) -> (n<=m -> P m) -> P (max n m).
+ Proof. intros; apply P.max_case_strong; auto. congruence. Defined.
+
+ Lemma max_case : forall n m (P:t -> Type),
+  P n -> P m -> P (max n m).
+ Proof. intros; apply max_case_strong; auto. Defined.
+
+ Lemma max_dec : forall n m, {max n m = n} + {max n m = m}.
+ Proof. exact P.max_dec. Defined.
+
+ Lemma min_case_strong : forall n m (P:O.t -> Type),
+  (m<=n -> P m) -> (n<=m -> P n) -> P (min n m).
+ Proof. intros; apply P.min_case_strong; auto. congruence. Defined.
+
+ Lemma min_case : forall n m (P:O.t -> Type),
+  P n -> P m -> P (min n m).
+ Proof. intros. apply min_case_strong; auto. Defined.
+
+ Lemma min_dec : forall n m, {min n m = n} + {min n m = m}.
+ Proof. exact P.min_dec. Defined.
+
+End UsualMinMaxDecProperties.
+
+Module UsualMinMaxProperties
+ (Import O:UsualOrderedTypeFull')(Import M:HasMinMax O).
+ Module OT := OTF_to_TotalOrder O.
+ Include UsualMinMaxLogicalProperties OT M.
+ Include UsualMinMaxDecProperties O M.
+End UsualMinMaxProperties.
+
+
+(** From [TotalOrder] and [HasMax] and [HasEqDec], we can prove
+    that the order is decidable and build an [OrderedTypeFull]. *)
+
+Module TOMaxEqDec_to_Compare
+ (Import O:TotalOrder')(Import M:HasMax O)(Import E:HasEqDec O) <: HasCompare O.
+
+ Definition compare x y :=
+  if eq_dec x y then Eq
+  else if eq_dec (M.max x y) y then Lt else Gt.
+
+ Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
+ Proof.
+ intros; unfold compare; repeat destruct eq_dec; auto; constructor.
+ destruct (lt_total x y); auto.
+ absurd (x==y); auto. transitivity (max x y); auto.
+ symmetry. apply max_l. rewrite le_lteq; intuition.
+ destruct (lt_total y x); auto.
+ absurd (max x y == y); auto. apply max_r; rewrite le_lteq; intuition.
+ Qed.
+
+End TOMaxEqDec_to_Compare.
+
+Module TOMaxEqDec_to_OTF (O:TotalOrder)(M:HasMax O)(E:HasEqDec O)
+ <: OrderedTypeFull
+ := O <+ E <+ TOMaxEqDec_to_Compare O M E.
+
+
 
 (** TODO: Some Remaining questions...