[Conway] Discharge PoV map/coin assumptions via reusable Ledger.Prelude lemmas

src/Ledger/Conway/Conformance/Properties.lagda.md

@@ -124,8 +124,6 @@ module _ (s : ChainState) where
   -- Transaction properties
 
   module _ {slot} {tx} (let txb = body tx) (valid : validTxIn₂ s slot tx)
-    (indexedSum-∪⁺-hom : ∀ {A V : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq V ⦄ ⦃ mon : CommutativeMonoid 0ℓ 0ℓ V ⦄
-      → (d₁ d₂ : A ⇀ V) → indexedSumᵛ' id (d₁ ∪⁺ d₂) ≡ indexedSumᵛ' id d₁ ◇ indexedSumᵛ' id d₂)
     (indexedSum-⊆ : ∀ {A : Type} ⦃ _ : DecEq A ⦄ (d d' : A ⇀ ℕ) → d ˢ ⊆ d' ˢ
       → indexedSumᵛ' id d ≤ indexedSumᵛ' id d') -- technically we could use an ordered monoid instead of ℕ
     where

src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md

@@ -46,19 +46,12 @@ private variable
 instance
   _ = +-0-monoid
 
-module Certs-PoV  ( indexedSumᵛ'-∪' :  {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin)
-                              → disjoint (dom m) (dom m')
-                              → getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m' )
-    -- TODO: prove some or all of the following assumptions, used in roof of `CERTBASE-pov`.
-    ( sumConstZero'    :  {A : Type} ⦃ _ : DecEq A ⦄ {X : ℙ A} → getCoin (constMap X 0) ≡ 0 )
-    ( res-decomp'      :  {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin)
-                         → (m ∪ˡ m')ˢ ≡ᵉ (m ∪ˡ (m' ∣ dom (m ˢ) ᶜ))ˢ )
-    ( getCoin-cong'    :  {A : Type} ⦃ _ : DecEq A ⦄ (s : A ⇀ Coin) (s' : ℙ (A × Coin)) → s ˢ ≡ᵉ s'
-                         → indexedSum' proj₂ (s ˢ) ≡ indexedSum' proj₂ s' )
-    ( ≡ᵉ-getCoinˢ'     :  {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'}
-                         → InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s )
+module Certs-PoV
+    -- TODO: prove the following assumption, used in proof of `CERTBASE-pov`.
+    ( ≡ᵉ-getCoinˢ' :  {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'}
+                      → InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s )
     where
-    open Certs-Pov-lemmas indexedSumᵛ'-∪' sumConstZero' res-decomp' getCoin-cong' ≡ᵉ-getCoinˢ'
+    open Certs-Pov-lemmas ≡ᵉ-getCoinˢ'
 ```
 -->
 

src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md

@@ -23,7 +23,7 @@ open import Axiom.Set.Properties th
 open import Algebra using (CommutativeMonoid)
 open import Data.Maybe.Properties
 open import Data.Nat.Properties using (+-0-monoid; +-0-commutativeMonoid; +-identityʳ; +-identityˡ)
-open import Relation.Binary using (IsEquivalence)
+import Relation.Binary as Eq using (IsEquivalence)
 open import Relation.Nullary.Decidable
 open import Tactic.ReduceDec
 
@@ -40,35 +40,7 @@ private variable
 instance
   _ = +-0-monoid
 
-getCoin-singleton : ⦃ _ : DecEq A ⦄ {(a , c) : A × Coin} → indexedSumᵛ' id ❴ (a , c) ❵ ≡ c
-getCoin-singleton = indexedSum-singleton' {M = Coin} (finiteness _)
-
-∪ˡsingleton∈dom :  ⦃ _ : DecEq A ⦄ (m : A ⇀ Coin) {(a , c) : A × Coin}
-                → a ∈ dom m → getCoin (m ∪ˡ ❴ (a , c) ❵ᵐ) ≡ getCoin m
-∪ˡsingleton∈dom m {(a , c)} a∈dom = ≡ᵉ-getCoin (m ∪ˡ ❴ (a , c) ❵) m (singleton-∈-∪ˡ {m = m} a∈dom)
-
-module _  ( indexedSumᵛ'-∪ :  {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin)
-                              → disjoint (dom m) (dom m')
-                              → getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m' )
-  where
-  open ≡-Reasoning
-  open Equivalence
-
-  ∪ˡsingleton∉dom :  ⦃ _ : DecEq A ⦄ (m : A ⇀ Coin) {(a , c) : A × Coin}
-                   → a ∉ dom m → getCoin (m ∪ˡ ❴ (a , c) ❵ᵐ) ≡ getCoin m + c
-  ∪ˡsingleton∉dom m {(a , c)} a∉dom = begin
-    getCoin (m ∪ˡ ❴ a , c ❵ᵐ)
-      ≡⟨ indexedSumᵛ'-∪ m ❴ a , c ❵ᵐ
-         ( λ x y → a∉dom (subst (_∈ dom m) (from ∈-dom-singleton-pair y) x) ) ⟩
-    getCoin m + getCoin ❴ a , c ❵ᵐ
-      ≡⟨ cong (getCoin m +_) getCoin-singleton ⟩
-    getCoin m + c
-      ∎
-
-  ∪ˡsingleton0≡ : ⦃ _ : DecEq A ⦄ → (m : A ⇀ Coin) {a : A} → getCoin (m ∪ˡ ❴ (a , 0) ❵ᵐ) ≡ getCoin m
-  ∪ˡsingleton0≡ m {a} with a ∈? dom m
-  ... | yes a∈dom = ∪ˡsingleton∈dom m a∈dom
-  ... | no a∉dom = trans (∪ˡsingleton∉dom m a∉dom) (+-identityʳ (getCoin m))
+open ≡-Reasoning
 ```
 -->
 
@@ -83,61 +55,55 @@ some `dcert`{.AgdaBound} : `DCert`{.AgdaDatatype}. Then,
 *Formally*.
 
 ```agda
-  CERT-pov : {Γ : CertEnv} {s s'  : CertState}
-    → Γ ⊢ s ⇀⦇ dCert ,CERT⦈ s'
-    → getCoin s ≡ getCoin s'
+CERT-pov : {Γ : CertEnv} {s s'  : CertState}
+  → Γ ⊢ s ⇀⦇ dCert ,CERT⦈ s' → getCoin s ≡ getCoin s'
 ```
 
 *Proof*.  (Click the "Show more Agda" button to reveal the proof.)
 
 <!--
 ```agda
-  CERT-pov (CERT-deleg (DELEG-delegate {rwds = rwds} _)) = sym (∪ˡsingleton0≡ rwds)
-  CERT-pov (CERT-deleg (DELEG-reg {rwds = rwds} _)) = sym (∪ˡsingleton0≡ rwds)
-  CERT-pov {s = ⟦ _ , stᵖ , stᵍ ⟧ᶜˢ}{⟦ _ , stᵖ' , stᵍ' ⟧ᶜˢ}
-    (CERT-deleg (DELEG-dereg {c = c} {rwds} {vDelegs = vDelegs}{sDelegs} x)) = begin
-    getCoin ⟦ ⟦ vDelegs , sDelegs , rwds ⟧ , stᵖ , stᵍ ⟧
-      ≡˘⟨ ≡ᵉ-getCoin rwds-∪ˡ-decomp rwds
-          ( ≡ᵉ.trans rwds-∪ˡ-∪ (≡ᵉ.trans ∪-sym (res-ex-∪ Dec-∈-singleton)) ) ⟩
-    getCoin rwds-∪ˡ-decomp
-      ≡⟨ ≡ᵉ-getCoin rwds-∪ˡ-decomp ((rwds ∣ ❴ c ❵ ᶜ) ∪ˡ ❴ (c , 0) ❵ᵐ) rwds-∪ˡ≡sing-∪ˡ  ⟩
-    getCoin ((rwds ∣ ❴ c ❵ ᶜ) ∪ˡ ❴ (c , 0) ❵ᵐ )
-      ≡⟨ ∪ˡsingleton0≡ (rwds ∣ ❴ c ❵ ᶜ) ⟩
-    getCoin ⟦ ⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ ⟧ , stᵖ' , stᵍ' ⟧
-      ∎
-    where
-    module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin})
-    rwds-∪ˡ-decomp = (rwds ∣ ❴ c ❵ ᶜ) ∪ˡ (rwds ∣ ❴ c ❵ )
-
-    rwds-∪ˡ-∪ : rwds-∪ˡ-decomp ˢ ≡ᵉ (rwds ∣ ❴ c ❵ ᶜ)ˢ ∪ (rwds ∣ ❴ c ❵)ˢ
-    rwds-∪ˡ-∪ = disjoint-∪ˡ-∪ (disjoint-sym res-ex-disjoint)
-
-    disj : disjoint (dom ((rwds ∣ ❴ c ❵ˢ ᶜ) ˢ)) (dom (❴ c , 0 ❵ᵐ ˢ))
-    disj {a} a∈res a∈dom  = res-comp-dom a∈res (dom-single→single a∈dom)
-
-    rwds-∪ˡ≡sing-∪ˡ : rwds-∪ˡ-decomp ˢ ≡ᵉ ((rwds ∣ ❴ c ❵ ᶜ) ∪ˡ ❴ (c , 0) ❵ᵐ )ˢ
-    rwds-∪ˡ≡sing-∪ˡ = ≡ᵉ.trans rwds-∪ˡ-∪
-                              ( ≡ᵉ.trans (∪-cong ≡ᵉ.refl (res-singleton'{m = rwds} x))
-                                         (≡ᵉ.sym $ disjoint-∪ˡ-∪ disj) )
-  CERT-pov (CERT-pool x) = refl
-  CERT-pov (CERT-vdel x) = refl
-
-  injOn : (wdls : Withdrawals)
-          → ∀[ a ∈ dom (wdls ˢ) ] NetworkIdOf a ≡ NetworkId
-          → InjectiveOn (dom (wdls ˢ)) RewardAddress.stake
-  injOn _ h {record { stake = stakex }} {record { stake = stakey }} x∈ y∈ refl =
-    cong (λ u → record { net = u ; stake = stakex }) (trans (h x∈) (sym (h y∈)))
-
-  module Certs-Pov-lemmas
-    -- TODO: prove some or all of the following assumptions, used in roof of `CERTBASE-pov`.
-    ( sumConstZero    :  {A : Type} ⦃ _ : DecEq A ⦄ {X : ℙ A} → getCoin (constMap X 0) ≡ 0 )
-    ( res-decomp      :  {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin)
-                         → (m ∪ˡ m')ˢ ≡ᵉ (m ∪ˡ (m' ∣ dom (m ˢ) ᶜ))ˢ )
-    ( getCoin-cong    :  {A : Type} ⦃ _ : DecEq A ⦄ (s : A ⇀ Coin) (s' : ℙ (A × Coin)) → s ˢ ≡ᵉ s'
-                         → indexedSum' proj₂ (s ˢ) ≡ indexedSum' proj₂ s' )
-    ( ≡ᵉ-getCoinˢ     :  {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'}
-                         → InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s )
-    where
+CERT-pov (CERT-deleg (DELEG-delegate {rwds = rwds} _)) = sym (∪ˡsingleton0≡ rwds)
+CERT-pov (CERT-deleg (DELEG-reg {rwds = rwds} _)) = sym (∪ˡsingleton0≡ rwds)
+CERT-pov {s = ⟦ _ , stᵖ , stᵍ ⟧ᶜˢ}{⟦ _ , stᵖ' , stᵍ' ⟧ᶜˢ}
+  (CERT-deleg (DELEG-dereg {c = c} {rwds} {vDelegs = vDelegs}{sDelegs} x)) = begin
+  getCoin ⟦ ⟦ vDelegs , sDelegs , rwds ⟧ , stᵖ , stᵍ ⟧
+    ≡˘⟨ ≡ᵉ-getCoin rwds-∪ˡ-decomp rwds
+        ( ≡ᵉ.trans rwds-∪ˡ-∪ (≡ᵉ.trans ∪-sym (res-ex-∪ Dec-∈-singleton)) ) ⟩
+  getCoin rwds-∪ˡ-decomp
+    ≡⟨ ≡ᵉ-getCoin rwds-∪ˡ-decomp ((rwds ∣ ❴ c ❵ ᶜ) ∪ˡ ❴ (c , 0) ❵ᵐ) rwds-∪ˡ≡sing-∪ˡ  ⟩
+  getCoin ((rwds ∣ ❴ c ❵ ᶜ) ∪ˡ ❴ (c , 0) ❵ᵐ )
+    ≡⟨ ∪ˡsingleton0≡ (rwds ∣ ❴ c ❵ ᶜ) ⟩
+  getCoin ⟦ ⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ ⟧ , stᵖ' , stᵍ' ⟧
+    ∎
+  where
+  module ≡ᵉ = Eq.IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin})
+  rwds-∪ˡ-decomp = (rwds ∣ ❴ c ❵ ᶜ) ∪ˡ (rwds ∣ ❴ c ❵ )
+
+  rwds-∪ˡ-∪ : rwds-∪ˡ-decomp ˢ ≡ᵉ (rwds ∣ ❴ c ❵ ᶜ)ˢ ∪ (rwds ∣ ❴ c ❵)ˢ
+  rwds-∪ˡ-∪ = disjoint-∪ˡ-∪ (disjoint-sym res-ex-disjoint)
+
+  disj : disjoint (dom ((rwds ∣ ❴ c ❵ˢ ᶜ) ˢ)) (dom (❴ c , 0 ❵ᵐ ˢ))
+  disj {a} a∈res a∈dom  = res-comp-dom a∈res (dom-single→single a∈dom)
+
+  rwds-∪ˡ≡sing-∪ˡ : rwds-∪ˡ-decomp ˢ ≡ᵉ ((rwds ∣ ❴ c ❵ ᶜ) ∪ˡ ❴ (c , 0) ❵ᵐ )ˢ
+  rwds-∪ˡ≡sing-∪ˡ = ≡ᵉ.trans rwds-∪ˡ-∪
+                            ( ≡ᵉ.trans (∪-cong ≡ᵉ.refl (res-singleton'{m = rwds} x))
+                                       (≡ᵉ.sym $ disjoint-∪ˡ-∪ disj) )
+CERT-pov (CERT-pool x) = refl
+CERT-pov (CERT-vdel x) = refl
+
+injOn : (wdls : Withdrawals)
+        → ∀[ a ∈ dom (wdls ˢ) ] NetworkIdOf a ≡ NetworkId
+        → InjectiveOn (dom (wdls ˢ)) RewardAddress.stake
+injOn _ h {record { stake = stakex }} {record { stake = stakey }} x∈ y∈ refl =
+  cong (λ u → record { net = u ; stake = stakex }) (trans (h x∈) (sym (h y∈)))
+
+module Certs-Pov-lemmas
+  -- TODO: prove the following assumption, used in proof of `CERTBASE-pov`.
+  ( ≡ᵉ-getCoinˢ :  {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'}
+                   → InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s )
+  where
 ```
 -->
 
@@ -175,7 +141,7 @@ value of the withdrawals in `Γ`{.AgdaBound}.  In other terms,
       let
         open DState (dState cs )
         open DState (dState cs') renaming (rewards to rewards')
-        module ≡ᵉ       = IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin})
+        module ≡ᵉ       = Eq.IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin})
         wdrlsCC         = mapˢ (map₁ RewardAddress.stake) (wdrls ˢ)
         zeroMap         = constMap (mapˢ RewardAddress.stake (dom wdrls)) 0
         rwds-∪ˡ-decomp  = (rewards ∣ dom wdrlsCC ᶜ) ∪ˡ (rewards ∣ dom wdrlsCC)

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

