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

[williamdemeo]

Description

Splits the Conway-era PoV proof cleanup out of the LEDGER-pov work (#1203), where it didn't belong. This change is independent of the Dijkstra preservation-of-value proof: it proves a handful of reusable coin/map facts in Ledger.Prelude and uses them to discharge assumption parameters that the Conway PoV proofs previously carried.

What changes

Ledger.Prelude — add reusable coin/map lemmas (pure additions):
getCoin-singleton, getCoin-cong, indexedSumᵛ'-∪, res-decomp, ∪ˡsingleton∈dom, ∪ˡsingleton∉dom, ∪ˡsingleton0≡, sumConstZero, indexedSumL-proj₂-zero, setToList-∈, and a relocation of the existing ≡ᵉ-getCoin into the ⦃ DecEq A ⦄ module (so callers no longer pass A/the instance explicitly).

Conway PoV proofs — drop the now-provable assumptions, using the Prelude lemmas instead:

File	Change
Certs/Properties/PoV	drop indexedSumᵛ'-∪, sumConstZero, res-decomp, getCoin-cong parameters; keep only ≡ᵉ-getCoinˢ'
Certs/Properties/PoVLemmas	remove the local ∪ˡsingleton* / getCoin-singleton helpers and the indexedSumᵛ'-∪ assumption module; qualify IsEquivalence as Eq.IsEquivalence
Ledger/Properties/PoV	drop the same four parameters; keep only ≡ᵉ-getCoinˢ
Conformance/Properties	drop the indexedSum-∪⁺-hom parameter
Utxo/Properties/GenMinSpend	use the hoisted getCoin-singleton

Notes

• No spec-semantic change (proof refactor only) → no CHANGELOG.md entry.
• This PR is foundational: the LEDGER-pov line ([Dijkstra] CIP-159-11c: Prove LEDGER preservation of value (#1187) #1203 and its follow-ups) also consumes some of these Ledger.Prelude lemmas via Entities/Properties/ApplyToRewardsPoV. The plan is to merge this first, then rebase 1187-dijkstra-NEW-ENTITIES-ledger-pov onto master so this cleanup drops out of [Dijkstra] CIP-159-11c: Prove LEDGER preservation of value (#1187) #1203's diff. The two purely-Dijkstra helpers (sum-map-+, +-interleave) are intentionally not included here; they stay with the LEDGER-pov line where they're used.

Verification

All changed/affected modules typecheck under Agda 2.8.0 via the project Nix flake:
Ledger.Prelude, Conway/…/Certs/Properties/{PoVLemmas,PoV}, Conway/…/Ledger/Properties/PoV, Conway/…/Utxo/Properties/GenMinSpend, and Conway/Conformance/Properties — all green.

Checklist

• Commit sequence broadly makes sense and commits have useful messages
• Any semantic changes to the specifications are documented in CHANGELOG.md (n/a — proof refactor only)
• Code is formatted according to CONTRIBUTING.md
• Self-reviewed the diff

🤖 Generated with Claude Code

https://claude.ai/code/session_01We2YdXX2ozJAdAbCrRwi6r

---

Generated by Claude Code

[Copilot]

Pull request overview

This PR refactors the Conway preservation-of-value (PoV) proof stack by hoisting previously-assumed coin/map lemmas into Ledger.Prelude, then removing those assumptions from downstream PoV modules so the proofs rely on reusable Prelude facts instead.

Changes:

• Add reusable finite-map / coin-sum lemmas to Ledger.Prelude (e.g., singleton coin sum, union homomorphism, constMap-zero sum, restriction decomposition).
• Simplify Conway PoV proof modules (Certs / Ledger) by dropping now-provable lemma parameters and using the Prelude versions.
• Update a conformance property module signature to remove an unneeded indexed-sum union homomorphism parameter.

Reviewed changes

Copilot reviewed 6 out of 6 changed files in this pull request and generated 4 comments.

Show a summary per file

File	Description
src/Ledger/Prelude.lagda.md	Adds reusable coin/map lemmas (singleton, union, restriction decomposition, constMap zero-sum, setToList membership).
src/Ledger/Conway/Specification/Utxo/Properties/GenMinSpend.lagda.md	Switches to the hoisted getCoin-singleton lemma (removes local helper).
src/Ledger/Conway/Specification/Ledger/Properties/PoV.lagda.md	Drops several previously-parameterized assumptions; keeps only the remaining injectivity-based assumption.
src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md	Removes local singleton/union helpers and assumption module; qualifies IsEquivalence usage.
src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md	Drops now-provable assumptions from Certs-PoV module parameters.
src/Ledger/Conway/Conformance/Properties.lagda.md	Removes an unused indexedSum-∪⁺-hom module parameter.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[carlostome]

LGTM!