Change definition of IsStrictTotalOrder (#2137)

Author: MatthewDaggitt

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

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

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 _ _ _

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
   }
 
 ------------------------------------------------------------------------

src/Data/Integer/Properties.agda

@@ -331,9 +331,8 @@ _<?_ : Decidable _<_
 
 <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
 <-isStrictTotalOrder = record
-  { isEquivalence = isEquivalence
-  ; trans         = <-trans
-  ; compare       = <-cmp
+  { isStrictPartialOrder = <-isStrictPartialOrder
+  ; compare              = <-cmp
   }
 
 ------------------------------------------------------------------------

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 ℓ₁ ℓ₂ →

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
   }
 
 ------------------------------------------------------------------------

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

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₂)
       }

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 _≡_ _<_