alternative type classes for order relations

src/Data/Nat/Properties/Ext.agda

@@ -2,7 +2,7 @@
 
 module Data.Nat.Properties.Ext where
 
-open import Data.Nat using (_<_)
+import Data.Nat as ℕ
 open import Data.Nat.Properties
 open import Ledger.Prelude
 open import Relation.Nullary.Decidable
@@ -17,14 +17,14 @@ negInduction {P = P} P? P0 (N , ¬PN)
 ... | yes (k , _ , h) = k , h
 ... | no ¬p           = contradiction (k≤N⇒Pk ≤-refl) ¬PN
   where
-    helper : ∀ {k} → k < N → P k → P k × P (suc k)
+    helper : ∀ {k} → k ℕ.< N → P k → P k × P (suc k)
     helper {k} k<N Pk =
       Pk , decidable-stable (P? _) (curry (curry (¬∃⟶∀¬ ¬p k) k<N) Pk)
 
-    k<N⇒P'k : ∀ {k} → k < N → P k × P (suc k)
+    k<N⇒P'k : ∀ {k} → k ℕ.< N → P k × P (suc k)
     k<N⇒P'k {zero}  k<N = helper k<N P0
     k<N⇒P'k {suc k} k<N = helper k<N (proj₂ $ k<N⇒P'k {k} (<⇒≤ k<N))
 
-    k≤N⇒Pk : ∀ {k} → k ≤ N → P k
+    k≤N⇒Pk : ∀ {k} → k ℕ.≤ N → P k
     k≤N⇒Pk {zero}  k≤N = P0
     k≤N⇒Pk {suc k} k≤N = proj₂ $ k<N⇒P'k k≤N

src/Interface/HasOrder.agda

@@ -2,31 +2,140 @@
 
 module Interface.HasOrder where
 
+open import Prelude hiding (_⊔_; suc; isPartialOrder; isEquivalence; trans)
 open import Level using (_⊔_; suc)
 open import Relation.Binary using (Rel)
-open import Relation.Binary.Definitions using (Decidable; Antisymmetric)
-open import Relation.Binary.Structures using (IsPreorder; IsPartialOrder)
+open import Relation.Binary.Definitions using (Decidable; Antisymmetric; Irreflexive; Asymmetric)
+open import Relation.Binary.Structures using (IsPreorder; IsPartialOrder; IsStrictPartialOrder)
+open import Relation.Binary.Structures using (IsDecTotalOrder ; IsStrictTotalOrder; IsTotalOrder)
 
-module _ {a ℓ ℓ₂} (A : Set a) (_≈_ : Rel A ℓ) where
+module _ {α ℓ} (A : Set α) (_≈_ : Rel A ℓ) where
 
-  record HasPreorder : Set (a ⊔ ℓ ⊔ suc ℓ₂) where
-    infix 4 _≤_
+  record HasPreorder : Set (α ⊔ suc ℓ) where
+    infix 4 _≤_ _<_
     field
-      _≤_    : Rel A ℓ₂
-      isPreorder : IsPreorder _≈_ _≤_
+      _≤_ _<_       : Rel A ℓ
+      ≤-isPreorder  : IsPreorder _≈_ _≤_
+      <-irrefl      : Irreflexive _≈_ _<_
+      ≤⇔<∨≈         : ∀ {a b} → a ≤ b ⇔ (a < b ⊎ a ≈ b)
 
-  record HasPartialOrder : Set (a ⊔ ℓ ⊔ suc ℓ₂) where
-    open HasPreorder
+  record HasPartialOrder : Set (α ⊔ suc ℓ) where
     field
       hasPreorder  : HasPreorder
-      antisym      : Antisymmetric _≈_ (_≤_ hasPreorder)
+      ≤-antisym    : Antisymmetric _≈_ (HasPreorder._≤_ hasPreorder)
 
