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, 16 insertions, 17 deletions

diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v
index c95d03b..78c5295 100644
--- a/mathcomp/character/character.v
+++ b/mathcomp/character/character.v
@@ -1,9 +1,9 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype choice ssrnat seq.
-From mathcomp Require Import path div fintype tuple finfun bigop prime ssralg.
-From mathcomp Require Import poly finset gproduct fingroup morphism perm.
-From mathcomp Require Import automorphism quotient finalg action zmodp.
+From mathcomp Require Import path div fintype tuple finfun bigop prime order.
+From mathcomp Require Import ssralg poly finset gproduct fingroup morphism.
+From mathcomp Require Import perm automorphism quotient finalg action zmodp.
 From mathcomp Require Import commutator cyclic center pgroup nilpotent sylow.
 From mathcomp Require Import abelian matrix mxalgebra mxpoly mxrepresentation.
 From mathcomp Require Import vector ssrnum algC classfun.
@@ -67,7 +67,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Import GroupScope GRing.Theory Num.Theory.
+Import Order.TTheory GroupScope GRing.Theory Num.Theory.
 Local Open Scope ring_scope.
 
 Local Notation algCF := [fieldType of algC].
@@ -656,7 +656,7 @@ Lemma irr1_gt0 i : 0 < 'chi_i 1%g.
 Proof. by rewrite irr1_degree ltr0n irr_degree_gt0. Qed.
 
 Lemma irr1_neq0 i : 'chi_i 1%g != 0.
-Proof. by rewrite eqr_le ltr_geF ?irr1_gt0. Qed.
+Proof. by rewrite eq_le lt_geF ?irr1_gt0. Qed.
 
 Lemma irr_neq0 i : 'chi_i != 0.
 Proof. by apply: contraNneq (irr1_neq0 i) => ->; rewrite cfunE. Qed.
@@ -880,7 +880,7 @@ Lemma char1_eq0 chi : chi \is a character -> (chi 1%g == 0) = (chi == 0).
 Proof.
 case/char_sum_irr=> r ->; apply/idP/idP=> [|/eqP->]; last by rewrite cfunE.
 case: r => [|i r]; rewrite ?big_nil // sum_cfunE big_cons.
-rewrite paddr_eq0 ?sumr_ge0  => // [||j _]; rewrite 1?ltrW ?irr1_gt0 //.
+rewrite paddr_eq0 ?sumr_ge0  => // [||j _]; rewrite 1?ltW ?irr1_gt0 //.
 by rewrite (negbTE (irr1_neq0 i)).
 Qed.
 
@@ -1021,7 +1021,7 @@ Proof. by move=> Gx; rewrite -lin_charX // expg_order lin_char1. Qed.
 
 Lemma normC_lin_char x : x \in G -> `|xi x| = 1.
 Proof.
-move=> Gx; apply/eqP; rewrite -(@pexpr_eq1 _ _ #[x]) ?normr_ge0 //.
+move=> Gx; apply/eqP; rewrite -(@pexpr_eq1 _ _ #[x]) //.
 by rewrite -normrX // lin_char_unity_root ?normr1.
 Qed.
 
@@ -1163,12 +1163,11 @@ have exp_e j: e 0 j ^+ #[x] = 1.
   rewrite expgS repr_mxM ?groupX // {1}rGx -!mulmxA mulKVmx //.
   by rewrite mul_diag_mx mulmxA [M in _ = M]mxE -IHn exprS {1}mxE eqxx.
 have norm1_e j: `|e 0 j| = 1.
