Remove postulates; import module from Epoch.Properties

Author: carlostome

src/Ledger/Conway/Specification/Epoch/Properties.agda

@@ -4,5 +4,6 @@ module Ledger.Conway.Specification.Epoch.Properties where
 
 open import Ledger.Conway.Specification.Epoch.Properties.Computational
 open import Ledger.Conway.Specification.Epoch.Properties.ConstRwds
+open import Ledger.Conway.Specification.Epoch.Properties.ExpiredDReps
 open import Ledger.Conway.Specification.Epoch.Properties.GovDepsMatch
 open import Ledger.Conway.Specification.Epoch.Properties.NoPropSameDReps

src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.agda

@@ -1,4 +1,5 @@
--- {-# OPTIONS --without-K #-}
+{-# OPTIONS --safe #-}
+
 open import Ledger.Conway.Specification.Transaction
 open import Ledger.Conway.Specification.Abstract
 
@@ -26,10 +27,6 @@ open import Ledger.Conway.Specification.Gov.Actions govStructure using (Vote)
 open import Axiom.Set.Properties th
 open import Relation.Binary.PropositionalEquality hiding (cong)
 
-postulate
-  e<sucᵉ : ∀ {e : Epoch} → e < sucᵉ e
-  ≤-predᵉ : ∀ {e e' : Epoch} → sucᵉ e ≤ sucᵉ e' → e ≤ e'
-
 -- | Epoch indexed relation.
 -- Two DReps (Map Credential Epoch) are related iff: Non-expired DReps are the same.
 DReps-[_]_≈_ : Epoch → B.Rel DReps 0ℓ

src/Ledger/Core/Specification/Epoch.agda

@@ -6,11 +6,11 @@ open import Ledger.Prelude hiding (compare; Rel)
 
 open import Agda.Builtin.FromNat
 open import Algebra using (Semiring)
-open import Relation.Binary
-open import Data.Nat.Properties using (+-*-semiring)
+open import Data.Nat.Properties using (+-monoˡ-≤; +-cancelˡ-<; +-*-semiring; suc-injective)
 open import Data.Rational using (ℚ)
 import      Data.Rational as ℚ
 import      Data.Rational.Properties as ℚ
+open import Data.Sum using ([_,_]′)
 
 additionVia : ∀{A : Set} → (A → A) → ℕ → A → A
 additionVia sucFun zero r = r
@@ -49,6 +49,10 @@ record EpochStructure : Type₁ where
         ; <-resp-≈ = (λ where refl → id) , (λ where refl → id)
         }
 
+  field
+    e<sucᵉ : ∀ {e : Epoch} → e < sucᵉ e
+    ≤-predᵉ : ∀ {e e' : Epoch} → sucᵉ e ≤ sucᵉ e' → e ≤ e'
+
   _ = _<_ {A = Slot}  ⁇² ∋ it
   _ = _≤_ {A = Slot}  ⁇² ∋ it
   _ = _<_ {A = Epoch} ⁇² ∋ it
@@ -94,12 +98,15 @@ record GlobalConstants : Type₁ where
   ℕEpochStructure : EpochStructure
   ℕEpochStructure = λ where
     .Slotʳ                         → +-*-semiring
+    .DecPo-Slot                    → ℕ-hasDecPartialOrder
     .Epoch                         → ℕ
     .epoch slot                    → slot / SlotsPerEpochᶜ
     .firstSlot e                   → e * SlotsPerEpochᶜ
     .RandomnessStabilisationWindow → RandomnessStabilisationWindowᶜ
     .StabilityWindow               → StabilityWindowᶜ
     .sucᵉ                          → suc
+    .e<sucᵉ                        → +-monoˡ-≤ _ (>-nonZero⁻¹ SlotsPerEpochᶜ)
+    .≤-predᵉ                       → [ (λ p → inj₁ (+-cancelˡ-< _ _ _ p)) , (λ p → inj₂ (suc-injective p)) ]′
     ._+ᵉ'_                         → _+_
     .+ᵉ≡+ᵉ' {a} {b}                → ℕ+ᵉ≡+ᵉ' {a} {b}