-  record HasDecPartialOrder : Set (a ⊔ ℓ ⊔ suc ℓ₂) where
+    open HasPreorder hasPreorder public   -- HasPartialOrder should expose fields of HasPreorder
+
+    <⇒≤∧≠ : ∀{x y} → x < y → x ≤ y × ¬ (x ≈ y)
+    <⇒≤∧≠ {x}{y} x<y = (Equivalence.from ≤⇔<∨≈ (inj₁ x<y)) , λ x≈y → <-irrefl x≈y x<y
+
+    ≤-antisym⇒<-asym : Antisymmetric _≈_ _≤_ → Asymmetric _<_
+    ≤-antisym⇒<-asym antisym x<y y<x = proj₂ (<⇒≤∧≠ x<y) (antisym (proj₁ (<⇒≤∧≠ x<y)) (proj₁ (<⇒≤∧≠ y<x)))
+
+    <-asymmetric : Asymmetric _<_
+    <-asymmetric = ≤-antisym⇒<-asym ≤-antisym
+
+    <⇒¬>⊎≈ : ∀{x y} → x < y → ¬ (y < x ⊎ x ≈ y)
+    <⇒¬>⊎≈ x<y (inj₁ y<x) = <-asymmetric x<y y<x
+    <⇒¬>⊎≈ x<y (inj₂ x≈y) = <-irrefl x≈y x<y
+
+
+    ≤-isPartialOrder : IsPartialOrder _≈_ _≤_
+    ≤-isPartialOrder = record { isPreorder = ≤-isPreorder ; antisym = ≤-antisym }
+
+  record HasDecPartialOrder : Set (α ⊔ suc ℓ) where
     infix 4 _≤?_
     field
       hasPartialOrder : HasPartialOrder
