Fix instance resolution of _≤ᵉ_, and left-over renamings from #900a1

src/Axiom/Set.agda

@@ -8,7 +8,6 @@ open import Prelude hiding (filter)
 
 import Function.Related.Propositional as R
 open import Data.List.Ext.Properties using (∈-dedup; _×-cong_)
-open import Data.List.Membership.Propositional using () renaming (_∈_ to _∈ˡ_)
 open import Data.List.Relation.Unary.Any using (here; there)
 open import Data.List.Relation.Unary.Unique.DecPropositional.Properties using (deduplicate-!)
 open import Data.List.Relation.Unary.Unique.Propositional using (Unique; [])
@@ -17,9 +16,6 @@ open import Data.Product.Properties using (∃∃↔∃∃)
 open import Data.Product.Properties.Ext using (∃-cong′; ∃-≡)
 open import Interface.DecEq using (DecEq; _≟_)
 open import Relation.Binary using () renaming (Decidable to Dec₂)
-open import Relation.Nullary using (¬?; Dec; yes; no)
-open import Relation.Nullary.Decidable using (⌊_⌋)
-open import Relation.Unary using (Pred) renaming (Decidable to Decidable¹)
 
 private variable
   ℓ : Level
@@ -309,7 +305,7 @@ record Theoryᵈ : Type₁ where
 
   field
     ∈-sp : ⦃ DecEq A ⦄ → spec-∈ A
-    _∈?_ : ⦃ DecEq A ⦄ → Dec₂ (_∈_ {A = A})
+    _∈?_ : ⦃ DecEq A ⦄ → Decidable² (_∈_ {A = A})
     all? : ⦃ DecEq A ⦄ → {P : A → Type} (P? : Decidable¹ P) {X : Set A} → Dec (All P X)
     any? : ⦃ DecEq A ⦄ → {P : A → Type} (P? : Decidable¹ P) (X : Set A) → Dec (Any P X)
 

src/Axiom/Set/Map/Dec.agda

@@ -10,7 +10,6 @@ open import Algebra using (Monoid)
 import Data.Sum as Sum
 open import Data.These hiding (map)
 open import Interface.DecEq using (DecEq)
