diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 4 | ||||
| -rw-r--r-- | mathcomp/ssreflect/order.v | 212 |
2 files changed, 151 insertions, 65 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 943f404..b4cc0ec 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -9,6 +9,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). ## [Unreleased] ### Added +- Arithmetic theorems in ssrnat, div and prime about `logn`, + `coprime`, `gcd`, `lcm` and `partn`: `logn_coprime`, `logn_gcd`, + `logn_lcm`, `eq_partn_from_log` and `eqn_from_log`. - Lemmas `ltnNleqif`, `eq_leqif`, `eqTleqif` in `ssrnat` @@ -115,4 +118,3 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). ### Infrastructure ### Misc - diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index 572c9ae..718eea5 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -5,7 +5,8 @@ From mathcomp Require Import path fintype tuple bigop finset div prime. (******************************************************************************) (* This files defines types equipped with order relations. *) -(* It contains several modules implementing different theories: *) +(* *) +(* 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. *) @@ -18,45 +19,79 @@ From mathcomp Require Import path fintype tuple bigop finset div prime. (* delimiting key "O". *) (* *) (* We provide the following structures of ordered types *) -(* porderType == the type of partially ordered types *) -(* distrLatticeType == the type of distributive lattices *) -(* bDistrLatticeType == distrLatticeType with a bottom element *) -(* tbDistrLatticeType == distrLatticeType with both a top and a bottom *) -(* cbDistrLatticeType == the type of sectionally complemented distributive *) -(* lattices *) -(* (lattices with bottom and a difference operation) *) -(* ctbDistrLatticeType == the type of complemented distributive lattices *) -(* (lattices with top, bottom, difference, complement)*) -(* orderType == the type of totally ordered types *) -(* finPOrderType == the type of partially ordered finite types *) -(* finDistrLatticeType == the type of nonempty finite distributive lattices *) -(* finCDistrLatticeType == the type of nonempty finite complemented *) -(* distributive lattices *) -(* finOrderType == the type of nonempty totally ordered finite types *) +(* porderType d == the type of partially ordered types *) +(* 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 *) +(* 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 adter 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) *) +(* For distrLatticeType T *) +(* @Order.meet disp T x y == x `&` y (in order_scope) *) +(* @Order.join disp T x y == x `|` y (in order_scope) *) +(* For bDistrLatticeType T *) +(* @Order.bottom disp T == 0 (in order_scope) *) +(* For tbDistrLatticeType 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) *) (* *) -(* Each of these structures take a first argument named display, of type *) -(* unit. Instantiating it with tt or an unknown key will lead to a default *) -(* display for notations, i.e. over these structures, we have: *) +(* 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)). *) (* x >= y <-> x is greater than or equal to y (:= y <= x). *) (* x > y <-> x is greater than y (:= y < x). *) (* x <= y ?= iff C <-> x is less than y, or equal iff C is true. *) (* x >=< y <-> x and y are comparable (:= (x <= y) || (y <= x)). *) -(* x >< y <-> x and y are incomparable. *) -(* For lattices we provide the following operations *) +(* x >< y <-> x and y are incomparable (:= ~~ x >=< y). *) +(* For x, y of type T, where T is canonically a distrLatticeType 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 bDistrLatticeType 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 tbDistrLatticeType 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]. *) -(* \meet_<range> e == iterated meet of a lattice with a top. *) -(* \join_<range> e == iterated join of a lattice with a bottom. *) (* *) (* There are three distinct uses of the symbols *) -(* <, <=, >, >=, _ <= _ ?= iff _, >=<, and ><: *) -(* 0-ary, unary (prefix), and binary (infix). *) +(* <, <=, >, >=, _ <= _ ?= 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 *) @@ -70,25 +105,73 @@ From mathcomp Require Import path fintype tuple bigop finset div prime. (* 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 canoincal porderType structures using *) +(* 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 := @le my_display _ x y` or *) -(* `Notation "x <<< y" := @lt my_display _ x y (at level ...)` *) +(* `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 desambiguate between *) -(* different structures defined on copies of one. Two examples of this are *) -(* given in this library: *) -(* - the converse ordered structures. If T is an ordered type (and in *) -(* particular porderType d), then T^c is a copy of T with the same ordered *) -(* structures but with the display (converse_display d) which prints all *) -(* of the above notations with an addition ^c in the notation (<=^c ...) *) -(* - natural number in divisibility order. The type natdvd is a copy of nat *) -(* where the canonical order is given by dvdn and meet and join by gcdn *) -(* and lcmn. The display is dvd_display and overloads le using %|, lt using *) -(* %<| and meet and join using gcd and lcm. *) +(* 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^c := converse T, *) +(* where converse is a new definition for (fun T => T) *) +(* == a "copy" of T, such that if T is canonically ordered, *) +(* then T^c is canonically ordered with the converse *) +(* order, and displayed with an extra ^c in the notation *) +(* i.e. <=^c, <^c, >=<^c, ><^c, `&`^c, `|`^c 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 *) (* *) (* Beware that canonical structure inference will not try to find the copy of *) (* the structures that fits the display one mentioned, but will rather *) @@ -105,7 +188,7 @@ From mathcomp Require Import path fintype tuple bigop finset div prime. (* The default display is tt and users can define their own as explained *) (* above. *) (* *) -(* For orderType we provide the following operations *) +(* For orderType we provide the following operations (in total_display) *) (* [arg minr_(i < i0 | P) M] == a value i : T minimizing M : R, subject to *) (* the condition P (i may appear in P and M), and *) (* provided P holds for i0. *) @@ -115,6 +198,7 @@ From mathcomp Require Import path fintype tuple bigop finset div prime. (* [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 *) (* *) (* In order to build the above structures, one must provide the appropriate *) (* mixin to the following structure constructors. The list of possible mixins *) @@ -160,7 +244,7 @@ From mathcomp Require Import path fintype tuple bigop finset div prime. (* *) (* Additionally: *) (* - [porderType of _] ... notations are available to recover structures on *) -(* copies of the types, as in eqtype, choicetype, ssralg... *) +(* "copies" of the types, as in eqtype, choicetype, ssralg... *) (* - [finPOrderType of _] ... notations to compute joins between finite types *) (* and ordered types *) (* *) @@ -225,27 +309,27 @@ From mathcomp Require Import path fintype tuple bigop finset div prime. (* are respectively gcdn and lcmn *) (* - porderType, distrLatticeType, orderType, bDistrLatticeType, *) (* tbDistrLatticeType, cbDistrLatticeType, ctbDistrLatticeType *) -(* on T *prod[disp] T' a copy of T * T' *) +(* on T *prod[disp] T' a "copy" of T * T' *) (* using product order (and T *p T' its specialization to prod_display) *) (* - porderType, distrLatticeType, and orderType, on T *lexi[disp] T' *) -(* another copy of T * T', with lexicographic ordering *) +(* another "copy" of T * T', with lexicographic ordering *) (* (and T *l T' its specialization to lexi_display) *) (* - porderType, distrLatticeType, and orderType, on {t : T & T' x} *) (* with lexicographic ordering *) (* - porderType, distrLatticeType, orderType, bDistrLatticeType, *) (* cbDistrLatticeType, tbDistrLatticeType, ctbDistrLatticeType *) -(* on seqprod_with disp T a copy of seq T *) +(* on seqprod_with disp T a "copy" of seq T *) (* using product order (and seqprod T' its specialization to prod_display)*) (* - porderType, distrLatticeType, and orderType, on seqlexi_with disp T *) -(* another copy of seq T, with lexicographic ordering *) +(* another "copy" of seq T, with lexicographic ordering *) (* (and seqlexi T its specialization to lexi_display) *) (* - porderType, distrLatticeType, orderType, bDistrLatticeType, *) (* cbDistrLatticeType, tbDistrLatticeType, ctbDistrLatticeType *) -(* on n.-tupleprod[disp] a copy of n.-tuple T *) +(* on n.-tupleprod[disp] a "copy" of n.-tuple T *) (* using product order (and n.-tupleprod T its specialization *) (* to prod_display) *) (* - porderType, distrLatticeType, and orderType, on n.-tuplelexi[d] T *) -(* another copy of n.-tuple T, with lexicographic ordering *) +(* another "copy" of n.-tuple T, with lexicographic ordering *) (* (and n.-tuplelexi T its specialization to lexi_display) *) (* and all possible finite type instances *) (* *) @@ -3972,12 +4056,12 @@ Import SubOrder.Exports. (* We declare two distinct canonical orders: *) (* - leq which is total, and where meet and join are minn and maxn, on nat *) (* - dvdn which is partial, and where meet and join are gcdn and lcmn, *) -(* on a copy of nat we name natdiv *) +(* on a "copy" of nat we name natdiv *) (******************************************************************************) (******************************************************************************) (* The Module NatOrder defines leq as the canonical order on the type nat, *) -(* i.e. without creating a copy. We use the predefined total_display, which *) +(* i.e. without creating a "copy". We use the predefined total_display, which *) (* is designed to parse and print meet and join as minn and maxn. This looks *) (* like standard canonical structure declaration, except we use a display. *) (* We also use a single factory LeOrderMixin to instanciate three different *) @@ -4119,7 +4203,7 @@ End DvdSyntax. (* is abbreviated using the notation natdvd at the end of the module. *) (* We use the newly defined dvd_display, described above. This looks *) (* like standard canonical structure declaration, except we use a display and *) -(* we declare it on a copy of the type. *) +(* we declare it on a "copy" of the type. *) (* We first recover structures that are common to both nat and natdiv *) (* (eqType, choiceType, countType) through the clone mechanisms, then we use *) (* a single factory MeetJoinMixin to instanciate both porderType and *) @@ -4502,10 +4586,10 @@ Notation "\min^l_ ( i 'in' A ) F" := End LexiSyntax. -(***********************************************) -(* We declare a copy of the cartesian product, *) -(* which has canonical product order. *) -(***********************************************) +(*************************************************) +(* We declare a "copy" of the cartesian product, *) +(* which has canonical product order. *) +(*************************************************) Module ProdOrder. Section ProdOrder. @@ -4888,10 +4972,10 @@ End Exports. End SigmaOrder. Import SigmaOrder.Exports. -(***********************************************) -(* We declare a copy of the cartesian product, *) -(* which has canonical lexicographic order. *) -(***********************************************) +(*************************************************) +(* We declare a "copy" of the cartesian product, *) +(* which has canonical lexicographic order. *) +(*************************************************) Module ProdLexiOrder. Section ProdLexiOrder. @@ -5067,10 +5151,10 @@ Canonical prodlexi_finOrderType (T : finOrderType disp1) End DefaultProdLexiOrder. End DefaultProdLexiOrder. -(***************************************) -(* We declare a copy of the sequences, *) -(* which has canonical product order. *) -(***************************************) +(*****************************************) +(* We declare a "copy" of the sequences, *) +(* which has canonical product order. *) +(*****************************************) Module SeqProdOrder. Section SeqProdOrder. @@ -5240,7 +5324,7 @@ End DefaultSeqProdOrder. End DefaultSeqProdOrder. (*********************************************) -(* We declare a copy of the sequences, *) +(* We declare a "copy" of the sequences, *) (* which has canonical lexicographic order. *) (*********************************************) @@ -5417,7 +5501,7 @@ End DefaultSeqLexiOrder. End DefaultSeqLexiOrder. (***************************************) -(* We declare a copy of the tuples, *) +(* We declare a "copy" of the tuples, *) (* which has canonical product order. *) (***************************************) @@ -5698,7 +5782,7 @@ End DefaultTupleProdOrder. End DefaultTupleProdOrder. (*********************************************) -(* We declare a copy of the tuples, *) +(* We declare a "copy" of the tuples, *) (* which has canonical lexicographic order. *) (*********************************************) |