editing documentation in order.v and ssrnum.v

2 files changed, 94 insertions, 89 deletions

diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index 5737a2d..6bbf24a 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -6,7 +6,10 @@ From mathcomp Require Import ssralg poly.
 
 (******************************************************************************)
 (* This file defines some classes to manipulate number structures, i.e        *)
-(* structures with an order and a norm.                                       *)
+(* structures with an order and a norm. To use this file, insert              *)
+(* "Import Num.Theory." before your scripts. You can also "Import Num.Def."   *)
+(* to enjoy shorter notations (e.g., minr instead of Num.min, lerif instead   *)
+(* of Num.leif, etc.).                                                        *)
 (*                                                                            *)
 (*   * NumDomain (Integral domain with an order and a norm)                   *)
 (*    numDomainType == interface for a num integral domain.                   *)
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index 0daacfb..f5dfa03 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -4,75 +4,118 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
 From mathcomp Require Import div choice fintype tuple bigop finset.
 
 (******************************************************************************)
-(* This files defines a ordered and decidable relations on a type as          *)
-(* canonical structure.  One need to import some of the following modules to  *)
-(* get the definitions, notations, and theory of such relations.              *)
-(*       Order.Def: definitions of basic operations.                          *)
-(*    Order.Syntax: fancy notations for ordering declared in the order_scope  *)
-(*                  (%O).                                                     *)
-(*   Order.LTheory: theory of partially ordered types and lattices excluding  *)
-(*                  complement and totality related theorems.                 *)
-(*   Order.CTheory: theory of complemented lattices including Order.LTheory.  *)
-(*   Order.TTheory: theory of totally ordered types including Order.LTheory.  *)
-(*    Order.Theory: theory of ordered types including all of the above        *)
-(*                  theory modules.                                           *)
+(* This files defines order relations. It contains several modules            *)
+(* implementing different theories:                                           *)
+(*   Order.LTheory: partially ordered types and lattices excluding complement *)
+(*                  and totality related theorems.                            *)
+(*   Order.CTheory: complemented lattices including Order.LTheory.            *)
+(*   Order.TTheory: totally ordered types including Order.LTheory.            *)
+(*    Order.Theory: ordered types including all of the above theory modules   *)
+(*                                                                            *)
+(* To access the definitions, notations, and the theory from, say,            *)
+(* "Order.Xyz", insert "Import Order.Xyz." on the top of your scripts.        *)
+(* Notations are accessible by opening the scope "order_scope" bound to the   *)
+(* delimiting key "O".                                                        *)
 (*                                                                            *)
 (* We provide the following structures of ordered types                       *)
 (*        porderType == the type of partially ordered types                   *)
 (*       latticeType == the type of distributive lattices                     *)
-(*      blatticeType == ... with a bottom elemnt                              *)
-(*     tblatticeType == ... with both a top and a bottom                      *)
+(*      blatticeType == latticeType with a bottom element                     *)
+(*     tblatticeType == latticeType with both a top and a bottom              *)
 (*     cblatticeType == the type of sectionally complemented lattices         *)
-(*                      (lattices with a complement to, and bottom)           *)
+(*                      (lattices with bottom and a difference operation)     *)
 (*    ctblatticeType == the type of complemented lattices                     *)
-(*                      (lattices with a top, bottom, and general complement) *)
+(*                      (lattices with top, bottom, difference, complement)   *)
 (*         orderType == the type of totally ordered types                     *)
-(*    finPOrderType == the type of partially ordered finite types             *)
+(*     finPOrderType == the type of partially ordered finite types            *)
 (*    finLatticeType == the type of nonempty finite lattices                  *)
 (*   finClatticeType == the type of nonempty finite complemented lattices     *)
 (*      finOrderType == the type of nonempty totally ordered finite types     *)
 (*                                                                            *)