-open import Relation.Nullary.Decidable using (yes; no)
 
 open Theoryᵈ thᵈ using (_∈?_; th; incl-set'; incl-set)
 open Theory th

src/Axiom/Set/Rel.agda

@@ -1,6 +1,8 @@
 {-# OPTIONS --safe --no-import-sorts #-}
 {-# OPTIONS -v allTactics:100 #-}
 
+open import Prelude hiding (filter)
+
 open import Agda.Primitive using (lzero) renaming (Set to Type)
 open import Axiom.Set using (Theory)
 
@@ -12,8 +14,6 @@ import Function.Related.Propositional as R
 open Theory th
 open import Axiom.Set.Properties th
 
-open import Prelude hiding (filter)
-
 import Data.Product
 open import Data.These hiding (map)
 open import Data.Maybe.Base using () renaming (map to map?)

src/Axiom/Set/Sum.agda

@@ -19,7 +19,6 @@ open import Data.List.Relation.Binary.Permutation.Propositional
 open import Data.List.Relation.Unary.Unique.Propositional using (Unique)
 open import Interface.DecEq using (DecEq; _≟_)
 open import Relation.Binary using (_Preserves_⟶_; IsEquivalence)
-open import Relation.Nullary.Decidable using (¬?)
 open import Relation.Unary using (Decidable)
 
 open import Tactic.AnyOf
@@ -121,7 +120,9 @@ module _ ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq B ⦄ where
     → indexedSumᵐ f Preserves (_≡ᵉ_ on proj₁) ⟶ _≈_
   indexedSumᵐ-cong {x = x , _ , h} {y , _ , h'} = indexedSum-cong {x = x , h} {y , h'}
 
-  module IndexedSumUnionᵐ (sp-∈ : spec-∈ A) (∈-A-dec : {X : Set A} → Decidable (_∈ X)) where
+  module IndexedSumUnionᵐ
+    (sp-∈ : spec-∈ A) (∈-A-dec : {X : Set A} → Decidable¹ (_∈ X)) where
+
     open Unionᵐ sp-∈
 
     ∪ᵐˡ-finite : {R R' : Rel A B} → finite R → finite R' → finite (R ∪ᵐˡ' R')

src/Axiom/Set/TotalMap.agda

@@ -7,7 +7,6 @@ module Axiom.Set.TotalMap (th : Theory) where
 open import Prelude hiding (lookup)
 
 open import Agda.Primitive              using () renaming (Set to Type)
-open import Relation.Nullary.Decidable  using (yes ; no)
 open import Function.Related.TypeIsomorphisms  using (Σ-≡,≡→≡)
 open import Axiom.Set.Map th            using (left-unique; Map ; mapWithKey-uniq ; left-unique-mapˢ)
 open import Axiom.Set.Rel th            using (Rel ; dom ; dom∈)

src/Axiom/Set/TotalMapOn.agda

@@ -10,7 +10,6 @@ open import Agda.Primitive              using () renaming (Set to Type)
 open import Axiom.Set.Map th            using (left-unique ; Map ; mapWithKey-uniq)
 open import Axiom.Set.Rel th            using (Rel ; dom ; dom∈)
 open import Interface.DecEq             using (DecEq ; _≟_)
-open import Relation.Nullary.Decidable  using (Dec ; yes ; no)
 
 open Theory th    using ( Set ; _⊆_ ; _∈_ ; map ; ∈-map′ )
 open Equivalence  using (to)

src/Ledger/Epoch.agda

@@ -23,52 +23,57 @@ record EpochStructure : Set₁ where
         StabilityWindow : Slot
         sucᵉ            : Epoch → Epoch
 
-  _≥ˢ_ : Slot → Slot → Set
-  _≥ˢ_ = ¬_ ∘₂ _<ˢ_
+  -- inequality
 
-  _≤ˢ_ : Slot → Slot → Set
+  _≥ˢ_ _≤ˢ_ : Slot → Slot → Set
+  _≥ˢ_ = ¬_ ∘₂ _<ˢ_
   _≤ˢ_ = flip _≥ˢ_
 
+  _<ᵉ_ _≤ᵉ_ : Epoch → Epoch → Set
+  _<ᵉ_ = _<ˢ_ on firstSlot
+  _≤ᵉ_ = _≤ˢ_ on firstSlot
+
   open IsStrictTotalOrder Slot-STO using () renaming (_<?_ to _<ˢ?_) public
 
-  _≤ˢ?_ : (s s' : Slot) → Dec (s ≤ˢ s')
+  _≤ˢ?_ : ∀ s s' → Dec (s ≤ˢ s')
   s ≤ˢ? s' = ¬? (s' <ˢ? s)
 
+  _≤ᵉ?_ : ∀ e e' → Dec (e ≤ᵉ e')
+  e ≤ᵉ? e' = firstSlot e ≤ˢ? firstSlot e'
+
+  instance
+    Dec-<ˢ : ∀ {n m} → Dec (n <ˢ m)
+    Dec-<ˢ = Decidable²⇒Dec _<ˢ?_
+
+  _ = (∀ {n m} → Dec (n ≤ˢ m)) ∋ it
+  _ = (∀ {n m} → Dec (n <ᵉ m)) ∋ it
+  _ = (∀ {n m} → Dec (n ≤ᵉ m)) ∋ it
+
+  -- addition
+
+  open Semiring Slotʳ renaming (_+_ to _+ˢ_)
+
   ℕtoEpoch : ℕ → Epoch
-  ℕtoEpoch zero    = epoch (Semiring.0# Slotʳ)
+  ℕtoEpoch zero    = epoch 0#
   ℕtoEpoch (suc n) = sucᵉ (ℕtoEpoch n)
 
   _+ᵉ_ : ℕ → Epoch → Epoch
-  zero +ᵉ e = e
+  zero  +ᵉ e = e
   suc n +ᵉ e = sucᵉ (n +ᵉ e)
 
-  open Semiring Slotʳ renaming (_+_ to _+ˢ_)
   _+ᵉ'_ : Epoch → Epoch → Epoch
   e +ᵉ' e' = epoch (firstSlot e +ˢ firstSlot e')
 
-  _<ᵉ_ : Epoch → Epoch → Set
-  e <ᵉ e' = firstSlot e <ˢ firstSlot e'
-
-  _≤ᵉ_ : Epoch → Epoch → Set
-  e ≤ᵉ e' = firstSlot e ≤ˢ firstSlot e'
-
-  _≤ᵉ?_ : (e e' : Epoch) → Dec (e ≤ᵉ e')
-  e ≤ᵉ? e' = firstSlot e ≤ˢ? firstSlot e'
-
   instance
     addSlot : HasAdd Slot
-    addSlot = record { _+_ = _+ˢ_ }
+    addSlot ._+_ = _+ˢ_
 
     addEpoch : HasAdd Epoch
-    addEpoch = record { _+_ = _+ᵉ'_ }
-
-    Dec-≤ᵉ : ∀ {n m} → Dec (n ≤ᵉ m)
-    Dec-≤ᵉ = Decidable²⇒Dec _≤ᵉ?_
+    addEpoch ._+_ = _+ᵉ'_
 
 record GlobalConstants : Set₁ where
   field Network : Set; ⦃ DecEq-Netw ⦄ : DecEq Network
-        SlotsPerEpochᶜ : ℕ
-        ⦃ NonZero-SlotsPerEpoch ⦄ : NonZero SlotsPerEpochᶜ
+        SlotsPerEpochᶜ : ℕ; ⦃ NonZero-SlotsPerEpochᶜ ⦄ : NonZero SlotsPerEpochᶜ
         StabilityWindowᶜ : ℕ
         Quorum : ℕ
         NetworkId : Network

src/Ledger/Gov.lagda

@@ -4,7 +4,6 @@
 {-# OPTIONS --safe #-}
 
 import Data.List as L
-open import Data.List.Membership.Propositional renaming (_∈_ to _∈ˡ_)
 open import Data.List.Membership.Propositional.Properties
 open import Data.List.Relation.Unary.Any renaming (Any to Anyˡ; any? to decAny)
 open import Function.Related using (fromRelated)

src/Ledger/GovernanceActions.lagda

@@ -20,8 +20,6 @@ open import Data.Nat using (_≤_)
 open import Data.Nat.Properties using (+-0-commutativeMonoid; +-0-monoid)
 open import Data.Rational using (ℚ; 0ℚ; 1ℚ)
 
-open import Relation.Nullary.Decidable using (dec-yes)
-
 open import Tactic.Derive.DecEq
 
 module Ledger.GovernanceActions (gs : _) (open GovStructure gs) where
@@ -378,17 +376,15 @@ instance
   ... | .NewCommittee new rem q | Enact-NewComm p
     rewrite dec-yes
       (¿ ∀[ term ∈ range (new ˢ) ] term
-           ≤ᵉ (s .pparams .proj₁ .PParams.ccMaxTermLength +ᵉ e) ¿)
-      p .proj₂
+           ≤ᵉ (s .pparams .proj₁ .PParams.ccMaxTermLength +ᵉ e) ¿) p .proj₂
       = refl
   ... | .NewConstitution dh sh  | Enact-NewConst = refl
   ... | .TriggerHF v            | Enact-HF       = refl
   ... | .ChangePParams up       | Enact-PParams  = refl
   ... | .Info                   | Enact-Info     = refl
   ... | .TreasuryWdrl wdrl      | Enact-Wdrl p
-      with ¿ (Σᵐᵛ[ x ← (s .withdrawals ∪⁺ wdrl) ᶠᵐ ] x) ≤ t ¿ | "bug"
-  ... | yesᵈ p | _ = refl
-  ... | noᵈ ¬p | _ = ⊥-elim (¬p p)
+    rewrite dec-yes (¿ (Σᵐᵛ[ x ← (s .withdrawals ∪⁺ wdrl) ᶠᵐ ] x) ≤ t ¿) p .proj₂
+    = refl
 
   Computational-ENACT = fromComputational' Computational'-ENACT
 \end{code}

src/Ledger/Ledger/Properties.agda

@@ -2,7 +2,6 @@
 
 open import Data.Product.Properties
 
-open import Relation.Nullary.Decidable hiding (map)
 import Relation.Binary.PropositionalEquality as Eq
 
 open import Tactic.ReduceDec using (fromWitness')

src/Ledger/PDF.lagda

@@ -11,10 +11,6 @@
 
 module Ledger.PDF where
 
-open import Data.Maybe.Properties.Ext
--- ^ This module is not used but we import it here for now
---   so that the CI doesn't complain about an unused module.
-
 open import Ledger.BaseTypes
 open import Ledger.Introduction
 open import Ledger.Crypto

src/Ledger/PParams.lagda

@@ -62,7 +62,7 @@ record PParams : Set where
         collateralPercent  : ℕ
 \end{code}
 \emph{Governance group}
-\AgdaTarget{drepThresholds, poolThresholds, minCCSize, ccTermLimit, govExpiration, govActionDeposit, drepDeposit, drepActivity, minimumAVS}
+\AgdaTarget{drepThresholds, poolThresholds, ccMinSize, ccTermLimit, govActionLifetime, govActionDeposit, drepDeposit, drepActivity, minimumAVS}
 \begin{code}
         drepThresholds     : DrepThresholds
         poolThresholds     : PoolThresholds
@@ -109,10 +109,10 @@ These new parameters are declared in Figure~\ref{fig:protocol-parameter-declarat
   \item \drepThresholds: governance thresholds for \DReps; these are rational numbers
   named \Pone, \Ptwoa, \Ptwob, \Pthree, \Pfour, \Pfivea, \Pfiveb, \Pfivec, \Pfived, and \Psix;
   \item \poolThresholds: pool-related governance thresholds; these are rational numbers named \Qone, \Qtwoa, \Qtwob, and \Qfour;
-  \item \minCCSize: minimum constitutional committee size;
+  \item \ccMinSize: minimum constitutional committee size;
   \item \ccTermLimit: maximum term limit (in epochs) of constitutional committee members;
-  \item \govExpiration: governance action expiration;
-  \item \govDeposit: governance action deposit;
+  \item \govActionLifetime: governance action expiration;
+  \item \govActionDeposit: governance action deposit;
   \item \drepDeposit: \DRep deposit amount;
   \item \drepActivity: \DRep activity period;
   \item \minimumAVS: the minimum active voting threshold.

src/Ledger/Prelude.agda

@@ -15,9 +15,7 @@ open import Prelude public
 
 open import Ledger.Prelude.Base public
 
-open import Data.List.Membership.Propositional using () renaming (_∈_ to _∈ˡ_)
-open import Relation.Nullary public
-open import Relation.Unary using () renaming (Decidable to Decidable¹) public
+open import Data.Maybe.Properties.Ext public
 open import Interface.DecEq.Ext public
 open import Interface.HasAdd public
 open import Interface.HasAdd.Instance public

src/Ledger/Ratify.lagda

@@ -86,7 +86,6 @@ open import Data.Nat hiding (_≟_)
 open import Data.Nat.Properties hiding (_≟_)
 open import Data.Nat.Properties.Ext
 open import Data.Product using (map₂)
-open import Relation.Nullary.Decidable using (⌊_⌋)
 
 open import Ledger.Prelude hiding (_∧_)
 open import Ledger.Transaction

src/Ledger/Utxo.lagda

@@ -94,7 +94,7 @@ module _ (open TxBody) where
 
   propDepositᵐ : PParams → GovActionID → GovProposal → DepositPurpose ⇀ Coin
   propDepositᵐ pp gaid record { returnAddr = record { stake = c } }
-    = ❴ GovActionDeposit gaid , pp .govDeposit ❵ᵐ
+    = ❴ GovActionDeposit gaid , pp .govActionDeposit ❵ᵐ
 
   certRefund : DCert → Maybe DepositPurpose
   certRefund (delegate c nothing nothing x)  = just (CredentialDeposit c)

src/Ledger/Utxow/Properties.agda

@@ -20,8 +20,8 @@ private
         witsKeyHashes     = map hash (dom (vkSigs ˢ))
         witsScriptHashes  = map hash scripts
     in
-      ∀[ (vk , σ) ∈ vkSigs ˢ ] isSigned vk (txidBytes txid) σ
-    × ∀[ s ∈ scriptsP1 ] validP1Script witsKeyHashes txvldt s
+      (∀[ (vk , σ) ∈ vkSigs ˢ ] isSigned vk (txidBytes txid) σ)
+    × (∀[ s ∈ scriptsP1 ] validP1Script witsKeyHashes txvldt s)
     × witsVKeyNeeded ppolicy utxo txb ⊆ witsKeyHashes
     × scriptsNeeded ppolicy utxo txb ≡ᵉ witsScriptHashes
     × txADhash ≡ M.map hash txAD

src/Prelude.agda

@@ -4,19 +4,40 @@ module Prelude where
 
 open import Test.GetType
 
-open import Level hiding (lower) renaming (_⊔_ to _⊔ˡ_; suc to sucˡ; zero to zeroˡ) public
+open import Level public
+  hiding (lower)
+  renaming (_⊔_ to _⊔ˡ_; suc to sucˡ; zero to zeroˡ)
 open import Function public
 
-open import Data.Bool hiding (_≟_; _≤_; _≤?_; _<_; _<?_) public
+open import Data.Bool public
+  hiding (_≟_; _≤_; _≤?_; _<_; _<?_)
 open import Data.Empty public
-open import Data.List hiding (align; alignWith; fromMaybe; map; zip; zipWith) public
-open import Data.Maybe hiding (_>>=_; align; alignWith; ap; fromMaybe; map; zip; zipWith) public
-open import Data.Unit hiding (_≟_) public
-open import Data.Sum hiding (assocʳ; assocˡ; map; map₁; map₂; reduce; swap) public
-open import Data.Product hiding (assocʳ; assocˡ; map; map₁; map₂; swap) public
-open import Data.Nat hiding (_≟_; _≤_; _≤?_; _<_; _<?_; _≤ᵇ_; _≡ᵇ_) renaming (_+_ to _+ℕ_) public
-open import Data.Integer as ℤ using (ℤ; _⊖_) renaming (_+_ to _+ℤ_) public
-open import Data.String using (String; _<+>_) public
+open import Data.List public
+  hiding (align; alignWith; fromMaybe; map; zip; zipWith)
+open import Data.List.Membership.Propositional public
+  using () renaming (_∈_ to _∈ˡ_)
+open import Data.Maybe public
+  hiding (_>>=_; align; alignWith; ap; fromMaybe; map; zip; zipWith) public
+open import Data.Unit public
+  hiding (_≟_)
+open import Data.Sum public
+  hiding (assocʳ; assocˡ; map; map₁; map₂; reduce; swap)
+open import Data.Product public
+  hiding (assocʳ; assocˡ; map; map₁; map₂; swap)
+open import Data.Nat public
+  hiding (_≟_; _≤_; _≤?_; _<_; _<?_; _≤ᵇ_; _≡ᵇ_) renaming (_+_ to _+ℕ_)
+open import Data.Integer as ℤ public
+  using (ℤ; _⊖_) renaming (_+_ to _+ℤ_)
+open import Data.String public
+  using (String; _<+>_)
 
+open import Relation.Nullary public
 open import Relation.Nullary.Negation public
-open import Relation.Binary.PropositionalEquality hiding (preorder; setoid; [_]; module ≡-Reasoning) public
+open import Relation.Nullary.Decidable public
+  using (Dec; yes; no; dec-yes; dec-no; ⌊_⌋; ¬?; toWitness; fromWitness)
+open import Relation.Unary public
+  using (Pred) renaming (Decidable to Decidable¹)
+open import Relation.Binary public
+  using () renaming (Decidable to Decidable²)
+open import Relation.Binary.PropositionalEquality public
+  hiding (preorder; setoid; [_]; module ≡-Reasoning)

src/latex/agda-latex-macros.sty

@@ -251,9 +251,9 @@
 \newcommand{\GovActionID}{\AgdaDatatype{GovActionID}\xspace}
 \newcommand{\GovActionIDFunction}{\AgdaFunction{GovActionID}\xspace}
 \newcommand{\GovActionState}{\AgdaRecord{GovActionState}\xspace}
-\newcommand{\govDeposit}{\AgdaField{govDeposit}\xspace}
+\newcommand{\govActionDeposit}{\AgdaField{govActionDeposit}\xspace}
 \newcommand{\GovernanceGroup}{\AgdaInductiveConstructor{GovernanceGroup}\xspace}
-\newcommand{\govExpiration}{\AgdaField{govExpiration}\xspace}
+\newcommand{\govActionLifetime}{\AgdaField{govActionLifetime}\xspace}
 \newcommand{\GovProposal}{\AgdaRecord{GovProposal}\xspace}
 \newcommand{\GovRole}{\AgdaDatatype{GovRole}\xspace}
 \newcommand{\GovVote}{\AgdaRecord{GovVote}\xspace}
@@ -308,7 +308,7 @@
 \newcommand{\maybeprime}{\AgdaFunction{maybe′}\xspace}
 \newcommand{\meetsMinAVS}{\AgdaFunction{meetsMinAVS}\xspace}
 \newcommand{\minimumAVS}{\AgdaField{minimumAVS}\xspace}
-\newcommand{\minCCSize}{\AgdaField{minCCSize}\xspace}
+\newcommand{\ccMinSize}{\AgdaField{ccMinSize}\xspace}
 \newcommand{\mleqmplusn}{\AgdaFunction{m≤m+n}\xspace}
 \newcommand{\module}{\AgdaKeyword{module}\xspace}
 \newcommand{\mostStakeDRepDist}{\AgdaFunction{mostStakeDRepDist}\xspace}