-      _≤?_  : Decidable (HasPreorder._≤_ (HasPartialOrder.hasPreorder hasPartialOrder))
+    open HasPartialOrder hasPartialOrder
+    field
+      _≤?_ : Decidable _≤_
+
+-- conversions
+  -- strict to nonstrict
+  module _  (_<_ : Rel A ℓ) where                                      -- If we start with
+    module _ (<-isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_)   -- a strict partial order...
+      where
+      open import Relation.Binary.Construct.StrictToNonStrict _≈_ _<_
+
+      hasPreorderFromStrict : HasPreorder                               -- ...we have a preorder, including
+      hasPreorderFromStrict = record                                    -- a nonstrict ordering _≤_ and
+        { _≤_           = _≤_                                           -- a (trivial) proof of ≤⇔<∨≈.
+        ; _<_           = _<_
+        ; ≤-isPreorder  = isPreorder₂ <-isStrictPartialOrder            -- Note we don't need decidability of
+        ; <-irrefl      = irrefl <-isStrictPartialOrder                 -- _≈_ to go from strict to non-strict.
+        ; ≤⇔<∨≈         = mk⇔ id id
+        }
+        where open IsStrictPartialOrder
+
+
+    module _ (<-isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_)   -- a strict partial order...
+      where
+      open import Relation.Binary.Construct.StrictToNonStrict _≈_ _<_
+
+
+      <-STO⇒≤-isTotalOrder : IsTotalOrder _≈_ _≤_
+      <-STO⇒≤-isTotalOrder = isTotalOrder <-isStrictTotalOrder
+
+      <-STO⇒≤-isPartialOrder : IsPartialOrder _≈_ _≤_
+      <-STO⇒≤-isPartialOrder = IsTotalOrder.isPartialOrder <-STO⇒≤-isTotalOrder
+
+      <-STO⇒≤-isPreorder : IsPreorder _≈_ _≤_
+      <-STO⇒≤-isPreorder = IsPartialOrder.isPreorder (IsTotalOrder.isPartialOrder <-STO⇒≤-isTotalOrder)
+
+      <-STO⇒<-isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_
+      <-STO⇒<-isStrictPartialOrder = IsStrictTotalOrder.isStrictPartialOrder <-isStrictTotalOrder
+
+      hasPreorderFromStrictTotalOrder : HasPreorder
+      hasPreorderFromStrictTotalOrder = record                                    -- including a nonstrict ordering _≤_
+        { _≤_           = _≤_                                           -- and a (trivial) proof of ≤⇔<∨≈.
+        ; _<_           = _<_
+        ; ≤-isPreorder  = <-STO⇒≤-isPreorder
+        ; <-irrefl      = IsStrictTotalOrder.irrefl <-isStrictTotalOrder                 -- _≈_ to go from strict to non-strict.
+        ; ≤⇔<∨≈         = mk⇔ id id
+        }
+
+
+      <-STO⇒≤-antisym : Antisymmetric _≈_ _≤_                                  -- Note that the non-strict ordering
+      <-STO⇒≤-antisym = antisym  (isEquivalence <-STO⇒<-isStrictPartialOrder)  -- is necessarily antisymmetric,
+                                 (transEq <-STO⇒<-isStrictPartialOrder)        -- hence a partial ordering.
+                                 (<-irrefl hasPreorderFromStrictTotalOrder)
+        where
+        open IsStrictPartialOrder renaming (trans to transEq)
+        open HasPreorder using (<-irrefl)
+
+      hasPartialOrderFromStrictTotalOrder : HasPartialOrder
+      hasPartialOrderFromStrictTotalOrder = record
+        { hasPreorder = hasPreorderFromStrictTotalOrder
+        ; ≤-antisym = <-STO⇒≤-antisym }
+
+      <-STO⇒≤-isDecidable : IsDecTotalOrder _≈_ _≤_
+      <-STO⇒≤-isDecidable = isDecTotalOrder <-isStrictTotalOrder  --
+
+      hasDecPartialOrderFromStrictTotalOrder : HasDecPartialOrder
+      hasDecPartialOrderFromStrictTotalOrder = record
+        { hasPartialOrder = hasPartialOrderFromStrictTotalOrder
+        ; _≤?_ = IsDecTotalOrder._≤?_ <-STO⇒≤-isDecidable }
+
+  -- nonstrict to strict
+  module _  (_≤_ : Rel A ℓ)                        -- If we start with
+            (≤-isPreorder : IsPreorder _≈_ _≤_)    -- a non-strict preorder and
+            (_≈?_ : ∀ a b → Dec (a ≈ b))           -- a decidable equality...
+    where
+    open import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_
+
+    hasPreorderFromNonStrict : HasPreorder
+    hasPreorderFromNonStrict = record              -- including a strict ordering _<_
+      { _≤_           = _≤_                        -- and a proof of ≤⇔<∨≈.
+      ; _<_           = _<_
+      ; ≤-isPreorder  = ≤-isPreorder
+      ; <-irrefl      = <-irrefl
+      ; ≤⇔<∨≈         = λ {a b} → mk⇔
+        (λ a≤b → case (a ≈? b) of λ where (yes p) → inj₂ p ; (no ¬p) → inj₁ (a≤b , ¬p))
+        λ where (inj₁ a<b) → proj₁ a<b ; (inj₂ a≈b) → IsPreorder.reflexive ≤-isPreorder a≈b
+      }
+
 
 open HasPreorder ⦃...⦄ public
--- open HasPartialOrder ⦃...⦄ public
--- open HasDecPartialOrder ⦃...⦄ public
+open HasPartialOrder ⦃...⦄ public
+open HasDecPartialOrder ⦃...⦄ public

src/Interface/HasOrder/Instance.agda

@@ -12,19 +12,19 @@ import Data.Nat.Properties as NatProp
 
 instance
   preoInt : HasPreorder ℤ _≡_
-  preoInt = record { _≤_ = ℤ._≤_; isPreorder = IntProp.≤-isPreorder }
+  preoInt = hasPreorderFromNonStrict ℤ _≡_ ℤ._≤_ IntProp.≤-isPreorder IntProp._≟_
 
   leqInt : HasPartialOrder ℤ _≡_
-  leqInt = record { hasPreorder = preoInt; antisym = IntProp.≤-antisym }
+  leqInt = record { hasPreorder = preoInt ; ≤-antisym = IntProp.≤-antisym }
 
   DecLeqInt : HasDecPartialOrder ℤ _≡_
   DecLeqInt = record { hasPartialOrder = leqInt ; _≤?_ = ℤ._≤?_ }
 
   preoNat : HasPreorder ℕ _≡_