-  apply/eqP; rewrite -(@pexpr_eq1 _ _ #[x]) ?normr_ge0 //.
-  by rewrite -normrX exp_e normr1.
+  by apply/eqP; rewrite -(@pexpr_eq1 _ _ #[x]) // -normrX exp_e normr1.
 exists e; split=> //; first by exists B.
   rewrite cfRepr1 !cfunE Gx rGx mxtrace_mulC mulKVmx // mxtrace_diag.
-  split=> //=; apply: (ler_trans (ler_norm_sum _ _ _)).
-  by rewrite (eq_bigr _ (in1W norm1_e)) sumr_const card_ord lerr.
+  split=> //=; apply: (le_trans (ler_norm_sum _ _ _)).
+  by rewrite (eq_bigr _ (in1W norm1_e)) sumr_const card_ord lexx.
 rewrite !cfunE groupV !mulrb Gx rGx mxtrace_mulC mulKVmx //.
 rewrite -trace_map_mx map_diag_mx; set d' := diag_mx _.
 rewrite -[d'](mulKVmx unitB) mxtrace_mulC -[_ *m _](repr_mxK rG Gx) rGx.
@@ -1559,7 +1558,7 @@ Lemma constt_ortho_char (phi psi : 'CF(G)) i j :
 Proof.
 move=> _ _ /constt_charP[//|phi1 Nphi1 ->] /constt_charP[//|psi1 Npsi1 ->].
 rewrite cfdot_irr; case: eqP => // -> /eqP/idPn[].
-rewrite cfdotDl !cfdotDr cfnorm_irr -addrA gtr_eqF ?ltr_paddr ?ltr01 //.
+rewrite cfdotDl !cfdotDr cfnorm_irr -addrA gt_eqF ?ltr_paddr ?ltr01 //.
 by rewrite Cnat_ge0 ?rpredD ?Cnat_cfdot_char ?irr_char.
 Qed.
 
@@ -1756,7 +1755,7 @@ Lemma constt_Res_trans j psi :
     psi \is a character -> j \in irr_constt psi -> 
   {subset irr_constt ('Res[H, G] 'chi_j) <= irr_constt ('Res[H] psi)}.
 Proof.
-move=> Npsi Cj i; apply: contraNneq; rewrite eqr_le => {1}<-.
+move=> Npsi Cj i; apply: contraNneq; rewrite eq_le => {1}<-.
 rewrite cfdot_Res_ge_constt ?Cnat_ge0 ?Cnat_cfdot_char_irr //.
 by rewrite cfRes_char ?irr_char.
 Qed.
@@ -2859,18 +2858,18 @@ by rewrite cfcenter_eq_center subsetIr.
 Qed.
 
 (* This is Isaacs (2.29). *)
-Lemma cfnorm_Res_lerif H phi :
+Lemma cfnorm_Res_leif H phi :
     H \subset G ->
   '['Res[H] phi] <= #|G : H|%:R * '[phi] ?= iff (phi \in 'CF(G, H)).
 Proof.
 move=> sHG; rewrite cfun_onE mulrCA natf_indexg // -mulrA mulKf ?neq0CG //.
 rewrite (big_setID H) (setIidPr sHG) /= addrC.
-rewrite (mono_lerif (ler_pmul2l _)) ?invr_gt0 ?gt0CG // -lerif_subLR -sumrB.
+rewrite (mono_leif (ler_pmul2l _)) ?invr_gt0 ?gt0CG // -leif_subLR -sumrB.
 rewrite big1 => [|x Hx]; last by rewrite !cfResE ?subrr.
 have ->: (support phi \subset H) = (G :\: H \subset [set x | phi x == 0]).
   rewrite subDset setUC -subDset; apply: eq_subset => x.
   by rewrite !inE (andb_idr (contraR _)) // => /cfun0->.
-rewrite (sameP subsetP forall_inP); apply: lerif_0_sum => x _.
+rewrite (sameP subsetP forall_inP); apply: leif_0_sum => x _.
 by rewrite !inE /<?=%R mul_conjC_ge0 eq_sym mul_conjC_eq0.
 Qed.
 
@@ -2879,7 +2878,7 @@ Lemma irr1_bound (i : Iirr G) :
   ('chi_i 1%g) ^+ 2 <= #|G : 'Z('chi_i)%CF|%:R
                     ?= iff ('chi_i \in 'CF(G, 'Z('chi_i)%CF)).
 Proof.
-congr (_ <= _ ?= iff _): (cfnorm_Res_lerif 'chi_i (cfcenter_sub 'chi_i)).
+congr (_ <= _ ?= iff _): (cfnorm_Res_leif 'chi_i (cfcenter_sub 'chi_i)).
   have [xi Lxi ->] := cfcenter_Res 'chi_i.
   have /irrP[j ->] := lin_char_irr Lxi; rewrite cfdotZl cfdotZr cfdot_irr eqxx.
   by rewrite mulr1 irr1_degree conjC_nat.