Library mathcomp.ssreflect.order

This files defines types equipped with order relations. Use one of the following modules implementing different theories: Order.LTheory: partially ordered types and lattices excluding complement and totality related theorems. Order.CTheory: complemented lattices including Order.LTheory. Order.TTheory: totally ordered types including Order.LTheory. Order.Theory: ordered types including all of the above theory modules To access the definitions, notations, and the theory from, say, "Order.Xyz", insert "Import Order.Xyz." at the top of your scripts. Notations are accessible by opening the scope "order_scope" bound to the delimiting key "O". We provide the following structures of ordered types porderType d == the type of partially ordered types latticeType d == the type of non-distributive lattices bLatticeType d == latticeType with a bottom element tbLatticeType d == latticeType with both a top and a bottom distrLatticeType d == the type of distributive lattices bDistrLatticeType d == distrLatticeType with a bottom element tbDistrLatticeType d == distrLatticeType with both a top and a bottom cbDistrLatticeType d == the type of sectionally complemented distributive lattices (lattices with bottom and a difference operation) ctbDistrLatticeType d == the type of complemented distributive lattices (lattices with top, bottom, difference, and complement) orderType d == the type of totally ordered types finPOrderType d == the type of partially ordered finite types finLatticeType d == the type of nonempty finite non-distributive lattices finDistrLatticeType d == the type of nonempty finite distributive lattices finCDistrLatticeType d == the type of nonempty finite complemented distributive lattices finOrderType d == the type of nonempty totally ordered finite types Each generic partial order and lattice operations symbols also has a first argument which is the display, the second which is the minimal structure they operate on and then the operands. Here is the exhaustive list of all such symbols for partial orders and lattices together with their default display (as displayed by Check). We document their meaning in the paragraph after the next. For porderType T @Order.le disp T == <=%O (in fun_scope) @Order.lt disp T == <%O (in fun_scope) @Order.comparable disp T == >=<%O (in fun_scope) @Order.ge disp T == >=%O (in fun_scope) @Order.gt disp T == >%O (in fun_scope) @Order.leif disp T == <?=%O (in fun_scope) @Order.lteif disp T == <?<=%O (in fun_scope) For latticeType T @Order.meet disp T x y == x `&` y (in order_scope) @Order.join disp T x y == x `|` y (in order_scope) For bLatticeType T @Order.bottom disp T == 0 (in order_scope) For tbLatticeType T @Order.top disp T == 1 (in order_scope) For cbDistrLatticeType T @Order.sub disp T x y == x `|` y (in order_scope) For ctbDistrLatticeType T @Order.compl disp T x == ~` x (in order_scope) This first argument named either d, disp or display, of type unit, configures the printing of notations. Instantiating d with tt or an unknown key will lead to a default display for notations, i.e. we have: For x, y of type T, where T is canonically a porderType d: x <= y <-> x is less than or equal to y. x < y <-> x is less than y (:= (y != x) && (x <= y)). min x y <-> if x < y then x else y max x y <-> if x < y then y else x x >= y <-> x is greater than or equal to y (:= y <= x). x > y <-> x is greater than y (:= y < x). x <= y ?= iff C <-> x is less than y, or equal iff C is true. x < y ?<= if C <-> x is smaller than y, and strictly if C is false. x >=< y <-> x and y are comparable (:= (x <= y) || (y <= x)). x >< y <-> x and y are incomparable (:= ~~ x >=< y). f \min g <-> the function x |-> Order.min (f x) (g x); f \min g simplifies on application. f \max g <-> the function x |-> Order.max (f x) (g x); f \max g simplifies on application. For x, y of type T, where T is canonically a latticeType d: x `&` y == the meet of x and y. x `|` y == the join of x and y. In a type T, where T is canonically a bLatticeType d: 0 == the bottom element. \join<range> e == iterated join of a lattice with a bottom. In a type T, where T is canonically a tbLatticeType d: 1 == the top element. \meet<range> e == iterated meet of a lattice with a top. For x, y of type T, where T is canonically a cbDistrLatticeType d: x `\` y == the (sectional) complement of y in [0, x]. For x of type T, where T is canonically a ctbDistrLatticeType d: ~` x == the complement of x in [0, 1]. There are three distinct uses of the symbols <, <=, >, >=, _ <= _ ?= iff _, >=<, and >< in the default display: they can be 0-ary, unary (prefix), and binary (infix). 0. <%O, <=%O, >%O, >=%O, <?=%O, >=<%O, and ><%O stand respectively for lt, le, gt, ge, leif (_ <= _ ?= iff _), comparable, and incomparable. 1. (< x), (<= x), (> x), (>= x), (>=< x), and (>< x) stand respectively for (>%O x), (>=%O x), (<%O x), (<=%O x), (>=<%O x), and (><%O x). So (< x) is a predicate characterizing elements smaller than x. 2. (x < y), (x <= y), ... mean what they are expected to. These conventions are compatible with Haskell's, where ((< y) x) = (x < y) = ((<) x y), except that we write <%O instead of (<). Alternative notation displays can be defined by : 1. declaring a new opaque definition of type unit. Using the idiom `Lemma my_display : unit. Proof. exact: tt. Qed.` 2. using this symbol to tag canonical porderType structures using `Canonical my_porderType := POrderType my_display my_type my_mixin`, 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. One may use displays either for convenience or to disambiguate between different structures defined on "copies" of a type (as explained below.) We provide the following "copies" of types, the first one is a *documented example* natdvd := nat == a "copy" of 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) == a "copy" of 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' == a "copy" of 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] T' where prod_display adds an extra ^p to all notations T *lexi[d] T' := T * T' == a "copy" of 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] T' where lexi_display adds an extra ^l to all notations seqprod_with d T := seq T == a "copy" of 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 prod_display T n.-tupleprod T := n.-tuple[prod_display] T seqlexi_with d T := seq T == a "copy" of 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 lexi_display T n.-tuplelexi T := n.-tuple[lexi_display] T {subset[d] T} := {set T} == a "copy" of set which is canonically ordered by the subset order and displayed in display d {subset T} := {subset[subset_display] T} Beware that canonical structure inference will not try to find the copy of the structures that fits the display one mentioned, but will rather determine which canonical structure and display to use depending on the copy of the type one provided. In this sense they are merely displays to inform the user of what the inference did, rather than additional input for the inference. Existing displays are either dual_display d (where d is a display), dvd_display (both explained above), ring_display (from algebra/ssrnum to change the scope of the usual notations to ring_scope). We also provide lexi_display and prod_display for lexicographic and product order respectively. The default display is tt and users can define their own as explained above. For porderType we provide the following operations [arg min(i < i0 | P) M] == a value i : T minimizing M : R, subject to the condition P (i may appear in P and M), and provided P holds for i0. [arg max(i > i0 | P) M] == a value i maximizing M subject to P and provided P holds for i0. [arg min(i < i0 in A) M] == an i \in A minimizing M if i0 \in A. [arg max(i > i0 in A) M] == an i \in A maximizing M if i0 \in A. [arg min(i < i0) M] == an i : T minimizing M, given i0 : T. [arg max(i > i0) M] == an i : T maximizing M, given i0 : T. with head symbols Order.arg_min and Order.arg_max The user may use extremumP or extremum_inP to eliminate them.

