indexedSumᵛ'-∪ and sumConstZero have proofs!

There were unresolved proof obligations from Conway.

Author: williamdemeo

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,16 @@ 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' )
+module Certs-PoV
     -- 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
-    open Certs-Pov-lemmas indexedSumᵛ'-∪' sumConstZero' res-decomp' getCoin-cong' ≡ᵉ-getCoinˢ'
+    open Certs-Pov-lemmas res-decomp' getCoin-cong' ≡ᵉ-getCoinˢ'
 ```
 -->
 

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

@@ -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,59 @@ 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 ≡ᵉ = 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`.
+  ( 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
 ```
 -->
 

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

@@ -38,9 +38,6 @@ 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'
@@ -84,7 +81,7 @@ 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ˢ
+      open Certs-PoV res-decomp  getCoin-cong ≡ᵉ-getCoinˢ
       zeroMap    = constMap (mapˢ RewardAddress.stake (dom txWithdrawals)) 0
     in
     begin

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/Dijkstra/Specification/Certs/Properties/ApplyWithdrawalsPoV.lagda.md

@@ -68,15 +68,13 @@ We parameterize over the standard finite-map sum lemmas (same pattern as Conway)
 <!--
 ```agda
 module ApplyWithdrawals-PoV
-  ( indexedSumᵛ'-∪ :  {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin)
-                      → disjoint (dom m) (dom m')
-                      → getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m' )
   ( getCoin-cong :  {A : Type} ⦃ _ : DecEq A ⦄ (s : A ⇀ Coin) (s' : ℙ (A × Coin))
                   → s ˢ ≡ᵉ s' → indexedSum' proj₂ (s ˢ) ≡ indexedSum' proj₂ s' )
   where
   open ≡-Reasoning
   open Equivalence
   module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin})
+
 ```
 -->
 
@@ -95,21 +93,58 @@ applying a single withdrawal decreases the total by exactly `amt`.
 
 <!--
 ```agda
-  applyOne-pov acc addr amt bal lookup-eq amt≤bal = {!!}
-    -- Proof sketch:
-    --
-    -- getCoin acc
-    --   ≡ getCoin (acc ∣ ❴ c ❵ ᶜ) + getCoin (acc ∣ ❴ c ❵)
-    --       -- by: acc ≡ᵉ (acc ∣ ❴ c ❵ ᶜ) ∪ (acc ∣ ❴ c ❵), then indexedSumᵛ'-∪
-    --   ≡ getCoin (acc ∣ ❴ c ❵ ᶜ) + bal
-    --       -- by: getCoin-cong on (acc ∣ ❴ c ❵) ≡ᵉ ❴ c , bal ❵ (from lookup-eq)
-    --   ≡ getCoin (acc ∣ ❴ c ❵ ᶜ) + (bal ∸ amt + amt)
-    --       -- by: m∸n+n≡m amt≤bal
-    --   ≡ (bal ∸ amt) + getCoin (acc ∣ ❴ c ❵ ᶜ) + amt
-    --       -- by: +-comm, +-assoc
-    --   ≡ getCoin (❴ c , bal ∸ amt ❵ ∪ˡ (acc ∣ ❴ c ❵ ᶜ)) + amt
-    --       -- by: indexedSumᵛ'-∪ (disjoint since c ∉ dom (acc ∣ ❴ c ❵ ᶜ))
-    -- where c = stake addr
+  applyOne-pov acc addr amt bal lookup-eq amt≤bal = trans acc≡decomp decomp≡goal
+    where
+    c : Credential
+    c = stake addr
+
+    ξ : acc ˢ ≡ᵉ (acc ∣ ❴ c ❵) ˢ ∪ (acc ∣ ❴ c ❵ ᶜ) ˢ
+    ξ = IsEquivalence.sym ≡ᵉ-isEquivalence (res-ex-∪ Dec-∈-singleton)
+
+    c∈acc : (c , bal) ∈ acc ˢ
+    c∈acc with c ∈? dom (acc ˢ)
+    ... | yes c∈dom =
+      subst (λ v → (c , v) ∈ acc ˢ)
+            (just-injective lookup-eq)    -- lookupᵐ acc c ≡ bal
+            (lookupᵐ-∈ acc c c∈dom)      -- (c , lookupᵐ acc c) ∈ acc ˢ
+    ... | no c∉dom = case lookup-eq of λ ()
+      -- lookupᵐ? resolves to nothing, so nothing ≡ just bal is absurd
+
+    acc∣c≡bal : getCoin (acc ∣ ❴ c ❵) ≡ bal
+    acc∣c≡bal =
+      trans (getCoin-cong (acc ∣ ❴ c ❵) ❴ (c , bal) ❵ (res-singleton' c∈acc))
+            getCoin-singleton
+
+    c∉dom-compl : c ∉ dom ((acc ∣ ❴ c ❵ ᶜ) ˢ)
+    c∉dom-compl c∈ = res-comp-dom c∈ (∈-singleton .Equivalence.to refl)
+
+
+    decomp : acc ≡ (acc ∣ ❴ c ❵ ᶜ) ∪ˡ (acc ∣ ❴ c ❵)
+    decomp = ?
+
+    acc≡decomp : getCoin acc ≡ getCoin decomp
+    acc≡decomp =
+      ≡ᵉ-getCoin decomp acc
+        ( ≡ᵉ.trans (disjoint-∪ˡ-∪ (disjoint-sym res-ex-disjoint))
+                   ( ≡ᵉ.trans ∪-sym (res-ex-∪ Dec-∈-singleton)) ) ⟩
+
+    decomp≡goal : getCoin decomp ≡ getCoin (acc ∣ ❴ c ❵ ᶜ) + getCoin (acc ∣ ❴ c ❵)
+    decomp≡goal = indexedSumᵛ'-∪ (acc ∣ ❴ c ❵ ᶜ) (acc ∣ ❴ c ❵) (disjoint-sym res-ex-disjoint) ⟩
+
+    -- Goal : getCoin acc ≡ getCoin (❴ c , bal ∸ amt ❵ᵐ ∪ˡ (acc ∣ ❴ c ❵ˢ ᶜ)) + amt
+    -- Goal = begin
+    --   getCoin acc
+    --     ≡⟨ {!!} ⟩        -- by: acc ≡ᵉ (acc ∣ ❴ c ❵ ᶜ) ∪ (acc ∣ ❴ c ❵), then indexedSumᵛ'-∪
+    --   getCoin (acc ∣ ❴ c ❵ ᶜ) + getCoin (acc ∣ ❴ c ❵)
+    --     ≡⟨ {!!} ⟩        -- by: getCoin-cong on (acc ∣ ❴ c ❵) ≡ᵉ ❴ c , bal ❵ (from lookup-eq)
+    --   getCoin (acc ∣ ❴ c ❵ ᶜ) + bal
+    --     ≡⟨ {!!} ⟩        -- by: m∸n+n≡m amt≤bal
+    --   getCoin (acc ∣ ❴ c ❵ ᶜ) + (bal ∸ amt + amt)
+    --     ≡⟨ {!!} ⟩        -- by: +-comm, +-assoc
+    --   (bal ∸ amt) + getCoin (acc ∣ ❴ c ❵ ᶜ) + amt
+    --     ≡⟨ {!!} ⟩        -- by: indexedSumᵛ'-∪ (disjoint since c ∉ dom (acc ∣ ❴ c ❵ ᶜ))
+    --   getCoin (❴ c , bal ∸ amt ❵ᵐ ∪ˡ (acc ∣ ❴ c ❵ˢ ᶜ)) + amt
+    --   ∎
 ```
 -->
 

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

@@ -60,5 +60,5 @@ module Certs-PoV
 ```agda
     CERTS-pov {Γ = Γ} validNetId (run (pre-cert , certs)) =
       trans  (PRE-CERT-pov validNetId pre-cert)
-             (cong (_+ getCoin (WithdrawalsOf Γ)) {!!}) -- (sts-pov certs))
+             (cong (_+ getCoin (WithdrawalsOf Γ)) (sts-pov indexedSumᵛ'-∪' certs))
 ```