Skip to content

Commit dd49253

Browse files
claudewilliamdemeo
claude
authored and
williamdemeo
committed
Conway PoV: discharge map/coin assumptions via new Ledger.Prelude lemmas
Split out of the LEDGER-pov work (#1203): this Conway-era properties cleanup is independent of the Dijkstra PoV proof and belongs in its own PR. - Add reusable coin/map lemmas to `Ledger.Prelude`: `getCoin-singleton`, `getCoin-cong`, `indexedSumᵛ'-∪`, `res-decomp`, `∪ˡsingleton∈dom`, `∪ˡsingleton∉dom`, `∪ˡsingleton0≡`, `sumConstZero`, `indexedSumL-proj₂-zero`, `setToList-∈`; relocate `≡ᵉ-getCoin` into the `⦃ DecEq A ⦄` module. - Drop the now-provable assumption parameters from the Conway PoV proofs, using the Prelude lemmas instead: - `Certs/Properties/PoV`: keep only `≡ᵉ-getCoinˢ'`. - `Certs/Properties/PoVLemmas`: remove the local `∪ˡsingleton*`/`getCoin-singleton` helpers and the `indexedSumᵛ'-∪` assumption module; qualify `IsEquivalence` as `Eq`. - `Ledger/Properties/PoV`: keep only `≡ᵉ-getCoinˢ`. - `Conformance/Properties`: drop the `indexedSum-∪⁺-hom` parameter. - `Utxo/Properties/GenMinSpend`: use the hoisted `getCoin-singleton`. No spec-semantic change (proof refactor only), so no CHANGELOG entry. `Ledger.Prelude` typechecks under Agda 2.8.0 via the project flake; the Conway files are their 1187 versions (which typecheck) and depend only on the hoisted lemmas. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01We2YdXX2ozJAdAbCrRwi6r
1 parent 42bf875 commit dd49253

6 files changed

Lines changed: 149 additions & 112 deletions

File tree

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

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -124,8 +124,6 @@ module _ (s : ChainState) where
124124
-- Transaction properties
125125
126126
module _ {slot} {tx} (let txb = body tx) (valid : validTxIn₂ s slot tx)
127-
(indexedSum-∪⁺-hom : ∀ {A V : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq V ⦄ ⦃ mon : CommutativeMonoid 0ℓ 0ℓ V ⦄
128-
→ (d₁ d₂ : A ⇀ V) → indexedSumᵛ' id (d₁ ∪⁺ d₂) ≡ indexedSumᵛ' id d₁ ◇ indexedSumᵛ' id d₂)
129127
(indexedSum-⊆ : ∀ {A : Type} ⦃ _ : DecEq A ⦄ (d d' : A ⇀ ℕ) → d ˢ ⊆ d' ˢ
130128
→ indexedSumᵛ' id d ≤ indexedSumᵛ' id d') -- technically we could use an ordered monoid instead of ℕ
131129
where

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

Lines changed: 5 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -46,19 +46,12 @@ private variable
4646
instance
4747
_ = +-0-monoid
4848
49-
module Certs-PoV ( indexedSumᵛ'-∪' : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin)
50-
→ disjoint (dom m) (dom m')
51-
→ getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m' )
52-
-- TODO: prove some or all of the following assumptions, used in roof of `CERTBASE-pov`.
53-
( sumConstZero' : {A : Type} ⦃ _ : DecEq A ⦄ {X : ℙ A} → getCoin (constMap X 0) ≡ 0 )
54-
( res-decomp' : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin)
55-
→ (m ∪ˡ m')ˢ ≡ᵉ (m ∪ˡ (m' ∣ dom (m ˢ) ᶜ))ˢ )
56-
( getCoin-cong' : {A : Type} ⦃ _ : DecEq A ⦄ (s : A ⇀ Coin) (s' : ℙ (A × Coin)) → s ˢ ≡ᵉ s'
57-
→ indexedSum' proj₂ (s ˢ) ≡ indexedSum' proj₂ s' )
58-
( ≡ᵉ-getCoinˢ' : {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'}
59-
→ InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s )
49+
module Certs-PoV
50+
-- TODO: prove the following assumption, used in roof of `CERTBASE-pov`.
51+
( ≡ᵉ-getCoinˢ' : {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'}
52+
→ InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s )
6053
where
61-
open Certs-Pov-lemmas indexedSumᵛ'-∪' sumConstZero' res-decomp' getCoin-cong' ≡ᵉ-getCoinˢ'
54+
open Certs-Pov-lemmas ≡ᵉ-getCoinˢ'
6255
```
6356
-->
6457

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

Lines changed: 46 additions & 80 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ open import Axiom.Set.Properties th
2323
open import Algebra using (CommutativeMonoid)
2424
open import Data.Maybe.Properties
2525
open import Data.Nat.Properties using (+-0-monoid; +-0-commutativeMonoid; +-identityʳ; +-identityˡ)
26-
open import Relation.Binary using (IsEquivalence)
26+
import Relation.Binary as Eq using (IsEquivalence)
2727
open import Relation.Nullary.Decidable
2828
open import Tactic.ReduceDec
2929
@@ -40,35 +40,7 @@ private variable
4040
instance
4141
_ = +-0-monoid
4242
43-
getCoin-singleton : ⦃ _ : DecEq A ⦄ {(a , c) : A × Coin} → indexedSumᵛ' id ❴ (a , c) ❵ ≡ c
44-
getCoin-singleton = indexedSum-singleton' {M = Coin} (finiteness _)
45-
46-
∪ˡsingleton∈dom : ⦃ _ : DecEq A ⦄ (m : A ⇀ Coin) {(a , c) : A × Coin}
47-
→ a ∈ dom m → getCoin (m ∪ˡ ❴ (a , c) ❵ᵐ) ≡ getCoin m
48-
∪ˡsingleton∈dom m {(a , c)} a∈dom = ≡ᵉ-getCoin (m ∪ˡ ❴ (a , c) ❵) m (singleton-∈-∪ˡ {m = m} a∈dom)
49-
50-
module _ ( indexedSumᵛ'-∪ : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin)
51-
→ disjoint (dom m) (dom m')
52-
→ getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m' )
53-
where
54-
open ≡-Reasoning
55-
open Equivalence
56-
57-
∪ˡsingleton∉dom : ⦃ _ : DecEq A ⦄ (m : A ⇀ Coin) {(a , c) : A × Coin}
58-
→ a ∉ dom m → getCoin (m ∪ˡ ❴ (a , c) ❵ᵐ) ≡ getCoin m + c
59-
∪ˡsingleton∉dom m {(a , c)} a∉dom = begin
60-
getCoin (m ∪ˡ ❴ a , c ❵ᵐ)
61-
≡⟨ indexedSumᵛ'-∪ m ❴ a , c ❵ᵐ
62-
( λ x y → a∉dom (subst (_∈ dom m) (from ∈-dom-singleton-pair y) x) ) ⟩
63-
getCoin m + getCoin ❴ a , c ❵ᵐ
64-
≡⟨ cong (getCoin m +_) getCoin-singleton ⟩
65-
getCoin m + c
66-
∎
67-
68-
∪ˡsingleton0≡ : ⦃ _ : DecEq A ⦄ → (m : A ⇀ Coin) {a : A} → getCoin (m ∪ˡ ❴ (a , 0) ❵ᵐ) ≡ getCoin m
69-
∪ˡsingleton0≡ m {a} with a ∈? dom m
70-
... | yes a∈dom = ∪ˡsingleton∈dom m a∈dom
71-
... | no a∉dom = trans (∪ˡsingleton∉dom m a∉dom) (+-identityʳ (getCoin m))
43+
open ≡-Reasoning
7244
```
7345
-->
7446

@@ -83,61 +55,55 @@ some `dcert`{.AgdaBound} : `DCert`{.AgdaDatatype}. Then,
8355
*Formally*.
8456

8557
```agda
86-
CERT-pov : {Γ : CertEnv} {s s' : CertState}
87-
→ Γ ⊢ s ⇀⦇ dCert ,CERT⦈ s'
88-
→ getCoin s ≡ getCoin s'
58+
CERT-pov : {Γ : CertEnv} {s s' : CertState}
59+
→ Γ ⊢ s ⇀⦇ dCert ,CERT⦈ s' → getCoin s ≡ getCoin s'
8960
```
9061

9162
*Proof*. (Click the "Show more Agda" button to reveal the proof.)
9263

9364
<!--
9465
```agda
95-
CERT-pov (CERT-deleg (DELEG-delegate {rwds = rwds} _)) = sym (∪ˡsingleton0≡ rwds)
96-
CERT-pov (CERT-deleg (DELEG-reg {rwds = rwds} _)) = sym (∪ˡsingleton0≡ rwds)
97-
CERT-pov {s = ⟦ _ , stᵖ , stᵍ ⟧ᶜˢ}{⟦ _ , stᵖ' , stᵍ' ⟧ᶜˢ}
98-
(CERT-deleg (DELEG-dereg {c = c} {rwds} {vDelegs = vDelegs}{sDelegs} x)) = begin
99-
getCoin ⟦ ⟦ vDelegs , sDelegs , rwds ⟧ , stᵖ , stᵍ ⟧
100-
≡˘⟨ ≡ᵉ-getCoin rwds-∪ˡ-decomp rwds
101-
( ≡ᵉ.trans rwds-∪ˡ-∪ (≡ᵉ.trans ∪-sym (res-ex-∪ Dec-∈-singleton)) ) ⟩
102-
getCoin rwds-∪ˡ-decomp
103-
≡⟨ ≡ᵉ-getCoin rwds-∪ˡ-decomp ((rwds ∣ ❴ c ❵ ᶜ) ∪ˡ ❴ (c , 0) ❵ᵐ) rwds-∪ˡ≡sing-∪ˡ ⟩
104-
getCoin ((rwds ∣ ❴ c ❵ ᶜ) ∪ˡ ❴ (c , 0) ❵ᵐ )
105-
≡⟨ ∪ˡsingleton0≡ (rwds ∣ ❴ c ❵ ᶜ) ⟩
106-
getCoin ⟦ ⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ ⟧ , stᵖ' , stᵍ' ⟧
107-
∎
108-
where
109-
module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin})
110-
rwds-∪ˡ-decomp = (rwds ∣ ❴ c ❵ ᶜ) ∪ˡ (rwds ∣ ❴ c ❵ )
111-
112-
rwds-∪ˡ-∪ : rwds-∪ˡ-decomp ˢ ≡ᵉ (rwds ∣ ❴ c ❵ ᶜ)ˢ ∪ (rwds ∣ ❴ c ❵)ˢ
113-
rwds-∪ˡ-∪ = disjoint-∪ˡ-∪ (disjoint-sym res-ex-disjoint)
114-
115-
disj : disjoint (dom ((rwds ∣ ❴ c ❵ˢ ᶜ) ˢ)) (dom (❴ c , 0 ❵ᵐ ˢ))
116-
disj {a} a∈res a∈dom = res-comp-dom a∈res (dom-single→single a∈dom)
117-
118-
rwds-∪ˡ≡sing-∪ˡ : rwds-∪ˡ-decomp ˢ ≡ᵉ ((rwds ∣ ❴ c ❵ ᶜ) ∪ˡ ❴ (c , 0) ❵ᵐ )ˢ
119-
rwds-∪ˡ≡sing-∪ˡ = ≡ᵉ.trans rwds-∪ˡ-∪
120-
( ≡ᵉ.trans (∪-cong ≡ᵉ.refl (res-singleton'{m = rwds} x))
121-
(≡ᵉ.sym $ disjoint-∪ˡ-∪ disj) )
122-
CERT-pov (CERT-pool x) = refl
123-
CERT-pov (CERT-vdel x) = refl
124-
125-
injOn : (wdls : Withdrawals)
126-
→ ∀[ a ∈ dom (wdls ˢ) ] NetworkIdOf a ≡ NetworkId
127-
→ InjectiveOn (dom (wdls ˢ)) RewardAddress.stake
128-
injOn _ h {record { stake = stakex }} {record { stake = stakey }} x∈ y∈ refl =
129-
cong (λ u → record { net = u ; stake = stakex }) (trans (h x∈) (sym (h y∈)))
130-
131-
module Certs-Pov-lemmas
132-
-- TODO: prove some or all of the following assumptions, used in roof of `CERTBASE-pov`.
133-
( sumConstZero : {A : Type} ⦃ _ : DecEq A ⦄ {X : ℙ A} → getCoin (constMap X 0) ≡ 0 )
134-
( res-decomp : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin)
135-
→ (m ∪ˡ m')ˢ ≡ᵉ (m ∪ˡ (m' ∣ dom (m ˢ) ᶜ))ˢ )
136-
( getCoin-cong : {A : Type} ⦃ _ : DecEq A ⦄ (s : A ⇀ Coin) (s' : ℙ (A × Coin)) → s ˢ ≡ᵉ s'
137-
→ indexedSum' proj₂ (s ˢ) ≡ indexedSum' proj₂ s' )
138-
( ≡ᵉ-getCoinˢ : {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'}
139-
→ InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s )
140-
where
66+
CERT-pov (CERT-deleg (DELEG-delegate {rwds = rwds} _)) = sym (∪ˡsingleton0≡ rwds)
67+
CERT-pov (CERT-deleg (DELEG-reg {rwds = rwds} _)) = sym (∪ˡsingleton0≡ rwds)
68+
CERT-pov {s = ⟦ _ , stᵖ , stᵍ ⟧ᶜˢ}{⟦ _ , stᵖ' , stᵍ' ⟧ᶜˢ}
69+
(CERT-deleg (DELEG-dereg {c = c} {rwds} {vDelegs = vDelegs}{sDelegs} x)) = begin
70+
getCoin ⟦ ⟦ vDelegs , sDelegs , rwds ⟧ , stᵖ , stᵍ ⟧
71+
≡˘⟨ ≡ᵉ-getCoin rwds-∪ˡ-decomp rwds
72+
( ≡ᵉ.trans rwds-∪ˡ-∪ (≡ᵉ.trans ∪-sym (res-ex-∪ Dec-∈-singleton)) ) ⟩
73+
getCoin rwds-∪ˡ-decomp
74+
≡⟨ ≡ᵉ-getCoin rwds-∪ˡ-decomp ((rwds ∣ ❴ c ❵ ᶜ) ∪ˡ ❴ (c , 0) ❵ᵐ) rwds-∪ˡ≡sing-∪ˡ ⟩
75+
getCoin ((rwds ∣ ❴ c ❵ ᶜ) ∪ˡ ❴ (c , 0) ❵ᵐ )
76+
≡⟨ ∪ˡsingleton0≡ (rwds ∣ ❴ c ❵ ᶜ) ⟩
77+
getCoin ⟦ ⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ ⟧ , stᵖ' , stᵍ' ⟧
78+
∎
79+
where
80+
module ≡ᵉ = Eq.IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin})
81+
rwds-∪ˡ-decomp = (rwds ∣ ❴ c ❵ ᶜ) ∪ˡ (rwds ∣ ❴ c ❵ )
82+
83+
rwds-∪ˡ-∪ : rwds-∪ˡ-decomp ˢ ≡ᵉ (rwds ∣ ❴ c ❵ ᶜ)ˢ ∪ (rwds ∣ ❴ c ❵)ˢ
84+
rwds-∪ˡ-∪ = disjoint-∪ˡ-∪ (disjoint-sym res-ex-disjoint)
85+
86+
disj : disjoint (dom ((rwds ∣ ❴ c ❵ˢ ᶜ) ˢ)) (dom (❴ c , 0 ❵ᵐ ˢ))
87+
disj {a} a∈res a∈dom = res-comp-dom a∈res (dom-single→single a∈dom)
88+
89+
rwds-∪ˡ≡sing-∪ˡ : rwds-∪ˡ-decomp ˢ ≡ᵉ ((rwds ∣ ❴ c ❵ ᶜ) ∪ˡ ❴ (c , 0) ❵ᵐ )ˢ
90+
rwds-∪ˡ≡sing-∪ˡ = ≡ᵉ.trans rwds-∪ˡ-∪
91+
( ≡ᵉ.trans (∪-cong ≡ᵉ.refl (res-singleton'{m = rwds} x))
92+
(≡ᵉ.sym $ disjoint-∪ˡ-∪ disj) )
93+
CERT-pov (CERT-pool x) = refl
94+
CERT-pov (CERT-vdel x) = refl
95+
96+
injOn : (wdls : Withdrawals)
97+
→ ∀[ a ∈ dom (wdls ˢ) ] NetworkIdOf a ≡ NetworkId
98+
→ InjectiveOn (dom (wdls ˢ)) RewardAddress.stake
99+
injOn _ h {record { stake = stakex }} {record { stake = stakey }} x∈ y∈ refl =
100+
cong (λ u → record { net = u ; stake = stakex }) (trans (h x∈) (sym (h y∈)))
101+
102+
module Certs-Pov-lemmas
103+
-- TODO: prove the following assumption, used in roof of `CERTBASE-pov`.
104+
( ≡ᵉ-getCoinˢ : {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'}
105+
→ InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s )
106+
where
141107
```
142108
-->
143109

@@ -175,7 +141,7 @@ value of the withdrawals in `Γ`{.AgdaBound}. In other terms,
175141
let
176142
open DState (dState cs )
177143
open DState (dState cs') renaming (rewards to rewards')
178-
module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin})
144+
module ≡ᵉ = Eq.IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin})
179145
wdrlsCC = mapˢ (map₁ RewardAddress.stake) (wdrls ˢ)
180146
zeroMap = constMap (mapˢ RewardAddress.stake (dom wdrls)) 0
181147
rwds-∪ˡ-decomp = (rewards ∣ dom wdrlsCC ᶜ) ∪ˡ (rewards ∣ dom wdrlsCC)

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

