Make an appropriate use of the order library everywhere (#278, #280, #282, #283, #285, #286, #288, #296, #330, #334, and #341)

ssrnum related changes:
- Redefine the intermediate structure between `idomainType` and `numDomainType`,
  which is `normedDomainType` (normed integral domain without an order).
- Generalize (by using `normedDomainType` or the order structures), relocate
  (to order.v), and rename ssrnum related definitions and lemmas.
- Add a compatibility module `Num.mc_1_9` and export it to check compilation.
- Remove the use of the deprecated definitions and lemmas from entire theories.
- Implement factories mechanism to construct several ordered and num structures
  from fewer axioms.

order related changes:
- Reorganize the hierarchy of finite lattice structures. Finite lattices have
  top and bottom elements except for empty set. Therefore we removed finite
  lattice structures without top and bottom.
- Reorganize the theory modules in order.v:
  + `LTheory` (lattice and partial order, without complement and totality)
  + `CTheory` (`LTheory` + complement)
  + `Theory` (all)
- Give a unique head symbol for `Total.mixin_of`.
- Replace reverse and `^r` with converse and `^c` respectively.
- Fix packing and cloning functions and notations.
- Provide more ordered type instances:
  Products and lists can be ordered in two different ways: the lexicographical
  ordering and the pointwise ordering. Now their canonical instances are not
  exported to make the users choose them.
- Export `Order.*.Exports` modules by default.
- Specify the core hint database explicitly in order.v. (see #252)
- Apply 80 chars per line restriction.

General changes:
- Give consistency to shape of formulae and namings of `lt_def` and `lt_neqAle`
  like lemmas:
  lt_def    x y : (x < y) = (y != x) && (x <= y),
  lt_neqAle x y : (x < y) = (x != y) && (x <= y).
- Enable notation overloading by using scopes and displays:
  + Define `min` and `max` notations (`minr` and `maxr` for `ring_display`) as
    aliases of `meet` and `join` specialized for `total_display`.
  + Provide the `ring_display` version of `le`, `lt`, `ge`, `gt`, `leif`, and
    `comparable` notations and their explicit variants in `Num.Def`.
  + Define 3 variants of `[arg min_(i < n | P) F]` and `[arg max_(i < n | P) F]`
    notations in `nat_scope` (specialized for nat), `order_scope` (general
    version), and `ring_scope` (specialized for `ring_display`).
- Update documents and put CHANGELOG entries.

1 files changed, 29 insertions, 31 deletions

diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v
index eb0785f..48d5254 100644
--- a/mathcomp/algebra/interval.v
+++ b/mathcomp/algebra/interval.v
@@ -1,7 +1,8 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
-From mathcomp Require Import div fintype bigop ssralg finset fingroup ssrnum.
+From mathcomp Require Import div fintype bigop order ssralg finset fingroup.
+From mathcomp Require Import ssrnum.
 
 (*****************************************************************************)
 (* This file provide support for intervals in numerical and real domains.    *)
@@ -39,13 +40,14 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 Local Open Scope ring_scope.
-Import GRing.Theory Num.Theory.
+Import Order.Theory Order.Syntax GRing.Theory Num.Theory.
 
 Local Notation mid x y := ((x + y) / 2%:R).
 
 Section LersifPo.
 
 Variable R : numDomainType.
+Implicit Types (b : bool) (x y z : R).
 
 Definition lersif (x y : R) b := if b then x < y else x <= y.
 
@@ -65,7 +67,7 @@ Lemma lersif_trans x y z b1 b2 :
   x <= y ?< if b1 -> y <= z ?< if b2 -> x <= z ?< if b1 || b2.
 Proof.
 by case: b1 b2 => [] [];
-  apply (ltr_trans, ltr_le_trans, ler_lt_trans, ler_trans).
+  [apply: lt_trans | apply: lt_le_trans | apply: le_lt_trans | apply: le_trans].
 Qed.
 
 Lemma lersif01 b : 0 <= 1 ?< if b.
@@ -74,16 +76,16 @@ Proof. by case: b; apply lter01. Qed.
 Lemma lersif_anti b1 b2 x y :
   (x <= y ?< if b1) && (y <= x ?< if b2) =
   if b1 || b2 then false else x == y.
-Proof. by case: b1 b2 => [] []; rewrite lter_anti. Qed.
+Proof. by case: b1 b2 => [] []; rewrite lte_anti. Qed.
 
 Lemma lersifxx x b : (x <= x ?< if b) = ~~ b.
-Proof. by case: b; rewrite /= lterr. Qed.
+Proof. by case: b; rewrite /= ltexx. Qed.
 
 Lemma lersifNF x y b : y <= x ?< if ~~ b -> x <= y ?< if b = false.
-Proof. by case: b => /= [/ler_gtF|/ltr_geF]. Qed.
+Proof. by case: b => /= [/le_gtF|/lt_geF]. Qed.
 
 Lemma lersifS x y b : x < y -> x <= y ?< if b.
-Proof. by case: b => //= /ltrW. Qed.
+Proof. by case: b => //= /ltW. Qed.
 
 Lemma lersifT x y : x <= y ?< if true = (x < y). Proof. by []. Qed.
 
@@ -132,25 +134,25 @@ Definition lersif_sub_addl := (lersif_subl_addl, lersif_subr_addl).
 
 Lemma lersif_andb x y : {morph lersif x y : p q / p || q >-> p && q}.
 Proof.
-by case=> [] [] /=; rewrite ?ler_eqVlt;
+by case=> [] [] /=; rewrite ?le_eqVlt;
   case: (_ < _)%R; rewrite ?(orbT, orbF, andbF, andbb).
 Qed.
 
 Lemma lersif_orb x y : {morph lersif x y : p q / p && q >-> p || q}.
 Proof.
-by case=> [] [] /=; rewrite ?ler_eqVlt;
+by case=> [] [] /=; rewrite ?le_eqVlt;
   case: (_ < _)%R; rewrite ?(orbT, orbF, orbb).
 Qed.
 
 Lemma lersif_imply b1 b2 r1 r2 :
   b2 ==> b1 -> r1 <= r2 ?< if b1 -> r1 <= r2 ?< if b2.
-Proof. by case: b1 b2 => [] [] //= _ /ltrW. Qed.
+Proof. by case: b1 b2 => [] [] //= _ /ltW. Qed.
 
 Lemma lersifW b x y : x <= y ?< if b -> x <= y.
-Proof. by case: b => // /ltrW. Qed.
+Proof. by case: b => // /ltW. Qed.
 
 Lemma ltrW_lersif b x y : x < y -> x <= y ?< if b.
-Proof. by case: b => // /ltrW. Qed.
+Proof. by case: b => // /ltW. Qed.
 
 Lemma lersif_pmul2l b x : 0 < x -> {mono *%R x : y z / y <= z ?< if b}.
 Proof. by case: b; apply lter_pmul2l. Qed.
@@ -166,7 +168,7 @@ Proof. by case: b; apply lter_nmul2r. Qed.
 
 Lemma real_lersifN x y b : x \is Num.real -> y \is Num.real ->
   x <= y ?< if ~~b = ~~ (y <= x ?< if b).
-Proof. by case: b => [] xR yR /=; case: real_ltrgtP. Qed.
+Proof. by case: b => [] xR yR /=; case: real_ltgtP. Qed.
 
 Lemma real_lersif_norml b x y :
   x \is Num.real ->
@@ -207,20 +209,20 @@ Lemma lersif_distl :
 Proof. by case: b; apply lter_distl. Qed.
 
 Lemma lersif_minr :
-  (x <= Num.min y z ?< if b) = (x <= y ?< if b) && (x <= z ?< if b).
-Proof. by case: b; apply lter_minr. Qed.
+  (x <= y `&` z ?< if b) = (x <= y ?< if b) && (x <= z ?< if b).
+Proof. by case: b; rewrite /= ltexI. Qed.
 
 Lemma lersif_minl :
-  (Num.min y z <= x ?< if b) = (y <= x ?< if b) || (z <= x ?< if b).
-Proof. by case: b; apply lter_minl. Qed.
+  (y `&` z <= x ?< if b) = (y <= x ?< if b) || (z <= x ?< if b).
+Proof. by case: b; rewrite /= lteIx. Qed.
 
 Lemma lersif_maxr :
-  (x <= Num.max y z ?< if b) = (x <= y ?< if b) || (x <= z ?< if b).
-Proof. by case: b; apply lter_maxr. Qed.
+  (x <= y `|` z ?< if b) = (x <= y ?< if b) || (x <= z ?< if b).
+Proof. by case: b; rewrite /= ltexU. Qed.
 
 Lemma lersif_maxl :
-  (Num.max y z <= x ?< if b) = (y <= x ?< if b) && (z <= x ?< if b).
-Proof. by case: b; apply lter_maxl. Qed.
+  (y `|` z <= x ?< if b) = (y <= x ?< if b) && (z <= x ?< if b).
+Proof. by case: b; rewrite /= lteUx. Qed.
 
 End LersifOrdered.
 
@@ -459,13 +461,9 @@ Definition bound_in_itv := (boundl_in_itv, boundr_in_itv).
 
 Lemma itvP : forall (x : R) (i : interval R), x \in i -> itv_rewrite i x.
 Proof.
-move=> x [[[] a|] [[] b|]] /itv_dec // [? ?];
-  do ?split => //; rewrite ?bound_in_itv /le_boundl /le_boundr //=;
-  do 1?[apply/negbTE; rewrite (ler_gtF, ltr_geF) //];
-  by [ rewrite ltrW
-     | rewrite (@ler_trans _ x) // 1?ltrW
-     | rewrite (@ltr_le_trans _ x)
-     | rewrite (@ler_lt_trans _ x) // 1?ltrW ].
+move=> x [[[] a|] [[] b|]] /itv_dec [ha hb]; do !split;
+  rewrite ?bound_in_itv //=; do 1?[apply/negbTE; rewrite (le_gtF, lt_geF)];
+  by [ | apply: ltW | move: (lersif_trans ha hb) => //=; exact: ltW ].
 Qed.
 
 Arguments itvP [x i].
@@ -484,7 +482,7 @@ Definition itv_intersectioni1 : right_id `]-oo, +oo[ itv_intersection.
 Proof. by case=> [[lb lr |] [ub ur |]]. Qed.
 
 Lemma itv_intersectionii : idempotent itv_intersection.
-Proof. by case=> [[[] lr |] [[] ur |]] //=; rewrite !lerr. Qed.
+Proof. by case=> [[[] lr |] [[] ur |]] //=; rewrite !lexx. Qed.
 
 Definition subitv (i1 i2 : interval R) :=
   match i1, i2 with
@@ -558,7 +556,7 @@ Lemma le_boundl_total : total (@le_boundl R).
 Proof. by move=> [[] l |] [[] r |] //=; case: (ltrgtP l r). Qed.
 
 Lemma le_boundr_total : total (@le_boundr R).
-Proof. by move=> [[] l |] [[] r |] //=; case (ltrgtP l r). Qed.
+Proof. by move=> [[] l |] [[] r |] //=; case: (ltrgtP l r). Qed.
 
 Lemma itv_splitU (xc : R) bc a b : xc \in Interval a b ->
   forall y, y \in Interval a b =
@@ -626,7 +624,7 @@ Variable R : realFieldType.
 Lemma mid_in_itv : forall ba bb (xa xb : R), xa <= xb ?< if ba || bb
   -> mid xa xb \in Interval (BOpen_if ba xa) (BOpen_if bb xb).
 Proof.
-by move=> [] [] xa xb /= ?; apply/itv_dec=> /=; rewrite ?midf_lte // ?ltrW.
+by move=> [] [] xa xb /= ?; apply/itv_dec=> /=; rewrite ?midf_lte // ?ltW.
 Qed.
 
 Lemma mid_in_itvoo : forall (xa xb : R), xa < xb -> mid xa xb \in `]xa, xb[.