-  preoNat = record { _≤_ = ℕ._≤_; isPreorder = NatProp.≤-isPreorder }
+  preoNat = hasPreorderFromNonStrict ℕ _≡_ ℕ._≤_ NatProp.≤-isPreorder NatProp._≟_
 
   leqNat : HasPartialOrder ℕ _≡_
-  leqNat = record { hasPreorder = preoNat; antisym = NatProp.≤-antisym }
+  leqNat = record { hasPreorder = preoNat ; ≤-antisym = NatProp.≤-antisym }
 
   DecLeqNat : HasDecPartialOrder ℕ _≡_
   DecLeqNat = record { hasPartialOrder = leqNat ; _≤?_ = ℕ._≤?_ }

src/Ledger/Epoch.agda

@@ -7,99 +7,103 @@ open import Ledger.Prelude hiding (compare; Rel)
 open import Algebra using (Semiring)
 open import Relation.Binary
 open import Relation.Binary.Definitions using (Total)
-open import Relation.Binary.Consequences using (tri⇒irr)
+open import Relation.Binary.Consequences -- using (tri⇒irr)
 open import Relation.Nullary.Negation
 open import Data.Nat.Properties using (+-*-semiring; ≤-isTotalOrder)
 
 import Data.Nat as ℕ
 
 record EpochStructure : Set₁ where
-  infix 4 _≤ˢ_ _<ˢ_
+  infix 4 _<ˢ_
   field Slotʳ : Semiring 0ℓ 0ℓ
-        Epoch : Set; ⦃ DecEq-Epoch ⦄ : DecEq Epoch
+        Epoch : Set
+        ⦃ DecEq-Epoch ⦄ : DecEq Epoch
+
+  _≡ᵉ?_ : (e e' : Epoch) → Dec(e ≡ e')
+  _ ≡ᵉ? _ = it
 
   Slot = Semiring.Carrier Slotʳ
 
   field epoch           : Slot → Epoch
         firstSlot       : Epoch → Slot
-        _≤ˢ_            : Rel Slot 0ℓ
-        Slot-TO         : IsTotalOrder _≡_ _≤ˢ_
+        _<ˢ_            : Rel Slot 0ℓ
+        Slot-STO         : IsStrictTotalOrder _≡_ _<ˢ_
         StabilityWindow : Slot
         sucᵉ            : Epoch → Epoch
         ⦃ DecEq-Slot ⦄  : DecEq Slot
 
   _≡ˢ?_ : (s s' : Slot) → Dec(s ≡ s')
   _ ≡ˢ? _ = it
 
