Change definition of IsStrictTotalOrder (#2137)

MatthewDaggitt · web-flow · commit 7f64664c8725 · 2023-10-13T18:22:01.000+09:00
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -918,6 +918,46 @@ Non-backwards compatible changes
 
 * The old names (and the names of all proofs about these functions) have been deprecated appropriately.
 
+### Changes to definition of `IsStrictTotalOrder`
+
+* The previous definition of the record `IsStrictTotalOrder` did not build upon `IsStrictPartialOrder`
+  as would be expected. Instead it omitted several fields like irreflexivity as they were derivable from the
+  proof of trichotomy. However, this led to problems further up the hierarchy where bundles such as `StrictTotalOrder`
+  which contained multiple distinct proofs of `IsStrictPartialOrder`.
+  
+* To remedy this the definition of `IsStrictTotalOrder` has been changed to so that it builds upon 
+  `IsStrictPartialOrder` as would be expected. 
+
+* To aid migration, the old record definition has been moved to `Relation.Binary.Structures.Biased`
+  which contains the `isStrictTotalOrderᶜ` smart constructor (which is re-exported by `Relation.Binary`) . 
+  Therefore the old code:
+  ```agda
+  <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
+  <-isStrictTotalOrder = record
+	{ isEquivalence = isEquivalence
+	; trans         = <-trans
+	; compare       = <-cmp
+	}
+  ```
+  can be migrated either by updating to the new record fields if you have a proof of `IsStrictPartialOrder`
+  available:
+  ```agda
+  <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
+  <-isStrictTotalOrder = record
+	{ isStrictPartialOrder = <-isStrictPartialOrder
+	; compare              = <-cmp
+	}
+  ```
+  or simply applying the smart constructor to the record definition as follows:
+  ```agda
+  <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
+  <-isStrictTotalOrder = isStrictTotalOrderᶜ record
+	{ isEquivalence = isEquivalence
+	; trans         = <-trans
+	; compare       = <-cmp
+	}
+  ```
+  
 ### Changes to triple reasoning interface
 
 * The module `Relation.Binary.Reasoning.Base.Triple` now takes an extra proof that the strict
diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda
@@ -210,9 +210,8 @@ true  <? _     = no  (λ())
 
 <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
 <-isStrictTotalOrder = record
-  { isEquivalence = isEquivalence
-  ; trans         = <-trans
-  ; compare       = <-cmp
+  { isStrictPartialOrder = <-isStrictPartialOrder
+  ; compare              = <-cmp
   }
 
 -- Bundles
diff --git a/src/Data/Char/Properties.agda b/src/Data/Char/Properties.agda
@@ -123,9 +123,8 @@ _<?_ = On.decidable toℕ ℕ._<_ ℕₚ._<?_
 
 <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
 <-isStrictTotalOrder = record
-  { isEquivalence = PropEq.isEquivalence
-  ; trans         = λ {a} {b} {c} → <-trans {a} {b} {c}
-  ; compare       = <-cmp
+  { isStrictPartialOrder = <-isStrictPartialOrder
+  ; compare              = <-cmp
   }
 
 <-strictPartialOrder : StrictPartialOrder _ _ _
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
@@ -406,9 +406,8 @@ m <? n = suc (toℕ m) ℕₚ.≤? toℕ n
 
 <-isStrictTotalOrder : IsStrictTotalOrder {A = Fin n} _≡_ _<_
 <-isStrictTotalOrder = record
-  { isEquivalence = P.isEquivalence
-  ; trans         = <-trans
-  ; compare       = <-cmp
+  { isStrictPartialOrder = <-isStrictPartialOrder
+  ; compare              = <-cmp
   }
 
 ------------------------------------------------------------------------
diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda
@@ -331,9 +331,8 @@ _<?_ : Decidable _<_
 
 <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
 <-isStrictTotalOrder = record
-  { isEquivalence = isEquivalence
-  ; trans         = <-trans
-  ; compare       = <-cmp
+  { isStrictPartialOrder = <-isStrictPartialOrder
+  ; compare              = <-cmp
   }
 
 ------------------------------------------------------------------------
diff --git a/src/Data/List/Relation/Binary/Lex/Strict.agda b/src/Data/List/Relation/Binary/Lex/Strict.agda
@@ -121,9 +121,8 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where
     <-isStrictTotalOrder : IsStrictTotalOrder _≈_ _≺_ →
                            IsStrictTotalOrder _≋_ _<_
     <-isStrictTotalOrder sto = record
-      { isEquivalence = Pointwise.isEquivalence isEquivalence
-      ; trans         = <-transitive isEquivalence <-resp-≈ trans
-      ; compare       = <-compare Eq.sym compare
+      { isStrictPartialOrder = <-isStrictPartialOrder isStrictPartialOrder
+      ; compare              = <-compare Eq.sym compare
       } where open IsStrictTotalOrder sto
 
 <-strictPartialOrder : ∀ {a ℓ₁ ℓ₂} → StrictPartialOrder a ℓ₁ ℓ₂ →
diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda
@@ -414,9 +414,8 @@ _<?_ = tri⇒dec< <-cmp
 
 <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
 <-isStrictTotalOrder = record
-  { isEquivalence = isEquivalence
-  ; trans         = <-trans
-  ; compare       = <-cmp
+  { isStrictPartialOrder = <-isStrictPartialOrder
+  ; compare              = <-cmp
   }
 
 ------------------------------------------------------------------------
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
@@ -32,12 +32,7 @@ open import Level using (0ℓ)
 open import Relation.Unary as U using (Pred)
 open import Relation.Binary.Core
   using (_⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
-open import Relation.Binary.Bundles
-  using (DecSetoid; Preorder; TotalPreorder; Poset; TotalOrder; DecTotalOrder; StrictPartialOrder; StrictTotalOrder)
-open import Relation.Binary.Structures
-  using (IsDecEquivalence; IsPreorder; IsTotalPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder)
-open import Relation.Binary.Definitions
-  using (DecidableEquality; Irrelevant; Reflexive; Antisymmetric; Transitive; Total; Decidable; Connex; Irreflexive; Asymmetric; LeftTrans; RightTrans; Trichotomous; tri≈; tri>; tri<; _Respects₂_)
+open import Relation.Binary
 open import Relation.Binary.Consequences using (flip-Connex)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary hiding (Irrelevant)
@@ -402,7 +397,7 @@ _>?_ = flip _<?_
   }
 
 <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
-<-isStrictTotalOrder = record
+<-isStrictTotalOrder = isStrictTotalOrderᶜ record
   { isEquivalence = isEquivalence
   ; trans         = <-trans
   ; compare       = <-cmp
diff --git a/src/Data/Product/Relation/Binary/Lex/Strict.agda b/src/Data/Product/Relation/Binary/Lex/Strict.agda
@@ -269,12 +269,9 @@ module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂}
                          IsStrictTotalOrder _≋_ _<ₗₑₓ_
   ×-isStrictTotalOrder spo₁ spo₂ =
     record
-      { isEquivalence = Pointwise.×-isEquivalence
-                          (isEquivalence spo₁) (isEquivalence spo₂)
-      ; trans         = ×-transitive {_<₁_ = _<₁_} {_<₂_ = _<₂_}
-                          (isEquivalence spo₁)
-                          (<-resp-≈ spo₁) (trans spo₁)
-                          (trans spo₂)
+      { isStrictPartialOrder = ×-isStrictPartialOrder
+                                 (isStrictPartialOrder spo₁)
+                                 (isStrictPartialOrder spo₂)
       ; compare       = ×-compare (Eq.sym spo₁) (compare spo₁)
                                                 (compare spo₂)
       }
diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
@@ -702,9 +702,8 @@ _>?_ = flip _<?_
 
 <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
 <-isStrictTotalOrder = record
-  { isEquivalence = isEquivalence
-  ; trans         = <-trans
-  ; compare       = <-cmp
+  { isStrictPartialOrder = <-isStrictPartialOrder
+  ; compare              = <-cmp
   }
 
 <-isDenseLinearOrder : IsDenseLinearOrder _≡_ _<_
diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda
@@ -542,9 +542,8 @@ _>?_ = flip _<?_
 
 <-isStrictTotalOrder : IsStrictTotalOrder _≃_ _<_
 <-isStrictTotalOrder = record
-  { isEquivalence = ≃-isEquivalence
-  ; trans         = <-trans
-  ; compare       = <-cmp
+  { isStrictPartialOrder = <-isStrictPartialOrder
+  ; compare              = <-cmp
   }
 
 <-isDenseLinearOrder : IsDenseLinearOrder _≃_ _<_
diff --git a/src/Data/Sum/Relation/Binary/LeftOrder.agda b/src/Data/Sum/Relation/Binary/LeftOrder.agda
@@ -192,9 +192,8 @@ module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂}
                            IsStrictTotalOrder ≈₂ ∼₂ →
                            IsStrictTotalOrder (Pointwise ≈₁ ≈₂) (∼₁ ⊎-< ∼₂)
   ⊎-<-isStrictTotalOrder sto₁ sto₂ = record
-    { isEquivalence = PW.⊎-isEquivalence (isEquivalence sto₁) (isEquivalence sto₂)
-    ; trans         = ⊎-<-transitive (trans sto₁) (trans sto₂)
-    ; compare       = ⊎-<-trichotomous (compare sto₁) (compare sto₂)
+    { isStrictPartialOrder = ⊎-<-isStrictPartialOrder (isStrictPartialOrder sto₁) (isStrictPartialOrder sto₂)
+    ; compare              = ⊎-<-trichotomous (compare sto₁) (compare sto₂)
     }
     where open IsStrictTotalOrder
 
diff --git a/src/Data/Vec/Relation/Binary/Lex/Strict.agda b/src/Data/Vec/Relation/Binary/Lex/Strict.agda
@@ -168,8 +168,7 @@ module _ {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
   <-isStrictTotalOrder : IsStrictTotalOrder _≈_ _≺_ →
                          ∀ {n} → IsStrictTotalOrder (_≋_ {n} {n}) _<_
   <-isStrictTotalOrder ≺-isStrictTotalOrder {n} = record
-    { isEquivalence = Pointwise.isEquivalence O.isEquivalence n
-    ; trans         = <-trans O.Eq.isPartialEquivalence O.<-resp-≈ O.trans
+    { isStrictPartialOrder = <-isStrictPartialOrder O.isStrictPartialOrder
     ; compare       = <-cmp O.Eq.sym O.compare
     } where module O = IsStrictTotalOrder ≺-isStrictTotalOrder
 
diff --git a/src/Induction/WellFounded.agda b/src/Induction/WellFounded.agda
@@ -14,7 +14,7 @@ open import Induction
 open import Level using (Level; _⊔_)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions
-  using (Symmetric; Asymmetric; Irreflexive; _Respects₂_; 
+  using (Symmetric; Asymmetric; Irreflexive; _Respects₂_;
     _Respectsʳ_; _Respects_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Relation.Binary.Consequences using (asym⇒irr)
@@ -130,7 +130,7 @@ module _ {_<_ : Rel A r} where
   wf⇒asym : WellFounded _<_ → Asymmetric _<_
   wf⇒asym wf = acc⇒asym (wf _)
 
-  wf⇒irrefl : {_≈_ : Rel A ℓ} → _<_ Respects₂ _≈_ → 
+  wf⇒irrefl : {_≈_ : Rel A ℓ} → _<_ Respects₂ _≈_ →
               Symmetric _≈_ → WellFounded _<_ → Irreflexive _≈_ _<_
   wf⇒irrefl r s wf = asym⇒irr r s (wf⇒asym wf)
 
diff --git a/src/Relation/Binary.agda b/src/Relation/Binary.agda
@@ -14,4 +14,5 @@ module Relation.Binary where
 open import Relation.Binary.Core public
 open import Relation.Binary.Definitions public
 open import Relation.Binary.Structures public
+open import Relation.Binary.Structures.Biased public
 open import Relation.Binary.Bundles public
diff --git a/src/Relation/Binary/Bundles.agda b/src/Relation/Binary/Bundles.agda
@@ -100,7 +100,7 @@ record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   _≳_ = flip _≲_
 
   -- Deprecated.
-  infix 4 _∼_ 
+  infix 4 _∼_
   _∼_ = _≲_
   {-# WARNING_ON_USAGE _∼_
   "Warning: _∼_ was deprecated in v2.0.
diff --git a/src/Relation/Binary/Construct/Add/Infimum/Strict.agda b/src/Relation/Binary/Construct/Add/Infimum/Strict.agda
@@ -153,9 +153,8 @@ module _ {e} {_≈_ : Rel A e} where
 <₋-isStrictTotalOrder-≡ : IsStrictTotalOrder _≡_ _<_ →
                           IsStrictTotalOrder _≡_ _<₋_
 <₋-isStrictTotalOrder-≡ strictot = record
-  { isEquivalence = P.isEquivalence
-  ; trans         = <₋-trans trans
-  ; compare       = <₋-cmp-≡ compare
+  { isStrictPartialOrder = <₋-isStrictPartialOrder-≡ isStrictPartialOrder
+  ; compare              = <₋-cmp-≡ compare
   } where open IsStrictTotalOrder strictot
 
 ------------------------------------------------------------------------
@@ -185,7 +184,6 @@ module _ {e} {_≈_ : Rel A e} where
   <₋-isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_ →
                           IsStrictTotalOrder _≈₋_ _<₋_
   <₋-isStrictTotalOrder strictot = record
-    { isEquivalence = ≈₋-isEquivalence isEquivalence
-    ; trans         = <₋-trans trans
-    ; compare       = <₋-cmp compare
+    { isStrictPartialOrder = <₋-isStrictPartialOrder isStrictPartialOrder
+    ; compare              = <₋-cmp compare
     } where open IsStrictTotalOrder strictot
diff --git a/src/Relation/Binary/Construct/Add/Supremum/Strict.agda b/src/Relation/Binary/Construct/Add/Supremum/Strict.agda
@@ -154,9 +154,8 @@ module _ {e} {_≈_ : Rel A e} where
 <⁺-isStrictTotalOrder-≡ : IsStrictTotalOrder _≡_ _<_ →
                           IsStrictTotalOrder _≡_ _<⁺_
 <⁺-isStrictTotalOrder-≡ strictot = record
-  { isEquivalence = P.isEquivalence
-  ; trans         = <⁺-trans trans
-  ; compare       = <⁺-cmp-≡ compare
+  { isStrictPartialOrder = <⁺-isStrictPartialOrder-≡ isStrictPartialOrder
+  ; compare              = <⁺-cmp-≡ compare
   } where open IsStrictTotalOrder strictot
 
 ------------------------------------------------------------------------
@@ -186,7 +185,6 @@ module _ {e} {_≈_ : Rel A e} where
   <⁺-isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_ →
                           IsStrictTotalOrder _≈⁺_ _<⁺_
   <⁺-isStrictTotalOrder strictot = record
-    { isEquivalence = ≈⁺-isEquivalence isEquivalence
-    ; trans         = <⁺-trans trans
-    ; compare       = <⁺-cmp compare
+    { isStrictPartialOrder = <⁺-isStrictPartialOrder isStrictPartialOrder
+    ; compare              = <⁺-cmp compare
     } where open IsStrictTotalOrder strictot
diff --git a/src/Relation/Binary/Construct/Flip/EqAndOrd.agda b/src/Relation/Binary/Construct/Flip/EqAndOrd.agda
@@ -145,9 +145,8 @@ isStrictPartialOrder {< = <} O = record
 isStrictTotalOrder : IsStrictTotalOrder ≈ < →
                      IsStrictTotalOrder ≈ (flip <)
 isStrictTotalOrder {< = <} O = record
-  { isEquivalence = O.isEquivalence
-  ; trans         = trans < O.trans
-  ; compare       = compare _ O.compare
+  { isStrictPartialOrder = isStrictPartialOrder O.isStrictPartialOrder
+  ; compare              = compare _ O.compare
   } where module O = IsStrictTotalOrder O
 
 ------------------------------------------------------------------------
diff --git a/src/Relation/Binary/Construct/Flip/Ord.agda b/src/Relation/Binary/Construct/Flip/Ord.agda
@@ -139,9 +139,8 @@ isStrictPartialOrder {≈ = ≈} {< = <} O = record
 isStrictTotalOrder : IsStrictTotalOrder ≈ < →
                      IsStrictTotalOrder (flip ≈) (flip <)
 isStrictTotalOrder {≈ = ≈} {< = <} O = record
-  { isEquivalence = isEquivalence O.isEquivalence
-  ; trans         = transitive < O.trans
-  ; compare       = trichotomous ≈ < O.compare
+  { isStrictPartialOrder = isStrictPartialOrder O.isStrictPartialOrder
+  ; compare              = trichotomous ≈ < O.compare
   } where module O = IsStrictTotalOrder O
 
 ------------------------------------------------------------------------
diff --git a/src/Relation/Binary/Construct/NonStrictToStrict.agda b/src/Relation/Binary/Construct/NonStrictToStrict.agda
@@ -138,9 +138,8 @@ x < y = x ≤ y × x ≉ y
 <-isStrictTotalOrder₁ : Decidable _≈_ → IsTotalOrder _≈_ _≤_ →
                         IsStrictTotalOrder _≈_ _<_
 <-isStrictTotalOrder₁ ≟ tot = record
-  { isEquivalence = isEquivalence
-  ; trans         = <-trans isPartialOrder
-  ; compare       = <-trichotomous Eq.sym ≟ antisym total
+  { isStrictPartialOrder = <-isStrictPartialOrder isPartialOrder
+  ; compare              = <-trichotomous Eq.sym ≟ antisym total
   } where open IsTotalOrder tot
 
 <-isStrictTotalOrder₂ : IsDecTotalOrder _≈_ _≤_ →
diff --git a/src/Relation/Binary/Construct/On.agda b/src/Relation/Binary/Construct/On.agda
@@ -150,9 +150,8 @@ module _ (f : B → A) {≈ : Rel A ℓ₁} {∼ : Rel A ℓ₂} where
   isStrictTotalOrder : IsStrictTotalOrder ≈ ∼ →
                        IsStrictTotalOrder (≈ on f) (∼ on f)
   isStrictTotalOrder sto = record
-    { isEquivalence = isEquivalence f Sto.isEquivalence
-    ; trans         = transitive f ∼ Sto.trans
-    ; compare       = trichotomous f ≈ ∼ Sto.compare
+    { isStrictPartialOrder = isStrictPartialOrder Sto.isStrictPartialOrder
+    ; compare              = trichotomous _ _ _ Sto.compare
     } where module Sto = IsStrictTotalOrder sto
 
 ------------------------------------------------------------------------
diff --git a/src/Relation/Binary/Morphism/OrderMonomorphism.agda b/src/Relation/Binary/Morphism/OrderMonomorphism.agda
@@ -105,7 +105,6 @@ isStrictPartialOrder O = record
 isStrictTotalOrder : IsStrictTotalOrder _≈₂_ _≲₂_ →
                      IsStrictTotalOrder _≈₁_ _≲₁_
 isStrictTotalOrder O = record
-  { isEquivalence = EqM.isEquivalence O.isEquivalence
-  ; trans         = trans O.trans
-  ; compare       = compare O.compare
+  { isStrictPartialOrder = isStrictPartialOrder O.isStrictPartialOrder
+  ; compare              = compare O.compare
   } where module O = IsStrictTotalOrder O
diff --git a/src/Relation/Binary/Structures.agda b/src/Relation/Binary/Structures.agda
diff --git a/src/Relation/Binary/Structures/Biased.agda b/src/Relation/Binary/Structures/Biased.agda