@@ -38,15 +38,9 @@ instance
 
 module _
   (tx : Tx) (let open Tx tx; open TxBody body)
-  ( indexedSumᵛ'-∪  :  {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin)
-                       → disjoint (dom m) (dom m') → getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m' )
-  ( sumConstZero    :  {A : Type} ⦃ _ : DecEq A ⦄ {X : ℙ A} → getCoin (constMap X 0) ≡ 0 )
-  ( res-decomp      :  {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin)
-                       → (m ∪ˡ m')ˢ ≡ᵉ (m ∪ˡ (m' ∣ dom (m ˢ) ᶜ))ˢ )
-  ( getCoin-cong    :  {A : Type} ⦃ _ : DecEq A ⦄ (s : A ⇀ Coin) (s' : ℙ (A × Coin)) → s ˢ ≡ᵉ s'
-                       → indexedSum' proj₂ (s ˢ) ≡ indexedSum' proj₂ s' )
-  ( ≡ᵉ-getCoinˢ     :  {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'}
-                       → InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s )
+  -- TODO: prove the following assumption, used in proof of `CERTBASE-pov`.
+  ( ≡ᵉ-getCoinˢ :  {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'}
+                   → InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s )
   where
 
   pattern UTXO-induction r = UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ r _ _ _
@@ -84,8 +78,8 @@ then the coin values of `s`{.AgdaBound} and `s'`{.AgdaBound} are equal, that is,
       open LState s' renaming (utxoSt to utxoSt'; govSt to govSt'; certState to certState')
       open CertState certState'
       open ≡-Reasoning
-      open Certs-PoV indexedSumᵛ'-∪ sumConstZero res-decomp  getCoin-cong ≡ᵉ-getCoinˢ
-      zeroMap    = constMap (mapˢ RewardAddress.stake (dom txWithdrawals)) 0
+      open Certs-PoV ≡ᵉ-getCoinˢ
+      zeroMap = constMap (mapˢ RewardAddress.stake (dom txWithdrawals)) 0
     in
     begin
       getCoin utxoSt + getCoin certState

src/Ledger/Conway/Specification/Utxo/Properties/GenMinSpend.lagda.md

@@ -51,9 +51,6 @@ coin∅ = begin
   0 ∎
   where open Prelude.≡-Reasoning
 
-getCoin-singleton : ((dp , c) : DepositPurpose × Coin) → indexedSumᵛ' id ❴ (dp , c) ❵ ≡ c
-getCoin-singleton _ = indexedSum-singleton' {A = DepositPurpose × Coin} {f = proj₂} (finiteness _)
-
 module _ -- ASSUMPTION --
          (gc-hom : (d₁ d₂ : Deposits) → getCoin (d₁ ∪⁺ d₂) ≡ getCoin d₁ + getCoin d₂)
   where
@@ -63,7 +60,7 @@ module _ -- ASSUMPTION --
     getCoin (deps ∪⁺ ❴ (dp , c) ❵)
       ≡⟨ gc-hom deps ❴ (dp , c) ❵ ⟩
     getCoin deps + getCoin{A = Deposits} ❴ (dp , c) ❵
-      ≡⟨ cong (getCoin deps +_) (getCoin-singleton (dp , c)) ⟩
+      ≡⟨ cong (getCoin deps +_) getCoin-singleton ⟩
     getCoin deps + c
       ∎
     where open Prelude.≡-Reasoning

src/Ledger/Prelude.lagda.md

@@ -48,16 +48,14 @@ open import abstract-set-theory.Axiom.Set.Map.Extra public
 
 import Data.Integer as ℤ
 open import Data.Integer using (0ℤ) public
+open import Data.Nat.Properties using (+-identityʳ)
 import Data.Rational as ℚ
 open import Data.Rational using (ℚ)
 
 dec-de-morgan : ∀{P Q : Type} → ⦃ P ⁇ ⦄ → ¬ (P × Q) → ¬ P ⊎ ¬ Q
 dec-de-morgan ⦃ ⁇ no ¬p ⦄ ¬pq = inj₁ ¬p
 dec-de-morgan ⦃ ⁇ yes p ⦄ ¬pq = inj₂ λ q → ¬pq (p , q)
 
-≡ᵉ-getCoin : ∀ {A} → ⦃ _ : DecEq A ⦄ → (s s' : A ⇀ Coin) → s ˢ ≡ᵉ s' ˢ → getCoin s ≡ getCoin s'
-≡ᵉ-getCoin {A} ⦃ decEqA ⦄ s s' s≡s' = indexedSumᵛ'-cong {C = Coin} {x = s} {y = s'} s≡s'
-
 setToMap : ∀ {A B : Type} → ⦃ DecEq A ⦄ → ℙ (A × B) → A ⇀ B
 setToMap = fromListᵐ ∘ setToList
 
@@ -98,4 +96,95 @@ Is-∅ X = Is-[] (setToList X)
 
 concatMapˡ : {A B : Type} → (A → ℙ B) → List A → ℙ B
 concatMapˡ f as = proj₁ $ unions (fromList (map f as))
+
+indexedSumL-proj₂-zero : ∀ {A : Type} (l : List (A × Coin))
+  → (∀ {x} → x ∈ˡ l → proj₂ x ≡ 0)
+  → indexedSumL {M = Coin} proj₂ l ≡ 0
+indexedSumL-proj₂-zero [] _ = refl
+indexedSumL-proj₂-zero ((a , v) ∷ xs) all-zero =
+  trans (cong (_+ indexedSumL proj₂ xs) (all-zero (Prelude.Init.here refl)))
+        (indexedSumL-proj₂-zero xs (all-zero ∘ Prelude.Init.there))
+
+module _ {A : Type} ⦃ _ : DecEq A ⦄ where
+
+  -- A coin singleton has the coin you expect.
+  getCoin-singleton : {(a , c) : A × Coin} → indexedSumᵛ' id ❴ (a , c) ❵ ≡ c
+  getCoin-singleton = indexedSum-singleton' {M = Coin} (finiteness _)
+
+  ≡ᵉ-getCoin : (s s' : A ⇀ Coin) → s ˢ ≡ᵉ s' ˢ → getCoin s ≡ getCoin s'
+  ≡ᵉ-getCoin s s' s≡s' = indexedSumᵛ'-cong {C = Coin} {x = s} {y = s'} s≡s'
+
+  getCoin-cong : (s : A ⇀ Coin) (s' : ℙ (A × Coin))
+    → s ˢ ≡ᵉ s' → indexedSum' proj₂ (s ˢ) ≡ indexedSum' proj₂ s'
+  getCoin-cong s s' eq = indexedSum-cong {f = proj₂} {x = (s ˢ) ᶠˢ} {y = s' ᶠˢ} eq
+
+  indexedSumᵛ'-∪ : (m m' : A ⇀ Coin) → disjoint (dom m) (dom m')
+    → getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m'
+  indexedSumᵛ'-∪ m m' disj =
+    trans (indexedSumᵐ-∪ˡ-∪ˡᶠ m m')
+          (indexedSumᵐ-∪ {X = m ᶠᵐ} {m' ᶠᵐ} {f = proj₂} disj)
+
+  open import Axiom.Set.Properties th
+  open import Relation.Binary using (IsEquivalence)
+
+  res-decomp : (m m' : A ⇀ Coin) → (m ∪ˡ m')ˢ ≡ᵉ (m ∪ˡ (m' ∣ dom (m ˢ) ᶜ))ˢ
+  res-decomp m m' = ∪-cong (≡ᵉ.refl {x = m ˢ}) (≡ᵉ.sym (filterᵐ-idem {m = m'}))
+    where module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence {A × Coin})
+
+  -- If a is already in domain of m, left-biased union with singleton at a
+  -- leaves total unchanged (existing entry wins).
+  ∪ˡsingleton∈dom : (m : A ⇀ Coin) {(a , c) : A × Coin}
+    → a ∈ dom m → getCoin (m ∪ˡ ❴ (a , c) ❵ᵐ) ≡ getCoin m
+  ∪ˡsingleton∈dom m {(a , c)} a∈dom =
+    ≡ᵉ-getCoin (m ∪ˡ ❴ (a , c) ❵ᵐ) m (singleton-∈-∪ˡ {m = m} a∈dom)
+
+  -- If a is *not* in domain of m, left-biased union with singleton adds cleanly.
+  ∪ˡsingleton∉dom : (m : A ⇀ Coin) {(a , c) : A × Coin}
+    → a ∉ dom m → getCoin (m ∪ˡ ❴ (a , c) ❵ᵐ) ≡ getCoin m + c
+  ∪ˡsingleton∉dom m {(a , c)} a∉dom =
+    begin
+    getCoin (m ∪ˡ ❴ a , c ❵ᵐ)
+      ≡⟨ indexedSumᵛ'-∪ m ❴ a , c ❵ᵐ
+         ( λ x y → a∉dom (subst (_∈ dom m) (from ∈-dom-singleton-pair y) x) ) ⟩
+    getCoin m + getCoin ❴ a , c ❵ᵐ
+      ≡⟨ cong (getCoin m +_) getCoin-singleton ⟩
+    getCoin m + c
+      ∎
+    where open Equivalence ; open ≡-Reasoning
+
+  -- The case-split corollary specialised to a zero-valued singleton.
+  ∪ˡsingleton0≡ : (m : A ⇀ Coin) {a : A} → getCoin (m ∪ˡ ❴ (a , 0) ❵ᵐ) ≡ getCoin m
+  ∪ˡsingleton0≡ m {a} with a ∈? dom m
+  ... | yes a∈dom = ∪ˡsingleton∈dom m a∈dom
+  ... | no a∉dom = trans (∪ˡsingleton∉dom m a∉dom) (+-identityʳ (getCoin m))
+
+
+  open import Data.List.Membership.Propositional.Properties using (∈-deduplicate⁻)
+
+  sumConstZero : {X : ℙ A} → getCoin (constMap X 0) ≡ 0
+  sumConstZero {X} = indexedSumL-proj₂-zero (deduplicate _≟_ l) all-zero-dedup
+    where
+    open Equivalence
+
+    fin : finite (mapˢ (_, 0) X)
+    fin = finiteness (mapˢ (_, 0) X)
+
+    l : List (A × Coin)
+    l   = fin .proj₁
+
+    h : ∀ {a} → a ∈ (mapˢ (_, 0) X) ⇔ a ∈ˡ l
+    h   = fin .proj₂
+
+    all-zero : ∀ {x} → x ∈ˡ l → proj₂ x ≡ 0
+    all-zero x∈l with from ∈-map (from h x∈l)
+    ... | (a , refl , _) = refl
+
+    all-zero-dedup : ∀ {x} → x ∈ˡ deduplicate _≟_ l → proj₂ x ≡ 0
+    all-zero-dedup x∈dedup = all-zero (∈-deduplicate⁻ (DecEq._≟_ DecEq-×′) l x∈dedup)
+
+opaque
+  unfolding setToList List-Model
+
+  setToList-∈ : ∀ {A : Type} {a : A} {X : ℙ A} → a ∈ˡ setToList X → a ∈ X
+  setToList-∈ = id
 ```