-  _<ˢ_ : Rel Slot _
-  s <ˢ s' = s ≤ˢ s' × ¬ (s ≡ s')
+  -- preorders and partial orders
 
-  -- partial order
+  instance
+    preoSlot : HasPreorder Slot _≡_
+    preoSlot = hasPreorderFromStrictTotalOrder Slot _≡_ _<ˢ_ Slot-STO
 
-  ≤ˢ-isPartialOrder : IsPartialOrder _≡_ _≤ˢ_
-  ≤ˢ-isPartialOrder = IsTotalOrder.isPartialOrder Slot-TO
+    poSlot : HasPartialOrder Slot _≡_
+    poSlot = hasPartialOrderFromStrictTotalOrder Slot _≡_ _<ˢ_ Slot-STO
 
-  ≤ˢ-isPreorder : IsPreorder _≡_ _≤ˢ_
-  ≤ˢ-isPreorder = IsPartialOrder.isPreorder ≤ˢ-isPartialOrder
+    decpoSlot : HasDecPartialOrder Slot _≡_
+    decpoSlot = hasDecPartialOrderFromStrictTotalOrder Slot _≡_ _<ˢ_ Slot-STO
 
-  ≤ˢ-isAntisymmetric : Antisymmetric _≡_ _≤ˢ_
-  ≤ˢ-isAntisymmetric = IsPartialOrder.antisym ≤ˢ-isPartialOrder
+  _≤ˢ_ : Rel Slot _
+  _≤ˢ_ = _≤_ preoSlot    -- old definition: s ≤ˢ s' = s <ˢ s' ⊎ s ≡ s'
 
-  ≤ˢ-isTransitive : Transitive _≤ˢ_
-  ≤ˢ-isTransitive = IsPreorder.trans ≤ˢ-isPreorder
+  ≤ˢ-antisym : Antisymmetric _≡_ _≤ˢ_
+  ≤ˢ-antisym = ≤-antisym
 
-  ≤ˢ-isTotal : Total _≤ˢ_
-  ≤ˢ-isTotal = IsTotalOrder.total Slot-TO
+  ≤ˢ-isPreorder : IsPreorder _≡_ _≤ˢ_
+  ≤ˢ-isPreorder = ≤-isPreorder preoSlot
 
-  instance
-    preoSlot : HasPreorder Slot _≡_
-    preoSlot = record { _≤_ = _≤ˢ_ ; isPreorder = ≤ˢ-isPreorder }
+  ≤ˢ-reflexive : Reflexive _≤ˢ_
+  ≤ˢ-reflexive = IsPreorder.reflexive ≤ˢ-isPreorder refl
 
-    poSlot : HasPartialOrder Slot _≡_
-    poSlot = record { hasPreorder = preoSlot ; antisym = ≤ˢ-isAntisymmetric }
+  ≤ˢ-transitive : Transitive _≤ˢ_
+  ≤ˢ-transitive = IsPreorder.trans (≤-isPreorder preoSlot)
 
-  Dec≡⋀TotAntisym≤⇒Dec≤ : Decidable _≡_ → Antisymmetric _≡_ _≤ˢ_ → Total _≤ˢ_ → Decidable _≤ˢ_
-  Dec≡⋀TotAntisym≤⇒Dec≤ dec≡ antisym≤ tot≤ x y with dec≡ x y | tot≤ x y
-  ... | yes refl | _ = true because ofʸ (IsPartialOrder.reflexive ≤ˢ-isPartialOrder refl)
-  ... | no ¬p | inj₁ x≤y = true because ofʸ x≤y
-  ... | no ¬p | inj₂ y≤x = false because (ofⁿ (λ x≤y → ¬p (antisym≤ x≤y y≤x)))
+  ≤ˢ-isTotalOrder : IsTotalOrder _≡_ _≤ˢ_
+  ≤ˢ-isTotalOrder = <-STO⇒≤-isTotalOrder Slot _≡_ _<ˢ_ Slot-STO
 
+  ≤ˢ-total : Total _≤ˢ_
+  ≤ˢ-total = IsTotalOrder.total ≤ˢ-isTotalOrder
 
   _≤ˢ?_ : (s s' : Slot) → Dec (s ≤ˢ s')
-  _≤ˢ?_ = Dec≡⋀TotAntisym≤⇒Dec≤ _≡ˢ?_ ≤ˢ-isAntisymmetric ≤ˢ-isTotal
+  _≤ˢ?_ = _≤?_
 
   ≤ˢ-isDecTotalOrder : IsDecTotalOrder _≡_ _≤ˢ_
-  ≤ˢ-isDecTotalOrder = record { isTotalOrder = Slot-TO ; _≟_ = _≡ˢ?_ ; _≤?_ = _≤ˢ?_ }
+  ≤ˢ-isDecTotalOrder = record { isTotalOrder = ≤ˢ-isTotalOrder ; _≟_ = _≡ˢ?_ ; _≤?_ = _≤ˢ?_ }
 
   instance
-    Dec-≤ˢ : ∀ {n m} → Dec (n ≤ˢ m)
-    Dec-≤ˢ = Decidable²⇒Dec _≤ˢ?_
-
-    decpoSlot : HasDecPartialOrder Slot _≡_
-    decpoSlot = record { hasPartialOrder = poSlot ; _≤?_ = _≤ˢ?_ }
+    Dec-<ˢ : ∀ {n m : Slot} → Dec (n <ˢ m)
+    Dec-<ˢ = Decidable²⇒Dec (IsStrictTotalOrder._<?_ Slot-STO)
 
   _≤ᵉ_ : Epoch → Epoch → Set
   e ≤ᵉ e' = firstSlot e ≤ˢ firstSlot e'
 
-  ≤ᵉ-isReflexive : Reflexive _≤ᵉ_
-  ≤ᵉ-isReflexive = IsPreorder.reflexive ≤ˢ-isPreorder refl
+  ≤ᵉ-reflexive : Reflexive _≤ᵉ_
+  ≤ᵉ-reflexive = ≤ˢ-reflexive
 
   _≤ᵉ?_ : ∀ e e' → Dec (e ≤ᵉ e')
   e ≤ᵉ? e' = firstSlot e ≤ˢ? firstSlot e'
 
   ≤ᵉ-isPreorder : IsPreorder _≡_ _≤ᵉ_
   ≤ᵉ-isPreorder .IsPreorder.isEquivalence     = Ledger.Prelude.isEquivalence
