Merge pull request #983 from IntersectMBO/fd/use-add-excluded

Update agda-sets and remove migrated proofs

Author: facundominguez

flake.lock

@@ -292,7 +292,16 @@ lem-upd-cert-ddeps {pp} deps (L.reg c v ∷ certs) =
   lem-upd-cert-ddeps (deps ∪⁺ dep) certs
   where dep = ❴ L.CredentialDeposit c , pp .PParams.keyDeposit ❵
 lem-upd-cert-ddeps {pp} deps (L.regpool kh p ∷ certs) =
-  ≈-sym (cong-updateDDeps certs (lem-add-excluded-∪ˡ deps λ ())) ⟨≈⟩
+  ≈-sym
+    (cong-updateDDeps
+      certs
+      (subst
+        (λ spQ → filterᵐ? spQ (deps ∪ˡ dep) ≡ᵐ filterᵐ? spQ deps)
+        ≡-sp-∘
+        (add-excluded-∪ˡ-l _ deps λ ())
+      )
+    )
+    ⟨≈⟩
   lem-upd-cert-ddeps (deps ∪ˡ dep) certs
   where dep = ❴ L.PoolDeposit kh , pp .PParams.poolDeposit ❵
 lem-upd-cert-ddeps {pp} deps (L.regdrep c v a ∷ certs) =
@@ -322,7 +331,16 @@ lem-upd-cert-gdeps {pp} deps (L.reg c v ∷ certs) =
   lem-upd-cert-gdeps (deps ∪⁺ dep) certs
   where dep = ❴ L.CredentialDeposit c , pp .PParams.keyDeposit ❵
 lem-upd-cert-gdeps {pp} deps (L.regpool kh p ∷ certs) =
-  ≈-sym (cong-updateGDeps certs (lem-add-excluded-∪ˡ deps λ ())) ⟨≈⟩
+  ≈-sym
+    (cong-updateGDeps
+      certs
+      (subst
+        (λ spQ → filterᵐ? spQ (deps ∪ˡ dep) ≡ᵐ filterᵐ? spQ deps)
+        ≡-sp-∘
+        (add-excluded-∪ˡ-l _ deps λ ())
+      )
+    )
+    ⟨≈⟩
   lem-upd-cert-gdeps (deps ∪ˡ dep) certs
   where dep = ❴ L.PoolDeposit kh , pp .PParams.poolDeposit ❵
 lem-upd-cert-gdeps {pp} deps (L.regdrep c v a ∷ certs) =

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

@@ -2,7 +2,7 @@
 
 module Ledger.Conway.Conformance.Equivalence.Map where
 
-open import Ledger.Prelude hiding (filterᵐ-singleton-false)
+open import Ledger.Prelude
 open import Axiom.Set.Properties th
 
 import Algebra as Alg
@@ -613,13 +613,6 @@ module _  {A B : Type}
       filterᵐ-singleton-true p .proj₁ = proj₂ ∘ (from ∈-filter)
       filterᵐ-singleton-true {k}{v} p .proj₂ {a} x = to ∈-filter (subst P′ (sym (from ∈-singleton x)) p , x)
 
-      -- TODO: move to agda-sets
-      -- https://github.com/input-output-hk/agda-sets/pull/19
-      filterᵐ-singleton-false : ¬ P k → filterᵐ P′ ❴ k , v ❵ ≡ᵐ ∅
-      filterᵐ-singleton-false ¬p .proj₁ x =
-        ⊥-elim $ ¬p $ subst P′ (from ∈-singleton $ proj₂ (from ∈-filter x)) (proj₁ $ from ∈-filter x)
-      filterᵐ-singleton-false _ .proj₂ = ⊥-elim ∘ ∉-∅
-
       filterᵐ-restrict : ∀ m {ks} → filterᵐ P′ (m ∣ ks ᶜ) ≡ᵐ filterᵐ P′ m ∣ ks ᶜ
       filterᵐ-restrict m {ks} .proj₁ {a , b} h with from ∈-filter h
       ... | Pa , ab∈m∖ks with resᶜ-dom∉⁻ m ab∈m∖ks
@@ -647,43 +640,30 @@ module _  {A B : Type}
           ... | px , b , refl = ⊥-elim (¬p px)
           ¬P→res-∅ .proj₂ = ⊥-elim ∘ ∉-∅
 
-
     opaque
+
       lem-add-included : P k → filterᵐ P′ (m ∪⁺ ❴ k , v ❵) ≡ᵐ filterᵐ P′ m ∪⁺ ❴ k , v ❵
-      lem-add-included p =
+      lem-add-included  p =
         filterᵐ-∪⁺-distr _ _ ⟨≈⟩ ∪⁺-cong-l (filterᵐ-singleton-true p)
 
