diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/order.v | 125 |
1 files changed, 59 insertions, 66 deletions
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index 385a9aa..5c8f251 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -298,10 +298,11 @@ From mathcomp Require Import path fintype tuple bigop finset div prime. (* - 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. *) +(* NB: the above three mixins are kept separate from each other (even *) +(* though they are convertible), in order to avoid ambiguous coercion *) +(* paths. *) (* *) -(* - distrLatticeMixin == on a porderType T, takes meet, join *) +(* - distrLatticeMixin == on a latticeType T, takes meet, join *) (* commutativity and associativity of meet and join *) (* idempotence of meet and some De Morgan laws *) (* (can build: distrLatticeType) *) @@ -320,37 +321,51 @@ From mathcomp Require Import path fintype tuple bigop finset div prime. (* - IsoLatticeMixin creates a distrLatticeMixin from an ordered structure *) (* isomorphism (i.e., cancel f f', cancel f' f, {mono f : x y / x <= y}) *) (* *) +(* List of "big pack" notations: *) +(* - DistrLatticeOfChoiceType builds a distrLatticeType from a choiceType and *) +(* a meetJoinMixin. *) +(* - OrderOfChoiceType builds an orderType from a choiceType, and a *) +(* leOrderMixin or a ltOrderMixin. *) +(* - OrderOfPOrder builds an orderType from a porderType and a *) +(* totalPOrderMixin. *) +(* - OrderOfLattice builds an orderType from a latticeType and a *) +(* totalLatticeMixin. *) +(* NB: These big pack notations should be used only to construct instances on *) +(* the fly, e.g., in the middle of a proof, and should not be used to *) +(* declare canonical instances. See field/algebraics_fundamentals.v for *) +(* an example usage. *) +(* *) (* We provide the following canonical instances of ordered types *) (* - all possible structures on bool *) -(* - porderType, distrLatticeType, orderType and bDistrLatticeType on nat for *) -(* the leq order *) -(* - porderType, distrLatticeType, bDistrLatticeType, cbDistrLatticeType, *) -(* ctbDistrLatticeType on nat for the dvdn order, where meet and join *) -(* are respectively gcdn and lcmn *) -(* - porderType, distrLatticeType, orderType, bDistrLatticeType, *) +(* - porderType, latticeType, distrLatticeType, orderType and *) +(* bDistrLatticeType on nat for the leq order *) +(* - porderType, latticeType, distrLatticeType, bDistrLatticeType, *) +(* cbDistrLatticeType, ctbDistrLatticeType on nat for the dvdn order, where *) +(* meet and join are respectively gcdn and lcmn *) +(* - porderType, latticeType, 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, distrLatticeType, and orderType, on T *lexi[disp] T' *) -(* another "copy" of T * T', with lexicographic ordering *) +(* - porderType, latticeType, distrLatticeType, and orderType, on *) +(* T *lexi[disp] T' another "copy" of T * T', with lexicographic ordering *) (* (and T *l T' its specialization to lexi_display) *) -(* - porderType, distrLatticeType, and orderType, on {t : T & T' x} *) -(* with lexicographic ordering *) -(* - porderType, distrLatticeType, orderType, bDistrLatticeType, *) +(* - porderType, latticeType, distrLatticeType, and orderType, on *) +(* {t : T & T' x} with lexicographic ordering *) +(* - porderType, latticeType, 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, 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, distrLatticeType, orderType, bDistrLatticeType, *) +(* - porderType, latticeType, distrLatticeType, and orderType, on *) +(* seqlexi_with disp T another "copy" of seq T, with lexicographic *) +(* ordering (and seqlexi T its specialization to lexi_display) *) +(* - porderType, latticeType, distrLatticeType, orderType, 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, distrLatticeType, and orderType, on n.-tuplelexi[d] T *) -(* another "copy" of n.-tuple T, with lexicographic ordering *) -(* (and n.-tuplelexi T its specialization to lexi_display) *) +(* - porderType, latticeType, distrLatticeType, 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 *) (* *) (* In order to get a canonical order on prod or seq, one may import modules *) @@ -4269,7 +4284,7 @@ Notation leOrderMixin := of_. Notation LeOrderMixin := Build. Coercion distrLatticeMixin : leOrderMixin >-> meetJoinMixin. Coercion totalMixin : leOrderMixin >-> totalOrderMixin. -Definition LeOrderOfChoiceType disp (T : choiceType) (m : of_ T) := +Definition OrderOfChoiceType disp (T : choiceType) (m : of_ T) := OrderType (DistrLatticeOfChoiceType disp m) m. End Exports. @@ -4296,62 +4311,40 @@ Record of_ := Build { Variables (m : of_). -Let T_total_porderType : porderType tt := - POrderType tt T (LtPOrderMixin (le_def m) (lt_irr m) (@lt_trans m)). +Fact lt_def x y : lt m x y = (y != x) && le m x y. +Proof. by rewrite le_def; case: eqVneq => //= ->; rewrite lt_irr. Qed. -Fact le_total : totalPOrderMixin T_total_porderType. -Proof. -by move=> x y; rewrite /<=%O /= !le_def; case: eqVneq; last exact: lt_total. -Qed. +Fact meet_def_le x y : meet m x y = if le m x y then x else y. +Proof. by rewrite meet_def le_def; case: eqP => //= ->; rewrite lt_irr. Qed. -Let T_orderType := OrderOfPOrder le_total. +Fact join_def_le x y : join m x y = if le m y x then x else y. +Proof. by rewrite join_def le_def; case: eqP => //= ->; rewrite lt_irr. Qed. -Implicit Types (x y z : T_orderType). - -Fact leP x y : - lel_xor_gt x y (x <= y) (y < x) (y `&` x) (x `&` y) (y `|` x) (x `|` y). -Proof. by apply/lcomparable_leP/le_total. Qed. -Fact meetE x y : meet m x y = x `&` y. -Proof. by rewrite meet_def (_ : lt m x y = (x < y)) //; case: (leP y). Qed. -Fact joinE x y : join m x y = x `|` y. -Proof. by rewrite join_def (_ : lt m y x = (y < x)) //; case: leP. Qed. -Fact meetC : commutative (meet m). -Proof. by move=> *; rewrite !meetE meetC. Qed. -Fact joinC : commutative (join m). -Proof. by move=> *; rewrite !joinE joinC. Qed. -Fact meetA : associative (meet m). -Proof. by move=> *; rewrite !meetE meetA. Qed. -Fact joinA : associative (join m). -Proof. by move=> *; rewrite !joinE joinA. Qed. -Fact joinKI y x : meet m x (join m x y) = x. -Proof. by rewrite meetE joinE joinKI. Qed. -Fact meetKU y x : join m x (meet m x y) = x. -Proof. by rewrite meetE joinE meetKU. Qed. -Fact meetUl : left_distributive (meet m) (join m). -Proof. by move=> *; rewrite !meetE !joinE meetUl. Qed. -Fact meetxx : idempotent (meet m). -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. +Fact le_anti : antisymmetric (le m). +Proof. +move=> x y; rewrite !le_def; case: eqVneq => //= _ /andP [] hxy. +by move/(lt_trans hxy); rewrite lt_irr. +Qed. -Definition distrLatticeMixin : meetJoinMixin T := - @MeetJoinMixin _ (le m) (lt m) (meet m) (join m) - le_def' (@lt_def _ T_orderType) - meetC joinC meetA joinA joinKI meetKU meetUl meetxx. +Fact le_trans : transitive (le m). +Proof. +move=> y x z; rewrite !le_def; case: eqVneq => [->|_] //=. +by case: eqVneq => [-> ->|_ hxy /(lt_trans hxy) ->]; rewrite orbT. +Qed. -Let T_distrLatticeType := DistrLatticeOfChoiceType tt distrLatticeMixin. +Fact le_total : total (le m). +Proof. by move=> x y; rewrite !le_def; case: eqVneq => //; exact: lt_total. Qed. -Definition totalMixin : totalOrderMixin T_distrLatticeType := le_total. +Definition orderMixin : leOrderMixin T := + @LeOrderMixin _ (le m) (lt m) (meet m) (join m) + lt_def meet_def_le join_def_le le_anti le_trans le_total. End LtOrderMixin. Module Exports. Notation ltOrderMixin := of_. Notation LtOrderMixin := Build. -Coercion distrLatticeMixin : ltOrderMixin >-> meetJoinMixin. -Coercion totalMixin : ltOrderMixin >-> totalOrderMixin. -Definition LtOrderOfChoiceType disp (T : choiceType) (m : of_ T) := - OrderType (DistrLatticeOfChoiceType disp m) m. +Coercion orderMixin : ltOrderMixin >-> leOrderMixin. End Exports. End LtOrderMixin. |