• > patterns for contextual rewriting: leLHS := (X in (X <= _)%O)%pattern leRHS := (X in (_ <= X)%O)%pattern ltLHS := (X in (X < _)%O)%pattern ltRHS := (X in (_ < X)%O)%pattern

In order to build the above structures, one must provide the appropriate factory instance to the following structure constructors. The list of possible factories is indicated after each constructor. Each factory is documented in the next paragraph. NB: Since each mixim_of record of structure in this library is an internal interface that is not designed to be used by users directly, one should not build structure instances from their Mixin constructors. POrderType disp T pord_mixin == builds a porderType from a canonical choiceType instance of T where pord_mixin can be of types lePOrderMixin, ltPOrderMixin, meetJoinMixin, leOrderMixin, or ltOrderMixin or computed using PcanPOrderMixin or CanPOrderMixin. disp is a display as explained above LatticeType T lat_mixin == builds a latticeType from a porderType where lat_mixin can be of types latticeMixin, distrLatticePOrderMixin, totalPOrderMixin, meetJoinMixin, leOrderMixin, or ltOrderMixin or computed using IsoLatticeMixin. BLatticeType T bot_mixin == builds a bLatticeType from a latticeType and bottom where bot_mixin is of type bottomMixin. TBLatticeType T top_mixin == builds a tbLatticeType from a bLatticeType and top where top_mixin is of type topMixin. DistrLatticeType T lat_mixin == builds a distrLatticeType from a porderType where lat_mixin can be of types distrLatticeMixin, distrLatticePOrderMixin, totalLatticeMixin, totalPOrderMixin, meetJoinMixin, leOrderMixin, or ltOrderMixin or computed using IsoLatticeMixin. CBDistrLatticeType T sub_mixin == builds a cbDistrLatticeType from a bDistrLatticeType and a difference operation where sub_mixin is of type cbDistrLatticeMixin. CTBDistrLatticeType T compl_mixin == builds a ctbDistrLatticeType from a tbDistrLatticeType and a complement operation where compl_mixin is of type ctbDistrLatticeMixin. OrderType T ord_mixin == builds an orderType from a distrLatticeType where ord_mixin can be of types totalOrderMixin, totalPOrderMixin, totalLatticeMixin, leOrderMixin, or ltOrderMixin or computed using MonoTotalMixin. Additionally:

