Module mathcomp.order.order

From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq.
From mathcomp Require Import path fintype tuple bigop finset div prime finfun.
From mathcomp Require Import finset.
From mathcomp Require Export preorder.

                  Types equipped with order relations

NB: See CONTRIBUTING.md for an introduction to HB concepts and commands.

This files defines types equipped with order relations.

* How to use orders in MathComp?
Use one of the following modules implementing different theories (all
located in the module Order):
  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." at the top of your scripts. You can
also "Import Order.Def." to enjoy shorter notations (e.g., min instead of
Order.min, nondecreasing instead of Order.nondecreasing, etc.).

In order to reason about abstract orders, notations are accessible by
opening the scope "order_scope" bound to the delimiting key "O"; however,
when dealing with another notation scope providing order notations for
a concrete instance (e.g., "ring_scope"), it is not recommended to open
"order_scope" at the same time.

* Control of inference (parsing) and printing
One characteristic of ordered types is that one carrier type may have
several orders. For example, natural numbers can be totally or partially
ordered by the less than or equal relation, the divisibility relation, and
their dual relations. Therefore, we need a way to control inference of
ordered type instances and printing of generic relations and operations on
ordered types. As a rule of thumb, we use the carrier type or its "alias"
(named copy) to control inference (using canonical structures), and use a
"display" to control the printing of notations.

Each generic interface and operation for ordered types has, as its first
argument, a "display" of type Order.disp_t. For example, the less than or
equal relation has type:
  Order.le : forall {d : Order.disp_t} {T : porderType d}, rel T,
where porderType d is the structure of partially ordered types with
display d. (@Order.le dvd_display _ m n) is printed as m %| n because
ordered type instances associated to the display dvd_display is intended
to represent natural numbers partially ordered by the divisibility
relation.

We stress that order structure inference can be triggered only from the
carrier type (or its alias), but not the display. For example, writing
m %| n for m and n of type nat does not trigger an inference of the
divisibility relation on natural numbers, which is associated to an alias
natdvd for nat; such an inference should be triggered through the use of
the corresponding alias, i.e., (m : natdvd) %| n. In other words, displays
are merely used to inform the user and the notation mechanism of what the
inference did; they are not additional input for the inference.

See below for various aliases and their associated displays.

NB: algebra/ssrnum.v provides the display ring_display to change the
scope of the usual notations to ring_scope.

Instantiating d with Disp tt tt or an unknown display will lead to a
default display for notations.

Alternative notation displays can be defined by :
1. declaring a new opaque definition of type unit. Using the idiom
   `Fact my_display : Order.disp_t. Proof. exact: Disp tt tt. Qed.`
2. using this symbol to tag canonical porderType structures using
   `HB.instance Definition _ := isPOrder.Build my_display my_type ...`,
3. declaring notations for the main operations of this library, by
   setting the first argument of the definition to the display, e.g.
   `Notation my_syndef_le x y := @Order.le my_display _ x y.` or
   `Notation "x <=< y" := @Order.lt my_display _ x y (at level ...).`
   Non overloaded notations will default to the default display.
We suggest the user to refer to the example of natdvd below as a guideline
example to add their own displays.

* Interfaces
We provide the following interfaces for types equipped with an order:

             porderType d == the type of partially ordered types
                             The HB class is called POrder.
            bPOrderType d == porderType with a bottom element (\bot)
                             The HB class is called BPOrder.
            tPOrderType d == porderType with a top element (\top)
                             The HB class is called TPOrder.
           tbPOrderType d == porderType with both a top and a bottom
                             The HB class is called TBPOrder.
    meetSemilatticeType d == the type of meet semilattices
                             The HB class is called MeetSemilattice.
   bMeetSemilatticeType d == meetSemilatticeType with a bottom element
                             The HB class is called BMeetSemilattice.
   tMeetSemilatticeType d == meetSemilatticeType with a top element
                             The HB class is called TMeetSemilattice.
  tbMeetSemilatticeType d == meetSemilatticeType with both a top and a
                             bottom
                             The HB class is called TBMeetSemilattice.
    joinSemilatticeType d == the type of join semilattices
                             The HB class is called JoinSemilattice.
   bJoinSemilatticeType d == joinSemilatticeType with a bottom element
                             The HB class is called BJoinSemilattice.
   tJoinSemilatticeType d == joinSemilatticeType with a top element
                             The HB class is called TJoinSemilattice.
  tbJoinSemilatticeType d == joinSemilatticeType with both a top and a
                             bottom
                             The HB class is called TBJoinSemilattice.
            latticeType d == the type of lattices
                             The HB class is called Lattice.
           bLatticeType d == latticeType with a bottom element
                             The HB class is called BLattice.
           tLatticeType d == latticeType with a top element
                             The HB class is called TLattice.
          tbLatticeType d == latticeType with both a top and a bottom
                             The HB class is called TBLattice.
       distrLatticeType d == the type of distributive lattices
                             The HB class is called DistrLattice.
      bDistrLatticeType d == distrLatticeType with a bottom element
                             The HB class is called BDistrLattice.
      tDistrLatticeType d == distrLatticeType with a top element
                             The HB class is called TDistrLattice.
     tbDistrLatticeType d == distrLatticeType with both a top and a bottom
                             The HB class is called TBDistrLattice.
              orderType d == the type of totally ordered types
                             The HB class is called Total.
             bOrderType d == orderType with a bottom element
                             The HB class is called BTotal.
             tOrderType d == orderType with a top element
                             The HB class is called TTotal.
            tbOrderType d == orderType with both a top and a bottom
                             The HB class is called TBTotal.
      cDistrLatticeType d == the type of relatively complemented
                             distributive lattices, where each interval
                             [a, b] is equipped with a complement operation
                             The HB class is called CDistrLattice.
     cbDistrLatticeType d == the type of sectionally complemented
                             distributive lattices, equipped with a bottom,
                             a relative complement operation, and a
                             difference operation, i.e., a complement
                             operation for each interval of the form
                             [\bot, b]
                             The HB class is called CBDistrLattice.
     ctDistrLatticeType d == the type of dually sectionally complemented
                             distributive lattices, equipped with a top,
                             a relative complement operation, and a
                             dual difference operation, i.e. a complement
                             operation for each interval of the form
                             [a, \top]
                             The HB class is called CTDistrLattice.
    ctbDistrLatticeType d == the type of complemented distributive
                             lattices, equipped with top, bottom,
                             difference, dual difference, and complement
                             The HB class is called CTBDistrLattice.
          finPOrderType d == the type of partially ordered finite types
                             The HB class is called FinPOrder.
         finBPOrderType d == finPOrderType with a bottom element
                             The HB class is called FinBPOrder.
         finTPOrderType d == finPOrderType with a top element
                             The HB class is called FinTPOrder.
        finTBPOrderType d == finPOrderType with both a top and a bottom
                             The HB class is called FinTBPOrder.
 finMeetSemilatticeType d == the type of finite meet semilattice types
                             The HB class is called FinMeetSemilattice.
finBMeetSemilatticeType d == finMeetSemilatticeType with a bottom element
                             Note that finTMeetSemilatticeType is just
                             finTBLatticeType.
                             The HB class is called FinBMeetSemilattice.
 finJoinSemilatticeType d == the type of finite join semilattice types
                             The HB class is called FinJoinSemilattice.
finTJoinSemilatticeType d == finJoinSemilatticeType with a top element
                             Note that finBJoinSemilatticeType is just
                             finTBLatticeType.
                             The HB class is called FinTJoinSemilattice.
         finLatticeType d == the type of finite lattices
                             The HB class is called FinLattice.
       finTBLatticeType d == the type of nonempty finite lattices
                             The HB class is called FinTBLattice.
    finDistrLatticeType d == the type of finite distributive lattices
                             The HB class is called FinDistrLattice.
  finTBDistrLatticeType d == the type of nonempty finite distributive
                             lattices
                             The HB class is called FinTBDistrLattice.
           finOrderType d == the type of totally ordered finite types
                             The HB class is called FinTotal.
         finTBOrderType d == the type of nonempty totally ordered finite
                             types
                             The HB class is called FinTBTotal.
   finCDistrLatticeType d == the type of finite relatively complemented
                             distributive lattices
                             The HB class is called FinCDistrLattice.
 finCTBDistrLatticeType d == the type of finite complemented distributive
                             lattices
                             The HB class is called FinCTBDistrLattice.

and their joins with subType:

         subPOrder d T P d' == join of porderType d' and subType
                               (P : pred T) such that val is monotonic
                               The HB class is called SubPOrder.
    meetSubLattice d T P d' == join of latticeType d' and subType
                               (P : pred T) such that val is monotonic and
                               a morphism for meet
                               The HB class is called MeetSubLattice.
    joinSubLattice d T P d' == join of latticeType d' and subType
                               (P : pred T) such that val is monotonic and
                               a morphism for join
                               The HB class is called JoinSubLattice.
        subLattice d T P d' == join of JoinSubLattice and MeetSubLattice
                               The HB class is called SubLattice.
   bJoinSubLattice d T P d' == join of JoinSubLattice and BLattice
                               such that val is a morphism for \bot
                               The HB class is called BJoinSubLattice.
   tMeetSubLattice d T P d' == join of MeetSubLattice and TLattice
                               such that val is a morphism for \top
                               The HB class is called TMeetSubLattice.
       bSubLattice d T P d' == join of SubLattice and BLattice
                               such that val is a morphism for \bot
                               The HB class is called BSubLattice.
       tSubLattice d T P d' == join of SubLattice and TLattice
                               such that val is a morphism for \top
                               The HB class is called BSubLattice.
          subOrder d T P d' == join of orderType d' and
                               subLatticeType d T P d'
                               The HB class is called SubOrder.
  subPOrderLattice d T P d' == join of SubPOrder and Lattice
                               The HB class is called SubPOrderLattice.
 subPOrderBLattice d T P d' == join of SubPOrder and BLattice
                               The HB class is called SubPOrderBLattice.
 subPOrderTLattice d T P d' == join of SubPOrder and TLattice
                               The HB class is called SubPOrderTLattice.
subPOrderTBLattice d T P d' == join of SubPOrder and TBLattice
                               The HB class is called SubPOrderTBLattice.
   meetSubBLattice d T P d' == join of MeetSubLattice and BLattice
                               The HB class is called MeetSubBLattice.
   meetSubTLattice d T P d' == join of MeetSubLattice and TLattice
                               The HB class is called MeetSubTLattice.
  meetSubTBLattice d T P d' == join of MeetSubLattice and TBLattice
                               The HB class is called MeetSubTBLattice.
   joinSubBLattice d T P d' == join of JoinSubLattice and BLattice
                               The HB class is called JoinSubBLattice.
   joinSubTLattice d T P d' == join of JoinSubLattice and TLattice
                               The HB class is called JoinSubTLattice.
  joinSubTBLattice d T P d' == join of JoinSubLattice and TBLattice
                               The HB class is called JoinSubTBLattice.
       subBLattice d T P d' == join of SubLattice and BLattice
                               The HB class is called SubBLattice.
       subTLattice d T P d' == join of SubLattice and TLattice
                               The HB class is called SubTLattice.
      subTBLattice d T P d' == join of SubLattice and TBLattice
                               The HB class is called SubTBLattice.
  bJoinSubTLattice d T P d' == join of BJoinSubLattice and TBLattice
                               The HB class is called BJoinSubTLattice.
  tMeetSubBLattice d T P d' == join of TMeetSubLattice and TBLattice
                               The HB class is called TMeetSubBLattice.
      bSubTLattice d T P d' == join of BSubLattice and TBLattice
                               The HB class is called BSubTLattice.
      tSubBLattice d T P d' == join of TSubLattice and TBLattice
                               The HB class is called TSubBLattice.
     tbSubBLattice d T P d' == join of BSubLattice and TSubLattice
                               The HB class is called TBSubLattice.

Morphisms between the above structures:

MeetLatticeMorphism.type d T d' T',
JoinLatticeMorphism.type d T d' T',
LatticeMorphism.type d T d' T' == nondecreasing function between two
                          lattices which are morphism for meet, join, and
                          meet/join respectively