-(* Each of these structure take a first argument named display, of type unit  *)
-(* instanciating it with tt or an unknown key will lead to a default display. *)
-(* Optionally, one can configure the display by setting one owns notation on  *)
-(* operators instanciated for their particular display.                       *)
+(* Each of these structures take a first argument named display, of type      *)
+(* unit. Instantiating it with tt or an unknown key will lead to a default    *)
+(* display. Optionally, one can configure the display by setting one own's    *)
+(* notation on operators instantiated for their particular display.           *)
 (* One example of this is the converse display ^c, every notation with the    *)
 (* suffix ^c (e.g. x <=^c y) is about the converse order, in order not to     *)
 (* confuse the normal order with its converse.                                *)
 (*                                                                            *)
+(* Over these structures, we have the following relations                     *)
+(*            x <= y <-> x is less than or equal to y.                        *)
+(*             x < y <-> x is less than y (:= (y != x) && (x <= y)).          *)
+(*            x >= y <-> x is greater than or equal to y (:= y <= x).         *)
+(*             x > y <-> x is greater than y (:= y < x).                      *)
+(*   x <= y ?= iff C <-> x is less than y, or equal iff C is true.            *)
+(*           x >=< y <-> x and y are comparable (:= (x <= y) || (y <= x)).    *)
+(*            x >< y <-> x and y are incomparable.                            *)
+(* For lattices we provide the following operations                           *)
+(*           x `&` y == the meet of x and y.                                  *)
+(*           x `|` y == the join of x and y.                                  *)
+(*                 0 == the bottom element.                                   *)
+(*                 1 == the top element.                                      *)
+(*           x `\` y == the (sectional) complement of y in [0, x].            *)
+(*              ~` x == the complement of x in [0, 1].                        *)
+(*   \meet_<range> e == iterated meet of a lattice with a top.                *)
+(*   \join_<range> e == iterated join of a lattice with a bottom.             *)
+(* For orderType we provide the following operations                          *)
+(*   [arg minr_(i < i0 | P) M] == a value i : T minimizing M : R, subject to  *)
+(*                      the condition P (i may appear in P and M), and        *)
+(*                      provided P holds for i0.                              *)
+(*   [arg maxr_(i > i0 | P) M] == a value i maximizing M subject to P and     *)
+(*                      provided P holds for i0.                              *)
+(*   [arg min_(i < i0 in A) M] == an i \in A minimizing M if i0 \in A.        *)
+(*   [arg max_(i > i0 in A) M] == an i \in A maximizing M if i0 \in A.        *)
+(*   [arg min_(i < i0) M] == an i : T minimizing M, given i0 : T.             *)
+(*   [arg max_(i > i0) M] == an i : T maximizing M, given i0 : T.             *)
+(*                                                                            *)
+(* There are three distinct uses of the symbols                               *)
+(* <, <=, >, >=, _ <= _ ?= iff _, >=<, and ><:                                *)
+(*    0-ary, unary (prefix), and binary (infix).                              *)
+(* 0. <%O, <=%O, >%O, >=%O, <?=%O, >=<%O, and ><%O stand respectively for     *)
+(*    lt, le, gt, ge, leif (_ <= _ ?= iff _), comparable, and incomparable.   *)
+(* 1. (< x),  (<= x), (> x), (>= x), (>=< x), and (>< x) stand respectively   *)
+(*    for (>%O x), (>=%O x), (<%O x), (<=%O x), (>=<%O x), and (><%O x).      *)
+(*    So (< x) is a predicate characterizing elements smaller than x.         *)
+(* 2. (x < y), (x <= y), ... mean what they are expected to.                  *)
+(*  These conventions are compatible with Haskell's,                          *)
+(*   where ((< y) x) = (x < y) = ((<) x y),                                   *)
+(*   except that we write <%O instead of (<).                                 *)
+(*                                                                            *)
 (* In order to build the above structures, one must provide the appropriate   *)
 (* mixin to the following structure constructors. The list of possible mixins *)
-(* is indicated after each constructor. Each mixin is documented in the next. *)
+(* is indicated after each constructor. Each mixin is documented in the next  *)
 (* paragraph.                                                                 *)
 (*                                                                            *)
-(* POrderType pord_mixin == builds a porderType from a choiceType             *)
+(* POrderType disp T pord_mixin == builds a porderType from a canonical       *)
+(* choiceType instance of T                                                   *)
 (*   where pord_mixin can be of types                                         *)
 (*     lePOrderMixin, ltPOrderMixin, meetJoinMixin,                           *)
-(*     leOrderMixin or ltOrderMixin,                                          *)
-(*   or computed using PCanPOrderMixin or CanPOrderMixin.                     *)
+(*     leOrderMixin or ltOrderMixin                                           *)
+(*   or computed using PcanPOrderMixin or CanPOrderMixin.                     *)
 (*                                                                            *)
-(* LatticeType lat_mixin == builds a distributive lattice from a porderType   *)
+(* LatticeType T lat_mixin == builds a distributive lattice from a porderType *)
 (*   where lat_mixin can be of types                                          *)
 (*     latticeMixin, totalPOrderMixin, meetJoinMixin,                         *)
 (*     leOrderMixin or ltOrderMixin                                           *)
 (*   or computed using IsoLatticeMixin.                                       *)
 (*                                                                            *)
-(* OrderType pord_mixin == builds a orderType from a latticeType              *)
+(* OrderType T pord_mixin == builds an orderType from a latticeType           *)
 (*   where pord_mixin can be of types                                         *)
 (*     leOrderMixin, ltOrderMixin or orderMixin,                              *)
-(*   or computed using MonoOrderMixin.                                        *)
+(*   or computed using MonoTotalMixin.                                        *)
 (*                                                                            *)
-(* BLatticeType bot_mixin == builds a blatticeType from a latticeType         *)
-(*                            and a bottom operation                          *)
+(* BLatticeType T bot_mixin == builds a blatticeType from a latticeType       *)
+(*                             and a bottom element                           *)
 (*                                                                            *)
-(* TBLatticeType top_mixin == builds a tblatticeType from a blatticeType      *)
-(*                            and a top operation                             *)
+(* TBLatticeType T top_mixin == builds a tblatticeType from a blatticeType    *)
+(*                              and a top element                             *)
 (*                                                                            *)
-(* CBLatticeType compl_mixin == builds a cblatticeType from a blatticeType    *)
-(*                              and a relative complement operation           *)
+(* CBLatticeType T sub_mixin == builds a cblatticeType from a blatticeType    *)
+(*                              and a difference operation                    *)
 (*                                                                            *)
-(* CTBLatticeType sub_mixin == builds a cblatticeType from a blatticeType     *)
-(*                             and a total complement supplement operation    *)
+(* CTBLatticeType T compl_mixin == builds a ctblatticeType from a             *)
+(*                                 tblatticeType and a complement             *)
+(*                                 operation                                  *)
 (*                                                                            *)
 (* Additionally:                                                              *)
 (* - [porderType of _] ... notations are available to recover structures on   *)
@@ -80,7 +123,7 @@ From mathcomp Require Import div choice fintype tuple bigop finset.
 (* - [finPOrderType of _] ... notations to compute joins between finite types *)
 (*                            and ordered types                               *)
 (*                                                                            *)
-(* List of possible mixins:                                                   *)
+(* List of possible mixins (a.k.a. factories):                                *)
 (*                                                                            *)
 (* - lePOrderMixin == on a choiceType, takes le, lt,                          *)
 (*                    reflexivity, antisymmetry and transitivity of le.       *)
@@ -119,60 +162,19 @@ From mathcomp Require Import div choice fintype tuple bigop finset.
 (*                   (can build: latticeType)                                 *)
 (*                                                                            *)
 (* - blatticeMixin, tblatticeMixin, cblatticeMixin, ctblatticeMixin           *)
-(*   == mixins with with one extra operator                                   *)
+(*   == mixins with one extra operation                                       *)
 (*      (respectively bottom, top, relative complement, and total complement  *)
 (*                                                                            *)
 (* Additionally:                                                              *)
-(* - [porderMixin of T by <:] creates an porderMixin by subtyping.            *)
+(* - [porderMixin of T by <:] creates a porderMixin by subtyping.             *)
 (* - [totalOrderMixin of T by <:] creates the associated totalOrderMixin.     *)
 (* - PCanPOrderMixin, CanPOrderMixin create porderMixin from cancellations    *)
 (* - MonoTotalMixin creates a totalPOrderMixin from monotonicity              *)
 (* - IsoLatticeMixin creates a latticeMixin from an ordered structure         *)
-(*   isomorphism (i.e. cancel f f', cancel f' f, {mono f : x y / x <= y})     *)
-(*                                                                            *)
-(* Over these structures, we have the following operations                    *)
-(*            x <= y <-> x is less than or equal to y.                        *)
-(*             x < y <-> x is less than y (:= (y != x) && (x <= y)).          *)
-(*            x >= y <-> x is greater than or equal to y (:= y <= x).         *)
-(*             x > y <-> x is greater than y (:= y < x).                      *)
-(*   x <= y ?= iff C <-> x is less than y, or equal iff C is true.            *)
-(*           x >=< y <-> x and y are comparable (:= (x <= y) || (y <= x)).    *)
-(*            x >< y <-> x and y are incomparable.                            *)
-(* For lattices we provide the following operations                           *)
-(*           x `&` y == the meet of x and y.                                  *)
-(*           x `|` y == the join of x and y.                                  *)
-(*                 0 == the bottom element.                                   *)
-(*                 1 == the top element.                                      *)
-(*           x `\` y == the (sectional) complement of y in [0, x].            *)
-(*              ~` x == the complement of x in [0, 1].                        *)
-(*   \meet_<range> e == iterated meet of a lattice with a top.                *)
-(*   \join_<range> e == iterated join of a lattice with a bottom.             *)
-(* For orderType we provide the following operations                          *)
-(*   [arg minr_(i < i0 | P) M] == a value i : T minimizing M : R, subject to  *)
-(*                      the condition P (i may appear in P and M), and        *)
-(*                      provided P holds for i0.                              *)
-(*   [arg maxr_(i > i0 | P) M] == a value i maximizing M subject to P and     *)
-(*                      provided P holds for i0.                              *)
-(*   [arg min_(i < i0 in A) M] == an i \in A minimizing M if i0 \in A.        *)
-(*   [arg max_(i > i0 in A) M] == an i \in A maximizing M if i0 \in A.        *)
-(*   [arg min_(i < i0) M] == an i : T minimizing M, given i0 : T.             *)
-(*   [arg max_(i > i0) M] == an i : T maximizing M, given i0 : T.             *)
-(*                                                                            *)
-(* There are three distinct uses of the symbols                               *)
-(* <, <=, >, >=, _ <= _ ?= iff _, >=<, and ><:                                *)
-(*    0-ary, unary (prefix), and binary (infix).                              *)
-(* 0. <%O, <=%O, >%O, >=%O, <?=%O, >=<%O, and ><%O stand respectively for     *)
-(*    lt, le, gt, ge, leif (_ <= _ ?= iff _), comparable, and incomparable.   *)
-(* 1. (< x),  (<= x), (> x), (>= x), (>=< x), and (>< x) stand respectively   *)
-(*    for (>%O x), (>=%O x), (<%O x), (<=%O x), (>=<%O x), and (><%O x).      *)
-(*    So (< x) is a predicate characterizing elements smaller than x.         *)
-(* 2. (x < y), (x <= y), ... mean what they are expected to.                  *)
-(*  These convention are compatible with Haskell's,                           *)
-(*   where ((< y) x) = (x < y) = ((<) x y),                                   *)
-(*   except that we write <%O instead of (<).                                 *)
+(*   isomorphism (i.e., cancel f f', cancel f' f, {mono f : x y / x <= y})    *)
 (*                                                                            *)
 (* We provide the following canonical instances of ordered types              *)
-(* - all possible strucutre on bool                                           *)
+(* - all possible structures on bool                                          *)
 (* - porderType, latticeType, orderType, blatticeType on nat                  *)
 (* - porderType, latticeType, orderType, blatticeType, cblatticeType,         *)
 (*   tblatticeType, ctblatticeType on T *prod[disp] T' a copy of T * T'       *)
@@ -197,17 +199,17 @@ From mathcomp Require Import div choice fintype tuple bigop finset.
 (*     (and n.-tuplelexi T its specialization to lexi_display)                *)
 (* and all possible finite type instances                                     *)
 (*                                                                            *)
-(* In order to get a cannoical order on prod or seq, one may import modules   *)
+(* In order to get a canonical order on prod or seq, one may import modules   *)
 (*   DefaultProdOrder or DefaultProdLexiOrder, DefaultSeqProdOrder or         *)
 (*   DefaultSeqLexiOrder, and DefaultTupleProdOrder or DefaultTupleLexiOrder. *)
 (*                                                                            *)
-(* On orderType leP ltP ltgtP are the three main lemmas for case analysis.    *)
-(* On porderType, one may use comparableP comparable_leP comparable_ltP       *)
-(*   and comparable_ltgtP are the three main lemmas for case analysis.        *)
+(* On orderType, leP ltP ltgtP are the three main lemmas for case analysis.   *)
+(* On porderType, one may use comparableP, comparable_leP, comparable_ltP,    *)
+(*   and comparable_ltgtP, which are the four main lemmas for case analysis.  *)
 (*                                                                            *)
-(* We also provide specialized version of some theorems from path.v.          *)
+(* We also provide specialized versions of some theorems from path.v.         *)
 (*                                                                            *)
-(* This file is based on prior works by                                       *)
+(* This file is based on prior work by                                        *)
 (* D. Dreyer, G. Gonthier, A. Nanevski, P-Y Strub, B. Ziliani                 *)
 (******************************************************************************)