Merge pull request #547 from pi8027/qualified-dual-op

Qualify the dual_* notations with the Order module

2 files changed, 35 insertions, 34 deletions

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 8dd9383..07f4a85 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -22,16 +22,14 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 - in `finset.v`, new lemmas: `properC`, `properCr`, `properCl`
 - in `ssrnat.v`, new lemmas: `subn_minl`, `subn_maxl`
 
-### Changed
-
-- in ssrbool.v, use `Reserved Notation` for `[rel _ _ : _ | _]` to avoid warnings with coq-8.12
-- in `ssrAC.v`, fix `non-reversible-notation` warnings
-
 - Added a factory `distrLatticePOrderMixin` in order.v to build a
   `distrLatticeType` from a `porderType`.
 
 ### Changed
 
+- in ssrbool.v, use `Reserved Notation` for `[rel _ _ : _ | _]` to avoid warnings with coq-8.12
+- in `ssrAC.v`, fix `non-reversible-notation` warnings
+
 - In the definition of structures in order.v, displays are removed from
   parameters of mixins and fields of classes internally and now only appear in
   parameters of structures. Consequently, each mixin is now parameterized by a
@@ -41,6 +39,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
   and `tbLatticeMixin` have been renamed to `bottomMixin` and `topMixin`
   respectively.
 
+- The `dual_*` notations such as `dual_le` in order.v are now qualified with the
+  `Order` module.
+
 ### Renamed
 
 ### Removed
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index adfcf57..cd54fd3 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -2484,22 +2484,33 @@ Export FinTotal.Exports.
 Definition dual T : Type := T.
 Definition dual_display : unit -> unit. Proof. exact. Qed.
 
+Notation dual_le := (@le (dual_display _) _).
+Notation dual_lt := (@lt (dual_display _) _).
+Notation dual_comparable := (@comparable (dual_display _) _).
+Notation dual_ge := (@ge (dual_display _) _).
+Notation dual_gt := (@gt (dual_display _) _).
+Notation dual_leif := (@leif (dual_display _) _).
+Notation dual_max := (@max (dual_display _) _).
+Notation dual_min := (@min (dual_display _) _).
+Notation dual_meet := (@meet (dual_display _) _).
+Notation dual_join := (@join (dual_display _) _).
+Notation dual_bottom := (@bottom (dual_display _) _).
+Notation dual_top := (@top (dual_display _) _).
+
 Module Import DualSyntax.
 
 Notation "T ^d" := (dual T) (at level 2, format "T ^d") : type_scope.
-Notation "<=^d%O" := (@le (dual_display _) _) : fun_scope.
-Notation ">=^d%O" := (@ge (dual_display _) _)  : fun_scope.
-Notation ">=^d%O" := (@ge (dual_display _) _)  : fun_scope.
-Notation "<^d%O" := (@lt (dual_display _) _) : fun_scope.
-Notation ">^d%O" := (@gt (dual_display _) _) : fun_scope.
-Notation "<?=^d%O" := (@leif (dual_display _) _) : fun_scope.
-Notation ">=<^d%O" := (@comparable (dual_display _) _) : fun_scope.
-Notation "><^d%O" := (fun x y => ~~ (@comparable (dual_display _) _ x y)) :
-  fun_scope.
+Notation "<=^d%O" := dual_le : fun_scope.
+Notation ">=^d%O" := dual_ge : fun_scope.
+Notation "<^d%O" := dual_lt : fun_scope.
+Notation ">^d%O" := dual_gt : fun_scope.
+Notation "<?=^d%O" := dual_leif : fun_scope.
+Notation ">=<^d%O" := dual_comparable : fun_scope.
+Notation "><^d%O" := (fun x y => ~~ dual_comparable x y) : fun_scope.
 
 Notation "<=^d y" := (>=^d%O y) : order_scope.
 Notation "<=^d y :> T" := (<=^d (y : T)) (only parsing) : order_scope.
-Notation ">=^d y"  := (<=^d%O y) : order_scope.
+Notation ">=^d y" := (<=^d%O y) : order_scope.
 Notation ">=^d y :> T" := (>=^d (y : T)) (only parsing) : order_scope.
 
 Notation "<^d y" := (>^d%O y) : order_scope.
@@ -2515,9 +2526,9 @@ Notation "x <=^d y :> T" := ((x : T) <=^d (y : T)) (only parsing) : order_scope.
 Notation "x >=^d y" := (y <=^d x) (only parsing) : order_scope.
 Notation "x >=^d y :> T" := ((x : T) >=^d (y : T)) (only parsing) : order_scope.
 
-Notation "x <^d y"  := (<^d%O x y) : order_scope.
+Notation "x <^d y" := (<^d%O x y) : order_scope.
 Notation "x <^d y :> T" := ((x : T) <^d (y : T)) (only parsing) : order_scope.
-Notation "x >^d y"  := (y <^d x) (only parsing) : order_scope.
+Notation "x >^d y" := (y <^d x) (only parsing) : order_scope.
 Notation "x >^d y :> T" := ((x : T) >^d (y : T)) (only parsing) : order_scope.
 
 Notation "x <=^d y <=^d z" := ((x <=^d y) && (y <=^d z)) : order_scope.
@@ -2537,15 +2548,8 @@ Notation "><^d x" := (fun y => ~~ (>=<^d%O x y)) : order_scope.
 Notation "><^d x :> T" := (><^d (x : T)) (only parsing) : order_scope.
 Notation "x ><^d y" := (~~ (><^d%O x y)) : order_scope.
 
-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 dual_max := (@max (dual_display _) _).
-Notation dual_min := (@min (dual_display _) _).
-
-Notation "x `&^d` y" :=  (@meet (dual_display _) _ x y) : order_scope.
-Notation "x `|^d` y" := (@join (dual_display _) _ x y) : order_scope.
+Notation "x `&^d` y" := (dual_meet x y) : order_scope.
+Notation "x `|^d` y" := (dual_join x y) : order_scope.
 
 Notation "\join^d_ ( i <- r | P ) F" :=
   (\big[join/0]_(i <- r | P%B) F%O) : order_scope.
@@ -3228,19 +3232,15 @@ Canonical dual_finType (T : finType) := [finType of T^d].
 Context {disp : unit}.
 Variable T : porderType disp.
 
-Definition dual_le (x y : T) := (y <= x).
-Definition dual_lt (x y : T) := (y < x).
-
-Lemma dual_lt_def (x y : T) :
-  dual_lt x y = (y != x) && (dual_le x y).
+Lemma dual_lt_def (x y : T) : gt x y = (y != x) && ge x y.
 Proof. by apply: lt_neqAle. Qed.
 
-Fact dual_le_anti : antisymmetric dual_le.
+Fact dual_le_anti : antisymmetric (@ge _ T).
 Proof. by move=> x y /andP [xy yx]; apply/le_anti/andP; split. Qed.
 
 Definition dual_porderMixin :=
-  POrder.Mixin dual_lt_def (lexx : reflexive dual_le) dual_le_anti
-               (fun y z x zy yx => @le_trans _ _ y x z yx zy).
+  @POrder.Mixin _ _ ge gt dual_lt_def (lexx : reflexive ge) dual_le_anti
+                (fun y z x zy yx => @le_trans _ _ y x z yx zy).
 Canonical dual_porderType :=
   POrderType (dual_display disp) T^d dual_porderMixin.