-  ≤ᵉ-isPreorder .IsPreorder.reflexive refl    = ≤ᵉ-isReflexive
-  ≤ᵉ-isPreorder .IsPreorder.trans ij jk       = ≤ˢ-isTransitive ij jk
+  ≤ᵉ-isPreorder .IsPreorder.reflexive refl    = ≤ᵉ-reflexive
+  ≤ᵉ-isPreorder .IsPreorder.trans ij jk       = ≤ˢ-transitive ij jk
+
+  instance
+    preoEpoch : HasPreorder Epoch _≡_
+    preoEpoch = hasPreorderFromNonStrict Epoch _≡_ _≤ᵉ_ ≤ᵉ-isPreorder _≡ᵉ?_
+
+  _<ᵉ_ : Rel Epoch _
+  _<ᵉ_ = HasPreorder._<_ preoEpoch
 
   _ = (∀ {n m} → Dec (n <ˢ m)) ∋ it
   _ = (∀ {n m} → Dec (n ≤ˢ m)) ∋ it
+  _ = (∀ {n m} → Dec (n <ᵉ m)) ∋ it
   _ = (∀ {n m} → Dec (n ≤ᵉ m)) ∋ it
 
-  instance
-    preoEpoch : HasPreorder Epoch _≡_
-    preoEpoch = record { _≤_ = _≤ᵉ_ ; isPreorder = ≤ᵉ-isPreorder }
-
   -- addition
 
   open Semiring Slotʳ renaming (_+_ to _+ˢ_)
@@ -132,8 +136,8 @@ record GlobalConstants : Set₁ where
     .Epoch           → ℕ
     .epoch slot      → slot / SlotsPerEpochᶜ
     .firstSlot e     → e * SlotsPerEpochᶜ
-    ._≤ˢ_            → ℕ._≤_
-    .Slot-TO         → ≤-isTotalOrder
+    ._<ˢ_            → ℕ._<_
+    .Slot-STO         → Data.Nat.Properties.<-isStrictTotalOrder
     .StabilityWindow → StabilityWindowᶜ
     .sucᵉ            → suc
 

src/Ledger/Foreign/HSLedger.agda

@@ -8,6 +8,7 @@ open import Algebra             using (CommutativeMonoid)
 open import Algebra.Morphism    using (module MonoidMorphisms)
 open import Data.Nat.Properties using (+-0-commutativeMonoid)
 open import Relation.Binary.Morphism.Structures
+import Data.Nat as ℕ
 
 open import Foreign.Convertible
 
@@ -61,7 +62,7 @@ module Implementation where
     .inject                    → id
     .policies                  → λ _ → ∅
     .size                      → λ x → 1 -- there is only ada in this token algebra
-    ._≤ᵗ_                      → _≤_
+    ._≤ᵗ_                      → ℕ._≤_
     .AssetName                 → String
     .specialAsset              → "Ada"
     .property                  → λ _ → refl