• [porderType of _ ] ... notations are available to recover structures on "copies" of the types, as in eqType, choiceType, ssralg...
• [finPOrderType of _ ] ... notations to compute joins between finite types and ordered types

List of possible factories:

• lePOrderMixin == on a choiceType, takes le, lt, reflexivity, antisymmetry and transitivity of le. (can build: porderType)
• ltPOrderMixin == on a choiceType, takes le, lt, irreflexivity and transitivity of lt. (can build: porderType)
• latticeMixin == on a porderType, takes meet, join, commutativity and associativity of meet and join, and some absorption laws. (can build: latticeType)
• distrLatticeMixin == on a latticeType, takes distributivity of meet over join. (can build: distrLatticeType)
• distrLatticePOrderMixin == on a porderType, takes meet, join, commutativity and associativity of meet and join, and the absorption and distributive laws. (can build: latticeType, distrLatticeType)
• meetJoinMixin == on a choiceType, takes le, lt, meet, join, commutativity and associativity of meet and join, the absorption and distributive laws, and idempotence of meet. (can build: porderType, latticeType, distrLatticeType)
• meetJoinLeMixin == on a porderType, takes meet, join, and a proof that those are respectvely the greatest lower bound and the least upper bound. (can build: latticeType)
• leOrderMixin == on a choiceType, takes le, lt, meet, join, antisymmetry, transitivity and totality of le. (can build: porderType, latticeType, distrLatticeType, orderType)
• ltOrderMixin == on a choiceType, takes le, lt, meet, join, irreflexivity, transitivity and totality of lt. (can build: porderType, latticeType, distrLatticeType, orderType)
• totalPOrderMixin == on a porderType T, totality of the order of T := total (<=%O : rel T) (can build: latticeType, distrLatticeType, orderType)
• totalLatticeMixin == on a latticeType T, totality of the order of T := total (<=%O : rel T) (can build distrLatticeType, orderType)
• totalOrderMixin == on a distrLatticeType T, totality of the order of T := total (<=%O : rel T) (can build: orderType) NB: the above three mixins are kept separate from each other (even though they are convertible), in order to avoid ambiguous coercion paths.
• bottomMixin, topMixin, cbDistrLatticeMixin, ctbDistrLatticeMixin == mixins with one extra operation (respectively bottom, top, difference, and complement)

Additionally:

• [porderMixin of T by <: ] creates a porderMixin by subtyping.
• [totalOrderMixin of T by <: ] creates the associated totalOrderMixin.
• PCanPOrderMixin, CanPOrderMixin create porderMixin from cancellations
• MonoTotalMixin creates a totalPOrderMixin from monotonicity
• IsoLatticeMixin creates a distrLatticeMixin from an ordered structure isomorphism (i.e., cancel f f', cancel f' f, {mono f : x y / x <= y})

List of "big pack" notations:

• DistrLatticeOfChoiceType builds a distrLatticeType from a choiceType and a meetJoinMixin.
• DistrLatticeOfPOrderType builds a distrLatticeType from a porderType and a distrLatticePOrderMixin.
• OrderOfChoiceType builds an orderType from a choiceType, and a leOrderMixin or a ltOrderMixin.
• OrderOfPOrder builds an orderType from a porderType and a totalPOrderMixin.
• OrderOfLattice builds an orderType from a latticeType and a totalLatticeMixin.

