Address some TODOs about moving proofs to agda-sets

Author: facundominguez

flake.lock

@@ -2,9 +2,8 @@
 
 module Ledger.Conway.Conformance.Equivalence.Map where
 
-open import Ledger.Prelude
+open import Ledger.Prelude hiding (filterᵐ-singleton-false)
 open import Axiom.Set.Properties th
-open import Axiom.Set.Map.Dec
 
 import Algebra as Alg
 import Algebra.Definitions as AlgDefs

src/Ledger/Conway/Conformance/Equivalence/Map.agda

@@ -113,59 +113,6 @@ module LEDGER-PROPS (tx : Tx) (Γ : LEnv) (s : LState) where
     dpMap-rmOrphanDRepVotes : ∀ certState govSt → dpMap (rmOrphanDRepVotes certState govSt) ≡ dpMap govSt
     dpMap-rmOrphanDRepVotes certState govSt = sym (fmap-∘ govSt) -- map proj₁ ∘ map (map₂ _) ≡ map (proj₁ ∘ map₂ _) ≡ map proj₁
 
--- TODO: Move these proofs to agda-sets
--- https://github.com/input-output-hk/agda-sets/pull/18
-module _ {A V : Set} ⦃ mon : CommutativeMonoid 0ℓ 0ℓ V ⦄ ⦃ dA : DecEq A ⦄ {m m' : A ⇀ V} where
-  open import Function.Reasoning
-
-  rhs-∪ˡ : A ⇀ V
-  rhs-∪ˡ = filterᵐ? (sp-∘ (sp-¬ (∈-sp {X = dom (m ˢ)})) proj₁) m'
-
-  dom∪ˡˡ : dom (m ˢ) ⊆ dom ((m ∪ˡ m') ˢ)
-  dom∪ˡˡ {a} a∈ = a∈ ∶
-      a ∈ dom (m ˢ)                   |> ∪-⊆ˡ ∶
-      a ∈ dom (m ˢ) ∪ dom (rhs-∪ˡ ˢ)  |> proj₂ dom∪ ∶
-      a ∈ dom ((m ˢ) ∪ (rhs-∪ˡ ˢ))    |> id ∶
-      a ∈ dom ((m ∪ˡ m') ˢ)
-
-  dom∪ˡʳ : dom (m' ˢ) ⊆ dom ((m ∪ˡ m') ˢ)
-  dom∪ˡʳ {a} a∈ with a ∈? dom m
-  ... | yes p = dom∪ˡˡ p
-  ... | no ¬p = a∈ ∶
-      a ∈ dom m'                            |> from ∈-map ∶
-      (∃[ ab ] a ≡ proj₁ ab × ab ∈ (m' ˢ))  |>
-         (λ { (ab , refl , ab∈m') → (¬p , ab∈m') ∶
-             (a ∉ dom m × ab ∈ m')  |> to ∈-filter ∶
-             ab ∈ rhs-∪ˡ            |> (λ ab∈f → to ∈-map (ab , refl , ab∈f)) ∶
-             a ∈ dom rhs-∪ˡ
-         }) ∶
-      a ∈ dom rhs-∪ˡ                |> ∈-∪⁺ ∘ inj₂ ∶
-      a ∈ dom m ∪ dom rhs-∪ˡ        |> proj₂ dom∪ ∶
-      a ∈ dom ((m ˢ) ∪ (rhs-∪ˡ ˢ))  |> id ∶
-      a ∈ dom ((m ∪ˡ m') ˢ)
-
-  dom∪ˡ⊆∪dom : dom ((m ∪ˡ m') ˢ) ⊆ dom (m ˢ) ∪ dom (m' ˢ)
-  dom∪ˡ⊆∪dom {a} a∈dom∪ with ∈-∪⁻ (proj₁ dom∪ a∈dom∪)
-  ... | inj₁ a∈domm = ∈-∪⁺ (inj₁ a∈domm)
-  ... | inj₂ a∈domf = a∈domf ∶
-      a ∈ dom rhs-∪ˡ                        |> from ∈-map ∶
-      (∃[ ab ] a ≡ proj₁ ab × ab ∈ rhs-∪ˡ)  |>
-         (λ { (ab , refl , ab∈fm') → ab∈fm' ∶
-             ab ∈ rhs-∪ˡ                    |> proj₂ ∘ from ∈-filter ∶
-             ab ∈ m'                        |> (λ ab∈m' → to ∈-map (ab , refl , ab∈m')) ∶
-             a ∈ dom m'
-         }) ∶
-      a ∈ dom m'          |> ∈-∪⁺ ∘ inj₂ ∶
-      a ∈ dom m ∪ dom m'
-
-  ∪dom⊆dom∪ˡ : dom (m ˢ) ∪ dom (m' ˢ) ⊆ dom ((m ∪ˡ m') ˢ)
-  ∪dom⊆dom∪ˡ {a} a∈
-    with from ∈-∪ a∈
-  ... | inj₁ a∈ˡ = dom∪ˡˡ a∈ˡ
-  ... | inj₂ a∈ʳ = dom∪ˡʳ a∈ʳ
-
-  dom∪ˡ≡∪dom : dom ((m ∪ˡ m')ˢ) ≡ᵉ dom (m ˢ) ∪ dom (m' ˢ)
-  dom∪ˡ≡∪dom = dom∪ˡ⊆∪dom , ∪dom⊆dom∪ˡ
 
 module SetoidProperties (tx : Tx) (Γ : LEnv) (s : LState) where
   open Tx tx renaming (body to txb); open TxBody txb

src/Ledger/Conway/Specification/Ledger/Properties/Base.lagda.md

@@ -129,30 +129,16 @@ module _ -- ASSUMPTION --
                                  (disjoint-sing ¬p)
                              ⟩
       indexedSumᵐ proj₂ ((d ᶠᵐ) ∪ˡᶠ (❴ dp , c ❵ ᶠᵐ))
-                            ≡⟨ sym $ indexedSumᵐ-∪ˡ-∪ˡᶠ d ❴ dp , c ❵ ⟩
+                            ≡⟨ sym $ indexedSumᵐ-∪ˡ-∪ˡᶠ {B = ⊤} d ❴ dp , c ❵ ⟩
       getCoin (d ∪ˡ ❴ dp , c ❵)
       ∎
     where
       open ≤-Reasoning
-      open import Relation.Binary.Structures using (IsEquivalence)
-      module ≡ᵉ = IsEquivalence ≡ᵉ-isEquivalence
 
       disjoint-sing : dp ∉ dom d → disjoint (dom d) (dom ❴ dp , c ❵ˢ)
       disjoint-sing dp∉d a∈d a∈sing
         rewrite from ∈-dom-singleton-pair a∈sing = dp∉d a∈d
 
-      -- TODO: remove after adopting
-      -- https://github.com/input-output-hk/agda-sets/pull/17
-      indexedSumᵐ-∪ˡ-∪ˡᶠ
-        : ∀ m m'
-        → indexedSumᵐ proj₂ ((m ∪ˡ m') ᶠᵐ) ≡ indexedSumᵐ proj₂ ((m ᶠᵐ) ∪ˡᶠ (m' ᶠᵐ))
-      indexedSumᵐ-∪ˡ-∪ˡᶠ m m' =
-        indexedSumᵐ-cong
-          {f = proj₂}
-          {x = (m ∪ˡ m') ᶠᵐ}
-          {y = (m ᶠᵐ) ∪ˡᶠ (m' ᶠᵐ)}
-          ≡ᵉ.refl
-
   ≤updateCertDeps : (cs : List DCert) {pp : PParams} {deposits : Deposits}
     → noRefundCert cs
     → getCoin deposits ≤ getCoin (updateCertDeposits pp cs deposits)