diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/order.v | 47 |
1 files changed, 43 insertions, 4 deletions
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index 96cd9b9..8a7238e 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -2204,10 +2204,10 @@ Notation "x ><^d y" := (~~ (><^d%O x y)) : order_scope. Notation "x `&^d` y" := (@meet (dual_display _) _ x y) : order_scope. Notation "x `|^d` y" := (@join (dual_display _) _ x y) : order_scope. -Local Notation "0" := bottom. -Local Notation "1" := top. -Local Notation join := (@join (dual_display _) _). -Local Notation meet := (@meet (dual_display _) _). +Notation dual_bottom := (@bottom (dual_display _)). +Notation dual_top := (@top (dual_display _)). +Notation dual_join := (@join (dual_display _) _). +Notation dual_meet := (@meet (dual_display _) _). Notation "\join^d_ ( i <- r | P ) F" := (\big[join/0]_(i <- r | P%B) F%O) : order_scope. @@ -2604,6 +2604,8 @@ Module Import DualPOrder. Section DualPOrder. Canonical dual_eqType (T : eqType) := EqType T [eqMixin of T^d]. Canonical dual_choiceType (T : choiceType) := [choiceType of T^d]. +Canonical dual_countType (T : countType) := [countType of T^d]. +Canonical dual_finType (T : finType) := [finType of T^d]. Context {disp : unit}. Local Notation porderType := (porderType disp). @@ -2625,7 +2627,14 @@ Definition dual_porderMixin := Canonical dual_porderType := POrderType (dual_display disp) (T^d) dual_porderMixin. +Lemma leEdual (x y : T) : (x <=^d y :> T^d) = (y <= x). Proof. by []. Qed. +Lemma ltEdual (x y : T) : (x <^d y :> T^d) = (y < x). Proof. by []. Qed. + End DualPOrder. + +Canonical dual_finPOrderType d (T : finPOrderType d) := + [finPOrderType of T^d]. + End DualPOrder. Module Import DualDistrLattice. @@ -2681,6 +2690,10 @@ Definition dual_distrLatticeMixin := joinA meetA meetKU joinKI dual_leEmeet joinIl. Canonical dual_distrLatticeType := DistrLatticeType L^d dual_distrLatticeMixin. + +Lemma meetEdual x y : ((x : L^d) `&^d` y) = (x `|` y). Proof. by []. Qed. +Lemma joinEdual x y : ((x : L^d) `|^d` y) = (x `&` y). Proof. by []. Qed. + End DualDistrLattice. End DualDistrLattice. @@ -3166,7 +3179,14 @@ Definition dual_tbDistrLatticeMixin := Canonical dual_tbDIstrLatticeType := TBDistrLatticeType L^d dual_tbDistrLatticeMixin. +Lemma botEdual : (dual_bottom : L^d) = 1 :> L. Proof. by []. Qed. +Lemma topEdual : (dual_top : L^d) = 0 :> L. Proof. by []. Qed. + End DualTBDistrLattice. + +Canonical dual_finDistrLatticeType d (T : finDistrLatticeType d) := + [finDistrLatticeType of T^d]. + End DualTBDistrLattice. Module Import TBDistrLatticeTheory. @@ -5975,6 +5995,24 @@ Canonical tlexi_finOrderType n (T : finOrderType disp) := End DefaultTupleLexiOrder. End DefaultTupleLexiOrder. +Module Import DualOrder. +Section DualOrder. +Context {disp : unit}. +Local Notation orderType := (orderType disp). + +Variable O : orderType. + +Lemma dual_totalMixin : totalOrderMixin [distrLatticeType of O^d]. +Proof. by move=> x y; rewrite le_total. Qed. +Canonical dual_orderType := OrderType O^d dual_totalMixin. + +End DualOrder. + +Canonical dual_finOrderType d (T : finOrderType d) := + [finOrderType of T^d]. + +End DualOrder. + Module Syntax. Export POSyntax. Export DistrLatticeSyntax. @@ -5998,6 +6036,7 @@ Export DistrLatticeTheoryJoin. Export BDistrLatticeTheory. Export DualTBDistrLattice. Export TBDistrLatticeTheory. +Export DualOrder. End LTheory. Module CTheory. |