diff options
| -rw-r--r-- | .gitlab-ci.yml | 8 | ||||
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/rat.v | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrint.v | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 98 | ||||
| -rw-r--r-- | mathcomp/field/algebraics_fundamentals.v | 3 | ||||
| -rw-r--r-- | mathcomp/ssreflect/order.v | 1509 |
7 files changed, 850 insertions, 774 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 1be2f3e..87befed 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -145,7 +145,7 @@ coq-dev: - make install except: - /^experiment\/order$/ - - /^pr-(270|388|395)$/ + - /^pr-(270|388|402)$/ ci-fourcolor-8.7: extends: .ci-fourcolor @@ -182,7 +182,7 @@ ci-fourcolor-dev: - make install only: - /^experiment\/order$/ - - /^pr-(270|388|395)$/ + - /^pr-(270|388|402)$/ ci-fourcolor-8.7-270: extends: .ci-fourcolor-270 @@ -210,7 +210,7 @@ ci-fourcolor-dev-270: - make install except: - /^experiment\/order$/ - - /^pr-(270|388|395)$/ + - /^pr-(270|388|402)$/ ci-odd-order-8.7: extends: .ci-odd-order @@ -247,7 +247,7 @@ ci-odd-order-dev: - make install only: - /^experiment\/order$/ - - /^pr-(270|388|395)$/ + - /^pr-(270|388|402)$/ ci-odd-order-8.7-270: extends: .ci-odd-order-270 diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 432cb50..943f404 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -15,7 +15,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - Lemmas `eqEtupe`, `tnthS` and `tnth_nseq` in `tuple` - Ported `order.v` from the finmap library, which provides structures of ordered - sets (`porderType`, `latticeType`, `orderType`, etc.) and its theory. + sets (`porderType`, `distrLatticeType`, `orderType`, etc.) and its theory. ### Changed diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v index 939046e..15cc4fc 100644 --- a/mathcomp/algebra/rat.v +++ b/mathcomp/algebra/rat.v @@ -573,7 +573,7 @@ Definition ratLeMixin : realLeMixin rat_idomainType := (@le_rat_total 0) norm_ratN ge_rat0_norm lt_rat_def. Canonical rat_porderType := POrderType ring_display rat ratLeMixin. -Canonical rat_latticeType := LatticeType rat ratLeMixin. +Canonical rat_distrLatticeType := DistrLatticeType rat ratLeMixin. Canonical rat_orderType := OrderType rat le_rat_total. Canonical rat_numDomainType := NumDomainType rat ratLeMixin. Canonical rat_normedZmodType := NormedZmoduleType rat rat ratLeMixin. diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index b85f0bc..fabe541 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -431,7 +431,7 @@ End intOrdered. End intOrdered. Canonical int_porderType := POrderType ring_display int intOrdered.Mixin. -Canonical int_latticeType := LatticeType int intOrdered.Mixin. +Canonical int_distrLatticeType := DistrLatticeType int intOrdered.Mixin. Canonical int_orderType := OrderType int intOrdered.lez_total. Canonical int_numDomainType := NumDomainType int intOrdered.Mixin. Canonical int_normedZmodType := NormedZmoduleType int int intOrdered.Mixin. diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 6bbf24a..45a79b8 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -728,14 +728,15 @@ Section ClassDef. Record class_of R := Class { base : NumDomain.class_of R; lmixin_disp : unit; - lmixin : Order.Lattice.mixin_of (Order.POrder.Pack lmixin_disp base); + lmixin : Order.DistrLattice.mixin_of (Order.POrder.Pack lmixin_disp base); tmixin_disp : unit; tmixin : Order.Total.mixin_of - (Order.Lattice.Pack tmixin_disp (Order.Lattice.Class lmixin)); + (Order.DistrLattice.Pack + tmixin_disp (Order.DistrLattice.Class lmixin)); }. Local Coercion base : class_of >-> NumDomain.class_of. Local Coercion base2 T (c : class_of T) : Order.Total.class_of T := - @Order.Total.Class _ (Order.Lattice.Class (@lmixin _ c)) _ (@tmixin _ c). + @Order.Total.Class _ (Order.DistrLattice.Class (@lmixin _ c)) _ (@tmixin _ c). Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. @@ -748,7 +749,7 @@ Definition pack := fun mT ldisp l mdisp m & phant_id (@Order.Total.class ring_display mT) (@Order.Total.Class - T (@Order.Lattice.Class T b ldisp l) mdisp m) => + T (@Order.DistrLattice.Class T b ldisp l) mdisp m) => Pack (@Class T b ldisp l mdisp m). Definition eqType := @Equality.Pack cT xclass. @@ -760,24 +761,26 @@ Definition unitRingType := @GRing.UnitRing.Pack cT xclass. Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass. Definition idomainType := @GRing.IntegralDomain.Pack cT xclass. Definition porderType := @Order.POrder.Pack ring_display cT xclass. -Definition latticeType := @Order.Lattice.Pack ring_display cT xclass. +Definition distrLatticeType := @Order.DistrLattice.Pack ring_display cT xclass. Definition orderType := @Order.Total.Pack ring_display cT xclass. Definition numDomainType := @NumDomain.Pack cT xclass. Definition normedZmodType := NormedZmoduleType numDomainType cT xclass. -Definition zmod_latticeType := @Order.Lattice.Pack ring_display zmodType xclass. -Definition ring_latticeType := @Order.Lattice.Pack ring_display ringType xclass. -Definition comRing_latticeType := - @Order.Lattice.Pack ring_display comRingType xclass. -Definition unitRing_latticeType := - @Order.Lattice.Pack ring_display unitRingType xclass. -Definition comUnitRing_latticeType := - @Order.Lattice.Pack ring_display comUnitRingType xclass. -Definition idomain_latticeType := - @Order.Lattice.Pack ring_display idomainType xclass. -Definition normedZmod_latticeType := - @Order.Lattice.Pack ring_display normedZmodType xclass. -Definition numDomain_latticeType := - @Order.Lattice.Pack ring_display numDomainType xclass. +Definition zmod_distrLatticeType := + @Order.DistrLattice.Pack ring_display zmodType xclass. +Definition ring_distrLatticeType := + @Order.DistrLattice.Pack ring_display ringType xclass. +Definition comRing_distrLatticeType := + @Order.DistrLattice.Pack ring_display comRingType xclass. +Definition unitRing_distrLatticeType := + @Order.DistrLattice.Pack ring_display unitRingType xclass. +Definition comUnitRing_distrLatticeType := + @Order.DistrLattice.Pack ring_display comUnitRingType xclass. +Definition idomain_distrLatticeType := + @Order.DistrLattice.Pack ring_display idomainType xclass. +Definition normedZmod_distrLatticeType := + @Order.DistrLattice.Pack ring_display normedZmodType xclass. +Definition numDomain_distrLatticeType := + @Order.DistrLattice.Pack ring_display numDomainType xclass. Definition zmod_orderType := @Order.Total.Pack ring_display zmodType xclass. Definition ring_orderType := @Order.Total.Pack ring_display ringType xclass. Definition comRing_orderType := @@ -820,20 +823,20 @@ Coercion porderType : type >-> Order.POrder.type. Canonical porderType. Coercion numDomainType : type >-> NumDomain.type. Canonical numDomainType. -Coercion latticeType : type >-> Order.Lattice.type. -Canonical latticeType. +Coercion distrLatticeType : type >-> Order.DistrLattice.type. +Canonical distrLatticeType. Coercion orderType : type >-> Order.Total.type. Canonical orderType. Coercion normedZmodType : type >-> NormedZmodule.type. Canonical normedZmodType. -Canonical zmod_latticeType. -Canonical ring_latticeType. -Canonical comRing_latticeType. -Canonical unitRing_latticeType. -Canonical comUnitRing_latticeType. -Canonical idomain_latticeType. -Canonical normedZmod_latticeType. -Canonical numDomain_latticeType. +Canonical zmod_distrLatticeType. +Canonical ring_distrLatticeType. +Canonical comRing_distrLatticeType. +Canonical unitRing_distrLatticeType. +Canonical comUnitRing_distrLatticeType. +Canonical idomain_distrLatticeType. +Canonical normedZmod_distrLatticeType. +Canonical numDomain_distrLatticeType. Canonical zmod_orderType. Canonical ring_orderType. Canonical comRing_orderType. @@ -857,10 +860,11 @@ Section ClassDef. Record class_of R := Class { base : NumField.class_of R; lmixin_disp : unit; - lmixin : Order.Lattice.mixin_of (@Order.POrder.Pack lmixin_disp R base); + lmixin : Order.DistrLattice.mixin_of (@Order.POrder.Pack lmixin_disp R base); tmixin_disp : unit; tmixin : Order.Total.mixin_of - (Order.Lattice.Pack tmixin_disp (Order.Lattice.Class lmixin)); + (Order.DistrLattice.Pack + tmixin_disp (Order.DistrLattice.Class lmixin)); }. Local Coercion base : class_of >-> NumField.class_of. Local Coercion base2 R (c : class_of R) : RealDomain.class_of R := @@ -888,18 +892,18 @@ Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass. Definition idomainType := @GRing.IntegralDomain.Pack cT xclass. Definition porderType := @Order.POrder.Pack ring_display cT xclass. Definition numDomainType := @NumDomain.Pack cT xclass. -Definition latticeType := @Order.Lattice.Pack ring_display cT xclass. +Definition distrLatticeType := @Order.DistrLattice.Pack ring_display cT xclass. Definition orderType := @Order.Total.Pack ring_display cT xclass. Definition realDomainType := @RealDomain.Pack cT xclass. Definition fieldType := @GRing.Field.Pack cT xclass. Definition numFieldType := @NumField.Pack cT xclass. Definition normedZmodType := NormedZmoduleType numDomainType cT xclass. -Definition field_latticeType := - @Order.Lattice.Pack ring_display fieldType xclass. +Definition field_distrLatticeType := + @Order.DistrLattice.Pack ring_display fieldType xclass. Definition field_orderType := @Order.Total.Pack ring_display fieldType xclass. Definition field_realDomainType := @RealDomain.Pack fieldType xclass. -Definition numField_latticeType := - @Order.Lattice.Pack ring_display numFieldType xclass. +Definition numField_distrLatticeType := + @Order.DistrLattice.Pack ring_display numFieldType xclass. Definition numField_orderType := @Order.Total.Pack ring_display numFieldType xclass. Definition numField_realDomainType := @RealDomain.Pack numFieldType xclass. @@ -931,8 +935,8 @@ Coercion porderType : type >-> Order.POrder.type. Canonical porderType. Coercion numDomainType : type >-> NumDomain.type. Canonical numDomainType. -Coercion latticeType : type >-> Order.Lattice.type. -Canonical latticeType. +Coercion distrLatticeType : type >-> Order.DistrLattice.type. +Canonical distrLatticeType. Coercion orderType : type >-> Order.Total.type. Canonical orderType. Coercion realDomainType : type >-> RealDomain.type. @@ -943,10 +947,10 @@ Coercion numFieldType : type >-> NumField.type. Canonical numFieldType. Coercion normedZmodType : type >-> NormedZmodule.type. Canonical normedZmodType. -Canonical field_latticeType. +Canonical field_distrLatticeType. Canonical field_orderType. Canonical field_realDomainType. -Canonical numField_latticeType. +Canonical numField_distrLatticeType. Canonical numField_orderType. Canonical numField_realDomainType. Notation realFieldType := type. @@ -986,7 +990,7 @@ Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass. Definition idomainType := @GRing.IntegralDomain.Pack cT xclass. Definition porderType := @Order.POrder.Pack ring_display cT xclass. Definition numDomainType := @NumDomain.Pack cT xclass. -Definition latticeType := @Order.Lattice.Pack ring_display cT xclass. +Definition distrLatticeType := @Order.DistrLattice.Pack ring_display cT xclass. Definition orderType := @Order.Total.Pack ring_display cT xclass. Definition realDomainType := @RealDomain.Pack cT xclass. Definition fieldType := @GRing.Field.Pack cT xclass. @@ -1020,8 +1024,8 @@ Coercion porderType : type >-> Order.POrder.type. Canonical porderType. Coercion numDomainType : type >-> NumDomain.type. Canonical numDomainType. -Coercion latticeType : type >-> Order.Lattice.type. -Canonical latticeType. +Coercion distrLatticeType : type >-> Order.DistrLattice.type. +Canonical distrLatticeType. Coercion orderType : type >-> Order.Total.type. Canonical orderType. Coercion realDomainType : type >-> RealDomain.type. @@ -1074,7 +1078,7 @@ Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass. Definition idomainType := @GRing.IntegralDomain.Pack cT xclass. Definition porderType := @Order.POrder.Pack ring_display cT xclass. Definition numDomainType := @NumDomain.Pack cT xclass. -Definition latticeType := @Order.Lattice.Pack ring_display cT xclass. +Definition distrLatticeType := @Order.DistrLattice.Pack ring_display cT xclass. Definition orderType := @Order.Total.Pack ring_display cT xclass. Definition realDomainType := @RealDomain.Pack cT xclass. Definition fieldType := @GRing.Field.Pack cT xclass. @@ -1110,8 +1114,8 @@ Coercion numDomainType : type >-> NumDomain.type. Canonical numDomainType. Coercion realDomainType : type >-> RealDomain.type. Canonical realDomainType. -Coercion latticeType : type >-> Order.Lattice.type. -Canonical latticeType. +Coercion distrLatticeType : type >-> Order.DistrLattice.type. +Canonical distrLatticeType. Coercion orderType : type >-> Order.Total.type. Canonical orderType. Coercion fieldType : type >-> GRing.Field.type. @@ -4792,7 +4796,7 @@ by rewrite unfold_in !ler_def subr0 add0r opprB orbC. Qed. Definition totalMixin : - Order.Total.mixin_of (LatticeType R le_total) := le_total. + Order.Total.mixin_of (DistrLatticeType R le_total) := le_total. End RealMixin. diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v index 4fe5f70..4824697 100644 --- a/mathcomp/field/algebraics_fundamentals.v +++ b/mathcomp/field/algebraics_fundamentals.v @@ -589,7 +589,8 @@ have add_Rroot xR p c: {yR | extendsR xR yR & has_Rroot xR p c -> root_in yR p}. pose QyNum : realLtMixin (Q y) := RealLtMixin posD posM posNneg posB posVneg absN absE (rrefl _). pose QyOrder := - OrderType (LatticeType (POrderType ring_display (Q y) QyNum) QyNum) QyNum. + OrderType + (DistrLatticeType (POrderType ring_display (Q y) QyNum) QyNum) QyNum. pose QyNumField := [numFieldType of NumDomainType QyOrder QyNum]. pose Ry := [realFieldType of [realDomainType of QyNumField]]. have archiRy := @rat_algebraic_archimedean Ry _ alg_integral. diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index bfb247f..fb4025d 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -18,19 +18,21 @@ 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 *) -(* latticeType == the type of distributive lattices *) -(* blatticeType == latticeType with a bottom element *) -(* tblatticeType == latticeType with both a top and a bottom *) -(* cblatticeType == the type of sectionally complemented lattices *) -(* (lattices with bottom and a difference operation) *) -(* ctblatticeType == the type of complemented lattices *) -(* (lattices with top, bottom, difference, complement) *) -(* orderType == the type of totally ordered types *) -(* finPOrderType == the type of partially ordered finite types *) -(* finLatticeType == the type of nonempty finite lattices *) -(* finClatticeType == the type of nonempty finite complemented lattices *) -(* finOrderType == the type of nonempty totally ordered finite types *) +(* 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 *) (* *) (* 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 *) @@ -86,36 +88,41 @@ From mathcomp Require Import path fintype tuple bigop finset div prime. (* is indicated after each constructor. Each mixin is documented in the next *) (* paragraph. *) (* *) -(* 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. *) +(* 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. *) (* *) -(* LatticeType T lat_mixin == builds a distributive lattice from a porderType *) -(* where lat_mixin can be of types *) -(* latticeMixin, totalPOrderMixin, meetJoinMixin, *) -(* leOrderMixin or ltOrderMixin *) -(* or computed using IsoLatticeMixin. *) +(* DistrLatticeType T lat_mixin *) +(* == builds a distrLatticeType from a porderType where *) +(* lat_mixin can be of types *) +(* latticeMixin, totalPOrderMixin, meetJoinMixin, *) +(* leOrderMixin, or ltOrderMixin *) +(* or computed using IsoLatticeMixin. *) (* *) -(* OrderType T pord_mixin == builds an orderType from a latticeType *) -(* where pord_mixin can be of types *) -(* leOrderMixin, ltOrderMixin or orderMixin, *) -(* or computed using MonoTotalMixin. *) +(* BLatticeType T bot_mixin *) +(* == builds a bDistrLatticeType from a distrLatticeType and *) +(* a bottom element *) (* *) -(* BLatticeType T bot_mixin == builds a blatticeType from a latticeType *) -(* and a bottom element *) +(* TBLatticeType T top_mixin *) +(* == builds a tbDistrLatticeType from a bDistrLatticeType *) +(* and a top element *) (* *) -(* TBLatticeType T top_mixin == builds a tblatticeType from a blatticeType *) -(* and a top element *) +(* CBLatticeType T sub_mixin *) +(* == builds a cbDistrLatticeType from a bDistrLatticeType *) +(* and a difference operation *) (* *) -(* CBLatticeType T sub_mixin == builds a cblatticeType from a blatticeType *) -(* and a difference operation *) +(* CTBLatticeType T compl_mixin *) +(* == builds a ctbDistrLatticeType from a tbDistrLatticeType *) +(* and a complement operation *) (* *) -(* CTBLatticeType T compl_mixin == builds a ctblatticeType from a *) -(* tblatticeType and a complement *) -(* operation *) +(* OrderType T ord_mixin *) +(* == builds an orderType from a distrLatticeType where *) +(* ord_mixin can be of types *) +(* leOrderMixin, ltOrderMixin, or orderMixin, *) +(* or computed using MonoTotalMixin. *) (* *) (* Additionally: *) (* - [porderType of _] ... notations are available to recover structures on *) @@ -136,65 +143,70 @@ From mathcomp Require Import path fintype tuple bigop finset div prime. (* - meetJoinMixin == on a choiceType, takes le, lt, meet, join, *) (* commutativity and associativity of meet and join *) (* idempotence of meet and some De Morgan laws *) -(* (can build: porderType, latticeType) *) +(* (can build: porderType, distrLatticeType) *) (* *) (* - leOrderMixin == on a choiceType, takes le, lt, meet, join *) (* antisymmetry, transitivity and totality of le. *) -(* (can build: porderType, latticeType, orderType) *) +(* (can build: porderType, distrLatticeType, orderType) *) (* *) (* - ltOrderMixin == on a choiceType, takes le, lt, *) (* irreflexivity, transitivity and totality of lt. *) -(* (can build: porderType, latticeType, orderType) *) +(* (can build: porderType, distrLatticeType, orderType) *) (* *) (* - totalPOrderMixin == on a porderType T, totality of the order of T *) (* := total (<=%O : rel T) *) -(* (can build: latticeType) *) +(* (can build: distrLatticeType) *) (* *) -(* - totalOrderMixin == on a latticeType T, totality of the order of T *) +(* - totalOrderMixin == on a distrLatticeType T, totality of the order of T *) (* := total (<=%O : rel T) *) (* (can build: orderType) *) (* NB: this mixin is kept separate from totalPOrderMixin (even though it *) (* is convertible to it), in order to avoid ambiguous coercion paths. *) (* *) -(* - latticeMixin == on a porderType T, takes meet, join *) +(* - distrLatticeMixin == on a porderType T, takes meet, join *) (* commutativity and associativity of meet and join *) (* idempotence of meet and some De Morgan laws *) -(* (can build: latticeType) *) +(* (can build: distrLatticeType) *) (* *) -(* - blatticeMixin, tblatticeMixin, cblatticeMixin, ctblatticeMixin *) -(* == mixins with one extra operation *) -(* (respectively bottom, top, relative complement, and total complement *) +(* - bDistrLatticeMixin, tbDistrLatticeMixin, cbDistrLatticeMixin, *) +(* ctbDistrLatticeMixin *) +(* == mixins with one extra operation *) +(* (respectively bottom, top, relative complement, and *) +(* total 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 latticeMixin from an ordered structure *) +(* - IsoLatticeMixin creates a distrLatticeMixin from an ordered structure *) (* isomorphism (i.e., cancel f f', cancel f' f, {mono f : x y / x <= y}) *) (* *) (* We provide the following canonical instances of ordered types *) (* - all possible structures on bool *) -(* - porderType, latticeType, orderType, blatticeType on nat *) -(* - porderType, latticeType, orderType, blatticeType, cblatticeType, *) -(* tblatticeType, ctblatticeType on T *prod[disp] T' a copy of T * T' *) +(* - porderType, distrLatticeType, orderType, bDistrLatticeType on nat *) +(* - porderType, distrLatticeType, orderType, bDistrLatticeType, *) +(* tbDistrLatticeType, 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, and orderType, on T *lexi[disp] T' *) +(* - porderType, 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, and orderType, on {t : T & T' x} *) +(* - porderType, distrLatticeType, and orderType, on {t : T & T' x} *) (* with lexicographic ordering *) -(* - porderType, latticeType, orderType, blatticeType, cblatticeType, *) -(* tblatticeType, ctblatticeType on seqprod_with disp T a copy of seq T *) +(* - porderType, distrLatticeType, orderType, bDistrLatticeType, *) +(* cbDistrLatticeType, tbDistrLatticeType, ctbDistrLatticeType *) +(* on seqprod_with disp T a copy of seq T *) (* using product order (and seqprod T' its specialization to prod_display)*) -(* - porderType, latticeType, and orderType, on seqlexi_with disp T *) +(* - porderType, 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, orderType, blatticeType, cblatticeType, *) -(* tblatticeType, ctblatticeType on n.-tupleprod[disp] a copy of n.-tuple T *) +(* - porderType, distrLatticeType, orderType, bDistrLatticeType, *) +(* cbDistrLatticeType, tbDistrLatticeType, 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, and orderType, on n.-tuplelexi[d] T *) +(* - porderType, 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) *) (* and all possible finite type instances *) @@ -967,7 +979,7 @@ Module POCoercions. Coercion le_of_leif : leif >-> is_true. End POCoercions. -Module Lattice. +Module DistrLattice. Section ClassDef. Record mixin_of d (T : porderType d) := Mixin { @@ -1022,32 +1034,35 @@ Coercion porderType : type >-> POrder.type. Canonical eqType. Canonical choiceType. Canonical porderType. -Notation latticeType := type. -Notation latticeMixin := mixin_of. -Notation LatticeMixin := Mixin. -Notation LatticeType T m := (@pack T _ _ _ m _ _ id _ id). -Notation "[ 'latticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ id) - (at level 0, format "[ 'latticeType' 'of' T 'for' cT ]") : form_scope. -Notation "[ 'latticeType' 'of' T 'for' cT 'with' disp ]" := +Notation distrLatticeType := type. +Notation distrLatticeMixin := mixin_of. +Notation DistrLatticeMixin := Mixin. +Notation DistrLatticeType T m := (@pack T _ _ _ m _ _ id _ id). +Notation "[ 'distrLatticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ id) + (at level 0, format "[ 'distrLatticeType' 'of' T 'for' cT ]") : + form_scope. +Notation "[ 'distrLatticeType' 'of' T 'for' cT 'with' disp ]" := (@clone_with T _ cT disp _ id) - (at level 0, format "[ 'latticeType' 'of' T 'for' cT 'with' disp ]") : + (at level 0, + format "[ 'distrLatticeType' 'of' T 'for' cT 'with' disp ]") : + form_scope. +Notation "[ 'distrLatticeType' 'of' T ]" := [distrLatticeType of T for _] + (at level 0, format "[ 'distrLatticeType' 'of' T ]") : form_scope. +Notation "[ 'distrLatticeType' 'of' T 'with' disp ]" := + [distrLatticeType of T for _ with disp] + (at level 0, format "[ 'distrLatticeType' 'of' T 'with' disp ]") : form_scope. -Notation "[ 'latticeType' 'of' T ]" := [latticeType of T for _] - (at level 0, format "[ 'latticeType' 'of' T ]") : form_scope. -Notation "[ 'latticeType' 'of' T 'with' disp ]" := - [latticeType of T for _ with disp] - (at level 0, format "[ 'latticeType' 'of' T 'with' disp ]") : form_scope. End Exports. -End Lattice. -Export Lattice.Exports. +End DistrLattice. +Export DistrLattice.Exports. -Section LatticeDef. +Section DistrLatticeDef. Context {disp : unit}. -Local Notation latticeType := (latticeType disp). -Context {T : latticeType}. -Definition meet : T -> T -> T := Lattice.meet (Lattice.class T). -Definition join : T -> T -> T := Lattice.join (Lattice.class T). +Local Notation distrLatticeType := (distrLatticeType disp). +Context {T : distrLatticeType}. +Definition meet : T -> T -> T := DistrLattice.meet (DistrLattice.class T). +Definition join : T -> T -> T := DistrLattice.join (DistrLattice.class T). Variant lel_xor_gt (x y : T) : bool -> bool -> T -> T -> T -> T -> Set := | LelNotGt of x <= y : lel_xor_gt x y true false x x y y @@ -1079,26 +1094,26 @@ Variant incomparel (x y : T) : | InComparelEq of x = y : incomparel x y true true true true false false true true x x x x. -End LatticeDef. +End DistrLatticeDef. -Module Import LatticeSyntax. +Module Import DistrLatticeSyntax. Notation "x `&` y" := (meet x y) : order_scope. Notation "x `|` y" := (join x y) : order_scope. -End LatticeSyntax. +End DistrLatticeSyntax. Module Total. -Definition mixin_of d (T : latticeType d) := total (<=%O : rel T). +Definition mixin_of d (T : distrLatticeType d) := total (<=%O : rel T). Section ClassDef. Record class_of (T : Type) := Class { - base : Lattice.class_of T; + base : DistrLattice.class_of T; mixin_disp : unit; - mixin : mixin_of (Lattice.Pack mixin_disp base) + mixin : mixin_of (DistrLattice.Pack mixin_disp base) }. -Local Coercion base : class_of >-> Lattice.class_of. +Local Coercion base : class_of >-> DistrLattice.class_of. Structure type (d : unit) := Pack { sort; _ : class_of sort }. @@ -1112,28 +1127,28 @@ Definition clone_with disp' c & phant_id class c := @Pack disp' T c. Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition pack d0 b0 (m0 : mixin_of (@Lattice.Pack d0 T b0)) := - fun bT b & phant_id (@Lattice.class disp bT) b => +Definition pack d0 b0 (m0 : mixin_of (@DistrLattice.Pack d0 T b0)) := + fun bT b & phant_id (@DistrLattice.class disp bT) b => fun m & phant_id m0 m => Pack disp (@Class T b d0 m). Definition eqType := @Equality.Pack cT xclass. Definition choiceType := @Choice.Pack cT xclass. Definition porderType := @POrder.Pack disp cT xclass. -Definition latticeType := @Lattice.Pack disp cT xclass. +Definition distrLatticeType := @DistrLattice.Pack disp cT xclass. End ClassDef. Module Exports. -Coercion base : class_of >-> Lattice.class_of. +Coercion base : class_of >-> DistrLattice.class_of. Coercion sort : type >-> Sortclass. Coercion eqType : type >-> Equality.type. Coercion choiceType : type >-> Choice.type. Coercion porderType : type >-> POrder.type. -Coercion latticeType : type >-> Lattice.type. +Coercion distrLatticeType : type >-> DistrLattice.type. Canonical eqType. Canonical choiceType. Canonical porderType. -Canonical latticeType. +Canonical distrLatticeType. Notation totalOrderMixin := Total.mixin_of. Notation orderType := type. Notation OrderType T m := (@pack T _ _ _ m _ _ id _ id). @@ -1153,7 +1168,7 @@ End Exports. End Total. Import Total.Exports. -Module BLattice. +Module BDistrLattice. Section ClassDef. Record mixin_of d (T : porderType d) := Mixin { bottom : T; @@ -1161,12 +1176,12 @@ Record mixin_of d (T : porderType d) := Mixin { }. Record class_of (T : Type) := Class { - base : Lattice.class_of T; + base : DistrLattice.class_of T; mixin_disp : unit; mixin : mixin_of (POrder.Pack mixin_disp base) }. -Local Coercion base : class_of >-> Lattice.class_of. +Local Coercion base : class_of >-> DistrLattice.class_of. Structure type (d : unit) := Pack { sort; _ : class_of sort}. @@ -1180,52 +1195,55 @@ Definition clone_with disp' c of phant_id class c := @Pack disp' T c. Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition pack d0 b0 (m0 : mixin_of (@Lattice.Pack d0 T b0)) := - fun bT b & phant_id (@Lattice.class disp bT) b => +Definition pack d0 b0 (m0 : mixin_of (@DistrLattice.Pack d0 T b0)) := + fun bT b & phant_id (@DistrLattice.class disp bT) b => fun m & phant_id m0 m => Pack disp (@Class T b d0 m). Definition eqType := @Equality.Pack cT xclass. Definition choiceType := @Choice.Pack cT xclass. Definition porderType := @POrder.Pack disp cT xclass. -Definition latticeType := @Lattice.Pack disp cT xclass. +Definition distrLatticeType := @DistrLattice.Pack disp cT xclass. End ClassDef. Module Exports. -Coercion base : class_of >-> Lattice.class_of. +Coercion base : class_of >-> DistrLattice.class_of. Coercion mixin : class_of >-> mixin_of. Coercion sort : type >-> Sortclass. Coercion eqType : type >-> Equality.type. Coercion choiceType : type >-> Choice.type. Coercion porderType : type >-> POrder.type. -Coercion latticeType : type >-> Lattice.type. +Coercion distrLatticeType : type >-> DistrLattice.type. Canonical eqType. Canonical choiceType. Canonical porderType. -Canonical latticeType. -Notation blatticeType := type. -Notation blatticeMixin := mixin_of. -Notation BLatticeMixin := Mixin. -Notation BLatticeType T m := (@pack T _ _ _ m _ _ id _ id). -Notation "[ 'blatticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ id) - (at level 0, format "[ 'blatticeType' 'of' T 'for' cT ]") : form_scope. -Notation "[ 'blatticeType' 'of' T 'for' cT 'with' disp ]" := +Canonical distrLatticeType. +Notation bDistrLatticeType := type. +Notation bDistrLatticeMixin := mixin_of. +Notation BDistrLatticeMixin := Mixin. +Notation BDistrLatticeType T m := (@pack T _ _ _ m _ _ id _ id). +Notation "[ 'bDistrLatticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ id) + (at level 0, format "[ 'bDistrLatticeType' 'of' T 'for' cT ]") : + form_scope. +Notation "[ 'bDistrLatticeType' 'of' T 'for' cT 'with' disp ]" := (@clone_with T _ cT disp _ id) - (at level 0, format "[ 'blatticeType' 'of' T 'for' cT 'with' disp ]") : + (at level 0, + format "[ 'bDistrLatticeType' 'of' T 'for' cT 'with' disp ]") : + form_scope. +Notation "[ 'bDistrLatticeType' 'of' T ]" := [bDistrLatticeType of T for _] + (at level 0, format "[ 'bDistrLatticeType' 'of' T ]") : form_scope. +Notation "[ 'bDistrLatticeType' 'of' T 'with' disp ]" := + [bDistrLatticeType of T for _ with disp] + (at level 0, format "[ 'bDistrLatticeType' 'of' T 'with' disp ]") : form_scope. -Notation "[ 'blatticeType' 'of' T ]" := [blatticeType of T for _] - (at level 0, format "[ 'blatticeType' 'of' T ]") : 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. End Exports. -End BLattice. -Export BLattice.Exports. +End BDistrLattice. +Export BDistrLattice.Exports. -Definition bottom {disp : unit} {T : blatticeType disp} : T := - BLattice.bottom (BLattice.class T). +Definition bottom {disp : unit} {T : bDistrLatticeType disp} : T := + BDistrLattice.bottom (BDistrLattice.class T). -Module Import BLatticeSyntax. +Module Import BDistrLatticeSyntax. Notation "0" := bottom : order_scope. Notation "\join_ ( i <- r | P ) F" := @@ -1253,9 +1271,9 @@ Notation "\join_ ( i 'in' A | P ) F" := Notation "\join_ ( i 'in' A ) F" := (\big[@join _ _/0%O]_(i in A) F%O) : order_scope. -End BLatticeSyntax. +End BDistrLatticeSyntax. -Module TBLattice. +Module TBDistrLattice. Section ClassDef. Record mixin_of d (T : porderType d) := Mixin { top : T; @@ -1263,12 +1281,12 @@ Record mixin_of d (T : porderType d) := Mixin { }. Record class_of (T : Type) := Class { - base : BLattice.class_of T; + base : BDistrLattice.class_of T; mixin_disp : unit; mixin : mixin_of (POrder.Pack mixin_disp base) }. -Local Coercion base : class_of >-> BLattice.class_of. +Local Coercion base : class_of >-> BDistrLattice.class_of. Structure type (d : unit) := Pack { sort; _ : class_of sort }. @@ -1282,54 +1300,57 @@ Definition clone_with disp' c of phant_id class c := @Pack disp' T c. Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition pack d0 b0 (m0 : mixin_of (@BLattice.Pack d0 T b0)) := - fun bT b & phant_id (@BLattice.class disp bT) b => +Definition pack d0 b0 (m0 : mixin_of (@BDistrLattice.Pack d0 T b0)) := + fun bT b & phant_id (@BDistrLattice.class disp bT) b => fun m & phant_id m0 m => Pack disp (@Class T b d0 m). Definition eqType := @Equality.Pack cT xclass. Definition choiceType := @Choice.Pack cT xclass. Definition porderType := @POrder.Pack disp cT xclass. -Definition latticeType := @Lattice.Pack disp cT xclass. -Definition blatticeType := @BLattice.Pack disp cT xclass. +Definition distrLatticeType := @DistrLattice.Pack disp cT xclass. +Definition bDistrLatticeType := @BDistrLattice.Pack disp cT xclass. End ClassDef. Module Exports. -Coercion base : class_of >-> BLattice.class_of. +Coercion base : class_of >-> BDistrLattice.class_of. Coercion mixin : class_of >-> mixin_of. Coercion sort : type >-> Sortclass. Coercion eqType : type >-> Equality.type. Coercion porderType : type >-> POrder.type. -Coercion latticeType : type >-> Lattice.type. -Coercion blatticeType : type >-> BLattice.type. +Coercion distrLatticeType : type >-> DistrLattice.type. +Coercion bDistrLatticeType : type >-> BDistrLattice.type. Canonical eqType. Canonical choiceType. Canonical porderType. -Canonical latticeType. -Canonical blatticeType. -Notation tblatticeType := type. -Notation tblatticeMixin := mixin_of. -Notation TBLatticeMixin := Mixin. -Notation TBLatticeType T m := (@pack T _ _ _ m _ _ id _ id). -Notation "[ 'tblatticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ id) - (at level 0, format "[ 'tblatticeType' 'of' T 'for' cT ]") : form_scope. -Notation "[ 'tblatticeType' 'of' T 'for' cT 'with' disp ]" := +Canonical distrLatticeType. +Canonical bDistrLatticeType. +Notation tbDistrLatticeType := type. +Notation tbDistrLatticeMixin := mixin_of. +Notation TBDistrLatticeMixin := Mixin. +Notation TBDistrLatticeType T m := (@pack T _ _ _ m _ _ id _ id). +Notation "[ 'tbDistrLatticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ id) + (at level 0, format "[ 'tbDistrLatticeType' 'of' T 'for' cT ]") : + form_scope. +Notation "[ 'tbDistrLatticeType' 'of' T 'for' cT 'with' disp ]" := (@clone_with T _ cT disp _ id) - (at level 0, format "[ 'tblatticeType' 'of' T 'for' cT 'with' disp ]") : + (at level 0, + format "[ 'tbDistrLatticeType' 'of' T 'for' cT 'with' disp ]") : + form_scope. +Notation "[ 'tbDistrLatticeType' 'of' T ]" := [tbDistrLatticeType of T for _] + (at level 0, format "[ 'tbDistrLatticeType' 'of' T ]") : form_scope. +Notation "[ 'tbDistrLatticeType' 'of' T 'with' disp ]" := + [tbDistrLatticeType of T for _ with disp] + (at level 0, format "[ 'tbDistrLatticeType' 'of' T 'with' disp ]") : form_scope. -Notation "[ 'tblatticeType' 'of' T ]" := [tblatticeType of T for _] - (at level 0, format "[ 'tblatticeType' 'of' T ]") : form_scope. -Notation "[ 'tblatticeType' 'of' T 'with' disp ]" := - [tblatticeType of T for _ with disp] - (at level 0, format "[ 'tblatticeType' 'of' T 'with' disp ]") : form_scope. End Exports. -End TBLattice. -Export TBLattice.Exports. +End TBDistrLattice. +Export TBDistrLattice.Exports. -Definition top disp {T : tblatticeType disp} : T := - TBLattice.top (TBLattice.class T). +Definition top disp {T : tbDistrLatticeType disp} : T := + TBDistrLattice.top (TBDistrLattice.class T). -Module Import TBLatticeSyntax. +Module Import TBDistrLatticeSyntax. Notation "1" := top : order_scope. @@ -1358,23 +1379,23 @@ Notation "\meet_ ( i 'in' A | P ) F" := Notation "\meet_ ( i 'in' A ) F" := (\big[meet/1]_(i in A) F%O) : order_scope. -End TBLatticeSyntax. +End TBDistrLatticeSyntax. -Module CBLattice. +Module CBDistrLattice. Section ClassDef. -Record mixin_of d (T : blatticeType d) := Mixin { +Record mixin_of d (T : bDistrLatticeType d) := Mixin { sub : T -> T -> T; _ : forall x y, y `&` sub x y = bottom; _ : forall x y, (x `&` y) `|` sub x y = x }. Record class_of (T : Type) := Class { - base : BLattice.class_of T; + base : BDistrLattice.class_of T; mixin_disp : unit; - mixin : mixin_of (BLattice.Pack mixin_disp base) + mixin : mixin_of (BDistrLattice.Pack mixin_disp base) }. -Local Coercion base : class_of >-> BLattice.class_of. +Local Coercion base : class_of >-> BDistrLattice.class_of. Structure type (d : unit) := Pack { sort; _ : class_of sort }. @@ -1388,76 +1409,80 @@ Definition clone_with disp' c of phant_id class c := @Pack disp' T c. Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition pack d0 b0 (m0 : mixin_of (@BLattice.Pack d0 T b0)) := - fun bT b & phant_id (@BLattice.class disp bT) b => +Definition pack d0 b0 (m0 : mixin_of (@BDistrLattice.Pack d0 T b0)) := + fun bT b & phant_id (@BDistrLattice.class disp bT) b => fun m & phant_id m0 m => Pack disp (@Class T b d0 m). Definition eqType := @Equality.Pack cT xclass. Definition choiceType := @Choice.Pack cT xclass. Definition porderType := @POrder.Pack disp cT xclass. -Definition latticeType := @Lattice.Pack disp cT xclass. -Definition blatticeType := @BLattice.Pack disp cT xclass. +Definition distrLatticeType := @DistrLattice.Pack disp cT xclass. +Definition bDistrLatticeType := @BDistrLattice.Pack disp cT xclass. End ClassDef. Module Exports. -Coercion base : class_of >-> BLattice.class_of. +Coercion base : class_of >-> BDistrLattice.class_of. Coercion mixin : class_of >-> mixin_of. Coercion sort : type >-> Sortclass. Coercion eqType : type >-> Equality.type. Coercion choiceType : type >-> Choice.type. Coercion porderType : type >-> POrder.type. -Coercion latticeType : type >-> Lattice.type. -Coercion blatticeType : type >-> BLattice.type. +Coercion distrLatticeType : type >-> DistrLattice.type. +Coercion bDistrLatticeType : type >-> BDistrLattice.type. Canonical eqType. Canonical choiceType. Canonical porderType. -Canonical latticeType. -Canonical blatticeType. -Notation cblatticeType := type. -Notation cblatticeMixin := mixin_of. -Notation CBLatticeMixin := Mixin. -Notation CBLatticeType T m := (@pack T _ _ _ m _ _ id _ id). -Notation "[ 'cblatticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ id) - (at level 0, format "[ 'cblatticeType' 'of' T 'for' cT ]") : form_scope. -Notation "[ 'cblatticeType' 'of' T 'for' cT 'with' disp ]" := +Canonical distrLatticeType. +Canonical bDistrLatticeType. +Notation cbDistrLatticeType := type. +Notation cbDistrLatticeMixin := mixin_of. +Notation CBDistrLatticeMixin := Mixin. +Notation CBDistrLatticeType T m := (@pack T _ _ _ m _ _ id _ id). +Notation "[ 'cbDistrLatticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ id) + (at level 0, format "[ 'cbDistrLatticeType' 'of' T 'for' cT ]") : + form_scope. +Notation "[ 'cbDistrLatticeType' 'of' T 'for' cT 'with' disp ]" := (@clone_with T _ cT disp _ id) - (at level 0, format "[ 'cblatticeType' 'of' T 'for' cT 'with' disp ]") : + (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 "[ 'cblatticeType' 'of' T ]" := [cblatticeType of T for _] - (at level 0, format "[ 'cblatticeType' 'of' T ]") : form_scope. -Notation "[ 'cblatticeType' 'of' T 'with' disp ]" := - [cblatticeType of T for _ with disp] - (at level 0, format "[ 'cblatticeType' 'of' T 'with' disp ]") : form_scope. End Exports. -End CBLattice. -Export CBLattice.Exports. +End CBDistrLattice. +Export CBDistrLattice.Exports. -Definition sub {disp : unit} {T : cblatticeType disp} : T -> T -> T := - CBLattice.sub (CBLattice.class T). +Definition sub {disp : unit} {T : cbDistrLatticeType disp} : T -> T -> T := + CBDistrLattice.sub (CBDistrLattice.class T). -Module Import CBLatticeSyntax. +Module Import CBDistrLatticeSyntax. Notation "x `\` y" := (sub x y) : order_scope. -End CBLatticeSyntax. +End CBDistrLatticeSyntax. -Module CTBLattice. +Module CTBDistrLattice. Section ClassDef. -Record mixin_of d (T : tblatticeType d) (sub : T -> T -> T) := Mixin { +Record mixin_of d (T : tbDistrLatticeType d) (sub : T -> T -> T) := Mixin { compl : T -> T; _ : forall x, compl x = sub top x }. Record class_of (T : Type) := Class { - base : TBLattice.class_of T; + base : TBDistrLattice.class_of T; mixin1_disp : unit; - mixin1 : CBLattice.mixin_of (BLattice.Pack mixin1_disp base); + mixin1 : CBDistrLattice.mixin_of (BDistrLattice.Pack mixin1_disp base); mixin2_disp : unit; - mixin2 : @mixin_of _ (TBLattice.Pack mixin2_disp base) (CBLattice.sub mixin1) + mixin2 : @mixin_of _ (TBDistrLattice.Pack mixin2_disp base) + (CBDistrLattice.sub mixin1) }. -Local Coercion base : class_of >-> TBLattice.class_of. -Local Coercion base2 T (c : class_of T) : CBLattice.class_of T := - CBLattice.Class (mixin1 c). +Local Coercion base : class_of >-> TBDistrLattice.class_of. +Local Coercion base2 T (c : class_of T) : CBDistrLattice.class_of T := + CBDistrLattice.Class (mixin1 c). Structure type (d : unit) := Pack { sort; _ : class_of sort }. @@ -1472,73 +1497,76 @@ Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). Definition pack := - fun bT b & phant_id (@TBLattice.class disp bT) b => - fun disp1 m1T m1 & phant_id (@CBLattice.class disp1 m1T) - (@CBLattice.Class _ _ _ m1) => + fun bT b & phant_id (@TBDistrLattice.class disp bT) b => + fun disp1 m1T m1 & phant_id (@CBDistrLattice.class disp1 m1T) + (@CBDistrLattice.Class _ _ _ m1) => fun disp2 m2 => Pack disp (@Class T b disp1 m1 disp2 m2). Definition eqType := @Equality.Pack cT xclass. Definition choiceType := @Choice.Pack cT xclass. Definition porderType := @POrder.Pack disp cT xclass. -Definition latticeType := @Lattice.Pack disp cT xclass. -Definition blatticeType := @BLattice.Pack disp cT xclass. -Definition tblatticeType := @TBLattice.Pack disp cT xclass. -Definition cblatticeType := @CBLattice.Pack disp cT xclass. -Definition tbd_cblatticeType := - @CBLattice.Pack disp tblatticeType xclass. +Definition distrLatticeType := @DistrLattice.Pack disp cT xclass. +Definition bDistrLatticeType := @BDistrLattice.Pack disp cT xclass. +Definition tbDistrLatticeType := @TBDistrLattice.Pack disp cT xclass. +Definition cbDistrLatticeType := @CBDistrLattice.Pack disp cT xclass. +Definition tbd_cbDistrLatticeType := + @CBDistrLattice.Pack disp tbDistrLatticeType xclass. End ClassDef. Module Exports. -Coercion base : class_of >-> TBLattice.class_of. -Coercion base2 : class_of >-> CBLattice.class_of. -Coercion mixin1 : class_of >-> CBLattice.mixin_of. +Coercion base : class_of >-> TBDistrLattice.class_of. +Coercion base2 : class_of >-> CBDistrLattice.class_of. +Coercion mixin1 : class_of >-> CBDistrLattice.mixin_of. Coercion mixin2 : class_of >-> mixin_of. Coercion sort : type >-> Sortclass. Coercion eqType : type >-> Equality.type. Coercion choiceType : type >-> Choice.type. Coercion porderType : type >-> POrder.type. -Coercion latticeType : type >-> Lattice.type. -Coercion blatticeType : type >-> BLattice.type. -Coercion tblatticeType : type >-> TBLattice.type. -Coercion cblatticeType : type >-> CBLattice.type. +Coercion distrLatticeType : type >-> DistrLattice.type. +Coercion bDistrLatticeType : type >-> BDistrLattice.type. +Coercion tbDistrLatticeType : type >-> TBDistrLattice.type. +Coercion cbDistrLatticeType : type >-> CBDistrLattice.type. Canonical eqType. Canonical choiceType. Canonical porderType. -Canonical latticeType. -Canonical blatticeType. -Canonical tblatticeType. -Canonical cblatticeType. -Canonical tbd_cblatticeType. -Notation ctblatticeType := type. -Notation ctblatticeMixin := mixin_of. -Notation CTBLatticeMixin := Mixin. -Notation CTBLatticeType T m := (@pack T _ _ _ id _ _ _ id _ m). -Notation "[ 'ctblatticeType' 'of' T 'for' cT ]" := (@clone T _ cT _ id) - (at level 0, format "[ 'ctblatticeType' 'of' T 'for' cT ]") : form_scope. -Notation "[ 'ctblatticeType' 'of' T 'for' cT 'with' disp ]" := +Canonical distrLatticeType. +Canonical bDistrLatticeType. +Canonical tbDistrLatticeType. +Canonical cbDistrLatticeType. +Canonical tbd_cbDistrLatticeType. +Notation ctbDistrLatticeType := type. +Notation ctbDistrLatticeMixin := mixin_of. +Notation CTBDistrLatticeMixin := Mixin. +Notation CTBDistrLatticeType T m := (@pack T _ _ _ id _ _ _ id _ m). +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 "[ 'ctblatticeType' 'of' T 'for' cT 'with' disp ]") + (at level 0, + format "[ 'ctbDistrLatticeType' 'of' T 'for' cT 'with' disp ]") : form_scope. -Notation "[ 'ctblatticeType' 'of' T ]" := [ctblatticeType of T for _] - (at level 0, format "[ 'ctblatticeType' 'of' T ]") : form_scope. -Notation "[ 'ctblatticeType' 'of' T 'with' disp ]" := - [ctblatticeType of T for _ with disp] - (at level 0, format "[ 'ctblatticeType' 'of' T 'with' disp ]") : +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_ctblatticeType' 'of' T ]" := +Notation "[ 'default_ctbDistrLatticeType' 'of' T ]" := (@pack T _ _ _ id _ _ id (Mixin (fun=> erefl))) - (at level 0, format "[ 'default_ctblatticeType' 'of' T ]") : form_scope. + (at level 0, format "[ 'default_ctbDistrLatticeType' 'of' T ]") : + form_scope. End Exports. -End CTBLattice. -Export CTBLattice.Exports. +End CTBDistrLattice. +Export CTBDistrLattice.Exports. -Definition compl {d : unit} {T : ctblatticeType d} : T -> T := - CTBLattice.compl (CTBLattice.class T). +Definition compl {d : unit} {T : ctbDistrLatticeType d} : T -> T := + CTBDistrLattice.compl (CTBDistrLattice.class T). -Module Import CTBLatticeSyntax. +Module Import CTBDistrLatticeSyntax. Notation "~` A" := (compl A) : order_scope. -End CTBLatticeSyntax. +End CTBDistrLatticeSyntax. Section TotalDef. Context {disp : unit} {T : orderType disp} {I : finType}. @@ -1704,15 +1732,15 @@ End FinPOrder. Import FinPOrder.Exports. Bind Scope cpo_sort with FinPOrder.sort. -Module FinLattice. +Module FinDistrLattice. Section ClassDef. Record class_of (T : Type) := Class { - base : TBLattice.class_of T; + base : TBDistrLattice.class_of T; mixin : Finite.mixin_of (Equality.Pack base); }. -Local Coercion base : class_of >-> TBLattice.class_of. +Local Coercion base : class_of >-> TBDistrLattice.class_of. Local Coercion base2 T (c : class_of T) : Finite.class_of T := Finite.Class (mixin c). Local Coercion base3 T (c : class_of T) : FinPOrder.class_of T := @@ -1729,7 +1757,7 @@ Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). Definition pack := - fun bT b & phant_id (@TBLattice.class disp bT) b => + fun bT b & phant_id (@TBDistrLattice.class disp bT) b => fun mT m & phant_id (@Finite.class mT) (@Finite.Class _ _ m) => Pack disp (@Class T b m). @@ -1739,23 +1767,27 @@ Definition countType := @Countable.Pack cT xclass. Definition finType := @Finite.Pack cT xclass. Definition porderType := @POrder.Pack disp cT xclass. Definition finPOrderType := @FinPOrder.Pack disp cT xclass. -Definition latticeType := @Lattice.Pack disp cT xclass. -Definition blatticeType := @BLattice.Pack disp cT xclass. -Definition tblatticeType := @TBLattice.Pack disp cT xclass. -Definition count_latticeType := @Lattice.Pack disp countType xclass. -Definition count_blatticeType := @BLattice.Pack disp countType xclass. -Definition count_tblatticeType := @TBLattice.Pack disp countType xclass. -Definition fin_latticeType := @Lattice.Pack disp finType xclass. -Definition fin_blatticeType := @BLattice.Pack disp finType xclass. -Definition fin_tblatticeType := @TBLattice.Pack disp finType xclass. -Definition finPOrder_latticeType := @Lattice.Pack disp finPOrderType xclass. -Definition finPOrder_blatticeType := @BLattice.Pack disp finPOrderType xclass. -Definition finPOrder_tblatticeType := @TBLattice.Pack disp finPOrderType xclass. +Definition distrLatticeType := @DistrLattice.Pack disp cT xclass. +Definition bDistrLatticeType := @BDistrLattice.Pack disp cT xclass. +Definition tbDistrLatticeType := @TBDistrLattice.Pack disp cT xclass. +Definition count_distrLatticeType := @DistrLattice.Pack disp countType xclass. +Definition count_bDistrLatticeType := @BDistrLattice.Pack disp countType xclass. +Definition count_tbDistrLatticeType := + @TBDistrLattice.Pack disp countType xclass. +Definition fin_distrLatticeType := @DistrLattice.Pack disp finType xclass. +Definition fin_bDistrLatticeType := @BDistrLattice.Pack disp finType xclass. +Definition fin_tbDistrLatticeType := @TBDistrLattice.Pack disp finType xclass. +Definition finPOrder_distrLatticeType := + @DistrLattice.Pack disp finPOrderType xclass. +Definition finPOrder_bDistrLatticeType := + @BDistrLattice.Pack disp finPOrderType xclass. +Definition finPOrder_tbDistrLatticeType := + @TBDistrLattice.Pack disp finPOrderType xclass. End ClassDef. Module Exports. -Coercion base : class_of >-> TBLattice.class_of. +Coercion base : class_of >-> TBDistrLattice.class_of. Coercion base2 : class_of >-> Finite.class_of. Coercion base3 : class_of >-> FinPOrder.class_of. Coercion sort : type >-> Sortclass. @@ -1765,48 +1797,48 @@ Coercion countType : type >-> Countable.type. Coercion finType : type >-> Finite.type. Coercion porderType : type >-> POrder.type. Coercion finPOrderType : type >-> FinPOrder.type. -Coercion latticeType : type >-> Lattice.type. -Coercion blatticeType : type >-> BLattice.type. -Coercion tblatticeType : type >-> TBLattice.type. +Coercion distrLatticeType : type >-> DistrLattice.type. +Coercion bDistrLatticeType : type >-> BDistrLattice.type. +Coercion tbDistrLatticeType : type >-> TBDistrLattice.type. Canonical eqType. Canonical choiceType. Canonical countType. Canonical finType. Canonical porderType. Canonical finPOrderType. -Canonical latticeType. -Canonical blatticeType. -Canonical tblatticeType. -Canonical count_latticeType. -Canonical count_blatticeType. -Canonical count_tblatticeType. -Canonical fin_latticeType. -Canonical fin_blatticeType. -Canonical fin_tblatticeType. -Canonical finPOrder_latticeType. -Canonical finPOrder_blatticeType. -Canonical finPOrder_tblatticeType. -Notation finLatticeType := type. -Notation "[ 'finLatticeType' 'of' T ]" := (@pack T _ _ _ id _ _ id) - (at level 0, format "[ 'finLatticeType' 'of' T ]") : form_scope. +Canonical distrLatticeType. +Canonical bDistrLatticeType. +Canonical tbDistrLatticeType. +Canonical count_distrLatticeType. +Canonical count_bDistrLatticeType. +Canonical count_tbDistrLatticeType. +Canonical fin_distrLatticeType. +Canonical fin_bDistrLatticeType. +Canonical fin_tbDistrLatticeType. +Canonical finPOrder_distrLatticeType. +Canonical finPOrder_bDistrLatticeType. +Canonical finPOrder_tbDistrLatticeType. +Notation finDistrLatticeType := type. +Notation "[ 'finDistrLatticeType' 'of' T ]" := (@pack T _ _ _ id _ _ id) + (at level 0, format "[ 'finDistrLatticeType' 'of' T ]") : form_scope. End Exports. -End FinLattice. -Export FinLattice.Exports. +End FinDistrLattice. +Export FinDistrLattice.Exports. -Module FinCLattice. +Module FinCDistrLattice. Section ClassDef. Record class_of (T : Type) := Class { - base : CTBLattice.class_of T; + base : CTBDistrLattice.class_of T; mixin : Finite.mixin_of (Equality.Pack base); }. -Local Coercion base : class_of >-> CTBLattice.class_of. +Local Coercion base : class_of >-> CTBDistrLattice.class_of. Local Coercion base2 T (c : class_of T) : Finite.class_of T := Finite.Class (mixin c). -Local Coercion base3 T (c : class_of T) : FinLattice.class_of T := - @FinLattice.Class T c c. +Local Coercion base3 T (c : class_of T) : FinDistrLattice.class_of T := + @FinDistrLattice.Class T c c. Structure type (disp : unit) := Pack { sort; _ : class_of sort }. @@ -1819,7 +1851,7 @@ Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). Definition pack := - fun bT b & phant_id (@CTBLattice.class disp bT) b => + fun bT b & phant_id (@CTBDistrLattice.class disp bT) b => fun mT m & phant_id (@Finite.class mT) (@Finite.Class _ _ m) => Pack disp (@Class T b m). @@ -1829,30 +1861,33 @@ Definition countType := @Countable.Pack cT xclass. Definition finType := @Finite.Pack cT xclass. Definition porderType := @POrder.Pack disp cT xclass. Definition finPOrderType := @FinPOrder.Pack disp cT xclass. -Definition latticeType := @Lattice.Pack disp cT xclass. -Definition blatticeType := @BLattice.Pack disp cT xclass. -Definition tblatticeType := @TBLattice.Pack disp cT xclass. -Definition finLatticeType := @FinLattice.Pack disp cT xclass. -Definition cblatticeType := @CBLattice.Pack disp cT xclass. -Definition ctblatticeType := @CTBLattice.Pack disp cT xclass. -Definition count_cblatticeType := @CBLattice.Pack disp countType xclass. -Definition count_ctblatticeType := @CTBLattice.Pack disp countType xclass. -Definition fin_cblatticeType := @CBLattice.Pack disp finType xclass. -Definition fin_ctblatticeType := @CTBLattice.Pack disp finType xclass. -Definition finPOrder_cblatticeType := @CBLattice.Pack disp finPOrderType xclass. -Definition finPOrder_ctblatticeType := - @CTBLattice.Pack disp finPOrderType xclass. -Definition finLattice_cblatticeType := - @CBLattice.Pack disp finLatticeType xclass. -Definition finLattice_ctblatticeType := - @CTBLattice.Pack disp finLatticeType xclass. +Definition distrLatticeType := @DistrLattice.Pack disp cT xclass. +Definition bDistrLatticeType := @BDistrLattice.Pack disp cT xclass. +Definition tbDistrLatticeType := @TBDistrLattice.Pack disp cT xclass. +Definition finDistrLatticeType := @FinDistrLattice.Pack disp cT xclass. +Definition cbDistrLatticeType := @CBDistrLattice.Pack disp cT xclass. +Definition ctbDistrLatticeType := @CTBDistrLattice.Pack disp cT xclass. +Definition count_cbDistrLatticeType := + @CBDistrLattice.Pack disp countType xclass. +Definition count_ctbDistrLatticeType := + @CTBDistrLattice.Pack disp countType xclass. +Definition fin_cbDistrLatticeType := @CBDistrLattice.Pack disp finType xclass. +Definition fin_ctbDistrLatticeType := @CTBDistrLattice.Pack disp finType xclass. +Definition finPOrder_cbDistrLatticeType := + @CBDistrLattice.Pack disp finPOrderType xclass. +Definition finPOrder_ctbDistrLatticeType := + @CTBDistrLattice.Pack disp finPOrderType xclass. +Definition finDistrLattice_cbDistrLatticeType := + @CBDistrLattice.Pack disp finDistrLatticeType xclass. +Definition finDistrLattice_ctbDistrLatticeType := + @CTBDistrLattice.Pack disp finDistrLatticeType xclass. End ClassDef. Module Exports. -Coercion base : class_of >-> CTBLattice.class_of. +Coercion base : class_of >-> CTBDistrLattice.class_of. Coercion base2 : class_of >-> Finite.class_of. -Coercion base3 : class_of >-> FinLattice.class_of. +Coercion base3 : class_of >-> FinDistrLattice.class_of. Coercion sort : type >-> Sortclass. Coercion eqType : type >-> Equality.type. Coercion choiceType : type >-> Choice.type. @@ -1860,50 +1895,50 @@ Coercion countType : type >-> Countable.type. Coercion finType : type >-> Finite.type. Coercion porderType : type >-> POrder.type. Coercion finPOrderType : type >-> FinPOrder.type. -Coercion latticeType : type >-> Lattice.type. -Coercion blatticeType : type >-> BLattice.type. -Coercion tblatticeType : type >-> TBLattice.type. -Coercion finLatticeType : type >-> FinLattice.type. -Coercion cblatticeType : type >-> CBLattice.type. -Coercion ctblatticeType : type >-> CTBLattice.type. +Coercion distrLatticeType : type >-> DistrLattice.type. +Coercion bDistrLatticeType : type >-> BDistrLattice.type. +Coercion tbDistrLatticeType : type >-> TBDistrLattice.type. +Coercion finDistrLatticeType : type >-> FinDistrLattice.type. +Coercion cbDistrLatticeType : type >-> CBDistrLattice.type. +Coercion ctbDistrLatticeType : type >-> CTBDistrLattice.type. Canonical eqType. Canonical choiceType. Canonical countType. Canonical finType. Canonical porderType. Canonical finPOrderType. -Canonical latticeType. -Canonical blatticeType. -Canonical tblatticeType. -Canonical finLatticeType. -Canonical cblatticeType. -Canonical ctblatticeType. -Canonical count_cblatticeType. -Canonical count_ctblatticeType. -Canonical fin_cblatticeType. -Canonical fin_ctblatticeType. -Canonical finPOrder_cblatticeType. -Canonical finPOrder_ctblatticeType. -Canonical finLattice_cblatticeType. -Canonical finLattice_ctblatticeType. -Notation finCLatticeType := type. -Notation "[ 'finCLatticeType' 'of' T ]" := (@pack T _ _ _ id _ _ id) - (at level 0, format "[ 'finCLatticeType' 'of' T ]") : form_scope. +Canonical distrLatticeType. +Canonical bDistrLatticeType. +Canonical tbDistrLatticeType. +Canonical finDistrLatticeType. +Canonical cbDistrLatticeType. +Canonical ctbDistrLatticeType. +Canonical count_cbDistrLatticeType. +Canonical count_ctbDistrLatticeType. +Canonical fin_cbDistrLatticeType. +Canonical fin_ctbDistrLatticeType. +Canonical finPOrder_cbDistrLatticeType. +Canonical finPOrder_ctbDistrLatticeType. +Canonical finDistrLattice_cbDistrLatticeType. +Canonical finDistrLattice_ctbDistrLatticeType. +Notation finCDistrLatticeType := type. +Notation "[ 'finCDistrLatticeType' 'of' T ]" := (@pack T _ _ _ id _ _ id) + (at level 0, format "[ 'finCDistrLatticeType' 'of' T ]") : form_scope. End Exports. -End FinCLattice. -Export FinCLattice.Exports. +End FinCDistrLattice. +Export FinCDistrLattice.Exports. Module FinTotal. Section ClassDef. Record class_of (T : Type) := Class { - base : FinLattice.class_of T; + base : FinDistrLattice.class_of T; mixin_disp : unit; - mixin : totalOrderMixin (Lattice.Pack mixin_disp base) + mixin : totalOrderMixin (DistrLattice.Pack mixin_disp base) }. -Local Coercion base : class_of >-> FinLattice.class_of. +Local Coercion base : class_of >-> FinDistrLattice.class_of. Local Coercion base2 T (c : class_of T) : Total.class_of T := @Total.Class _ c _ (mixin (c := c)). @@ -1918,7 +1953,7 @@ Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). Definition pack := - fun bT b & phant_id (@FinLattice.class disp bT) b => + fun bT b & phant_id (@FinDistrLattice.class disp bT) b => fun disp' mT m & phant_id (@Total.class disp mT) (@Total.Class _ _ _ m) => Pack disp (@Class T b disp' m). @@ -1928,22 +1963,24 @@ Definition countType := @Countable.Pack cT xclass. Definition finType := @Finite.Pack cT xclass. Definition porderType := @POrder.Pack disp cT xclass. Definition finPOrderType := @FinPOrder.Pack disp cT xclass. -Definition latticeType := @Lattice.Pack disp cT xclass. -Definition blatticeType := @BLattice.Pack disp cT xclass. -Definition tblatticeType := @TBLattice.Pack disp cT xclass. -Definition finLatticeType := @FinLattice.Pack disp cT xclass. +Definition distrLatticeType := @DistrLattice.Pack disp cT xclass. +Definition bDistrLatticeType := @BDistrLattice.Pack disp cT xclass. +Definition tbDistrLatticeType := @TBDistrLattice.Pack disp cT xclass. +Definition finDistrLatticeType := @FinDistrLattice.Pack disp cT xclass. Definition orderType := @Total.Pack disp cT xclass. Definition order_countType := @Countable.Pack orderType xclass. Definition order_finType := @Finite.Pack orderType xclass. Definition order_finPOrderType := @FinPOrder.Pack disp orderType xclass. -Definition order_blatticeType := @BLattice.Pack disp orderType xclass. -Definition order_tblatticeType := @TBLattice.Pack disp orderType xclass. -Definition order_finLatticeType := @FinLattice.Pack disp orderType xclass. +Definition order_bDistrLatticeType := @BDistrLattice.Pack disp orderType xclass. +Definition order_tbDistrLatticeType := + @TBDistrLattice.Pack disp orderType xclass. +Definition order_finDistrLatticeType := + @FinDistrLattice.Pack disp orderType xclass. End ClassDef. Module Exports. -Coercion base : class_of >-> FinLattice.class_of. +Coercion base : class_of >-> FinDistrLattice.class_of. Coercion base2 : class_of >-> Total.class_of. Coercion sort : type >-> Sortclass. Coercion eqType : type >-> Equality.type. @@ -1952,10 +1989,10 @@ Coercion countType : type >-> Countable.type. Coercion finType : type >-> Finite.type. Coercion porderType : type >-> POrder.type. Coercion finPOrderType : type >-> FinPOrder.type. -Coercion latticeType : type >-> Lattice.type. -Coercion blatticeType : type >-> BLattice.type. -Coercion tblatticeType : type >-> TBLattice.type. -Coercion finLatticeType : type >-> FinLattice.type. +Coercion distrLatticeType : type >-> DistrLattice.type. +Coercion bDistrLatticeType : type >-> BDistrLattice.type. +Coercion tbDistrLatticeType : type >-> TBDistrLattice.type. +Coercion finDistrLatticeType : type >-> FinDistrLattice.type. Coercion orderType : type >-> Total.type. Canonical eqType. Canonical choiceType. @@ -1963,17 +2000,17 @@ Canonical countType. Canonical finType. Canonical porderType. Canonical finPOrderType. -Canonical latticeType. -Canonical blatticeType. -Canonical tblatticeType. -Canonical finLatticeType. +Canonical distrLatticeType. +Canonical bDistrLatticeType. +Canonical tbDistrLatticeType. +Canonical finDistrLatticeType. Canonical orderType. Canonical order_countType. Canonical order_finType. Canonical order_finPOrderType. -Canonical order_blatticeType. -Canonical order_tblatticeType. -Canonical order_finLatticeType. +Canonical order_bDistrLatticeType. +Canonical order_tbDistrLatticeType. +Canonical order_finDistrLatticeType. Notation finOrderType := type. Notation "[ 'finOrderType' 'of' T ]" := (@pack T _ _ _ id _ _ _ id) (at level 0, format "[ 'finOrderType' 'of' T ]") : form_scope. @@ -2469,12 +2506,12 @@ Canonical converse_porderType := End ConversePOrder. End ConversePOrder. -Module Import ConverseLattice. -Section ConverseLattice. +Module Import ConverseDistrLattice. +Section ConverseDistrLattice. Context {disp : unit}. -Local Notation latticeType := (latticeType disp). +Local Notation distrLatticeType := (distrLatticeType disp). -Variable L : latticeType. +Variable L : distrLatticeType. Implicit Types (x y : L). Lemma meetC : commutative (@meet _ L). Proof. by case: L => [?[? ?[]]]. Qed. @@ -2517,18 +2554,19 @@ Proof. by move=> x y z; rewrite meetUr joinIK meetUl -joinA meetUKC. Qed. Fact converse_leEmeet (x y : L^c) : (x <= y) = (x `|` y == x). Proof. by rewrite [LHS]leEjoin joinC. Qed. -Definition converse_latticeMixin := - @LatticeMixin _ [porderType of L^c] _ _ joinC meetC +Definition converse_distrLatticeMixin := + @DistrLatticeMixin _ [porderType of L^c] _ _ joinC meetC joinA meetA meetKU joinKI converse_leEmeet joinIl. -Canonical converse_latticeType := LatticeType L^c converse_latticeMixin. -End ConverseLattice. -End ConverseLattice. +Canonical converse_distrLatticeType := + DistrLatticeType L^c converse_distrLatticeMixin. +End ConverseDistrLattice. +End ConverseDistrLattice. -Module Import LatticeTheoryMeet. -Section LatticeTheoryMeet. +Module Import DistrLatticeTheoryMeet. +Section DistrLatticeTheoryMeet. Context {disp : unit}. -Local Notation latticeType := (latticeType disp). -Context {L : latticeType}. +Local Notation distrLatticeType := (distrLatticeType disp). +Context {L : distrLatticeType}. Implicit Types (x y : L). (* lattice theory *) @@ -2597,75 +2635,75 @@ Proof. by rewrite meetC eq_meetl. 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. -End LatticeTheoryMeet. -End LatticeTheoryMeet. +End DistrLatticeTheoryMeet. +End DistrLatticeTheoryMeet. -Module Import LatticeTheoryJoin. -Section LatticeTheoryJoin. +Module Import DistrLatticeTheoryJoin. +Section DistrLatticeTheoryJoin. Context {disp : unit}. -Local Notation latticeType := (latticeType disp). -Context {L : latticeType}. +Local Notation distrLatticeType := (distrLatticeType disp). +Context {L : distrLatticeType}. Implicit Types (x y : L). (* lattice theory *) Lemma joinAC : right_commutative (@join _ L). -Proof. exact: (@meetAC _ [latticeType of L^c]). Qed. +Proof. exact: (@meetAC _ [distrLatticeType of L^c]). Qed. Lemma joinCA : left_commutative (@join _ L). -Proof. exact: (@meetCA _ [latticeType of L^c]). Qed. +Proof. exact: (@meetCA _ [distrLatticeType of L^c]). Qed. Lemma joinACA : interchange (@join _ L) (@join _ L). -Proof. exact: (@meetACA _ [latticeType of L^c]). Qed. +Proof. exact: (@meetACA _ [distrLatticeType of L^c]). Qed. Lemma joinxx x : x `|` x = x. -Proof. exact: (@meetxx _ [latticeType of L^c]). Qed. +Proof. exact: (@meetxx _ [distrLatticeType of L^c]). Qed. Lemma joinKU y x : x `|` (x `|` y) = x `|` y. -Proof. exact: (@meetKI _ [latticeType of L^c]). Qed. +Proof. exact: (@meetKI _ [distrLatticeType of L^c]). Qed. Lemma joinUK y x : (x `|` y) `|` y = x `|` y. -Proof. exact: (@meetIK _ [latticeType of L^c]). Qed. +Proof. exact: (@meetIK _ [distrLatticeType of L^c]). Qed. Lemma joinKUC y x : x `|` (y `|` x) = x `|` y. -Proof. exact: (@meetKIC _ [latticeType of L^c]). Qed. +Proof. exact: (@meetKIC _ [distrLatticeType of L^c]). Qed. Lemma joinUKC y x : y `|` x `|` y = x `|` y. -Proof. exact: (@meetIKC _ [latticeType of L^c]). Qed. +Proof. exact: (@meetIKC _ [distrLatticeType of L^c]). Qed. (* interaction with order *) Lemma leUx x y z : (x `|` y <= z) = (x <= z) && (y <= z). -Proof. exact: (@lexI _ [latticeType of L^c]). Qed. +Proof. exact: (@lexI _ [distrLatticeType of L^c]). Qed. Lemma lexUl x y z : x <= y -> x <= y `|` z. -Proof. exact: (@leIxl _ [latticeType of L^c]). Qed. +Proof. exact: (@leIxl _ [distrLatticeType of L^c]). Qed. Lemma lexUr x y z : x <= z -> x <= y `|` z. -Proof. exact: (@leIxr _ [latticeType of L^c]). Qed. +Proof. exact: (@leIxr _ [distrLatticeType of L^c]). Qed. Lemma lexU2 x y z : (x <= y) || (x <= z) -> x <= y `|` z. -Proof. exact: (@leIx2 _ [latticeType of L^c]). Qed. +Proof. exact: (@leIx2 _ [distrLatticeType of L^c]). Qed. Lemma leUr x y : x <= y `|` x. -Proof. exact: (@leIr _ [latticeType of L^c]). Qed. +Proof. exact: (@leIr _ [distrLatticeType of L^c]). Qed. Lemma leUl x y : x <= x `|` y. -Proof. exact: (@leIl _ [latticeType of L^c]). Qed. +Proof. exact: (@leIl _ [distrLatticeType of L^c]). Qed. Lemma join_idPl {x y} : reflect (x `|` y = y) (x <= y). -Proof. exact: (@meet_idPr _ [latticeType of L^c]). Qed. +Proof. exact: (@meet_idPr _ [distrLatticeType of L^c]). Qed. Lemma join_idPr {x y} : reflect (y `|` x = y) (x <= y). -Proof. exact: (@meet_idPl _ [latticeType of L^c]). Qed. +Proof. exact: (@meet_idPl _ [distrLatticeType of L^c]). Qed. Lemma join_l x y : y <= x -> x `|` y = x. Proof. exact/join_idPr. Qed. Lemma join_r x y : x <= y -> x `|` y = y. Proof. exact/join_idPl. Qed. Lemma leUidl x y : (x `|` y <= y) = (x <= y). -Proof. exact: (@leIidr _ [latticeType of L^c]). Qed. +Proof. exact: (@leIidr _ [distrLatticeType of L^c]). Qed. Lemma leUidr x y : (y `|` x <= y) = (x <= y). -Proof. exact: (@leIidl _ [latticeType of L^c]). Qed. +Proof. exact: (@leIidl _ [distrLatticeType of L^c]). Qed. Lemma eq_joinl x y : (x `|` y == x) = (y <= x). -Proof. exact: (@eq_meetl _ [latticeType of L^c]). Qed. +Proof. exact: (@eq_meetl _ [distrLatticeType of L^c]). Qed. Lemma eq_joinr x y : (x `|` y == y) = (x <= y). -Proof. exact: (@eq_meetr _ [latticeType of L^c]). Qed. +Proof. exact: (@eq_meetr _ [distrLatticeType of L^c]). Qed. Lemma leU2 x y z t : x <= z -> y <= t -> x `|` y <= z `|` t. -Proof. exact: (@leI2 _ [latticeType of L^c]). Qed. +Proof. exact: (@leI2 _ [distrLatticeType of L^c]). Qed. (* Distributive lattice theory *) Lemma joinIr : right_distributive (@join _ L) (@meet _ L). -Proof. exact: (@meetUr _ [latticeType of L^c]). Qed. +Proof. exact: (@meetUr _ [distrLatticeType of L^c]). Qed. Lemma lcomparableP x y : incomparel x y (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y) @@ -2690,8 +2728,8 @@ Lemma lcomparable_ltP x y : x >=< y -> ltl_xor_ge 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 LatticeTheoryJoin. -End LatticeTheoryJoin. +End DistrLatticeTheoryJoin. +End DistrLatticeTheoryJoin. Module Import TotalTheory. Section TotalTheory. @@ -2725,9 +2763,10 @@ 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 := LatticeTheoryJoin.lcomparable_ltgtP (comparableT x y). -Definition leP x y := LatticeTheoryJoin.lcomparable_leP (comparableT x y). -Definition ltP x y := LatticeTheoryJoin.lcomparable_ltP (comparableT x y). +Definition ltgtP x y := + DistrLatticeTheoryJoin.lcomparable_ltgtP (comparableT x y). +Definition leP x y := DistrLatticeTheoryJoin.lcomparable_leP (comparableT x y). +Definition ltP x y := DistrLatticeTheoryJoin.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) -> @@ -2836,11 +2875,11 @@ Proof. exact: total_homo_mono_in. Qed. End TotalMonotonyTheory. End TotalTheory. -Module Import BLatticeTheory. -Section BLatticeTheory. +Module Import BDistrLatticeTheory. +Section BDistrLatticeTheory. Context {disp : unit}. -Local Notation blatticeType := (blatticeType disp). -Context {L : blatticeType}. +Local Notation bDistrLatticeType := (bDistrLatticeType disp). +Context {L : bDistrLatticeType}. Implicit Types (I : finType) (T : eqType) (x y z : L). Local Notation "0" := bottom. @@ -2984,33 +3023,35 @@ case; rewrite (andbF, andbT) // => Pi /(_ isT) dy /eqP dFi. by rewrite meetUr dy dFi joinxx. Qed. -End BLatticeTheory. -End BLatticeTheory. +End BDistrLatticeTheory. +End BDistrLatticeTheory. -Module Import ConverseTBLattice. -Section ConverseTBLattice. +Module Import ConverseTBDistrLattice. +Section ConverseTBDistrLattice. Context {disp : unit}. -Local Notation tblatticeType := (tblatticeType disp). -Context {L : tblatticeType}. +Local Notation tbDistrLatticeType := (tbDistrLatticeType disp). +Context {L : tbDistrLatticeType}. Lemma lex1 (x : L) : x <= top. Proof. by case: L x => [?[? ?[]]]. Qed. -Definition converse_blatticeMixin := - @BLatticeMixin _ [latticeType of L^c] top lex1. -Canonical converse_blatticeType := BLatticeType L^c converse_blatticeMixin. +Definition converse_bDistrLatticeMixin := + @BDistrLatticeMixin _ [distrLatticeType of L^c] top lex1. +Canonical converse_bDistrLatticeType := + BDistrLatticeType L^c converse_bDistrLatticeMixin. -Definition converse_tblatticeMixin := - @TBLatticeMixin _ [latticeType of L^c] (bottom : L) (@le0x _ L). -Canonical converse_tblatticeType := TBLatticeType L^c converse_tblatticeMixin. +Definition converse_tbDistrLatticeMixin := + @TBDistrLatticeMixin _ [distrLatticeType of L^c] (bottom : L) (@le0x _ L). +Canonical converse_tbDIstrLatticeType := + TBDistrLatticeType L^c converse_tbDistrLatticeMixin. -End ConverseTBLattice. -End ConverseTBLattice. +End ConverseTBDistrLattice. +End ConverseTBDistrLattice. -Module Import TBLatticeTheory. -Section TBLatticeTheory. +Module Import TBDistrLatticeTheory. +Section TBDistrLatticeTheory. Context {disp : unit}. -Local Notation tblatticeType := (tblatticeType disp). -Context {L : tblatticeType}. +Local Notation tbDistrLatticeType := (tbDistrLatticeType disp). +Context {L : tbDistrLatticeType}. Implicit Types (I : finType) (T : eqType) (x y : L). Local Notation "1" := top. @@ -3018,40 +3059,44 @@ Local Notation "1" := top. Hint Resolve le0x lex1 : core. Lemma meetx1 : right_id 1 (@meet _ L). -Proof. exact: (@joinx0 _ [tblatticeType of L^c]). Qed. +Proof. exact: (@joinx0 _ [tbDistrLatticeType of L^c]). Qed. Lemma meet1x : left_id 1 (@meet _ L). -Proof. exact: (@join0x _ [tblatticeType of L^c]). Qed. +Proof. exact: (@join0x _ [tbDistrLatticeType of L^c]). Qed. Lemma joinx1 : right_zero 1 (@join _ L). -Proof. exact: (@meetx0 _ [tblatticeType of L^c]). Qed. +Proof. exact: (@meetx0 _ [tbDistrLatticeType of L^c]). Qed. Lemma join1x : left_zero 1 (@join _ L). -Proof. exact: (@meet0x _ [tblatticeType of L^c]). Qed. +Proof. exact: (@meet0x _ [tbDistrLatticeType of L^c]). Qed. Lemma le1x x : (1 <= x) = (x == 1). -Proof. exact: (@lex0 _ [tblatticeType of L^c]). Qed. +Proof. exact: (@lex0 _ [tbDistrLatticeType of L^c]). Qed. Lemma leI2l_le y t x z : y `|` z = 1 -> x `&` y <= z `&` t -> x <= z. -Proof. rewrite joinC; exact: (@leU2l_le _ [tblatticeType of L^c]). Qed. +Proof. rewrite joinC; exact: (@leU2l_le _ [tbDistrLatticeType of L^c]). Qed. Lemma leI2r_le y t x z : y `|` z = 1 -> y `&` x <= t `&` z -> x <= z. -Proof. rewrite joinC; exact: (@leU2r_le _ [tblatticeType of L^c]). Qed. +Proof. rewrite joinC; exact: (@leU2r_le _ [tbDistrLatticeType of L^c]). Qed. Lemma cover_leIxl z x y : z `|` y = 1 -> (x `&` z <= y) = (x <= y). -Proof. rewrite joinC; exact: (@disjoint_lexUl _ [tblatticeType of L^c]). Qed. +Proof. +rewrite joinC; exact: (@disjoint_lexUl _ [tbDistrLatticeType of L^c]). +Qed. Lemma cover_leIxr z x y : z `|` y = 1 -> (z `&` x <= y) = (x <= y). -Proof. rewrite joinC; exact: (@disjoint_lexUr _ [tblatticeType of L^c]). Qed. +Proof. +rewrite joinC; exact: (@disjoint_lexUr _ [tbDistrLatticeType of L^c]). +Qed. Lemma leI2E x y z t : x `|` t = 1 -> y `|` z = 1 -> (x `&` y <= z `&` t) = (x <= z) && (y <= t). Proof. -by move=> ? ?; apply: (@leU2E _ [tblatticeType of L^c]); rewrite meetC. +by move=> ? ?; apply: (@leU2E _ [tbDistrLatticeType of L^c]); rewrite meetC. Qed. Lemma meet_eq1 x y : (x `&` y == 1) = (x == 1) && (y == 1). -Proof. exact: (@join_eq0 _ [tblatticeType of L^c]). Qed. +Proof. exact: (@join_eq0 _ [tbDistrLatticeType of L^c]). Qed. Canonical meet_monoid := Monoid.Law (@meetA _ _) meet1x meetx1. Canonical meet_comoid := Monoid.ComLaw (@meetC _ _). @@ -3063,53 +3108,53 @@ Canonical meet_addoid := Monoid.AddLaw (@joinIl _ L) (@joinIr _ _). Lemma meets_inf I (j : I) (P : {pred I}) (F : I -> L) : P j -> \meet_(i | P i) F i <= F j. -Proof. exact: (@join_sup _ [tblatticeType of L^c]). Qed. +Proof. exact: (@join_sup _ [tbDistrLatticeType of L^c]). 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: (@join_min _ [tblatticeType of L^c]). Qed. +Proof. exact: (@join_min _ [tbDistrLatticeType of L^c]). 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. exact: (@joinsP _ [tblatticeType of L^c]). Qed. +Proof. exact: (@joinsP _ [tbDistrLatticeType of L^c]). Qed. Lemma meet_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. exact: (@join_sup_seq _ [tblatticeType of L^c]). Qed. +Proof. exact: (@join_sup_seq _ [tbDistrLatticeType of L^c]). Qed. Lemma meet_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. exact: (@join_min_seq _ [tblatticeType of L^c]). Qed. +Proof. exact: (@join_min_seq _ [tbDistrLatticeType of L^c]). 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. exact: (@joinsP_seq _ [tblatticeType of L^c]). Qed. +Proof. exact: (@joinsP_seq _ [tbDistrLatticeType of L^c]). 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. exact: (@le_joins _ [tblatticeType of L^c]). Qed. +Proof. exact: (@le_joins _ [tbDistrLatticeType of L^c]). 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. exact: (@joins_setU _ [tblatticeType of L^c]). Qed. +Proof. exact: (@joins_setU _ [tbDistrLatticeType of L^c]). Qed. Lemma meet_seq I (r : seq I) (F : I -> L) : \meet_(i <- r) F i = \meet_(i in r) F i. -Proof. exact: (@join_seq _ [tblatticeType of L^c]). Qed. +Proof. exact: (@join_seq _ [tbDistrLatticeType of L^c]). Qed. Lemma meets_total I (d : L) (P : {pred I}) (F : I -> L) : (forall i : I, P i -> d `|` F i = 1) -> d `|` \meet_(i | P i) F i = 1. -Proof. exact: (@joins_disjoint _ [tblatticeType of L^c]). Qed. +Proof. exact: (@joins_disjoint _ [tbDistrLatticeType of L^c]). Qed. -End TBLatticeTheory. -End TBLatticeTheory. +End TBDistrLatticeTheory. +End TBDistrLatticeTheory. -Module Import CBLatticeTheory. -Section CBLatticeTheory. +Module Import CBDistrLatticeTheory. +Section CBDistrLatticeTheory. Context {disp : unit}. -Local Notation cblatticeType := (cblatticeType disp). -Context {L : cblatticeType}. +Local Notation cbDistrLatticeType := (cbDistrLatticeType disp). +Context {L : cbDistrLatticeType}. Implicit Types (x y z : L). Local Notation "0" := bottom. @@ -3281,14 +3326,14 @@ Proof. by move=> ?; rewrite lt_leAnge leBRL leBLR le0x meet0x eqxx joinx0 /= lt_geF. Qed. -End CBLatticeTheory. -End CBLatticeTheory. +End CBDistrLatticeTheory. +End CBDistrLatticeTheory. -Module Import CTBLatticeTheory. -Section CTBLatticeTheory. +Module Import CTBDistrLatticeTheory. +Section CTBDistrLatticeTheory. Context {disp : unit}. -Local Notation ctblatticeType := (ctblatticeType disp). -Context {L : ctblatticeType}. +Local Notation ctbDistrLatticeType := (ctbDistrLatticeType disp). +Context {L : ctbDistrLatticeType}. Implicit Types (x y z : L). Local Notation "0" := bottom. Local Notation "1" := top. @@ -3362,8 +3407,8 @@ Lemma compl_meets (J : Type) (r : seq J) (P : {pred J}) (F : J -> L) : ~` (\meet_(j <- r | P j) F j) = \join_(j <- r | P j) ~` F j. Proof. by elim/big_rec2: _=> [|i x y ? <-]; rewrite ?compl1 ?complI. Qed. -End CTBLatticeTheory. -End CTBLatticeTheory. +End CTBDistrLatticeTheory. +End CTBDistrLatticeTheory. (*************) (* FACTORIES *) @@ -3432,18 +3477,19 @@ case: (leP y z) => yz; case: (leP y x) => xy //=; first 1 last. - by have [] := (leP x z); rewrite ?xy ?yz. Qed. -Definition latticeMixin := - @LatticeMixin _ (@POrder.Pack disp T (POrder.class T)) _ _ - meetC joinC meetA joinA joinKI meetKU leEmeet meetUl. +Definition distrLatticeMixin := + @DistrLatticeMixin _ (@POrder.Pack disp T (POrder.class T)) _ _ + meetC joinC meetA joinA joinKI meetKU leEmeet meetUl. -Definition orderMixin : totalOrderMixin (LatticeType _ latticeMixin) := +Definition orderMixin : + totalOrderMixin (DistrLatticeType _ distrLatticeMixin) := m. End TotalPOrderMixin. Module Exports. Notation totalPOrderMixin := of_. -Coercion latticeMixin : totalPOrderMixin >-> Order.Lattice.mixin_of. +Coercion distrLatticeMixin : totalPOrderMixin >-> Order.DistrLattice.mixin_of. Coercion orderMixin : totalPOrderMixin >-> totalOrderMixin. End Exports. @@ -3541,10 +3587,10 @@ Definition porderMixin : lePOrderMixin T := Let T_porderType := POrderType tt T porderMixin. -Definition latticeMixin : latticeMixin T_porderType := - @LatticeMixin tt (POrderType tt T porderMixin) (meet m) (join m) - (meetC m) (joinC m) (meetA m) (joinA m) - (joinKI m) (meetKU m) (le_def m) (meetUl m). +Definition distrLatticeMixin : distrLatticeMixin T_porderType := + @DistrLatticeMixin tt (POrderType tt T porderMixin) (meet m) (join m) + (meetC m) (joinC m) (meetA m) (joinA m) + (joinKI m) (meetKU m) (le_def m) (meetUl m). End MeetJoinMixin. @@ -3552,7 +3598,7 @@ Module Exports. Notation meetJoinMixin := of_. Notation MeetJoinMixin := Build. Coercion porderMixin : meetJoinMixin >-> lePOrderMixin. -Coercion latticeMixin : meetJoinMixin >-> Lattice.mixin_of. +Coercion distrLatticeMixin : meetJoinMixin >-> DistrLattice.mixin_of. End Exports. End MeetJoinMixin. @@ -3586,11 +3632,11 @@ Definition lePOrderMixin := Let T_total_porderType : porderType tt := POrderType tt T lePOrderMixin. -Let T_total_latticeType : latticeType tt := - LatticeType T_total_porderType - (le_total m : totalPOrderMixin T_total_porderType). +Let T_total_distrLatticeType : distrLatticeType tt := + DistrLatticeType T_total_porderType + (le_total m : totalPOrderMixin T_total_porderType). -Implicit Types (x y z : T_total_latticeType). +Implicit Types (x y z : T_total_distrLatticeType). Fact meetE x y : meet m x y = x `&` y. Proof. by rewrite meet_def. Qed. Fact joinE x y : join m x y = x `|` y. Proof. by rewrite join_def. Qed. @@ -3613,21 +3659,22 @@ Proof. by move=> *; rewrite meetE meetxx. Qed. Fact le_def x y : x <= y = (meet m x y == x). Proof. by rewrite meetE (eq_meetl x y). Qed. -Definition latticeMixin : meetJoinMixin T := +Definition distrLatticeMixin : meetJoinMixin T := @MeetJoinMixin _ (le m) (lt m) (meet m) (join m) le_def (lt_def m) meetC joinC meetA joinA joinKI meetKU meetUl meetxx. -Let T_porderType := POrderType tt T latticeMixin. -Let T_latticeType : latticeType tt := LatticeType T_porderType latticeMixin. +Let T_porderType := POrderType tt T distrLatticeMixin. +Let T_distrLatticeType : distrLatticeType tt := + DistrLatticeType T_porderType distrLatticeMixin. -Definition totalMixin : totalOrderMixin T_latticeType := le_total m. +Definition totalMixin : totalOrderMixin T_distrLatticeType := le_total m. End LeOrderMixin. Module Exports. Notation leOrderMixin := of_. Notation LeOrderMixin := Build. -Coercion latticeMixin : leOrderMixin >-> meetJoinMixin. +Coercion distrLatticeMixin : leOrderMixin >-> meetJoinMixin. Coercion totalMixin : leOrderMixin >-> totalOrderMixin. End Exports. @@ -3662,11 +3709,11 @@ move=> x y; rewrite !le_def (eq_sym y). by case: (altP eqP); last exact: lt_total. Qed. -Let T_total_latticeType : latticeType tt := - LatticeType T_total_porderType +Let T_total_distrLatticeType : distrLatticeType tt := + DistrLatticeType T_total_porderType (le_total : totalPOrderMixin T_total_porderType). -Implicit Types (x y z : T_total_latticeType). +Implicit Types (x y z : T_total_distrLatticeType). Fact leP x y : lel_xor_gt x y (x <= y) (y < x) (y `&` x) (x `&` y) (y `|` x) (x `|` y). @@ -3694,22 +3741,23 @@ Proof. by move=> *; rewrite meetE meetxx. Qed. Fact le_def' x y : x <= y = (meet m x y == x). Proof. by rewrite meetE (eq_meetl x y). Qed. -Definition latticeMixin : meetJoinMixin T := +Definition distrLatticeMixin : meetJoinMixin T := @MeetJoinMixin _ (le m) (lt m) (meet m) (join m) - le_def' (@lt_def _ T_total_latticeType) + le_def' (@lt_def _ T_total_distrLatticeType) meetC joinC meetA joinA joinKI meetKU meetUl meetxx. -Let T_porderType := POrderType tt T latticeMixin. -Let T_latticeType : latticeType tt := LatticeType T_porderType latticeMixin. +Let T_porderType := POrderType tt T distrLatticeMixin. +Let T_distrLatticeType : distrLatticeType tt := + DistrLatticeType T_porderType distrLatticeMixin. -Definition totalMixin : totalOrderMixin T_latticeType := le_total. +Definition totalMixin : totalOrderMixin T_distrLatticeType := le_total. End LtOrderMixin. Module Exports. Notation ltOrderMixin := of_. Notation LtOrderMixin := Build. -Coercion latticeMixin : ltOrderMixin >-> meetJoinMixin. +Coercion distrLatticeMixin : ltOrderMixin >-> meetJoinMixin. Coercion totalMixin : ltOrderMixin >-> totalOrderMixin. End Exports. @@ -3782,10 +3830,10 @@ Definition CanOrder f' (f_can : cancel f f') := PcanOrder (can_pcan f_can). End Total. End Order. -Section Lattice. +Section DistrLattice. Variables (disp : unit) (T : porderType disp). -Variables (disp' : unit) (T' : latticeType disp) (f : T -> T'). +Variables (disp' : unit) (T' : distrLatticeType disp) (f : T -> T'). Variables (f' : T' -> T) (f_can : cancel f f') (f'_can : cancel f' f). Variable (f_mono : {mono f : x y / x <= y}). @@ -3808,9 +3856,10 @@ Proof. by rewrite /meet -(can_eq f_can) f'_can eq_meetl f_mono. Qed. Lemma meetUl : left_distributive meet join. Proof. by move=> x y z; rewrite /meet /join !f'_can meetUl. Qed. -Definition IsoLattice := LatticeMixin meetC joinC meetA joinA joinKI meetKI meet_eql meetUl. +Definition IsoDistrLattice := + DistrLatticeMixin meetC joinC meetA joinA joinKI meetKI meet_eql meetUl. -End Lattice. +End DistrLattice. End CanMixin. @@ -3820,7 +3869,7 @@ Notation PcanPOrderMixin := PcanPOrder. Notation CanPOrderMixin := CanPOrder. Notation PcanOrderMixin := PcanOrder. Notation CanOrderMixin := CanOrder. -Notation IsoLatticeMixin := IsoLattice. +Notation IsoDistrLatticeMixin := IsoDistrLattice. End Exports. End CanMixin. Import CanMixin.Exports. @@ -3844,7 +3893,8 @@ Context {disp : unit} {T : orderType disp} (P : {pred T}) (sT : subType P). Definition sub_TotalOrderMixin : totalPOrderMixin (sub_POrderType sT) := @MonoTotalMixin _ _ _ val (fun _ _ => erefl) (@le_total _ T). -Canonical sub_LatticeType := Eval hnf in LatticeType sT sub_TotalOrderMixin. +Canonical sub_DistrLatticeType := + Eval hnf in DistrLatticeType sT sub_TotalOrderMixin. Canonical sub_OrderType := Eval hnf in OrderType sT sub_TotalOrderMixin. End Total. @@ -3861,7 +3911,7 @@ Notation "[ 'totalOrderMixin' 'of' T 'by' <: ]" := only parsing) : form_scope. Canonical sub_POrderType. -Canonical sub_LatticeType. +Canonical sub_DistrLatticeType. Canonical sub_OrderType. Definition leEsub := @leEsub. @@ -3890,9 +3940,9 @@ Definition orderMixin := LeOrderMixin ltn_def minnE maxnE anti_leq leq_trans leq_total. Canonical porderType := POrderType total_display nat orderMixin. -Canonical latticeType := LatticeType nat orderMixin. +Canonical distrLatticeType := DistrLatticeType nat orderMixin. Canonical orderType := OrderType nat orderMixin. -Canonical blatticeType := BLatticeType nat (BLatticeMixin leq0n). +Canonical bDistrLatticeType := BDistrLatticeType nat (BDistrLatticeMixin leq0n). Lemma leEnat: le = leq. Proof. by []. Qed. Lemma ltEnat (n m : nat): (n < m) = (n < m)%N. Proof. by []. Qed. @@ -3900,9 +3950,9 @@ Lemma ltEnat (n m : nat): (n < m) = (n < m)%N. Proof. by []. Qed. End NatOrder. Module Exports. Canonical porderType. -Canonical latticeType. +Canonical distrLatticeType. Canonical orderType. -Canonical blatticeType. +Canonical bDistrLatticeType. Definition leEnat := leEnat. Definition ltEnat := ltEnat. End Exports. @@ -4012,7 +4062,7 @@ apply: eqn_from_log; rewrite ?(gcdn_gt0, lcmn_gt0)//= => p. by rewrite !(logn_gcd, logn_lcm) ?(gcdn_gt0, lcmn_gt0)// minn_maxl. Qed. -Definition t_latticeMixin := MeetJoinMixin le_def (fun _ _ => erefl _) +Definition t_distrLatticeMixin := MeetJoinMixin le_def (fun _ _ => erefl _) gcdnC lcmnC gcdnA lcmnA joinKI meetKU meetUl gcdnn. Import DvdSyntax. @@ -4021,12 +4071,12 @@ Definition t := nat. Canonical eqType := [eqType of t]. Canonical choiceType := [choiceType of t]. Canonical countType := [countType of t]. -Canonical porderType := POrderType dvd_display t t_latticeMixin. -Canonical latticeType := LatticeType t t_latticeMixin. -Canonical blatticeType := BLatticeType t - (BLatticeMixin (dvd1n : forall m : t, (1 %| m)%N)). -Canonical tlatticeType := TBLatticeType t - (TBLatticeMixin (dvdn0 : forall m : t, (m %| 0)%N)). +Canonical porderType := POrderType dvd_display t t_distrLatticeMixin. +Canonical distrLatticeType := DistrLatticeType t t_distrLatticeMixin. +Canonical bDistrLatticeType := BDistrLatticeType t + (BDistrLatticeMixin (dvd1n : forall m : t, (1 %| m)%N)). +Canonical tbDistrLatticeType := TBDistrLatticeType t + (TBDistrLatticeMixin (dvdn0 : forall m : t, (m %| 0)%N)). Lemma dvdE : dvd = dvdn :> rel t. Proof. by []. Qed. Lemma gcdE : gcd = gcdn :> (t -> t -> t). Proof. by []. Qed. @@ -4041,9 +4091,9 @@ Canonical eqType. Canonical choiceType. Canonical countType. Canonical porderType. -Canonical latticeType. -Canonical blatticeType. -Canonical tlatticeType. +Canonical distrLatticeType. +Canonical bDistrLatticeType. +Canonical tbDistrLatticeType. Definition dvdEnat := dvdE. Definition gcdEnat := gcdE. Definition lcmEnat := lcmE. @@ -4080,19 +4130,20 @@ Definition orderMixin := LeOrderMixin ltn_def andbE orbE anti leq_trans leq_total. Canonical porderType := POrderType total_display bool orderMixin. -Canonical latticeType := LatticeType bool orderMixin. +Canonical distrLatticeType := DistrLatticeType bool orderMixin. Canonical orderType := OrderType bool orderMixin. -Canonical blatticeType := BLatticeType bool - (@BLatticeMixin _ _ false (fun b : bool => leq0n b)). -Canonical tblatticeType := TBLatticeType bool (@TBLatticeMixin _ _ true leq_b1). -Canonical cblatticeType := CBLatticeType bool - (@CBLatticeMixin _ _ (fun x y => x && ~~ y) subKI joinIB). -Canonical ctblatticeType := CTBLatticeType bool - (@CTBLatticeMixin _ _ sub negb (fun x => erefl : ~~ x = sub true x)). +Canonical bDistrLatticeType := BDistrLatticeType bool + (@BDistrLatticeMixin _ _ false (fun b : bool => leq0n b)). +Canonical tbDistrLatticeType := + TBDistrLatticeType bool (@TBDistrLatticeMixin _ _ true leq_b1). +Canonical cbDistrLatticeType := CBDistrLatticeType bool + (@CBDistrLatticeMixin _ _ (fun x y => x && ~~ y) subKI joinIB). +Canonical ctbDistrLatticeType := CTBDistrLatticeType bool + (@CTBDistrLatticeMixin _ _ sub negb (fun x => erefl : ~~ x = sub true x)). Canonical finPOrderType := [finPOrderType of bool]. -Canonical finLatticeType := [finLatticeType of bool]. -Canonical finClatticeType := [finCLatticeType of bool]. +Canonical finDistrLatticeType := [finDistrLatticeType of bool]. +Canonical finCDistrLatticeType := [finCDistrLatticeType of bool]. Canonical finOrderType := [finOrderType of bool]. Lemma leEbool: le = (leq : rel bool). Proof. by []. Qed. @@ -4101,16 +4152,16 @@ Lemma ltEbool x y : (x < y) = (x < y)%N. Proof. by []. Qed. End BoolOrder. Module Exports. Canonical porderType. -Canonical latticeType. +Canonical distrLatticeType. Canonical orderType. -Canonical blatticeType. -Canonical cblatticeType. -Canonical tblatticeType. -Canonical ctblatticeType. +Canonical bDistrLatticeType. +Canonical cbDistrLatticeType. +Canonical tbDistrLatticeType. +Canonical ctbDistrLatticeType. Canonical finPOrderType. -Canonical finLatticeType. +Canonical finDistrLatticeType. Canonical finOrderType. -Canonical finClatticeType. +Canonical finCDistrLatticeType. Definition leEbool := leEbool. Definition ltEbool := ltEbool. End Exports. @@ -4391,8 +4442,8 @@ Proof. by rewrite ltEprod negb_and. Qed. End POrder. -Section Lattice. -Variable (T : latticeType disp1) (T' : latticeType disp2). +Section DistrLattice. +Variable (T : distrLatticeType disp1) (T' : distrLatticeType disp2). Implicit Types (x y : T * T'). Definition meet x y := (x.1 `&` y.1, x.2 `&` y.2). @@ -4422,9 +4473,9 @@ Proof. by rewrite eqE /= -!leEmeet. Qed. Fact meetUl : left_distributive meet join. Proof. by move=> ? ? ?; congr pair; rewrite meetUl. Qed. -Definition latticeMixin := - Lattice.Mixin meetC joinC meetA joinA joinKI meetKU leEmeet meetUl. -Canonical latticeType := LatticeType (T * T') latticeMixin. +Definition distrLatticeMixin := + DistrLattice.Mixin meetC joinC meetA joinA joinKI meetKU leEmeet meetUl. +Canonical distrLatticeType := DistrLatticeType (T * T') distrLatticeMixin. Lemma meetEprod x y : x `&` y = (x.1 `&` y.1, x.2 `&` y.2). Proof. by []. Qed. @@ -4432,34 +4483,36 @@ Proof. by []. Qed. Lemma joinEprod x y : x `|` y = (x.1 `|` y.1, x.2 `|` y.2). Proof. by []. Qed. -End Lattice. +End DistrLattice. -Section BLattice. -Variable (T : blatticeType disp1) (T' : blatticeType disp2). +Section BDistrLattice. +Variable (T : bDistrLatticeType disp1) (T' : bDistrLatticeType disp2). Fact le0x (x : T * T') : (0, 0) <= x :> T * T'. Proof. by rewrite /<=%O /= /le !le0x. Qed. -Canonical blatticeType := BLatticeType (T * T') (BLattice.Mixin le0x). +Canonical bDistrLatticeType := + BDistrLatticeType (T * T') (BDistrLattice.Mixin le0x). Lemma botEprod : 0 = (0, 0) :> T * T'. Proof. by []. Qed. -End BLattice. +End BDistrLattice. -Section TBLattice. -Variable (T : tblatticeType disp1) (T' : tblatticeType disp2). +Section TBDistrLattice. +Variable (T : tbDistrLatticeType disp1) (T' : tbDistrLatticeType disp2). Fact lex1 (x : T * T') : x <= (top, top). Proof. by rewrite /<=%O /= /le !lex1. Qed. -Canonical tblatticeType := TBLatticeType (T * T') (TBLattice.Mixin lex1). +Canonical tbDistrLatticeType := + TBDistrLatticeType (T * T') (TBDistrLattice.Mixin lex1). Lemma topEprod : 1 = (1, 1) :> T * T'. Proof. by []. Qed. -End TBLattice. +End TBDistrLattice. -Section CBLattice. -Variable (T : cblatticeType disp1) (T' : cblatticeType disp2). +Section CBDistrLattice. +Variable (T : cbDistrLatticeType disp1) (T' : cbDistrLatticeType disp2). Implicit Types (x y : T * T'). Definition sub x y := (x.1 `\` y.1, x.2 `\` y.2). @@ -4470,16 +4523,16 @@ Proof. by congr pair; rewrite subKI. Qed. Lemma joinIB x y : x `&` y `|` sub x y = x. Proof. by case: x => ? ?; congr pair; rewrite joinIB. Qed. -Definition cblatticeMixin := CBLattice.Mixin subKI joinIB. -Canonical cblatticeType := CBLatticeType (T * T') cblatticeMixin. +Definition cbDistrLatticeMixin := CBDistrLattice.Mixin subKI joinIB. +Canonical cbDistrLatticeType := CBDistrLatticeType (T * T') cbDistrLatticeMixin. Lemma subEprod x y : x `\` y = (x.1 `\` y.1, x.2 `\` y.2). Proof. by []. Qed. -End CBLattice. +End CBDistrLattice. -Section CTBLattice. -Variable (T : ctblatticeType disp1) (T' : ctblatticeType disp2). +Section CTBDistrLattice. +Variable (T : ctbDistrLatticeType disp1) (T' : ctbDistrLatticeType disp2). Implicit Types (x y : T * T'). Definition compl x : T * T' := (~` x.1, ~` x.2). @@ -4487,28 +4540,29 @@ Definition compl x : T * T' := (~` x.1, ~` x.2). Lemma complE x : compl x = sub 1 x. Proof. by congr pair; rewrite complE. Qed. -Definition ctblatticeMixin := CTBLattice.Mixin complE. -Canonical ctblatticeType := CTBLatticeType (T * T') ctblatticeMixin. +Definition ctbDistrLatticeMixin := CTBDistrLattice.Mixin complE. +Canonical ctbDistrLatticeType := + CTBDistrLatticeType (T * T') ctbDistrLatticeMixin. Lemma complEprod x : ~` x = (~` x.1, ~` x.2). Proof. by []. Qed. -End CTBLattice. +End CTBDistrLattice. Canonical finPOrderType (T : finPOrderType disp1) (T' : finPOrderType disp2) := [finPOrderType of T * T']. -Canonical finLatticeType (T : finLatticeType disp1) - (T' : finLatticeType disp2) := [finLatticeType of T * T']. +Canonical finDistrLatticeType (T : finDistrLatticeType disp1) + (T' : finDistrLatticeType disp2) := [finDistrLatticeType of T * T']. -Canonical finClatticeType (T : finCLatticeType disp1) - (T' : finCLatticeType disp2) := [finCLatticeType of T * T']. +Canonical finCDistrLatticeType (T : finCDistrLatticeType disp1) + (T' : finCDistrLatticeType disp2) := [finCDistrLatticeType of T * T']. End ProdOrder. Module Exports. -Notation "T *p[ d ] T'" := (type d T T') - (at level 70, d at next level, format "T *p[ d ] T'") : order_scope. +Notation "T *prod[ d ] T'" := (type d T T') + (at level 70, d at next level, format "T *prod[ d ] T'") : order_scope. Notation "T *p T'" := (type prod_display T T') (at level 70, format "T *p T'") : order_scope. @@ -4517,14 +4571,14 @@ Canonical choiceType. Canonical countType. Canonical finType. Canonical porderType. -Canonical latticeType. -Canonical blatticeType. -Canonical tblatticeType. -Canonical cblatticeType. -Canonical ctblatticeType. +Canonical distrLatticeType. +Canonical bDistrLatticeType. +Canonical tbDistrLatticeType. +Canonical cbDistrLatticeType. +Canonical ctbDistrLatticeType. Canonical finPOrderType. -Canonical finLatticeType. -Canonical finClatticeType. +Canonical finDistrLatticeType. +Canonical finCDistrLatticeType. Definition leEprod := @leEprod. Definition ltEprod := @ltEprod. @@ -4547,26 +4601,27 @@ Context {disp1 disp2 : unit}. Canonical prod_porderType (T : porderType disp1) (T' : porderType disp2) := [porderType of T * T' for [porderType of T *p T']]. -Canonical prod_latticeType (T : latticeType disp1) (T' : latticeType disp2) := - [latticeType of T * T' for [latticeType of T *p T']]. -Canonical prod_blatticeType - (T : blatticeType disp1) (T' : blatticeType disp2) := - [blatticeType of T * T' for [blatticeType of T *p T']]. -Canonical prod_tblatticeType - (T : tblatticeType disp1) (T' : tblatticeType disp2) := - [tblatticeType of T * T' for [tblatticeType of T *p T']]. -Canonical prod_cblatticeType - (T : cblatticeType disp1) (T' : cblatticeType disp2) := - [cblatticeType of T * T' for [cblatticeType of T *p T']]. -Canonical prod_ctblatticeType - (T : ctblatticeType disp1) (T' : ctblatticeType disp2) := - [ctblatticeType of T * T' for [ctblatticeType of T *p T']]. +Canonical prod_distrLatticeType + (T : distrLatticeType disp1) (T' : distrLatticeType disp2) := + [distrLatticeType of T * T' for [distrLatticeType of T *p T']]. +Canonical prod_bDistrLatticeType + (T : bDistrLatticeType disp1) (T' : bDistrLatticeType disp2) := + [bDistrLatticeType of T * T' for [bDistrLatticeType of T *p T']]. +Canonical prod_tbDistrLatticeType + (T : tbDistrLatticeType disp1) (T' : tbDistrLatticeType disp2) := + [tbDistrLatticeType of T * T' for [tbDistrLatticeType of T *p T']]. +Canonical prod_cbDistrLatticeType + (T : cbDistrLatticeType disp1) (T' : cbDistrLatticeType disp2) := + [cbDistrLatticeType of T * T' for [cbDistrLatticeType of T *p T']]. +Canonical prod_ctbDistrLatticeType + (T : ctbDistrLatticeType disp1) (T' : ctbDistrLatticeType disp2) := + [ctbDistrLatticeType of T * T' for [ctbDistrLatticeType of T *p T']]. Canonical prod_finPOrderType (T : finPOrderType disp1) (T' : finPOrderType disp2) := [finPOrderType of T * T']. -Canonical prod_finLatticeType (T : finLatticeType disp1) - (T' : finLatticeType disp2) := [finLatticeType of T * T']. -Canonical prod_finClatticeType (T : finCLatticeType disp1) - (T' : finCLatticeType disp2) := [finCLatticeType of T * T']. +Canonical prod_finDistrLatticeType (T : finDistrLatticeType disp1) + (T' : finDistrLatticeType disp2) := [finDistrLatticeType of T * T']. +Canonical prod_finCDistrLatticeType (T : finCDistrLatticeType disp1) + (T' : finCDistrLatticeType disp2) := [finCDistrLatticeType of T * T']. End DefaultProdOrder. End DefaultProdOrder. @@ -4649,12 +4704,12 @@ case: x y => [x x'] [y y']/= eqxy; elim: _ /eqxy in y' *. by rewrite !tagged_asE le_total. Qed. -Canonical latticeType := LatticeType {t : T & T' t} total. +Canonical distrLatticeType := DistrLatticeType {t : T & T' t} total. Canonical orderType := OrderType {t : T & T' t} total. End Total. -Section FinLattice. +Section FinDistrLattice. Variable (T : finOrderType disp1) (T' : T -> finOrderType disp2). Fact le0x (x : {t : T & T' t}) : Tagged T' (0 : T' 0) <= x. @@ -4662,7 +4717,8 @@ Proof. rewrite leEsig /=; case: comparableP (le0x (tag x)) => //=. by case: x => //= x px x0; rewrite x0 in px *; rewrite tagged_asE le0x. Qed. -Canonical blatticeType := BLatticeType {t : T & T' t} (BLattice.Mixin le0x). +Canonical bDistrLatticeType := + BDistrLatticeType {t : T & T' t} (BDistrLattice.Mixin le0x). Lemma botEsig : 0 = Tagged T' (0 : T' 0). Proof. by []. Qed. @@ -4671,16 +4727,17 @@ Proof. rewrite leEsig /=; case: comparableP (lex1 (tag x)) => //=. by case: x => //= x px x0; rewrite x0 in px *; rewrite tagged_asE lex1. Qed. -Canonical tblatticeType := TBLatticeType {t : T & T' t} (TBLattice.Mixin lex1). +Canonical tbDistrLatticeType := + TBDistrLatticeType {t : T & T' t} (TBDistrLattice.Mixin lex1). Lemma topEsig : 1 = Tagged T' (1 : T' 1). Proof. by []. Qed. -End FinLattice. +End FinDistrLattice. Canonical finPOrderType (T : finPOrderType disp1) (T' : T -> finPOrderType disp2) := [finPOrderType of {t : T & T' t}]. -Canonical finLatticeType (T : finOrderType disp1) - (T' : T -> finOrderType disp2) := [finLatticeType of {t : T & T' t}]. +Canonical finDistrLatticeType (T : finOrderType disp1) + (T' : T -> finOrderType disp2) := [finDistrLatticeType of {t : T & T' t}]. Canonical finOrderType (T : finOrderType disp1) (T' : T -> finOrderType disp2) := [finOrderType of {t : T & T' t}]. @@ -4689,10 +4746,10 @@ End SigmaOrder. Module Exports. Canonical porderType. -Canonical latticeType. +Canonical distrLatticeType. Canonical orderType. Canonical finPOrderType. -Canonical finLatticeType. +Canonical finDistrLatticeType. Canonical finOrderType. Definition leEsig := @leEsig. @@ -4781,38 +4838,40 @@ Proof. move=> x y; rewrite /<=%O /= /le; case: ltgtP => //= _; exact: le_total. Qed. -Canonical latticeType := LatticeType (T * T') total. +Canonical distrLatticeType := DistrLatticeType (T * T') total. Canonical orderType := OrderType (T * T') total. End Total. -Section FinLattice. +Section FinDistrLattice. Variable (T : finOrderType disp1) (T' : finOrderType disp2). Fact le0x (x : T * T') : (0, 0) <= x :> T * T'. Proof. by case: x => // x1 x2; rewrite leEprodlexi/= !le0x implybT. Qed. -Canonical blatticeType := BLatticeType (T * T') (BLattice.Mixin le0x). +Canonical bDistrLatticeType := + BDistrLatticeType (T * T') (BDistrLattice.Mixin le0x). Lemma botEprodlexi : 0 = (0, 0) :> T * T'. Proof. by []. Qed. Fact lex1 (x : T * T') : x <= (1, 1) :> T * T'. Proof. by case: x => // x1 x2; rewrite leEprodlexi/= !lex1 implybT. Qed. -Canonical tblatticeType := TBLatticeType (T * T') (TBLattice.Mixin lex1). +Canonical tbDistrLatticeType := + TBDistrLatticeType (T * T') (TBDistrLattice.Mixin lex1). Lemma topEprodlexi : 1 = (1, 1) :> T * T'. Proof. by []. Qed. -End FinLattice. +End FinDistrLattice. Canonical finPOrderType (T : finPOrderType disp1) (T' : finPOrderType disp2) := [finPOrderType of T * T']. -Canonical finLatticeType (T : finOrderType disp1) - (T' : finOrderType disp2) := [finLatticeType of T * T']. +Canonical finDistrLatticeType (T : finOrderType disp1) + (T' : finOrderType disp2) := [finDistrLatticeType of T * T']. Canonical finOrderType (T : finOrderType disp1) (T' : finOrderType disp2) := [finOrderType of T * T']. Lemma sub_prod_lexi d (T : POrder.Exports.porderType disp1) (T' : POrder.Exports.porderType disp2) : - subrel (<=%O : rel (T *p[d] T')) (<=%O : rel (T * T')). + subrel (<=%O : rel (T *prod[d] T')) (<=%O : rel (T * T')). Proof. by case=> [x1 x2] [y1 y2]; rewrite leEprod leEprodlexi /=; case: comparableP. Qed. @@ -4821,8 +4880,8 @@ End ProdLexiOrder. Module Exports. -Notation "T *l[ d ] T'" := (type d T T') - (at level 70, d at next level, format "T *l[ d ] T'") : order_scope. +Notation "T *lexi[ d ] T'" := (type d T T') + (at level 70, d at next level, format "T *lexi[ d ] T'") : order_scope. Notation "T *l T'" := (type lexi_display T T') (at level 70, format "T *l T'") : order_scope. @@ -4831,12 +4890,12 @@ Canonical choiceType. Canonical countType. Canonical finType. Canonical porderType. -Canonical latticeType. +Canonical distrLatticeType. Canonical orderType. -Canonical blatticeType. -Canonical tblatticeType. +Canonical bDistrLatticeType. +Canonical tbDistrLatticeType. Canonical finPOrderType. -Canonical finLatticeType. +Canonical finDistrLatticeType. Canonical finOrderType. Definition leEprodlexi := @leEprodlexi. @@ -4858,22 +4917,22 @@ Context {disp1 disp2 : unit}. Canonical prodlexi_porderType (T : porderType disp1) (T' : porderType disp2) := [porderType of T * T' for [porderType of T *l T']]. -Canonical prodlexi_latticeType +Canonical prodlexi_distrLatticeType (T : orderType disp1) (T' : orderType disp2) := - [latticeType of T * T' for [latticeType of T *l T']]. + [distrLatticeType of T * T' for [distrLatticeType of T *l T']]. Canonical prodlexi_orderType (T : orderType disp1) (T' : orderType disp2) := [orderType of T * T' for [orderType of T *l T']]. -Canonical prodlexi_blatticeType +Canonical prodlexi_bDistrLatticeType (T : finOrderType disp1) (T' : finOrderType disp2) := - [blatticeType of T * T' for [blatticeType of T *l T']]. -Canonical prodlexi_tblatticeType + [bDistrLatticeType of T * T' for [bDistrLatticeType of T *l T']]. +Canonical prodlexi_tbDistrLatticeType (T : finOrderType disp1) (T' : finOrderType disp2) := - [tblatticeType of T * T' for [tblatticeType of T *l T']]. + [tbDistrLatticeType of T * T' for [tbDistrLatticeType of T *l T']]. Canonical prodlexi_finPOrderType (T : finPOrderType disp1) (T' : finPOrderType disp2) := [finPOrderType of T * T']. -Canonical prodlexi_finLatticeType (T : finOrderType disp1) - (T' : finOrderType disp2) := [finLatticeType of T * T']. +Canonical prodlexi_finDistrLatticeType (T : finOrderType disp1) + (T' : finOrderType disp2) := [finDistrLatticeType of T * T']. Canonical prodlexi_finOrderType (T : finOrderType disp1) (T' : finOrderType disp2) := [finOrderType of T * T']. @@ -4932,8 +4991,8 @@ Proof. by []. Qed. End POrder. -Section BLattice. -Variable T : latticeType disp. +Section BDistrLattice. +Variable T : distrLatticeType disp. Implicit Types s : seq T. Fixpoint meet s1 s2 := @@ -4980,10 +5039,11 @@ Qed. Fact meetUl : left_distributive meet join. Proof. by elim=> [|? ? ih] [|? ?] [|? ?] //=; rewrite meetUl ih. Qed. -Definition latticeMixin := - Lattice.Mixin meetC joinC meetA joinA joinKI meetKU leEmeet meetUl. -Canonical latticeType := LatticeType (seq T) latticeMixin. -Canonical blatticeType := BLatticeType (seq T) (BLattice.Mixin (@le0s _)). +Definition distrLatticeMixin := + DistrLattice.Mixin meetC joinC meetA joinA joinKI meetKU leEmeet meetUl. +Canonical distrLatticeType := DistrLatticeType (seq T) distrLatticeMixin. +Canonical bDistrLatticeType := + BDistrLatticeType (seq T) (BDistrLattice.Mixin (@le0s _)). Lemma botEseq : 0 = [::] :> seq T. Proof. by []. Qed. @@ -5006,7 +5066,7 @@ Lemma join_cons x1 s1 x2 s2 : (x1 :: s1 : seq T) `|` (x2 :: s2) = (x1 `|` x2) :: s1 `|` s2. Proof. by []. Qed. -End BLattice. +End BDistrLattice. End SeqProdOrder. @@ -5016,8 +5076,8 @@ Notation seqprod_with := type. Notation seqprod := (type prod_display). Canonical porderType. -Canonical latticeType. -Canonical blatticeType. +Canonical distrLatticeType. +Canonical bDistrLatticeType. Definition leEseq := @leEseq. Definition le0s := @le0s. @@ -5038,10 +5098,10 @@ Context {disp : unit}. Canonical seqprod_porderType (T : porderType disp) := [porderType of seq T for [porderType of seqprod T]]. -Canonical seqprod_latticeType (T : latticeType disp) := - [latticeType of seq T for [latticeType of seqprod T]]. -Canonical seqprod_blatticeType (T : blatticeType disp) := - [blatticeType of seq T for [blatticeType of seqprod T]]. +Canonical seqprod_distrLatticeType (T : distrLatticeType disp) := + [distrLatticeType of seq T for [distrLatticeType of seqprod T]]. +Canonical seqprod_bDistrLatticeType (T : bDistrLatticeType disp) := + [bDistrLatticeType of seq T for [bDistrLatticeType of seqprod T]]. End DefaultSeqProdOrder. End DefaultSeqProdOrder. @@ -5155,8 +5215,9 @@ suff: total (<=%O : rel (seq T)) by []. by elim=> [|x1 s1 ihs1] [|x2 s2]//=; rewrite !lexi_cons; case: ltgtP => /=. Qed. -Canonical latticeType := LatticeType (seq T) total. -Canonical blatticeType := BLatticeType (seq T) (BLattice.Mixin (@lexi0s _)). +Canonical distrLatticeType := DistrLatticeType (seq T) total. +Canonical bDistrLatticeType := + BDistrLatticeType (seq T) (BDistrLattice.Mixin (@lexi0s _)). Canonical orderType := OrderType (seq T) total. End Total. @@ -5176,8 +5237,8 @@ Notation seqlexi_with := type. Notation seqlexi := (type lexi_display). Canonical porderType. -Canonical latticeType. -Canonical blatticeType. +Canonical distrLatticeType. +Canonical bDistrLatticeType. Canonical orderType. Definition leEseqlexi := @leEseqlexi. @@ -5207,10 +5268,10 @@ Context {disp : unit}. Canonical seqlexi_porderType (T : porderType disp) := [porderType of seq T for [porderType of seqlexi T]]. -Canonical seqlexi_latticeType (T : orderType disp) := - [latticeType of seq T for [latticeType of seqlexi T]]. -Canonical seqlexi_blatticeType (T : orderType disp) := - [blatticeType of seq T for [blatticeType of seqlexi T]]. +Canonical seqlexi_distrLatticeType (T : orderType disp) := + [distrLatticeType of seq T for [distrLatticeType of seqlexi T]]. +Canonical seqlexi_bDistrLatticeType (T : orderType disp) := + [bDistrLatticeType of seq T for [bDistrLatticeType of seqlexi T]]. Canonical seqlexi_orderType (T : orderType disp) := [orderType of seq T for [orderType of seqlexi T]]. @@ -5262,8 +5323,8 @@ Proof. by rewrite lt_neqAle leEtprod eqEtuple negb_forall. Qed. End POrder. -Section Lattice. -Variables (n : nat) (T : latticeType disp). +Section DistrLattice. +Variables (n : nat) (T : distrLatticeType disp). Implicit Types (t : n.-tuple T). Definition meet t1 t2 : n.-tuple T := @@ -5317,9 +5378,9 @@ move=> t1 t2 t3; apply: eq_from_tnth => i. by rewrite !(tnth_meet, tnth_join) meetUl. Qed. -Definition latticeMixin := - Lattice.Mixin meetC joinC meetA joinA joinKI meetKU leEmeet meetUl. -Canonical latticeType := LatticeType (n.-tuple T) latticeMixin. +Definition distrLatticeMixin := + DistrLattice.Mixin meetC joinC meetA joinA joinKI meetKU leEmeet meetUl. +Canonical distrLatticeType := DistrLatticeType (n.-tuple T) distrLatticeMixin. Lemma meetEtprod t1 t2 : t1 `&` t2 = [tuple of [seq x.1 `&` x.2 | x <- zip t1 t2]]. @@ -5329,36 +5390,38 @@ Lemma joinEtprod t1 t2 : t1 `|` t2 = [tuple of [seq x.1 `|` x.2 | x <- zip t1 t2]]. Proof. by []. Qed. -End Lattice. +End DistrLattice. -Section BLattice. -Variables (n : nat) (T : blatticeType disp). +Section BDistrLattice. +Variables (n : nat) (T : bDistrLatticeType disp). Implicit Types (t : n.-tuple T). Fact le0x t : [tuple of nseq n 0] <= t :> n.-tuple T. Proof. by rewrite leEtprod; apply/forallP => i; rewrite tnth_nseq le0x. Qed. -Canonical blatticeType := BLatticeType (n.-tuple T) (BLattice.Mixin le0x). +Canonical bDistrLatticeType := + BDistrLatticeType (n.-tuple T) (BDistrLattice.Mixin le0x). Lemma botEtprod : 0 = [tuple of nseq n 0] :> n.-tuple T. Proof. by []. Qed. -End BLattice. +End BDistrLattice. -Section TBLattice. -Variables (n : nat) (T : tblatticeType disp). +Section TBDistrLattice. +Variables (n : nat) (T : tbDistrLatticeType disp). Implicit Types (t : n.-tuple T). Fact lex1 t : t <= [tuple of nseq n 1] :> n.-tuple T. Proof. by rewrite leEtprod; apply/forallP => i; rewrite tnth_nseq lex1. Qed. -Canonical tblatticeType := TBLatticeType (n.-tuple T) (TBLattice.Mixin lex1). +Canonical tbDistrLatticeType := + TBDistrLatticeType (n.-tuple T) (TBDistrLattice.Mixin lex1). Lemma topEtprod : 1 = [tuple of nseq n 1] :> n.-tuple T. Proof. by []. Qed. -End TBLattice. +End TBDistrLattice. -Section CBLattice. -Variables (n : nat) (T : cblatticeType disp). +Section CBDistrLattice. +Variables (n : nat) (T : cbDistrLatticeType disp). Implicit Types (t : n.-tuple T). Definition sub t1 t2 : n.-tuple T := @@ -5380,16 +5443,18 @@ Proof. by apply: eq_from_tnth => i; rewrite tnth_join tnth_meet tnth_sub joinIB. Qed. -Definition cblatticeMixin := CBLattice.Mixin subKI joinIB. -Canonical cblatticeType := CBLatticeType (n.-tuple T) cblatticeMixin. +Definition cbDistrLatticeMixin := CBDistrLattice.Mixin subKI joinIB. +Canonical cbDistrLatticeType := + CBDistrLatticeType (n.-tuple T) cbDistrLatticeMixin. -Lemma subEtprod t1 t2 : t1 `\` t2 = [tuple of [seq x.1 `\` x.2 | x <- zip t1 t2]]. +Lemma subEtprod t1 t2 : + t1 `\` t2 = [tuple of [seq x.1 `\` x.2 | x <- zip t1 t2]]. Proof. by []. Qed. -End CBLattice. +End CBDistrLattice. -Section CTBLattice. -Variables (n : nat) (T : ctblatticeType disp). +Section CTBDistrLattice. +Variables (n : nat) (T : ctbDistrLatticeType disp). Implicit Types (t : n.-tuple T). Definition compl t : n.-tuple T := map_tuple compl t. @@ -5402,29 +5467,31 @@ Proof. by apply: eq_from_tnth => i; rewrite tnth_compl tnth_sub complE tnth_nseq. Qed. -Definition ctblatticeMixin := CTBLattice.Mixin complE. -Canonical ctblatticeType := CTBLatticeType (n.-tuple T) ctblatticeMixin. +Definition ctbDistrLatticeMixin := CTBDistrLattice.Mixin complE. +Canonical ctbDistrLatticeType := + CTBDistrLatticeType (n.-tuple T) ctbDistrLatticeMixin. Lemma complEtprod t : ~` t = [tuple of [seq ~` x | x <- t]]. Proof. by []. Qed. -End CTBLattice. +End CTBDistrLattice. Canonical finPOrderType n (T : finPOrderType disp) := [finPOrderType of n.-tuple T]. -Canonical finLatticeType n (T : finLatticeType disp) := - [finLatticeType of n.-tuple T]. +Canonical finDistrLatticeType n (T : finDistrLatticeType disp) := + [finDistrLatticeType of n.-tuple T]. -Canonical finClatticeType n (T : finCLatticeType disp) := - [finCLatticeType of n.-tuple T]. +Canonical finCDistrLatticeType n (T : finCDistrLatticeType disp) := + [finCDistrLatticeType of n.-tuple T]. End TupleProdOrder. Module Exports. Notation "n .-tupleprod[ disp ]" := (type disp n) - (at level 2, disp at next level, format "n .-tupleprod[ disp ]") : order_scope. + (at level 2, disp at next level, format "n .-tupleprod[ disp ]") : + order_scope. Notation "n .-tupleprod" := (n.-tupleprod[prod_display]) (at level 2, format "n .-tupleprod") : order_scope. @@ -5433,14 +5500,14 @@ Canonical choiceType. Canonical countType. Canonical finType. Canonical porderType. -Canonical latticeType. -Canonical blatticeType. -Canonical tblatticeType. -Canonical cblatticeType. -Canonical ctblatticeType. +Canonical distrLatticeType. +Canonical bDistrLatticeType. +Canonical tbDistrLatticeType. +Canonical cbDistrLatticeType. +Canonical ctbDistrLatticeType. Canonical finPOrderType. -Canonical finLatticeType. -Canonical finClatticeType. +Canonical finDistrLatticeType. +Canonical finCDistrLatticeType. Definition leEtprod := @leEtprod. Definition ltEtprod := @ltEtprod. @@ -5466,22 +5533,23 @@ Context {disp : unit}. Canonical tprod_porderType n (T : porderType disp) := [porderType of n.-tuple T for [porderType of n.-tupleprod T]]. -Canonical tprod_latticeType n (T : latticeType disp) := - [latticeType of n.-tuple T for [latticeType of n.-tupleprod T]]. -Canonical tprod_blatticeType n (T : blatticeType disp) := - [blatticeType of n.-tuple T for [blatticeType of n.-tupleprod T]]. -Canonical tprod_tblatticeType n (T : tblatticeType disp) := - [tblatticeType of n.-tuple T for [tblatticeType of n.-tupleprod T]]. -Canonical tprod_cblatticeType n (T : cblatticeType disp) := - [cblatticeType of n.-tuple T for [cblatticeType of n.-tupleprod T]]. -Canonical tprod_ctblatticeType n (T : ctblatticeType disp) := - [ctblatticeType of n.-tuple T for [ctblatticeType of n.-tupleprod T]]. +Canonical tprod_distrLatticeType n (T : distrLatticeType disp) := + [distrLatticeType of n.-tuple T for [distrLatticeType of n.-tupleprod T]]. +Canonical tprod_bDistrLatticeType n (T : bDistrLatticeType disp) := + [bDistrLatticeType of n.-tuple T for [bDistrLatticeType of n.-tupleprod T]]. +Canonical tprod_tbDistrLatticeType n (T : tbDistrLatticeType disp) := + [tbDistrLatticeType of n.-tuple T for [tbDistrLatticeType of n.-tupleprod T]]. +Canonical tprod_cbDistrLatticeType n (T : cbDistrLatticeType disp) := + [cbDistrLatticeType of n.-tuple T for [cbDistrLatticeType of n.-tupleprod T]]. +Canonical tprod_ctbDistrLatticeType n (T : ctbDistrLatticeType disp) := + [ctbDistrLatticeType of n.-tuple T for + [ctbDistrLatticeType of n.-tupleprod T]]. Canonical tprod_finPOrderType n (T : finPOrderType disp) := [finPOrderType of n.-tuple T]. -Canonical tprod_finLatticeType n (T : finLatticeType disp) := - [finLatticeType of n.-tuple T]. -Canonical tprod_finClatticeType n (T : finCLatticeType disp) := - [finCLatticeType of n.-tuple T]. +Canonical tprod_finDistrLatticeType n (T : finDistrLatticeType disp) := + [finDistrLatticeType of n.-tuple T]. +Canonical tprod_finCDistrLatticeType n (T : finCDistrLatticeType disp) := + [finCDistrLatticeType of n.-tuple T]. End DefaultTupleProdOrder. End DefaultTupleProdOrder. @@ -5522,9 +5590,9 @@ rewrite [_ <= _]lexi_cons; apply: (iffP idP) => [|[k leif_xt12]]. case: comparableP => //= [ltx12 _|-> /IHn[k kP]]. exists ord0 => i; rewrite leqn0 => /eqP/(@ord_inj n.+1 i ord0)->. by apply/leifP; rewrite !tnth0. - exists (lift ord0 k) => i; case: (unliftP ord0 i) => [j ->|-> _]; last first. - by apply/leifP; rewrite !tnth0 eqxx. - by rewrite !ltnS => /kP; rewrite !tnthS. + exists (lift ord0 k) => i; case: (unliftP ord0 i) => [j ->|-> _]. + by rewrite !ltnS => /kP; rewrite !tnthS. + by apply/leifP; rewrite !tnth0 eqxx. have /= := leif_xt12 ord0 isT; rewrite !tnth0 => leif_x12. rewrite leif_x12/=; move: leif_x12 leif_xt12 => /leifP. case: (unliftP ord0 k) => {k} [k-> /eqP<-{x2}|-> /lt_geF->//] leif_xt12. @@ -5543,9 +5611,9 @@ rewrite [_ < _]ltxi_cons; apply: (iffP idP) => [|[k leif_xt12]]. case: (comparableP x1 x2) => //= [ltx12 _|-> /IHn[k kP]]. exists ord0 => i; rewrite leqn0 => /eqP/(@ord_inj n.+1 i ord0)->. by apply/leifP; rewrite !tnth0. - exists (lift ord0 k) => i; case: (unliftP ord0 i) => {i} [i ->|-> _]; last first. - by apply/leifP; rewrite !tnth0 eqxx. - by rewrite !ltnS => /kP; rewrite !tnthS. + exists (lift ord0 k) => i; case: (unliftP ord0 i) => {i} [i ->|-> _]. + by rewrite !ltnS => /kP; rewrite !tnthS. + by apply/leifP; rewrite !tnth0 eqxx. have /= := leif_xt12 ord0 isT; rewrite !tnth0 => leif_x12. rewrite leif_x12/=; move: leif_x12 leif_xt12 => /leifP. case: (unliftP ord0 k) => {k} [k-> /eqP<-{x2}|-> /lt_geF->//] leif_xt12. @@ -5573,41 +5641,43 @@ Implicit Types (t : n.-tuple T). Definition total : totalPOrderMixin [porderType of n.-tuple T] := [totalOrderMixin of n.-tuple T by <:]. -Canonical latticeType := LatticeType (n.-tuple T) total. +Canonical distrLatticeType := DistrLatticeType (n.-tuple T) total. Canonical orderType := OrderType (n.-tuple T) total. End Total. -Section BLattice. +Section BDistrLattice. Variables (n : nat) (T : finOrderType disp). Implicit Types (t : n.-tuple T). Fact le0x t : [tuple of nseq n 0] <= t :> n.-tuple T. Proof. by apply: sub_seqprod_lexi; apply: le0x (t : n.-tupleprod T). Qed. -Canonical blatticeType := BLatticeType (n.-tuple T) (BLattice.Mixin le0x). +Canonical bDistrLatticeType := + BDistrLatticeType (n.-tuple T) (BDistrLattice.Mixin le0x). Lemma botEtlexi : 0 = [tuple of nseq n 0] :> n.-tuple T. Proof. by []. Qed. -End BLattice. +End BDistrLattice. -Section TBLattice. +Section TBDistrLattice. Variables (n : nat) (T : finOrderType disp). Implicit Types (t : n.-tuple T). Fact lex1 t : t <= [tuple of nseq n 1]. Proof. by apply: sub_seqprod_lexi; apply: lex1 (t : n.-tupleprod T). Qed. -Canonical tblatticeType := TBLatticeType (n.-tuple T) (TBLattice.Mixin lex1). +Canonical tbDistrLatticeType := + TBDistrLatticeType (n.-tuple T) (TBDistrLattice.Mixin lex1). Lemma topEtlexi : 1 = [tuple of nseq n 1] :> n.-tuple T. Proof. by []. Qed. -End TBLattice. +End TBDistrLattice. Canonical finPOrderType n (T : finPOrderType disp) := [finPOrderType of n.-tuple T]. -Canonical finLatticeType n (T : finOrderType disp) := - [finLatticeType of n.-tuple T]. +Canonical finDistrLatticeType n (T : finOrderType disp) := + [finDistrLatticeType of n.-tuple T]. Canonical finOrderType n (T : finOrderType disp) := [finOrderType of n.-tuple T]. @@ -5620,7 +5690,8 @@ End TupleLexiOrder. Module Exports. Notation "n .-tuplelexi[ disp ]" := (type disp n) - (at level 2, disp at next level, format "n .-tuplelexi[ disp ]") : order_scope. + (at level 2, disp at next level, format "n .-tuplelexi[ disp ]") : + order_scope. Notation "n .-tuplelexi" := (n.-tuplelexi[lexi_display]) (at level 2, format "n .-tuplelexi") : order_scope. @@ -5629,12 +5700,12 @@ Canonical choiceType. Canonical countType. Canonical finType. Canonical porderType. -Canonical latticeType. +Canonical distrLatticeType. Canonical orderType. -Canonical blatticeType. -Canonical tblatticeType. +Canonical bDistrLatticeType. +Canonical tbDistrLatticeType. Canonical finPOrderType. -Canonical finLatticeType. +Canonical finDistrLatticeType. Canonical finOrderType. Definition lexi_tupleP := @lexi_tupleP. @@ -5657,18 +5728,18 @@ Context {disp : unit}. Canonical tlexi_porderType n (T : porderType disp) := [porderType of n.-tuple T for [porderType of n.-tuplelexi T]]. -Canonical tlexi_latticeType n (T : orderType disp) := - [latticeType of n.-tuple T for [latticeType of n.-tuplelexi T]]. -Canonical tlexi_blatticeType n (T : finOrderType disp) := - [blatticeType of n.-tuple T for [blatticeType of n.-tuplelexi T]]. -Canonical tlexi_tblatticeType n (T : finOrderType disp) := - [tblatticeType of n.-tuple T for [tblatticeType of n.-tuplelexi T]]. +Canonical tlexi_distrLatticeType n (T : orderType disp) := + [distrLatticeType of n.-tuple T for [distrLatticeType of n.-tuplelexi T]]. +Canonical tlexi_bDistrLatticeType n (T : finOrderType disp) := + [bDistrLatticeType of n.-tuple T for [bDistrLatticeType of n.-tuplelexi T]]. +Canonical tlexi_tbDistrLatticeType n (T : finOrderType disp) := + [tbDistrLatticeType of n.-tuple T for [tbDistrLatticeType of n.-tuplelexi T]]. Canonical tlexi_orderType n (T : orderType disp) := [orderType of n.-tuple T for [orderType of n.-tuplelexi T]]. Canonical tlexi_finPOrderType n (T : finPOrderType disp) := [finPOrderType of n.-tuple T]. -Canonical tlexi_finLatticeType n (T : finOrderType disp) := - [finLatticeType of n.-tuple T]. +Canonical tlexi_finDistrLatticeType n (T : finOrderType disp) := + [finDistrLatticeType of n.-tuple T]. Canonical tlexi_finOrderType n (T : finOrderType disp) := [finOrderType of n.-tuple T]. @@ -5677,11 +5748,11 @@ End DefaultTupleLexiOrder. Module Syntax. Export POSyntax. -Export LatticeSyntax. -Export BLatticeSyntax. -Export TBLatticeSyntax. -Export CBLatticeSyntax. -Export CTBLatticeSyntax. +Export DistrLatticeSyntax. +Export BDistrLatticeSyntax. +Export TBDistrLatticeSyntax. +Export CBDistrLatticeSyntax. +Export CTBDistrLatticeSyntax. Export TotalSyntax. Export ConverseSyntax. Export DvdSyntax. @@ -5692,16 +5763,16 @@ Export POCoercions. Export ConversePOrder. Export POrderTheory. -Export ConverseLattice. -Export LatticeTheoryMeet. -Export LatticeTheoryJoin. -Export BLatticeTheory. -Export ConverseTBLattice. -Export TBLatticeTheory. +Export ConverseDistrLattice. +Export DistrLatticeTheoryMeet. +Export DistrLatticeTheoryJoin. +Export BDistrLatticeTheory. +Export ConverseTBDistrLattice. +Export TBDistrLatticeTheory. End LTheory. Module CTheory. -Export LTheory CBLatticeTheory CTBLatticeTheory. +Export LTheory CBDistrLatticeTheory CTBDistrLatticeTheory. End CTheory. Module TTheory. @@ -5718,13 +5789,13 @@ Export Order.Syntax. Export Order.POrder.Exports. Export Order.FinPOrder.Exports. -Export Order.Lattice.Exports. -Export Order.BLattice.Exports. -Export Order.TBLattice.Exports. -Export Order.FinLattice.Exports. -Export Order.CBLattice.Exports. -Export Order.CTBLattice.Exports. -Export Order.FinCLattice.Exports. +Export Order.DistrLattice.Exports. +Export Order.BDistrLattice.Exports. +Export Order.TBDistrLattice.Exports. +Export Order.FinDistrLattice.Exports. +Export Order.CBDistrLattice.Exports. +Export Order.CTBDistrLattice.Exports. +Export Order.FinCDistrLattice.Exports. Export Order.Total.Exports. Export Order.FinTotal.Exports. |