NB: These big pack notations should be used only to construct instances on the fly, e.g., in the middle of a proof, and should not be used to declare canonical instances. See field/algebraics_fundamentals.v for an example usage. We provide the following canonical instances of ordered types

• all possible structures on bool
• porderType, latticeType, distrLatticeType, orderType and bLatticeType on nat for the leq order
• porderType, latticeType, distrLatticeType, orderType and finPOrderType on 'I_n and bLatticeType, tbLatticeType, bDistrLatticeType, tbDistrLatticeType, finLatticeType, finDistrLatticeType and finOrderType on 'I_n.+1 (to guarantee it is nonempty).
• porderType, latticeType, distrLatticeType, bLatticeType, tbLatticeType, on nat for the dvdn order, where meet and join are respectively gcdn and lcmn
• porderType, latticeType, distrLatticeType, orderType, bLatticeType, tbLatticeType, cbDistrLatticeType, ctbDistrLatticeType on T *prod[disp] T' a "copy" of T * T' using product order (and T *p T' its specialization to prod_display)
• porderType, latticeType, distrLatticeType, and orderType, on T *lexi[disp] T' another "copy" of T * T', with lexicographic ordering (and T *l T' its specialization to lexi_display)
• porderType, latticeType, distrLatticeType, and orderType, on {t : T & T' x} with lexicographic ordering
• porderType, latticeType, distrLatticeType, orderType, bLatticeType, tbLatticeType, cbDistrLatticeType, ctbDistrLatticeType on seqprod_with disp T a "copy" of seq T using product order (and seqprod T' its specialization to prod_display)
• porderType, latticeType, distrLatticeType, and orderType, on seqlexi_with disp T another "copy" of seq T, with lexicographic ordering (and seqlexi T its specialization to lexi_display)
• porderType, latticeType, distrLatticeType, orderType, bLatticeType, tbLatticeType, cbDistrLatticeType, ctbDistrLatticeType on n.-tupleprod[disp] a "copy" of n.-tuple T using product order (and n.-tupleprod T its specialization to prod_display)
• porderType, latticeType, distrLatticeType, and orderType, on n.-tuplelexi[d] T another "copy" of n.-tuple T, with lexicographic ordering (and n.-tuplelexi T its specialization to lexi_display)
• porderType, latticeType, distrLatticeType, orderType, bLatticeType, tbLatticeType, cbDistrLatticeType, ctbDistrLatticeType on {subset[disp] T} a "copy" of {set T} using subset order (and {subset T} its specialization to subset_display)

and all possible finite type instances 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. On orderType, leP ltP ltgtP are the three main lemmas for case analysis. On porderType, one may use comparableP, comparable_leP, comparable_ltP, and comparable_ltgtP, which are the four main lemmas for case analysis. We also provide specialized versions of some theorems from path.v. We provide Order.enum_val, Order.enum_rank, and Order.enum_rank_in, which are monotonous 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) This file is based on prior work by D. Dreyer, G. Gonthier, A. Nanevski, P-Y Strub, B. Ziliani

Reserved notation for lattice operations.

Notations for dual partial and total order

Reserved notation for dual lattice operations.

Reserved notations for product ordering of prod or seq

Reserved notation for dual lattice operations.

Reserved notations for lexicographic ordering of prod or seq

Reserved notations for divisibility

Reserved notation for dual lattice operations.

STRUCTURES

TODO: print nice error message when keyed type is not provided

Bind Scope order_scope with POrder.sort.

Lifted min/max operations.

HB.mixin Record POrder_isJoinSemiLattice d (T : indexed Type) of POrder d T := { join : T -> T -> T; joinC : commutative join; joinA : associative join; le_defU : forall x y, (x <= y) = (join x y == y); }. # [short(type="joinSemiLatticeType") ] HB.structure Definition JoinSemiLattice d := { T of POrder_isJoinSemiLattice d T & POrder d T }. HB.mixin Record POrder_isMeetSemiLattice d (T : indexed Type) of POrder d T := { meet : T -> T -> T; meetC : commutative meet; meetA : associative meet; le_def : forall x y, (x <= y) = (meet x y == x); }. # [short(type="meetSemiLatticeType") ] HB.structure Definition MeetSemiLattice d := { T of POrder_isMeetSemiLattice d T & POrder d T }.

HB.builders Context d T of POrder_isLattice d T. Let le_defU : forall x y, (x <= y) = (join x y == y). Proof. Admitted. HB.instance Definition _ := @POrder_isMeetSemiLattice.Build d T meet meetC meetA le_def. HB.instance Definition _ := @POrder_isJoinSemiLattice.Build d T join joinC joinA le_defU. HB.end.

TODO: Restore when we remove the mathcomp attribute HB.structure Definition BPOrder d := { T of hasBottom d T & POrder d T }.

Notation " [ 'bLatticeType' 'of' T 'for' cT 'with' disp ]" := (@clone_with T _ cT disp _ id) (at level 0, format " [ 'bLatticeType' 'of' T 'for' cT 'with' disp ]") : form_scope. Notation " [ 'bLatticeType' 'of' T 'with' disp ]" := [bLatticeType of T for _ with disp] (at level 0, format " [ 'bLatticeType' 'of' T 'with' disp ]") : form_scope.

TODO: Restore when we remove the mathcomp attribute HB.structure Definition TPOrder d := { T of hasBottom d T & POrder d T }. HB.structure Definition TLattice d := { T of hasTop d T & Lattice d T }. HB.structure Definition TBOrder d := { T of hasTop d T & BPOrder d T }.

FIXME: clone?

TODO: rename to lattice_ismeet_distributive ?

FIXME: clone?

Notation " [ 'cbDistrLatticeType' 'of' T 'for' cT ]" := (@CBDistrLattice.clone _ T%type cT) (at level 0, format " [ 'cbDistrLatticeType' 'of' T 'for' cT ]") : form_scope. Notation " [ 'cbDistrLatticeType' 'of' T 'for' cT 'with' disp ]" := (@CBDistrLattice.clone disp T%type cT) (at level 0, format " [ 'cbDistrLatticeType' 'of' T 'for' cT 'with' disp ]") : form_scope. Notation " [ 'cbDistrLatticeType' 'of' T ]" := [cbDistrLatticeType of T for _ ] (at level 0, format " [ 'cbDistrLatticeType' 'of' T ]") : form_scope. Notation " [ 'cbDistrLatticeType' 'of' T 'with' disp ]" := [cbDistrLatticeType of T for _ with disp] (at level 0, format " [ 'cbDistrLatticeType' 'of' T 'with' disp ]") : form_scope.

Notation " [ 'ctbDistrLatticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ id) (at level 0, format " [ 'ctbDistrLatticeType' 'of' T 'for' cT ]") : form_scope. Notation " [ 'ctbDistrLatticeType' 'of' T 'for' cT 'with' disp ]" := (@clone_with T _ cT disp _ id) (at level 0, format " [ 'ctbDistrLatticeType' 'of' T 'for' cT 'with' disp ]") : form_scope. Notation " [ 'ctbDistrLatticeType' 'of' T ]" := [ctbDistrLatticeType of T for _ ] (at level 0, format " [ 'ctbDistrLatticeType' 'of' T ]") : form_scope. Notation " [ 'ctbDistrLatticeType' 'of' T 'with' disp ]" := [ctbDistrLatticeType of T for _ with disp] (at level 0, format " [ 'ctbDistrLatticeType' 'of' T 'with' disp ]") : form_scope. Notation " [ 'default_ctbDistrLatticeType' 'of' T ]" := (@pack T _ id _ id (Mixin (fun=> erefl))) (at level 0, format " [ 'default_ctbDistrLatticeType' 'of' T ]") : form_scope.

Notation " [ 'orderType' 'of' T 'for' cT ]" := (@clone T _ cT _ id) (at level 0, format " [ 'orderType' 'of' T 'for' cT ]") : form_scope. Notation " [ 'orderType' 'of' T 'for' cT 'with' disp ]" := (@clone_with T _ cT disp _ id) (at level 0, format " [ 'orderType' 'of' T 'for' cT 'with' disp ]") : form_scope. Notation " [ 'orderType' 'of' T ]" := [orderType of T for _ ] (at level 0, format " [ 'orderType' 'of' T ]") : form_scope. Notation " [ 'orderType' 'of' T 'with' disp ]" := [orderType of T for _ with disp] (at level 0, format " [ 'orderType' 'of' T 'with' disp ]") : form_scope.

FINITE