-      lem-add-excluded : ¬ P k → filterᵐ P′ (m ∪⁺ ❴ k , v ❵) ≡ᵐ filterᵐ P′ m
-      lem-add-excluded p =
-        filterᵐ-∪⁺-distr _ _ ⟨≈⟩ ∪⁺-cong-l (filterᵐ-singleton-false p) ⟨≈⟩ ∪⁺-id-r _
-
-      -- TODO: move to agda-sets
-      -- https://github.com/input-output-hk/agda-sets/pull/19
-      lem-add-excluded-∪ˡ
-        : (m : A ⇀ B)
-        → ¬ P k
-        → filterᵐ P′ (m ∪ˡ ❴ k , v ❵) ≡ᵐ filterᵐ P′ m
-      lem-add-excluded-∪ˡ {k = k} {v = v} m ¬p with k ∈? dom m
-      ... | yes k∈m =
-          filterᵐ-cong
-            {m = m ∪ˡ ❴ k , v ❵}
-            {m' = m}
-            (singleton-∈-∪ˡ {m = m} k∈m)
-      ... | no k∉m = begin
-          filterᵐ P′ (m ∪ˡ ❴ k , v ❵) ˢ
-            ≈⟨ filter-cong $ disjoint-∪ˡ-∪ (disjoint-sing k∉m) ⟩
-          filterˢ P′ (m ˢ ∪ ❴ k , v ❵)
-            ≈⟨ filter-hom-∪ ⟩
-          filterˢ P′ (m ˢ) ∪ filterˢ P′ ❴ k , v ❵
-            ≈⟨ ∪-cong ≡ᵉ.refl (filterᵐ-singleton-false ¬p) ⟩
-          filterˢ P′ (m ˢ) ∪ ∅
-            ≈⟨ ∪-identityʳ (filterˢ P′ (m ˢ)) ⟩
-          filterˢ P′ (m ˢ)
-          ∎
-        where
-          disjoint-sing : k ∉ dom m → disjoint (dom m) (dom (singleton (k , v)))
-          disjoint-sing k∉m a∈d a∈sing
-            rewrite from ∈-dom-singleton-pair a∈sing = k∉m a∈d
+    opaque
+      unfolding to-sp
+
+      ≡-sp-∘ : sp-∘ (to-sp P) proj₁ ≡ to-sp P′
+      ≡-sp-∘ = refl
+
+      lem-add-excluded : {m : A ⇀ B} → ¬ P k → filterᵐ P′ (m ∪⁺ ❴ k , v ❵ᵐ) ≡ᵐ filterᵐ P′ m
+      lem-add-excluded {k = k} {v = v} {m = m} p = begin
+        filterᵐ P′ (m ∪⁺ ❴ k , v ❵ᵐ) ˢ
+            ≈⟨ filterᵐ-∪⁺-distr m ❴ k , v ❵ ⟩
+        (filterᵐ P′ m ∪⁺ filterᵐ P′ ❴ k , v ❵) ˢ
+            ≈⟨ ∪⁺-cong-l $ filterᵐ-singleton-false (to-sp P) p ⟩
+        (filterᵐ P′ m ∪⁺ ∅ᵐ) ˢ
+            ≈⟨ ∪⁺-id-r _ ⟩
+        filterᵐ P′ m ˢ
+        ∎
+
+    opaque
 
       lem-del-excluded : ∀ m → ¬ P k → filterᵐ P′ (m ∣ ❴ k ❵ ᶜ) ≡ᵐ filterᵐ P′ m
       lem-del-excluded m ¬p = filterᵐ-restrict m ⟨≈⟩ restrict-singleton-filterᵐ-false m ¬p

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

@@ -233,7 +233,7 @@ module AcceptedByDRep-≈ {Γ Γ' : RatifyEnv} (Γ≈Γ' : RatifyEnv- Γ ≈ Γ'
 
   acceptedStake : abdr.acceptedStake ≡ abdr'.acceptedStake
   acceptedStake =
-    indexedSumᵛ'-cong ⦃ it ⦄ ⦃ it ⦄ ⦃ CommMonoid-ℕ-+ ⦄ {f = id}
+    indexedSumᵛ'-cong {f = id}
       {x = StakeDistrs.stakeDistrVDeleg Γ.stakeDistrs ∣ abdr.actualVotes ⁻¹ _}
       {y = StakeDistrs.stakeDistrVDeleg Γ'.stakeDistrs ∣ abdr'.actualVotes ⁻¹ _}
       (resᵐ-cong {m = StakeDistrs.stakeDistrVDeleg Γ.stakeDistrs}
@@ -242,7 +242,7 @@ module AcceptedByDRep-≈ {Γ Γ' : RatifyEnv} (Γ≈Γ' : RatifyEnv- Γ ≈ Γ'
         (⁻¹-cong {m = abdr.actualVotes} {m' = abdr'.actualVotes} actualVotes))
 
   totalStake : abdr.totalStake ≡ abdr'.totalStake
-  totalStake = indexedSumᵛ'-cong ⦃ it ⦄ ⦃ it ⦄ ⦃ CommMonoid-ℕ-+ ⦄ {f = id}
+  totalStake = indexedSumᵛ'-cong {f = id}
                  {x = StakeDistrs.stakeDistrVDeleg Γ.stakeDistrs ∣ dom (abdr.actualVotes ∣^ (❴ Vote.yes ❵ ∪ ❴ Vote.no ❵))}
                  {y = StakeDistrs.stakeDistrVDeleg Γ'.stakeDistrs ∣ dom (abdr'.actualVotes ∣^ (❴ Vote.yes ❵ ∪ ❴ Vote.no ❵))}
                  (resᵐ-cong {m = StakeDistrs.stakeDistrVDeleg Γ.stakeDistrs}

src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.lagda.md

@@ -129,7 +129,7 @@ module _ -- ASSUMPTION --
                                  (disjoint-sing ¬p)
                              ⟩
       indexedSumᵐ proj₂ ((d ᶠᵐ) ∪ˡᶠ (❴ dp , c ❵ ᶠᵐ))
-                            ≡⟨ sym $ indexedSumᵐ-∪ˡ-∪ˡᶠ {B = ⊤} d ❴ dp , c ❵ ⟩
+                            ≡⟨ sym $ indexedSumᵐ-∪ˡ-∪ˡᶠ d ❴ dp , c ❵ ⟩
       getCoin (d ∪ˡ ❴ dp , c ❵)
       ∎
     where