Lines changed: 5 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -38,15 +38,9 @@ instance
3838
3939
module _
4040
(tx : Tx) (let open Tx tx; open TxBody body)
41-
( indexedSumᵛ'-∪ : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin)
42-
→ disjoint (dom m) (dom m') → getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m' )
43-
( sumConstZero : {A : Type} ⦃ _ : DecEq A ⦄ {X : ℙ A} → getCoin (constMap X 0) ≡ 0 )
44-
( res-decomp : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin)
45-
→ (m ∪ˡ m')ˢ ≡ᵉ (m ∪ˡ (m' ∣ dom (m ˢ) ᶜ))ˢ )
46-
( getCoin-cong : {A : Type} ⦃ _ : DecEq A ⦄ (s : A ⇀ Coin) (s' : ℙ (A × Coin)) → s ˢ ≡ᵉ s'
47-
→ indexedSum' proj₂ (s ˢ) ≡ indexedSum' proj₂ s' )
48-
( ≡ᵉ-getCoinˢ : {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'}
49-
→ InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s )
41+
-- TODO: prove the following assumption, used in roof of `CERTBASE-pov`.
42+
( ≡ᵉ-getCoinˢ : {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'}
43+
→ InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s )
5044
where
5145
5246
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,
8478
open LState s' renaming (utxoSt to utxoSt'; govSt to govSt'; certState to certState')
8579
open CertState certState'
8680
open ≡-Reasoning
87-
open Certs-PoV indexedSumᵛ'-∪ sumConstZero res-decomp getCoin-cong ≡ᵉ-getCoinˢ
88-
zeroMap = constMap (mapˢ RewardAddress.stake (dom txWithdrawals)) 0
81+
open Certs-PoV ≡ᵉ-getCoinˢ
82+
zeroMap = constMap (mapˢ RewardAddress.stake (dom txWithdrawals)) 0
8983
in
9084
begin
9185
getCoin utxoSt + getCoin certState

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

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -51,9 +51,6 @@ coin∅ = begin
5151
0 ∎
5252
where open Prelude.≡-Reasoning
5353
54-
getCoin-singleton : ((dp , c) : DepositPurpose × Coin) → indexedSumᵛ' id ❴ (dp , c) ❵ ≡ c
55-
getCoin-singleton _ = indexedSum-singleton' {A = DepositPurpose × Coin} {f = proj₂} (finiteness _)
56-
5754
module _ -- ASSUMPTION --
5855
(gc-hom : (d₁ d₂ : Deposits) → getCoin (d₁ ∪⁺ d₂) ≡ getCoin d₁ + getCoin d₂)
5956
where
@@ -63,7 +60,7 @@ module _ -- ASSUMPTION --
6360
getCoin (deps ∪⁺ ❴ (dp , c) ❵)
6461
≡⟨ gc-hom deps ❴ (dp , c) ❵ ⟩
6562
getCoin deps + getCoin{A = Deposits} ❴ (dp , c) ❵
66-
≡⟨ cong (getCoin deps +_) (getCoin-singleton (dp , c)) ⟩
63+
≡⟨ cong (getCoin deps +_) getCoin-singleton ⟩
6764
getCoin deps + c
6865
∎
6966
where open Prelude.≡-Reasoning

‎src/Ledger/Prelude.lagda.md‎

Lines changed: 92 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -48,16 +48,14 @@ open import abstract-set-theory.Axiom.Set.Map.Extra public
4848
4949
import Data.Integer as ℤ
5050
open import Data.Integer using (0ℤ) public
51+
open import Data.Nat.Properties using (+-identityʳ)
5152
import Data.Rational as ℚ
5253
open import Data.Rational using (ℚ)
5354
5455
dec-de-morgan : ∀{P Q : Type} → ⦃ P ⁇ ⦄ → ¬ (P × Q) → ¬ P ⊎ ¬ Q
5556
dec-de-morgan ⦃ ⁇ no ¬p ⦄ ¬pq = inj₁ ¬p
5657
dec-de-morgan ⦃ ⁇ yes p ⦄ ¬pq = inj₂ λ q → ¬pq (p , q)
5758
58-
≡ᵉ-getCoin : ∀ {A} → ⦃ _ : DecEq A ⦄ → (s s' : A ⇀ Coin) → s ˢ ≡ᵉ s' ˢ → getCoin s ≡ getCoin s'
59-
≡ᵉ-getCoin {A} ⦃ decEqA ⦄ s s' s≡s' = indexedSumᵛ'-cong {C = Coin} {x = s} {y = s'} s≡s'
60-
6159
setToMap : ∀ {A B : Type} → ⦃ DecEq A ⦄ → ℙ (A × B) → A ⇀ B
6260
setToMap = fromListᵐ ∘ setToList
6361
@@ -98,4 +96,95 @@ Is-∅ X = Is-[] (setToList X)
9896
9997
concatMapˡ : {A B : Type} → (A → ℙ B) → List A → ℙ B
10098
concatMapˡ f as = proj₁ $ unions (fromList (map f as))
99+
100+
indexedSumL-proj₂-zero : ∀ {A : Type} (l : List (A × Coin))
101+
→ (∀ {x} → x ∈ˡ l → proj₂ x ≡ 0)
102+
→ indexedSumL {M = Coin} proj₂ l ≡ 0
103+
indexedSumL-proj₂-zero [] _ = refl
104+
indexedSumL-proj₂-zero ((a , v) ∷ xs) all-zero =
105+
trans (cong (_+ indexedSumL proj₂ xs) (all-zero (Prelude.Init.here refl)))
106+
(indexedSumL-proj₂-zero xs (all-zero ∘ Prelude.Init.there))
107+
108+
module _ {A : Type} ⦃ _ : DecEq A ⦄ where
109+
110+
-- A coin singleton has the coin you expect.
111+
getCoin-singleton : {(a , c) : A × Coin} → indexedSumᵛ' id ❴ (a , c) ❵ ≡ c
112+
getCoin-singleton = indexedSum-singleton' {M = Coin} (finiteness _)
113+
114+
≡ᵉ-getCoin : (s s' : A ⇀ Coin) → s ˢ ≡ᵉ s' ˢ → getCoin s ≡ getCoin s'
115+
≡ᵉ-getCoin s s' s≡s' = indexedSumᵛ'-cong {C = Coin} {x = s} {y = s'} s≡s'
116+
117+
getCoin-cong : (s : A ⇀ Coin) (s' : ℙ (A × Coin))
118+
→ s ˢ ≡ᵉ s' → indexedSum' proj₂ (s ˢ) ≡ indexedSum' proj₂ s'
119+
getCoin-cong s s' eq = indexedSum-cong {f = proj₂} {x = (s ˢ) ᶠˢ} {y = s' ᶠˢ} eq
120+
121+
indexedSumᵛ'-∪ : (m m' : A ⇀ Coin) → disjoint (dom m) (dom m')
122+
→ getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m'
123+
indexedSumᵛ'-∪ m m' disj =
124+
trans (indexedSumᵐ-∪ˡ-∪ˡᶠ m m')
125+
(indexedSumᵐ-∪ {X = m ᶠᵐ} {m' ᶠᵐ} {f = proj₂} disj)
126+
127+
open import Axiom.Set.Properties th
128+
open import Relation.Binary using (IsEquivalence)
129+
130+
res-decomp : (m m' : A ⇀ Coin) → (m ∪ˡ m')ˢ ≡ᵉ (m ∪ˡ (m' ∣ dom (m ˢ) ᶜ))ˢ
131+
res-decomp m m' = ∪-cong (≡ᵉ.refl {x = m ˢ}) (≡ᵉ.sym (filterᵐ-idem {m = m'}))
132+
where module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence {A × Coin})
133+
134+
-- If a is already in domain of m, left-biased union with singleton at a
135+
-- leaves total unchanged (existing entry wins).
136+
∪ˡsingleton∈dom : (m : A ⇀ Coin) {(a , c) : A × Coin}
137+
→ a ∈ dom m → getCoin (m ∪ˡ ❴ (a , c) ❵ᵐ) ≡ getCoin m
138+
∪ˡsingleton∈dom m {(a , c)} a∈dom =
139+
≡ᵉ-getCoin (m ∪ˡ ❴ (a , c) ❵) m (singleton-∈-∪ˡ {m = m} a∈dom)
140+
141+
-- If a is *not* in domain of m, left-biased union with singleton adds cleanly.
142+
∪ˡsingleton∉dom : (m : A ⇀ Coin) {(a , c) : A × Coin}
143+
→ a ∉ dom m → getCoin (m ∪ˡ ❴ (a , c) ❵ᵐ) ≡ getCoin m + c
144+
∪ˡsingleton∉dom m {(a , c)} a∉dom =
145+
begin
146+
getCoin (m ∪ˡ ❴ a , c ❵ᵐ)
147+
≡⟨ indexedSumᵛ'-∪ m ❴ a , c ❵ᵐ
148+
( λ x y → a∉dom (subst (_∈ dom m) (from ∈-dom-singleton-pair y) x) ) ⟩
149+
getCoin m + getCoin ❴ a , c ❵ᵐ
150+
≡⟨ cong (getCoin m +_) getCoin-singleton ⟩
151+
getCoin m + c
152+
∎
153+
where open Equivalence ; open ≡-Reasoning
154+
155+
-- The case-split corollary specialised to a zero-valued singleton.
156+
∪ˡsingleton0≡ : (m : A ⇀ Coin) {a : A} → getCoin (m ∪ˡ ❴ (a , 0) ❵ᵐ) ≡ getCoin m
157+
∪ˡsingleton0≡ m {a} with a ∈? dom m
158+
... | yes a∈dom = ∪ˡsingleton∈dom m a∈dom
159+
... | no a∉dom = trans (∪ˡsingleton∉dom m a∉dom) (+-identityʳ (getCoin m))
160+
161+
162+
open import Data.List.Membership.Propositional.Properties using (∈-deduplicate⁻)
163+
164+
sumConstZero : {X : ℙ A} → getCoin (constMap X 0) ≡ 0
165+
sumConstZero {X} = indexedSumL-proj₂-zero (deduplicate _≟_ l) all-zero-dedup
166+
where
167+
open Equivalence
168+
169+
fin : finite (mapˢ (_, 0) X)
170+
fin = finiteness (mapˢ (_, 0) X)
171+
172+
l : List (A × Coin)
173+
l = fin .proj₁
174+
175+
h : ∀ {a} → a ∈ (mapˢ (_, 0) X) ⇔ a ∈ˡ l
176+
h = fin .proj₂
177+
178+
all-zero : ∀ {x} → x ∈ˡ l → proj₂ x ≡ 0
179+
all-zero x∈l with from ∈-map (from h x∈l)
180+
... | (a , refl , _) = refl
181+
182+
all-zero-dedup : ∀ {x} → x ∈ˡ deduplicate _≟_ l → proj₂ x ≡ 0
183+
all-zero-dedup x∈dedup = all-zero (∈-deduplicate⁻ (DecEq._≟_ DecEq-×′) l x∈dedup)
184+
185+
opaque
186+
unfolding setToList List-Model
187+
188+
setToList-∈ : ∀ {A : Type} {a : A} {X : ℙ A} → a ∈ˡ setToList X → a ∈ X
189+
setToList-∈ = id
101190
```

0 commit comments

Comments
 (0)