BLatticeMorphism.type d T d' T' := {blmorphism T -> T'},
TLatticeMorphism.type d T d' T' := {tlmorphism T -> T'},
TBLatticeMorphism.type d T d' T' := {tblmorphism T -> T'}
                       == nondecreasing function between two lattices with
                          bottom/top which are morphism for bottom/top

Closedness predicates for the algebraic structures:

 meetLatticeClosed d T == predicate closed under meet on T : latticeType d
                          The HB class is MeetLatticeClosed.
 joinLatticeClosed d T == predicate closed under join on T : latticeType d
                          The HB class is JoinLatticeClosed.
     latticeClosed d T == predicate closed under meet and join
                          The HB class is JoinLatticeClosed.
    bLatticeClosed d T == predicate that contains bottom
                          The HB class is BLatticeClosed.
    tLatticeClosed d T == predicate that contains top
                          The HB class is TLatticeClosed.
   tbLatticeClosed d T == predicate that contains top and bottom
                          the HB class ie TBLatticeClosed.
bJoinLatticeClosed d T == predicate that contains bottom and is closed
                          under join
                          The HB class is BJoinLatticeClosed.
tMeetLatticeClosed d T == predicate that contains top and is closed under
                          meet
                          The HB class is TMeetLatticeClosed.

* Useful lemmas:
On orderType, leP, ltP, and 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.

* Order relations and operations:
In general, an overloaded relation or operation on ordered types takes the
following arguments:
1. a display d of type Order.disp_t,
2. an instance T of the minimal structure it operates on, and
3. operands.
Here is the exhaustive list of all such operations together with their
default notation (defined in order_scope unless specified otherwise).

For T of type meetSemilatticeType d, and x, y of type T:
        x `&` y :=  @Order.meet d T x y
                ==  the meet of x and y
For T of type joinSemilatticeType d, and x, y of type T:
        x `|` y :=  @Order.join d T x y
                ==  the join of x and y

For T of type tMeetSemilatticeType d:
\meet_<range> e :=  \big[Order.meet / Order.top]_<range> e
                ==  iterated meet of a meet-semilattice with a top
                    the possible <range>s are documented in bigop.v
For T of type bJoinSemilatticeType d:
\join_<range> e :=  \big[Order.join / Order.bottom]_<range> e
                ==  iterated join of a join-semilattice with a bottom
                    the possible <range>s are documented in bigop.v

For T of type cDistrLatticeType d, and x, y, z of type T:
   rcompl x y z == the (relative) complement of z in [x, y]

For T of type cbDistrLatticeType d, and x, y of type T:
        x `\` y := @Order.diff d T x y
                == the (sectional) complement of y in [\bot, x],
                   i.e., rcompl \bot x y

For T of type ctDistrLatticeType d, and x, y of type T:
     codiff x y == the (dual sectional) complement of y in [x, \top],
                   i.e., rcompl x \top y

For T of type ctbDistrLatticeType d, and x of type T:
           ~` x := @Order.compl d T x
                == the complement of x in [\bot, \top],
                   i.e., rcompl \bot \top x

We provide aliases for various types and their displays:
           natdvd := nat (associated with display dvd_display)
                  == an alias for nat which is canonically ordered using
                     divisibility predicate dvdn
                     Notation %|, %<|, gcd, lcm are used instead of
                     <=, <, meet and join.
             T^d  := dual T,
                     where dual is a new definition for (fun T => T)
                     (associated with dual_display d where d is a display)
                  == an alias for T, such that if T is canonically
                     ordered, then T^d is canonically ordered with the
                     dual order, and displayed with an extra ^d in the
                     notation, i.e.,  <=^d, <^d, >=<^d, ><^d, `&`^d, `|`^d
                     are used and displayed instead of
                     <=, <, >=<, ><, `&`, `|`
    T *prod[d] T' := T * T'
                  == an alias for the cartesian product such that,
                     if T and T' are canonically ordered,
                     then T *prod[d] T' is canonically ordered in product
                     order, i.e.,
                     (x1, x2) <= (y1, y2) = (x1 <= y1) && (x2 <= y2),
                     and displayed in display d
          T *p T' := T *prod[prod_display d d'] T'
                     where d and d' are the displays of T and T',
                     respectively, and prod_display adds an extra ^p to
                     all notations
    T *lexi[d] T' := T * T'
                  == an alias for the cartesian product such that,
                     if T and T' are canonically ordered,
                     then T *lexi[d] T' is canonically ordered in
                     lexicographic order,
                     i.e., (x1, x2) <= (y1, y2) =
                             (x1 <= y1) && ((x1 >= y1) ==> (x2 <= y2))
                     and   (x1, x2) < (y1, y2) =
                             (x1 <= y1) && ((x1 >= y1) ==> (x2 < y2))
                     and displayed in display d
          T *l T' := T *lexi[lexi_display d d'] T'
                     where d and d' are the displays of T and T',
                     respectively, and lexi_display adds an extra ^l to
                     all notations
 seqprod_with d T := seq T
                  == an alias for seq, such that if T is canonically
                     ordered, then seqprod_with d T is canonically ordered
                     in product order, i.e.,
                     [:: x1, .., xn] <= [y1, .., yn] =
                       (x1 <= y1) && ... && (xn <= yn)
                     and displayed in display d
n.-tupleprod[d] T == same with n.tuple T
        seqprod T := seqprod_with (seqprod_display d) T
                     where d is the display of T, and seqprod_display adds
                     an extra ^sp to all notations
   n.-tupleprod T := n.-tuple[seqprod_display d] T
                     where d is the display of T
 seqlexi_with d T := seq T
                  == an alias for seq, such that if T is canonically
                     ordered, then seqprod_with d T is canonically ordered
                     in lexicographic order, i.e.,
                     [:: x1, .., xn] <= [y1, .., yn] =
                       (x1 <= x2) && ((x1 >= y1) ==> ((x2 <= y2) && ...))
                     and displayed in display d
n.-tuplelexi[d] T == same with n.tuple T
        seqlexi T := lexiprod_with (seqlexi_display d) T
                     where d is the display of T, and seqlexi_display adds
                     an extra ^sl to all notations
   n.-tuplelexi T := n.-tuple[seqlexi_display d] T
                     where d is the display of T
    {subset[d] T} := {set T}
                  == an alias for set which is canonically ordered by the
                     subset order and displayed in display d
       {subset T} := {subset[subset_display] T}

The following notations are provided to build substructures:
[SubChoice_isSubPOrder of U by <: with disp] ==
[SubChoice_isSubPOrder of U by <:] == porderType mixin for a subType
                         whose base type is a porderType
[SubPOrder_isSubLattice of U by <: with disp] ==
[SubPOrder_isSubLattice of U by <:] ==
[SubChoice_isSubLattice of U by <: with disp] ==
[SubChoice_isSubLattice of U by <:] == latticeType mixin for a subType
                         whose base type is a latticeType and whose
                         predicate is a latticeClosed
[SubPOrder_isBSubLattice of U by <: with disp] ==
[SubPOrder_isBSubLattice of U by <:] ==
[SubChoice_isBSubLattice of U by <: with disp] ==
[SubChoice_isBSubLattice of U by <:] == blatticeType mixin for a subType
                         whose base type is a blatticeType and whose
                         predicate is both a latticeClosed
                         and a bLatticeClosed
[SubPOrder_isTSubLattice of U by <: with disp] ==
[SubPOrder_isTSubLattice of U by <:] ==
[SubChoice_isTSubLattice of U by <: with disp] ==
[SubChoice_isTSubLattice of U by <:] == tlatticeType mixin for a subType
                         whose base type is a tlatticeType and whose
                         predicate is both a latticeClosed
                         and a tLatticeClosed
[SubPOrder_isTBSubLattice of U by <: with disp] ==
[SubPOrder_isTBSubLattice of U by <:] ==
[SubChoice_isTBSubLattice of U by <: with disp] ==
[SubChoice_isTBSubLattice of U by <:] == tblatticeType mixin for a subType
                         whose base type is a tblatticeType and whose
                         predicate is both a latticeClosed
                         and a tbLatticeClosed
[SubLattice_isSubOrder of U by <: with disp] ==
[SubLattice_isSubOrder of U by <:] ==
[SubPOrder_isSubOrder of U by <: with disp] ==
[SubPOrder_isSubOrder of U by <:] ==
[SubChoice_isSubOrder of U by <: with disp] ==
[SubChoice_isSubOrder of U by <:] == orderType mixin for a subType whose
                         base type is an orderType
  [POrder of U by <:] == porderType mixin for a subType whose base type is
                         a porderType
   [Order of U by <:] == orderType mixin for a subType whose base type is
                         an orderType

We provide expected instances of ordered types for bool, nat (for leq and
and dvdn), 'I_n, 'I_n.+1 (with a top and bottom), nat for dvdn,
T *prod[disp] T', T *lexi[disp] T', {t : T & T' x} (with lexicographic
ordering), seqprod_with d T (using product order), seqlexi_with d T
(with lexicographic ordering), n.-tupleprod[disp] (using product order),
n.-tuplelexi[d] T (with lexicographic ordering), on {subset[disp] T}
(using subset order) and all possible finite type instances.
(Use `HB.about type` to discover the instances on type.)

In order to get a canonical order on prod, seq, tuple or set, one may
import modules DefaultProdOrder or DefaultProdLexiOrder,
DefaultSeqProdOrder or DefaultSeqLexiOrder,
DefaultTupleProdOrder or DefaultTupleLexiOrder,
and DefaultSetSubsetOrder.

We also provide specialized versions of some theorems from path.v.

We provide Order.enum_val, Order.enum_rank, and Order.enum_rank_in, which
are monotonic variations of enum_val, enum_rank, and enum_rank_in
whenever the type is porderType, and their monotonicity is provided if
this order is total. The theory is in the module Order (Order.enum_valK,
Order.enum_rank_inK, etc) but Order.Enum can be imported to shorten these.

We provide an opaque monotonous bijection tagnat.sig / tagnat.rank between
the finite types {i : 'I_n & 'I_(p_ i)} and 'I_(\sum_i p_ i):
 tagnat.sig  : 'I_(\sum_i p_ i) -> {i : 'I_n & 'I_(p_ i)}
 tagnat.rank : {i : 'I_n & 'I_(p_ i)} -> 'I_(\sum_i p_ i)
 tagnat.sig1 : 'I_(\sum_i p_ i) -> 'I_n
 tagnat.sig2 : forall p : 'I_(\sum_i p_ i), 'I_(p_ (tagnat.sig1 p))
 tagnat.Rank : forall i, 'I_(p_ i) -> 'I_(\sum_i p_ i)

Acknowledgments: This file is based on prior work by D. Dreyer, G.
Gonthier, A. Nanevski, P-Y Strub, B. Ziliani

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Declare Scope order_scope.

Delimit Scope order_scope with O.
Local Open Scope order_scope.

Reserved Notation "A `&` B" (at level 48, left associativity).
Reserved Notation "A `|` B" (at level 52, left associativity).
Reserved Notation "A `\` B" (at level 50, left associativity).
Reserved Notation "~` A" (at level 35, right associativity).

Reserved Notation "A `&^d` B" (at level 48, left associativity).
Reserved Notation "A `|^d` B" (at level 52, left associativity).
Reserved Notation "A `\^d` B" (at level 50, left associativity).
Reserved Notation "~^d` A" (at level 35, right associativity).

Reserved Notation "A `&^p` B" (at level 48, left associativity).
Reserved Notation "A `|^p` B" (at level 52, left associativity).
Reserved Notation "A `\^p` B" (at level 50, left associativity).
Reserved Notation "~^p` A" (at level 35, right associativity).

Reserved Notation "A `&^sp` B" (at level 48, left associativity).
Reserved Notation "A `|^sp` B" (at level 52, left associativity).
Reserved Notation "A `\^sp` B" (at level 50, left associativity).
Reserved Notation "~^sp` A" (at level 35, right associativity).

Reserved Notation "A `&^l` B" (at level 48, left associativity).
Reserved Notation "A `|^l` B" (at level 52, left associativity).
Reserved Notation "A `\^l` B" (at level 50, left associativity).
Reserved Notation "~^l` A" (at level 35, right associativity).

Reserved Notation "A `&^sl` B" (at level 48, left associativity).
Reserved Notation "A `|^sl` B" (at level 52, left associativity).
Reserved Notation "A `\^sl` B" (at level 50, left associativity).
Reserved Notation "~^sl` A" (at level 35, right associativity).

Reserved Notation "\gcd_ i F"
  (at level 34, F at level 41, i at level 0,
           format "'[' \gcd_ i '/ ' F ']'").
Reserved Notation "\gcd_ ( i <- r | P ) F"
  (at level 34, F at level 41, i, r at level 60,
           format "'[' \gcd_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\gcd_ ( i <- r ) F"
  (F at level 41,
           format "'[' \gcd_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\gcd_ ( m <= i < n | P ) F"
  (F at level 41, i, n at level 60,
           format "'[' \gcd_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\gcd_ ( m <= i < n ) F"
  (F at level 41,
           format "'[' \gcd_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\gcd_ ( i | P ) F"
  (F at level 41,
           format "'[' \gcd_ ( i | P ) '/ ' F ']'").
Reserved Notation "\gcd_ ( i : t | P ) F" (F at level 41).
Reserved Notation "\gcd_ ( i : t ) F" (F at level 41).
Reserved Notation "\gcd_ ( i < n | P ) F"
  (F at level 41, n at level 60,
           format "'[' \gcd_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\gcd_ ( i < n ) F"
  (F at level 41,
           format "'[' \gcd_ ( i < n ) F ']'").
Reserved Notation "\gcd_ ( i 'in' A | P ) F"
  (F at level 41, A at level 60,
           format "'[' \gcd_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\gcd_ ( i 'in' A ) F"
  (F at level 41,
           format "'[' \gcd_ ( i 'in' A ) '/ ' F ']'").

Reserved Notation "\lcm_ i F"
  (at level 34, F at level 41, i at level 0,
           format "'[' \lcm_ i '/ ' F ']'").
Reserved Notation "\lcm_ ( i <- r | P ) F"
  (at level 34, F at level 41, i, r at level 60,
           format "'[' \lcm_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\lcm_ ( i <- r ) F"
  (F at level 41,
           format "'[' \lcm_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\lcm_ ( m <= i < n | P ) F"
  (F at level 41, i, n at level 60,
           format "'[' \lcm_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\lcm_ ( m <= i < n ) F"
  (F at level 41,
           format "'[' \lcm_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\lcm_ ( i | P ) F"
  (F at level 41,
           format "'[' \lcm_ ( i | P ) '/ ' F ']'").
Reserved Notation "\lcm_ ( i : t | P ) F" (F at level 41).
Reserved Notation "\lcm_ ( i : t ) F" (F at level 41).
Reserved Notation "\lcm_ ( i < n | P ) F"
  (F at level 41, n at level 60,
           format "'[' \lcm_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\lcm_ ( i < n ) F"
  (F at level 41,
           format "'[' \lcm_ ( i < n ) F ']'").
Reserved Notation "\lcm_ ( i 'in' A | P ) F"
  (F at level 41, A at level 60,
           format "'[' \lcm_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\lcm_ ( i 'in' A ) F"
  (F at level 41,
           format "'[' \lcm_ ( i 'in' A ) '/ ' F ']'").

Reserved Notation "\meet_ i F"
  (at level 34, F at level 41, i at level 0,
           format "'[' \meet_ i '/ ' F ']'").
Reserved Notation "\meet_ ( i <- r | P ) F"
  (at level 34, F at level 41, i, r at level 60,
           format "'[' \meet_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\meet_ ( i <- r ) F"
  (F at level 41,
           format "'[' \meet_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\meet_ ( m <= i < n | P ) F"
  (F at level 41, i, n at level 60,
           format "'[' \meet_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\meet_ ( m <= i < n ) F"
  (F at level 41,
           format "'[' \meet_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\meet_ ( i | P ) F"
  (F at level 41,
           format "'[' \meet_ ( i | P ) '/ ' F ']'").
Reserved Notation "\meet_ ( i : t | P ) F" (F at level 41).
Reserved Notation "\meet_ ( i : t ) F" (F at level 41).
Reserved Notation "\meet_ ( i < n | P ) F"
  (F at level 41, n at level 60,
           format "'[' \meet_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\meet_ ( i < n ) F"
  (F at level 41,
           format "'[' \meet_ ( i < n ) F ']'").
Reserved Notation "\meet_ ( i 'in' A | P ) F"
  (F at level 41, A at level 60,
           format "'[' \meet_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\meet_ ( i 'in' A ) F"
  (F at level 41,
           format "'[' \meet_ ( i 'in' A ) '/ ' F ']'").

Reserved Notation "\join_ i F"
  (at level 34, F at level 41, i at level 0,
           format "'[' \join_ i '/ ' F ']'").
Reserved Notation "\join_ ( i <- r | P ) F"
  (at level 34, F at level 41, i, r at level 60,
           format "'[' \join_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\join_ ( i <- r ) F"
  (F at level 41,
           format "'[' \join_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\join_ ( m <= i < n | P ) F"
  (F at level 41, i, n at level 60,
           format "'[' \join_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\join_ ( m <= i < n ) F"
  (F at level 41,
           format "'[' \join_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\join_ ( i | P ) F"
  (F at level 41,
           format "'[' \join_ ( i | P ) '/ ' F ']'").
Reserved Notation "\join_ ( i : t | P ) F" (F at level 41).
Reserved Notation "\join_ ( i : t ) F" (F at level 41).
Reserved Notation "\join_ ( i < n | P ) F"
  (F at level 41, n at level 60,
           format "'[' \join_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\join_ ( i < n ) F"
  (F at level 41,
           format "'[' \join_ ( i < n ) F ']'").
Reserved Notation "\join_ ( i 'in' A | P ) F"
  (F at level 41, A at level 60,
           format "'[' \join_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\join_ ( i 'in' A ) F"
  (F at level 41,
           format "'[' \join_ ( i 'in' A ) '/ ' F ']'").

Reserved Notation "\meet^d_ i F"
  (at level 34, F at level 41, i at level 0,
           format "'[' \meet^d_ i '/ ' F ']'").
Reserved Notation "\meet^d_ ( i <- r | P ) F"
  (at level 34, F at level 41, i, r at level 60,
           format "'[' \meet^d_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\meet^d_ ( i <- r ) F"
  (F at level 41,
           format "'[' \meet^d_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\meet^d_ ( m <= i < n | P ) F"
  (F at level 41, i, n at level 60,
           format "'[' \meet^d_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\meet^d_ ( m <= i < n ) F"
  (F at level 41,
           format "'[' \meet^d_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\meet^d_ ( i | P ) F"
  (F at level 41,
           format "'[' \meet^d_ ( i | P ) '/ ' F ']'").
Reserved Notation "\meet^d_ ( i : t | P ) F" (F at level 41).
Reserved Notation "\meet^d_ ( i : t ) F" (F at level 41).
Reserved Notation "\meet^d_ ( i < n | P ) F"
  (F at level 41, n at level 60,
           format "'[' \meet^d_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\meet^d_ ( i < n ) F"
  (F at level 41,
           format "'[' \meet^d_ ( i < n ) F ']'").
Reserved Notation "\meet^d_ ( i 'in' A | P ) F"
  (F at level 41, A at level 60,
           format "'[' \meet^d_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\meet^d_ ( i 'in' A ) F"
  (F at level 41,
           format "'[' \meet^d_ ( i 'in' A ) '/ ' F ']'").

Reserved Notation "\join^d_ i F"
  (at level 34, F at level 41, i at level 0,
           format "'[' \join^d_ i '/ ' F ']'").
Reserved Notation "\join^d_ ( i <- r | P ) F"
  (at level 34, F at level 41, i, r at level 60,
           format "'[' \join^d_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\join^d_ ( i <- r ) F"
  (F at level 41,
           format "'[' \join^d_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\join^d_ ( m <= i < n | P ) F"
  (F at level 41, i, n at level 60,
           format "'[' \join^d_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\join^d_ ( m <= i < n ) F"
  (F at level 41,
           format "'[' \join^d_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\join^d_ ( i | P ) F"
  (F at level 41,
           format "'[' \join^d_ ( i | P ) '/ ' F ']'").
Reserved Notation "\join^d_ ( i : t | P ) F" (F at level 41).
Reserved Notation "\join^d_ ( i : t ) F" (F at level 41).
Reserved Notation "\join^d_ ( i < n | P ) F"
  (F at level 41, n at level 60,
           format "'[' \join^d_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\join^d_ ( i < n ) F"
  (F at level 41,
           format "'[' \join^d_ ( i < n ) F ']'").
Reserved Notation "\join^d_ ( i 'in' A | P ) F"
  (F at level 41, A at level 60,
           format "'[' \join^d_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\join^d_ ( i 'in' A ) F"
  (F at level 41,
           format "'[' \join^d_ ( i 'in' A ) '/ ' F ']'").

Reserved Notation "\meet^p_ i F"
  (at level 34, F at level 41, i at level 0,
           format "'[' \meet^p_ i '/ ' F ']'").
Reserved Notation "\meet^p_ ( i <- r | P ) F"
  (at level 34, F at level 41, i, r at level 60,
           format "'[' \meet^p_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\meet^p_ ( i <- r ) F"
  (F at level 41,
           format "'[' \meet^p_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\meet^p_ ( m <= i < n | P ) F"
  (F at level 41, i, n at level 60,
           format "'[' \meet^p_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\meet^p_ ( m <= i < n ) F"
  (F at level 41,
           format "'[' \meet^p_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\meet^p_ ( i | P ) F"
  (F at level 41,
           format "'[' \meet^p_ ( i | P ) '/ ' F ']'").
Reserved Notation "\meet^p_ ( i : t | P ) F" (F at level 41).
Reserved Notation "\meet^p_ ( i : t ) F" (F at level 41).
Reserved Notation "\meet^p_ ( i < n | P ) F"
  (F at level 41, n at level 60,
           format "'[' \meet^p_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\meet^p_ ( i < n ) F"
  (F at level 41,
           format "'[' \meet^p_ ( i < n ) F ']'").
Reserved Notation "\meet^p_ ( i 'in' A | P ) F"
  (F at level 41, A at level 60,
           format "'[' \meet^p_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\meet^p_ ( i 'in' A ) F"
  (F at level 41,
           format "'[' \meet^p_ ( i 'in' A ) '/ ' F ']'").

Reserved Notation "\join^p_ i F"
  (at level 34, F at level 41, i at level 0,
           format "'[' \join^p_ i '/ ' F ']'").
Reserved Notation "\join^p_ ( i <- r | P ) F"
  (at level 34, F at level 41, i, r at level 60,
           format "'[' \join^p_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\join^p_ ( i <- r ) F"
  (F at level 41,
           format "'[' \join^p_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\join^p_ ( m <= i < n | P ) F"
  (F at level 41, i, n at level 60,
           format "'[' \join^p_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\join^p_ ( m <= i < n ) F"
  (F at level 41,
           format "'[' \join^p_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\join^p_ ( i | P ) F"
  (F at level 41,
           format "'[' \join^p_ ( i | P ) '/ ' F ']'").
Reserved Notation "\join^p_ ( i : t | P ) F" (F at level 41).
Reserved Notation "\join^p_ ( i : t ) F" (F at level 41).
Reserved Notation "\join^p_ ( i < n | P ) F"
  (F at level 41, n at level 60,
           format "'[' \join^p_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\join^p_ ( i < n ) F"
  (F at level 41,
           format "'[' \join^p_ ( i < n ) F ']'").
Reserved Notation "\join^p_ ( i 'in' A | P ) F"
  (F at level 41, A at level 60,
           format "'[' \join^p_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\join^p_ ( i 'in' A ) F"
  (F at level 41,
           format "'[' \join^p_ ( i 'in' A ) '/ ' F ']'").

Reserved Notation "\min^p_ i F"
  (at level 34, F at level 41, i at level 0,
           format "'[' \min^p_ i '/ ' F ']'").
Reserved Notation "\min^p_ ( i <- r | P ) F"
  (at level 34, F at level 41, i, r at level 60,
           format "'[' \min^p_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\min^p_ ( i <- r ) F"
  (F at level 41,
           format "'[' \min^p_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\min^p_ ( m <= i < n | P ) F"
  (F at level 41, i, n at level 60,
           format "'[' \min^p_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\min^p_ ( m <= i < n ) F"
  (F at level 41,
           format "'[' \min^p_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\min^p_ ( i | P ) F"
  (F at level 41,
           format "'[' \min^p_ ( i | P ) '/ ' F ']'").
Reserved Notation "\min^p_ ( i : t | P ) F" (F at level 41).
Reserved Notation "\min^p_ ( i : t ) F" (F at level 41).
Reserved Notation "\min^p_ ( i < n | P ) F"
  (F at level 41, n at level 60,
           format "'[' \min^p_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\min^p_ ( i < n ) F"
  (F at level 41,
           format "'[' \min^p_ ( i < n ) F ']'").
Reserved Notation "\min^p_ ( i 'in' A | P ) F"
  (F at level 41, A at level 60,
           format "'[' \min^p_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\min^p_ ( i 'in' A ) F"
  (F at level 41,
           format "'[' \min^p_ ( i 'in' A ) '/ ' F ']'").

Reserved Notation "\max^p_ i F"
  (at level 34, F at level 41, i at level 0,
           format "'[' \max^p_ i '/ ' F ']'").
Reserved Notation "\max^p_ ( i <- r | P ) F"
  (at level 34, F at level 41, i, r at level 60,
           format "'[' \max^p_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\max^p_ ( i <- r ) F"
  (F at level 41,
           format "'[' \max^p_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\max^p_ ( m <= i < n | P ) F"
  (F at level 41, i, n at level 60,
           format "'[' \max^p_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\max^p_ ( m <= i < n ) F"
  (F at level 41,
           format "'[' \max^p_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\max^p_ ( i | P ) F"
  (F at level 41,
           format "'[' \max^p_ ( i | P ) '/ ' F ']'").
Reserved Notation "\max^p_ ( i : t | P ) F" (F at level 41).
Reserved Notation "\max^p_ ( i : t ) F" (F at level 41).
Reserved Notation "\max^p_ ( i < n | P ) F"
  (F at level 41, n at level 60,
           format "'[' \max^p_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\max^p_ ( i < n ) F"
  (F at level 41,
           format "'[' \max^p_ ( i < n ) F ']'").
Reserved Notation "\max^p_ ( i 'in' A | P ) F"
  (F at level 41, A at level 60,
           format "'[' \max^p_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\max^p_ ( i 'in' A ) F"
  (F at level 41,
           format "'[' \max^p_ ( i 'in' A ) '/ ' F ']'").

Reserved Notation "\meet^sp_ i F"
  (at level 34, F at level 41, i at level 0,
           format "'[' \meet^sp_ i '/ ' F ']'").
Reserved Notation "\meet^sp_ ( i <- r | P ) F"
  (at level 34, F at level 41, i, r at level 60,
           format "'[' \meet^sp_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\meet^sp_ ( i <- r ) F"
  (F at level 41,
           format "'[' \meet^sp_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\meet^sp_ ( m <= i < n | P ) F"
  (F at level 41, i, n at level 60,
           format "'[' \meet^sp_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\meet^sp_ ( m <= i < n ) F"
  (F at level 41,
           format "'[' \meet^sp_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\meet^sp_ ( i | P ) F"
  (F at level 41,
           format "'[' \meet^sp_ ( i | P ) '/ ' F ']'").
Reserved Notation "\meet^sp_ ( i : t | P ) F" (F at level 41).
Reserved Notation "\meet^sp_ ( i : t ) F" (F at level 41).
Reserved Notation "\meet^sp_ ( i < n | P ) F"
  (F at level 41, n at level 60,
           format "'[' \meet^sp_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\meet^sp_ ( i < n ) F"
  (F at level 41,
           format "'[' \meet^sp_ ( i < n ) F ']'").
Reserved Notation "\meet^sp_ ( i 'in' A | P ) F"
  (F at level 41, A at level 60,
           format "'[' \meet^sp_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\meet^sp_ ( i 'in' A ) F"
  (F at level 41,
           format "'[' \meet^sp_ ( i 'in' A ) '/ ' F ']'").

Reserved Notation "\join^sp_ i F"
  (at level 34, F at level 41, i at level 0,
           format "'[' \join^sp_ i '/ ' F ']'").
Reserved Notation "\join^sp_ ( i <- r | P ) F"
  (at level 34, F at level 41, i, r at level 60,
           format "'[' \join^sp_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\join^sp_ ( i <- r ) F"
  (F at level 41,
           format "'[' \join^sp_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\join^sp_ ( m <= i < n | P ) F"
  (F at level 41, i, n at level 60,
           format "'[' \join^sp_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\join^sp_ ( m <= i < n ) F"
  (F at level 41,
           format "'[' \join^sp_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\join^sp_ ( i | P ) F"
  (F at level 41,
           format "'[' \join^sp_ ( i | P ) '/ ' F ']'").
Reserved Notation "\join^sp_ ( i : t | P ) F" (F at level 41).
Reserved Notation "\join^sp_ ( i : t ) F" (F at level 41).
Reserved Notation "\join^sp_ ( i < n | P ) F"
  (F at level 41, n at level 60,
           format "'[' \join^sp_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\join^sp_ ( i < n ) F"
  (F at level 41,
           format "'[' \join^sp_ ( i < n ) F ']'").
Reserved Notation "\join^sp_ ( i 'in' A | P ) F"
  (F at level 41, A at level 60,
           format "'[' \join^sp_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\join^sp_ ( i 'in' A ) F"
  (F at level 41,
           format "'[' \join^sp_ ( i 'in' A ) '/ ' F ']'").

Reserved Notation "\min^sp_ i F"
  (at level 34, F at level 41, i at level 0,
           format "'[' \min^sp_ i '/ ' F ']'").
Reserved Notation "\min^sp_ ( i <- r | P ) F"
  (at level 34, F at level 41, i, r at level 60,
           format "'[' \min^sp_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\min^sp_ ( i <- r ) F"
  (F at level 41,
           format "'[' \min^sp_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\min^sp_ ( m <= i < n | P ) F"
  (F at level 41, i, n at level 60,
           format "'[' \min^sp_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\min^sp_ ( m <= i < n ) F"
  (F at level 41,
           format "'[' \min^sp_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\min^sp_ ( i | P ) F"
  (F at level 41,
           format "'[' \min^sp_ ( i | P ) '/ ' F ']'").
Reserved Notation "\min^sp_ ( i : t | P ) F" (F at level 41).
Reserved Notation "\min^sp_ ( i : t ) F" (F at level 41).
Reserved Notation "\min^sp_ ( i < n | P ) F"
  (F at level 41, n at level 60,
           format "'[' \min^sp_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\min^sp_ ( i < n ) F"
  (F at level 41,
           format "'[' \min^sp_ ( i < n ) F ']'").
Reserved Notation "\min^sp_ ( i 'in' A | P ) F"
  (F at level 41, A at level 60,
           format "'[' \min^sp_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\min^sp_ ( i 'in' A ) F"
  (F at level 41,
           format "'[' \min^sp_ ( i 'in' A ) '/ ' F ']'").

Reserved Notation "\max^sp_ i F"
  (at level 34, F at level 41, i at level 0,
           format "'[' \max^sp_ i '/ ' F ']'").
Reserved Notation "\max^sp_ ( i <- r | P ) F"
  (at level 34, F at level 41, i, r at level 60,
           format "'[' \max^sp_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\max^sp_ ( i <- r ) F"
  (F at level 41,
           format "'[' \max^sp_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\max^sp_ ( m <= i < n | P ) F"
  (F at level 41, i, n at level 60,
           format "'[' \max^sp_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\max^sp_ ( m <= i < n ) F"
  (F at level 41,
           format "'[' \max^sp_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\max^sp_ ( i | P ) F"
  (F at level 41,
           format "'[' \max^sp_ ( i | P ) '/ ' F ']'").
Reserved Notation "\max^sp_ ( i : t | P ) F" (F at level 41).
Reserved Notation "\max^sp_ ( i : t ) F" (F at level 41).
Reserved Notation "\max^sp_ ( i < n | P ) F"
  (F at level 41, n at level 60,
           format "'[' \max^sp_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\max^sp_ ( i < n ) F"
  (F at level 41,
           format "'[' \max^sp_ ( i < n ) F ']'").
Reserved Notation "\max^sp_ ( i 'in' A | P ) F"
  (F at level 41, A at level 60,
           format "'[' \max^sp_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\max^sp_ ( i 'in' A ) F"
  (F at level 41,
           format "'[' \max^sp_ ( i 'in' A ) '/ ' F ']'").

Reserved Notation "\meet^l_ i F"
  (at level 34, F at level 41, i at level 0,
           format "'[' \meet^l_ i '/ ' F ']'").
Reserved Notation "\meet^l_ ( i <- r | P ) F"
  (at level 34, F at level 41, i, r at level 60,
           format "'[' \meet^l_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\meet^l_ ( i <- r ) F"
  (F at level 41,
           format "'[' \meet^l_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\meet^l_ ( m <= i < n | P ) F"
  (F at level 41, i, n at level 60,
           format "'[' \meet^l_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\meet^l_ ( m <= i < n ) F"
  (F at level 41,
           format "'[' \meet^l_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\meet^l_ ( i | P ) F"
  (F at level 41,
           format "'[' \meet^l_ ( i | P ) '/ ' F ']'").
Reserved Notation "\meet^l_ ( i : t | P ) F" (F at level 41).
Reserved Notation "\meet^l_ ( i : t ) F" (F at level 41).
Reserved Notation "\meet^l_ ( i < n | P ) F"
  (F at level 41, n at level 60,
           format "'[' \meet^l_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\meet^l_ ( i < n ) F"
  (F at level 41,
           format "'[' \meet^l_ ( i < n ) F ']'").
Reserved Notation "\meet^l_ ( i 'in' A | P ) F"
  (F at level 41, A at level 60,
           format "'[' \meet^l_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\meet^l_ ( i 'in' A ) F"
  (F at level 41,
           format "'[' \meet^l_ ( i 'in' A ) '/ ' F ']'").

Reserved Notation "\join^l_ i F"
  (at level 34, F at level 41, i at level 0,
           format "'[' \join^l_ i '/ ' F ']'").
Reserved Notation "\join^l_ ( i <- r | P ) F"
  (at level 34, F at level 41, i, r at level 60,
           format "'[' \join^l_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\join^l_ ( i <- r ) F"
  (F at level 41,
           format "'[' \join^l_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\join^l_ ( m <= i < n | P ) F"
  (F at level 41, i, n at level 60,
           format "'[' \join^l_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\join^l_ ( m <= i < n ) F"
  (F at level 41,
           format "'[' \join^l_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\join^l_ ( i | P ) F"
  (F at level 41,
           format "'[' \join^l_ ( i | P ) '/ ' F ']'").
Reserved Notation "\join^l_ ( i : t | P ) F" (F at level 41).
Reserved Notation "\join^l_ ( i : t ) F" (F at level 41).
Reserved Notation "\join^l_ ( i < n | P ) F"
  (F at level 41, n at level 60,
           format "'[' \join^l_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\join^l_ ( i < n ) F"
  (F at level 41,
           format "'[' \join^l_ ( i < n ) F ']'").
Reserved Notation "\join^l_ ( i 'in' A | P ) F"
  (F at level 41, A at level 60,
           format "'[' \join^l_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\join^l_ ( i 'in' A ) F"
  (F at level 41,
           format "'[' \join^l_ ( i 'in' A ) '/ ' F ']'").

Reserved Notation "\min^l_ i F"
  (at level 34, F at level 41, i at level 0,
           format "'[' \min^l_ i '/ ' F ']'").
Reserved Notation "\min^l_ ( i <- r | P ) F"
  (at level 34, F at level 41, i, r at level 60,
           format "'[' \min^l_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\min^l_ ( i <- r ) F"
  (F at level 41,
           format "'[' \min^l_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\min^l_ ( m <= i < n | P ) F"
  (F at level 41, i, n at level 60,
           format "'[' \min^l_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\min^l_ ( m <= i < n ) F"
  (F at level 41,
           format "'[' \min^l_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\min^l_ ( i | P ) F"
  (F at level 41,
           format "'[' \min^l_ ( i | P ) '/ ' F ']'").
Reserved Notation "\min^l_ ( i : t | P ) F" (F at level 41).
Reserved Notation "\min^l_ ( i : t ) F" (F at level 41).
Reserved Notation "\min^l_ ( i < n | P ) F"
  (F at level 41, n at level 60,
           format "'[' \min^l_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\min^l_ ( i < n ) F"
  (F at level 41,
           format "'[' \min^l_ ( i < n ) F ']'").
Reserved Notation "\min^l_ ( i 'in' A | P ) F"
  (F at level 41, A at level 60,
           format "'[' \min^l_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\min^l_ ( i 'in' A ) F"
  (F at level 41,
           format "'[' \min^l_ ( i 'in' A ) '/ ' F ']'").

Reserved Notation "\max^l_ i F"
  (at level 34, F at level 41, i at level 0,
           format "'[' \max^l_ i '/ ' F ']'").
Reserved Notation "\max^l_ ( i <- r | P ) F"
  (at level 34, F at level 41, i, r at level 60,
           format "'[' \max^l_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\max^l_ ( i <- r ) F"
  (F at level 41,
           format "'[' \max^l_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\max^l_ ( m <= i < n | P ) F"
  (F at level 41, i, n at level 60,
           format "'[' \max^l_ ( m <= i < n | P ) '/ ' F ']'").
Reserved Notation "\max^l_ ( m <= i < n ) F"
  (F at level 41,
           format "'[' \max^l_ ( m <= i < n ) '/ ' F ']'").
Reserved Notation "\max^l_ ( i | P ) F"
  (F at level 41,
           format "'[' \max^l_ ( i | P ) '/ ' F ']'").
Reserved Notation "\max^l_ ( i : t | P ) F" (F at level 41).
Reserved Notation "\max^l_ ( i : t ) F" (F at level 41).
Reserved Notation "\max^l_ ( i < n | P ) F"
  (F at level 41, n at level 60,
           format "'[' \max^l_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\max^l_ ( i < n ) F"
  (F at level 41,
           format "'[' \max^l_ ( i < n ) F ']'").
Reserved Notation "\max^l_ ( i 'in' A | P ) F"
  (F at level 41, A at level 60,
           format "'[' \max^l_ ( i 'in' A | P ) '/ ' F ']'").
Reserved Notation "\max^l_ ( i 'in' A ) F"
  (F at level 41,
           format "'[' \max^l_ ( i 'in' A ) '/ ' F ']'").

Reserved Notation "'{' 'omorphism' U '->' V '}'"
  (U at level 98, V at level 99, format "{ 'omorphism' U -> V }").
Reserved Notation "'{' 'mlmorphism' U '->' V '}'"
  (U at level 98, V at level 99, format "{ 'mlmorphism' U -> V }").
Reserved Notation "'{' 'jlmorphism' U '->' V '}'"
  (U at level 98, V at level 99, format "{ 'jlmorphism' U -> V }").
Reserved Notation "'{' 'lmorphism' U '->' V '}'"
  (U at level 98, V at level 99, format "{ 'lmorphism' U -> V }").
Reserved Notation "'{' 'blmorphism' U '->' V '}'"
  (U at level 98, V at level 99, format "{ 'blmorphism' U -> V }").
Reserved Notation "'{' 'tlmorphism' U '->' V '}'"
  (U at level 98, V at level 99, format "{ 'tlmorphism' U -> V }").
Reserved Notation "'{' 'tblmorphism' U '->' V '}'"
  (U at level 98, V at level 99, format "{ 'tblmorphism' U -> V }").

Module Order.

Export Order.

#[key="T", primitive]
HB.mixin Record Preorder_isDuallyPOrder (d : disp_t) T & Preorder d T := {
  le_anti : antisymmetric (@le d T);
  ge_anti : antisymmetric (fun x y => @le d T y x);
}.

#[short(type="porderType")]
HB.structure Definition POrder (d : disp_t) :=
  { T of Preorder d T & Preorder_isDuallyPOrder d T }.

#[short(type="bPOrderType")]
HB.structure Definition BPOrder d := { T of hasBottom d T & POrder d T }.
#[short(type="tPOrderType")]
HB.structure Definition TPOrder d := { T of hasTop d T & POrder d T }.
#[short(type="tbPOrderType")]
HB.structure Definition TBPOrder d := { T of hasTop d T & BPOrder d T }.

Module POrderExports.
Arguments le_trans {d s} [_ _ _].
End POrderExports.
HB.export POrderExports.

#[key="T", primitive]
HB.mixin Record POrder_isMeetSemilattice d (T : Type) & POrder d T := {
  meet : T -> T -> T;
  lexI : forall x y z, (x <= meet y z) = (x <= y) && (x <= z);
}.

#[key="T", primitive]
HB.mixin Record POrder_isJoinSemilattice d T & POrder d T := {
  join : T -> T -> T;
  leUx : forall x y z, (join x y <= z) = (x <= z) && (y <= z);
}.

#[short(type="meetSemilatticeType")]
HB.structure Definition MeetSemilattice d :=
  { T of POrder d T & POrder_isMeetSemilattice d T }.

#[short(type="bMeetSemilatticeType")]
HB.structure Definition BMeetSemilattice d :=
  { T of MeetSemilattice d T & hasBottom d T }.

#[short(type="tMeetSemilatticeType")]
HB.structure Definition TMeetSemilattice d :=
  { T of MeetSemilattice d T & hasTop d T }.

#[short(type="tbMeetSemilatticeType")]
HB.structure Definition TBMeetSemilattice d :=
  { T of BMeetSemilattice d T & hasTop d T }.

#[short(type="joinSemilatticeType")]
HB.structure Definition JoinSemilattice d :=
  { T of POrder d T & POrder_isJoinSemilattice d T }.

#[short(type="bJoinSemilatticeType")]
HB.structure Definition BJoinSemilattice d :=
  { T of JoinSemilattice d T & hasBottom d T }.

#[short(type="tJoinSemilatticeType")]
HB.structure Definition TJoinSemilattice d :=
  { T of JoinSemilattice d T & hasTop d T }.

#[short(type="tbJoinSemilatticeType")]
HB.structure Definition TBJoinSemilattice d :=
  { T of BJoinSemilattice d T & hasTop d T }.

#[short(type="latticeType")]
HB.structure Definition Lattice d :=
  { T of JoinSemilattice d T & POrder_isMeetSemilattice d T }.

#[short(type="bLatticeType")]
HB.structure Definition BLattice d := { T of Lattice d T & hasBottom d T }.

#[short(type="tLatticeType")]
HB.structure Definition TLattice d := { T of Lattice d T & hasTop d T }.

#[short(type="tbLatticeType")]
HB.structure Definition TBLattice d := { T of BLattice d T & hasTop d T }.

Section LatticeDef.
Context {disp : disp_t} {T : latticeType disp}.

Variant lel_xor_gt (x y : T) :
  T -> T -> T -> T -> T -> T -> T -> T -> bool -> bool -> Set :=
  | LelNotGt of x <= y : lel_xor_gt x y x x y y x x y y true false
  | GtlNotLe of y < x : lel_xor_gt x y y y x x y y x x false true.

Variant ltl_xor_ge (x y : T) :
  T -> T -> T -> T -> T -> T -> T -> T -> bool -> bool -> Set :=
  | LtlNotGe of x < y : ltl_xor_ge x y x x y y x x y y false true
  | GelNotLt of y <= x : ltl_xor_ge x y y y x x y y x x true false.

Variant comparel (x y : T) :
   T -> T -> T -> T -> T -> T -> T -> T ->
   bool -> bool -> bool -> bool -> bool -> bool -> Set :=
  | ComparelLt of x < y : comparel x y
    x x y y x x y y false false false true false true
  | ComparelGt of y < x : comparel x y
    y y x x y y x x false false true false true false
  | ComparelEq of x = y : comparel x y
    x x x x x x x x true true true true false false.

Variant incomparel (x y : T) :
  T -> T -> T -> T -> T -> T -> T -> T ->
  bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> Set :=
  | InComparelLt of x < y : incomparel x y
    x x y y x x y y false false false true false true true true
  | InComparelGt of y < x : incomparel x y
    y y x x y y x x false false true false true false true true
  | InComparel of x >< y : incomparel x y
    x y y x (meet y x) (meet x y) (join y x) (join x y)
    false false false false false false false false
  | InComparelEq of x = y : incomparel x y
    x x x x x x x x true true true true false false true true.

End LatticeDef.

Module LatticeSyntax.

Notation "x `&` y" := (meet x y) : order_scope.
Notation "x `|` y" := (join x y) : order_scope.

End LatticeSyntax.
HB.export LatticeSyntax.

Module BLatticeSyntax.

Notation "\join_ ( i <- r | P ) F" :=
  (\big[@join _ _ / \bot]_(i <- r | P%B) F%O) : order_scope.
Notation "\join_ ( i <- r ) F" :=
  (\big[@join _ _ / \bot]_(i <- r) F%O) : order_scope.
Notation "\join_ ( i | P ) F" :=
  (\big[@join _ _ / \bot]_(i | P%B) F%O) : order_scope.
Notation "\join_ i F" :=
  (\big[@join _ _ / \bot]_i F%O) : order_scope.
Notation "\join_ ( i : I | P ) F" :=
  (\big[@join _ _ / \bot]_(i : I | P%B) F%O) (only parsing) : order_scope.
Notation "\join_ ( i : I ) F" :=
  (\big[@join _ _ / \bot]_(i : I) F%O) (only parsing) : order_scope.
Notation "\join_ ( m <= i < n | P ) F" :=
  (\big[@join _ _ / \bot]_(m <= i < n | P%B) F%O) : order_scope.
Notation "\join_ ( m <= i < n ) F" :=
  (\big[@join _ _ / \bot]_(m <= i < n) F%O) : order_scope.
Notation "\join_ ( i < n | P ) F" :=
  (\big[@join _ _ / \bot]_(i < n | P%B) F%O) : order_scope.
Notation "\join_ ( i < n ) F" :=
  (\big[@join _ _ / \bot]_(i < n) F%O) : order_scope.
Notation "\join_ ( i 'in' A | P ) F" :=
  (\big[@join _ _ / \bot]_(i in A | P%B) F%O) : order_scope.
Notation "\join_ ( i 'in' A ) F" :=
  (\big[@join _ _ / \bot]_(i in A) F%O) : order_scope.

End BLatticeSyntax.
HB.export BLatticeSyntax.

Module TLatticeSyntax.

Notation "\meet_ ( i <- r | P ) F" :=
  (\big[meet / \top]_(i <- r | P%B) F%O) : order_scope.
Notation "\meet_ ( i <- r ) F" :=
  (\big[meet / \top]_(i <- r) F%O) : order_scope.
Notation "\meet_ ( i | P ) F" :=
  (\big[meet / \top]_(i | P%B) F%O) : order_scope.
Notation "\meet_ i F" :=
  (\big[meet / \top]_i F%O) : order_scope.
Notation "\meet_ ( i : I | P ) F" :=
  (\big[meet / \top]_(i : I | P%B) F%O) (only parsing) : order_scope.
Notation "\meet_ ( i : I ) F" :=
  (\big[meet / \top]_(i : I) F%O) (only parsing) : order_scope.
Notation "\meet_ ( m <= i < n | P ) F" :=
(\big[meet / \top]_(m <= i < n | P%B) F%O) : order_scope.
Notation "\meet_ ( m <= i < n ) F" :=
(\big[meet / \top]_(m <= i < n) F%O) : order_scope.
Notation "\meet_ ( i < n | P ) F" :=
(\big[meet / \top]_(i < n | P%B) F%O) : order_scope.
Notation "\meet_ ( i < n ) F" :=
(\big[meet / \top]_(i < n) F%O) : order_scope.
Notation "\meet_ ( i 'in' A | P ) F" :=
(\big[meet / \top]_(i in A | P%B) F%O) : order_scope.
Notation "\meet_ ( i 'in' A ) F" :=
(\big[meet / \top]_(i in A) F%O) : order_scope.

End TLatticeSyntax.
HB.export TLatticeSyntax.

#[key="T", primitive]
HB.mixin Record Lattice_isDistributive d (T : Type) & Lattice d T := {
  meetUl : @left_distributive T T meet join;
  joinIl : @left_distributive T T join meet;
}.

#[short(type="distrLatticeType")]
HB.structure Definition DistrLattice d :=
  { T of Lattice_isDistributive d T & Lattice d T }.

#[short(type="bDistrLatticeType")]
HB.structure Definition BDistrLattice d :=
  { T of DistrLattice d T & hasBottom d T }.

#[short(type="tDistrLatticeType")]
HB.structure Definition TDistrLattice d :=
  { T of DistrLattice d T & hasTop d T }.

#[short(type="tbDistrLatticeType")]
HB.structure Definition TBDistrLattice d :=
  { T of BDistrLattice d T & hasTop d T }.

#[key="T", primitive]
HB.mixin Record DistrLattice_isTotal d T & DistrLattice d T :=
  { le_total : total (<=%O : rel T) }.

#[short(type="orderType")]
HB.structure Definition Total d :=
  { T of DistrLattice_isTotal d T & DistrLattice d T }.

#[short(type="bOrderType")]
HB.structure Definition BTotal d := { T of Total d T & hasBottom d T }.

#[short(type="tOrderType")]
HB.structure Definition TTotal d := { T of Total d T & hasTop d T }.

#[short(type="tbOrderType")]
HB.structure Definition TBTotal d := { T of BTotal d T & hasTop d T }.

#[key="T", primitive]
HB.mixin Record DistrLattice_hasRelativeComplement d T & DistrLattice d T := {
  rcompl : T -> T -> T -> T;
  rcomplPmeet : forall x y z, ((x `&` y) `|` z) `&` rcompl x y z = x `&` y;
  rcomplPjoin : forall x y z, ((y `|` x) `&` z) `|` rcompl x y z = y `|` x;
}.

#[short(type="cDistrLatticeType")]
HB.structure Definition CDistrLattice d :=
  { T of DistrLattice d T & DistrLattice_hasRelativeComplement d T }.

#[key="T", primitive]
HB.mixin Record CDistrLattice_hasSectionalComplement d T
         & CDistrLattice d T & hasBottom d T := {
  diff : T -> T -> T;
  diffErcompl : forall x y, diff x y = rcompl (\bot : T) x y;
}.

#[short(type="cbDistrLatticeType")]
HB.structure Definition CBDistrLattice d :=
  { T of CDistrLattice d T & hasBottom d T &
         CDistrLattice_hasSectionalComplement d T }.

#[key="T", primitive]
HB.mixin Record CDistrLattice_hasDualSectionalComplement d T
         & CDistrLattice d T & hasTop d T := {
  codiff : T -> T -> T;
  codiffErcompl : forall x y, codiff x y = rcompl x \top y;
}.

#[short(type="ctDistrLatticeType")]
HB.structure Definition CTDistrLattice d :=
  { T of CDistrLattice d T & hasTop d T &
         CDistrLattice_hasDualSectionalComplement d T }.

Module Import CBDistrLatticeSyntax.
Notation "x `\` y" := (diff x y) : order_scope.
End CBDistrLatticeSyntax.

#[key="T", primitive]
HB.mixin Record CDistrLattice_hasComplement d T &
         CTDistrLattice d T & CBDistrLattice d T := {
  compl : T -> T;
  complEdiff : forall x : T, compl x = (\top : T) `\` x;
  complEcodiff : forall x : T, compl x = codiff (\bot : T) x;
}.

#[short(type="ctbDistrLatticeType")]
HB.structure Definition CTBDistrLattice d :=
  { T of CBDistrLattice d T & CTDistrLattice d T &
         CDistrLattice_hasComplement d T }.

Module Import CTBDistrLatticeSyntax.
Notation "~` A" := (compl A) : order_scope.
End CTBDistrLatticeSyntax.

FINITE

DUAL

Proof.

by []. Qed.

HB.instance Definition _ d (T : meetSemilatticeType d) :=
POrder_isJoinSemilattice.Build (dual_display d) T^d (fun x y z => lexI z x y).

Lemma joinEdual d (T : meetSemilatticeType d) (x y : T) :
((x : T^d) `|^d` y) = (x `&` y).

Proof.

by []. Qed.

HB.saturate.

HB.instance Definition _ d (T : distrLatticeType d) :=
  Lattice_isDistributive.Build (dual_display d) T^d joinIl meetUl.

HB.instance Definition _ d (T : orderType d) :=
  DistrLattice_isTotal.Build (dual_display d) T^d (fun x y => le_total y x).

HB.saturate.

HB.instance Definition _ d (T : cDistrLatticeType d) :=
  DistrLattice_hasRelativeComplement.Build (dual_display d) T^d
    (fun x y => rcomplPjoin y x) (fun x y => rcomplPmeet y x).
HB.instance Definition _ d (T : ctDistrLatticeType d) :=
  CDistrLattice_hasSectionalComplement.Build (dual_display d) T^d codiffErcompl.
HB.instance Definition _ d (T : cbDistrLatticeType d) :=
  CDistrLattice_hasDualSectionalComplement.Build (dual_display d) T^d
    diffErcompl.
HB.instance Definition _ d (T : ctbDistrLatticeType d) :=
  CDistrLattice_hasComplement.Build (dual_display d) T^d
    complEcodiff complEdiff.

HB.saturate.

End DualOrder.
HB.export DualOrder.

THEORY

Module Import POrderTheory.

Include PreorderTheory.

Section POrderTheory.

Context {disp : disp_t} {T : porderType disp}.

Implicit Types (x y : T) (s : seq T).

Lemma le_anti: antisymmetric (<=%O : rel T).

Proof.

exact: le_anti. Qed.

Lemma ge_anti: antisymmetric (>=%O : rel T).

Proof.

by move=> x y /le_anti. Qed.

Lemma eq_le x y: (x == y) = (x <= y <= x).

Proof.

by apply/eqP/idP => [->|/le_anti]; rewrite ?lexx. Qed.

Lemma lt_def x y : (x < y) = (y != x) && (x <= y).

Proof.

rewrite andbC lt_le_def; case/boolP: (x <= y) => //= xy.
congr negb; apply/idP/eqP => [yx|->]; last exact/lexx.
by apply/le_anti; rewrite yx.
Qed.

Lemma lt_neqAle x y: (x < y) = (x != y) && (x <= y).

Proof.

by rewrite lt_def eq_sym. Qed.

Lemma le_eqVlt x y: (x <= y) = (x == y) || (x < y).

Proof.

by rewrite lt_neqAle; case: eqP => //= ->; rewrite lexx. Qed.

Definition lte_anti := (=^~ eq_le, @lt_asym disp T, @lt_le_asym disp T, @le_lt_asym disp T).

Lemma eq_geP {x y} : reflect (forall z, (z <= x) = (z <= y)) (x == y).

Proof.

by apply: (iffP idP) => [/eqP->//|/[dup]] /[!eq_le] -> <-; rewrite !lexx.
Qed.

Lemma eq_leP {x y} : reflect (forall z, (x <= z) = (y <= z)) (x == y).

Proof.

by apply: (iffP idP) => [/eqP->//|/[dup]] /[!eq_le] <- ->; rewrite !lexx.
Qed.

Lemma lt_sorted_uniq_le s : sorted <%O s = uniq s && sorted <=%O s.

Proof.

rewrite le_sorted_pairwise lt_sorted_pairwise uniq_pairwise -pairwise_relI.
by apply/eq_pairwise => ? ?; rewrite lt_neqAle.
Qed.

Lemma le_sorted_eq s1 s2 :
sorted <=%O s1 -> sorted <=%O s2 -> perm_eq s1 s2 -> s1 = s2.

Proof.

exact/sorted_eq/le_anti/le_trans. Qed.

Lemma count_lt_le_mem x s : (count (< x) s < count (<= x) s)%N = (x \in s).

Proof.

have := count_predUI (pred1 x) (< x) s.
have -> : count (predI (pred1 x) (< x)) s = 0%N.
rewrite (@eq_count _ _ pred0) ?count_pred0 // => y /=.
by rewrite lt_neqAle; case: eqP => //= ->; rewrite eqxx.
have /eq_count-> : [predU1 x & < x] =1 (<= x) by move=> y /=; rewrite le_eqVlt.
by rewrite addn0 => ->; rewrite -add1n leq_add2r -has_count has_pred1.
Qed.

Lemma comparable_ltgtP x y : x >=< y ->
compare x y (min y x) (min x y) (max y x) (max x y)
(y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y).

Proof.

rewrite /min /max />=<%O !le_eqVlt [y == x]eq_sym.
have := (eqVneq x y, (boolP (x < y), boolP (y < x))).
move=> [[->//|neq_xy /=] [[] xy [] //=]] ; do ?by rewrite ?ltxx; constructor.
by rewrite ltxx in xy.
by rewrite le_gtF // ltW.
Qed.

Lemma comparable_leP x y : x >=< y ->
le_xor_gt x y (min y x) (min x y) (max y x) (max x y) (x <= y) (y < x).

Proof.

by move=> /comparable_ltgtP [?|?|->]; constructor; rewrite // ltW. Qed.

Lemma comparable_ltP x y : x >=< y ->
lt_xor_ge x y (min y x) (min x y) (max y x) (max x y) (y <= x) (x < y).

Proof.

by move=> /comparable_ltgtP [?|?|->]; constructor; rewrite // ltW. Qed.

Lemma comparableP x y : incompare x y
  (min y x) (min x y) (max y x) (max x y)
  (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y)
  (y >=< x) (x >=< y).

Proof.

rewrite ![y >=< _]comparable_sym; have [c_xy|i_xy] := boolP (x >=< y).
by case: (comparable_ltgtP c_xy) => ?; constructor.
by rewrite /min /max ?incomparable_eqF ?incomparable_leF;
rewrite ?incomparable_ltF// 1?comparable_sym //; constructor.
Qed.

Lemma leifP x y C : reflect (x <= y ?= iff C) (if C then x == y else x < y).

Proof.

rewrite /leif le_eqVlt; apply: (iffP idP)=> [|[]].
by case: C => [/eqP->|lxy]; rewrite ?eqxx // lxy lt_eqF.
by move=> /orP[/eqP->|lxy] <-; rewrite ?eqxx // lt_eqF.
Qed.

Lemma leif_trans x1 x2 x3 C12 C23 :
x1 <= x2 ?= iff C12 -> x2 <= x3 ?= iff C23 -> x1 <= x3 ?= iff C12 && C23.

Proof.

move=> ltx12 ltx23; apply/leifP; rewrite -ltx12.
case eqx12: (x1 == x2).
by rewrite (eqP eqx12) lt_neqAle !ltx23 andbT; case C23.
by rewrite (@lt_le_trans _ _ x2) ?ltx23 // lt_neqAle eqx12 ltx12.
Qed.

Lemma leif_le x y : x <= y -> x <= y ?= iff (x >= y).

Proof.

by move=> lexy; split=> //; rewrite eq_le lexy. Qed.

Lemma leif_eq x y : x <= y -> x <= y ?= iff (x == y).

Proof.

by []. Qed.

Lemma ge_leif x y C : x <= y ?= iff C -> (y <= x) = C.

Proof.

by case=> le_xy; rewrite eq_le le_xy. Qed.

Lemma lt_leif x y C : x <= y ?= iff C -> (x < y) = ~~ C.

Proof.

by move=> le_xy; rewrite lt_neqAle !le_xy andbT. Qed.

Lemma ltNleif x y C : x <= y ?= iff ~~ C -> (x < y) = C.

Proof.

by move=> /lt_leif; rewrite negbK. Qed.

Lemma lteif_anti C1 C2 x y :
(x < y ?<= if C1) && (y < x ?<= if C2) = C1 && C2 && (x == y).

Proof.

by case: C1 C2 => [][]; rewrite lte_anti. Qed.

Lemma lteifN C x y : x < y ?<= if ~~ C -> ~~ (y < x ?<= if C).

Proof.

by case: C => /=; case: comparableP. Qed.

Lemma minEle x y : min x y = if x <= y then x else y.

Proof.

by case: comparableP. Qed.

Lemma maxEle x y : max x y = if x <= y then y else x.

Proof.

by case: comparableP. Qed.

Lemma comparable_minEgt x y : x >=< y -> min x y = if x > y then y else x.

Proof.

by case: comparableP. Qed.

Lemma comparable_maxEgt x y : x >=< y -> max x y = if x > y then x else y.

Proof.

by case: comparableP. Qed.

Lemma comparable_minEge x y : x >=< y -> min x y = if x >= y then y else x.

Proof.

by case: comparableP. Qed.

Lemma comparable_maxEge x y : x >=< y -> max x y = if x >= y then x else y.

Proof.

by case: comparableP. Qed.

Lemma min_l x y : x <= y -> min x y = x

Proof.

by case: comparableP. Qed.

Lemma min_r x y : y <= x -> min x y = y

Proof.

by case: comparableP. Qed.

Lemma max_l x y : y <= x -> max x y = x

Proof.

by case: comparableP. Qed.

Lemma max_r x y : x <= y -> max x y = y

Proof.

by case: comparableP. Qed.

Lemma eq_minl x y : (min x y == x) = (x <= y).

Proof.

by rewrite !(fun_if, if_arg) eqxx; case: comparableP. Qed.

Lemma eq_maxr x y : (max x y == y) = (x <= y).

Proof.

by rewrite !(fun_if, if_arg) eqxx; case: comparableP. Qed.

Lemma min_idPl x y : reflect (min x y = x) (x <= y).

Proof.

by rewrite -eq_minl; apply/eqP. Qed.

Lemma max_idPr x y : reflect (max x y = y) (x <= y).

Proof.

by rewrite -eq_maxr; apply/eqP. Qed.

Section Comparable2.
Context (z x y : T) (cmp_xy : x >=< y).

Lemma comparable_minC : min x y = min y x.

Proof.

by case: comparableP cmp_xy. Qed.

Lemma comparable_maxC : max x y = max y x.

Proof.

by case: comparableP cmp_xy. Qed.

Lemma comparable_eq_minr : (min x y == y) = (y <= x).

Proof.

by rewrite !(fun_if, if_arg) eqxx; case: comparableP cmp_xy. Qed.

Lemma comparable_eq_maxl : (max x y == x) = (y <= x).

Proof.

by rewrite !(fun_if, if_arg) eqxx; case: comparableP cmp_xy. Qed.

Lemma comparable_min_idPr : reflect (min x y = y) (y <= x).

Proof.

by rewrite -comparable_eq_minr; apply/eqP. Qed.

Lemma comparable_max_idPl : reflect (max x y = x) (y <= x).

Proof.

by rewrite -comparable_eq_maxl; apply/eqP. Qed.

Lemma comparable_lteifNE C :
x >=< y -> (x < y ?<= if ~~ C) = ~~ (y < x ?<= if C).

Proof.

by case: C => /=; case: comparableP. Qed.

End Comparable2.

Section Comparable3.
Context (x y z : T) (cmp_xy : x >=< y) (cmp_xz : x >=< z) (cmp_yz : y >=< z).
Let P := comparableP.

Lemma comparable_max_minl : max (min x y) z = min (max x z) (max y z).

Proof.

move: cmp_xy cmp_xz cmp_yz; rewrite !(fun_if, if_arg)/=.
move: (P x y) (P x z) (P y z).
move=> [xy|xy|xy|<-] [xz|xz|xz|<-] [yz|yz|yz|//->]//= _; rewrite ?ltxx//.
- by have := lt_trans xy (lt_trans yz xz); rewrite ltxx.
- by have := lt_trans xy (lt_trans xz yz); rewrite ltxx.
Qed.

End Comparable3.

Section Comparable4.
Context (x y z w : T) (cmp_xy : x >=< y) (cmp_zw : z >=< w).

Lemma comparable_le_min2 : x <= z -> y <= w ->
Order.min x y <= Order.min z w.

Proof.

move: cmp_xy cmp_zw => /comparable_leP[] xy /comparable_leP[] zw // xz yw.
- exact: le_trans xy yw.
- exact: le_trans (ltW xy) xz.
Qed.

Lemma comparable_le_max2 : x <= z -> y <= w ->
Order.max x y <= Order.max z w.

Proof.

move: cmp_xy cmp_zw => /comparable_leP[] xy /comparable_leP[] zw // xz yw.
- exact: le_trans yw (ltW zw).
- exact: le_trans xz zw.
Qed.

End Comparable4.

Lemma comparable_minAC x y z : x >=< y -> x >=< z -> y >=< z ->
min (min x y) z = min (min x z) y.

Proof.

move=> xy xz yz; rewrite -comparable_minA// [min y z]comparable_minC//.
by rewrite comparable_minA// 1?comparable_sym.
Qed.

Lemma comparable_maxAC x y z : x >=< y -> x >=< z -> y >=< z ->
max (max x y) z = max (max x z) y.

Proof.

move=> xy xz yz; rewrite -comparable_maxA// [max y z]comparable_maxC//.
by rewrite comparable_maxA// 1?comparable_sym.
Qed.

Lemma comparable_minCA x y z : x >=< y -> x >=< z -> y >=< z ->
min x (min y z) = min y (min x z).

Proof.

move=> xy xz yz; rewrite comparable_minA// [min x y]comparable_minC//.
by rewrite -comparable_minA// 1?comparable_sym.
Qed.

Lemma comparable_maxCA x y z : x >=< y -> x >=< z -> y >=< z ->
max x (max y z) = max y (max x z).

Proof.

move=> xy xz yz; rewrite comparable_maxA// [max x y]comparable_maxC//.
by rewrite -comparable_maxA// 1?comparable_sym.
Qed.

Lemma comparable_minACA x y z t :
x >=< y -> x >=< z -> x >=< t -> y >=< z -> y >=< t -> z >=< t ->
min (min x y) (min z t) = min (min x z) (min y t).

Proof.

move=> xy xz xt yz yt zt; rewrite comparable_minA// ?comparable_minl//.
rewrite [min _ z]comparable_minAC// -comparable_minA// ?comparable_minl//.
by rewrite inE comparable_sym.
Qed.

Lemma comparable_maxACA x y z t :
x >=< y -> x >=< z -> x >=< t -> y >=< z -> y >=< t -> z >=< t ->
max (max x y) (max z t) = max (max x z) (max y t).

Proof.

move=> xy xz xt yz yt zt; rewrite comparable_maxA// ?comparable_maxl//.
rewrite [max _ z]comparable_maxAC// -comparable_maxA// ?comparable_maxl//.
by rewrite inE comparable_sym.
Qed.

Lemma comparable_min_maxr x y z : x >=< y -> x >=< z -> y >=< z ->
min x (max y z) = max (min x y) (min x z).

Proof.

move=> xy xz yz; rewrite ![min x _]comparable_minC// ?comparable_maxr//.
by rewrite comparable_min_maxl// 1?comparable_sym.
Qed.

Lemma mono_in_leif (A : {pred T}) (f : T -> T) C :
{in A &, {mono f : x y / x <= y}} ->
{in A &, forall x y, (f x <= f y ?= iff C) = (x <= y ?= iff C)}.

Proof.

by move=> mf x y Ax Ay; rewrite /leif !eq_le !mf. Qed.

Lemma mono_leif (f : T -> T) C :
{mono f : x y / x <= y} ->
forall x y, (f x <= f y ?= iff C) = (x <= y ?= iff C).

Proof.

by move=> mf x y; rewrite /leif !eq_le !mf. Qed.

Lemma nmono_in_leif (A : {pred T}) (f : T -> T) C :
{in A &, {mono f : x y /~ x <= y}} ->
{in A &, forall x y, (f x <= f y ?= iff C) = (y <= x ?= iff C)}.

Proof.

by move=> mf x y Ax Ay; rewrite /leif !eq_le !mf. Qed.

Lemma nmono_leif (f : T -> T) C : {mono f : x y /~ x <= y} ->
forall x y, (f x <= f y ?= iff C) = (y <= x ?= iff C).

Proof.

by move=> mf x y; rewrite /leif !eq_le !mf. Qed.

Section bigminmax.
Context (I : Type) (r : seq I) (f : I -> T) (x0 x : T) (P : pred I).

Lemma bigmax_le : x0 <= x -> (forall i, P i -> f i <= x) ->
\big[max/x0]_(i <- r | P i) f i <= x.

Proof.

by move=> ? ?; elim/big_ind: _ => // *; rewrite maxEle; case: ifPn. Qed.

Lemma le_bigmin : x <= x0 -> (forall i, P i -> x <= f i) ->
x <= \big[min/x0]_(i <- r | P i) f i.

Proof.

by move=> ? ?; elim/big_ind: _ => // *; rewrite minEle; case: ifPn. Qed.

End bigminmax.

End POrderTheory.

#[global] Hint Resolve comparable_minr comparable_minl : core.
#[global] Hint Resolve comparable_maxr comparable_maxl : core.

Section ContraTheory.
Context {disp1 disp2 : disp_t} {T1 : porderType disp1} {T2 : porderType disp2}.
Implicit Types (x y : T1) (z t : T2) (b : bool) (m n : nat) (P : Prop).

Lemma contra_leT b x y : (~~ b -> x < y) -> (y <= x -> b).

Proof.

by case: comparableP; case: b. Qed.

Lemma contra_ltT b x y : (~~ b -> x <= y) -> (y < x -> b).

Proof.

by case: comparableP; case: b. Qed.

Lemma contra_leN b x y : (b -> x < y) -> (y <= x -> ~~ b).

Proof.

by case: comparableP; case: b. Qed.

Lemma contra_ltN b x y : (b -> x <= y) -> (y < x -> ~~ b).

Proof.

by case: comparableP; case: b. Qed.

Lemma contra_le_not P x y : (P -> x < y) -> (y <= x -> ~ P).

Proof.

by case: comparableP => // _ PF _ /PF. Qed.

Lemma contra_lt_not P x y : (P -> x <= y) -> (y < x -> ~ P).

Proof.

by case: comparableP => // _ PF _ /PF. Qed.

Lemma contra_leF b x y : (b -> x < y) -> (y <= x -> b = false).

Proof.

by case: comparableP; case: b => // _ /implyP. Qed.

Lemma contra_ltF b x y : (b -> x <= y) -> (y < x -> b = false).

Proof.

by case: comparableP; case: b => // _ /implyP. Qed.

Lemma contra_le_leq x y m n : ((n < m)%N -> y < x) -> (x <= y -> (m <= n)%N).

Proof.

by case: comparableP; case: ltngtP. Qed.

Lemma contra_le_ltn x y m n : ((n <= m)%N -> y < x) -> (x <= y -> (m < n)%N).

Proof.

by case: comparableP; case: ltngtP. Qed.

Lemma contra_lt_leq x y m n : ((n < m)%N -> y <= x) -> (x < y -> (m <= n)%N).

Proof.

by case: comparableP; case: ltngtP. Qed.

Lemma contra_lt_ltn x y m n : ((n <= m)%N -> y <= x) -> (x < y -> (m < n)%N).

Proof.

by case: comparableP; case: ltngtP. Qed.

End ContraTheory.

Section POrderMonotonyTheory.
Context {disp disp' : disp_t} {T : porderType disp} {T' : porderType disp'}.
Context (D D' : {pred T}) (f : T -> T').

Let leT_anti := @le_anti _ T.
Hint Resolve lexx lt_neqAle : core.

Let ge_antiT : antisymmetric (>=%O : rel T).

Proof.

by move=> ? ? /le_anti. Qed.

Lemma ltW_homo : {homo f : x y / x < y} -> {homo f : x y / x <= y}.

Proof.

exact: homoW. Qed.

Lemma ltW_nhomo : {homo f : x y /~ x < y} -> {homo f : x y /~ x <= y}.

Proof.

by apply: homoW=> // x y; rewrite eq_sym. Qed.

Lemma inj_homo_lt :
injective f -> {homo f : x y / x <= y} -> {homo f : x y / x < y}.

Proof.

exact: inj_homo. Qed.

Lemma inj_nhomo_lt :
injective f -> {homo f : x y /~ x <= y} -> {homo f : x y /~ x < y}.

Proof.

by apply: inj_homo=> // x y; rewrite eq_sym. Qed.

Lemma inc_inj : {mono f : x y / x <= y} -> injective f.

Proof.

exact: mono_inj. Qed.

Lemma dec_inj : {mono f : x y /~ x <= y} -> injective f.

Proof.

exact: mono_inj. Qed.

Lemma ltW_homo_in :
{in D & D', {homo f : x y / x < y}} -> {in D & D', {homo f : x y / x <= y}}.

Proof.

exact: homoW_in. Qed.

Lemma ltW_nhomo_in :
{in D & D', {homo f : x y /~ x < y}} -> {in D & D', {homo f : x y /~ x <= y}}.

Proof.

by apply: homoW_in=> // x y; rewrite eq_sym. Qed.

Lemma inj_homo_lt_in :
{in D & D', injective f} -> {in D & D', {homo f : x y / x <= y}} ->
{in D & D', {homo f : x y / x < y}}.

Proof.

exact: inj_homo_in. Qed.

Lemma inj_nhomo_lt_in :
{in D & D', injective f} -> {in D & D', {homo f : x y /~ x <= y}} ->
{in D & D', {homo f : x y /~ x < y}}.

Proof.

by apply: inj_homo_in=> // x y; rewrite eq_sym. Qed.

Lemma inc_inj_in : {in D &, {mono f : x y / x <= y}} ->
{in D &, injective f}.

Proof.

exact: mono_inj_in. Qed.

Lemma dec_inj_in :
{in D &, {mono f : x y /~ x <= y}} -> {in D &, injective f}.

Proof.

exact: mono_inj_in. Qed.

End POrderMonotonyTheory.

End POrderTheory.

Arguments leifP {disp T x y C}.
Arguments mono_in_leif [disp T A f C].
Arguments nmono_in_leif [disp T A f C].
Arguments mono_leif [disp T f C].
Arguments nmono_leif [disp T f C].
Arguments min_idPl {disp T x y}.
Arguments max_idPr {disp T x y}.
Arguments comparable_min_idPr {disp T x y _}.
Arguments comparable_max_idPl {disp T x y _}.

Module Import BPOrderTheory.

Export BPreorderTheory.

Section BPOrderTheory.
Context {disp : disp_t} {T : bPOrderType disp}.
Implicit Types (x y : T).

Lemma lex0 x : (x <= \bot) = (x == \bot).

Proof.

by rewrite le_eqVlt ltx0 orbF. Qed.

Lemma lt0x x : (\bot < x) = (x != \bot).

Proof.

by rewrite lt_def le0x andbT. Qed.

Variant eq0_xor_gt0 x : bool -> bool -> Set :=
Eq0NotPOs : x = \bot -> eq0_xor_gt0 x true false
| POsNotEq0 : \bot < x -> eq0_xor_gt0 x false true.

Lemma posxP x : eq0_xor_gt0 x (x == \bot) (\bot < x).

Proof.

by rewrite lt0x; have [] := eqVneq; constructor; rewrite ?lt0x. Qed.

End BPOrderTheory.
End BPOrderTheory.

Module Import TPOrderTheory.
Section TPOrderTheory.
Context {disp : disp_t} {T : tPOrderType disp}.
Implicit Types (x y : T).

Lemma le1x x : (\top <= x) = (x == \top)

Proof.

exact: (@lex0 _ T^d). Qed.

Lemma ltx1 x : (x < \top) = (x != \top)

Proof.

exact: (@lt0x _ T^d). Qed.

End TPOrderTheory.
End TPOrderTheory.

Module Import MeetTheory.
Section MeetTheory.
Context {disp : disp_t} {L : meetSemilatticeType disp}.
Implicit Types (x y : L).

Lemma lexI x y z : (x <= y `&` z) = (x <= y) && (x <= z).

Proof.

exact: lexI. Qed.

Lemma leIr x y : y `&` x <= x.

Proof.

by have:= le_refl (meet y x); rewrite lexI => /andP []. Qed.

Lemma leIl x y : x `&` y <= x.

Proof.

by have:= le_refl (meet x y); rewrite lexI => /andP []. Qed.

Lemma leIxl x y z : y <= x -> y `&` z <= x.

Proof.

exact/le_trans/leIl. Qed.

Lemma leIxr x y z : z <= x -> y `&` z <= x.

Proof.

exact/le_trans/leIr. Qed.

Lemma leIx2 x y z : (y <= x) || (z <= x) -> y `&` z <= x.

Proof.

by case/orP => [/leIxl|/leIxr]. Qed.

Lemma leEmeet x y : (x <= y) = (x `&` y == x).

Proof.

by rewrite eq_le lexI leIl lexx. Qed.

Lemma eq_meetl x y : (x `&` y == x) = (x <= y).

Proof.

by apply/esym/leEmeet. Qed.

Lemma eq_meetr x y : (x `&` y == y) = (y <= x).

Proof.

by rewrite eq_le lexI leIr lexx andbT. Qed.

Lemma meet_idPl {x y} : reflect (x `&` y = x) (x <= y).

Proof.

by rewrite -eq_meetl; apply/eqP. Qed.

Lemma meet_idPr {x y} : reflect (y `&` x = x) (x <= y).

Proof.

by rewrite -eq_meetr; apply/eqP. Qed.

Lemma meet_l x y : x <= y -> x `&` y = x

Proof.

exact/meet_idPl. Qed.

Lemma meet_r x y : y <= x -> x `&` y = y

Proof.

exact/meet_idPr. Qed.

Lemma leIidl x y : (x <= x `&` y) = (x <= y).

Proof.

by rewrite lexI lexx. Qed.

Lemma leIidr x y : (x <= y `&` x) = (x <= y).

Proof.

by rewrite lexI lexx andbT. Qed.

Lemma leI2 x y z t : x <= z -> y <= t -> x `&` y <= z `&` t.

Proof.

by move=> xz yt; rewrite lexI !leIx2 ?xz ?yt ?orbT //. Qed.

Lemma meetC : commutative (@meet _ L).

Proof.

by move=> x y; apply: le_anti; rewrite !lexI !leIr !leIl. Qed.

Lemma meetA : associative (@meet _ L).

Proof.

move=> x y z; apply: le_anti.
rewrite !lexI leIr leIl /= andbT -andbA.
rewrite ![_ `&` (_ `&` _) <= _]leIxr ?(leIr, leIl) //=.
by rewrite leIxl ?leIl // leIxl // leIr.
Qed.

HB.instance Definition _ := SemiGroup.isComLaw.Build L meet meetA meetC.

Lemma meetxx : idempotent_op (@meet _ L).

Proof.

by move=> x; apply/eqP; rewrite -leEmeet. Qed.

Lemma meetAC : right_commutative (@meet _ L).

Proof.

by move=> x y z; rewrite -!meetA [X in _ `&` X]meetC. Qed.

Lemma meetCA : left_commutative (@meet _ L).

Proof.

by move=> x y z; rewrite !meetA [X in X `&` _]meetC. Qed.

Lemma meetACA : interchange (@meet _ L) (@meet _ L).

Proof.

by move=> x y z t; rewrite !meetA [X in X `&` _]meetAC. Qed.

Lemma meetKI y x : x `&` (x `&` y) = x `&` y.

Proof.

by rewrite meetA meetxx. Qed.

Lemma meetIK y x : (x `&` y) `&` y = x `&` y.

Proof.

by rewrite -meetA meetxx. Qed.

Lemma meetKIC y x : x `&` (y `&` x) = x `&` y.

Proof.

by rewrite meetC meetIK meetC. Qed.

Lemma meetIKC y x : y `&` x `&` y = x `&` y.

Proof.

by rewrite meetAC meetC meetxx. Qed.

End MeetTheory.
End MeetTheory.

Arguments meet_idPl {disp L x y}.
Arguments meet_idPr {disp L x y}.

Module Import BMeetTheory.
Section BMeetTheory.
Context {disp : disp_t} {L : bMeetSemilatticeType disp}.

Lemma meet0x : left_zero \bot (@meet _ L).

Proof.

by move=> x; apply/eqP; rewrite -leEmeet. Qed.

Lemma meetx0 : right_zero \bot (@meet _ L).

Proof.

by move=> x; rewrite meetC meet0x. Qed.

HB.instance Definition _ := Monoid.isMulLaw.Build L \bot meet meet0x meetx0.

End BMeetTheory.
End BMeetTheory.

Module Import TMeetTheory.
Section TMeetTheory.
Context {disp : disp_t} {L : tMeetSemilatticeType disp}.
Implicit Types (I : finType) (T : eqType) (x y : L).

Lemma meetx1 : right_id \top (@meet _ L).

Proof.

by move=> x; apply/eqP; rewrite -leEmeet. Qed.

Lemma meet1x : left_id \top (@meet _ L).

Proof.

by move=> x; apply/eqP; rewrite meetC meetx1. Qed.

Lemma meet_eq1 x y : (x `&` y == \top) = (x == \top) && (y == \top).

Proof.

apply/idP/idP; last by move=> /andP[/eqP-> /eqP->]; rewrite meetx1.
by move=> /eqP xIy1; rewrite -!le1x -xIy1 leIl leIr.
Qed.

HB.instance Definition _ := Monoid.isMonoidLaw.Build L \top meet meet1x meetx1.

Lemma meets_inf_seq T (r : seq T) (P : {pred T}) (F : T -> L) (x : T) :
x \in r -> P x -> \meet_(i <- r | P i) F i <= F x.

Proof.

by move=> xr Px; rewrite (big_rem x) ?Px //= leIl. Qed.

Lemma meets_max_seq T (r : seq T) (P : {pred T}) (F : T -> L) (x : T) (u : L) :
x \in r -> P x -> F x <= u -> \meet_(x <- r | P x) F x <= u.

Proof.

by move=> ? ?; apply/le_trans/meets_inf_seq. Qed.

Lemma meets_inf I (j : I) (P : {pred I}) (F : I -> L) :
P j -> \meet_(i | P i) F i <= F j.

Proof.

exact: meets_inf_seq. Qed.

Lemma meets_max I (j : I) (u : L) (P : {pred I}) (F : I -> L) :
P j -> F j <= u -> \meet_(i | P i) F i <= u.

Proof.

exact: meets_max_seq. Qed.

Lemma meets_ge J (r : seq J) (P : {pred J}) (F : J -> L) (u : L) :
(forall x : J, P x -> u <= F x) -> u <= \meet_(x <- r | P x) F x.

Proof.

by move=> leFm; elim/big_rec: _ => // i x Px xu; rewrite lexI leFm. Qed.

Lemma meetsP_seq T (r : seq T) (P : {pred T}) (F : T -> L) (l : L) :
reflect (forall x : T, x \in r -> P x -> l <= F x)
(l <= \meet_(x <- r | P x) F x).

Proof.

apply: (iffP idP) => leFm => [x xr Px|].
exact/(le_trans leFm)/meets_inf_seq.
by rewrite big_seq_cond meets_ge// => x /andP[/leFm].
Qed.

Lemma meetsP I (l : L) (P : {pred I}) (F : I -> L) :
reflect (forall i : I, P i -> l <= F i) (l <= \meet_(i | P i) F i).

Proof.

by apply: (iffP (meetsP_seq _ _ _ _)) => H ? ?; apply: H. Qed.

Lemma le_meets I (A B : {set I}) (F : I -> L) :
A \subset B -> \meet_(i in B) F i <= \meet_(i in A) F i.

Proof.

by move=> /subsetP AB; apply/meetsP => i iA; apply/meets_inf/AB. Qed.

Lemma meets_setU I (A B : {set I}) (F : I -> L) :
\meet_(i in (A :|: B)) F i = \meet_(i in A) F i `&` \meet_(i in B) F i.

Proof.

rewrite -!big_enum; have /= <- := @big_cat _ _ meet.
apply/eq_big_idem; first exact: meetxx.
by move=> ?; rewrite mem_cat !fintype.mem_enum inE.
Qed.

Lemma meets_seq I (r : seq I) (F : I -> L) :
\meet_(i <- r) F i = \meet_(i in r) F i.

Proof.

by rewrite -big_enum; apply/eq_big_idem => ?; rewrite /= ?meetxx ?fintype.mem_enum.
Qed.

End TMeetTheory.
End TMeetTheory.

Module Import JoinTheory.
Section JoinTheory.
Context {disp : disp_t} {L : joinSemilatticeType disp}.
Implicit Types (x y : L).

Lemma leUx x y z : (x `|` y <= z) = (x <= z) && (y <= z).

Proof.

exact: leUx. Qed.

Lemma leUr x y : x <= y `|` x

Proof.

exact: (@leIr _ L^d). Qed.

Lemma leUl x y : x <= x `|` y

Proof.

exact: (@leIl _ L^d). Qed.

Lemma lexUl x y z : x <= y -> x <= y `|` z.

Proof.

exact: (@leIxl _ L^d). Qed.

Lemma lexUr x y z : x <= z -> x <= y `|` z.

Proof.

exact: (@leIxr _ L^d). Qed.

Lemma lexU2 x y z : (x <= y) || (x <= z) -> x <= y `|` z.

Proof.

exact: (@leIx2 _ L^d). Qed.

Lemma leEjoin x y : (x <= y) = (x `|` y == y).

Proof.

by rewrite [LHS](@leEmeet _ L^d) meetC. Qed.

Lemma eq_joinl x y : (x `|` y == x) = (y <= x).

Proof.

exact: (@eq_meetl _ L^d). Qed.

Lemma eq_joinr x y : (x `|` y == y) = (x <= y).

Proof.

exact: (@eq_meetr _ L^d). Qed.

Lemma join_idPl {x y} : reflect (y `|` x = y) (x <= y).

Proof.

exact: (@meet_idPl _ L^d). Qed.

Lemma join_idPr {x y} : reflect (x `|` y = y) (x <= y).

Proof.

exact: (@meet_idPr _ L^d). Qed.

Lemma join_l x y : y <= x -> x `|` y = x

Proof.

exact/join_idPl. Qed.

Lemma join_r x y : x <= y -> x `|` y = y

Proof.

exact/join_idPr. Qed.

Lemma leUidl x y : (x `|` y <= y) = (x <= y).

Proof.

exact: (@leIidr _ L^d). Qed.

Lemma leUidr x y : (y `|` x <= y) = (x <= y).

Proof.

exact: (@leIidl _ L^d). Qed.

Lemma leU2 x y z t : x <= z -> y <= t -> x `|` y <= z `|` t.

Proof.

exact: (@leI2 _ L^d). Qed.

Lemma joinC : commutative (@join _ L)

Proof.

exact: (@meetC _ L^d). Qed.

Lemma joinA : associative (@join _ L)

Proof.

exact: (@meetA _ L^d). Qed.

HB.instance Definition _ := SemiGroup.isComLaw.Build L join joinA joinC.

Lemma joinxx : idempotent_op (@join _ L).

Proof.

exact: (@meetxx _ L^d). Qed.

Lemma joinAC : right_commutative (@join _ L).

Proof.

exact: (@meetAC _ L^d). Qed.

Lemma joinCA : left_commutative (@join _ L).

Proof.

exact: (@meetCA _ L^d). Qed.

Lemma joinACA : interchange (@join _ L) (@join _ L).

Proof.

exact: (@meetACA _ L^d). Qed.

Lemma joinKU y x : x `|` (x `|` y) = x `|` y.

Proof.

exact: (@meetKI _ L^d). Qed.

Lemma joinUK y x : (x `|` y) `|` y = x `|` y.

Proof.

exact: (@meetIK _ L^d). Qed.

Lemma joinKUC y x : x `|` (y `|` x) = x `|` y.

Proof.

exact: (@meetKIC _ L^d). Qed.

Lemma joinUKC y x : y `|` x `|` y = x `|` y.

Proof.

exact: (@meetIKC _ L^d). Qed.

End JoinTheory.
End JoinTheory.

Arguments join_idPl {disp L x y}.
Arguments join_idPr {disp L x y}.

Module Import BJoinTheory.
Section BJoinTheory.
Context {disp : disp_t} {L : bJoinSemilatticeType disp}.
Implicit Types (I : finType) (T : eqType) (x y : L).

Lemma joinx0 : right_id \bot (@join _ L).

Proof.

exact: (@meetx1 _ L^d). Qed.

Lemma join0x : left_id \bot (@join _ L).

Proof.

exact: (@meet1x _ L^d). Qed.

Lemma join_eq0 x y : (x `|` y == \bot) = (x == \bot) && (y == \bot).

Proof.

exact: (@meet_eq1 _ L^d). Qed.

HB.instance Definition _ := Monoid.isMonoidLaw.Build L \bot join join0x joinx0.

Lemma joins_sup_seq T (r : seq T) (P : {pred T}) (F : T -> L) (x : T) :
x \in r -> P x -> F x <= \join_(i <- r | P i) F i.

Proof.

exact: (@meets_inf_seq _ L^d). Qed.

Lemma joins_min_seq T (r : seq T) (P : {pred T}) (F : T -> L) (x : T) (l : L) :
x \in r -> P x -> l <= F x -> l <= \join_(x <- r | P x) F x.

Proof.

exact: (@meets_max_seq _ L^d). Qed.

Lemma joins_sup I (j : I) (P : {pred I}) (F : I -> L) :
P j -> F j <= \join_(i | P i) F i.

Proof.

exact: (@meets_inf _ L^d). Qed.

Lemma joins_min I (j : I) (l : L) (P : {pred I}) (F : I -> L) :
P j -> l <= F j -> l <= \join_(i | P i) F i.

Proof.

exact: (@meets_max _ L^d). Qed.

Lemma joins_le J (r : seq J) (P : {pred J}) (F : J -> L) (u : L) :
(forall x : J, P x -> F x <= u) -> \join_(x <- r | P x) F x <= u.

Proof.

exact: (@meets_ge _ L^d). Qed.

Lemma joinsP_seq T (r : seq T) (P : {pred T}) (F : T -> L) (u : L) :
reflect (forall x : T, x \in r -> P x -> F x <= u)
(\join_(x <- r | P x) F x <= u).

Proof.

exact: (@meetsP_seq _ L^d). Qed.

Lemma joinsP I (u : L) (P : {pred I}) (F : I -> L) :
reflect (forall i : I, P i -> F i <= u) (\join_(i | P i) F i <= u).

Proof.

exact: (@meetsP _ L^d). Qed.

Lemma le_joins I (A B : {set I}) (F : I -> L) :
A \subset B -> \join_(i in A) F i <= \join_(i in B) F i.

Proof.

exact: (@le_meets _ L^d). Qed.

Lemma joins_setU I (A B : {set I}) (F : I -> L) :
\join_(i in (A :|: B)) F i = \join_(i in A) F i `|` \join_(i in B) F i.

Proof.

exact: (@meets_setU _ L^d). Qed.

Lemma joins_seq I (r : seq I) (F : I -> L) :
\join_(i <- r) F i = \join_(i in r) F i.

Proof.

exact: (@meets_seq _ L^d). Qed.

End BJoinTheory.
End BJoinTheory.

Module Import TJoinTheory.
Section TJoinTheory.
Context {disp : disp_t} {L : tJoinSemilatticeType disp}.

Lemma joinx1 : right_zero \top (@join _ L)

Proof.

exact: (@meetx0 _ L^d). Qed.

Lemma join1x : left_zero \top (@join _ L)

Proof.

exact: (@meet0x _ L^d). Qed.

HB.instance Definition _ := Monoid.isMulLaw.Build L \top join join1x joinx1.

End TJoinTheory.
End TJoinTheory.

Module Import LatticeTheory.
Section LatticeTheory.
Context {disp : disp_t} {L : latticeType disp}.
Implicit Types (x y : L).

Lemma meetUK x y : (x `&` y) `|` y = y

Proof.

exact/join_idPr/leIr. Qed.

Lemma meetUKC x y : (y `&` x) `|` y = y

Proof.

by rewrite meetC meetUK. Qed.

Lemma meetKUC y x : x `|` (y `&` x) = x

Proof.

by rewrite joinC meetUK. Qed.

Lemma meetKU y x : x `|` (x `&` y) = x

Proof.

by rewrite meetC meetKUC. Qed.

Lemma joinIK x y : (x `|` y) `&` y = y

Proof.

exact/meet_idPr/leUr. Qed.

Lemma joinIKC x y : (y `|` x) `&` y = y

Proof.

by rewrite joinC joinIK. Qed.

Lemma joinKIC y x : x `&` (y `|` x) = x

Proof.

by rewrite meetC joinIK. Qed.

Lemma joinKI y x : x `&` (x `|` y) = x

Proof.

by rewrite joinC joinKIC. Qed.

Lemma lcomparableP x y : incomparel x y
  (min y x) (min x y) (max y x) (max x y)
  (y `&` x) (x `&` y) (y `|` x) (x `|` y)
  (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y) (y >=< x) (x >=< y).

Proof.

by case: (comparableP x) => [hxy|hxy|hxy|->]; do 1?have hxy' := ltW hxy;
   rewrite ?(meetxx, joinxx);
   rewrite ?(meet_l hxy', meet_r hxy', join_l hxy', join_r hxy');
   constructor.
Qed.

Lemma lcomparable_ltgtP x y : x >=< y ->
  comparel x y (min y x) (min x y) (max y x) (max x y)
               (y `&` x) (x `&` y) (y `|` x) (x `|` y)
               (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y).

Proof.

by case: (lcomparableP x) => // *; constructor. Qed.

Lemma lcomparable_leP x y : x >=< y ->
lel_xor_gt x y (min y x) (min x y) (max y x) (max x y)
(y `&` x) (x `&` y) (y `|` x) (x `|` y) (x <= y) (y < x).

Proof.

by move/lcomparable_ltgtP => [/ltW xy|xy|->]; constructor. Qed.

Lemma lcomparable_ltP x y : x >=< y ->
ltl_xor_ge x y (min y x) (min x y) (max y x) (max x y)
(y `&` x) (x `&` y) (y `|` x) (x `|` y) (y <= x) (x < y).

Proof.

by move=> /lcomparable_ltgtP [xy|/ltW xy|->]; constructor. Qed.

End LatticeTheory.
End LatticeTheory.

Module Import DistrLatticeTheory.
Section DistrLatticeTheory.
Context {disp : disp_t} {L : distrLatticeType disp}.

Lemma meetUl : left_distributive (@meet _ L) (@join _ L).

Proof.

exact: meetUl. Qed.

Lemma meetUr : right_distributive (@meet _ L) (@join _ L).

Proof.

by move=> x y z; rewrite ![x `&` _]meetC meetUl. Qed.

Lemma joinIl : left_distributive (@join _ L) (@meet _ L).

Proof.

exact: joinIl. Qed.

Lemma joinIr : right_distributive (@join _ L) (@meet _ L).

Proof.

by move=> x y z; rewrite ![x `|` _]joinC joinIl. Qed.

#[warning="-HB.no-new-instance"]
HB.instance Definition _ := Monoid.isAddLaw.Build L meet join meetUl meetUr.
HB.instance Definition _ := Monoid.isAddLaw.Build L join meet joinIl joinIr.

End DistrLatticeTheory.
End DistrLatticeTheory.

Module Import BDistrLatticeTheory.
Section BDistrLatticeTheory.
Context {disp : disp_t} {L : bDistrLatticeType disp}.
Implicit Types (x y z : L).

Lemma leU2l_le y t x z : x `&` t = \bot -> x `|` y <= z `|` t -> x <= z.

Proof.

by move=> xIt0 /(leI2 (lexx x)); rewrite joinKI meetUr xIt0 joinx0 leIidl.
Qed.

Lemma leU2r_le y t x z : x `&` t = \bot -> y `|` x <= t `|` z -> x <= z.

Proof.

by rewrite joinC [_ `|` z]joinC => /leU2l_le H /H. Qed.

Lemma disjoint_lexUl z x y : x `&` z = \bot -> (x <= y `|` z) = (x <= y).

Proof.

move=> xz0; apply/idP/idP=> xy; last by rewrite lexU2 ?xy.
by apply: (@leU2l_le x z); rewrite ?joinxx.
Qed.

Lemma disjoint_lexUr z x y : x `&` z = \bot -> (x <= z `|` y) = (x <= y).

Proof.

by move=> xz0; rewrite joinC; rewrite disjoint_lexUl. Qed.

Lemma leU2E x y z t : x `&` t = \bot -> y `&` z = \bot ->
(x `|` y <= z `|` t) = (x <= z) && (y <= t).

Proof.

move=> dxt dyz; apply/idP/andP; last by case=> ? ?; exact: leU2.
by move=> lexyzt; rewrite (leU2l_le _ lexyzt) // (leU2r_le _ lexyzt).
Qed.

Lemma joins_disjoint (I : finType) (d : L) (P : {pred I}) (F : I -> L) :
(forall i : I, P i -> d `&` F i = \bot) -> d `&` \join_(i | P i) F i = \bot.

Proof.

move=> d_Fi_disj; have : \big[andb/true]_(i | P i) (d `&` F i == \bot).
rewrite big_all_cond; apply/allP => i _ /=.
by apply/implyP => /d_Fi_disj ->.
elim/big_rec2: _ => [|i y]; first by rewrite meetx0.
case; rewrite (andbF, andbT) // => Pi /(_ isT) dy /eqP dFi.
by rewrite meetUr dy dFi joinxx.
Qed.

End BDistrLatticeTheory.
End BDistrLatticeTheory.

Module Import TDistrLatticeTheory.
Section TDistrLatticeTheory.
Context {disp : disp_t} {L : tDistrLatticeType disp}.
Implicit Types (x y : L).

Lemma leI2l_le y t x z : y `|` z = \top -> x `&` y <= z `&` t -> x <= z.

Proof.

by rewrite joinC; exact: (@leU2l_le _ L^d). Qed.

Lemma leI2r_le y t x z : y `|` z = \top -> y `&` x <= t `&` z -> x <= z.

Proof.

by rewrite joinC; exact: (@leU2r_le _ L^d). Qed.

Lemma cover_leIxl z x y : z `|` y = \top -> (x `&` z <= y) = (x <= y).

Proof.

by rewrite joinC; exact: (@disjoint_lexUl _ L^d). Qed.

Lemma cover_leIxr z x y : z `|` y = \top -> (z `&` x <= y) = (x <= y).

Proof.

by rewrite joinC; exact: (@disjoint_lexUr _ L^d). Qed.

Lemma leI2E x y z t : x `|` t = \top -> y `|` z = \top ->
(x `&` y <= z `&` t) = (x <= z) && (y <= t).

Proof.

by move=> ? ?; apply: (@leU2E _ L^d); rewrite meetC. Qed.

Lemma meets_total (I : finType) (d : L) (P : {pred I}) (F : I -> L) :
(forall i : I, P i -> d `|` F i = \top) -> d `|` \meet_(i | P i) F i = \top.

Proof.

exact: (@joins_disjoint _ L^d). Qed.

End TDistrLatticeTheory.
End TDistrLatticeTheory.

Module Import TotalTheory.
Section TotalTheory.
Context {disp : disp_t} {T : orderType disp}.
Implicit Types (x y z t : T) (s : seq T).

Definition le_total : total (<=%O : rel T) := le_total.
Hint Resolve le_total : core.

Lemma ge_total : total (>=%O : rel T).

Proof.

by move=> ? ?; apply: le_total. Qed.

Hint Resolve ge_total : core.

Lemma comparableT x y : x >=< y

Proof.

exact: le_total. Qed.

Hint Extern 0 (is_true (_ >=< _)%O) => solve [apply: comparableT] : core.

Lemma sort_le_sorted s : sorted <=%O (sort <=%O s).

Proof.

exact: sort_sorted. Qed.

Hint Resolve sort_le_sorted : core.

Lemma sort_lt_sorted s : sorted <%O (sort <=%O s) = uniq s.

Proof.

by rewrite lt_sorted_uniq_le sort_uniq sort_le_sorted andbT. Qed.

Lemma perm_sort_leP s1 s2 : reflect (sort <=%O s1 = sort <=%O s2) (perm_eq s1 s2).

Proof.

exact/perm_sortP/le_anti/le_trans/le_total. Qed.

Lemma filter_sort_le p s : filter p (sort <=%O s) = sort <=%O (filter p s).

Proof.

exact/filter_sort/le_trans/le_total. Qed.

Lemma mask_sort_le s (m : bitseq) :
{m_s : bitseq | mask m_s (sort <=%O s) = sort <=%O (mask m s)}.

Proof.

exact/mask_sort/le_trans/le_total. Qed.

Lemma sorted_mask_sort_le s (m : bitseq) :
sorted <=%O (mask m s) -> {m_s : bitseq | mask m_s (sort <=%O s) = mask m s}.

Proof.

exact/sorted_mask_sort/le_trans/le_total. Qed.

Lemma subseq_sort_le : {homo sort <=%O : s1 s2 / @subseq T s1 s2}.

Proof.

exact/subseq_sort/le_trans/le_total. Qed.

Lemma sorted_subseq_sort_le s1 s2 :
subseq s1 s2 -> sorted <=%O s1 -> subseq s1 (sort <=%O s2).

Proof.

exact/sorted_subseq_sort/le_trans/le_total. Qed.

Lemma mem2_sort_le s x y : x <= y -> mem2 s x y -> mem2 (sort <=%O s) x y.

Proof.

exact/mem2_sort/le_trans/le_total. Qed.

Lemma leNgt x y : (x <= y) = ~~ (y < x)

Proof.

exact: comparable_leNgt. Qed.

Lemma ltNge x y : (x < y) = ~~ (y <= x)

Proof.

exact: comparable_ltNge. Qed.

Definition ltgtP x y := LatticeTheory.lcomparable_ltgtP (comparableT x y).
Definition leP x y := LatticeTheory.lcomparable_leP (comparableT x y).
Definition ltP x y := LatticeTheory.lcomparable_ltP (comparableT x y).

Lemma wlog_le P :
(forall x y, P y x -> P x y) -> (forall x y, x <= y -> P x y) ->
forall x y, P x y.

Proof.

by move=> sP hP x y; case: (leP x y) => [| /ltW] /hP // /sP. Qed.

Lemma wlog_lt P :
    (forall x, P x x) ->
    (forall x y, (P y x -> P x y)) -> (forall x y, x < y -> P x y) ->
  forall x y, P x y.

Proof.

by move=> rP sP hP x y; case: (ltgtP x y) => [||->] // /hP // /sP. Qed.

Lemma neq_lt x y : (x != y) = (x < y) || (y < x)

Proof.

by case: ltgtP. Qed.

Lemma lt_total x y : x != y -> (x < y) || (y < x)

Proof.

by case: ltgtP. Qed.

Lemma eq_leLR x y z t :
(x <= y -> z <= t) -> (y < x -> t < z) -> (x <= y) = (z <= t).

Proof.

by rewrite !ltNge => ? /contraTT ?; apply/idP/idP. Qed.

Lemma eq_leRL x y z t :
(x <= y -> z <= t) -> (y < x -> t < z) -> (z <= t) = (x <= y).

Proof.

by move=> *; apply/esym/eq_leLR. Qed.

Lemma eq_ltLR x y z t :
(x < y -> z < t) -> (y <= x -> t <= z) -> (x < y) = (z < t).

Proof.

by rewrite !leNgt => ? /contraTT ?; apply/idP/idP. Qed.

Lemma eq_ltRL x y z t :
(x < y -> z < t) -> (y <= x -> t <= z) -> (z < t) = (x < y).

Proof.

by move=> *; apply/esym/eq_ltLR. Qed.

Lemma le_gtP {x y} : reflect (forall z, z < x -> z < y) (x <= y).

Proof.

by apply: (iffP idP) => [xy z /lt_le_trans|/(_ y)/[!ltNge]/contraTT]; apply.
Qed.

Lemma le_ltP {x y} : reflect (forall z, y < z -> x < z) (x <= y).

Proof.

by apply: (iffP idP) => [xy z /(le_lt_trans _)|/(_ x)/[!ltNge]/contraTT]; apply.
Qed.

Lemma eq_gtP {x y} : reflect (forall z, (z < x) = (z < y)) (x == y).

Proof.

by apply: (iffP eq_leP) => + k => /(_ k)/[!ltNge]/(congr1 negb); rewrite ?negbK.
Qed.

Lemma eq_ltP {x y} : reflect (forall z, (x < z) = (y < z)) (x == y).

Proof.

by apply: (iffP eq_geP) => + k => /(_ k)/[!ltNge]/(congr1 negb); rewrite ?negbK.
Qed.

Lemma meetEtotal x y : x `&` y = min x y

Proof.

by case: leP. Qed.

Lemma joinEtotal x y : x `|` y = max x y

Proof.

by case: leP. Qed.

Lemma minEgt x y : min x y = if x > y then y else x

Proof.

by case: ltP. Qed.

Lemma maxEgt x y : max x y = if x > y then x else y

Proof.

by case: ltP. Qed.

Lemma minEge x y : min x y = if x >= y then y else x

Proof.

by case: leP. Qed.

Lemma maxEge x y : max x y = if x >= y then x else y

Proof.

by case: leP. Qed.

Lemma minC : commutative (min : T -> T -> T).

Proof.

by move=> x y; apply: comparable_minC. Qed.

Lemma maxC : commutative (max : T -> T -> T).

Proof.

by move=> x y; apply: comparable_maxC. Qed.

Lemma minA : associative (min : T -> T -> T).

Proof.

by move=> x y z; apply: comparable_minA. Qed.

Lemma maxA : associative (max : T -> T -> T).

Proof.

by move=> x y z; apply: comparable_maxA. Qed.

Lemma minAC : right_commutative (min : T -> T -> T).

Proof.

by move=> x y z; apply: comparable_minAC. Qed.

Lemma maxAC : right_commutative (max : T -> T -> T).

Proof.

by move=> x y z; apply: comparable_maxAC. Qed.

Lemma minCA : left_commutative (min : T -> T -> T).

Proof.

by move=> x y z; apply: comparable_minCA. Qed.

Lemma maxCA : left_commutative (max : T -> T -> T).

Proof.

by move=> x y z; apply: comparable_maxCA. Qed.

Lemma minACA : interchange (min : T -> T -> T) min.

Proof.

by move=> x y z t; apply: comparable_minACA. Qed.

Lemma maxACA : interchange (max : T -> T -> T) max.

Proof.

by move=> x y z t; apply: comparable_maxACA. Qed.

Lemma eq_minr x y : (min x y == y) = (y <= x).

Proof.

exact: comparable_eq_minr. Qed.

Lemma eq_maxl x y : (max x y == x) = (y <= x).

Proof.

exact: comparable_eq_maxl. Qed.

Lemma min_idPr x y : reflect (min x y = y) (y <= x).

Proof.

exact: comparable_min_idPr. Qed.

Lemma max_idPl x y : reflect (max x y = x) (y <= x).

Proof.

exact: comparable_max_idPl. Qed.

Lemma le_min z x y : (z <= min x y) = (z <= x) && (z <= y).

Proof.

exact: comparable_le_min. Qed.

Lemma ge_min z x y : (min x y <= z) = (x <= z) || (y <= z).

Proof.

exact: comparable_ge_min. Qed.

Lemma lt_min z x y : (z < min x y) = (z < x) && (z < y).

Proof.

exact: comparable_lt_min. Qed.

Lemma gt_min z x y : (min x y < z) = (x < z) || (y < z).

Proof.

exact: comparable_gt_min. Qed.

Lemma le_max z x y : (z <= max x y) = (z <= x) || (z <= y).

Proof.

exact: comparable_le_max. Qed.

Lemma ge_max z x y : (max x y <= z) = (x <= z) && (y <= z).

Proof.

exact: comparable_ge_max. Qed.

Lemma lt_max z x y : (z < max x y) = (z < x) || (z < y).

Proof.

exact: comparable_lt_max. Qed.

Lemma gt_max z x y : (max x y < z) = (x < z) && (y < z).

Proof.

exact: comparable_gt_max. Qed.

Lemma minxK x y : max (min x y) y = y

Proof.

exact: comparable_minxK. Qed.

Lemma minKx x y : max x (min x y) = x

Proof.

exact: comparable_minKx. Qed.

Lemma maxxK x y : min (max x y) y = y

Proof.

exact: comparable_maxxK. Qed.

Lemma maxKx x y : min x (max x y) = x

Proof.

exact: comparable_maxKx. Qed.

Lemma max_minl : left_distributive (max : T -> T -> T) min.

Proof.

by move=> x y z; apply: comparable_max_minl. Qed.

Lemma min_maxl : left_distributive (min : T -> T -> T) max.

Proof.

by move=> x y z; apply: comparable_min_maxl. Qed.

Lemma max_minr : right_distributive (max : T -> T -> T) min.

Proof.

by move=> x y z; apply: comparable_max_minr. Qed.

Lemma min_maxr : right_distributive (min : T -> T -> T) max.

Proof.

by move=> x y z; apply: comparable_min_maxr. Qed.

HB.instance Definition _ := SemiGroup.isComLaw.Build T max maxA maxC.
HB.instance Definition _ := SemiGroup.isComLaw.Build T min minA minC.

Lemma leIx x y z : (meet y z <= x) = (y <= x) || (z <= x).

Proof.

by rewrite meetEtotal ge_min. Qed.

Lemma lexU x y z : (x <= join y z) = (x <= y) || (x <= z).

Proof.

by rewrite joinEtotal le_max. Qed.

Lemma ltxI x y z : (x < meet y z) = (x < y) && (x < z).

Proof.

by rewrite !ltNge leIx negb_or. Qed.

Lemma ltIx x y z : (meet y z < x) = (y < x) || (z < x).

Proof.

by rewrite !ltNge lexI negb_and. Qed.

Lemma ltxU x y z : (x < join y z) = (x < y) || (x < z).

Proof.

by rewrite !ltNge leUx negb_and. Qed.

Lemma ltUx x y z : (join y z < x) = (y < x) && (z < x).

Proof.

by rewrite !ltNge lexU negb_or. Qed.

Definition ltexI := (@lexI _ T, ltxI).
Definition lteIx := (leIx, ltIx).
Definition ltexU := (lexU, ltxU).
Definition lteUx := (@leUx _ T, ltUx).

Lemma le_min2 x y z t : x <= z -> y <= t -> Order.min x y <= Order.min z t.

Proof.

exact: comparable_le_min2. Qed.

Lemma le_max2 x y z t : x <= z -> y <= t -> Order.max x y <= Order.max z t.

Proof.

exact: comparable_le_max2. Qed.

Lemma lteifNE x y C : (x < y ?<= if ~~ C) = ~~ (y < x ?<= if C).

Proof.

by case: C => /=; case: leP. Qed.

Lemma lteif_minr z x y C :
(z < min x y ?<= if C) = (z < x ?<= if C) && (z < y ?<= if C).

Proof.

by case: C; rewrite /= (le_min, lt_min). Qed.

Lemma lteif_minl z x y C :
(min x y < z ?<= if C) = (x < z ?<= if C) || (y < z ?<= if C).

Proof.

by case: C; rewrite /= (ge_min, gt_min). Qed.

Lemma lteif_maxr z x y C :
(z < max x y ?<= if C) = (z < x ?<= if C) || (z < y ?<= if C).

Proof.

by case: C; rewrite /= (le_max, lt_max). Qed.

Lemma lteif_maxl z x y C :
(max x y < z ?<= if C) = (x < z ?<= if C) && (y < z ?<= if C).

Proof.

by case: C; rewrite /= (ge_max, gt_max). Qed.

Section ArgExtremum.
Context (I : finType) (i0 : I) (P : {pred I}) (F : I -> T) (Pi0 : P i0).

Lemma arg_minP: extremum_spec <=%O P F (arg_min i0 P F).

Proof.

by apply: extremumP => //; apply: le_trans. Qed.

Lemma arg_maxP: extremum_spec >=%O P F (arg_max i0 P F).

Proof.

by apply: extremumP => //; [apply: ge_refl | apply: ge_trans]. Qed.

End ArgExtremum.

Lemma count_le_gt x s : count (<= x) s = size s - count (> x) s.

Proof.

by rewrite -(count_predC (> x)) addKn; apply: eq_count => y; rewrite /= leNgt.
Qed.

Lemma count_lt_ge x s : count (< x) s = size s - count (>= x) s.

Proof.

by rewrite -(count_predC (>= x)) addKn; apply: eq_count => y; rewrite /= ltNge.
Qed.

Section bigminmax_Type.
Context (I : Type) (r : seq I) (x : T).
Implicit Types (P : pred I) (F : I -> T).

Lemma bigmin_mkcond P F : \big[min/x]_(i <- r | P i) F i =
\big[min/x]_(i <- r) (if P i then F i else x).

Proof.

by rewrite big_mkcond_idem //= minxx. Qed.

Lemma bigmax_mkcond P F :
\big[max/x]_(i <- r | P i) F i = \big[max/x]_(i <- r) if P i then F i else x.

Proof.

by rewrite big_mkcond_idem //= maxxx. Qed.

Lemma bigmin_mkcondl P Q F :
\big[min/x]_(i <- r | P i && Q i) F i
= \big[min/x]_(i <- r | Q i) if P i then F i else x.

Proof.

rewrite bigmin_mkcond [RHS]bigmin_mkcond.
by apply: eq_bigr => i _; case: P; case: Q.
Qed.

Lemma bigmin_mkcondr P Q F :
\big[min/x]_(i <- r | P i && Q i) F i
= \big[min/x]_(i <- r | P i) if Q i then F i else x.

Proof.

by under eq_bigl do rewrite andbC; apply: bigmin_mkcondl. Qed.

Lemma bigmax_mkcondl P Q F :
\big[max/x]_(i <- r | P i && Q i) F i
= \big[max/x]_(i <- r | Q i) if P i then F i else x.

Proof.

rewrite bigmax_mkcond [RHS]bigmax_mkcond.
by apply: eq_bigr => i _; case: P; case: Q.
Qed.

Lemma bigmax_mkcondr P Q F :
\big[max/x]_(i <- r | P i && Q i) F i
= \big[max/x]_(i <- r | P i) if Q i then F i else x.

Proof.

by under eq_bigl do rewrite andbC; apply: bigmax_mkcondl. Qed.

Lemma bigmin_split P F1 F2 :
\big[min/x]_(i <- r | P i) (min (F1 i) (F2 i)) =
min (\big[min/x]_(i <- r | P i) F1 i) (\big[min/x]_(i <- r | P i) F2 i).

Proof.

by rewrite big_split_idem //= minxx. Qed.

Lemma bigmax_split P F1 F2 :
\big[max/x]_(i <- r | P i) (max (F1 i) (F2 i)) =
max (\big[max/x]_(i <- r | P i) F1 i) (\big[max/x]_(i <- r | P i) F2 i).

Proof.

by rewrite big_split_idem //= maxxx. Qed.

Lemma bigmin_idl P F :
\big[min/x]_(i <- r | P i) F i = min x (\big[min/x]_(i <- r | P i) F i).

Proof.

by rewrite minC big_id_idem //= minxx. Qed.

Lemma bigmax_idl P F :
\big[max/x]_(i <- r | P i) F i = max x (\big[max/x]_(i <- r | P i) F i).

Proof.

by rewrite maxC big_id_idem //= maxxx. Qed.

Lemma bigmin_idr P F :
\big[min/x]_(i <- r | P i) F i = min (\big[min/x]_(i <- r | P i) F i) x.

Proof.

by rewrite [LHS]bigmin_idl minC. Qed.

Lemma bigmax_idr P F :
\big[max/x]_(i <- r | P i) F i = max (\big[max/x]_(i <- r | P i) F i) x.

Proof.

by rewrite [LHS]bigmax_idl maxC. Qed.

Lemma bigminID a P F : \big[min/x]_(i <- r | P i) F i =
min (\big[min/x]_(i <- r | P i && a i) F i)
(\big[min/x]_(i <- r | P i && ~~ a i) F i).

Proof.

by rewrite (bigID_idem _ _ a) //= minxx. Qed.

Lemma bigmaxID a P F : \big[max/x]_(i <- r | P i) F i =
max (\big[max/x]_(i <- r | P i && a i) F i)
(\big[max/x]_(i <- r | P i && ~~ a i) F i).

Proof.

by rewrite (bigID_idem _ _ a) //= maxxx. Qed.

End bigminmax_Type.

Let ge_min_id (x y : T) : x >= min x y

Proof.

by rewrite ge_min lexx. Qed.

Let le_max_id (x y : T) : x <= max x y

Proof.

by rewrite le_max lexx. Qed.

Lemma sub_bigmin [x0] I r (P P' : {pred I}) (F : I -> T) :
(forall i, P' i -> P i) ->
\big[min/x0]_(i <- r | P i) F i <= \big[min/x0]_(i <- r | P' i) F i.

Proof.

exact: (sub_le_big ge_refl). Qed.

Lemma sub_bigmax [x0] I r (P P' : {pred I}) (F : I -> T) :
(forall i, P i -> P' i) ->
\big[max/x0]_(i <- r | P i) F i <= \big[max/x0]_(i <- r | P' i) F i.

Proof.

exact: sub_le_big. Qed.

Local Notation "'{subset' x '<=' y '}'" :=
(sub_mem (mem x) (mem y)) (at level 0, x, y at level 1).

Lemma sub_bigmin_seq [x0] (I : eqType) r r' P (F : I -> T) : {subset r' <= r} ->
\big[min/x0]_(i <- r | P i) F i <= \big[min/x0]_(i <- r' | P i) F i.

Proof.

exact: (idem_sub_le_big ge_refl _ minxx). Qed.

Lemma sub_bigmax_seq [x0] (I : eqType) r r' P (F : I -> T) : {subset r <= r'} ->
\big[max/x0]_(i <- r | P i) F i <= \big[max/x0]_(i <- r' | P i) F i.

Proof.

exact: (idem_sub_le_big _ _ maxxx). Qed.

Lemma sub_bigmin_cond [x0] (I : eqType) r r' P P' (F : I -> T) :
{subset ([seq i <- r | P i]) <= ([seq i <- r' | P' i])} ->
\big[min/x0]_(i <- r' | P' i) F i <= \big[min/x0]_(i <- r | P i) F i.

Proof.

exact: (idem_sub_le_big_cond ge_refl _ minxx). Qed.

Lemma sub_bigmax_cond [x0] (I : eqType) r r' P P' (F : I -> T) :
{subset ([seq i <- r | P i]) <= ([seq i <- r' | P' i])} ->
\big[max/x0]_(i <- r | P i) F i <= \big[max/x0]_(i <- r' | P' i) F i.

Proof.

exact: (idem_sub_le_big_cond _ _ maxxx). Qed.

Lemma sub_in_bigmin [x0] [I : eqType] (r : seq I) (P P' : {pred I}) F :
{in r, forall i, P' i -> P i} ->
\big[min/x0]_(i <- r | P i) F i <= \big[min/x0]_(i <- r | P' i) F i.

Proof.

exact: (sub_in_le_big ge_refl). Qed.

Lemma sub_in_bigmax [x0] [I : eqType] (r : seq I) (P P' : {pred I}) F :
{in r, forall i, P i -> P' i} ->
\big[max/x0]_(i <- r | P i) F i <= \big[max/x0]_(i <- r | P' i) F i.

Proof.

exact: sub_in_le_big. Qed.

Lemma le_bigmin_nat [x0] n m n' m' P (F : nat -> T) :
(n <= n')%N -> (m' <= m)%N ->
\big[min/x0]_(n <= i < m | P i) F i <= \big[min/x0]_(n' <= i < m' | P i) F i.

Proof.

exact: (le_big_nat ge_refl). Qed.

Lemma le_bigmax_nat [x0] n m n' m' P (F : nat -> T) :
(n' <= n)%N -> (m <= m')%N ->
\big[max/x0]_(n <= i < m | P i) F i <= \big[max/x0]_(n' <= i < m' | P i) F i.

Proof.

exact: le_big_nat. Qed.

Lemma le_bigmin_nat_cond [x0] n m n' m' (P P' : pred nat) (F : nat -> T) :
(n <= n')%N -> (m' <= m)%N -> (forall i, (n' <= i < m')%N -> P' i -> P i) ->
\big[min/x0]_(n <= i < m | P i) F i <= \big[min/x0]_(n' <= i < m' | P' i) F i.

Proof.

exact: (le_big_nat_cond ge_refl). Qed.

Lemma le_bigmax_nat_cond [x0] n m n' m' (P P' : {pred nat}) (F : nat -> T) :
(n' <= n)%N -> (m <= m')%N -> (forall i, (n <= i < m)%N -> P i -> P' i) ->
\big[max/x0]_(n <= i < m | P i) F i <= \big[max/x0]_(n' <= i < m' | P' i) F i.

Proof.

exact: le_big_nat_cond. Qed.

Lemma le_bigmin_ord [x0] n m (P : pred nat) (F : nat -> T) : (m <= n)%N ->
\big[min/x0]_(i < n | P i) F i <= \big[min/x0]_(i < m | P i) F i.

Proof.

exact: (le_big_ord ge_refl). Qed.

Lemma le_bigmax_ord [x0] n m (P : {pred nat}) (F : nat -> T) : (n <= m)%N ->
\big[max/x0]_(i < n | P i) F i <= \big[max/x0]_(i < m | P i) F i.

Proof.

exact: le_big_ord. Qed.

Lemma le_bigmin_ord_cond [x0] n m (P P' : pred nat) (F : nat -> T) :
(m <= n)%N -> (forall i : 'I_m, P' i -> P i) ->
\big[min/x0]_(i < n | P i) F i <= \big[min/x0]_(i < m | P' i) F i.

Proof.

exact: (le_big_ord_cond ge_refl). Qed.

Lemma le_bigmax_ord_cond [x0] n m (P P' : {pred nat}) (F : nat -> T) :
(n <= m)%N -> (forall i : 'I_n, P i -> P' i) ->
\big[max/x0]_(i < n | P i) F i <= \big[max/x0]_(i < m | P' i) F i.

Proof.

exact: le_big_ord_cond. Qed.

Lemma subset_bigmin [x0] [I : finType] [A A' P : {pred I}] (F : I -> T) :
A' \subset A ->
\big[min/x0]_(i in A | P i) F i <= \big[min/x0]_(i in A' | P i) F i.

Proof.

exact: (subset_le_big ge_refl). Qed.

Lemma subset_bigmax [x0] [I : finType] (A A' P : {pred I}) (F : I -> T) :
A \subset A' ->
\big[max/x0]_(i in A | P i) F i <= \big[max/x0]_(i in A' | P i) F i.

Proof.

exact: subset_le_big. Qed.

Lemma subset_bigmin_cond [x0] (I : finType) (A A' P P' : {pred I}) (F : I -> T) :
[set i in A' | P' i] \subset [set i in A | P i] ->
\big[min/x0]_(i in A | P i) F i <= \big[min/x0]_(i in A' | P' i) F i.

Proof.

exact: (subset_le_big_cond ge_refl). Qed.

Lemma subset_bigmax_cond [x0] (I : finType) (A A' P P' : {pred I}) (F : I -> T) :
[set i in A | P i] \subset [set i in A' | P' i] ->
\big[max/x0]_(i in A | P i) F i <= \big[max/x0]_(i in A' | P' i) F i.

Proof.

exact: subset_le_big_cond. Qed.

Section bigminmax_Type.
Context (I : Type) (r : seq I) (x : T).
Implicit Types (P : pred I) (F : I -> T).

Lemma bigmin_le_id P F : \big[min/x]_(i <- r | P i) F i <= x.

Proof.

by rewrite bigmin_idl. Qed.

Lemma bigmax_ge_id P F : \big[max/x]_(i <- r | P i) F i >= x.

Proof.

by rewrite bigmax_idl. Qed.

Lemma bigmin_eq_id P F :
(forall i, P i -> x <= F i) -> \big[min/x]_(i <- r | P i) F i = x.

Proof.

by move=> x_le; apply: le_anti; rewrite bigmin_le_id le_bigmin. Qed.

Lemma bigmax_eq_id P F :
(forall i, P i -> x >= F i) -> \big[max/x]_(i <- r | P i) F i = x.

Proof.

by move=> x_ge; apply: le_anti; rewrite bigmax_ge_id bigmax_le. Qed.

End bigminmax_Type.

Section bigminmax_eqType.
Context (I : eqType) (r : seq I) (x : T).
Implicit Types (P : pred I) (F : I -> T).

Lemma ge_bigmin_seq i0 P F :
i0 \in r -> P i0 -> \big[min/x]_(i <- r | P i) F i <= F i0.

Proof.

move=> + Pi0; elim: r => // h t ih; rewrite inE big_cons.
move=> /predU1P[<-|i0t]; first by rewrite Pi0 ge_min// lexx.
by case: ifPn => Ph; [rewrite ge_min ih// orbT|rewrite ih].
Qed.

Lemma le_bigmax_seq i0 P F :
i0 \in r -> P i0 -> F i0 <= \big[max/x]_(i <- r | P i) F i.

Proof.

move=> + Pi0; elim: r => // h t ih; rewrite inE big_cons.
move=> /predU1P[<-|i0t]; first by rewrite Pi0 le_max// lexx.
by case: ifPn => Ph; [rewrite le_max ih// orbT|rewrite ih].
Qed.

Lemma bigmin_inf_seq i0 P t F :
i0 \in r -> P i0 -> F i0 <= t -> \big[min/x]_(i <- r | P i) F i <= t.

Proof.

by move=> ? ? ?; exact: le_trans (@ge_bigmin_seq i0 _ _ _ _) _. Qed.

Lemma bigmax_sup_seq i0 P t F :
i0 \in r -> P i0 -> t <= F i0 -> t <= \big[max/x]_(i <- r | P i) F i.

Proof.

by move=> ? ? ?; exact: le_trans (@le_bigmax_seq i0 _ _ _ _). Qed.

End bigminmax_eqType.

Section bigminmax_finType.
Context (I : finType) (x : T).
Implicit Types (P : pred I) (F : I -> T).

Lemma bigminD1 j P F : P j ->
\big[min/x]_(i | P i) F i = min (F j) (\big[min/x]_(i | P i && (i != j)) F i).

Proof.

by move/(bigD1 _) ->. Qed.

Lemma bigmaxD1 j P F : P j ->
\big[max/x]_(i | P i) F i = max (F j) (\big[max/x]_(i | P i && (i != j)) F i).

Proof.

by move/(bigD1 _) ->. Qed.

Lemma bigmin_le_cond j P F : P j -> \big[min/x]_(i | P i) F i <= F j.

Proof.

have := mem_index_enum j; rewrite unlock; elim: (index_enum I) => //= i l ih.
rewrite inE => /orP [/eqP-> ->|/ih leminlfi Pi]; first by rewrite ge_min lexx.
by case: ifPn => Pj; [rewrite ge_min leminlfi// orbC|exact: leminlfi].
Qed.

Lemma le_bigmax_cond j P F : P j -> F j <= \big[max/x]_(i | P i) F i.

Proof.

by move=> Pj; rewrite (bigmaxD1 _ Pj) le_max lexx. Qed.

Lemma bigmin_le j F : \big[min/x]_i F i <= F j.

Proof.

exact: bigmin_le_cond. Qed.

Lemma le_bigmax F j : F j <= \big[max/x]_i F i.

Proof.

exact: le_bigmax_cond. Qed.

Lemma bigmin_inf j P m F : P j -> F j <= m -> \big[min/x]_(i | P i) F i <= m.

Proof.

by move=> Pj ?; apply: le_trans (bigmin_le_cond _ Pj) _. Qed.

Files

Module mathcomp.order.order